Synthesizing barrier certificates using neural networks
HSCC '20: 23rd ACM International Conference on Hybrid Systems: Computation and Control Sydney New South Wales Australia April, 2020(2020)
摘要
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.
更多查看译文
关键词
Barrier certificates, Neural networks, Continuous dynamical systems, Verification
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络