Lumping-based equivalences in Markovian automata and applications to product-form analyses

Abstract. The analysis of models specified with formalisms like Marko-vian 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, in-duces an exact lumping on the underlying Markov chain instead of a strong lumping. We prove that this relation is a congruence for Marko-vian process algebras and stochastic automata whose synchronisation se-mantics 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.