Juergen Dix, Computational Intelligence Group, Clausthal University of Technology

**Abstract:**

ATL is a logic for open computational systems;
ATL model checking is known to be *linear in the size of models*.
We have already pointed out in another paper that the size of an
ATL model is usually *exponential in the number of
processes* (or agents), and we showed that the problem for
ATL semantics based on alternating transition systems is
NP-complete when the number of agents is considered
a parameter. On the other hand, it is PTIME-complete
for the special subclass of *turn-based transition
systems*. In this paper, we show a nondeterministic polynomial
reduction from model checking general ATS to model checking
turn-based ATS, thus providing another proof that the
problem is in NP. In our construction, the translation of
models and formulae are independent, which allows for
``pre-compiling'' models when one wants to check many properties
of a particular system.

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 |