2015/09/24 by François Laroussinie, Nicolas Markey, Arnaud Sangnier
Computer Science · #cs.LO
paper · pdf · doi:10.4204/eptcs.193.4
published as EPTCS 193, 2015, pp. 43-57 · In Proceedings GandALF 2015, arXiv:1509.06858
arxiv created 2015/09/24 · arxiv updated 2015/09/25
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.