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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
De Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford (1998)
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)
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)
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)
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)
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)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)
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)
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)
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)
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)
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)
Kemeny, J.G., Snell, J.L.: Finite Markov Chains. Springer, Heidelberg (1976)
Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., New York (1994)
Simon, H.A., Ando, A.: Aggregation of variables in dynamic systems. Econometrica 29(2), 111–138 (1961)
Tribastone, M., Duguid, A., Gilmore, S.: The PEPA Eclipse plugin. SIGMETRICS Performance Evaluation Review 36(4), 28–33 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Smith, M.J.A. (2010). Compositional Abstraction of PEPA Models for Transient Analysis. In: Aldini, A., Bernardo, M., Bononi, L., Cortellessa, V. (eds) Computer Performance Engineering. EPEW 2010. Lecture Notes in Computer Science, vol 6342. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15784-4_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-15784-4_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15783-7
Online ISBN: 978-3-642-15784-4
eBook Packages: Computer ScienceComputer Science (R0)