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 language | English |
---|---|
Title of host publication | Proceedings of the 7th European Performance Engineering Workshop (EPEW 2010) |
Publication date | 2010 |
Pages | 252-267 |
Publication status | Published - 2010 |
Event | 7th European Performance Engineering Workshop - Bertinoro, Italy Duration: 23 Sep 2010 → 24 Sep 2010 Conference number: 7 http://www.sti.uniurb.it/events/epew2010/ |
Workshop
Workshop | 7th European Performance Engineering Workshop |
---|---|
Number | 7 |
Country/Territory | Italy |
City | Bertinoro |
Period | 23/09/2010 → 24/09/2010 |
Internet address |
Series | Lecture Notes in Computer Science |
---|---|
Number | 6342 |