Verifying agents with memory is harder than it seemed
Nils Bulling, Wojciech Jamroga · AI Communications · 2010
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