A Lumpability-Driven Taxonomy of Strong and Weak Stochastic Bisimilarities with Their Congruence Properties

RESUMO

We study the relationships among the stochastic bisimulation-style equivalences over PEPA - Performance Evaluation Process Algebra definable according to the well known notions of lumpability for the continuous-time Markov chains (CTMCs) underlying process terms. Lumpability is a central tool in the analysis of a CTMC, because it results in aggregations of the state space enjoying properties that are useful for efficiently computing the state probability distribution of the original chain. At the level of process terms, various stochastic bisimilarities accounting for activity types and cumulative rates can be defined over PEPA, which induce different kinds of lumping. Since the formalisations of some of them are scattered across the literature, where they appear under different, and sometimes clashing, names, we collect them within a single, uniform framework, renaming each bisimilarity in a consistent way after the kind of lumping it induces. We present strong and weak variants of what we call ordinary, exact, and strict bisimilarities and show that they respectively induce ordinary, exact, and strict lumpings. We then organise the six bisimilarities into a taxonomy establishing all and only the inclusions holding among them. We also analyse how the taxonomy changes in three special cases: process terms whose underlying CTMCs are time reversible, process terms with no activities of unobservable types, and process terms with no recursion. The paper concludes by investigating the compositionality properties of the six bisimilarities. Some of them are not congruences with respect to the prefix and/or choice operators of PEPA. In that case we single out either a set of process terms over which congruence with respect to those operators is achieved, or the coarsest congruence with respect to them that is contained in the considered bisimilarity.