Learning safe neural network controllers with barrier certificates

Hengjun Zhao, Xia Zeng*, Taolue Chen, Zhiming Liu, Jim Woodcock

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review


We provide a new approach to synthesize controllers for nonlinear continuous dynamical systems withcontrol against safety properties. The controllers are based on neural networks (NNs).To certify the safety property we utilize barrier functions, which are represented by NNs as well.We train the controller-NN and barrier-NN simultaneously, achieving a verification-in-the-loop synthesis.We provide a prototype tool nncontroller with a number of case studies.The experiment results confirm the feasibility and efficacy of our approach.

Original languageEnglish
Pages (from-to)437-455
Number of pages18
JournalFormal Aspects of Computing
Publication statusPublished - 2 Apr 2021

Bibliographical note

© 2021, British Computer Society. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details.

Funding Information:
We thank the anonymous reviewers for their valuable comments on the earlier versions of this paper, and thank Prof. Jyotirmoy V. Deshmukh for the explanation on the bicycle model of Example 5.3. H. Zhao was supported partially by the National Natural Science Foundation of China (No. 61702425, 61972385); X. Zeng was supported partially by the National Natural Science Foundation of China (No. 61902325), and ?Fundamental Research Funds for the Central Universities" (SWU117058); T. Chen is partially supported by NSF Cgrant (No. 61872340), and Guangdong Science and Technology Department grant (No. 2018B010107004), the Overseas Grant of the State Key Laboratory of Novel Software Technology (No. KFKT2018A16), the Natural Science Foundation of Guangdong Province of China (No. 2019A1515011689); Z. Liu was supported partially by the National Natural Science Foundation of China (No. 62032019, 61672435, 61732019, 61811530327), and Capacity Development Grant of Southwest University (SWU116007); J. Woodcock was partially supported by the research grant from Southwest University.


  • Barrier certificates
  • Continuous dynamical systems
  • Controller synthesis
  • Neural networks
  • Safety verification

Cite this