Optimal decision procedures for satisfiability in fragments of alternating-time temporal logics

Valentin Goranko, Steen Vester

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


We consider several natural fragments of the alternating-time temporal logics ATL*and ATL with restrictions on the nesting between temporal operators and strate-gicquantifiers. We develop optimal decision procedures for satisfiability in these fragments, showing that they have much lower complexities than the fulllanguages. In particular, we prove that the satisfiability problem for stateformulae in the full ‘strategically at’ fragment of ATL* is PSPACE-complete,whereas the satisfiability problems in the at fragments of ATL and ATL+ are ∑P3-complete. We note that the nesting hierarchiesfor fragments of ATL* collapse in terms of expressiveness above nesting depth 1,hence our results cover all such fragments with lower complexities.

Original languageEnglish
Title of host publicationProceedings of Advances in Modal Logic 2014
EditorsRajeev Gore, Barteld Kooi, Agi Kurucz
PublisherCollege Publications
Publication date2014
ISBN (Print)978-1-84890-151-3
Publication statusPublished - 2014
EventAdvances in Modal Logic 2014 - Groningen, Netherlands
Duration: 5 Aug 20148 Aug 2014
Conference number: 10


ConferenceAdvances in Modal Logic 2014
SeriesAdvances in Modal Logic


  • Satisfiability
  • Decision Procedures
  • Alternating-time temporal logics
  • Flat Fragments
  • Complexity

Fingerprint Dive into the research topics of 'Optimal decision procedures for satisfiability in fragments of alternating-time temporal logics'. Together they form a unique fingerprint.

Cite this