Deciding the unguarded modal -calculus

DOI10.1080/11663081.2013.861181MaRDI QIDQ4583323zbMATH OpenOpenAlexFDO

Authors Oliver Friedmann, Martin Lange

Publication date 28 August 2018

Published in Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1080/11663081.2013.861181

zbMATH Keywords

automatasatisfiability checkingtableauxfixpoints

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• The modal \(\mu \)-calculus caught off guard
• Automated Reasoning with Analytic Tableaux and Related Methods
• A tableau system for the modal \(\mu \)-calculus
• EXPTIME tableaux for the coalgebraic \(\mu\)-calculus
• A decision procedure for alternation-free modal \(\mu\)-calculi

Cites work

• scientific article; zbMATH DE number 3887063 (Why is no real title available?)
• scientific article; zbMATH DE number 3898850 (Why is no real title available?)
• scientific article; zbMATH DE number 3972842 (Why is no real title available?)
• scientific article; zbMATH DE number 1318521 (Why is no real title available?)
• scientific article; zbMATH DE number 2080055 (Why is no real title available?)
• A Deterministic Subexponential Algorithm for Solving Parity Games
• A tableau system for the modal \(\mu \)-calculus
• An automata theoretic decision procedure for the propositional mu- calculus
• An automata-theoretic approach to branching-time model checking
• CTL^* and ECTL^* as fragments of the modal -calculus
• Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Game logic is strong enough for parity games
• Infinite games played on finite graphs
• Linear Time Logics Around PSL: Complexity, Expressiveness, and a Little Bit of Succinctness
• Modal logics and mu-calculi: An introduction
• Monadic second order logic on tree-like structures
• On guarded transformation in the modal \(\mu\)-calculus
• On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic
• Propositional dynamic logic of regular programs
• Results on the propositional \(\mu\)-calculus
• Solving Parity Games in Big Steps
• The Complexity of Tree Automata and Logics of Programs

Cited in

(11)

• Coalgebraic satisfiability checking for arithmetic \(\mu\)-calculi
• A tableau system for the modal \(\mu \)-calculus
• Parity game reductions
• The modal \(\mu \)-calculus caught off guard
• Quasipolynomial computation of nested fixpoints
• On the size of disjunctive formulas in the \(\mu\)-calculus
• Automated Reasoning with Analytic Tableaux and Related Methods
• A survey on satisfiability checking for the \(\mu \)-calculus through tree automata
• Proof systems for the modal \(\mu \)-calculus obtained by determinizing automata
• On guarded transformation in the modal \(\mu\)-calculus
• NP reasoning in the monotone \(\mu\)-calculus

This page was built for publication: Deciding the unguarded modal \(\mu\)-calculus

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