Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall
and Communicating Coalitions (joint work with Constantin Enea and Dimitar Guelev)
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 the "Proceedings of the 1st International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2010)", Minori, Amalfi Coast, Italy, 17-18 June 2010, Electronic Proceedings in Theoretical Computer Science p. 103-117, 2010.