Optimal Decision Procedures for Satisfiability in Fragments of Alternating-time Temporal Logics

In Rajeev Goré, Barteld Kooi & Agi Kurucz (eds.), Advances in Modal Logic, Volume 10. College Publications. pp. 234-253 (2014)
  Copy   BIBTEX


We consider several natural fragments of the alternating-time temporal logics ATL* and ATL with restrictions on the nesting between temporal operators and strategic quantifiers. We develop optimal decision procedures for satisfiability in these fragments, showing that they have much lower complexities than the full languages. In particular, we prove that the satisfiability problem for state formulae in the full `strategically flat' fragment of ATL* is PSPACE-complete, whereas the satisfiability problems in the flat fragments of ATL and ATL$^{+}$ are $\Sigma^P_3$-complete. We note that the nesting hierarchies for fragments of ATL* collapse in terms of expressiveness above nesting depth 1, hence our results cover all such fragments with lower complexities.

Author's Profile

Valentin Goranko
Stockholm University


Added to PP

102 (#55,445)

6 months
9 (#66,091)

Historical graph of downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.
How can I increase my downloads?