Synthesizing Barrier Certificates of Neural Network Controlled Continuous Systems via approximations
Hosted in Virtual Platform
Design Verification and Validation
DescriptionBarrier certificates can separate the over-approximation of the reachable set from the unsafe region, thus are widely used in proving safety properties in the infinite time horizon. The paper focuses on synthesizing barrier certificates of closed-loop systems controlled by neural networks. It constructs the approximated system of the original one by approximating the network controller with a polynomial with a bounded error and exploits it to synthesize the candidate barrier certificates. Satisfiability Modulo Theories solvers are then utilized to identify real barrier certificates from those candidates. We evaluate the efficacy of the approach by a set of benchmarks.