Satisfiability of ATL with strategy contexts

François Laroussinie
(LIAFA, Univ. Paris Diderot, France)
Nicolas Markey
(LSV, ENS Cachan, France)

Various extensions of the temporal logic ATL have recently been introduced to express rich properties of multi-agent systems. Among these, ATLsc extends ATL with strategy contexts, while Strategy Logic has first-order quantification over strategies. There is a price to pay for the rich expressiveness of these logics: model-checking is non-elementary, and satisfiability is undecidable.

We prove in this paper that satisfiability is decidable in several special cases. The most important one is when restricting to turn-based games. We prove that decidability also holds for concurrent games if the number of moves available to the agents is bounded. Finally, we prove that restricting strategy quantification to memoryless strategies brings back undecidability.

In Gabriele Puppis and Tiziano Villa: Proceedings Fourth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2013), Borca di Cadore, Dolomites, Italy, 29-31th August 2013, Electronic Proceedings in Theoretical Computer Science 119, pp. 208–223.
Published: 16th July 2013.

ArXived at: https://dx.doi.org/10.4204/EPTCS.119.18 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org