On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains
Hao Wu, Shenghua Feng, Ting Gan, Jie Wang, Bican Xia, Naijun Zhan
TL;DR
This work tackles the incomplete landscape of SDP-based barrier certificate synthesis for systems on unbounded domains by introducing two complete SOS-based approaches. First, a homogenization-driven complete characterization for polynomial barrier certificates on unbounded domains is developed, enabling a finite SOS formulation despite unbounded state spaces. Second, the authors define homogenized systems and extend the framework to a class of semialgebraic/non-polynomial barrier certificates, providing a complete SOS encoding for these as well. They implement the methods and demonstrate through experiments that the complete approaches achieve greater expressiveness while maintaining practical efficiency compared to the traditional bounded-domain, incomplete formulations. The results advance reliable safety verification for CPS in unbounded settings and offer practical tools for broader barrier certificate synthesis tasks, including potential extensions to Lyapunov and invariant synthesis.
Abstract
Barrier certificates, serving as differential invariants that witness system safety, play a crucial role in the verification of cyber-physical systems (CPS). Prevailing computational methods for synthesizing barrier certificates are based on semidefinite programming (SDP) by exploiting Putinar Positivstellensatz. Consequently, these approaches are limited by the Archimedean condition, which requires all variables to be bounded, i.e., systems are defined over bounded domains. For systems over unbounded domains, unfortunately, existing methods become incomplete and may fail to identify potential barrier certificates. In this paper, we address this limitation for the unbounded cases. We first give a complete characterization of polynomial barrier certificates by using homogenization, a recent technique in the optimization community to reduce an unbounded optimization problem to a bounded one. Furthermore, motivated by this formulation, we introduce the definition of homogenized systems and propose a complete characterization of a family of non-polynomial barrier certificates with more expressive power. Experimental results demonstrate that our two approaches are more effective while maintaining a comparable level of efficiency.