Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6873960 | Information and Computation | 2015 | 53 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
François Laroussinie, Nicolas Markey,