Sciweavers

Share
DALT
2008
Springer

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

9 years 7 months ago
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.
Dimitar P. Guelev, Catalin Dima
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where DALT
Authors Dimitar P. Guelev, Catalin Dima
Comments (0)
books