Research On Barrier Certificates Generation Method Based On Iterative Learning

Hybrid system is a kind of complex dynamical system,which includes both continuous dynamic system and discrete event system,and the interaction between them.The interaction between continuous variables and discrete events in hybrid systems makes the analysis and verification of hybrid systems very difficult.Therefore,the safety verification of hybrid systems is extremely challenging.Because the barrier function generation method avoids the complex reachable set calculation,it has been widely used in the analysis and verification of hybrid systems.This paper aims to study the generation method of the barrier function based on iterative learning to verify the safety of hybrid systems.The main research work is as follows.We consider the problem of barrier function generation based on counterexample guidance.In this paper,with the idea of counterexample guided inductive synthesis(CEGIS),the barrier function is synthesized interactively with the Learner component and the Verifier component.The Learner component uses the deep neural network as the template of the barrier function,and uses the fitting polynomial of the classic activation function such as Re LU function,as the legal activation function of the hidden layer of the neural network to construct a neural candidate barrier function.The Verifier component generates the worst counterexample via the sum of squares(SOS)optimization method and cylinder algebraic decomposition(CAD)technique,and adds the worst counterexample to the training set of the Neural Network in the Learner component to guide the next training,which can effectively reduce the CEGIS iteration number.And finally the correctness of the barrier function is strictly guaranteed by CAD.The experimental results show that this method has better effect and efficiency than the current mainstream barrier function generation method.We address the problem of barrier function generation based on iterative SOS programming.In this paper,we combine the deep learning and SOS programming.With the SOS relaxation to barrier conditions,the generation problem of the barrier function is transformed into a SOS optimization problem.Given the neural candidate barrier function obtained by supervised learning as the initial value of the barrier function,the bilinear constraint problem caused by SOS relaxation is further transformed into an iterative solution of a set of linear constraints,thus providing a formal guarantee for the safety of the hybrid systems.We developed a CEGIS based barrier function generation tool as well as the SOS programming based barrier function generation tool,both of which can be used to verify the safety of hybrid systems.