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

automatafixpointssatisfiability checkingtableaux

Mathematics Subject Classification ID

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

Recommendations

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

Cites work

• A Deterministic Subexponential Algorithm for Solving Parity Games
• A tableau system for the modal -calculus
• An automata theoretic decision procedure for the propositional mu- calculus
• An automata-theoretic approach to branching-time model checking
• Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
• CTL^* and ECTL^* as fragments of the modal -calculus
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Game logic is strong enough for parity games
• 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?)
• 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 -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

(12)

• Parity game reductions
• Quasipolynomial computation of nested fixpoints
• NP reasoning in the monotone \(\mu\)-calculus
• The modal -calculus caught off guard
• A tableau system for the modal -calculus
• On guarded transformation in the modal -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
• Coalgebraic satisfiability checking for arithmetic -calculi
• On the size of disjunctive formulas in the \(\mu\)-calculus
• Faster and smaller solutions of obliging games

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)