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 |