Electronic Proceedings in Theoretical Computer Science (Jun 2010)

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

  • Cătălin Dima,
  • Constantin Enea,
  • Dimitar Guelev

Journal volume & issue
Vol. 25, no. Proc. GANDALF 2010
pp. 103 – 117


Read online

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.