Skip to main content
SpringerLink
Log in

Machine Learning Methods in Statistical Model Checking and System Design – Tutorial

  • Conference paper
  • First Online:
Runtime Verification

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9333))

Abstract

Recent research has seen an increasingly fertile convergence of ideas from machine learning and formal modelling. Here we review some recently introduced methodologies for model checking and system design/parameter synthesis for logical properties against stochastic dynamical models. The crucial insight is a regularity result which states that the satisfaction probability of a logical formula is a smooth function of the parameters of a CTMC. This enables us to select an appropriate class of functional priors for Bayesian model checking and system design. We give a tutorial introduction to the statistical concepts, as well as an illustrative case study which demonstrates the usage of a newly-released software tool, U-check, which implements these methodologies.

D. Milios and G. Sanguinetti acknowledge support from the ERC under grant MLCS 306999. L.B. acknowledges partial support from EU-FET project QUANTICOL (nr. 600708), by FRA-UniTS, and by the German Research Council (DFG) as part of the Cluster of Excellence on Multimodal Computing and Interaction at Saarland University.

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

Notes

  1. 1.

    http://homepages.inf.ed.ac.uk/dmilios/ucheck.

References

  1. Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.: Model checking continuous-time Markov chains by transient analysis. In: Proceedings of CAV, pp. 358–372 (2000)

    Google Scholar 

  4. Katoen, J.-P., Khattri, M., Zapreevt, I.S.: A markov reward model checker. In: Proceedings of QEST, pp. 243–244 (2005)

    Google Scholar 

  5. Mateescu, M., Wolf, V., Didier, F., Henzinger, T.: Fast adaptive uniformisation of the chemical master equation. IET Syst. Biol. 4(6), 441–452 (2010)

    Article  Google Scholar 

  6. Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Proceeding of RV, pp. 122–135 (2010)

    Google Scholar 

  7. 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  MATH  Google Scholar 

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

    Google Scholar 

  9. Brim, L., Češka, M., Dražan, S., Šafránek, D.: Exploring parameter space of stochastic biochemical systems using quantitative model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 107–123. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  10. Češka, M., Dannenberg, F., Kwiatkowska, M., Paoletti, N.: Precise parameter synthesis for stochastic biochemical systems. In: Mendes, P., Dada, J.O., Smallbone, K. (eds.) CMSB 2014. LNCS, vol. 8859, pp. 86–98. Springer, Heidelberg (2014)

    Google Scholar 

  11. Bortolussi, L., Sanguinetti, G.: Learning and designing stochastic processes from logical constraints. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 89–105. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  12. Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous time Markov chains. CoRR arXiv:1402.1450

  13. Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: On the robustness of temporal properties for stochastic models. In: Proceedings of HSB, vol. 125. EPTCS, pp. 3–19 (2013)

    Google Scholar 

  14. Bortolussi, L., Sanguinetti, G.: Learning and designing stochastic processes from logical constraints. Logical Methods Comput. Sci. 11(2:3), 1–24 (2015)

    MathSciNet  MATH  Google Scholar 

  15. Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. Theoret. Comput. Sci. 587, 3–25 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  16. Bortolussi, L., Milios, D., Sanguinetti, G.: U-Check: model checking and parameter synthesis under uncertainty. In: Campos, J., Haverkort, B.R. (eds.) QEST 2015. LNCS, vol. 9259, pp. 89–104. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  17. Durrett, R.: Essentials of Stochastic Processes. Springer, Berlin (2012)

    Book  MATH  Google Scholar 

  18. Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous approximation of collective systems behaviour: a tutorial. Perform. Eval. 70(5), 317–349 (2013)

    Article  Google Scholar 

  19. Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  20. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  21. Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  22. Donzé, A., Ferrère, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264–279. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  23. Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Time-bounded verification of CTMCs against real-time specifications. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 26–42. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  24. Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. J. Phys. Chem. 81(25), 2340–2361 (1977)

    Article  Google Scholar 

  25. Bishop, C.M.: Pattern Recognition and Machine Learning. Springer, Berlin (2006)

    MATH  Google Scholar 

  26. Rasmussen, C.E., Williams, C.K.I.: Gaussian Processes for Machine Learning. MIT Press, Caambridge (2006)

    MATH  Google Scholar 

  27. Steinwart, I.: On the influence of the kernel on the consistency of support vector machines. J. Mach. Lear. Res. 2, 67–93 (2002)

    MathSciNet  MATH  Google Scholar 

  28. Andreychenko, A., Mikeev, L., Spieler, D., Wolf, V.: Approximate maximum likelihood estimation for stochastic chemical kinetics. EURASIP J. Bioinf. Syst. Biol. 1, 1–14 (2012)

    Google Scholar 

  29. Opper, M., Sanguinetti, G.: Variational inference for Markov jump processes. In: Proceedings of NIPS, pp. 1105–1112 (2007)

    Google Scholar 

  30. Srinivas, N., Krause, A., Kakade, S., Seeger, M.: Information-theoretic regret bounds for Gaussian process optimisation in the bandit setting. IEEE Trans. Inf. Theory 58(5), 3250–3265 (2012)

    Article  Google Scholar 

  31. Bartocci, E., Bortolussi, L., Sanguinetti, G.: Data-driven statistical learning of temporal logic properties. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 23–37. Springer, Heidelberg (2014)

    Google Scholar 

  32. Ciocchetta, F., Hillston, J.: Bio-PEPA: a framework for the modelling and analysis of biological systems. Theoret. Comput. Sci. 410(33–34), 3065–3084 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  33. Bortolussi, L., Galpin, V., Hillston, J.: Hybrid performance modelling of opportunistic networks. In: EPTCS, vol. 85, pp. 106–121 (2012)

    Google Scholar 

  34. Bortolussi, L., Nenzi, L.: Specifying and monitoring properties of stochastic spatio-temporal systems in signal temporal logic. In: Proceedings of VALUETOOLS (2014)

    Google Scholar 

  35. 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 

  36. Donaldson, R., Gilbert, D.: A model checking approach to the parameter estimation of biochemical pathways. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol. 5307, pp. 269–287. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  37. Bufo, S., Bartocci, E., Sanguinetti, G., Borelli, M., Lucangelo, U., Bortolussi, L.: Temporal logic based monitoring of assisted ventilation in intensive care patients. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part II. LNCS, vol. 8803, pp. 391–403. Springer, Heidelberg (2014)

    Google Scholar 

  38. Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326–340. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  39. Kong, Z., Jones, A., Ayala, A.M., Gol, E.A., Belta, C.: Temporal logic inference for classification and prediction from data. Proc. HSCC 2014, 273–282 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  40. Bortolussi, L., Milios, D., Sanguinetti, G.: Efficient stochastic simulation of systems with multiple time scales via statistical abstraction. In: Proceedings of CMSB (2015)

    Google Scholar 

  41. Legay, A., Sedwards, S.: Statistical abstraction boosts design and test efficiency of evolving critical systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part I. LNCS, vol. 8802, pp. 4–25. Springer, Heidelberg (2014)

    Google Scholar 

  42. Georgoulas, A., Clark, A., Ocone, A., Gilmore, S., Sanguinetti, G.: A subsystems approach for parameter estimation of ode models of hybrid systems. In: Proceedings of HSB, vol. 92. EPTCS (2012)

    Google Scholar 

  43. Georgoulas, A., Hillston, J., Milios, D., Sanguinetti, G.: Probabilistic programming process algebra. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 249–264. Springer, Heidelberg (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Modelling and Simulation Group, University of Saarland, Saarbrücken, Germany

    Luca Bortolussi

  2. Department of Mathematics and Geosciences, University of Trieste, Trieste, Italy

    Luca Bortolussi

  3. CNR/ISTI, Pisa, Italy

    Luca Bortolussi

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

    Dimitrios Milios & Guido Sanguinetti

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

    Guido Sanguinetti

Authors
  1. Luca Bortolussi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dimitrios Milios
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Guido Sanguinetti
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Luca Bortolussi .

Editor information

Editors and Affiliations

  1. TU Wien, Vienna, Austria

    Ezio Bartocci

  2. Max Planck Institute for Software Systems, Kaiserslautern, Germany

    Rupak Majumdar

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Bortolussi, L., Milios, D., Sanguinetti, G. (2015). Machine Learning Methods in Statistical Model Checking and System Design – Tutorial. In: Bartocci, E., Majumdar, R. (eds) Runtime Verification. Lecture Notes in Computer Science(), vol 9333. Springer, Cham. https://doi.org/10.1007/978-3-319-23820-3_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23820-3_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23819-7

  • Online ISBN: 978-3-319-23820-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation