Juergen Dix, Computational Intelligence Group, Clausthal University of Technology

**Abstract:**

Alternating-time temporal logic (ATL) is a logic
for reasoning about open computational systems and multi-agent
systems. It is well known that ATL model checking is
*linear in the size of the model*. We point out, however,
that the size of an ATL model is usually *exponential
in the number of agents*. When the size of models is defined in
terms of *states and agents* rather than *transitions*,
it turns out that the problem is (1) Delta3-complete for
concurrent game structures, and (2) Delta2-complete for
alternating transition systems. Moreover, for ``Positive
ATL'' that allows for negation only on the level of
propositions, model checking is (1) Sigma2-complete for
concurrent game structures, and (2) NP-complete for alternating
transition systems. We show a nondeterministic polynomial
reduction from checking arbitrary alternating transition systems
to checking turn-based transition systems, We also discuss the
determinism assumption in alternating transition systems, and show
that it can be easily removed.

In the second part of the paper, we study the model checking
complexity for formulae of *ATL with imperfect
information* (ATLir). We show that the problem is
Delta2-complete in the number of transitions and the length of
the formula (thereby closing a gap in previous work of
Schobbens). Then, we take a closer look and
use the same fine structure complexity measure as we did for
ATL with perfect information. We get the surprising result
that checking formulae of ATLir is also
Delta3-complete in the general case, and Sigma2-complete for
``Positive ATLir''. Thus, model checking agents'
abilities for both perfect and imperfect information systems
belongs to the same complexity class when a finer-grained analysis
is used.

**Keywords:** multi-agent systems, model checking, computational complexity.

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 |