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