Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions

Cătălin Dima
(LACL, Université Paris-Est Créteil)
Constantin Enea
(LIAFA, CNRS UMR 7089, Université Paris Diderot - Paris 7)
Dimitar Guelev
(Section of Logic, Institute of Mathematics and Informatics, Bulgarian Academy of Sciences)

We present a variant of ATL with distributed knowledge operators based on a synchronous and perfect recall semantics. The coalition modalities in this logic are based on partial observation of the full history, and incorporate a form of cooperation between members of the coalition in which agents issue their actions based on the distributed knowledge, for that coalition, of the system history. We show that model-checking is decidable for this logic. The technique utilizes two variants of games with imperfect information and partially observable objectives, as well as a subset construction for identifying states whose histories are indistinguishable to the considered coalition.

In Angelo Montanari, Margherita Napoli and Mimmo Parente: Proceedings First Symposium on Games, Automata, Logic, and Formal Verification (GANDALF 2010), Minori (Amalfi Coast), Italy, 17-18th June 2010, Electronic Proceedings in Theoretical Computer Science 25, pp. 103–117.
Published: 9th June 2010.

ArXived at: bibtex PDF

Comments and questions to:
For website issues: