Skip to main content
SpringerLink
Log in

Multilevel Monte Carlo Method for Statistical Model Checking of Hybrid Systems

  • Conference paper
  • First Online:
Quantitative Evaluation of Systems (QEST 2017)

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

Included in the following conference series:

Abstract

We study statistical model checking of continuous-time stochastic hybrid systems. The challenge in applying statistical model checking to these systems is that one cannot simulate such systems exactly. We employ the multilevel Monte Carlo method (MLMC) and work on a sequence of discrete-time stochastic processes whose executions approximate and converge weakly to that of the original continuous-time stochastic hybrid system with respect to satisfaction of the property of interest. With focus on bounded-horizon reachability, we recast the model checking problem as the computation of the distribution of the exit time, which is in turn formulated as the expectation of an indicator function. This latter computation involves estimating discontinuous functionals, which reduces the bound on the convergence rate of the Monte Carlo algorithm. We propose a smoothing step with tunable precision and formally quantify the error of the MLMC approach in the mean-square sense, which is composed of smoothing error, bias, and variance. We formulate a general adaptive algorithm which balances these error terms. Finally, we describe an application of our technique to verify a model of thermostatically controlled loads.

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.

    Solely for simplicity of exposition, we have put two restrictions on the ct-SHS model \(\mathcal H\) in Definition 1. First, the model includes only forced jumps activated by reaching the boundaries of the invariant sets \(\partial \mathcal {X}(q),\,q\in Q\). Second, the state z(t) remains continuous at the switching times as declared in Definition 2.

  2. 2.

    We slightly abuse the notation and indicate by \(MSE({\mathcal A}_\ell )\) the mean square error of Algorithm 3 with the embedded sampling algorithm \({\mathcal A}_\ell \).

References

  1. Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), 2724–2734 (2008)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MATH  Google Scholar 

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

    Google Scholar 

  4. Bujorianu, M.L., Lygeros, J.: Reachability questions in piecewise deterministic Markov processes. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 126–140. Springer, Heidelberg (2003). doi:10.1007/3-540-36580-X_12

    Chapter  Google Scholar 

  5. Bujorianu, M.L., Lygeros, J.: General stochastic hybrid systems: modelling and optimal control. In: Proceedings of 43rd IEEE Conference Decision Control, pp. 1872–1877 (2004)

    Google Scholar 

  6. Bulychev, P., David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: Checking and distributing statistical model checking. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 449–463. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28891-3_39

    Chapter  Google Scholar 

  7. Cassandras, C.G., Lygeros, J. (eds.) Stochastic Hybrid Systems. Control Engineering, vol. 24. CRC Press, Boca Raton (2006)

    Google Scholar 

  8. Clarke, E.M., Zuliani, P.: Statistical model checking for cyber-physical systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 1–12. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24372-1_1

    Chapter  Google Scholar 

  9. Daca, P., Henzinger, T.A., Křetínský, J., Petrov, T.: Faster statistical model checking for unbounded temporal properties. ACM Trans. Comput. Logic 18(2), 12:1–12:25 (2017)

    Google Scholar 

  10. Esmaeil Zadeh Soudjani, S.: Formal abstractions for automated verification and synthesis of stochastic systems. Ph.D. thesis, Delft, NL, November 2014

    Google Scholar 

  11. Esmaeil Zadeh Soudjani, S., Abate, A.: Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM J. Appl. Dyn. Syst. 12(2), 921–956 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  12. Esmaeil Zadeh Soudjani, S., Abate, A.: Aggregation and control of populations of thermostatically controlled loads by formal abstractions. IEEE Trans. Control Syst. Technol. 23(3), 975–990 (2015)

    Article  Google Scholar 

  13. Esmaeil Zadeh Soudjani, S., Gerwinn, S., Ellen, C., Fränzle, M., Abate, A.: Formal synthesis and validation of inhomogeneous thermostatically controlled loads. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 57–73. Springer, Cham (2014). doi:10.1007/978-3-319-10696-0_6

    Google Scholar 

  14. Esmaeil Zadeh Soudjani, S., Majumdar, R., Abate, A.: Safety verification of continuous-space pure jump Markov processes. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 147–163. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_9

    Chapter  Google Scholar 

  15. Fränzle, M., Hermanns, H., Teige, T.: Stochastic satisfiability modulo theory: a novel technique for the analysis of probabilistic hybrid systems. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 172–186. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78929-1_13

    Chapter  Google Scholar 

  16. Giles, M.B., Nagapetyan, T., Ritter, K.: Adaptive Multilevel Monte Carlo Approximation of Distribution Functions. ArXiv e-prints, June 2017

    Google Scholar 

  17. Giles, M.B.: Multilevel Monte Carlo path simulation. Oper. Res. 56(3), 607–617 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  18. Giles, M.B.: Multilevel Monte Carlo methods. Acta Numer. 24, 259–328 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  19. Giles, M.B., Nagapetyan, T., Ritter, K.: Multilevel Monte Carlo approximation of distribution functions and densities. SIAM/ASA J. Uncertain. Quantif. 3(1), 267–295 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  20. Heinrich, S.: Monte Carlo complexity of global solution of integral equations. J. Complexity 14(2), 151–175 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  21. Kamgarpour, M., Ellen, C., Esmaeil Zadeh Soudjani, S., Gerwinn, S., Mathieu, J.L., Mullner, N., Abate, A., Callaway, D.S., Fränzle, M., Lygeros, J.: Modeling options for demand side participation of thermostatically controlled loads. In: International Conference on Bulk Power System Dynamics and Control, pp. 1–15, August 2013

    Google Scholar 

  22. Křetínský, J.: Survey of statistical verification of linear unbounded properties: model checking and distances, pp. 27–45. Springer, Cham (2016)

    Google Scholar 

  23. Larsen, K.G., Legay, A.: Statistical model checking past, present, and future. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 135–142. Springer, Heidelberg (2014). doi:10.1007/978-3-662-45231-8_10

    Google Scholar 

  24. Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16612-9_11

    Chapter  Google Scholar 

  25. Mathieu, J.L., Koch, S., Callaway, D.S.: State estimation and control of electric loads to manage real-time energy imbalance. IEEE Trans. Power Syst. 28(1), 430–440 (2013)

    Article  Google Scholar 

  26. Pola, G., Bujorianu, M.L., Lygeros, J., Di Benedetto, M.D.: Stochastic hybrid models: an overview. In: Analysis and Design of Hybrid Systems (2003)

    Google Scholar 

  27. Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52(8), 1415–1428 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  28. Tkachev, I., Mereacre, A., Katoen, J.-P., Abate, A.: Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems. In: Hybrid Systems: Computation and Control, pp. 293–302. ACM, New York (2013)

    Google Scholar 

  29. Wang, Y., Roohi, N., West, M., Viswanathan, M., Dullerud, G.E.: Statistical verification of dynamical systems using set oriented methods. In: Hybrid Systems: Computation and Control, pp. 169–178. ACM, New York (2015)

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Sadegh Esmaeil Zadeh Soudjani & Rupak Majumdar

  2. Department of Statistics, University of Oxford, Oxford, UK

    Tigran Nagapetyan

Authors
  1. Sadegh Esmaeil Zadeh Soudjani
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rupak Majumdar
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tigran Nagapetyan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sadegh Esmaeil Zadeh Soudjani .

Editor information

Editors and Affiliations

  1. Inria, Rennes, France

    Nathalie Bertrand

  2. University of Trieste, Trieste, Italy

    Luca Bortolussi

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Esmaeil Zadeh Soudjani, S., Majumdar, R., Nagapetyan, T. (2017). Multilevel Monte Carlo Method for Statistical Model Checking of Hybrid Systems. In: Bertrand, N., Bortolussi, L. (eds) Quantitative Evaluation of Systems. QEST 2017. Lecture Notes in Computer Science(), vol 10503. Springer, Cham. https://doi.org/10.1007/978-3-319-66335-7_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66335-7_24

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66334-0

  • Online ISBN: 978-3-319-66335-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation