Verifying agents with memory is harder than it seemed

9 years 1 months ago
Verifying agents with memory is harder than it seemed
ATL+ is a variant of 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 P 3 -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 is not correct. That is, we prove that model checking ATL+ for agents that use strategies with memory is in fact PSPACE-complete. On a more optimistic note, we show that fairness constraints can be added to ATL+ without further increasing the complexity of model checking, which makes ATL+ an attractive alternative to the full language of ATL . Categories and Subject Descriptors I.2.11 [Artificial Intelligence]: Distributed Artificial Intelligence--Multiagent Systems; I.2.4 [Artificial Intelligence]: Knowledge Representation Formalisms and Methods--Modal logic General Terms Theory, Verification Keywords Strategic logic,...
Nils Bulling, Wojciech Jamroga
Added 06 Dec 2010
Updated 06 Dec 2010
Type Conference
Year 2010
Where ATAL
Authors Nils Bulling, Wojciech Jamroga
Comments (0)