Compositional Abstraction of PEPA Models for Transient Analysis

Michael James Andrew Smith

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

    Abstract

    Stochastic process algebras such as PEPA allow complex stochastic models to be described in a compositional way, but this leads to state space explosion problems. To combat this, there has been a great deal of work in developing techniques for abstracting Markov chains. In particular, abstract - or interval - Markov chains allow us to aggregate states in such a way as to safely bound transient probabilities of the original Markov chain. Whilst we can apply this technique directly to a PEPA model, it requires us to obtain the CTMC of the model, whose state space may be too large to construct explicitly. In this paper, we present a compositional application of abstract Markov chains to PEPA, based on a Kronecker representation of the underlying CTMC. This can be used to bound probabilistic reachability properties in the Continuous Stochastic Logic (CSL), and we have implemented this as part of the PEPA plug-in for Eclipse. We conclude with an example application - analysing the performance of a wireless network - and use this to illustrate the impact of the choice of states to aggregate on the precision of the bounds.
    Original languageEnglish
    Title of host publicationProceedings of the 7th European Performance Engineering Workshop (EPEW 2010)
    Publication date2010
    Pages252-267
    Publication statusPublished - 2010
    Event7th European Performance Engineering Workshop - Bertinoro, Italy
    Duration: 23 Sep 201024 Sep 2010
    Conference number: 7
    http://www.sti.uniurb.it/events/epew2010/

    Workshop

    Workshop7th European Performance Engineering Workshop
    Number7
    CountryItaly
    CityBertinoro
    Period23/09/201024/09/2010
    Internet address
    SeriesLecture Notes in Computer Science
    Number6342

    Fingerprint Dive into the research topics of 'Compositional Abstraction of PEPA Models for Transient Analysis'. Together they form a unique fingerprint.

    Cite this