Advertisement
Published in:
2009 | OriginalPaper | Chapter
ATL with Strategy Contexts and Bounded Memory
Authors : Thomas Brihaye, Arnaud Da Costa, François Laroussinie, Nicolas Markey
Published in: Logical Foundations of Computer Science
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.