ATL with strategy contexts and bounded memory

Abstract

We extend the alternating-time temporal logics ATL and ATL* with strategy contexts and memory constraints: the first extension makes strategy quantifiers to not "forget" the strategies being executed by the other players. The second extension allows strategy quantifiers to restrict to memoryless or bounded-memory strategies. We first consider expressiveness issues.We show that our logics can express important properties such as equilibria, and we formally compare them with other similar formalisms (ATL, ATL* , Game Logic, Strategy Logic, ⋯). We then address the problem of model-checking for our logics, especially we provide a PSPACE algorithm for the sublogics involving only memoryless strategies and an EXPSPACE algorithm for the bounded-memory case. © Springer-Verlag Berlin Heidelberg 2009.