Deciding the unguarded modal -calculus

DOI10.1080/11663081.2013.861181zbMATH Open1398.03092OpenAlexW2049154590MaRDI QIDQ4583323FDOQ4583323

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

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

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)

Cites Work

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

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
• A survey on satisfiability checking for the \(\mu \)-calculus through tree automata
• Automated Reasoning with Analytic Tableaux and Related Methods
• 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)