An axiomatization of bisimulation quantifiers via the \(\mu\)-calculus (Q557788): Difference between revisions

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.