Study compares ways to simplify complex mathematical models in computing
A Lumpability-Driven Taxonomy of Strong and Weak Stochastic Bisimilarities with Their Congruence Properties
Logic in Computer Science
Summary
When studying systems that change over time in unpredictable ways, like queuing networks or biological processes, scientists use models called continuous-time Markov chains (CTMCs). These can get very complicated, so simplifying them without losing important details is key. The authors looked at different mathematical ways—called stochastic bisimilarities—to group parts of these models together, making them easier to analyze. They organized these methods into a clear framework, explained how they relate, and explored when these simplifications work well with certain operations in the model-building language PEPA.
continuous-time Markov chainstochastic bisimilaritylumpabilityPEPAprocess algebrastate space aggregationstrong bisimulationweak bisimulationcongruencecompositionality
Authors
Riccardo Romanello, Andrea Esposito, Marco Bernardo, Carla Piazza, Sabina Rossi
Abstract
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.