Nicolas Markey

Résumé

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 ATLsc 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.

@article{icomp245()-LM,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas},
  title =               {Augmenting {ATL} with strategy contexts},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {245},
  pages =               {98-123},
  year =                {2015},
  month =               dec,
  doi =                 {10.1016/j.ic.2014.12.020},
  abstract =            {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.\par We show that our
                         extension ATLsc 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.},
}