Model-Checking Strategic Ability and Knowledge of the Past of Communicating Coalitions

We propose a variant of alternating 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 setting 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 to be treated as the epistemic goal of (eventually) establishing that holds and thus enables the handling of the cooperation modalities in a streamlined way.

• Type: Conference
• Year: 2008
• Where: DALT
• Authors: Dimitar P. Guelev, Catalin Dima
• Keywords: DALT 2008, Epistemic Modalities, Imperfect Information, Intelligent Agents, Perfect Recall