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) Delta_3 -complete for concurrent game structures, and (2) Delta_2 -complete for alternating transition systems.
In the second part, we study the model checking complexity for formulae of ATL with imperfect information (ATL_ir). We show that the problem is Delta_2 -complete n the number of transitions and the length of the formula (thereby closing a gap in previous work of chobbens). Then, we take a closer look and use the same fine structure complexity measure as we did for TL with perfect information. We get the surprising result that checking formulae of ATL_ir is also elta_3-complete in the general case, and Sigma_2-complete for ``Positive ATL_ir''. Thus, model checking agents' bilities for both perfect and imperfect information systems belongs to the same complexity class when a finer-grained analysis s used.
Kolloquium
