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 unsolv-able, 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.