Lumping-Based Equivalences in Markovian Automata and Applications to Product-Form Analyses

The analysis of models specified with formalisms like Markovian process algebras or stochastic automata can be based on equivalence relations among the states. In this paper we introduce a relation called exact equivalence that, differently from most aggegation approaches, induces an exact lumping on the underlying Markov chain instead of a strong lumping. We prove that this relation is a congruence for Markovian process algebras and stochastic automata whose synchronisation semantics can be seen as the master/slave synchronisation of the Stochastic Automata Networks (SAN). We show the usefulness of this relation by proving that the class of quasi-reversible models is closed under exact equivalence. Quasi-reversibility is a pivotal property to study product-form models, i.e., models whose equilibrium behaviour can be computed very efficiently without the problem of the state space explosion. Hence, exact equivalence turns out to be a theoretical tool to prove the product-form of models by showing that they are exactly equivalent to models which are known to be quasi-reversible.