A Semi-Algebraic Framework for Verification and Synthesis of Control Barrier Functions

Abstract

Safety is a critical property for control systems in medicine, transportation, manufacturing, and other applications, and can be defined as ensuring positive invariance of a predefined safe set. This paper investigates the problems of verifying positive invariance of a semi-algebraic set as well as synthesizing sets that can be made positive invariant through Control Barrier Function (CBF)-based control. The key to our approach consists of mapping conditions for positive invariance to sum-of-squares constraints via the Positivstellensatz from real algebraic geometry. Based on these conditions, we propose a framework for verifying safety of CBF-based control including single CBFs, high-order CBFs, multi-CBFs, and systems with trigonometric dynamics and actuation constraints. In the area of synthesis, we propose algorithms for constructing CBFs, namely, an alternating-descent approach and a local CBF approach. We evaluate our approach through case studies on quadrotor UAV and power converter test systems.

arXiv commentAccepted to IEEE Transactions on Automatic Control. To appear May 2025

Cited by in corpus (3)

• Safety-Critical Control for Autonomous Systems: Control Barrier Functions via Reduced-Order Models
• Synthesis and verification of robust-adaptive safe controllers
• Optimization-based Verification of Discrete-time Control Barrier Functions: A Branch-and-Bound Approach