Stochastic Approximation of Global Reachability Probabilities of Markov Population Models

  • Luca Bortolussi
  • Roberta Lanciani
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8721)


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.


Stochastic model checking reachability hitting times fluid approximation central limit approximation linear noise approximation 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abramov, R.: A practical computational framework for the multidimensional moment-constrained maximum entropy principle. Journal of Computational Physics 211(1), 198–209 (2006)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Andersson, H., Britton, T.: Stochastic epidemic models and their statistical analysis, vol. 151. Springer, New York (2000)zbMATHGoogle Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)Google Scholar
  5. 5.
    Bortolussi, L.: Hybrid behaviour of Markov population models. CoRR, abs/1211.1643 (2012)Google Scholar
  6. 6.
    Bortolussi, L., Hillston, J.: Fluid model checking. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 333–347. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous approximation of collective system behaviour: A tutorial. Performance Evaluation 70(5), 317–349 (2013)CrossRefGoogle Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    Bujorianu, L.M.: Stochastic Reachability Analysis of Hybrid Systems. In: Communications and Control Engineering. Springer (2012)Google Scholar
  11. 11.
    Ethier, S.N., Kurtz, T.G.: Markov Processes: Characterization and Convergence. Wiley (2005)Google Scholar
  12. 12.
    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)Google Scholar
  13. 13.
    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)Google Scholar
  14. 14.
    Hayden, R.A.: Mean field for performance models with deterministically-timed transitions. In: Proceedings of QEST 2012, pp. 63–73 (2012)Google Scholar
  15. 15.
    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)CrossRefGoogle Scholar
  16. 16.
    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)CrossRefzbMATHMathSciNetGoogle Scholar
  17. 17.
    Katoen, J.P., Khattri, M., Zapreevt, I.S.: A Markov reward model checker. In: Proceedings of QEST 2005, pp. 243–244 (2005)Google Scholar
  18. 18.
    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)CrossRefGoogle Scholar
  19. 19.
    Norris, J.R.: Markov Chains. Cambridge University Press (1997)Google Scholar
  20. 20.
    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)Google Scholar
  21. 21.
    Stamatiou, Y.C., Spirakis, P.G., Komninos, T., Vavitsas, G.: Computer Network Epidemics: Models and Techniques for Invasion and Defense. CRC Press (2012)Google Scholar
  22. 22.
    Van Kampen, N.G.: Stochastic Processes in Physics and Chemistry. Elsevier (1992)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Luca Bortolussi
    • 1
    • 2
  • Roberta Lanciani
    • 3
  1. 1.DMGUniversity of TriesteItaly
  2. 2.CNR/ISTIPisaItaly
  3. 3.IMT LuccaItaly

Personalised recommendations