Compositional Abstraction of PEPA Models for Transient Analysis
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.
KeywordsMarkov Chain Model Check Markov Decision Process Transient Analysis Exit Rate
Unable to display preview. Download preview PDF.
- 1.De Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford (1998)Google Scholar
- 10.Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS 1991: Proceedings of Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, The Netherlands, pp. 266–277 (1991)Google Scholar