Skip to main content
SpringerLink
Log in

Probably Approximate Safety Verification of Hybrid Dynamical Systems

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2019)

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

Included in the following conference series:

Abstract

In this paper we present a method based on linear programming that facilitates reliable safety verification of hybrid dynamical systems subject to perturbation inputs over the infinite time horizon. The verification algorithm applies the probably approximately correct (PAC) learning framework and consequently can be regarded as statistically formal verification in the sense that it provides formal safety guarantees expressed using error probabilities and confidences. The safety of hybrid systems in this framework is verified via the computation of so-called PAC barrier certificates, which can be computed by solving a linear programming problem. Based on scenario approaches, the linear program is constructed by a family of independent and identically distributed state samples. In this way we can conduct verification of hybrid dynamical systems that existing methods are not capable of dealing with. Some preliminary experiments demonstrate the performance of our approach.

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. Alur, R.: Formal verification of hybrid systems. In: EMSOFT 2011, pp. 273–278. IEEE (2011)

    Google Scholar 

  2. Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57318-6_30

    Chapter  Google Scholar 

  3. Asarin, E., Maler, O.: Achilles and the tortoise climbing up the arithmetical hierarchy. J. Comput. Syst. Sci. 57(3), 389–398 (1998)

    Article  MathSciNet  Google Scholar 

  4. Calafiore, G.C.: Random convex programs. SIAM J. Optim. 20(6), 3427–3464 (2010)

    Article  MathSciNet  Google Scholar 

  5. Campi, M.C., Garatti, S.: A sampling-and-discarding approach to chance-constrained optimization: feasibility and optimality. J. Optim. Theory Appl. 148(2), 257–280 (2011)

    Article  MathSciNet  Google Scholar 

  6. Campi, M.C., Garatti, S., Prandini, M.: The scenario approach for systems and control design. Annu. Rev. Control 33(2), 149–157 (2009)

    Article  Google Scholar 

  7. Dai, L., Gan, T., Xia, B., Zhan, N.: Barrier certificates revisited. J. Symb. Comput. 80, 62–86 (2017)

    Article  MathSciNet  Google Scholar 

  8. Djaballah, A.: Computation of barrier certificates for dynamical hybrids systems using interval analysis. Université Paris-Saclay (2017)

    Google Scholar 

  9. Egyed, A.: Invited talk: a roadmap for engineering safe and secure cyber-physical systems. In: MEDI 2018, pp. 113–114 (2018)

    Google Scholar 

  10. Fränzle, M.: Analysis of hybrid systems: an ounce of realism can save an infinity of states. In: Flum, J., Rodriguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 126–139. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48168-0_10

    Chapter  Google Scholar 

  11. Fränzle, M., Gerwinn, S., Kröger, P., Abate, A., Katoen, J.-P.: Multi-objective parameter synthesis in probabilistic hybrid systems. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 93–107. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22975-1_7

    Chapter  MATH  Google Scholar 

  12. Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. J. Satisf. Boolean Model. Comput. 1, 209–236 (2007)

    MATH  Google Scholar 

  13. Fränzle, M., Shirmohammadi, M., Swaminathan, M., Worrell, J.: Costs and rewards in priced timed automata. In: ICALP 2018, pp. 125:1–125:14 (2018)

    Google Scholar 

  14. Gao, S., Avigad, J., Clarke, E.M.: Delta-decidability over the reals. In: LICS 2012, pp. 305–314 (2012)

    Google Scholar 

  15. Haussler, D.: Probably approximately correct learning. Computer Research Laboratory, University of California, Santa Cruz (1990)

    Google Scholar 

  16. Henrion, D., Lasserre, J.B., Savorgnan, C.: Approximate volume and integration for basic semialgebraic sets. SIAM Rev. 51(4), 722–743 (2009)

    Article  MathSciNet  Google Scholar 

  17. Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)

    Article  MathSciNet  Google Scholar 

  18. Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58(301), 13–30 (1963)

    Article  MathSciNet  Google Scholar 

  19. Huang, C., Chen, X., Lin, W., Yang, Z., Li, X.: Probabilistic safety verification of stochastic hybrid systems using barrier certificates. ACM Trans. Embed. Comput. Syst. 16(5), 186:1–186:19 (2017)

    Google Scholar 

  20. Kong, H., Bogomolov, S., Schilling, C., Jiang, Y., Henzinger, T.A.: Safety verification of nonlinear hybrid systems based on invariant clusters. In: HSCC 2017, pp. 163–172. ACM (2017)

    Google Scholar 

  21. Kong, H., He, F., Song, X., Hung, W.N.N., Gu, M.: Exponential-condition-based barrier certificate generation for safety verification of hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 242–257. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_17

    Chapter  Google Scholar 

  22. Lin, W., Wu, M., Yang, Z., Zeng, Z.: Exact safety verification of hybrid systems using sums-of-squares representation. Sci. China Inf. Sci. 57(5), 1–13 (2014)

    Article  MathSciNet  Google Scholar 

  23. Nahhal, T., Dang, T.: Test coverage for continuous and hybrid systems. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 449–462. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_47

    Chapter  Google Scholar 

  24. Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24743-2_32

    Chapter  MATH  Google Scholar 

  25. Ratschan, S.: Simulation based computation of certificates for safety of dynamical systems. In: Abate, A., Geeraerts, G. (eds.) FORMATS 2017. LNCS, vol. 10419, pp. 303–317. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-65765-3_17

    Chapter  MATH  Google Scholar 

  26. Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans. Embed. Comput. S. 6(1), 8 (2007)

    Article  Google Scholar 

  27. Ratschan, S., She, Z.: Providing a basin of attraction to a target region of polynomial systems by computation of lyapunov-like functions. SIAM J. Control Optim. 48(7), 4377–4394 (2010)

    Article  MathSciNet  Google Scholar 

  28. Rohn, J.I., Kreslova, J.: Linear interval inequalities. Linear Multilinear Algebra 38, 79–82 (1994)

    Article  MathSciNet  Google Scholar 

  29. Sankaranarayanan, S., Chen, X., Ábrahám, E.: Lyapunov function synthesis using Handelman representations. In: NOLCOS 2013, pp. 576–581 (2013)

    Google Scholar 

  30. Schupp, S., et al.: Current challenges in the verification of hybrid systems. In: Berger, C., Mousavi, M.R. (eds.) CyPhy 2015. LNCS, vol. 9361, pp. 8–24. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25141-7_2

    Chapter  Google Scholar 

  31. Shmarov, F., Zuliani, P.: ProbReach: verified probabilistic delta-reachability for stochastic hybrid systems. In: HSCC 2015, pp. 134–139 (2015)

    Google Scholar 

  32. Sogokon, A., Ghorbal, K., Tan, Y.K., Platzer, A.: Vector barrier certificates and comparison systems. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 418–437. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-95582-7_25

    Chapter  Google Scholar 

  33. Xue, B. Fränzle, M., Zhan, N.: Inner-approximating reachable sets for polynomial systems with time-varying uncertainties. IEEE Trans. Autom. Control (2019)

    Google Scholar 

  34. Xue, B., She, Z., Easwaran, A.: Under-approximating backward reachable sets by polytopes. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 457–476. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_25

    Chapter  Google Scholar 

  35. Xue, B., She, Z., Easwaran, A.: Underapproximating backward reachable sets by semialgebraic sets. IEEE Trans. Autom. Control 62(10), 5185–5197 (2017)

    Article  MathSciNet  Google Scholar 

  36. Xue, B., Wang, Q., Zhan, N., Fränzle, M.: Robust invariant sets generation for state-constrained perturbed polynomial systems. In: HSCC 2019, pp. 128–137 (2019)

    Google Scholar 

  37. Zhang, Y., Yang, Z., Lin, W., Zhu, H., Chen, X., Li, X.: Safety verification of nonlinear hybrid systems based on bilinear programming. IEEE Trans. CAD Integr. Circuits Syst. 37(11), 2768–2778 (2018)

    Article  Google Scholar 

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

    Google Scholar 

Download references

Acknowledgements

Bai Xue was funded by CAS Pioneer Hundred Talents Program under grant No. Y8YC235015, NSFC under grant No. 61872341 and 61836005. Martin Fränzle was funded by Deutsche Forschungsgemeinschaft through grant FR 2715/4. Hengjun Zhao was funded by NSFC under grant No. 61702425. Naijun Zhan was funded by NSFC under grant No. 61625206 and 61732001. Arvind Easwaran was supported by the Energy Research Institute (ERI@N), NTU, Singapore.

Author information

Authors and Affiliations

  1. State Key Laboratory of Computer Science, Institute of Software, CAS, Beijing, China

    Bai Xue & Naijun Zhan

  2. University of Chinese Academy of Sciences, Beijing, China

    Bai Xue & Naijun Zhan

  3. Beijing Institute of Control Engineering, Beijing, China

    Bai Xue

  4. Carl von Ossietzky Universität Oldenburg, Oldenburg, Germany

    Martin Fränzle

  5. Southwest University, Chongqing, China

    Hengjun Zhao

  6. Nanyang Technological University, Singapore, Singapore

    Arvind Easwaran

Authors
  1. Bai Xue
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Fränzle
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Hengjun Zhao
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Naijun Zhan
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Arvind Easwaran
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Bai Xue .

Editor information

Editors and Affiliations

  1. IRIT/INPT - ENSEEIHT, Toulouse, France

    Yamine Ait-Ameur

  2. Teesside University, Middlesbrough, UK

    Shengchao Qin

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Xue, B., Fränzle, M., Zhao, H., Zhan, N., Easwaran, A. (2019). Probably Approximate Safety Verification of Hybrid Dynamical Systems. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32409-4_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32408-7

  • Online ISBN: 978-3-030-32409-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation