Abstract
We introduce an automated, formal, counterexample-based approach to synthesise Barrier Certificates (BC) for the safety verification of continuous and hybrid dynamical models. The approach is underpinned by an inductive framework: this is structured as a sequential loop between a learner, which manipulates a candidate BC structured as a neural network, and a sound verifier, which either certifies the candidate’s validity or generates counter-examples to further guide the learner. We compare the approach against state-of-the-art techniques, over polynomial and non-polynomial dynamical models: the outcomes show that we can synthesise sound BCs up to two orders of magnitude faster, with in particular a stark speedup on the verification engine (up to three orders less), whilst needing a far smaller data set (up to three orders less) for the learning part. Beyond improvements over the state of the art, we further challenge the new approach on a hybrid dynamical model and on larger-dimensional models, and showcase the numerical robustness of our algorithms and codebase.
Chapter PDF
Similar content being viewed by others
References
Alessandro Abate, Daniele Ahmed, Alec Edwards, Mirco Giacobbe, and Andrea Peruffo. FOSSIL: A Software Tool for the Formal Synthesis of Lyapunov Functions and Barrier Certificates using Neural Networks.In HSCC. ACM, 2021.
Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruffo. Formal Synthesis of Lyapunov Neural Networks. IEEE Control Systems Letters, 5(3):773–778, 2021.
Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, and Elizabeth Polgreen. Counterexample Guided Inductive Synthesis Modulo Theories. In Proceedings of CAV, LNCS 10981, pages 270–288, 2018.
Alessandro Abate, Ashish Tiwari, and Shankar Sastry. Box Invariance in Biologically-inspired Dynamical Systems. Automatica, 45(7):1601–1610, 2009.
Daniele Ahmed, Andrea Peruffo, and Alessandro Abate. Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers. In TACAS (1), volume 12078 of LNCS, pages 97–114. Springer, 2020.
Andrew J Barry, Anirudha Majumdar, and Russ Tedrake. Safety Verification of Reactive Controllers for UAV Flight in Cluttered Environments using Barrier Certificates. In 2012 IEEE International Conference on Robotics and Automation, pages 484–490. IEEE, 2012.
Urs Borrmann, Li Wang, Aaron D Ames, and Magnus Egerstedt. Control Barrier Certificates for Safe Swarm Behavior. IFAC-PapersOnLine, 48(27):68–73, 2015.
Dario Cattaruzza, Alessandro Abate, Peter Schrammel, and Daniel Kroening. Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration. Journal of Automated Reasoning, 2020.
Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural Lyapunov Control. In NeurIPS, pages 3240–3249, 2019
Liyun Dai, Ting Gan, Bican Xia, and Naijun Zhan. Barrier Certificates Revisited. Journal of Symbolic Computation, 80:62–86, 2017.
Leonardo de Moura and Nikolaj Bjørner.Z3: An Efficient SMT Solver. In TACAS, volume 4963 of LNCS, pages 337–340. Springer, 2008.
Sicun Gao, Jeremy Avigad, and Edmund M Clarke. \(\delta \)-complete Decision Procedures for Satisfiability over the Reals. In International Joint Conference on Automated Reasoning, pages 286–300. Springer, 2012.
Sicun Gao, Soonho Kong, and Edmund M Clarke. dReal: An SMT Solver for Nonlinear Theories over the Reals. In International conference on automated deduction, pages 208–214. Springer, 2013.
Hui Kong, Fei He, Xiaoyu Song, William NN Hung, and Ming Gu. Exponential-condition-based Barrier Certificate Generation for Safety Verification of Hybrid Systems. In International Conference on Computer Aided Verification, pages 242–257. Springer, 2013.
Daniel Kroening and Ofer Strichman. Decision Procedures - An Algorithmic Point of View.Springer Verlag, 2016.
Benoît Legat, Paulo Tabuada, and Raphaël M Jungers. Sum-of-Squares Methods for Controlled Invariant Sets with Applications to Model-predictive Control. Nonlinear Analysis: Hybrid Systems, 36:100858, 2020.
Jiang Liu, Naijun Zhan, Hengjun Zhao, and Liang Zou. Abstraction of Elementary Hybrid Systems by Variable Transformation. In International Symposium on Formal Methods, pages 360–377. Springer, 2015.
A. Papachristodoulou, J. Anderson, G. Valmorbida, S. Prajna, P. Seiler, and P. A. Parrilo. SOSTOOLS: Sum of squares optimization toolbox for MATLAB. http://arxiv.org/abs/1310.4716, 2013.
André Platzer and Edmund M Clarke. Computing Differential Invariants of Hybrid Systems as Fixedpoints. In International Conference on Computer Aided Verification, pages 176–189. Springer, 2008.
Stephen Prajna. Barrier Certificates for Nonlinear Model Validation. Automatica, 42(1):117–126, 2006.
Stephen Prajna and Ali Jadbabaie . Safety Verification of Hybrid Systems Using Barrier Certificates. In International Workshop on Hybrid Systems: Computation and Control, pages 477–492. Springer, 2004.
Stephen Prajna, Ali Jadbabaie , and George J Pappas . A Framework for Worst-case and Stochastic Safety Verification Using Barrier Certificates. IEEE Transactions on Automatic Control, 52(8):1415–1428, 2007.
Hadi Ravanbakhsh and Sriram Sankaranarayanan. Counter-example guided synthesis of control lyapunov functions for switched systems. In IEEE Control and Decision Conference (CDC), pages 4232–4239, 2015.
Hadi Ravanbakhsh and Sriram Sankaranarayanan. Robust Controller Synthesis of Switched Systems Using Counterexample Guided Framework. In ACM/IEEE Conference on Embedded Software (EMSOFT), pages 8:1–8:10, 2016.
Hadi Ravanbakhsh and Sriram Sankaranarayanan. Learning Control Lyapunov Functions from Counterexamples and Demonstrations. Autonomous Robots, pages 1–33, 2018.
Spencer M. Richards, Felix Berkenkamp, and Andreas Krause. The Lyapunov Neural Network: Adaptive Stability Certification for Safe Learning of Dynamical Systems. In CoRL, volume 87 of Proceedings of Machine Learning Research, pages 466–476. PMLR, 2018.
Sriram Sankaranarayanan, Xin Chen, and Erika Abraham. Lyapunov Function Synthesis using Handelman Representations. IFAC Proceedings Volumes, 46(23):576–581, 2013.
Shankar Sastry. Nonlinear Systems: Analysis, Stability and Control.Springer Verlag, 1999.
Christoffer Sloth, George J Pappas, and Rafael Wisniewski. Compositional Safety Analysis using Barrier Certificates. In Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control, pages 15–24, 2012.
Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan, and André Platzer. Vector Barrier Certificates and Comparison Systems. In International Symposium on Formal Methods, pages 418–437. Springer, 2018.
Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. Combinatorial sketching for finite programs. In Proceedings of the 12th international conference on Architectural support for programming languages and operating systems, pages 404–415, 2006.
Li Wang, Aaron D Ames, and Magnus Egerstedt. Safety Barrier Certificates for Collisions-free Multirobot Systems. IEEE Transactions on Robotics, 33(3):661–674, 2017
Xia Zeng, Wang Lin, Zhengfeng Yang, Xin Chen, and Lilei Wang. Darboux-type Barrier Certificates for Safety Verification of Nonlinear Hybrid Systems. In Proceedings of the 13th International Conference on Embedded Software, pages 1–10, 2016.
Hengjun Zhao, Xia Zeng, Taolue Chen, and Zhiming Liu. Synthesizing Barrier Certificates Using Neural Networks. In Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, HSCC ’20, New York, NY, USA, 2020. Association for Computing Machinery.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Peruffo, A., Ahmed, D., Abate, A. (2021). Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models. In: Groote, J.F., Larsen, K.G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. Lecture Notes in Computer Science(), vol 12651. Springer, Cham. https://doi.org/10.1007/978-3-030-72016-2_20
Download citation
DOI: https://doi.org/10.1007/978-3-030-72016-2_20
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-72015-5
Online ISBN: 978-3-030-72016-2
eBook Packages: Computer ScienceComputer Science (R0)