Abstract
Complex computer systems, from peer-to-peer networks to the spreading of computer virus epidemics, can often be described as Markovian models of large populations of interacting agents. Many properties of such systems can be rephrased as the computation of time bounded reachability probabilities. However, large population models suffer severely from state space explosion, hence a direct computation of these probabilities is often unfeasible. In this paper we present some results in estimating these probabilities using ideas borrowed from Fluid and Central Limit approximations. We consider also an empirical improvement of the basic method leveraging higher order stochastic approximations. Results are illustrated on a peer-to-peer example.
This research has been partially funded by the EU-FET project QUANTICOL (nr. 600708) and by FRA-UniTS.
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.
References
Abramov, R.: A practical computational framework for the multidimensional moment-constrained maximum entropy principle. Journal of Computational Physics 211(1), 198–209 (2006)
Andersson, H., Britton, T.: Stochastic epidemic models and their statistical analysis, vol. 151. Springer, New York (2000)
Baier, C., Boudewijn, H., 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., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)
Bortolussi, L.: Hybrid behaviour of Markov population models. CoRR, abs/1211.1643 (2012)
Bortolussi, L., Hillston, J.: Fluid model checking. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 333–347. Springer, Heidelberg (2012)
Bortolussi, L., Hillston, J.: Checking Individual Agent Behaviours in Markov Population Models by Fluid Approximation. In: Bernardo, M., de Vink, E., Di Pierro, A., Wiklicky, H. (eds.) SFM 2013. LNCS, vol. 7938, pp. 113–149. Springer, Heidelberg (2013)
Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous approximation of collective system behaviour: A tutorial. Performance Evaluation 70(5), 317–349 (2013)
Bortolussi, L., Lanciani, R.: Model checking markov population models by central limit approximation. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 123–138. Springer, Heidelberg (2013)
Bujorianu, L.M.: Stochastic Reachability Analysis of Hybrid Systems. In: Communications and Control Engineering. Springer (2012)
Ethier, S.N., Kurtz, T.G.: Markov Processes: Characterization and Convergence. Wiley (2005)
Fricker, C., Gast, N.: Incentives and redistribution in homogeneous bike-sharing systems with stations of finite capacity. EURO Journal on Transportation and Logistics, 1–31 (2012)
Grima, R.: An effective rate equation approach to reaction kinetics in small volumes: Theory and application to biochemical reactions in nonequilibrium steady-state conditions. The Journal of Chemical Physics 133(3), 035101 (2010)
Hayden, R.A.: Mean field for performance models with deterministically-timed transitions. In: Proceedings of QEST 2012, pp. 63–73 (2012)
Hayden, R.A., Bradley, J.T., Clark, A.: Performance specification and evaluation with unified stochastic probes and fluid analysis. IEEE Trans. Software Eng. 39(1), 97–118 (2013)
Hayden, R.A., Stefanek, A., Bradley, J.T.: Fluid computation of passage-time distributions in large Markov models. Theor. Comput. Sci. 413(1), 106–141 (2012)
Katoen, J.P., Khattri, M., Zapreevt, I.S.: A Markov reward model checker. In: Proceedings of QEST 2005, pp. 243–244 (2005)
Kwiatkowska, M., Norman, G., Parker, D.: Prism 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)
Norris, J.R.: Markov Chains. Cambridge University Press (1997)
Qiu, D., Srikant, R.: Modeling and performance analysis of BitTorrent-like peer-to-peer networks. In: Proceedings of ACM SIGCOMM 2004, pp. 367–378 (2004)
Stamatiou, Y.C., Spirakis, P.G., Komninos, T., Vavitsas, G.: Computer Network Epidemics: Models and Techniques for Invasion and Defense. CRC Press (2012)
Van Kampen, N.G.: Stochastic Processes in Physics and Chemistry. Elsevier (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Bortolussi, L., Lanciani, R. (2014). Stochastic Approximation of Global Reachability Probabilities of Markov Population Models. In: Horváth, A., Wolter, K. (eds) Computer Performance Engineering. EPEW 2014. Lecture Notes in Computer Science, vol 8721. Springer, Cham. https://doi.org/10.1007/978-3-319-10885-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-10885-8_16
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10884-1
Online ISBN: 978-3-319-10885-8
eBook Packages: Computer ScienceComputer Science (R0)