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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Barrier Certificate Synthesis via Interpolation and Difference-of-Convex Programming

  • Guanhua Lin,
  • Hao Wu,
  • Naijun Zhan

摘要

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.