Model Checking Markov Population Models by Central Limit Approximation

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


In this paper we investigate the use of Central Limit Approximation of Continuous Time Markov Chains to verify collective properties of large population models, describing the interaction of many similar individual agents. More precisely, we specify properties in terms of individual agents by means of deterministic timed automata with a single global clock (which cannot be reset), and then use the Central Limit Approximation to estimate the probability that a given fraction of agents satisfies the local specification.


Stochastic model checking fluid approximation central limit approximation linear noise approximation deterministic timed automata continuous stochastic logic 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Andersson, H., Britton, T.: Stochastic Epidemic Models and Their Statistical Analysis. Springer (2000)Google Scholar
  2. 2.
    Baier, C., Cloth, L., Haverkort, B.R., Kuntz, M., Siegle, M.: Model checking markov chains with actions and state labels. IEEE Trans. Software Eng. 33(4), 209–224 (2007)CrossRefGoogle Scholar
  3. 3.
    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
  4. 4.
    Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)Google Scholar
  5. 5.
    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
  6. 6.
    Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous approximation of collective systems behaviour: A tutorial. Perf. Eval (2013)Google Scholar
  7. 7.
    Bortolussi, L., Policriti, A.: Dynamical systems and stochastic programming: To ordinary differential equations and back. Trans. Comp. Sys. Bio. XI (2009)Google Scholar
  8. 8.
    Chen, T., Han, T., Katoen, J.P., Mereacre, A.: Model checking of continuous-time Markov chains against timed automata specifications. Logical Methods in Computer Science 7(1) (2011)Google Scholar
  9. 9.
    Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with csl{ TA}. IEEE Trans. Software Eng. 35(2), 224–240 (2009)CrossRefGoogle Scholar
  10. 10.
    Ethier, S.N., Kurtz, T.G.: Markov Processes: Characterization and Convergence. Wiley (2005)Google Scholar
  11. 11.
    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
  12. 12.
    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)MathSciNetzbMATHCrossRefGoogle Scholar
  13. 13.
    Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. Theor. Comput. Sci (2007)Google Scholar
  14. 14.
    Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218–234. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  15. 15.
    Kolesnichenko, A., Remke, A., de Boer, P.-T., Haverkort, B.R.: Comparison of the mean-field approach and simulation in a peer-to-peer botnet case study. In: Thomas, N. (ed.) EPEW 2011. LNCS, vol. 6977, pp. 133–147. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  16. 16.
    Kolesnichenko, A., Remke, A., de Boer, P.T., Haverkort, B.R.: A logic for model-checking of mean-field models. In: Proc. of DSN (2013)Google Scholar
  17. 17.
    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
  18. 18.
    Rasmussen, C.E., Williams, C.K.I.: Gaussian Processes for Machine Learning. MIT Press (2006)Google Scholar
  19. 19.
    Tribastone, M., Gilmore, S., Hillston, J.: Scalable differential analysis of process algebra models. IEEE Trans. Software Eng. 38(1), 205–219 (2012)CrossRefGoogle Scholar
  20. 20.
    Van Kampen, N.G.: Stochastic Processes in Physics and Chemistry. Elsevier (1992)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Luca Bortolussi
    • 1
    • 2
  • Roberta Lanciani
    • 3
  1. 1.Department of Mathematics and GeosciencesUniversity of TriesteItaly
  2. 2.CNR/ISTIPisaItaly
  3. 3.IMT LuccaItaly

Personalised recommendations