Verification and Synthesis of Control Barrier Functions

TL;DR

This paper introduces a polynomial-based framework for verifying and synthesizing Control Barrier Functions (CBFs) to ensure safety in control systems, leveraging algebraic geometry and sum-of-squares techniques.

Contribution

It develops a novel algebraic approach using Positivstellensatz for CBF verification and proposes heuristics for CBF synthesis in polynomial control systems.

Findings

Verification of CBFs reduces to solving polynomial equations.

Sum-of-squares constraints can certify the nonexistence of unsafe solutions.

Heuristics effectively synthesize CBFs for various safe regions.

Abstract

Control systems often must satisfy strict safety requirements over an extended operating lifetime. Control Barrier Functions (CBFs) are a promising recent approach to constructing simple and safe control policies. This paper proposes a framework for verifying that a CBF guarantees safety for all time and synthesizing CBFs with verifiable safety in polynomial control systems. Our approach is to show that safety of CBFs is equivalent to the non-existence of solutions to a family of polynomial equations, and then prove that this nonexistence is equivalent to a pair of sum-of-squares constraints via the Positivstellensatz of algebraic geometry. We develop this Positivstellensatz to verify CBFs, as well as generalization to high-degree systems and multiple CBF constraints. We then propose a set of heuristics for CBF synthesis, including a general alternating-descent heuristic, a specialized approach for compact safe regions, and an approach for convex unsafe regions. Our approach is illustrated on two numerical examples.