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.
CITATION STYLE
Marin, A., & Rossi, S. (2015). Lumping-based equivalences in markovian automata and applications to product-form analyses. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9259, pp. 160–175). Springer Verlag. https://doi.org/10.1007/978-3-319-22264-6_11
Mendeley helps you to discover research relevant for your work.