Markovian Testing and Trace Equivalences Exactly Lump More Than Markovian Bisimilarity

The notion of equivalence that is typically used to relate Markovian process terms and to reduce their underlying state spaces is Markovian bisimilarity. The reason is that, besides being a congruence, Markovian bisimilarity is consistent with ordinary lumping, an exact aggregation for Markov chains. 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.