Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
From MaRDI portal
Publication:1854336
DOI10.1006/inco.1999.2836zbMath1046.68628OpenAlexW2153364044MaRDI QIDQ1854336
Publication date: 14 January 2003
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/fbe03428b7ebf2b95ef178fecfa30f910eef8fa6
Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items (52)
Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS ⋮ The mu-calculus and Model Checking ⋮ Changing a Semantics: Opportunism or Courage? ⋮ $\aleph_1$ and the modal $\mu$-calculus ⋮ Program Schemata Technique to Solve Propositional Program Logics Revised ⋮ Unnamed Item ⋮ Extracting Proofs from Tabled Proof Search ⋮ Duality for modal \(\mu\)-logics ⋮ Deciding the unguarded modal -calculus ⋮ Axiomatising extended computation tree logic ⋮ Fixed point characterization of infinite behavior of finite-state systems ⋮ Contribution of Warsaw logicians to computational logic ⋮ Fixed point logics and definable topological properties ⋮ Focus-style proofs for the two-way alternation-free \(\mu \)-calculus ⋮ On the equational definition of the least prefixed point. ⋮ Fixed point logics and definable topological properties ⋮ Sahlqvist theorem for modal fixed point logic ⋮ A Buchholz rule for modal fixed point logics ⋮ Completeness for flat modal fixpoint logics ⋮ Coalgebraic semantics of modal logics: an overview ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Mathematical modal logic: A view of its evolution ⋮ Alternation-free weighted mu-calculus: decidability and completeness ⋮ Program schemata technique for propositional program logics: a 30-year history ⋮ Completions of \(\mu \)-algebras ⋮ Refinement modal logic ⋮ Completeness for \(\mu\)-calculi: a coalgebraic approach ⋮ Temporal refinements for guarded recursive types ⋮ Canonical completeness of infinitary \(\mu \) ⋮ The Modal μ-Calculus Caught Off Guard ⋮ The complexity of identifying characteristic formulae ⋮ Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics ⋮ Spatial logic of tangled closure operators and modal mu-calculus ⋮ The Recursion Scheme from the Cofree Recursive Comonad ⋮ Complete proof systems for weighted modal logic ⋮ \(\varSigma^{\mu}_2\) is decidable for \(\varPi^{\mu}_2\) ⋮ An axiomatization of bisimulation quantifiers via the \(\mu\)-calculus ⋮ Syntactic cut-elimination for a fragment of the modal mu-calculus ⋮ Beliefs supported by binary arguments ⋮ On modal \(\mu\)-calculus with explicit interpolants ⋮ Free \(\mu\)-lattices ⋮ On decidability of recursive weighted logics ⋮ Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs ⋮ On the proof theory of the modal mu-calculus ⋮ On modal \(\mu \)-calculus and Gödel-Löb logic ⋮ Domain mu-calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ EXPTIME Tableaux for the Coalgebraic μ-Calculus ⋮ Unnamed Item
Cites Work
This page was built for publication: Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
