A Note on the Congruence Proof for Recursion in Markovian Bisimulation Equivalence
Mario Bravetti, Marco Bernardo, Roberto Gorrieri · 2011
This note repairs some inaccuraces in the congruence proof for recursion previously developed for EMPA. We provide a revised proof based on standard machinery obtained by smoothly extending Milner's technique based on bisimulation up to. The machinery we introduce can be easily adapted in order to obtain accurate proofs for any other Markovian process algebra. 1 Introduction The Markovian process algebras presented in the literature are endowed with a notion of strong Markovian bisimulation equivalence in the style of [5] accounting for both functional and performance aspects. These equivalences are shown to be congruences with respect to the operators as well as recursion. To the best of our knowledge, only in [4, 1] complete proofs of congruence for recursion have been given. The proofs follow Milner's technique of bisimulation up to [6]. A particular relation B is introduced such that if we are able to prove that B is a bisimulation up to then we can conclude that recursion satisfy...