Skip to main content
SpringerLink
Log in

Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference

  • Conference paper
  • First Online:
Book cover Quantitative Evaluation of Systems (QEST 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11024))

Included in the following conference series:

Abstract

Probabilistic model checking for systems with large or unbounded state space is a challenging computational problem in formal modelling and its applications. Numerical algorithms require an explicit representation of the state space, while statistical approaches require a large number of samples to estimate the desired properties with high confidence. Here, we show how model checking of time-bounded path properties can be recast exactly as a Bayesian inference problem. In this novel formulation the problem can be efficiently approximated using techniques from machine learning. Our approach is inspired by a recent result in statistical physics which derived closed-form differential equations for the first-passage time distribution of stochastic processes. We show on a number of non-trivial case studies that our method achieves both high accuracy and significant computational gains compared to statistical model checking.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61474-5_75

    Chapter  Google Scholar 

  2. Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic 1(1), 162–170 (2000)

    Article  MathSciNet  Google Scholar 

  3. Azunre, P., Gomez-Uribe, C., Verghese, G.: Mass fluctuation kinetics: analysis and computation of equilibria and local dynamics. IET Syst. Biol. 5(6), 325–335 (2011)

    Article  Google Scholar 

  4. 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). https://doi.org/10.1007/10722167_28

    Chapter  Google Scholar 

  5. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Automated performance and dependability evaluation using model checking. In: Calzarossa, M.C., Tucci, S. (eds.) Performance 2002. LNCS, vol. 2459, pp. 261–289. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45798-4_12

    Chapter  MATH  Google Scholar 

  6. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524–541 (2003)

    Article  Google Scholar 

  7. Behrmann, G., David, A., Larsen, K.G., Hakansson, J., Petterson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: Proceedings of QEST 2006, pp. 125–126. IEEE Computer Society (2006)

    Google Scholar 

  8. Bortolussi, L., Cardelli, L., Kwiatkowska, M., Laurenti, L.: Approximation of probabilistic reachability for chemical reaction networks using the linear noise approximation. In: Agha, G., Van Houdt, B. (eds.) QEST 2016. LNCS, vol. 9826, pp. 72–88. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-43425-4_5

    Chapter  MATH  Google Scholar 

  9. Bortolussi, L., Hillston, J.: Fluid model checking. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 333–347. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32940-1_24

    Chapter  Google Scholar 

  10. Bortolussi, L., Hillston, J.: Model checking single agent behaviours by fluid approximation. Inf. Comput. 242(C), 183–226 (2015)

    Article  MathSciNet  Google Scholar 

  11. 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). https://doi.org/10.1007/978-3-642-40196-1_9

    Chapter  Google Scholar 

  12. Bortolussi, L., Lanciani, R.: Stochastic approximation of global reachability probabilities of Markov population models. In: Horváth, A., Wolter, K. (eds.) EPEW 2014. LNCS, vol. 8721, pp. 224–239. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10885-8_16

    Chapter  Google Scholar 

  13. Bortolussi, L., Lanciani, R., Nenzi, L.: Model checking Markov population models by stochastic approximations. CoRR, abs/1711.03826 (2017)

    Google Scholar 

  14. Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous time Markov chains. Inform. Comput. 247, 235–253 (2016)

    Article  MathSciNet  Google Scholar 

  15. Bradley, J.T., Hayden, R.A., Clark, A.: Performance specification and evaluation with unified stochastic probes and fluid analysis. IEEE Trans. Softw. Eng. 39, 97–118 (2013)

    Article  Google Scholar 

  16. Cseke, B., Opper, M., Sanguinetti, G.: Approximate inference in latent Gaussian-Markov models from continuous time observations. In: Proceedings of NIPS, pp. 971–979. Curran Associates Inc. (2013)

    Google Scholar 

  17. Cseke, B., Schnoerr, D., Opper, M., Sanguinetti, G.: Expectation propagation for continuous-time stochastic processes. J. Phys. A-Math. Theor. 49(49), 494002 (2016)

    Article  MathSciNet  Google Scholar 

  18. Durrett, R.: Essentials of Stochastic Processes. Springer, New York (2012)

    Book  Google Scholar 

  19. Feng, C., Hillston, J., Galpin, V.: Automatic moment-closure approximation of spatially distributed collective adaptive systems. ACM Trans. Model. Comput. Simul. 26(4), 26:1–26:22 (2016)

    Article  MathSciNet  Google Scholar 

  20. Gardiner, C.W.: Handbook of Stochastic Methods, vol. 3. Springer, Berlin (1985)

    Google Scholar 

  21. Goodman, L.A.: Population growth of the sexes. Biometrics 9(2), 212–225 (1953)

    Article  MathSciNet  Google Scholar 

  22. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512–535 (1994)

    Article  Google Scholar 

  23. Haseltine, E.L., Rawlings, J.B.: Approximate simulation of coupled fast and slow reactions for stochastic chemical kinetics. J. Chem. Phys. 117(15), 6959 (2002)

    Article  Google Scholar 

  24. Hayden, R.A., Stefanek, A., Bradley, J.T.: Fluid computation of passage-time distributions in large Markov models. In: Proceedings of QAPL, vol. 413, pp. 106–141 (2012)

    Google Scholar 

  25. Hespanha, J.P.: StochDynTools – a MATLAB toolbox to compute moment dynamics for stochastic networks of bio-chemical reactions

    Google Scholar 

  26. Katoen, J.-P., Khattri, M., Zapreevt, I.S.: A Markov reward model checker. In: Proceedings of QEST, pp. 243–244. IEEE Computer Society (2005)

    Google Scholar 

  27. Kierzek, A.M.: STOCKS: STOChastic Kinetic Simulations of biochemical systems with Gillespie algorithm. Bioinformatics 18(3), 470–481 (2002)

    Article  Google Scholar 

  28. 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). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  29. Maybeck, P.S.: Stochastic Models, Estimation, and Control. Academic Press, New York (1982)

    MATH  Google Scholar 

  30. Milios, D., Sanguinetti, G., Schnoerr, D.: Probabilistic model checking for continuous-time Markov chains via sequential Bayesian inference. CoRR ArXiv, abs/1711.01863v2 (2018)

    Google Scholar 

  31. Minka, T.P.: A family of algorithms for approximate Bayesian inference. Ph.D. thesis, MIT (2001)

    Google Scholar 

  32. Norris, J.R.: Markov Chains. Cambridge University Press, Cambridge (1997)

    Book  Google Scholar 

  33. Schnoerr, D., Cseke, B., Grima, R., Sanguinetti, G.: Efficient low-order approximation of first-passage time distributions. Phys. Rev. Lett. 119, 210601 (2017)

    Article  Google Scholar 

  34. Schnoerr, D., Sanguinetti, G., Grima, R.: Validity conditions for moment closure approximations in stochastic chemical kinetics. J. Chem. Phys. 141(8), 08B616\_1 (2014)

    Article  Google Scholar 

  35. Schnoerr, D., Sanguinetti, G., Grima, R.: Comparison of different moment-closure approximations for stochastic chemical kinetics. J. Chem. Phys. 143(18), 11B610\_1 (2015)

    Article  Google Scholar 

  36. Schnoerr, D., Sanguinetti, G., Grima, R.: Approximation and inference methods for stochastic biochemical kinetics - a tutorial review. J. Phys. A 50(9), 093001 (2017)

    Article  MathSciNet  Google Scholar 

  37. Younes, H.L., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Inf. Comput. 204(9), 1368–1409 (2006)

    Article  MathSciNet  Google Scholar 

  38. Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Simulink/Stateflow verification. In: Proceedings of HSCC, pp. 243–252. ACM (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Data Science, EURECOM, Biot, France

    Dimitrios Milios

  2. School of Informatics, University of Edinburgh, Edinburgh, UK

    Dimitrios Milios, Guido Sanguinetti & David Schnoerr

  3. SynthSys, Centre for Synthetic and Systems Biology, University of Edinburgh, Edinburgh, UK

    Guido Sanguinetti

  4. Centre for Integrative Systems Biology and Bioinformatics, Department of Life Sciences, Imperial College London, London, UK

    David Schnoerr

Authors
  1. Dimitrios Milios
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Guido Sanguinetti
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. David Schnoerr
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dimitrios Milios .

Editor information

Editors and Affiliations

  1. Macquarie University , Sydney, New South Wales, Australia

    Annabelle McIver

  2. University of Turin , Turin, Italy

    Andras Horvath

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Milios, D., Sanguinetti, G., Schnoerr, D. (2018). Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference. In: McIver, A., Horvath, A. (eds) Quantitative Evaluation of Systems. QEST 2018. Lecture Notes in Computer Science(), vol 11024. Springer, Cham. https://doi.org/10.1007/978-3-319-99154-2_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-99154-2_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-99153-5

  • Online ISBN: 978-3-319-99154-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation