Augmenting ATL with strategy contexts

We study the extension of the alternating-time temporal logic (ATL) with strategy contexts: contrary to the original semantics, in this semantics the strategy quantifiers do not reset the previously selected strategies. We show that our extension ATL s c is very expressive, but that its decision problems are quite hard: model checking is k-EXPTIME-complete when the formula has k nested strategy quantifiers; satisfiability is undecidable, but we prove that it is decidable when restricting to turn-based games. Our algorithms are obtained through a very convenient translation to QCTL (the computation-tree logic CTL extended with atomic quantification), which we show also applies to Strategy Logic, as well as when strategy quantification ranges over memoryless strategies.

Authors

• François Laroussinie
• Nicolas Markey

Keywords

• Temporal logics
• Games for synthesis
• Model checking
• Satisfiability