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.
|Data di pubblicazione:||2015|
|Titolo:||Lumping-Based Equivalences in Markovian Automata and Applications to Product-Form Analyses|
|Titolo del libro:||Proceedings of QEST 2015, th International Conference on Quantitative Evaluation of Systems|
|Digital Object Identifier (DOI):||http://dx.doi.org/10.1007/978-3-319-22264-6_11|
|Appare nelle tipologie:||4.1 Articolo in Atti di convegno|
File in questo prodotto:
|main.pdf||Articolo principale||Documento in Pre-print||Accesso chiuso-personale||Riservato|