Nicolas Markey

Résumé

Strategy Logic is a powerful specification language for expressing non-zero-sum properties of multi-player games. SL conveniently extends the logic ATL with explicit quantification and assignment of strategies. In this paper, we consider games over one-counter automata, and a quantitative extension 1cSL of SL with assertions over the value of the counter. We prove two results: we first show that, if decidable, model checking the so-called Boolean-goal fragment of 1cSL has non-elementary complexity; we actually prove the result for the Boolean-goal fragment of SL over finite-state games, which was an open question in (Mogavero et al. Reasoning about strategies: On the model-checking problem. 2014). As a first step towards proving decidability, we then show that the Boolean-goal fragment of 1cSL over one-counter games enjoys a nice periodicity property.

@inproceedings{fsttcs2015-BGM,
  author =              {Bouyer, Patricia and Gardy, Patrick and Markey,
                         Nicolas},
  title =               {Weighted strategy logic with boolean goals over
                         one-counter games},
  editor =              {Harsha, Prahladh and Ramalingam, G.},
  booktitle =           {{P}roceedings of the 35th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'15)},
  acronym =             {{FSTTCS}'15},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {45},
  pages =               {69-83},
  year =                {2015},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2015.69},
  abstract =            {Strategy Logic is a powerful specification language
                         for expressing non-zero-sum properties of
                         multi-player games. SL conveniently extends the
                         logic ATL with explicit quantification and
                         assignment of strategies. In this paper, we consider
                         games over one-counter automata, and a quantitative
                         extension 1cSL of SL with assertions over the value
                         of the counter. We prove two results: we first show
                         that, if decidable, model checking the so-called
                         Boolean-goal fragment of 1cSL has non-elementary
                         complexity; we actually prove the result for the
                         Boolean-goal fragment of SL over finite-state games,
                         which was an open question in (Mogavero
                         \emph{et~al.} Reasoning about strategies: On the
                         model-checking problem. 2014). As a first step
                         towards proving decidability, we then show that the
                         Boolean-goal fragment of 1cSL over one-counter games
                         enjoys a nice periodicity property.},
}