research-article

Synthesizing barrier certificates using neural networks

Authors:

Zhiming LiuAuthors Info & Claims

HSCC '20: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control

Article No.: 25, Pages 1 - 11

https://doi.org/10.1145/3365365.3382222

Published: 22 April 2020 Publication History

Abstract

This paper presents an approach of safety verification based on neural networks for continuous dynamical systems which are modeled as a system of ordinary differential equations. We adopt the deductive verification methods based on barrier certificates. These are functions over the states of the dynamical system with certain constraints the existence of which entails the safety of the system under consideration. We propose to represent the barrier function by neural networks and provide a comprehensive synthesis framework. In particular, we devise a new type of activation functions, i.e., Bent-ReLU, for the neural networks; we provide sampling based approaches to generate training sets and formulate the loss functions for neural network training which can capture the essence of barrier certificate; we also present practical methods to check a learnt candidate barrier certificate against the criteria of barrier certificates as a formal guarantee. We implement our approaches via proof-of-concept experiments with encouraging results.

References

[1]

Andrew J. Barry, Anirudha Majumdar, and Russ Tedrake. 2012. Safety verification of reactive controllers for UAV flight in cluttered environments using barrier certificates. In 2012 IEEE International Conference on Robotics and Automation, ICRA 2012. nstitute of Electrical and Electronics Engineers Inc., 484--490.

[2]

Marc Brockschmidt, Yuxin Chen, Pushmeet Kohli, Siddharth Krishna, and Daniel Tarlow. 2017. Learning Shape Analysis. In Static Analysis. Springer International Publishing, 66--87.

[3]

Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, and Naijun Zhan. 2019. NIL: Learning Nonlinear Interpolants. In Automated Deduction - CADE 27. Springer International Publishing, 178--196.

[4]

Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. 2012. Taylor Model Flowpipe Construction for Non-linear Hybrid Systems. In RTSS 2012. IEEE Computer Society, Los Alamitos, CA, USA, 183--192.

[5]

George E. Collins. 1975. Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In Automata Theory and Formal Languages, H. Brakhage (Ed.). LNCS, Vol. 33. Springer Berlin Heidelberg, 134--183.

[6]

Liyun Dai, Ting Gan, Bican Xia, and Naijun Zhan. 2017. Barrier Certificates Revisited. Journal of Symbolic Computation 80 (2017), 62--86.

Digital Library

[7]

James H. Davenport and Joos Heintz. 1988. Real quantifier elimination is doubly exponential. J. Symb. Comput. 5, 1-2 (Feb. 1988), 29--35.

Digital Library

[8]

A. Dolzmann, A. Seidl, and T. Sturm. 2006. Redlog User Manual (edition 3.1, for redlog version 3.06 (reduce 3.8) ed.). http://redlog.dolzmann.de/downloads/.

[9]

Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte, and Sanjit A. Seshia. 2019. VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems. In Computer Aided Verification. Springer International Publishing, 432--442.

[10]

Souradeep Dutta, Xin Chen, and Sriram Sankaranarayanan. 2019. Reachability analysis for neural feedback systems using regressive polynomial rule inference. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC. 157--168.

Digital Library

[11]

Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. 2018. Output Range Analysis for Deep Feedforward Neural Networks. In NASA Formal Methods. Springer International Publishing, 121--138.

[12]

P. Ezudheen, Daniel Neider, Deepak D'Souza, Pranav Garg, and P. Madhusudan. 2018. Horn-ICE learning for synthesizing invariants and contracts. PACMPL 2, OOPSLA (2018), 131:1--131:25.

Digital Library

[13]

Goran Frehse. 2008. PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf. 10, 3 (May 2008), 263--279.

[14]

Goran Frehse, Colas Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable Verification of Hybrid Systems. In CAV 2011, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). LNCS, Vol. 6806. Springer Berlin Heidelberg, 379--395.

[15]

Ting Gan, Mingshuai Chen, Liyun Dai, Bican Xia, and Naijun Zhan. 2015. Decidability of the Reachability for a Family of Linear Vector Fields. In Automated Technology for Verification and Analysis. Springer International Publishing, 482--499.

[16]

Ting Gan, Mingshuai Chen, Y. Li, Bican Xia, and Naijun Zhan. 2018. Reachability Analysis for Solvable Dynamical Systems. IEEE Trans. Automat. Control 63, 7 (2018), 2003--2018.

[17]

C. A. R. Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (Oct. 1969), 576--580.

Digital Library

[18]

Radoslav Ivanov, James Weimer, Rajeev Alur, George J. Pappas, and Insup Lee. 2019. Verisig: verifying safety properties of hybrid systems with neural network controllers. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019. 169--178.

Digital Library

[19]

Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. 2017. Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification. Springer, 97--117.

[20]

Hui Kong, Fei He, Xiaoyu Song, William NN Hung, and Ming Gu. 2013. Exponential-condition-based barrier certificate generation for safety verification of hybrid systems. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV). Springer, 242--257.

[21]

Hui Kong, Xiaoyu Song, Dong Han, Ming Gu, and Jiaguang Sun. 2014. A new barrier certificate for safety verification of hybrid systems. Comput. J. 57, 7 (2014), 1033--1045.

[22]

Gerardo Lafferriere, George J. Pappas, and Sergio Yovine. 1999. A New Class of Decidable Hybrid Systems. In HSCC 1999 (LNCS), Frits W. Vaandrager and Jan H. Schuppen (Eds.), Vol. 1569. Springer Berlin Heidelberg, 137--151.

[23]

Moshe Leshno, Vladimir Ya. Lin, Allan Pinkus, and Shimon Schocken. 1993. Multilayer feedforward networks with a nonpolynomial activation function can approximate any function. Neural Networks 6, 6 (1993), 861 -- 867.

Digital Library

[24]

Jianlin Li, Jiangchao Liu, Pengfei Yang, Liqian Chen, Xiaowei Huang, and Lijun Zhang. 2019. Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification. In Static Analysis. Springer International Publishing, 296--319.

[25]

Yi Li, Xuechao Sun, Yong Li, Andrea Turrini, and Lijun Zhang. 2019. Synthesizing Nested Ranking Functions for Loop Programs via SVM. In Formal Methods and Software Engineering. Springer International Publishing, 438--454.

[26]

Jiang Liu, Jidong Lv, Zhao Quan, Naijun Zhan, Hengjun Zhao, Chaochen Zhou, and Liang Zou. 2010. A Calculus for Hybrid CSP. In APLAS 2010, Kazunori Ueda (Ed.). LNCS, Vol. 6461. Springer Berlin Heidelberg, 1--15.

[27]

Jiang Liu, Naijun Zhan, and Hengjun Zhao. 2011. Computing semi-algebraic invariants for polynomial dynamical systems. In EMSOFT 2011. ACM, New York, NY, USA, 97--106.

Digital Library

[28]

Jiang Liu, Naijun Zhan, Hengjun Zhao, and Liang Zou. 2015. Abstraction of Elementary Hybrid Systems by Variable Transformation. In FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24--26, 2015, Proceedings. Springer, 360--377.

[29]

Johan Löfberg. 2004. YALMIP : A Toolbox for Modeling and Optimization in MATLAB. In Proc. of the CACSD Conference. Taipei, Taiwan. http://users.isy.liu.se/johanl/yalmip/.

[30]

Zhou Lu, Hongming Pu, Feicheng Wang, Zhiqiang Hu, and Liwei Wang. 2017. The Expressive Power of Neural Networks: A View from the Width. In Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, 4--9 December 2017, Long Beach, CA, USA. 6231--6239.

Digital Library

[31]

Zohar Manna andHenny B. Sipma. 1998. Deductive verification of hybrid systems using STeP. In HSCC 1998, Thomas A. Henzinger and Shankar Sastry (Eds.). LNCS, Vol. 1386. Springer Berlin Heidelberg, 305--318.

[32]

Ian Mitchell and Claire J. Tomlin. 2000. Level Set Methods for Computation in Hybrid Systems. In HSCC 2000, Nancy Lynch and Bruce H. Krogh (Eds.). LNCS, Vol. 1790. Springer Berlin Heidelberg, 310--323.

[33]

André Platzer. 2010. Differential-algebraic Dynamic Logic for Differential-algebraic Programs. J. Log. and Comput. 20, 1 (Feb. 2010), 309--352.

Digital Library

[34]

André Platzer and Edmund M. Clarke. 2008. Computing Differential Invariants of Hybrid Systems as Fixedpoints. In CAV 2008, Aarti Gupta and Sharad Malik (Eds.). LNCS, Vol. 5123. Springer Berlin Heidelberg, 176--189.

[35]

Stephen Prajna and Ali Jadbabaie. 2004. Safety Verification of Hybrid Systems Using Barrier Certificates. In Proceedings of the 7th International Workshop on Hybrid Systems: Computation and Control HSCC. 477--492.

[36]

Stephen Prajna, Ali Jadbabaie, and George J. Pappas. 2007. A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Automat. Control 52, 8 (2007), 1415--1429.

[37]

Luca Pulina and Armando Tacchella. 2010. An Abstraction-Refinement Approach to Verification of Artificial Neural Networks. In Computer Aided Verification. 243--257.

[38]

Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, Percy Liang, and Aditya V. Nori. 2013. A Data Driven Approach for Algebraic Loop Invariants. In Programming Languages and Systems. Springer Berlin Heidelberg, 574--592.

[39]

Rahul Sharma, Aditya V. Nori, and Alex. Aiken. 2012. Interpolants as Classifiers. In Computer Aided Verification. Springer Berlin Heidelberg, 71--87.

[40]

Christoffer Sloth, George J Pappas, and Rafael Wisniewski. 2012. Compositional safety analysis using barrier certificates. In Proc. of the Hybrid Systems: Computation and Control (HSCC). ACM, 15--24.

Digital Library

[41]

AndrewSogokon, Khalil Ghorbal, Yong Kiam Tan, and André Platzer. 2018. Vector Barrier Certificates and Comparison Systems. In Formal Methods. 418--437.

[42]

Xiaowu Sun, Haitham Khedr, and Yasser Shoukry. 2019. Formal verification of neural network controlled autonomous systems. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019. 147--156.

Digital Library

[43]

Tsui-Wei Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane S. Boning, and Inderjit S. Dhillon. 2018. Towards Fast Computation of Certified Robustness for ReLU Networks. In Proceedings of the 35th International Conference on Machine Learning, ICML 2018. 5273--5282.

[44]

Weiming Xiang, Hoang-Dung Tran, and Taylor T. Johnson. 2017. Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks. CoRR abs/1708.03322 (2017).

[45]

Bai Xue, Martin Fränzle, and Naijun Zhan. 2019. Inner-Approximating Reachable Sets for Polynomial Systems with Time-Varying Uncertainties. IEEE Trans. Automat. Control (2019), 1--1.

[46]

Bai Xue, Martin Fränzle, Hengjun Zhao, Naijun Zhan, and Arvind Easwaran. 2019. Probably Approximate Safety Verification of Hybrid Dynamical Systems. In Formal Methods and Software Engineering. Springer International Publishing, 236--252.

[47]

Zhengfeng Yang, Min Wu, and Wang Lin. 2015. Exact Verification of Hybrid Systems Based on Bilinear SOS Representation. (2015), 19 pages.

[48]

Xia Zeng, Wang Lin, Zhengfeng Yang, Xin Chen, and Lilei Wang. 2016. Darboux-type Barrier Certificates for Safety Verification of Nonlinear Hybrid Systems. In Proceedings of the 13th International Conference on Embedded Software. ACM, Article 11, 10 pages.

Digital Library

Cited By

Bajelani Mvan Heusden K(2024)Data-Driven Safety Filter: An Input-Output Perspective2024 American Control Conference (ACC)10.23919/ACC60939.2024.10644850(5106-5112)Online publication date: 10-Jul-2024
https://doi.org/10.23919/ACC60939.2024.10644850
Edwards APeruffo AAbate A(2024)Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical ModelsProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3651398(1-10)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3651398
Jin CMa XRen TLin WDing Z(2024)Safe Controller Synthesis for Nonlinear Systems Using Bayesian Optimization Enhanced Reinforcement LearningProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3650137(1-10)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3650137
Show More Cited By

Index Terms

Synthesizing barrier certificates using neural networks

Recommendations

Formal Synthesis of Neural Barrier Certificates for Continuous Systems via Counterexample Guided Learning
Special Issue ESWEEK 2023
This paper presents a novel approach to safety verification based on neural barrier certificates synthesis for continuous dynamical systems. We construct the synthesis framework as an inductive loop between a Learner and a Verifier based on barrier ...
Verifying Neural Network Controlled Systems Using Neural Networks
HSCC '22: Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control

Safety verification is an essential requirement of neural network controlled systems when they are adopted in safety-critical fields. This paper proposes a novel approach to synthesizing neural networks as barrier certificates, which can provide safety ...
Synthesizing ReLU neural networks with two hidden layers as barrier certificates for hybrid systems
HSCC '21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control

Barrier certificates provide safety guarantees for hybrid systems. In this paper, we propose a novel approach to synthesizing neural networks as barrier certificates. Candidate networks are trained from a special structure: ReLU neural networks ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '20: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control

April 2020

324 pages

ISBN:9781450370189

DOI:10.1145/3365365

Program Chairs:
Aaron Ames
California Institute of Technology
,
Sanjit A. Seshia
University of California, Berkeley
,
Publications Chair:
Jyotirmoy Deshmukh
University of Southern California

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication Notes

Badge change: Article originally badged under Version 1.0 guidelines https://www.acm.org/publications/policies/artifact-review-badging

Publication History

Published: 22 April 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Results Reproduced / v1.1

Author Tags

Qualifiers

Research-article

Funding Sources

National Natural Science Foundation of China
Birkbeck BEI School Project (ARTEFACT)
Guangdong Science and Technology Department grant
China's Fundamental Research Funds for the Central Universities
Capacity Development Grant of Southwest University
Basic Science and Frontier Technology Research Program of Chongqing

Conference

HSCC '20

Sponsor:

SIGBED

HSCC '20: 23rd ACM International Conference on Hybrid Systems: Computation and Control

April 22 - 24, 2020

New South Wales, Sydney, Australia

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

36
Total Citations
View Citations
737
Total Downloads

Downloads (Last 12 months)120
Downloads (Last 6 weeks)15

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bajelani Mvan Heusden K(2024)Data-Driven Safety Filter: An Input-Output Perspective2024 American Control Conference (ACC)10.23919/ACC60939.2024.10644850(5106-5112)Online publication date: 10-Jul-2024
https://doi.org/10.23919/ACC60939.2024.10644850
Edwards APeruffo AAbate A(2024)Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical ModelsProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3651398(1-10)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3651398
Jin CMa XRen TLin WDing Z(2024)Safe Controller Synthesis for Nonlinear Systems Using Bayesian Optimization Enhanced Reinforcement LearningProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3650137(1-10)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3650137
Anand MMurali VTrivedi AZamani M(2024)Verification of Hyperproperties for Dynamical Systems via Barrier CertificatesIEEE Transactions on Automatic Control10.1109/TAC.2024.338444869:10(6920-6934)Online publication date: Oct-2024
https://doi.org/10.1109/TAC.2024.3384448
Zhang HNiu LClark APoovendran R(2024)Fault Tolerant Neural Control Barrier Functions for Robotic Systems under Sensor Faults and Attacks2024 IEEE International Conference on Robotics and Automation (ICRA)10.1109/ICRA57147.2024.10610491(9901-9907)Online publication date: 13-May-2024
https://doi.org/10.1109/ICRA57147.2024.10610491
Samanipour PPoonawala H(2024)Invariant set estimation for piecewise affine dynamical systems using piecewise affine barrier functionEuropean Journal of Control10.1016/j.ejcon.2024.10111580(101115)Online publication date: Nov-2024
https://doi.org/10.1016/j.ejcon.2024.101115
Sheikhi SMehmood UBak SSmolka SStoller S(2024)The black-box simplex architecture for runtime assurance of multi-agent CPSInnovations in Systems and Software Engineering10.1007/s11334-024-00553-6Online publication date: 21-Mar-2024
https://doi.org/10.1007/s11334-024-00553-6
Li XLiu JLuo S(2024)Transient Safety Control for Inverter-Based Microgrids with Stochastic UncertaintiesProceedings of 2024 Chinese Intelligent Systems Conference10.1007/978-981-97-8654-1_47(479-487)Online publication date: 27-Oct-2024
https://doi.org/10.1007/978-981-97-8654-1_47
Wu HFeng SGan TWang JXia BZhan N(2024)On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded DomainsFormal Methods10.1007/978-3-031-71177-0_16(248-266)Online publication date: 13-Sep-2024
https://doi.org/10.1007/978-3-031-71177-0_16
Zhi DWang PLiu SOng CZhang M(2024)Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled SystemsComputer Aided Verification10.1007/978-3-031-65630-9_20(401-426)Online publication date: 25-Jul-2024
https://doi.org/10.1007/978-3-031-65630-9_20
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents