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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Alur, R.: Formal verification of hybrid systems. In: EMSOFT 2011, pp. 273–278. IEEE (2011)
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
Asarin, E., Maler, O.: Achilles and the tortoise climbing up the arithmetical hierarchy. J. Comput. Syst. Sci. 57(3), 389–398 (1998)
Calafiore, G.C.: Random convex programs. SIAM J. Optim. 20(6), 3427–3464 (2010)
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)
Campi, M.C., Garatti, S., Prandini, M.: The scenario approach for systems and control design. Annu. Rev. Control 33(2), 149–157 (2009)
Dai, L., Gan, T., Xia, B., Zhan, N.: Barrier certificates revisited. J. Symb. Comput. 80, 62–86 (2017)
Djaballah, A.: Computation of barrier certificates for dynamical hybrids systems using interval analysis. Université Paris-Saclay (2017)
Egyed, A.: Invited talk: a roadmap for engineering safe and secure cyber-physical systems. In: MEDI 2018, pp. 113–114 (2018)
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
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
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)
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)
Gao, S., Avigad, J., Clarke, E.M.: Delta-decidability over the reals. In: LICS 2012, pp. 305–314 (2012)
Haussler, D.: Probably approximately correct learning. Computer Research Laboratory, University of California, Santa Cruz (1990)
Henrion, D., Lasserre, J.B., Savorgnan, C.: Approximate volume and integration for basic semialgebraic sets. SIAM Rev. 51(4), 722–743 (2009)
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)
Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58(301), 13–30 (1963)
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)
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)
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
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)
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
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
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
Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans. Embed. Comput. S. 6(1), 8 (2007)
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)
Rohn, J.I., Kreslova, J.: Linear interval inequalities. Linear Multilinear Algebra 38, 79–82 (1994)
Sankaranarayanan, S., Chen, X., Ábrahám, E.: Lyapunov function synthesis using Handelman representations. In: NOLCOS 2013, pp. 576–581 (2013)
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
Shmarov, F., Zuliani, P.: ProbReach: verified probabilistic delta-reachability for stochastic hybrid systems. In: HSCC 2015, pp. 134–139 (2015)
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
Xue, B. Fränzle, M., Zhan, N.: Inner-approximating reachable sets for polynomial systems with time-varying uncertainties. IEEE Trans. Autom. Control (2019)
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
Xue, B., She, Z., Easwaran, A.: Underapproximating backward reachable sets by semialgebraic sets. IEEE Trans. Autom. Control 62(10), 5185–5197 (2017)
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)
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)
Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink/stateflow verification. In: HSCC 2010, pp. 243–252 (2010)
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
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
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)