Nicolas Markey

Résumé

Alternating-time temporal logic with strategy contexts (ATLsc) is a powerful formalism for expressing properties of multi-agent systems: it extends CTL with strategy quantifiers, offering a convenient way of expressing both collaboration and antagonism between several agents. Incomplete observation of the state space is a desirable feature in such a framework, but it quickly leads to undecidable verification problems. In this paper, we prove that uniform incomplete observation (where all players have the same observation) preserves decidability of the model checking problem, even for very expressive logics such as ATLsc.

@inproceedings{gandalf2015-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Sangnier, Arnaud},
  title =               {{{\(\textsf{ATL}_{\textsf{sc}}\)}} with partial
                         observation},
  editor =              {Esparza, Javier and Tronci, Enrico},
  booktitle =           {{P}roceedings of the 6th {I}nternational {S}ymposium
                         on {G}ames, {A}utomata, {L}ogics and {F}ormal
                         {V}erification ({GandALF}'15)},
  acronym =             {{GandALF}'15},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {193},
  pages =               {43-57},
  year =                {2015},
  month =               sep,
  doi =                 {10.4204/EPTCS.193.4},
  abstract =            {Alternating-time temporal logic with strategy
                         contexts ({{\(\textsf{ATL}_{\textsf{sc}}\)}}) is a
                         powerful formalism for expressing properties of
                         multi-agent systems: it~extends \textsf{CTL} with
                         \emph{strategy quantifiers}, offering a convenient
                         way of expressing both collaboration and antagonism
                         between several agents. Incomplete observation of
                         the state space is a desirable feature in such a
                         framework, but it quickly leads to undecidable
                         verification problems. In this paper, we prove that
                         \emph{uniform} incomplete observation (where all
                         players have the same observation) preserves
                         decidability of the model checking problem, even for
                         very expressive logics such as
                         {{\(\textsf{ATL}_{\textsf{sc}}\)}}.},
}