Title: Turning Game Models Turn-Based for Model Checking Properties of Agents
Authors: Wojciech Jamroga, Computational Intelligence Group, Clausthal University of Technology
   Juergen Dix, Computational Intelligence Group, Clausthal University of Technology

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.

Warning note: 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 Home
Human Media Interaction Group @ University of Twente
Computer Science Group @ University of Gdansk Last modified 2006-12-11