An axiomatization of bisimulation quantifiers via the \(\mu\)-calculus

DOI10.1016/j.tcs.2004.10.040zbMath1080.68078OpenAlexW2057583838MaRDI QIDQ557788

Giovanna D'Agostino, Giacomo Lenzi

Publication date: 30 June 2005

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2004.10.040

zbMATH Keywords

fixed points\(\mu\)-calculusbisimulationbisimulation quantifiersdisjunctive formulas

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Logic with extra quantifiers and operators (03C80)

Related Items

Uniform interpolation from cyclic proofs: the case of modal mu-calculus ⋮ Refinement modal logic ⋮ On modal \(\mu\)-calculus with explicit interpolants ⋮ Mathematical Logic for Life Science Ontologies ⋮ The many faces of interpolation ⋮ Some Formal Semantics for Epistemic Modesty

Cites Work

• Unnamed Item
• Characterizations of negative definability in modal logic
• Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
• A lattice-theoretical fixpoint theorem and its applications
• Automata for the modal μ-calculus and related results
• On an interpretation of second order quantification in first order intuitionistic propositional logic
• Monadic second order logic on tree-like structures
• A sheaf representation and duality for finitely presented Heyting algebras
• Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski
• An automata-theoretic approach to branching-time model checking