Derivation of Characteristic Formulae

This paper shows how modal mu-calculus formulae characterizing finite-state processes up to strong or weak bisimulation can be derived directly from the well-known greatest fixpoint characterizations of the bisimulation relations. Our derivation simplifies earlier proofs for the strong bisimulation case and, by virtue of derivation, immediately generalizes to various other bisimulation-like relations, in particular weak bisimulation.

• Type: Journal
• Year: 1998
• Where: ENTCS
• Authors: Markus Müller-Olm
• Keywords: Bisimulation, ENTCS 1998, Strong Bisimulation Case, Weak Bisimulation