Several Markovian process calculi have been proposed in the literature,
all of which come equipped with a notion of equivalence that aims at
relating process terms that behave the same both from the functional
and the performance viewpoint.
Most of the equivalences for Markovian process calculi are based on
the bisimulation approach, while only recently alternative approaches
based on testing scenarios and traces have been considered.
Such Markovian equivalences can be compared on the basis of
- exactness of the CTMC-level aggregation they induce;
- congruence property;
- sound and complete axiomatization;
- logical characterization;
- efficient algorithms to check for them.
After recalling the basics of Markovian process calculi,
in this tutorial we present several variants of Markovian
bisimulation equivalence, then we compare it to two more
recent non-branching-time alternatives called Markovian
testing equivalence and Markovian trace equivalence.