Barrier Certificate Synthesis via Interpolation and Difference-of-Convex Programming
摘要
Barrier certificates play a crucial role in the verification of cyber-physical systems (CPS), particularly in safety-critical scenarios. The underlying principle involves encoding the conditions for a polynomial’s zero sub-level set to be a differential invariant, enabling the application of powerful mathematical optimization techniques. A primary challenge in this approach is that, in general settings, the resulting constraints are non-convex and lack efficient solvers. To address this issue, Wang et al. [48, 49] proposed a difference-of-convex (DC) algorithm to approximate a non-convex program by solving a series of convex programs using semidefinite programming (SDP). While this approach offers a guarantee on convergence to local optimums, it suffers from the initial value problem. In this paper, we try to solve this problem based on the key insight that a user-defined polynomial in barrier certificate conditions should be selected to be an interpolant separating the initial region and the unsafe region. A novel approach is proposed to adjust the position of the interpolant via SDP, and the obtained interpolant is fed into the DC algorithm as the initial value. Experiments show that our strategy can significantly improve the performance of the DC algorithm.