ATL* Satisfiability Is 2EXPTIME-Complete

DOI10.1007/978-3-540-70583-3_31MaRDI QIDQ3519515zbMATH OpenOpenAlexFDO

Authors 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) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• ATL Satisfiability is Indeed EXPTIME-complete
• Deciding \(\mathsf {ATL}^*\) satisfiability by tableaux
• Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+
• On the complexity of \(\mathsf{ATL}\) and \(\mathsf{ATL}^*\) module checking
• Alternating-time temporal logic

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3767031 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 1500644 (Why is no real title available?)
• ATL Satisfiability is Indeed EXPTIME-complete
• Alternating tree automata, parity games, and modal -calculus
• Alternating-time temporal logic
• An automata-theoretic approach to branching-time model checking
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Bounded Synthesis
• Church's Problem Revisited
• Safraless Compositional Synthesis
• Satisfiability and Finite Model Property for the Alternating-Time μ-Calculus

Cited in

(25)

• Undecidability of QLTL and QCTL with two variables and one monadic predicate letter
• Optimal tableau method for constructive satisfiability testing and model synthesis in the alternating-time temporal logic \(\mathrm{ATL}^+\)
• On the complexity of \(\mathsf{ATL}\) and \(\mathsf{ATL}^*\) module checking
• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• HyperLTL Satisfiability Is Σ₁¹-Complete, HyperCTL* Satisfiability Is Σ₁²-Complete.
• ATL Satisfiability is Indeed EXPTIME-complete
• scientific article; zbMATH DE number 7445162 (Why is no real title available?)
• Solving parity games via priority promotion
• Alternating-time temporal logics with linear past
• Results on alternating-time temporal logics with linear past
• Model checking and strategy synthesis for multi-agent systems for resource allocation
• Module checking of pushdown multi-agent systems
• Natural strategic ability
• Priority promotion with Parysian flair
• Taming strategy logic: non-recurrent fragments
• Model-checking iterated games
• A tableau for bundled strategies
• Complexity of finite-variable fragments of propositional temporal and modal logics of computation
• On satisfiability in ATL with strategy contexts
• Reasoning about strategies: on the model-checking problem
• Robust worst cases for parity games algorithms
• Plan logic
• Deciding \(\mathsf {ATL}^*\) satisfiability by tableaux
• Robust alternating-time temporal logic
• Model checking open systems with alternating projection temporal logic

This page was built for publication: ATL* Satisfiability Is 2EXPTIME-Complete

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3519515)