Efficient Sum of Squares-Based Verification and Construction of Control Barrier Functions by Sampling on Algebraic Varieties

Safety is a critical property of control systems in vital applications such as manufacturing, energy, and autonomous vehicles. Control barrier functions have been proposed for safe control, however, verifying the safety guarantees of a given CBF and constructing CBFs to satisfy safety constraints are computationally challenging. In this paper, we propose a new approach to addressing these challenges, in which the global safety properties of CBFs are characterized based on a finite set of sample points. Specifically, we propose new algorithms for verifying CBFs for polynomial systems by solving a system of linear equalities and sum-of-squares constraints at a set of points sampled on an algebraic variety induced by the CBF. We extend this approach to high-order CBFs as well as systems with actuation constraints. Turning to the problem of constructing CBFs, we propose an algorithm that first selects a finite set of samples, and then computes a CBF such that the samples lie on the boundary of the safe region by solving a mixed-integer convex program. We prove that, if the number of samples is sufficiently large and a CBF exists, then our approach returns a function that satisfies necessary conditions of a CBF. We evaluate our approach on a linear cruise control scenario and a nonlinear quadrotor UAV, and find that both the verification and synthesis algorithms significantly outperform another state-of-the-art SOS-based algorithm.