ATL with Strategy Contexts and Bounded Memory

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 boundedmemory case.

• Type: Conference
• Year: 2009
• Where: LFCS
• Authors: Thomas Brihaye, Arnaud Da Costa Lopes, François Laroussinie, Nicolas Markey
• Keywords: Alternating-time Temporal Logics, Extension Makes Strategy, LFCS 2009, Strategy Quantifiers