Abstract:
ATL is a logic for multi-agent systems that enjoys model checking linear in the size of the models. We point out that the size of an ATL model is usually exponential in the number of agents. Moreover, we establish the precise ATL model checking complexity when the number of agents is considered a parameter. It turns out that the problem is Sigma2-complete for concurrent game structures, and NP-complete for alternating transition systems. We also show that ATL model checking over the broader class of nondeterministic alternating transition systems is still NP-complete, which suggests that using the more general class of models may be convenient in practice.

Warning note: The results reported in this paper contain some minor, but important errors! In particular, they are correct only for so called ``Positive ATL'' 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: multi-agent systems, model checking, temporal logic.

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