Verification and Synthesis Methods for High-Order Control Barrier Functions

TL;DR

This paper develops SOS-based methods for verifying and synthesizing high-order control barrier functions, ensuring real-time safety in autonomous systems with multiple constraints and control Lyapunov functions.

Contribution

It introduces SOS programs for verification and synthesis of HOCBFs, enabling guaranteed safety in complex autonomous systems with input constraints.

Findings

Successfully synthesized 14 class K functions for a system with seven HOCBFs.

Verified safety guarantees for systems with multiple HOCBFs and input constraints.

Demonstrated real-time safety assurance in numerical simulations.

Abstract

High-order control barrier functions (HOCBFs) can be used to provide autonomous systems with safety, though computational methods to verify and synthesize these functions remain lacking. In this work, we address this need by formulating SOS programs that verify and synthesize HOCBFs, such that continued safety is always guaranteed forward in time. We first propose a verification SOS program for systems with (i) one or multiple HOCBFs, (ii) a control Lyapunov function (CLF), and (iii) input constraints, and we show that a solution to this problem guarantees that the online implementation of the system is always safe. Next, we propose a sequence of SOS programs that synthesize the class K functions used in an HOCBF, and we show that this sequence of problems ensures that a system is guaranteed to remain safe while running. After that, a synthesis framework is given that ensures real-time safety for systems with (i) multiple HOCBFs, (ii) a CLF, and (iii) input constraints. Our developments are illustrated in numerical simulations for a system with seven HOCBFs of maximum relative degree two, with 14 total unknown class K functions, all of which are successfully synthesized in a way that produces safe autonomy.