Abstract:
In this paper we introduce and study the complexity of model checking alternating-time temporal logic (ATL) with imperfect information, using a fine-structured complexity measure. While ATL model checking with perfect information is linear in the size of the model when the number of agents is considered fixed, this is no longer true when the number of agents is considered parameters of the problem (fine structure).

Combining it with results from our previous paper, we get the surprising result that checking strategic abilities of agents under both perfect and imperfect information belong to the same complexity class: both problems are Sigma2-complete.

Warning note: The results reported in this paper contain some minor, but important errors! In particular, they are correct only for so called ``Positive ATLir'' that allows for negation only on the level of propositions. A thorough (and correct) survey of complexity results for model checking of several ATL variants can be found in: Wojciech Jamroga and Juergen Dix (2007), Model Checking Abilities of Agents: A Closer Look. Theory of Computing Systems, to appear soon.

Keywords: computational complexity, multi-agent systems, temporal logic, strategic ability, games with incomplete information.

Computational Intelligence Group @ Technical University of Clausthal
Human Media Interaction Group @ University of Twente
Computer Science Group @ University of Gdansk	Last modified 2005-12-11