Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Andrew Clark

TL;DR

This paper uses the algebraic-geometric Positivstellensatz to construct convex equivalent conditions for a CBF to ensure safety, and proposes algorithms for constructing CBFs, namely, an alternating-descent approach, a local CBF approach, and a Newton's method approach.

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.

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

TL;DR

This paper uses the algebraic-geometric Positivstellensatz to construct convex equivalent conditions for a CBF to ensure safety, and proposes algorithms for constructing CBFs, namely, an alternating-descent approach, a local CBF approach, and a Newton's method approach.

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.
Paper Structure (33 sections, 27 theorems, 76 equations, 1 figure, 1 table, 1 algorithm)

This paper contains 33 sections, 27 theorems, 76 equations, 1 figure, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Model and Preliminaries
  4. System Model and Safety Definitions
  5. Preliminary Results
  6. Problem Formulation: Safety Verification
  7. Viability Verification
  8. Special Cases of the Semi-Algebraic Framework
  9. Super-Level Set of Single Polynomial
  10. Simple Semi-Algebraic Sets
  11. Union of Polynomial Super-Level Sets
  12. Verifying Inclusion in a Given Safe Region
  13. Computational Complexity of Problem \ref{['problem:viability-verification']}
  14. Verifying Feedback Controlled Positive Invariance
  15. Generalization to Trigonometric Dynamics
  16. ...and 18 more sections

Key Result

Lemma 1

Suppose that the set $\mathcal{D} = \{x : b_{i}(x) \geq 0, i=1,\ldots,M\}$ for some functions $b_{1},\ldots,b_{M}: \mathbb{R}^{n} \rightarrow \mathbb{R}$. Furthermore, suppose that, for all $x \in \mathcal{D}$, there exists $z$ such that $b_{i}(x) + \nabla b_{i}(x)z > 0$ for all $i=1,\ldots,M$. Then

Figures (1)

  • Figure 1: Numerical evaluation of our approach on a linearized quadrotor model. (a) Geometry of the safe region for different values of the input constraint. As the input constraint becomes more restrictive, the size of the feasible safe region is reduced. (b) Comparison of trajectories from CBF-based control policies. In both cases, the control policy is given by (\ref{['eq:quadrotor-control-law']}) with $k=10$. Initializing the state within $\{x: b(x) \geq 0\}$ maintains the state within the safe region $\{x: ||x||_{2}^{2} \leq 1\}$, while initializing outside $\mathcal{C}$ results in a safety violation.

Theorems & Definitions (54)

  • Definition 1
  • Definition 2: blanchini2008set, Def. 4.6
  • Lemma 1: blanchini2008set, Eq. (4.6)
  • Theorem 1: Nagumo's Thoerem aubin2011viability, Theorem 11.2.3
  • Definition 3: aubin2011viability, Ch. 11.1
  • Definition 4
  • Definition 5
  • Theorem 2: ames2019control, Theorem 2
  • Definition 6: bochnak2013real, Def. 2.1.4
  • Lemma 2
  • ...and 44 more