{'fraction_non_alphanumeric': 0.05964599916212819, 'fraction_numerical': 0.014558022622538752, 'mean_word_length': 3.8041509433962264, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 12, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 32, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
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. One approach to ensuring safety is to construct a Control Barrier Function (CBF) such that the system is safe when the CBF is nonnegative, and then choose a control input to ensure nonnegativity of the CBF at each time step, provided that such an input exists. This paper investigates the problems of verification and synthesis of control barrier functions. In the area of verification, we use the algebraic-geometric Positivstellensatz to construct convex equivalent conditions for a CBF to ensure safety. We extend these conditions to control policies based on unions and intersections of CBFs, high-order CBFs, and systems with trigonometric dynamics, actuation constraints, and Euler-Lagrange dynamics. In the area of synthesis, we propose algorithms for constructing CBFs, namely, an alternating-descent approach, a local CBF approach, and a Newton's method approach. We prove that the latter algorithm guarantees local convergence to a CBF at a quadratic rate.


I. INTRODUCTION
Safety is a critical property of autonomous control systems in medical, manufacturing, transportation, and other vital applications. From a control-theoretic perspective, safety is typically characterized by positive invariance of a particular safe region, for example, ensuring that a vehicle remains a desired safe distance from humans or obstacles, or maintaining the temperature of a system within tolerated limits. Methodologies such as energy-based methods [1], counterexampleguided synthesis [2], and abstraction-based verification [3] have been proposed to verify system safety and design safe control algorithms.
Among these techniques, energy methods such as control barrier functions and barrier certificates have attracted significant research attention [4]- [6]. These methods map the safety constraint to a barrier function such that the system is safe if the barrier function is nonnegative. The control input is then chosen to ensure that the derivative of the barrier function is nonnegative at the boundary of the safe region. The main advantage of this approach is that it provides safety guarantees while also being minimally invasive, since additional control effort is only needed as the system approaches the safety boundary. While CBFs have shown great promise in a variety of applications including bipedal locomotion [7], autonomous driving [8], and spacecraft rendezvous [9], challenges remain. One practical difficulty is that there may not be a control input to satisfy the barrier function constraint at each time instant, which may lead to safety violations. This is the challenge of verifying a CBF. While some sufficient heuristic methods based on convex sum-of-squares optimization have been proposed [10], [11], they are not complete, i.e., they may fail to verify a CBF even if the CBF is valid. These challenges are especially salient for systems with actuation constraints and non-polynomial dynamics.
Another related challenge is synthesizing CBFs that will ensure a desired safety constraint. Typically, CBFs are constructed using trial-and-error or domain knowledge. While approaches to synthesizing CBFs using alternating descent sumof-squares [5] and neural networks [12], [13] are promising, these algorithms are not guaranteed to return a CBF with verifiable safety guarantees.
In this paper, we propose a semialgebraic optimization framework for verification and synthesis of control barrier functions. On the verification side, we first show that the verification problem is NP-hard and that existing SOS-based heuristics are incomplete. We then formulate exact SOS conditions for a function to be a CBF using the Positivstellensatz, which is a result from algebraic geometry that gives equivalent conditions for existence of solutions to systems of polynomial equations and inequalities. We generalize our approach to derive exact (albeit high-dimensional) SOS programs for intersections of multiple CBFs, high-order CBFs, semi-algebraic sets, actuation-constrained systems, and systems with Euler-Lagrange dynamics. We also propose a sufficient approach for systems with trigonometric dynamics. These generalizations ensure that our framework is applicable to a variety of different constraints, safe regions, and system dynamics that may arise in practical applications of safe control.
On the synthesis side, we propose three algorithms. The first is an alternating descent approach, similar to [11], which we generalize to high-order CBFs. The second constructs local CBFs for systems with fixed points, with driftless systems as an important special case. The third uses Newton's method in function space to synthesize a CBF. To the best of our knowledge, it is the first synthesis algorithm with guaranteed local convergence to a CBF.
The paper is organized as follows. Section II presents the related work. Section III presents the system model and background material. Section IV presents a convex, semialgebraic framework for verification of CBFs. Section V presents algorithms for synthesizing CBFs. Section VI presents simulation results. Section VII concludes the paper.
A standard approach to constructing CBFs is to jointly select a CBF and a controller that satisfies the CBF constraint at each time step. A sum-of-squares constraint is used to ensure that the Lie derivative of the CBF is nonnegative at the boundary of the safe region [5], [11]. If these approaches terminate and return a controller and CBF satisfying the constraint, then safety is guaranteed. However, even if the system is safe, there is no guarantee that these approaches terminate and return a safe control policy. An approach to refining CBFs via Hamilton-Jacobi-Bellman reachability was proposed in [21]. Safe synthesis under actuation constraints was considered in [22], but the derived conditions are sufficient but not necessary.
Our approach can be placed in the broader context of semialgebraic methods for verification of control systems. This approach was originally proposed for reachability verification via barrier certificates [4], and has more recently been applied to control barrier certificates. To the best of our knowledge, however, the present paper is the first to propose tight necessary and sufficient conditions for safety using the algebraicgeometric Positivstellensatz. Moreover, we are the first to propose a single framework that incorporates trigonometric functions, actuation constraints, and Euler-Lagrange dynamics.
The feasibility of CBF-based control policies has been investigated and heuristic methods have been proposed. The most widely-used is the high-order CBF (HOCBF), which guarantees safety for high relative-degree systems when there is a single constant r such that the r-th order Lie derivative is always nonzero [16]. We propose an algorithm for computing the safe region corresponding to an HOCBF. In [23], sufficient but not necessary conditions for feasibility of CBFs were proposed.
An emerging approach to CBF synthesis is to learn CBFs from samples of safe and unsafe trajectories [1], [24], [25]. Since learned CBFs must still be verified, the present paper can be viewed as complementary to these works.
The preliminary conference version of this paper presented an algebraic-geometric framework for verifying CBFs and HOCBFs, but did not consider unions of CBFs, Euler-Lagrange dynamics, trigonometric functions, or actuation constraints [26]. Moreover, the preliminary algorithms for synthesizing CBFs did not guarantee convergence to a CBF.

III. MODEL AND PRELIMINARIES
This section presents the system model and needed background.

A. System Model
We consider a nonlinear control system with dynamicṡ where x(t) ∈ R n denotes the state, u(t) ∈ R m is a control input, and f : R n → R n and g : R n → R n×m are continuous functions. Throughout the paper, we let [x] i denote the i-th element of x ∈ R n . The system is required to remain in a safe region C, which is defined by We define a safe control policy as follows.
Definition 1: A function µ : R n → R m is a safe control policy if (i) there exists a setC withC ⊆ C, and (ii) for any A set is controlled positive invariant (CPI) if it is positive invariant for some control policy µ.

B. Background on Control Barrier Functions
Control Barrier Functions (CBFs) have been proposed to ensure safety of nonlinear systems, and are defined as follows.
(2) The following result gives a safety proof for systems with CBFs.
Theorem 1 ( [5]): Suppose that b is a CBF, b(x(0)) ≥ 0, and u(t) satisfies (2) for all t. Then the set . . , M , then any control policy that satisfies (2) is a safe control policy. One challenge with CBF-based control policies is that the constraint (2) may become infeasible if ∂b ∂x g(x) = 0. High-order CBFs (HOCBFs), defined as follows, have been proposed to address this limitation.
The following result establishes safety of HOCBFs.
Theorem 2 ( [16]): If b is a HOCBF, then the set r i=0 C i is positive invariant under any control policy that satisfies (3) for all x ∈ r i=0 C i . As a corollary to Theorem 2, if r i=0 C i ⊆ C and b(x) is an HOCBF, then any control policy satisfying (3) is a safe control policy.

C. Preliminary Results
We now give two needed background results, namely, the Positivstellensatz and Farkas's Lemma. Recall that a Sum-of-Squares (SOS) polynomial is a polynomial f (x) such that for some polynomials g 1 (x), . . . , g k (x). Selecting coefficients of f (x) to ensure that f (x) is SOS can be represented as a semidefinite program, a procedure known as SOS optimization [27], [28]. The cone Σ[q 1 , . . . , q k ] associated with polynomials q 1 , . . . , q k is equal to the set of polynomials f with where p 0 , . . . , p N are SOS and β 1 , . . . , β N are products of powers of the q i 's. For a set of polynomials f 1 , . . . , f N , we define the ideal generated by the polynomials as The Positivstellensatz, stated as follows, gives equivalent conditions for existence of solutions to systems of polynomial equations and inequalities.
Theorem 3 (Positivstellensatz [29]): Consider a collection of polynomials {f j : j = 1, . . . , r}, {g i : i = 1, . . . , m} and {h k : k = 1, . . . , s}. Then the set is empty if and only if there exist polynomials f , g, and h When the f j 's, g i 's, and h k 's are given, attempting to find solutions of the equation f (x) + g(x) + h(x) 2 = 0 is an SOS optimization problem [27].
Finally, Farkas's Lemma is as follows. Lemma 1 (Farkas's Lemma [30]): Let A ∈ R m×n and b ∈ R m . Then exactly one of the following is true: 1) There exists x ∈ R n with Ax ≤ b 2) There exists y ∈ R m with A T y = 0, b T y < 0, and y ≥ 0. Farkas's Lemma gives equivalent conditions for existence of solutions of linear inequalities.

IV. PROBLEM FORMULATION: CBF VERIFICATION
This section presents our approach for CBF verification. We first give the problem statement and complexity results. We then formulate the problem of verifying CBFs as a sum-of-squares optimization. We generalize the verification problem to incorporate multiple CBFs, HOCBFs, dynamics with trigonometric functions, and actuation constraints.

A. Problem Statement and Complexity Results
The problem studied in this section is stated as follows. Problem 1: Given a function b : R n → R, dynamics (1), and a safety constraint C, determine if b is a CBF for safety constraint C.
The following initial result gives necessary and sufficient conditions for b to be a CBF.
We observe that, in the statement of Problem 1, we do not require that the control policy is continuous, although we develop sufficient conditions for continuity in Proposition 4. We first consider the complexity of Problem 1.
Proposition 2: Problem 1 is NP-hard. Proof: NP-hardness of Problem 1 is equivalent to NPhardness of checking whether there exists x satisfying the conditions of Proposition 1. We will show that there exists a polynomial time reduction of the NP-hard problem of checking nonnegativity of a polynomial to the problem of verifying conditions of Proposition 1.
Let r : R n → R be a polynomial.
One heuristic approach to Problem 1 is to search for a polynomial θ(x) such that is SOS [5]. While this approach can be formulated as a convex optimization problem and gives a sufficient condition, it is not complete as shown by the following. Proposition 3: There exist polynomials b, f , and g such that b is a CBF and, for any polynomial θ and class-K polynomial α, (4) is not a sum-of-squares. Proof: We next show that, for any polynomials α and θ, (4) is not SOS. Suppose that, in fact, (4) is SOS. Since α is a class-K polynomial, α(0) = 0 and hence α(z) = zα(z) for some polynomial α : R → R. Hence (4) is equivalent to We next give an equivalent condition for a function to be a CBF based on the Positivstellensatz. (1) if and only if there exist polynomials η, θ 1 , . . . , θ m , SOS polynomials α 0 (x) and α 1 (x), and an integer r such that Moreover, x(t) remains in the safe region C under a CBF policy for b if (5) holds and there exist SOS polynomials β 0 (x) and β 1 (x) and a polynomial ω(x) such that is equal to the set of polynomials of the form α 0 (x) + α 1 (x) ∂b ∂x f (x) where α 0 and α 1 are SOS. Hence the conditions of Proposition 1 are equivalent to (5) by Theorem 3. Now, suppose that (5), and hence b(x(t)) ≥ 0 for all t under any control policy satisfying (2). It therefore suffices to show that b(x(t)) ≥ 0 for all t implies that h(x(t)) ≥ 0 for all t. If not, then there exists a point satisfying h(x) = 0 and b(x) ≥ 0. This contradicts (6) by Theorem 3.
One potential drawback of CBF-based control policies is that there may not exist a smooth controller satisfying the conditions of the CBF. The following result builds on Theorem 4 to gives sufficient conditions for existence of a smooth safe policy.
Proof: Consider the control policy defined by Dividing through by Hence when b(x) = 0, we haveḃ(x(t)) ≥ 0, implying that {b(x) ≥ 0} is positive invariant by Nagumo's Theorem. We note that, since α 1 (x) is SOS, the condition α 1 (x) > 0 can be verified by checking if the matrix representation of α 1 (x) is positive definite.

B. Verification of Multiple CBFs
This section considers the problem of checking whether, for a given set of polynomials We have the following equivalent condition for controlled positive invariance.
, and yet the set is not CPI. Let µ be a control policy that chooses u(t) satisfying for all i with b i (x(t)) = 0 at each time t if such a u exists. By (i) and (iii), such a u always exists. Henceḃ i (x(t)) ≥ 0 whenever b i (x(t)) = 0 and positive invariance holds by Nagumo's Theorem.
The following intermediate result will be used to construct a convex formulation that is equivalent to the conditions of Proposition 5. As a preliminary, for any Proof: It suffices to show that conditions (c)-(e) above are equivalent to condition (iii) of Proposition 5. We have that condition (iii) of Proposition 5 holds if for any By Farkas's Lemma, this is equivalent to the non-existence of y satisfying conditions (c)-(e). Based on this result, we can define the following equivalent conditions for a set of polynomials to define a controlled positive invariant set.
integers {r i : i ∈ S}, and a polynomial Moreover, for a given safe region and ω i such that for all i = 1, . . . , M Proof: Eq. (12) is equivalent to the conditions of Lemma 2 by Theorem 3. Furthermore, in order for the control policy to ensure safety, we must have that there is no point with h i (x) = 0 and b j (x) ≥ 0 for j = 1, . . . , M . This condition is equivalent to (13) by Theorem 3.
While Theorem 5 leads to a convex formulation for verifying multiple CBFs, it requires solving SOS programs with 2 M SOS constraints. High-Order CBFs are a tractable subclass of multiple CBF-based control policies; their tractability follows from the fact that the control input u is only used to ensure positive invariance of ψ r , while positive invariance of the remaining sets is satisfied by construction. We have the following approach.
Theorem 6: If b(x) is a polynomial with relative degree r with respect to (1), then b(x) and ψ 0 , . . . , ψ r define a HOCBF if and only if there exist polynomials η(x), , and an integer s such that This is equivalent to (14) by Theorem 3. Now, we want to show that if x(t) ∈ C i for i = 0, . . . , r and h(x(0)) ≥ 0, then h(x(t)) ≥ 0 for all t if (15) holds. If (15) holds, then there is no x satisfying x ∈ C i for i = 0, . . . , r and h(x) = 0. Since x(t) ∈ C i for all t and i = 0, . . . , r, this implies that x(t) never reaches the boundary of C and hence remains in C for all time t.

C. Verification of Semi-Algebraic Sets
A set S is semi-algebraic if there exist polynomials b ij : i = 1, . . . , N, j = 1, . . . , K for some integers N and K such that In what follows, we present an approach for verifying controlled positive invariance of semi-algebraic sets. As a preliminary, we consider the case where for polynomials b 1 , . . . , b N . Lemma 3: The set S defined in (17) ∂bi ∂x g(x) = 0 for i ∈ S, and ∂bi ∂x f (x) < 0 for i ∈ S. Proof: Suppose that there exists such an x. We have that x lies outside the sets {b i (x) ≥ 0} for i / ∈ S and at the boundary of the sets {b i (x) ≥ 0} for i ∈ S. Furthermore, for all i ∈ S, we haveḃ i (x) < 0 regardless of the control input. Hence the state trajectory will leave the set S if x(0) = x.
Conversely, let µ be a control policy such that, for all sets S and all Hence for any x on the boundary of S, there exists at least one i with b i (x) = 0 andḃ i (x) ≥ 0. We then have that, if x(t) reaches the boundary of S, then there exists δ > 0 such that x(t ′ ) ∈ S for t ′ ∈ (t, t + δ).
The conditions of Lemma 3 can be mapped to an SOS program via the following.
Theorem 7: The set S defined in (17) is CPI if and only if for any S ⊆ {1, . . . , N }, there exists and integers r S i for i = 1, . . . , N such that Moreover, the set S is contained in the safe region if, for all i = 1, . . . , N , there exist SOS polynomials β i1 and β i0 as well as a polynomial ω i such that The proof generalizes the proofs of Proposition 5 and Lemma 3 and is omitted due to space constraints.
We now formulate equivalent conditions to Lemma 4 that can be mapped to an SOS program.
∂bT i ∂x f (x) T y < 0, where b Ti is defined as in Lemma 4.
We finally give a convex framework for verifying positive invariance of semialgebraic sets.

D. Dynamics with Trigonometric Functions
In what follows, we present an approach for verifying safety of systems with dynamics that contain trigonometric functions. We consider a system (1) such that there exists l ∈ {1, . . . , n} and polynomials f , g, and b such that where r i = φ(x j ) for some j ∈ {(l + 1), . . . , n} and φ ∈ {sin, cos, tan, csc, sec, cot}. This condition implies that there exist a subset of variables x l+1 , . . . , x n that only appear as arguments of trigonometric functions. We further assume that each of (20)-(23) is well-defined within the safe region, i.e., if tan x i appears in the system dynamics, then cos x i = 0 throughout the safe region. For each i ∈ {(l + 1), . . . , n}, we define auxiliary variables z ij , j = 1, . . . , 6. Each variable will define a different trigonometric function of x i , i.e., z i1 = sin x i , z i2 = cos x i , z i3 = tan x i , z i4 = csc x i , z i5 = sec x i , and z i6 = cot x i . We note that not all auxiliary variables may be required to describe the system dynamics, for example, only z i1 and z i2 are required if the system dynamics only contain functions of sin x i and cos x i . These auxiliary variables are incorporated into the Lie derivative computations of b(x) as follows. For i ≤ l, we have ∂b ∂xi = ∂b ∂xi . For i ∈ {(l + 1), . . . , n}, we have Finally, to ensure that the variables z ij are consistent with trigonometric functions, we impose the constraints We have the following result.
Proposition 6: For a system described by (1) and (20) such that τ + φ + 1 = 0, then the condition {h(x) ≥ 0} is satisfied for all time t. Proof: Proposition 6 gives sufficient conditions for safety based on non-existence of solutions to a system of polynomial equations.
Theorem 9 gives an SOS program for verifying safety of CBFs with trigonometric functions, at the cost of introducing additional polynomial constraints and variables.

E. Actuation Constraints
We next consider systems with actuation constraints of the form Au ≤ c for some matrix A ∈ R p×m and c ∈ R p . The following result gives a necessary and sufficient condition for b(x) to be a CBF in the presence of such an actuation constraint.
Proposition 7: The function b(x) is a CBF if and only if there do not exist x ∈ R n and y ∈ R p+1 satisfying Proof: In order to ensure thatḃ(x(t)) ≥ 0 whenever b(x(t)) = 0, it is necessary and sufficient to ensure that for every x with b(x) = 0, there exists u satisfying By Farkas's Lemma, the existence of such a u is equivalent to the non-existence of y satisfying (24). Define a set of polynomials d 1 , . . . , d m by so that the condition Proof: The proof follows from applying Theorem 3 to the polynomial constraints (24) in Proposition 7.
We observe that this approach can be applied to incorporating multiple safety constraints h 1 , . . . , h M as well as verifying multiple CBFs as in Section IV-B. We omit this generalization due to space constraints and for simplicity of the exposition.

F. Euler-Lagrange Dynamics
In what follows, we consider a generalization of (1) to systems with Euler-Lagrange dynamics that are described by ODEs of the form We further assume that the control input is constrained by The goal is to verify a CBF of the form b(x,ẋ). We have the following initial result.
for anyẍ satisfying (25). Proof: By Nagumo's Theorem, the set is controlled positive invariant if and only if, for any (x,ẋ) with b(x,ẋ) = 0, we haveḃ(x,ẋ) ≥ 0. This is equivalent to the existence of u that ensures (26) for all feasible values ofẍ, i.e., for all solutions to (25).
We will next derive conditions for verifying the conditions of Proposition 8 for a given function b. As a preliminary, we have the following generalization of Farkas's Lemma to strict inequalities.
Lemma 6 ( [30]): Exactly one of the following statements is true: 1) There exists an x satisfying Ax < b and Bx ≤ c.
2) There exist y and z that satisfy y ≥ 0, z ≥ 0, A T y + B T z = 0, and either b T y + c T z < 0 or (b T y + c T z = 0 and y = 0). We note two special cases of this lemma. First, if we are given an equality constraint Bx = c instead of an inequality constraint, then we can remove the constraint z ≥ 0. Second, if b = 0 and c = 0, then the second condition of Lemma 6 reduces to y ≥ 0, z ≥ 0, A T y + B T z = 0, and y = 0.
We next present a preliminary result before giving our main conditions. Lemma 7: The function b(x,ẋ) is a CBF for (25) if and only if, for every (x,ẋ) with b(x,ẋ) = 0, at least one of the following conditions holds: 1) There exists y ∈ R, z ∈ R m , and a vertex s of the hypercube U such that y ≥ 0 and 2) There exist z ∈ R m , y ∈ R, and vertices s, s ′ of the hypercube U such that y > 0 and ∂b ∂ẋ Proof: The conditions of Proposition 8 can be stated as, for some u ∈ U, there does not existẍ satisfying (25) and (26). By Lemma 6, these conditions are equivalent to at least one of the following holding: (i) There exists u ∈ U, y ∈ R ≥0 , and z ∈ R m such that (ii) There exists u ∈ U, y ∈ R >0 , and z ∈ R m such that Turning first to condition (i), we have that u T z is minimized at the vertices of U. Hence, it is sufficient to check whether (32) and (33) hold at the vertices, resulting in condition 1 of the lemma. Next, we examine condition (ii). For a given value of z, let v min and v max be the minimum and maximum of u T z over u ∈ U, respectively. Eq. (34) holds iff Since v min and v max are achieved at vertices of U, this is equivalent to condition 2 of the lemma. As a corollary to Lemma 7, a safe control policy can be constructed for a system (25) by selecting u ∈ U, y > 0, and z ∈ R m such that We now present a further equivalent condition for b(x,ẋ) to be a CBF. As a preliminary, for vertices s, s ′ of U, define The function b is a CBF for the system with dynamics (25) if and only if there do not exist x,ẋ, w s ≥ 0, v s,s ′ ≥ 0, r s ≥ 0, and q s,s ′ ≥ 0 with w s , v s,s ′ = 0 where s and s ′ are indexed as the vertices in U such that A T s w s +B T r s = 0 for all s vertices of U and C T v s,s ′ + D(s, s ′ , x,ẋ) T q s,s ′ = 0 for all s, s ′ vertices of U, and b(x,ẋ) = 0.
Proof: By Lemma 7, b(x,ẋ) is a CBF if and only if for every x,ẋ with b(x,ẋ) = 0, there exist y ≥ 0, z ∈ R m , and a vertex s such that (27) and (28) hold, or there exist z ∈ R m , y > 0, and vertices s, s ′ such that (29)-(31) hold. Equivalently, b is a CBF if and only if there do not exist x,ẋ with b(x,ẋ) = 0 such that conditions (27) and (28) fail to hold for all y ≥ 0, z ∈ R m , and s and the conditions (29)-(31) fail to hold for all y > 0, z ∈ R m , and vertices s, s ′ .
By Farkas's Lemma, the former condition is equivalent to A(s, x,ẋ) T w s + B T r s = 0 for all s, while the latter condition is equivalent to C T v s,s ′ + D(s, s ′ , x,ẋ) T q s,s ′ = 0 for all s, s ′ .
We finally give an SOS program for verifying a CBF for (25).
Theorem 11: The function b is a CBF for the system with dynamics (25) if and only if there exist polynomials η, θ s , λ s,s ′ , and φ ∈ Σ[w s , v s,s ′ , r s , q s,s ′ ] such that Proof: The proof follows from Lemma 8 and the Positivstellensatz.

V. PROBLEM FORMULATION: CBF SYNTHESIS
This section considers the following problem. Problem 2: Given a safety constraint C = {x : h(x) ≥ 0}, construct a CBF b : R n → R or family of CBFs b 1 , . . . , b M that guarantee safety with respect to C.
We present three approaches to synthesizing CBFs. The first approach uses an alternating descent method. The second approach exploits the existence of fixed points to construct CBFs for local neighborhoods. The third approach uses Newton's method in function space to guarantee local convergence to a CBF.

A. Alternating Descent Approach
Our first approach is based on the SOS constraints introduced in Section IV. When the function b(x) is unknown, the constraints become non-convex. We therefore propose an alternating-descent heuristic, in which we alternate between updating the CBF candidate b(x) and the polynomials used for verification. We describe our approach for synthesizing CBFs for polynomial dynamics, although a similar approach can be exploited for systems with Lagrangian dynamics or dynamics with trigonometric functions.
We initialize a function b 0 (x) arbitrarily (e.g., b 0 (x) = h i (x) for some i) and initialize parameters ρ 0 and ρ ′ 0 to be infinite. At step k, we solve the following SOS program with variables ρ, α k (x), η k (x), θ k 1 (x), . . . , θ k m (x), w(x), and β k (x): is an SOS polynomial chosen to ensure that the first constraint is SOS for sufficiently large ρ. We let ρ k denote the value of ρ returned by solving (34). The procedure terminates if ρ k ≤ 0 or if |ρ k − ρ ′ k−1 | < ǫ. Otherwise, we solve the SOS problem with variables ρ and b k given by minimize ρ k denote the value of ρ returned by the optimization. The procedure terminates if ρ ≤ 0 or if |ρ k − ρ ′ k | < ǫ. The following theorem establishes correctness of this approach.
Theorem 12: If the procedure described above terminates at stage k with ρ k ≤ 0, then b k−1 (x) is a CBF and {b k−1 (x) ≥ 0} is controlled positive invariant. If the procedure terminates at stage k with ρ ′ k ≤ 0, then b k (x) is a CBF and {b k (x) ≥ 0} is controlled positive invariant. The procedure converges in a finite number of iterations.
Proof: We will show that if ρ k ≤ 0, then b k−1 (x) is a CBF and {b k−1 (x) ≥ 0} is controlled positive invariant. If ρ k ≤ 0, then by construction of (34) there exist SOS polynomialsᾱ(x) andβ(x) such that Rearranging (36) and setting θ = −θ k i and η = −η k yields is SOS. Hence, by Theorem 4, there does not exist any x satisfying To prove convergence, we observe that , and β k−1 (x) comprise a feasible solution to (34) and ρ k , b k−1 (x) are feasible solutions to (35). Hence ρ 1 ≥ ρ ′ 1 ≥ · · · ≥ ρ k ≥ ρ ′ k ≥ · · · , i.e., the sequence is monotone nonincreasing. If the sequence is unbounded, then there exists K such that ρ k , ρ ′ k ≤ 0 for all k > K, and hence the algorithm terminates after K iterations. If the sequence is bounded below by zero, then it converges by the monotone convergence theorem and hence |ρ k − ρ ′ k | < ǫ and |ρ k − ρ ′ k−1 | < ǫ for k sufficiently large. We next consider synthesis of HOCBFs. We initialize functions b 0 (x), ψ 0 0 (x), . . . , ψ 0 r (x) arbitrarily. We initialize parameters ρ 0 and ρ ′ 0 to be infinite. We then solve an SOS problem with variables ρ, η k (x), θ The second constraint ensures containment within the safe region and is given by Hence the overall SOS program can be stated as We let ρ k denote the value of ρ returned by solving (40). The procedure terminates if ρ k ≤ 0 or if |ρ k − ρ ′ k−1 | < ǫ. Otherwise, the algorithm proceeds by solving the SOS problem with variables ρ, b k , and ψ k 0 , . . . , ψ k r and constraints and S⊆{0,...,r} The SOS program is stated as The procedure terminates if ρ ′ ≤ 0 or if |ρ k − ρ ′ k | < ǫ. Similar to Theorem 12, it can be shown that this approach terminates within finite time, and returns an HOCBF if ρ ≤ 0 or ρ ′ ≤ 0 at convergence.

B. CBF Computation at Fixed Points
We next describe how structures such as the existence of fixed points and periodic orbits in trajectories can be leveraged to construct CBFs. We first consider the case where the systeṁ x(t) = f (x) + g(x)u has a fixed point (x * , u * ), and have the following result.

This is equivalent to
The preceding lemma implies that we can construct a CBF by computing a fixed point (x * , u * ) and a stabilizing linear controller u = −Kx of the linearized system and solving the Lyapunov equation F T P + P F + N = 0 where F = (F − GK) and N is a positive definite matrix. It remains to choose the parameter ǫ, which can be performed via the following procedure. Theorem 13: Suppose that (x * , u * ) is a fixed point of (1), P is a solution to the Lyapunov equation for a stabilizing controller of the linearized sytsem at (x * , u * ), and the SOS constraints hold for some polynomials θ 1 , . . . , θ m , η(x) and SOS polynomials α(x) and β(x).
is a CBF and {b(x) ≥ 0} is in the safe region. Proof: If (44) holds, then b is a CBF by Theorem 4. By nonnegativity of SOS polynomials, we have that for SOS polynomials β and β 0 . Rearranging terms gives (45).

C. Newton's Method-Based Approach
In what follows, we describe a method for synthesizing a single CBF to satisfy a safety constraint B = {x : h(x) ≥ 0}. We assume that B is compact, and later discuss how relaxing this assumption to general B affects the results. Our approach is to compute polynomials b, η, θ 1 , . . . , θ m , w, α 01 , . . . , α 0N , β 01 , . . . , β 0N , α 11 , . . . , α 1N , β 11 , . . . , β 1N that solve the equations These equations correspond to the conditions (5) and (15) in the special case where there is no x with b(x) = 0, ∂b ∂x g(x) = 0, and ∂b ∂x f (x) ≤ 0. Our approach to solving the system is to use Newton's method over function space. Define the function F : X → Y , where X = (C 1 (B)) × (C 0 (B)) 4N +m+2 and Y = C 0 (B) × C 1 (B), and F = (F 1 F 2 ) T is given by In what follows, we let Here C 0 (B) denotes the set of continuous functions on B and C 1 (B) denotes the set of continuously differentiable functions on B.
The space X is equipped with the sup-norm while Y is equipped with the norm We recall that the Frechet derivative of a function F between Banach spaces X and Y is a bounded linear operator A : We have the following initial result. As a notation, we let 0 l denote the a vector of l 0's. Lemma 10: The Frechet derivative of F defined above is given by with where D j denotes the differentiation operator ∂b ∂xj , i.e., differentiation of the first element of ζ with respect to x j .
Proof: The fact that (49) is linear and satisfies (48) is clear. It remains to show that F ′ (ζ) is bounded, and it suffices to show that each entry of (49) is bounded. For the top-left entry, we have where the last inequality follows from the fact that The remaining entries consist of multiplying by functions that are bounded on B and hence are bounded linear operators. Within this framework, solving (46) and (47) is equivalent to solving an underdetermined system of nonlinear equations in function space. The Newton's method procedure for solving such systems is as follows [32]. First, define N )) T and select a parameter µ > 0. After initializing ζ 0 , ζ k is updated at each iteration as ζ k+1 = ζ k − φ k , where φ k is a solution to and F ′ (ζ k ) is the Frechet derivative of F at ζ k . The following preliminary result gives sufficient conditions for Newton's method to converge to a solution of an underdetermined nonlinear system. Theorem 14 ( [32],Theorem 3): Suppose that F : X → Y is defined and differentiable on a ball B = {||ζ 0 − ζ|| X ≤ r} and the following conditions hold: 2) There exists µ > 0 such that ||F ′ (ζ) * y|| ≥ µ||y|| for all ζ ∈ B and y ∈ Y * , where * denotes the dual. Define Then the update rule (50) converges to a solution ζ * of F (ζ) = 0, ||ζ * − ζ 0 || ≤ ρ, with the rate We will show that conditions 1) and 2) of Theorem 14 are satisfied, and hence our approach guarantees local convergence. We first give a sequence of preliminary results before stating and proving the main convergence result.
Proof: It suffices to show that each entry of F ′ (ζ) satisfies a Lipschitz condition for some L ≥ 0. This is equivalent to showing that there exists L such that, for any ζ 1 , ζ 2 , ζ ∈ X, we have Considering F ′ 11 first, we have by basic properties of the norm, where η 1 , η 2 , and the remaining polynomials denote the corresponding entries of ζ 1 and ζ 2 . Now, we have that ||ζ|| Y ≤ ||ζ|| X and ||D j ζ|| Y ≤ ||ζ|| X . Hence Implying that the Lipschitz property holds. The remaining entries are linear functions of the polynomials in ζ 1 and ζ 2 , and hence the local Lipschitz property holds for those entries as well.
The following known result states that the set of bounded and surjective linear operators is open.
Lemma 12 ( [33]): Let G : X → Y be a surjective and bounded linear operator between two Banach spaces X and Y . Then there exists ǫ > 0 such that any bounded linear operator We next give a sufficient condition for F ′ (ζ) to be surjective.
Next, we leverage this result to prove that F ′ (ζ) is surjective in a neighborhood of ζ * .
We are now ready to state the main convergence result. Theorem 15: There exist parameters r, L, and µ such that, if ||ζ 0 −ζ * || ≤ r, where ζ * is a polynomial solution to F (ζ) = 0, then the Newton update rule (50) converges to a fixed point ζ of F with rate given in Theorem 14.
Proof: The approach of the proof is to show that the conditions of Theorem 14 are satisfied. Conditions 1 follows from Lemma 11. By [33,Theorem 4.13], Condition 2 holds if F ′ (ζ) is surjective for all ζ in a neighborhood of ζ * . Hence Condition 2 holds by Lemma 14. Theorem 15 implies that the Newton's algorithm procedure converges at a quadratic rate to a fixed point b that satisfies (46) and (47), provided that the initial b 0 is sufficiently close to a solution. While there is no guarantee that b is a polynomial function, we note that any such solution can be used as a CBF. First, b is continuously differentiable. We have that, if h(x) = 0, then β 1 (x)b(x) + β 0 (x) + 1 = 0 for some SOS functions β 0 and β 1 , implying that b(x) < 0, implying that the controlled positive invariant set defined by b is contained in C. Furthermore, if b(x) = 0 and ∂b ∂x g(x) = 0 for all x, then −α 1 (x) ∂b ∂x f (x) + α 0 (x) + 1 = 0, implying that ∂b ∂x f (x) > 0. We next remark on the case where C is not compact. In order to ensure that the norm is well-defined, we can define X and Y over a different compact set, e.g., the ball in R n of radius 1. If the Newton's method procedure converges to a smooth function such as a polynomial, then (46) and (47) are guaranteed to hold over all of R n , implying that b is a CBF. However, there is no guarantee that the limit point of the procedure will satisfy this condition.

VI. SIMULATION STUDY
We simulated our proposed approach on a controlled van der Pol oscillator with dynamicṡ using Matlab. We utilized the SOStools library to solve the SOS programs [34]. We evaluated the barrier function candidate b = b 0 − x 2 1 − x 2 2 . For b 0 ≥ 1, the SOS-based approach verified the CBF using degree-four polynomials. For b 0 < 1, the SOS program was infeasible, since the set {b(x) ≥ 0} is not controlled positive invariant for b 0 < 1.

VII. CONCLUSIONS
This paper studied verification and synthesis of control barrier functions and controlled positive invariant sets. We showed that verifying that a semi-algebraic set is controlled positive invariant for a system with polynomial dynamics is equivalent to the non-existence of a solution to a system of polynomial equations and inequalities. We then proved that controlled positive invariance is equivalent to a sumof-squares optimization problem via the Positivstellensatz. We generalized this approach to systems with trigonometric dynamics, actuation constraints, and Lagrangian dynamics.
We proposed three algorithms for synthesizing control barrier functions. The first algorithm is an alternating descent heuristic based on solving a sequence of sum-of-squares programs. The second algorithm derives a local CBF in the neighborhood of a fixed point of the system. The third algorithm uses Newton's method on function space. We proved that the latter algorithm has guaranteed local quadratic convergence to a CBF.