This note repairs some inaccuracies in the congruence proof for recursion previously developed for Markovian bisimulation equivalence. 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 for EMPA can be easily adapted in order to obtain accurate proofs for any other Markovian process algebra.
A Note on the Congruence Proof for Recursion in Markovian Bisimulation Equivalence
Bernardo, Marco;
1998
Abstract
This note repairs some inaccuracies in the congruence proof for recursion previously developed for Markovian bisimulation equivalence. 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 for EMPA can be easily adapted in order to obtain accurate proofs for any other Markovian process algebra.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
