Non-Bisimulation-Based Markovian Behavioral Equivalences

The behavioral equivalence that is typically used to relate Markovian process terms and to reduce their underlying state spaces is Markovian bisimilarity. One of the reasons is that Markovian bisimilarity is consistent with ordinary lumping. The latter is an aggregation for Markov chains that is exact, hence it guarantees the preservation of the performance characteristics across Markovian bisimilar process terms. In this paper we show that two non-bisimulation-based Markovian behavioral equivalences -- Markovian testing equivalence and Markovian trace equivalence -- induce at the Markov chain level an aggregation strictly coarser than ordinary lumping that is still exact. We then show that only Markovian testing equivalence may constitute a useful alternative to Markovian bisimilarity, as it turns out to be a congruence with respect to the typical process algebraic operators, while Markovian trace equivalence is not a congruence with respect to parallel composition.