Synthesizing Barrier Certificates of Neural Network Controlled Continuous Systems via Approximations

The paper presents a barrier certificate based approach to verifying safety properties of closed-loop systems using neural networks as controllers. It deals with the verification problem in the infinite time horizon and exploits the approximated system of the original one to synthesize the candidate barrier certificates, where the behavior of a neural network controller is approximated by a polynomial with a bounded error. Satisfiability Modulo Theories solvers are then utilized to identify real barrier certificates from those candidates. As a barrier certificate can separate the over-approximation of the reachable set from the unsafe region, once it is constructed, the safety property gets proved. We show the advantage of our approach in barrier certificates synthesis by comparing it with the state-of-the-art work on a set of benchmarks.