Compositional Abstraction of PEPA Models for Transient Analysis

  • Michael J. A. Smith
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6342)


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.


Markov Chain Model Check Markov Decision Process Transient Analysis Exit Rate 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    De Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford (1998)Google Scholar
  2. 2.
    Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model checking continuous-time Markov chains by transient analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 358–372. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. 3.
    Baier, C., Hermanns, H., Katoen, J.-P., Haverkort, B.R.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theoretical Computer Science 345(1), 2–26 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Dayar, T., Stewart, W.J.: Quasi-lumpability, lower-bounding coupling matrices, and nearly completely decomposable Markov chains. SIAM Journal on Matrix Analysis and Applications 18(2), 482–498 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Fecher, H., Leucker, M., Wolf, V.: Don’t know in probabilistic systems. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 71–88. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    Fourneau, J.-M., Lecoz, M., Quessette, F.: Algorithms for an irreducible and lumpable strong stochastic bound. Linear Algebra and its Applications 386, 167–185 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)CrossRefzbMATHGoogle Scholar
  8. 8.
    Hillston, J., Kloul, L.: An efficient Kronecker representation for PEPA models. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 120–135. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  9. 9.
    Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  10. 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
  11. 11.
    Katoen, J.-P., Klink, D., Neuhäußer, M.R.: Compositional abstraction for stochastic systems. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 195–211. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  12. 12.
    Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for continuous-time Markov chains. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 311–324. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  13. 13.
    Kemeny, J.G., Snell, J.L.: Finite Markov Chains. Springer, Heidelberg (1976)zbMATHGoogle Scholar
  14. 14.
    Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., New York (1994)CrossRefzbMATHGoogle Scholar
  15. 15.
    Simon, H.A., Ando, A.: Aggregation of variables in dynamic systems. Econometrica 29(2), 111–138 (1961)CrossRefzbMATHGoogle Scholar
  16. 16.
    Tribastone, M., Duguid, A., Gilmore, S.: The PEPA Eclipse plugin. SIGMETRICS Performance Evaluation Review 36(4), 28–33 (2009)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Michael J. A. Smith
    • 1
  1. 1.Department of Informatics and Mathematical ModellingDanmarks Tekniske UniversitetLyngbyDenmark

Personalised recommendations