Chuanrui Jiang | Searcharxiv

arXiv2026

Verification Framework for the Union of Control Barrier Functions

Control Barrier Functions (CBFs) have been proposed to ensure safety of autonomous systems. This paper considers control policies that switch between CBF constraints. Under this approach, we represent a complex non-convex safe region as a union of sets that are computationally tractable to verify. We denote this framework as union-CBFs and make the following contributions. First, considering switching CBF-QP controllers, we propose a sufficient condition that ensures (i) the system undergoes a finite number of switches in any finite time interval and ensures (ii) the forward invariance of the closed-loop system in between switches. Second, we consider two types of switching strategies and propose union-CBFs conditions for each strategy to satisfy (i) and (ii). Third, we formulate Sum-of-Squares (SOS) algorithms to verify the conditions. The experiments show that our union-CBFs framework results in a larger safe region compared to high-degree polynomial CBFs. We also show the efficiency of the verification algorithms using a polynomial system model.

math.OC↗

arXiv2024

Verification and Synthesis of Compatible Control Lyapunov and Control Barrier Functions

Safety and stability are essential properties of control systems. Control Barrier Functions (CBFs) and Control Lyapunov Functions (CLFs) are powerful tools to ensure safety and stability respectively. However, previous approaches typically verify and synthesize the CBFs and CLFs separately, satisfying their respective constraints, without proving that the CBFs and CLFs are compatible with each other, namely at every state, there exists control actions within the input limits that satisfy both the CBF and CLF constraints simultaneously. Ignoring the compatibility criteria might cause the CLF-CBF-QP controller to fail at runtime. There exists some recent works that synthesized compatible CLF and CBF, but relying on nominal polynomial or rational controllers, which is just a sufficient but not necessary condition for compatibility. In this work, we investigate verification and synthesis of compatible CBF and CLF independent from any nominal controllers. We derive exact necessary and sufficient conditions for compatibility, and further formulate Sum-Of-Squares programs for the compatibility verification. Based on our verification framework, we also design a nominal-controller-free synthesis method, which can effectively expands the compatible region, in which the system is guaranteed to be both safe and stable. We evaluate our method on a non-linear toy problem, and also a 3D quadrotor to demonstrate its scalability. The code is open-sourced at \url{https://github.com/hongkai-dai/compatible_clf_cbf}.

eess.SY↗