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.
|Number of pages||18|
|Journal||Formal Aspects of Computing|
|Publication status||Published - 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.
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