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)
Download Edit this record How to cite View on PhilPapers
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.
(categorize this paper)
PhilPapers/Archive ID
Revision history
Archival date: 2018-04-20
View upload history
References found in this work BETA
On Satisfiability in ATL with Strategy Contexts.Troquard, Nicolas & Walther, Dirk

Add more references

Citations of this work BETA

No citations found.

Add more citations

Added to PP index

Total views
31 ( #33,273 of 38,902 )

Recent downloads (6 months)
14 ( #25,604 of 38,902 )

How can I increase my downloads?

Monthly downloads since first upload
This graph includes both downloads from PhilArchive and clicks to external links.