# Fast Verification of Control Barrier Functions via Linear Programming

Ellie Pond  Matthew Hale  University of Florida, Gainesville, FL 32611 USA
(email: elliempond@ufl.edu).  University of Florida, Gainesville, FL 32611 USA
(email: matthewhale@ufl.edu).

###### Abstract

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 properties, and one
must both formulate a candidate control barrier function and verify that it
does indeed satisfy the required properties. Targeting the latter problem,
this paper presents a method of verifying any finite number of candidate
control barrier functions with linear programming. We first apply techniques
from real algebraic geometry to formulate verification problem statements that
are solvable numerically. Typically, semidefinite programming is used to
verify candidate control barrier functions, but this does not always scale
well. Therefore, we next apply a method of inner-approximating the set of sums
of squares polynomials that significantly reduces the computational complexity
of these verification problems by transcribing them to linear programs. We
give explicit forms for the resulting linear programs, and simulation results
for a satellite inspection problem show that the computation time needed for
verification can be reduced by more than $95$%.

###### keywords:

Nonlinear control, Control of constrained systems, Autonomous robotic systems

††thanks:  This work was supported by AFOSR under grant FA9550-19-1-0169, ONR
under grants N00014-19-1-2543, N00014-21-2-2502, and N00014-22-1-2435, and
AFRL under grants FA8651-22-F-1052 and FA8651-23-FA-006.

##  1 Introduction

Interest in safety-critical autonomous systems has grown in recent years. For
example, mobile autonomous robots must avoid collisions with each other Zohaib
et al. (2013); Kunchev et al. (2006) and co-robots working alongside humans
must not collide with them Zacharaki et al. (2020); Vasic and Billard (2013).
Model predictive control Gao (2010), reachability analysis Althoff and Dolan
(2014), and “back-up" control strategies Roumeliotis and Mataric (2000) are
among the methods that address safety. However, these approaches may suffer
from poor performance or from being overly conservative. One alternative way
to formalize system safety is by defining a safe region of a system’s state
space and ensuring that the system’s dynamics render that set forward-
invariant in time.

A common method of ensuring this type of safety through invariance is with
control barrier functions (CBFs). A representative sample of works using CBFs
for safety is Xiao and Belta (2019); Jankovic and Santillo (2021); Landi et
al. (2019); Xu et al. (2015); Cortez et al. (2022). A CBF is a function that
is positive on the safe set and whose derivative satisfies a certain bound on
the safe set. A CBF is then used in controller design to impose inequality
constraints on the system input that ensure invariance of the safe set. These
inequality constraints are in terms of the control barrier function itself,
which must be found and verified to satisfy the conditions that make it a
valid CBF before it can be used in the control design process.

The need for verification has led to the development of several computational
approaches that are analogous to the verification of Lyapunov functions.
Recent work in this vein has used semidefinite programming and sums of squares
(SOS) optimization to validate that a candidate CBF is indeed a valid CBF Wang
et al. (2018); Isaly et al. (2022); Clark (2021). However, these verification
approaches may not scale well to systems with large state spaces, e.g.,
bipedal robot control Feng et al. (2015), or systems with many constraints
CBFs Wang et al. (2017).

To address this need, in this paper we develop scalable verification
techniques for systems with single and multiple CBFs. Our approach leverages
tools from real algebraic geometry to formulate computational problems to
assess the nonnegativity properties of a candidate CBF. We then apply the
method introduced in Ahmadi and Majumdar (2017) to translate these
verification statements to linear programs (LPs).

To summarize, our contributions are:

  * •

Derivation of CBF verification statements for dynamical systems with any
finite number of candidate CBFs

  * •

Explicit mapping of the verification statements to linear programs

  * •

Simulations that demonstrate the substantial improvement in scalability and
reduction of computation time in practice.

There are several works that propose verification methods for systems with
multiple candidate CBFs. In Cortez et al. (2022), a neighborhood notion is
employed to switch priority of CBFs to circumvent possible conflicts. In Black
and Panagou (2022), a method of consolidating multiple CBFs to one candidate
CBF through under-approximating the intersection of safe sets is proposed. The
most relevant work can be found in Wang et al. (2018); Isaly et al. (2022);
Clark (2021), where algebraic geometry tools are applied to create SOS
validation programs. However, we apply different results from algebraic
geometry and develop linear program translations that allow for improved
scaling and decreased computation times relative to SOS-based works. To the
best of our knowledge, CBF verification has not been addressed through linear
programming before.

The rest of this paper is organized as follows. In Section 2, we provide
necessary background on CBFs, Positivstellensätze from algebraic geometry, and
DSOS programs, as well as the problem statements solved in this work. In
Section 3, we develop verification statements for single and multiple
candidate CBFs through application of algebraic geometry. In Sections 4 and 5,
we explicitly state the translation from verification statement to linear
programs for single and multiple CBF problems, respectively. In Section 6, we
present simulation results that demonstrate the benefit of linear programming
over semidefinite programming for verification. In Section 7, we conclude.

##  2 Background and Problem Formulation

In this section, we introduce background on CBFs, Positivstellensätze, and
DSOS programs. We then provide three formal problem statements that will be
the focus of the remaining sections.

Throughout, for indexing up to an integer $N$ we use
$i\in[N]=\\{1,\dots,N\\}$. For functions $f$ and $g$, we define the Lie
derivative of $f$ with respect to $g$ as $L_{g}f(x)=\frac{\partial
f(x)}{\partial x}g(x)$. We use $\mathbb{R}[x]$ to denote the set of scalar-
valued polynomials with real coefficients. Here, $x=(x_{1},\dots,x_{n})^{T}$
is a vector of indeterminates whose dimension will be clear from context. We
define a polynomial matrix $p\in\mathbb{R}^{m\times n}[x]$ as an $m\times n$
matrix with polynomial entries $p_{ij}\in\mathbb{R}[x]$ for all $i\in[m]$,
$j\in[n]$. We write $\mathbb{R}^{m}[x]$ for $\mathbb{R}^{m\times 1}[x]$. We
define an operation $\text{col}:\mathbb{R}^{m\times
n}\rightarrow\mathbb{R}^{mn}$ as the mapping from a matrix to a column vector
containing the transposed rows of the matrix. For example, for a matrix

$p=\begin{bmatrix}p_{11}&p_{12}&\ldots&p_{1n}\\\
p_{21}&p_{22}&\ldots&p_{2n}\\\ \vdots&&\ddots&\vdots\\\
p_{m1}&p_{m2}&\ldots&p_{mn}\end{bmatrix}$ (1)

with $p_{ij}\in\mathbb{R}[x]$ for all $i\in[m]$, $j\in[n]$, we have

$\text{col}(p)=\begin{bmatrix}p_{11}&p_{12}&\dots&p_{1n}&\dots&p_{m1}&p_{m2}&\dots&p_{mn}\end{bmatrix}^{T}.\\\
$ (2)

###  2.1 Control Barrier Functions

We will consider dynamical systems that are affine in the control and take the
form

$\dot{x}=f(x)+g(x)u,$ (3)

where $x\in\mathbb{R}^{n}$ is the state of the system, $u\in\mathbb{R}^{m}$ is
the input, and $f\in\mathbb{R}^{n}[x]$, $g\in\mathbb{R}^{n\times m}[x]$ define
the system dynamics.

The polynomial $b\in\mathbb{R}[x]$ defines a safe set
$\mathcal{B}=\\{x\in\mathbb{R}^{n}\mid b(x)\geq 0\\}$. The function $b$ is a
CBF if there exists an extended class-$\mathcal{K}$ function, $\kappa$, such
that Ames et al. (2019)

$\displaystyle\sup_{u}\Big{\\{}L_{f}b(x)+L_{g}b(x)u+\kappa(b(x))\Big{\\}}$
$\displaystyle\geq 0,$ (4) $\displaystyle\text{for all }x\in\mathbb{R}^{n}.$

The Lie derivatives of $b$ are $L_{f}b\in\mathbb{R}[x]$ and
$L_{g}b\in\mathbb{R}^{m}[x]$. CBFs can be used to impose an inequality
constraint on the input that takes the form

$L_{g}b(x)u\geq\kappa(b(x))-L_{f}b(x).$ (5)

Control barrier functions are used to ensure safety for a system. In this
capacity, safety is equivalent to forward invariance of the system’s safe set
$\mathcal{B}$. The set $\mathcal{B}$ is forward invariant if for every
$x_{0}\in\mathcal{B}$, we have $x(t)\in\mathcal{B}$ for all $t\geq 0$. If a
control input exists that satisfies (5), then the safe set $\mathcal{B}$ can
be rendered forward invariant and the system is rendered safe Ames et al.
(2019).

In this work we focus on systems with unbounded control inputs. A candidate
CBF $b$ satisfies (5) if and only if there are no points $x\in\mathbb{R}^{n}$
such that $L_{f}b(x)<0$ while $b(x)=0$ and $L_{g}b(x)=0$ Clark (2021). When
$b(x)=0$, a control input can be chosen so that (5) is satisfied. However, if
both $b(x)=0$ and $L_{g}b(x)=0$, then the dynamics and candidate CBF must have
$L_{f}b(x)\geq 0$.

###  2.2 Positivstellensätze

We consider a finite set of polynomials

$S=\\{f_{1},\dots,f_{r};g_{1},\dots,g_{s}\\},$ (6)

where $f_{i},g_{j}\in\mathbb{R}[x]$ for all $i\in[r]$ and $j\in[s]$. The basic
semialgebraic set $K$ associated to $S$ is

$\displaystyle K=\\{x\in\mathbb{R}^{n}\;|\;f_{i}(x)$ $\displaystyle\geq
0,\;i=1,\dots,r;\;\;$ (7) $\displaystyle g_{j}(x)=0,\;j=1,\dots,s\\}.$

We denote by $\Sigma[x]$ the set of all sums of squares (SOS) polynomials in
$\mathbb{R}[x]$. All $s\in\Sigma[x]$ take the form $s(x)=\sum_{i}p_{i}^{2}(x)$
for some $p_{i}\in\mathbb{R}[x]$.

Preorders and quadratic modules are algebraic objects associated to the set of
polynomials $S$. Let the subset $P_{S}\subseteq\mathbb{R}[x]$ be the smallest
preorder containing the set $S$. Then a polynomial $q\in P_{S}$ if and only if
$q$ is of the form

$q=\sum_{\epsilon\subseteq\\{0,1\\}^{r}}s_{\epsilon}(x)f_{\epsilon}(x)+\sum_{j=1}^{s}p_{j}(x)g_{j}(x),$
(8)

where $p_{j}\in\mathbb{R}[x]$ for $j\in[s]$ and each
$s_{\epsilon}\in\Sigma[x]$, with
$f_{\epsilon}=f_{1}^{\epsilon_{1}}\cdot\dots\cdot f_{r}^{\epsilon_{r}}$ and
$f_{\emptyset}=1$ Powers (2021).

Let the subset $M_{S}\subseteq\mathbb{R}[x]$ be the smallest quadratic module
containing the set $S$. Then a polynomial $q\in M_{S}$ if and only if $q$ is
of the form

$q=s_{0}(x)+\sum_{i=1}^{r}s_{i}(x)f_{i}(x)+\sum_{j=1}^{s}p_{j}(x)g_{j}(x),$
(9)

where $p_{j}\in\mathbb{R}[x]$ for $j\in[s]$ and $s_{i}\in\Sigma[x]$ for
$i\in[r]\cup\\{0\\}$ Powers (2021).

Remark 1 (Powers and Wörmann (1998)). The quadratic module of $S$ is always
contained in the preorder, i.e., $M_{S}\subseteq P_{S}$. When $r\leq 1$ in
$K$, we have $M_{S}=P_{S}$.

Proposition 1 (Archimedean Property Powers (2021)). Fix a polynomial ring
$\mathbb{R}[x]$ over the indeterminates $x=(x_{1},\dots,x_{n})^{T}$, and fix a
set of polynomials $S=\\{f_{1},\dots,f_{r};g_{1},\dots,g_{s}\\}$. Then, for a
quadratic module $M_{S}$, the following conditions are equivalent:

  1. 1.

$M_{S}$ is Archimedean.

  2. 2.

There exists $C\in\mathbb{N}\backslash\\{0\\}$ such that
$C-\sum_{i=1}^{n}x_{i}^{2}\in M_{S}$.

  3. 3.

There exists $C\in\mathbb{N}\backslash\\{0\\}$ such that both $C\pm x_{i}\in
M_{S}$ for $i=1,\dots,n$.

The Archimedean property is slightly stronger than $K$ being compact Ahmadi
and Majumdar (2017).

The Positivstellensätze are a class of theorems in real algebraic geometry
that characterize positivity properties of polynomials over semialgebraic
sets. The broadest variation is credited to Krivine and Stengle.

Proposition 2 (KS Positivstellensatz Bochnak et al. (2013)). Fix a set
$S=\\{f_{1},\dots,f_{r};g_{1},\dots,g_{s}\\}$. Let $K$ and $P_{S}$ be as
defined in (7) and (8), and let $q\in\mathbb{R}[x]$. Then

  1. 1.

$q>0$ on $K$ if and only if there exist $h_{1},h_{2}\in P_{S}$ such that
$h_{1}q=1+h_{2}$.

  2. 2.

$q\geq 0$ on $K$ if and only if there exist an integer $m\geq 0$ and
$h_{1},h_{2}\in P_{S}$ such that $h_{1}q=q^{2m}+h_{2}$.

  3. 3.

$q=0$ on $K$ if and only if there exists an integer $m\geq 0$ such that
$-q^{2m}\in P_{S}$.

  4. 4.

$K=\emptyset$ if and only if $-1\in P_{S}$.

These four statements are equivalent.

Another variation of the Positivstellensatz is credited to Putinar. This
version makes use of the quadratic module through introducing an assumption.
Using the quadratic module in computations is advantageous to using the
preorder, due to the linear growth rate of the number of SOS terms in
expressions in the quadratic module compared to the exponential growth rate of
the number of SOS terms when using expressions in the preorder.

Proposition 3 (Putinar’s Positivstellensatz Powers (2021)). Fix a set
$S=\\{f_{1},\dots,f_{r};g_{1},\dots,g_{s}\\}$. Let $K$ and $P_{S}$ be as
defined in (7) and (8), and let $q\in\mathbb{R}[x]$. Assume that $M_{S}$ is
Archimedean, satisfying Proposition 1. Then $q>0$ on $K$ implies that $q\in
M_{S}$.

Lastly, a corollary credited to Jacobi is introduced. We note that a quadratic
module in $\mathbb{R}[x]$ can alternatively be defined as a
$\Sigma[x]$-module, where $\Sigma[x]$ is a generating preprime in
$\mathbb{R}[x]$, i.e., $\Sigma[x]-\Sigma[x]=\mathbb{R}[x]$. We present the
following proposition in terms of the polynomial ring $\mathbb{R}[x]$ because
that is what we will consider going forward, though it generally applies to
any commutative ring.

Proposition 4 (Jacobi’s Representation Corollary Jacobi (2001)). Suppose $T$
is a generating preprime in a commutative ring $\mathbb{R}[x]$, $M_{S}$ is an
Archimedean $T$-module, and $K$ is the nonnegativity set defined by (7). Then
$-1\in M_{S}$ if and only if $K=\emptyset$.

###  2.3 DSOS Programming

Traditionally, semidefinite programs (SDPs) have been used to solve problems
originating from Positivstellensätze or polynomial optimization problems with
nonnegativity constraints. Through this method, nonnegativity is approximated
by a more restrictive but computationally tractable SOS requirement.

We denote by $\mathcal{P}[x]$ the set of all nonnegative polynomials in
$\mathbb{R}[x]$. For indeterminates $x\in\mathbb{R}^{n}$, let
$m(x)\in\mathbb{R}^{k}$ be a monomial basis vector of degree $d$, where
$k=\binom{n+d}{n}$. Let $s\in\mathbb{R}[x]$ be of degree $2d$. Then $s$ is an
SOS polynomial if and only if there exists a symmetric Gram matrix, $Q$, such
that Powers and Wörmann (1998)

$s(x)=m^{T}(x)Qm(x)\quad\text{and}$ (10) $Q\succeq 0.$ (11)

Searching for a $Q$ that is positive semidefinite (PSD) is conventionally done
through semidefinite programming.

A matrix $Q\in\mathbb{R}^{k\times k}$ is diagonally dominant if

$Q_{ii}\geq\sum_{j\in[k]\backslash\\{i\\}}|Q_{ij}|\quad\quad\text{for all
}i\in[k].$ (12)

We define ‘$\succeq_{dd}$’ to indicate diagonal dominance of a matrix. That
is, $Q\succeq_{dd}0$ denotes that $Q$ satisfies (12) and thus is positive
semidefinite. A polynomial $s\in\mathbb{R}[x]$ is a diagonally dominant sums-
of-squares (DSOS) polynomial if it can be written as

$\displaystyle s(x)=\sum_{i}a_{i}m_{i}^{2}(x)+\sum_{i,j}$ $\displaystyle
b_{ij}(m_{i}(x)+m_{j}(x))^{2}$ (13) $\displaystyle+$
$\displaystyle\sum_{i,j}c_{ij}(m_{i}(x)-m_{j}(x))^{2}$

for some monomials $m_{i}(x),m_{j}(x)$ and some nonnegative scalars
$a_{i},b_{ij},c_{ij}$.

Proposition 5 (Ahmadi and Majumdar (2017)). Let $s\in\mathbb{R}[x]$ be of
degree $2d$. Then $s$ is a diagonally dominant sum of squares (DSOS)
polynomial if and only if there exists a symmetric Gram matrix, $Q$, such that

$s(x)=m^{T}(x)Qm(x)\quad\text{and}$ (14) $Q\succeq_{dd}0.$ (15)

Computationally, the condition $Q\succeq_{dd}0$ is enforced using the linear
constraints

$\displaystyle-Q_{ii}+\sum_{j\in[k]\backslash\\{i\\}}\tau_{ij}$
$\displaystyle\leq 0\quad\quad\text{for all }i\in[k]$ (16) $\displaystyle
Q_{ij}-\tau_{ij}$ $\displaystyle\leq 0\quad\quad\text{for all
}i,j\in[k],\;i\not=j$ $\displaystyle-Q_{ij}-\tau_{ij}$ $\displaystyle\leq
0\quad\quad\text{for all }i,j\in[k],\;i\not=j,$

where $\tau\in\mathbb{R}^{k\times k}$ is a symmetric bounding matrix that
enforces the absolute value constraints. We note that $\tau_{ij}\geq 0$ for
$i,j\in[k]$ is implicitly enforced by (16). We denote by $\mathcal{D}[x]$ the
set of all DSOS polynomials in $\mathbb{R}[x]$. The inclusion relationship
between the sets of polynomials is
$\mathcal{D}[x]\subseteq\Sigma[x]\subseteq\mathcal{P}[x]\subseteq\mathbb{R}[x]$.

Proposition 6 (Ahmadi and Majumdar (2017)). For a fixed degree $d$,
optimization over $\mathcal{D}[x]$ can be done through a linear program (LP).

In such an LP, the polynomial variables take the form $p(x)=c^{T}m(x)$. We
define the operation $\text{uTri}:\mathbb{R}^{k\times
k}\rightarrow\mathbb{R}^{\frac{1}{2}(k^{2}+k)}$ as the mapping from a
symmetric matrix to a vector of the upper trianglular elements of the matrix.
For example, for $k=3$ the matrix

$Q=\begin{bmatrix}q_{11}&q_{12}&q_{13}\\\ q_{12}&q_{22}&q_{23}\\\
q_{13}&q_{23}&q_{33}\end{bmatrix}$ (17)

gives

$\text{uTri}(Q)=\begin{bmatrix}q_{11}&q_{12}&q_{13}&q_{22}&q_{23}&q_{33}\end{bmatrix}^{T}.$
(18)

In DSOS programs with $I$ DSOS polynomial variables of the form
$m^{T}(x)Q_{i}m(x)$ for $i\in[I]$ and $J$ polynomial variables of the form
$c_{j}^{T}m(x)$ for $j\in[J]$, the decision vector is

$\displaystyle z=[c_{1}^{T}\;\;\ldots\;\;c_{J}^{T}\;\;\text{uTri}$
$\displaystyle(Q_{1})^{T}\;\;\text{uTri}(\tau_{1})^{T}\;\;\ldots\;\;$ (19)
$\displaystyle\text{uTri}(Q_{I})^{T}\;\;\text{uTri}(\tau_{I})^{T}]^{T}$

with size $z\in\mathbb{R}^{I(k^{2}+k)+Jk}$.

Lastly, we define the operation
$\text{G}_{k}:\mathbb{R}[x]\rightarrow\mathbb{R}^{k\times k}$ as the mapping
from a polynomial expression to the corresponding Gram matrix, where $k$ is
the degree of the monomial basis. For any polynomial $e(x)$, there exists a
Gram matrix representation of the form $e(x)=m^{T}(x)G_{k}(e)m(x)$, where
$G_{k}(e)$ is composed of the monomial coefficients of $e$. For example,
consider polynomials $p(x)=c_{1}+c_{2}x+c_{3}x^{2}$ and $b(x)=x^{2}-4$, with
indeterminate $x\in\mathbb{R}$ and monomial degree $k=4$. Then

$\text{G}_{4}(pb)=\begin{bmatrix}-4c_{1}&-4c_{2}&c_{1}-4c_{3}&c_{2}&c_{3}\\\
0&0&0&0&0\\\ 0&0&0&0&0\\\ 0&0&0&0&0\end{bmatrix}.$ (20)

The output of the Gram operation satisfies $p(x)b(x)=m^{T}(x)G_{4}(pb)m(x)$
with $m(x)=[1\;\;x\;\;x^{2}\;\;x^{3}\;\;x^{4}]^{T}$. This operation removes
dependence on the indeterminate $x\in\mathbb{R}$ and enables the development
of conditions that apply for all $x\in\mathbb{R}^{n}$, e.g., positive
definiteness. This property will be utilized in the linear programs we present
in Sections 4 and 5.

###  2.4 Problem Formulation

In this section, we state the problems we solve in the remainder of the paper.

####  2.4.1 Problem 1.

Given a collection of candidate CBFs, $S=\\{b_{1},\dots,b_{L}\\}$ with
$b_{i}\in\mathbb{R}[x]$ for $i\in[L]$, determine necessary and sufficient
conditions for safety using the Positivstellensätze.

For this problem, we will clearly establish the connection between real
algebraic geometry and candidate CBF verification. We will make explicit the
motivation behind the theorems we apply and the necessity of the assumptions
placed. In Section 3, we begin by considering the verification of a single
candidate CBF. This is then extended to the verification of multiple candidate
CBFs.

####  2.4.2 Problem 2.

Given a system (3) and a candidate CBF, $b\in\mathbb{R}[x]$, verify system
safety through forward invariance of the safe set
$\mathcal{B}=\\{x\in\mathbb{R}^{n}\mid b(x)\geq 0\\}$ with a linear program.

####  2.4.3 Problem 3.

Given a system (3) and a collection of candidate CBFs,
$S=\\{b_{1},\dots,b_{L}\\}$ with $b_{i}\in\mathbb{R}[x]$ for $i\in[L]$, verify
system safety through forward invariance to the system’s safe set
$\mathcal{B}=\\{x\in\mathbb{R}^{n}\mid b_{1}(x)\geq 0,\dots,b_{L}(x)\geq 0\\}$
with linear programming.

In Sections 4 and 5, we show the translation from the verification statements
derived in Section 3 to linear programs. While these verification statements
are nonlinear in the indeterminate variable $x\in\mathbb{R}^{n}$, they form
optimization programs that are linear over their decision variables.

##  3 Safety Verification with Positivstellensätze

In this section we solve Problem 1. We begin by considering systems with a
single candidate CBF. Several notions from algebraic geometry can be applied
to determine nonnegativity properties of a candidate CBF, and while these
variations can all theoretically verify candidate functions, their numerical
implementation can vary significantly in the size of the corresponding
problems and in the ease of computation of their solutions. In determining the
nonegativity theorems we apply to create verification statements, we keep in
mind the end goal of scaling to large numbers of CBFs and translating to
implementable optimization problems. This leads us to the following.

###### Theorem 1

Given a system in (3) and a single candidate CBF, $b\in\mathbb{R}[x]$, let
$S=\\{b,L_{g}b\\}$ and $K=\\{x\in\mathbb{R}^{n}\mid b(x)=0,L_{g}b(x)=0\\}$.
Then $b$ is a CBF and the system is verified forward invariant to
$\mathcal{B}$ if and only if there exists $a\in\mathbb{N}_{\geq 0}$, SOS
polynomials $s_{1},s_{2}\in\Sigma[x]$, and polynomials
$p_{10},p_{20}\in\mathbb{R}[x]$ and $p_{1},p_{2}\in\mathbb{R}^{m}[x]$ such
that

$h_{1}(x)L_{f}b(x)-h_{2}(x)-(L_{f}b(x))^{2a}=0$ (21)

and such that $h_{1},h_{2}\in M_{S}$ are of the form

$\displaystyle h_{i}(x)=s_{i}(x)+b(x)p_{i0}(x)+L_{g}b(x)$ $\displaystyle
p_{i}(x),\quad$ (22) $\displaystyle\text{for }i=1,2,$

as defined in (9).

###### Proof.

In order to verify safety, the candidate CBF $b$ must satisfy (5). As
introduced in Section 2.1, (5) is satisfied over the state
$x\in\mathbb{R}^{n}$ if and only if $L_{f}b(x)\geq 0$ over the set $K$.

Applying the KS Positivstellensatz in Proposition 2, we have $L_{f}b(x)\geq 0$
over $K$ if and only if there exists $a\in\mathbb{N}_{\geq 0}$ and
$h_{1},h_{2}\in P_{S}$ such that (21) is satisfied. Here, we have defined the
set $S$ with $r=0$ inequalities and $s=2$ equations. As noted in Remark 1,
since $r\leq 1$ we have $P_{S}=M_{S}$. Since $h_{1},h_{2}\in M_{S}$ they must
take the form of (9), which leads to (22). Then $L_{f}b(x)\geq 0$ over $K$ if
and only if

$h_{1}(x)L_{f}b(x)-h_{2}(x)-(L_{f}b(x))^{2a}=0$ (23)

for the $h_{1},h_{2}\in M_{S}$ and $a\in\mathbb{N}_{\geq 0}$ above. ∎

This theorem uses the same motivation as that in Clark (2021) to prove forward
invariance. However, we apply an alternate variation of the Positivstellensatz
to form a verification statement that is well-suited to numerical
implementation via linear programming and for scaling the number of candidate
CBFs. This difference arises in considering the nonnegativity of $L_{f}b$ over
the set $K$, as opposed to testing set emptiness of an augmented $S$. The
benefit of this alternate approach materializes in the next theorem.

A natural extension is safety verification for systems with $L$ candidate
CBFs. Each CBF $b_{i}$ corresponds to a basic semialgebraic set
$K_{i}=\\{x\in\mathbb{R}^{n}\mid b_{i}(x)=0,L_{g}b_{i}(x)=0\\}$ and an
independent safe set $\mathcal{B}_{i}=\\{x\in\mathbb{R}^{n}\mid b_{i}(x)\geq
0\\}$. The system safe set $\mathcal{B}$ is the intersection of all
independent safe sets, namely $\mathcal{B}=\cap_{i=1}^{L}\mathcal{B}_{i}$.

###### Theorem 2

Given a system defined by (3) and a collection of candidate CBFs,
$S=\\{b_{1},\dots,b_{L}\\}$, where $b_{i}\in\mathbb{R}[x]$ for $i=1,\dots,L$,
assume that $M_{S}$ satisfies the Archimedean property. Then $b_{i}\in S$ is a
CBF for all $i\in[L]$ and $\mathcal{B}\not=\emptyset$ if and only if the
following conditions are satisfied:

  1. 1.

Each of the $L$ candidate CBFs in $S$ satisfies Theorem 1.

  2. 2.

There do not exist SOS polynomials $s_{i}\in\Sigma[x]$ for $i=0,\dots,L$ such
that

$1+s_{0}(x)+\sum_{i=1}^{L}s_{i}(x)b_{i}(x)=0.$ (24)

###### Proof.

If each of the $L$ candidate CBFs satisfies the conditions of Theorem 1, then
all $b_{i}\in S$ are CBFs individually. This is shown by applying Theorem 1 to
each $b_{i}$. Thus, if Condition $1$ in the theorem statement is satisfied,
then for all $i\in[L]$ the CBF $b_{i}$ implies the existence of an input that
renders the system forward invariant to the safe set
$\mathcal{B}_{i}=\\{x\in\mathbb{R}^{n}\mid b_{i}(x)\geq 0\\}$.

When there are $L>1$ CBFs in a system, there must exist a solution to $L$
copies of (5) simultaneously. That is, we require the existence of an input
$u\in\mathbb{R}^{m}$ that satisfies the $L$ inequalities

$\displaystyle L_{g}b_{1}(x)u$
$\displaystyle\geq\kappa_{1}(b_{1}(x))-L_{f}b_{1}(x)$ (25)
$\displaystyle\vdots$ $\displaystyle L_{g}b_{L}(x)u$
$\displaystyle\geq\kappa_{L}(b_{L}(x))-L_{f}b_{L}(x).$

Condition 2 in the theorem statement then determines if such a $u$ exists and
thus determines if the intersection set
$\mathcal{B}=\cap_{i=1}^{L}\mathcal{B}_{i}$ is empty. Specifically, if
Condition 2 is satisfied, then there is no solution to (24) and the constant
polynomial $q=-1$ is not of the form of (9). Then, $-1\not\in M_{S}$. As
introduced in Section 2.2, the quadratic module $M_{S}$ is a
$\Sigma[x]$-module and $\Sigma[x]$ is a generating preprime in
$\mathbb{R}[x]$. Applying Proposition 4, since $M_{S}$ is Archimedean, if
$-1\not\in M_{S}$ then $\mathcal{B}\not=\emptyset$. Thus, satisfaction of
Conditions 1 and 2 implies $\mathcal{B}\not=\emptyset$.

To prove the other direction, now suppose that $\mathcal{B}\not=\emptyset$.
Clearly $\mathcal{B}\not=\emptyset$ implies $\mathcal{B}_{i}\not=\emptyset$
for all $i\in[L]$, which implies that Condition 1 holds for all $i\in[L]$.
Next, by applying the KS Positivstellensatz defined in Proposition 2, $-1\in
P_{S}$ if and only if $\mathcal{B}=\emptyset$. Thus,
$\mathcal{B}\not=\emptyset$ implies $-1\not\in P_{S}$. From Remark 1, we have
$M_{S}\subseteq P_{S}$ and thus $-1\not\in P_{S}$ implies $-1\not\in M_{S}$.
For $S=\\{b_{1},\dots,b_{L}\\}$, a polynomial $q\in M_{S}$ if and only if $q$
satisfies (9). The constant polynomial $q=-1\not\in M_{S}$, therefore there
cannot exist SOS polynomials $s_{0},s_{1},\dots,s_{L}$ such that (24) is
satisfied. Thus $\mathcal{B}\not=\emptyset$ implies that Conditions 1 and 2
hold, and the proof is complete. ∎

##  4 Single CBF Linear Program

In this section we solve Problem 2. We address the translation of the
verification statement derived in Theorem 1 for a single candidate CBF to a
linear program. The SDPs/LPs created from translating the Positivstellensätze
statements can involve both inequality and equality constraints containing the
SOS/DSOS polynomial decision variables. Inequality constraints of the form
$e(x)\leq 0$ are taken to be $-e(x)\in\mathcal{D}[x]$. This creates
constraints of the form $-e(x)=m^{T}(x)G_{k}(e)m(x)$ and
$G_{k}(e)\succeq_{dd}0$. Let $d$ be the degree of $e$, then $k=\lceil
d/2\rceil$.

There are a few methods for handling the equality constraints of the form
$e(x)=0$. One method is to constrain both $e(x)\in\mathcal{D}[x]$ and
$-e(x)\in\mathcal{D}[x]$ Ahmadi and Majumdar (2017). However, this can cause
numerical difficulties. Alternatively, $e(x)=m^{T}(x)G_{k}(e)m(x)$ with
$G_{k}(e)=0$ can be used to impose equality. Here, $G_{k}(e)=0$ is interpreted
element-wise. The following theorem uses this fact and ideas from Ahmadi and
Majumdar (2017) to create a linear program.

###### Theorem 3

Given a system (3) and a single candidate CBF $b\in\mathbb{R}[x]$, let $a\geq
0$ be an integer, $p_{10},p_{20}\in\mathbb{R}[x]$ and
$p_{1},p_{2}\in\mathbb{R}^{m}[x]$ be polynomials, and
$s_{1},s_{2}\in\mathcal{D}[x]$ be DSOS polynomials. Let $G_{k}$ be as defined
by (20) with $k=\lceil d/2\rceil$, where $d$ is the degree of its polynomial
argument. If the following LP has a solution, then $b$ is a CBF:

$\displaystyle\min_{z}$ $\displaystyle 0$ (26) s.t. $\displaystyle
Q_{i}\succeq_{dd}0\quad\quad\text{for }i=1,2$ $\displaystyle
G_{k}((s_{1}+bp_{10}+L_{g}bp_{1})L_{f}b-s_{2}$ $\displaystyle\quad\quad-
bp_{20}-L_{g}bp_{2}-(L_{f}b)^{2a})=0,$

where the decision variable is

$\displaystyle z=[c_{10}^{T}\;\;c_{20}^{T}$
$\displaystyle\text{col}(c_{1})^{T}\;\;\text{col}(c_{2})^{T}\;\;\text{uTri}(Q_{1})^{T}\;\;$
(27)
$\displaystyle\text{uTri}(\tau_{1})^{T}\;\;\text{uTri}(Q_{2})^{T}\;\;\text{uTri}(\tau_{2})^{T}]^{T},$

with $z\in\mathbb{R}^{2k^{2}+(2m+4)k}$, the DSOS variables take the form
$s_{i}(x)=m^{T}(x)Q_{i}m(x)$, the polynomial scalar variables take the form
$p_{i0}(x)=c_{i0}^{T}m(x)$, and the polynomial vector variables take the form
$p_{i}(x)=c_{i}^{T}m(x)$ for $i=1,2$.

###### Proof.

Applying Theorem 1, we require the existence of a solution to (21). In Theorem
1 we had $s_{1},s_{2}\in\Sigma[x]$. This creates an optimization problem over
the cone of SOS polynomials. Here, to create an LP, we inner-approximate the
SOS cone with the DSOS cone, as introduced in Section 2.3. By taking
$s_{1},s_{2}\in\mathcal{D}[x]$, each constraint of the form
$Q_{i}\succeq_{dd}0$ is enforced with the linear diagonal dominance
constraints from (16). Thus, there is no dependence on the indeterminate
$x\in\mathbb{R}^{n}$ when constraining $s_{1},s_{2}\in\mathcal{D}[x]$.

Likewise, the equation constraining $G_{k}$ in (26) has no dependence on the
indeterminate $x\in\mathbb{R}^{n}$. The Gram matrix operation, $G_{k}$,
removes dependence on the indeterminate while preserving equality with the
polynomial argument. Because $b$, $L_{f}b$, and $L_{g}b$ have no dependence on
$z$, each entry of $G_{k}$ is trivially a linear expression of the decision
variables. Therefore, each constraint in (26) is linear in the decision
variable $z$. As well, since the objective function is a constant $0$, the
program is linear.

Thus, if there is a solution to the linear program (26), then the conditions
of Theorem 1 are satisfied and the system is invariant to safe set
$\mathcal{B}$, verifying $b$ as a CBF. ∎

##  5 Multiple CBF Linear Programming

In this section we solve Problem 3. We consider the translation of the
multiple candidate verification statements derived in Theorem 2 to linear
programs. First, we establish a lemma that is utilized in the statement
transcription process.

###### Lemma 1

The cone of DSOS polynomials $\mathcal{D}[x]$ in $\mathbb{R}[x]$ is a
generating preprime.

###### Proof.

For any cone $\mathcal{C}\subseteq\mathbb{R}[x]$, $\mathcal{C}$ is closed
under addition, closed under multiplication, and $a^{2}\in\mathcal{C}$ if
$a\in\mathbb{R}[x]$ Bochnak et al. (2013). The cone
$\mathcal{D}[x]\subseteq\mathbb{R}[x]$ is closed under addition and
multiplication, and $1\in\mathcal{D}[x]$ since $1\in\mathbb{R}[x]$. By
definition, $\mathcal{D}[x]$ is a full-dimensional cone, i.e.,
$\mathcal{D}[x]-\mathcal{D}[x]=\mathbb{R}[x]$ Ahmadi and Majumdar (2017).
Thus, $\mathcal{D}[x]$ is a generating preprime in $\mathbb{R}[x]$ Powers
(2021). ∎

We define $M_{S,D}$ in an analogous manner to $M_{S}$ defined in (9), but with
the SOS polynomials replaced by DSOS polynomials. Then a polynomial $q\in
M_{S,D}$ if and only if $q$ is of the form

$q=s_{0}(x)+\sum_{i=1}^{L}s_{i}(x)b_{i}(x),$ (28)

where $s_{i}\in\mathcal{D}[x]$ for $i=0,\dots,L$. Thus, $M_{S,D}$ is a
$\mathcal{D}[x]$-module.

In the following theorem statement, we assume that $M_{S,D}$ is Archimedean.
The Archimedean property requires that the diameter of the set $\mathcal{B}$
is bounded by a natural number, as defined in Proposition 1. When the
assumption is not already satisfied by the polynomials in $\mathcal{B}$, it is
simple to enforce. By augmenting $S$ with the function
$C-\sum_{i=1}^{n}x_{i}^{2}\geq 0$, with $C\in\mathbb{N}\backslash\\{0\\}$
being a bound on the diameter of $\mathcal{B}$, the quadratic module with
respect to the augmented set $S^{\prime}=S\cap\\{x\in\mathbb{R}^{n}\mid
C-\sum_{i=1}^{n}x_{i}^{2}\geq 0\\}$ is Archimedean.

###### Theorem 4

Given a system (3) and a collection of candidate CBFs,
$S=\\{b_{1},\dots,b_{L}\\}$, assume that $M_{S,D}$ satisfies the Archimedean
property. Let $G_{k}$ be as defined by (20) with $k=\lceil d/2\rceil$, where
$d$ is the degree of its polynomial argument. If the following conditions are
satisfied, then for all $i\in[L]$ $b_{i}\in S$ is a CBF and
$\mathcal{B}\not=\emptyset$:

  1. 1.

Each of the $L$ candidate CBFs must independently produce solutions to the LP
(26), satisfying the conditions of Theorem 3.

  2. 2.

Let $s_{i}\in\mathcal{D}[x]$ for every $i\in[L]$. The following LP must not
have a solution:

$\displaystyle\min_{z}$ $\displaystyle 0$ (29) s.t. $\displaystyle
Q_{i}\succeq_{dd}0\quad\quad\text{for all }i=0,\dots,L$ $\displaystyle
G_{k}(1+s_{0}+\sum_{i=1}^{L}s_{i}b_{i})=0,$

where the decision variable is

$\displaystyle z=[\text{uTri}(Q_{0})^{T}\;\;\text{uTri}$
$\displaystyle(\tau_{0})^{T}\;\;\dots$ (30)
$\displaystyle\text{uTri}(Q_{L})^{T}\;\;\text{uTri}(\tau_{L})^{T}]^{T},$

with $z\in\mathbb{R}^{(k^{2}+k)(L+1)}$, and where the DSOS variables are
defined as $s_{i}(x)=m^{T}(x)Q_{i}m(x)$ for $i=[L]\cup\\{0\\}$. The variables
$\tau_{i}$ for $i=[L]\cup\\{0\\}$ are the symmetric bounding matrices used to
linearize the absolute value constraints from (16).

###### Proof.

Applying Theorem 2, each CBF candidate must independently satisfy (21) to be
verified as a CBF. In Theorem 2 we had $s_{i}(x)\in\Sigma[x]$ for
$i=0,\dots,L$. Here, we inner-approximate the SOS cone with the DSOS cone. As
explained in the proof of Theorem 3, using $s_{i}\in\mathcal{D}[x]$ for
$i=0,\dots,L$ transforms (24) from an SDP to an LP due to the diagonal
dominance constraints from (16) being linear inequalities. Similarly, the
equations constraining $G_{k}$ in (29) have no dependence on the indeterminate
$x\in\mathbb{R}^{n}$. Since each $b_{i}$ has no dependence on $z$, the
polynomial argument of $G_{k}$ is a linear expression of the decision
variables. Thus, (29) is a linear program.

From Theorem 2, we require that a solution does not exist to (24) to ensure
that $-1\not\in M_{S}$. As established in Lemma 1, $\mathcal{D}[x]$ is a
generating preprime in $\mathbb{R}[x]$ and $M_{S,D}$ is a
$\mathcal{D}[x]$-module. Then $M_{S,D}$ is an Archimedean
$\mathcal{D}[x]$-module due to the Archimedean assumption imposed in the
theorem statement. By Proposition 4, $-1\not\in M_{S,D}$ implies
$\mathcal{B}\not=\emptyset$. Then the lack of solution to the LP in (29)
implies $\mathcal{B}\not=\emptyset$. ∎

The safety verification program scales linearly with the number of candidate
CBFs, with $L$ candidate CBFs there are $L+1$ linear programs. In total, there
are $3L+1$ DSOS polynomial decision variables across the $L+1$ LPs that need
to be solved in Theorem 4. We note that the multiple CBF verification problem
can be solved using the preorder instead of the quadratic module. However,
doing this leads to an exponential growth rate in the number of DSOS
polynomial decision variables. The Archimedean assumption allows for the use
of the quadratic module and the improved computational transcription that
results.

##  6 Simulations

The proposed method for multiple CBF verification was simulated in MATLAB, and
the SPOT toolbox developed in Ahmadi and Majumdar (2017) was used for both SOS
and DSOS problems.111Code available at: https://github.com/elliempond/
SatelliteInspectionCBF.git SPOT is a parser that transforms SOS problems to
semidefinite programs and DSOS programs to linear programs, and we use it for
both to provide a fair comparison between the amounts of computation time they
require. We used the SDP solver SeDuMi for both the SOS and DSOS programs
Sturm (1999). The simulations were computed on a workstation running Ubuntu
20.04 with a 3.30 GHz Intel Core processor and 128 GB of RAM.

We consider a satellite inspection problem with $L$ chaser satellites indexed
over $[L]$ and one target satellite in a circular orbit, depicted in Figure 1.
The objective of this problem is for each of the $L$ chaser satellites to
approach the target satellite with a certain relative position. We use the
linearized Clohessy-Wiltshire equations of motion of relative position and
velocity for each of the $i\in[L]$ chaser satellites given by Curtis (2013)

$\displaystyle\ddot{x}_{i}$
$\displaystyle=2n\dot{y}_{i}+3n^{2}+\frac{F_{x,i}}{m_{i}}$ (31)
$\displaystyle\ddot{y}_{i}$
$\displaystyle=-2n\dot{x}_{i}+\frac{F_{y,i}}{m_{i}}$
$\displaystyle\ddot{z}_{i}$ $\displaystyle=-n^{2}z_{i}+\frac{F_{z,i}}{m_{i}},$

with state
$[x_{i}\;\;y_{i}\;\;z_{i}\;\;\dot{x}_{i}\;\;\dot{y}_{i}\;\;\dot{z}_{i}]^{T}$,
input $[F_{x,i}\;\;F_{y,i}\;\;F_{z,i}]^{T}$, mass of the chaser satellite
$m_{i}$, and mean motion $n$. The mean motion is the average angular speed of
a satellite during one full orbit. We let
$r_{i}=[x_{i}\;\;y_{i}\;\;z_{i}]^{T}$ be the relative position vector between
chaser $i$ and the target consisting of the radial, tangential, and out-of-
plane relative distances, respectively. This admits dynamics in the form of
(3). For each $i\in[L]$, we form barrier functions between chaser $i$ and the
target satellite as

$b_{i}(z)=r_{i}^{T}r_{i}+\frac{m_{i}}{T_{i}}\dot{r}_{i}^{T}\dot{r}_{i}-R_{t}^{2},$
(32)

where $R_{t}$ is the minimum safe radius about the target satellite and
$T_{i}$ is the nominal thrust of each chaser.

Figure 1: The satellite inspection problem depicted with $L=3$ chaser
satellites. The target satellite is represented by the red dot in a circular
orbit.

Following Theorem 4, this CBF verification problem consists of $L$ linear
programs in the form of (26). These LPs verify that each candidate of the form
of (32) is a CBF. Additionally, we have one linear program in the form of (29)
that verifies that $\mathcal{B}=\\{z\in\mathbb{R}^{6L}\mid b_{1}(z)\geq
0,\dots,b_{L}(z)\geq 0\\}\not=\emptyset$. We consider 3U cubesat
specifications for the chaser satellites with a mass of $m_{i}=2$ kg, nominal
thrust $T_{i}=0.5$ N for all $i\in[L]$, and the mean motion for a circular low
earth orbit $n=0.0010$ rad/s. We consider close approach and proximity
operations at $R_{t}=0.5$ km.

Table 1: Computation time. $L$ | DSOS (s) | SOS (s) | % Reduction
---|---|---|---
$1$ | $1.0$ | $1.7$ | $41.2\%$
$2$ | $2.1$ | $8.4$ | $75.0\%$
$3$ | $4.3$ | $29.5$ | $85.4\%$
$4$ | $10.2$ | $114.8$ | $91.1\%$
$5$ | $25.0$ | $499.0$ | $95.0\%$
$6$ | $63.0$ | $1215.4$ | $94.8\%$
$7$ | $156.5$ | $3423.7$ | $95.4\%$

Table 1 gives the computation time for up to $7$ chaser satellites. For $L=1$
satellite, only Theorem 3 was required for verification. There is little
improvement between the DSOS linear program and the SOS semidefinite program
for one satellite. However, the improvement is immediate for $L\geq 2$. The
DSOS programs required significantly less time to obtain the same affirmative
verification as the corresponding SOS program. While there can be a loss of
accuracy when inner-approximating SOS programs with DSOS LPs, it was not seen
with this example problem in the sense that the DSOS program produced an
affirmative verification for all scenarios that were considered, and this
verification is in agreement with the SOS program verification.

These results show that the transcription of CBF verification to linear
programs provides a substantial reduction in computation time while providing
the same feasibility assurances as the more complex SOS verification
formulation. In fact, Table 1 shows that for $L\geq 4$ chaser satellites the
LP formulation reduces computation time by more than $90$%, which is a
significant reduction. These results suggest that the LP formulation can not
only reduce the computations required for CBF verification, but also provide
new capabilities to verify larger problems.

##  7 Conclusion

We have presented, to the best of the authors’ knowledge, the first
verification procedure for the validation of candidate control barrier
functions using linear programming. We have also contributed a method of
multiple CBF verification that scales linearly with the number of candidate
functions. In future work, these verification methods will be extended to
high-order CBFs, dynamic systems with input constraints, and distributed
linear CBF certification in multi-agent systems.

## References

  * Gao (2010) (2010).  _Predictive Control of Autonomous Ground Vehicles With Obstacle Avoidance on Slippery Roads_ , volume ASME 2010 Dynamic Systems and Control Conference, Volume 1 of _Dynamic Systems and Control Conference_.  10.1115/DSCC2010-4263.  URL https://doi.org/10.1115/DSCC2010-4263.
  * Ahmadi and Majumdar (2017) Ahmadi, A.A. and Majumdar, A. (2017).  Dsos and sdsos optimization: More tractable alternatives to sum of squares and semidefinite optimization.  10.48550/ARXIV.1706.02586.  URL https://arxiv.org/abs/1706.02586.
  * Althoff and Dolan (2014) Althoff, M. and Dolan, J.M. (2014).  Online verification of automated road vehicles using reachability analysis.  _IEEE Transactions on Robotics_ , 30(4), 903–918.  10.1109/TRO.2014.2312453.
  * Ames et al. (2019) Ames, A.D., Coogan, S., Egerstedt, M., Notomista, G., Sreenath, K., and Tabuada, P. (2019).  Control barrier functions: Theory and applications.  In _2019 18th European Control Conference (ECC)_ , 3420–3431.  10.23919/ECC.2019.8796030.
  * Black and Panagou (2022) Black, M. and Panagou, D. (2022).  Adaptation for validation of a consolidated control barrier function based control synthesis.  10.48550/ARXIV.2209.08170.  URL https://arxiv.org/abs/2209.08170.
  * Bochnak et al. (2013) Bochnak, J., Coste, M., and Roy, M. (2013).  _Real Algebraic Geometry_.  Ergebnisse der Mathematik und ihrer Grenzgebiete. 3. Folge / A Series of Modern Surveys in Mathematics. Springer Berlin Heidelberg.  URL https://books.google.com/books?id=GJv6CAAAQBAJ.
  * Clark (2021) Clark, A. (2021).  Verification and synthesis of control barrier functions.  In _2021 60th IEEE Conference on Decision and Control (CDC)_ , 6105–6112.  10.1109/CDC45484.2021.9683520.
  * Cortez et al. (2022) Cortez, W.S., Tan, X., and Dimarogonas, D.V. (2022).  A robust, multiple control barrier function framework for input constrained systems.  10.48550/ARXIV.2205.13726.  URL https://arxiv.org/abs/2205.13726.
  * Curtis (2013) Curtis, H. (2013).  _Orbital mechanics for engineering students_.  Butterworth-Heinemann.
  * Feng et al. (2015) Feng, S., Xinjilefu, X., Atkeson, C.G., and Kim, J. (2015).  Optimization based controller design and implementation for the atlas robot in the darpa robotics challenge finals.  In _2015 IEEE-RAS 15th International Conference on Humanoid Robots (Humanoids)_ , 1028–1035.  10.1109/HUMANOIDS.2015.7363480.
  * Isaly et al. (2022) Isaly, A., Ghanbarpour, M., Sanfelice, R.G., and Dixon, W.E. (2022).  On the feasibility and continuity of feedback controllers defined by multiple control barrier functions for constrained differential inclusions.  In _2022 American Control Conference (ACC)_ , 5160–5165.  10.23919/ACC53348.2022.9867227.
  * Jacobi (2001) Jacobi, T. (2001).  A representation theorem for certain partially ordered commutative rings.  _Mathematische Zeitschrift_ , 237, 259–273.
  * Jankovic and Santillo (2021) Jankovic, M. and Santillo, M. (2021).  Collision avoidance and liveness of multi-agent systems with cbf-based controllers.  In _2021 60th IEEE Conference on Decision and Control (CDC)_ , 6822–6828.  10.1109/CDC45484.2021.9682854.
  * Kunchev et al. (2006) Kunchev, V., Jain, L., Ivancevic, V., and Finn, A. (2006).  Path planning and obstacle avoidance for autonomous mobile robots: A review.  In B. Gabrys, R.J. Howlett, and L.C. Jain (eds.), _Knowledge-Based Intelligent Information and Engineering Systems_ , 537–544. Springer Berlin Heidelberg, Berlin, Heidelberg.
  * Landi et al. (2019) Landi, C.T., Ferraguti, F., Costi, S., Bonfè, M., and Secchi, C. (2019).  Safety barrier functions for human-robot interaction with industrial manipulators.  In _2019 18th European Control Conference (ECC)_ , 2565–2570.  10.23919/ECC.2019.8796235.
  * Powers (2021) Powers, V. (2021).  _Certificates of Positivity for Real Polynomials_.  Developments in Mathematics. Springer Cham.
  * Powers and Wörmann (1998) Powers, V. and Wörmann, T. (1998).  An algorithm for sums of squares of real polynomials.  _Journal of pure and applied algebra_ , 127(1), 99–104.
  * Roumeliotis and Mataric (2000) Roumeliotis, S. and Mataric, M. (2000).  "small-world" networks of mobile robots.  1093\.
  * Sturm (1999) Sturm, J.F. (1999).  Using sedumi 1.02, a matlab toolbox for optimization over symmetric cones.  _Optimization methods and software_ , 11(1-4), 625–653.
  * Vasic and Billard (2013) Vasic, M. and Billard, A. (2013).  Safety issues in human-robot interactions.  In _2013 IEEE International Conference on Robotics and Automation_ , 197–204.  10.1109/ICRA.2013.6630576.
  * Wang et al. (2017) Wang, L., Ames, A.D., and Egerstedt, M. (2017).  Safety barrier certificates for collisions-free multirobot systems.  _IEEE Transactions on Robotics_ , 33(3), 661–674.  10.1109/TRO.2017.2659727.
  * Wang et al. (2018) Wang, L., Han, D., and Egerstedt, M. (2018).  Permissive barrier certificates for safe stabilization using sum-of-squares.  In _2018 Annual American Control Conference (ACC)_ , 585–590.  10.23919/ACC.2018.8431617.
  * Xiao and Belta (2019) Xiao, W. and Belta, C. (2019).  Control barrier functions for systems with high relative degree.  In _2019 IEEE 58th conference on decision and control (CDC)_ , 474–479. IEEE.
  * Xu et al. (2015) Xu, X., Tabuada, P., Grizzle, J.W., and Ames, A.D. (2015).  Robustness of control barrier functions for safety critical control**this work is partially supported by the national science foundation grants 1239055, 1239037 and 1239085.  _IFAC-PapersOnLine_ , 48(27), 54–61.  https://doi.org/10.1016/j.ifacol.2015.11.152.  Analysis and Design of Hybrid Systems ADHS.
  * Zacharaki et al. (2020) Zacharaki, A., Kostavelis, I., Gasteratos, A., and Dokas, I. (2020).  Safety bounds in human robot interaction: A survey.  _Safety Science_ , 127, 104667.  https://doi.org/10.1016/j.ssci.2020.104667.
  * Zohaib et al. (2013) Zohaib, M., Pasha, M., Riaz, R.A., Javaid, N., Ilahi, M., and Khan, R.D. (2013).  Control strategies for mobile robot with obstacle avoidance.  10.48550/ARXIV.1306.1144.  URL https://arxiv.org/abs/1306.1144.