Nicolas Markey

Abstract

We study the alternating-time temporal logics ATL and ATL* extended with strategy contexts: these make agents commit to their strategies during the evaluation of formulas, contrary to plain ATL and ATL* where strategy quantifiers reset previously selected strategies.

We illustrate the important expressive power of strategy contexts by proving that they make the extended logics, namely ATLsc and ATLsc*, equally expressive: any formula in ATLsc* can be translated into an equivalent, linear-size ATLsc formula. Despite the high expressiveness of these logics, we prove that they remain decidable by designing a tree-automata-based algorithm for model-checking ATLsc on the full class of n-player concurrent game structures.

@inproceedings{fsttcs2010-DLM,
  author =              {Da{~}Costa, Arnaud and Laroussinie, Fran{\c c}ois
                         and Markey, Nicolas},
  title =               {{ATL} with strategy contexts: Expressiveness and
                         Model Checking},
  editor =              {Lodaya, Kamal and Mahajan, Meena},
  booktitle =           {{P}roceedings of the 30th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)},
  acronym =             {{FSTTCS}'10},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {8},
  pages =               {120-132},
  year =                {2010},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2010.120},
  abstract =            {We study the alternating-time temporal logics
                         \(\textsf{ATL}\) and~\(\textsf{ATL}^{*}\) extended
                         with strategy contexts: these make agents commit to
                         their strategies during the evaluation of formulas,
                         contrary to plain \(\textsf{ATL}\)
                         and~\(\textsf{ATL}^{*}\) where strategy quantifiers
                         reset previously selected strategies.\par We
                         illustrate the important expressive power of
                         strategy contexts by proving that they make the
                         extended logics, namely
                         \(\textsf{ATL}_{\textsf{sc}}\)
                         and~\(\textsf{ATL}_{\textsf{sc}}^{*}\), equally
                         expressive: any~formula
                         in~\(\textsf{ATL}_{\textsf{sc}}^{*}\) can be
                         translated into an equivalent, linear-size
                         \(\textsf{ATL}_{\textsf{sc}}\) formula. Despite the
                         high expressiveness of these logics, we prove that
                         they remain decidable by designing a
                         tree-automata-based algorithm for model-checking
                         \(\textsf{ATL}_{\textsf{sc}}\) on the full class of
                         \(n\)-player concurrent game structures.},
}