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.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11576/1891881
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact