Compositional abstractions for long-run properties of stochastic systems

Michael James Andrew Smith

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


    When analysing the performance of a system, we are often interested in long-run properties, such as the proportion of time it spends in a certain state. Stochastic process algebras help us to answer this sort of question by building a compositional model of the system, and using tools to analyse its underlying Markov chain. However, this also leads to state space explosion problems as the number of components in the model increases, which severely limits the size of models we can analyse. Because of this, we look for abstraction techniques that allow us to analyse a smaller model that safely bounds the properties of the original. In this paper, we present an approach to bounding long-run properties of models in the stochastic process algebra PEPA. We use a method called stochastic bounds to build upper and lower bounds of the underlying Markov chain that are lumpable, and therefore can be reduced in size. Importantly, we do this compositionally, so that we bound each component of the model separately, and compose these to obtain a bound for the entire model. We present an algorithm for this, based on extending the algorithm by Fourneau et al. to deal with partially-ordered state spaces. Finally, we present some results from our implementation, which forms part of the PEPA plug-in for Eclipse. We compare the precision and state space reduction with results obtained by computing long-run averages on a CTMDP-based abstraction.
    Original languageEnglish
    Title of host publication2011 Eighth International Conference on Quantitative Evaluation of Systems (QEST)
    Publication date2011
    ISBN (Print)978-1-4577-0973-9
    Publication statusPublished - 2011
    Event8th International Conference on Quantitative Evaluation of Systems - Aachen, Germany
    Duration: 5 Sep 20118 Sep 2011
    Conference number: 8


    Conference8th International Conference on Quantitative Evaluation of Systems
    Internet address


    Dive into the research topics of 'Compositional abstractions for long-run properties of stochastic systems'. Together they form a unique fingerprint.

    Cite this