ATLsc with partial observation

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

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.

In Javier Esparza and Enrico Tronci: Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2015), Genoa, Italy, 21-22nd September 2015, Electronic Proceedings in Theoretical Computer Science 193, pp. 43–57.
Published: 23rd September 2015.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: