Title: Model Checking ATL+ Is Harder than It Seemed
Authors: Nils Bulling, Clausthal University of Technology
   Wojciech Jamroga, University of Luxembourg

ATL+ is a variant of the alternating-time temporal logic that does not have the expressive power of full ATL*, but still allows for expressing some natural properties of agents. It has been believed that verification with ATL+ is Delta3-complete for both memoryless agents and players who can memorize the whole history of the game. In this paper, we show that the latter result was not correct. That is, we prove that model checking ATL+ for agents that use strategies with memory is in fact PSPACE-complete.

Keywords: Strategic logic, model checking, complexity.

Individual and Collective Reasoning Group @ University of Luxembourg Home
Computational Intelligence Group @ Clausthal University of Technology Last modified 2010-01-08