A Semi-Algebraic Framework for Verification and Synthesis of Control Barrier Functions
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Verification and Synthesis of Control Barrier Functions
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 p…
Verification and Forward Invariance of Control Barrier Functions for Differential-Algebraic Systems
Differential-algebraic equations (DAEs) arise in power networks, chemical processes, and multibody systems, where algebraic constraints encode physical conservation laws. The safety of such systems is critical, yet safe …
Fast Verification of Control Barrier Functions via Linear Programming
Control barrier functions are a popular method of ensuring system safety, and these functions can be used to enforce invariance of a set under the dynamics of a system. A control barrier function must have certain proper…
Beyond Accuracy: Diagnosing Algebraic Reasoning Failures in LLMs Across Nine Complexity Dimensions
Algebraic reasoning remains one of the most informative stress tests for large language models, yet current benchmarks provide no mechanism for attributing failure to a specific cause. When a model fails an algebraic pro…
A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis
An emerging branch of control theory specialises in certificate learning, concerning the specification of a desired (possibly complex) system behaviour for an autonomous or control model, which is then analytically verif…