Compositional Abstraction of Stochastic Process Algebra Models
Stochastic process algebras such as PEPA allow us to model the stochastic behaviour of systems in a compositional way. In the case of PEPA, a model is 'compiled' to a continuous time Markov chain (CTMC). We usually build a model because we are interested in some quantitative property of a system — for example, that 99% of requests to a server will be responded to within five seconds. Unfortunately, the more accurate our model is, the larger it tends to become — in particular, the size of the model can grow exponentially with the number of components in the system — and this makes it difficult to analyse.
In this talk, I will present two techniques for abstracting Markov chains by aggregating states, so that a model can be made small enough to analyse. These techniques (abstract Markov chains and stochastic bounds) can be used to bound transient and steady state properties of the model respectively. I will then show how they can be applied compositionally, at the level of a PEPA model, so that we can avoid constructing the underlying Markov chain (which may be too large to even represent, let alone analyse).
I have developed a graphical interface, as part of the Eclipse plug-in for PEPA, that allows abstractions of a model to be specified, and also for abstract model checking of properties in the Continuous Stochastic Logic (CSL). I will give a demonstration, and show how these techniques can be used to quickly obtain bounds on properties of interest.