An axiomatization of bisimulation quantifiers via the \(\mu\)-calculus
type: Item
instance of: scholarly article
title: An axiomatization of bisimulation quantifiers via the \(\mu\)-calculus
zbMATH Open document ID: 1080.68078
author: Giovanna D'Agostino
author: Giacomo Lenzi
published in: Theoretical Computer Science
publication date: 2005-06-30T00:00:00Z
review text: The idea of a bisimulation quantifier can be exemplified in the existential bisimulation quantifier \(\widetilde\exists\): a formula \(\widetilde\exists X\phi\) holds in a model \((M,V)\) if and only if \(\phi(X)\) holds in a model which is bisimilar to \((M,V)\) with respect to the language of \(\phi\) minus the variable \(X\). In the paper the authors establish a complete axiom system for Bisimulation Quantifiers Logic (BQL) and prove that the subsystem of BQL which contains Propositional Dynamic Logic (PDL) and the axioms and rules for bisimulation quantifiers is strong enough to deduce all theorems of \(\mu\)-calculus translated into BQL. The authors prove the latter result using the completeness of the \(\mu\)-calculus [see \textit{I. Walukiewicz}, Inf. Comput. 157, No. 1--2, 142--182 (2000; Zbl 1046.68628)]. The exposition of logical techniques in the paper is perfectly flawless. However, there is a tiny misprint in the definition of a guarded formula on page 68. The definition says: ``A formula is called guarded if, for any bound occurrence of a variable \(X\), denoting by \(\sigma X\) its fixpoint binding, then \(X\) is contained in a Cover \dots''. The definition makes sense only if we remove ``then'' from the above cited statement. But it should be mentioned that technically this misprint does not imply any difficulties, and a reader familiar with [\textit{D. Kozen}, Theor. Comput. Sci. 27, 333--354 (1983; Zbl 0553.03007)] should easily find a straightforward analogy between the definition of a guarded formula given by Kozen there and the definition used in this paper.
reviewed by: Vladimir Komendantsky
Mathematics Subject Classification ID: 68Q85
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03C80
zbMATH DE Number: 2184035
zbMATH Keywords: bisimulation
zbMATH Keywords: fixed points
zbMATH Keywords: bisimulation quantifiers
zbMATH Keywords: \(\mu\)-calculus
zbMATH Keywords: disjunctive formulas
MaRDI profile type: Publication
full work available at URL: j.tcs.2004.10.040
OpenAlex ID: W2057583838
cites work: Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski
cites work: A sheaf representation and duality for finitely presented Heyting algebras
cites work: Characterizations of negative definability in modal logic
cites work: Automata for the modal μ-calculus and related results
cites work: An automata-theoretic approach to branching-time model checking
cites work: On an interpretation of second order quantification in first order intuitionistic propositional logic
cites work: A lattice-theoretical fixpoint theorem and its applications
cites work: Q4893140
cites work: Monadic second order logic on tree-like structures
cites work: Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
DOI: 10.1016/J.TCS.2004.10.040
Recommended article: The Freedoms of (Guarded) Bisimulation
Recommended article: On modal \(\mu\)-calculus with explicit interpolants
Recommended article: Q3509051
Recommended article: Q4218096
Recommended article: Introduction to Guarded Logics
Recommended article: Beyond Bisimulation: The “up-to” Techniques
Recommended article: Q3154151
Recommended article: Q4440830
Recommended article: Tableau-based Bisimulation Invariance Testing
description: scientific article; zbMATH DE number 2184035