Juergen Dix, Computational Intelligence Group, Clausthal University of Technology

**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.

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 |