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.



External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Branching-time logics repeatedly referring to states.Volker Weber - 2009 - Journal of Logic, Language and Information 18 (4):593-624.
Decidable fragments of first-order temporal logics.Ian Hodkinson, Frank Wolter & Michael Zakharyaschev - 2000 - Annals of Pure and Applied Logic 106 (1-3):85-134.
Decidable fragments of first-order modal logics.Frank Wolter & Michael Zakharyaschev - 2001 - Journal of Symbolic Logic 66 (3):1415-1438.
Decidable Fragments of First-Order Modal Logics.Frank Wolter & Michael Zakharyaschev - 2001 - Journal of Symbolic Logic 66 (3):1415-1438.
Deciding regular grammar logics with converse through first-order logic.Stéphane Demri & Hans De Nivelle - 2005 - Journal of Logic, Language and Information 14 (3):289-329.
An Event-Based Fragment of First-Order Logic over Intervals.Savas Konur - 2011 - Journal of Logic, Language and Information 20 (1):49-68.
Alternating automata and temporal logic normal forms.Clare Dixon, Alexander Bolotov & Michael Fisher - 2005 - Annals of Pure and Applied Logic 135 (1-3):263-285.
Semantic Decision Procedures for Some Relevant Logics.Ross Brady - 2003 - Australasian Journal of Logic 1:4-27.
Lewis Dichotomies in Many-Valued Logics.Simone Bova - 2012 - Studia Logica 100 (6):1271-1290.


Added to PP

109 (#115,837)

6 months
13 (#73,664)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Valentin Goranko
Stockholm University

Citations of this work

No citations found.

Add more citations

References found in this work

On satisfiability in ATL with strategy contexts.Nicolas Troquard & Dirk Walther - 2012 - In Luis Farinas del Cerro, Andreas Herzig & Jerome Mengin (eds.), Logics in Artificial Intelligence. Springer. pp. 398--410.

Add more references