Model-checking strategic ability and knowledge of the past of communicating coalitions (joint work with Dimitar Guelev)

We propose a variant of alternated-time temporal logic ($\ATL$) with imperfect information, perfect recall, epistemic modalities for the past and strategies which are required to be uniform with respect to distributed knowledge. The model-checking problem about $\ATL$ with perfect recall and imperfect information is believed to be unsolvable, whereas in our system it is solvable because of the uniformity of strategies. We propose a model-checking algorithm for that system, which exploits the interaction between the cooperation modalities and the epistemic modality for the past.  This interaction allows every expressible goal $\varphi$ to be treated as the epistemic goal of (eventually) establishing that $\varphi$ holds and thus enables the handling of the cooperation modalities in a streamlined way.

Proceedings of 6th International Workshop on "Declarative Agent Languages and Technologies" (DALT 2008), Estoril, Portugal, May 12, 2008. Revised selected and invited papers, Lecture Notes in Computer Science vol. 5397, p. 75-90, 2008.

 gzipped postscript file.