ATL* Satisfiability Is 2EXPTIME-Complete

DOI10.1007/978-3-540-70583-3_31zbMath1155.68447OpenAlexW1566513654MaRDI QIDQ3519515

Sven Schewe

Publication date: 19 August 2008

Published in: Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-70583-3_31

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items

Optimal Tableau Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-Time Temporal Logic ATL ⁺, Deciding $$\mathsf {ATL^*}$$ Satisfiability by Tableaux, A Tableau for Bundled Strategies, Undecidability of QLTL and QCTL with two variables and one monadic predicate letter, Complexity of finite-variable fragments of propositional temporal and modal logics of computation, Model checking and strategy synthesis for multi-agent systems for resource allocation, Model-checking iterated games, Robust worst cases for parity games algorithms, Reasoning About Strategies, Taming strategy logic: non-recurrent fragments, Model checking open systems with alternating projection temporal logic, HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems, Unnamed Item, Unnamed Item, Solving parity games via priority promotion, Alternating-time temporal logics with linear past, Unnamed Item, Natural strategic ability

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• ATL Satisfiability is Indeed EXPTIME-complete
• Alternating-time temporal logic
• Bounded Synthesis
• Satisfiability and Finite Model Property for the Alternating-Time μ-Calculus
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Church's Problem Revisited
• An automata-theoretic approach to branching-time model checking
• Safraless Compositional Synthesis
• Alternating tree automata, parity games, and modal \(\mu\)-calculus