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

Abstract

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
Pages234-253
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

Conference

ConferenceAdvances in Modal Logic 2014
Number10
CountryNetherlands
CityGroningen
Period05/08/201408/08/2014
SeriesAdvances in Modal Logic
Volume10

Keywords

  • 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