Satisfiability and Finite Model Property for the Alternating-Time μ-Calculus

DOI10.1007/11874683_39MaRDI QIDQ3613365zbMATH OpenOpenAlexFDO

Authors Sven Schewe, Bernd Finkbeiner

Publication date 12 March 2009

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11874683_39

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automated Reasoning with Analytic Tableaux and Related Methods
• A decision procedure for alternation-free modal -calculi
• Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+
• scientific article; zbMATH DE number 1223729
• scientific article; zbMATH DE number 3898850

Cited in

(25)

• Solving parity games via priority promotion
• Alternating-time temporal logics with linear past
• Robust worst cases for parity games algorithms
• Model checking open systems with alternating projection temporal logic
• Satisfiability of linear time mu-calculus on finite traces
• Efficiently deciding -calculus with converse over finite trees
• Synthesising strategy improvement and recursive algorithms for solving 2.5 player parity games
• A decision procedure for alternation-free modal -calculi
• From Parity and Payoff Games to Linear Programming
• scientific article; zbMATH DE number 7445162 (Why is no real title available?)
• On the complexity of \(\mathsf{ATL}\) and \(\mathsf{ATL}^*\) module checking
• Solving parity games in big steps
• Symmetric strategy improvement
• ATL* Satisfiability Is 2EXPTIME-Complete
• Tighter Bounds for the Determinisation of Büchi Automata
• scientific article; zbMATH DE number 1223729 (Why is no real title available?)
• Results on alternating-time temporal logics with linear past
• Solving Parity Games in Big Steps
• Automated Reasoning with Analytic Tableaux and Related Methods
• Alternation-free weighted mu-calculus: decidability and completeness
• A survey on satisfiability checking for the \(\mu \)-calculus through tree automata
• Priority promotion with Parysian flair
• An objective improvement approach to solving discounted payoff games
• Module checking of pushdown multi-agent systems
• An objective improvement approach to solving discounted payoff games

This page was built for publication: Satisfiability and Finite Model Property for the Alternating-Time μ-Calculus

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