Verification and Control for Finite-Time Safety of Stochastic Systems via Barrier Functions

TL;DR

This paper introduces a novel approach using stochastic barrier functions and sum-of-squares optimization to verify and control the finite-time safety probabilities of stochastic systems, including controller synthesis for affine-in-control dynamics.

Contribution

It proposes a new barrier certificate condition with a state-dependent bound and a method for synthesizing polynomial controllers to ensure safety probabilities.

Findings

Efficient numerical computation via sum-of-squares optimization.

Tighter probability bounds through state-dependent infinitesimal generator bounds.

Controller synthesis achieving specified safety probabilities.

Abstract

This paper studies the problem of enforcing safety of a stochastic dynamical system over a finite time horizon. We use stochastic barrier functions as a means to quantify the probability that a system exits a given safe region of the state space in finite time. A barrier certificate condition that bounds the infinitesimal generator of the system, and hence bounds the expected value of the barrier function over the time horizon, is recast as a sum-of-squares optimization problem for efficient numerical computation. Unlike prior works, the proposed certificate condition includes a state-dependent bound on the infinitesimal generator, allowing for tighter probability bounds. Moreover, for stochastic systems for which the drift dynamics are affine-in-control, we propose a method for synthesizing polynomial state feedback controllers that achieve a specified probability of safety. Two case studies are presented that benchmark and illustrate the performance of our method.

Tables

Table 1. TABLE 1: The results from the search for a control polynomial u(x) which reduces the probability of failure to P g ​ o ​ a ​ l = .10 subscript 𝑃 𝑔 𝑜 𝑎 𝑙 .10 P_{goal}=.10 . The probability of failure without a given control input is presented here for comparison.

Noise Level, $\sigma$	${𝐏}_{𝐮\left(𝐱\right)=\mathrm{𝟎}}$	$\alpha$	$\min 𝐜$
0.6	0.860	1.4	2.1821
0.9	0.919	1.3	0.5251
1.0	0.912	1.3	0.6396
1.3	0.949	1.5	1.1488

Equations

$$dx=F(x)dt+\sigma (x)dw.$$

$$\mathcal{A}B(x)=\underset{t\downarrow 0}{\lim }\frac{\mathbb{E}[B(x)|x_0]-B(x_0)}{t}$$

$$\mathcal{A}B(x)=\sum_{i=1}^{n}F_{i}(x)\frac{\partial B}{\partial x_{i}}+\frac{1}{2}\sum_{i=1}^{n}\sum_{j=1}^{n}\bigg{(}\sigma(x)\sigma^{T}(x)\bigg{)}_{i,j}\frac{\partial^{2}B}{\partial x_{i}\partial x_{j}}.$$

$$\tilde{x}(t)=\{\begin{array}{ll}x(t)& \text{for}t\le \tau \\ x(\tau )& \text{for}t\ge \tau .\end{array}$$

$$B(x)\le \gamma \forall x\in {\mathcal{X}}_0$$

$$B(x)\ge 1\forall x\in {\mathcal{X}}_u$$

$$B(x)\ge 0\forall x\in \mathcal{X}$$

$$\frac{\partial B}{\partial x}f(x)+\frac{1}{2}\text{Trace}\bigg{(}\sigma^{T}(x)\frac{\partial^{2}B}{\partial x^{2}}\sigma(x)\bigg{)}\leq 0\ \ \forall x\in\mathcal{X}.$$

$$P\{\tilde{x}(t)\in {\mathcal{X}}_u\text{ for some }t\ge 0\}\le B(x_0)\le \gamma$$

$$\Sigma[x]\triangleq\bigg{\{}s(x)\in\mathbb{R}[x]:s(x)=\sum_{i=1}^{m}g_{i}(x)^{2},g_{i}(x)\in\mathbb{R}[x]\bigg{\}}$$

$$p_0(x)+\sum _{i=1}^m{p}_i(x)q_i(x)\in \Sigma [x]$$

$$dx=(f(x)+g(x)u(x))dt+\sigma (x)dw$$

$$B(x)\le \gamma \forall x\in {\mathcal{X}}_0$$

$$B(x)\ge 1\forall x\in {\mathcal{X}}_u$$

$$B(x)\ge 0\forall x\in \mathcal{X}$$

$$\small\small\frac{\partial B}{\partial x}F(x)+\frac{1}{2}\text{Trace}\bigg{(}\sigma^{T}(x)\frac{\partial^{2}B}{\partial x^{2}}\sigma(x)\bigg{)}\leq-\alpha B(x)+\beta\ \ \ \forall x\in\mathcal{X}\setminus\mathcal{X}_{u}$$

$${\rho }_u$$

$$\rho_{u}\leq P\left\{\sup_{0\leq t\leq T}B(\tilde{x})\geq 1\right\}\leq 1-\bigg{(}1-B(x_{0})\bigg{)}e^{-\beta T}.$$

$${\rho }_u\le P\left\{\underset{0\le t\le T}{\sup }B(\tilde{x})\ge 1\right\}\le \frac{B(x_0)+(e^{\beta T}-1)\frac{\beta }{\alpha }}{e^{\beta T}}.$$

$${\rho }_u\le P\left\{\underset{0\le t\le T}{\sup }B(\tilde{x})\ge 1\right\}\le B(x_0)+\beta T.$$

$$B(x)-{\lambda }_{\mathcal{X}}(x)s_{\mathcal{X}}(x)\in \Sigma [x]$$

$$B(x)-{\lambda }_{{\mathcal{X}}_u}(x)s_{{\mathcal{X}}_u}(x)-1\in \Sigma [x]$$

$$-B(x)-{\lambda }_{{\mathcal{X}}_o}(x)s_{{\mathcal{X}}_o}(x)+\gamma \in \Sigma [x]$$

$$-\frac{\partial B(x)}{\partial x}F(x)-\alpha B(x)+\beta +{\lambda }_{{\mathcal{X}}_u}(x)s_{{\mathcal{X}}_u}(x)$$

$$-{\lambda }_{\mathcal{X}}(x)s_{\mathcal{X}}(x)\in \Sigma [x]$$

$$u(x)=z^{T}Qz$$

$$c\text{mathds}1-\mathrm{vec}(Q)\ge 0$$

$$\mathrm{vec}(Q)+c\text{mathds}1\ge 0$$

$$dx=\big{(}-x+u(x)\big{)}dt+\sigma dw.$$

$$d{x}_1$$

$$d{x}_2$$

Full text

I Introduction

Reliance on complex, safety-critical systems is increasing, which has made safety verification of such systems of utmost importance. For example, environments populated by both humans and autonomous systems (e.g. fulfillment centers, autonomous vehicles, and healthcare) require rigorous safety verification to ensure desired behavior is achieved. From a practical standpoint, safety verification can translate directly to ensuring qualitative guidelines such as collision avoidance are maintained. Safety-critical systems are often analyzed in a purely deterministic framework, however, many real-world applications are subject to stochastic disturbances and are better modeled as stochastic systems.

A common approach to safety verification in deterministic systems is via barrier functions which provide Lyapunov-like guarantees regarding system behavior. The existence of a barrier function which satisfies a barrier certificate can often be enough to certify the safe operation of a system [1]. Recent work has modified and improved the deterministic form of barrier functions and expanded their application. In particular, control barrier functions have been introduced to guaranteed safety in control affine systems [2, 3]. This is demonstrated in applications for cruise control [3, 4], collision avoidance in robotic swarms [5], and walking robots [6], and has recently been extended to allow for input-to-state safe control barrier functions [7] and to guarantee finite-time convergence to a safe region [8].

In the stochastic setting, safety verification via barrier certificates for infinite time horizons was introduced in [1] alongside the deterministic counterpart. The work presented in [1] provides a framework for bounding the probability a system will exit a safe region based on a non-negative barrier function defined on the system state space. In this approach, the probability is directly correlated with the set of initial conditions. However, this approach can be overly restrictive because it requires the infinitesimal generator, which dictates the expected value evolution of a stochastic process, to be non-positive; i.e., the barrier function is restricted to be a supermartingale.

The paper [9] relaxes this condition and instead provides a barrier certificate that only requires the infinitesimal generator of the barrier process to be upper-bounded by a constant. Such processes are called c-martingales and allow the expected value of the barrier function to increase over time. This approach results in a safety probability bound for finite time horizons. Recent work in [10] leverages c-martingales for temporal logic verification of discrete-time systems.

The present paper also studies the problem of verifying safety of stochastic systems on finite time horizons, and the contributions are as follows. First, we build on the approaches proposed in [1, 9] and propose a barrier certificate constraint that imposes a state-dependent bound on the infinitesimal generator. This bound was originally proposed and studied by Kushner in [11, 12]. The proposed barrier certificate allows the expected value of the barrier to increase and covers the c-martingale condition of [9] as a special case. However, our formulation also accounts for the system dynamics in the infinitesimal generator constraint. This allows for probability bounds that are no worse than the c-martingale condition, and in many cases, especially with high noise levels, provides better probability bounds.

Second, as in [1, 9], we compute barrier functions using sum-of-squares (SOS) optimization. Like in [1], but unlike [9], we utilize polynomial barrier functions. This provides a simpler formulation of the probability of failure on a finite time horizon when compared to the approach in [9] which uses exponential barrier functions and, empirically, provides tighter probability bounds.

Third, we extend our formulation to allow for control inputs and provide a method for synthesizing a safe controller. In particular, we consider affine-in-control systems and the proposed approach searches for a polynomial state feedback controller which ensures a system’s failure probability achieves a predetermined criterion via a stochastic control barrier function.

This paper is organized as follows: Section II covers the background information of stochastic differential equations, barrier functions and SOS optimization. Section III covers the problem which we are solving in detail. Section IV highlights the methodology we utilize to solve the SOS optimization and stochastic control problem. Section V and Section VI present numerical case studies which illustrate our results and conclusions, respectively.

II Preliminaries

In this section we first introduce our state space definitions as well as background information regarding stochastic processes, barrier functions, and SOS polynomials.

II-A Stochastic Process

Consider a complete probability space ($\Omega,\mathcal{F},P$) and a standard Wiener process, $w(t)$ in $\mathbb{R}^{m}$. We consider stochastic processes $x(t)$ satisfying a stochastic differential equation of the form

[TABLE]

The compact set $\mathcal{X}\subset\mathbb{R}^{n}$ is the system state space, $F:\mathcal{X}\rightarrow\mathbb{R}^{n}$ is the drift rate and $\sigma:\mathcal{X}\rightarrow\mathbb{R}^{n\times m}$ is the diffusion term. We assume the functions $F(x)$ and $\sigma(x)$ are Lipschitz continuous. The stochastic process $x$ is a right continuous strong Markov process [13]. We now introduce the infinitesimal generator, which extends the usual definition of a time derivative to instead consider the expectation of a function of a random process.

Definition 1**.**

Let $x$ be a stochastic process in $\mathbb{R}^{n}$. The infinitesimal generator $\mathcal{A}$ of $x$ acts on functions of the state space and is defined as

[TABLE]

where $B:\mathcal{X}\rightarrow\mathbb{R}$ such that the limit exists for all $x_{0}$.

In particular, the infinitesimal generator for any process as in (1) is of the form shown in Fact 1.

Fact 1** (Ch. 7, Theorem 7.3.3 of [13]).**

Let $x$ be a stochastic process satisfying (1), then the infinitesimal generator $\mathcal{A}$ of some twice differentiable function $B(x)$ is given by

[TABLE]

The stochastic process $x$ is not guaranteed to lie in $\mathcal{X}$ at all times which leads us to define the stopped process $\tilde{x}$.

Definition 2**.**

Suppose that $\tau$ is the first time of exit of $x$ from the open set Int($\mathcal{X}$). Then the stopped process $\tilde{x}$ is defined by [1]

[TABLE]

It is worth noting that the stopped process inherits the same strong Markovian property of $x$ and shares the same infinitesimal generator [11].

II-B Barrier Functions

Consider an unsafe region of the state space $\mathcal{X}_{u}\subseteq\mathcal{X}$ and a set of initial conditions $\mathcal{X}_{0}\subseteq\mathcal{X}\setminus\mathcal{X}_{u}$. In a similar spirit to Lyapunov functions, barrier functions are utilized as a means of guaranteeing a desired behavior on some region of a system’s domain defined as a sub-level set (or super-level set) of the barriers. In that regard, stochastic barrier functions have been introduced to upper bound the probability of exiting a safe region over an infinite time-horizon.

Proposition 1** (Theorem 15 from [1]).**

Given a stochastic differential equation of the form of (1) and the sets $\mathcal{X}$, $\mathcal{X}_{0}$, and $\mathcal{X}_{u}$ with $f(x)$ and $\sigma(x)$ locally Lipschitz continuous, consider the stopped process $\tilde{x}$. Suppose there exists a twice differentiable function $B$ such that

[TABLE]

[TABLE]

[TABLE]

[TABLE]

Then, the probability of the system entering the unsafe region of the state space is bounded by

[TABLE]

where $x_{0}\in\mathcal{X}_{0}$ is the initial state of the system.

This theorem provides a powerful means of bounding the probability of failure of a stochastic process on an infinite time horizon. However, we note that the inequality condition (5), also referred to as the barrier certificate, imposes that $B(x)$ is a supermartingale. This inequality enforces that the expectation of the barrier function decreases at all points of $\mathcal{X}$. In practice, this is often overly restrictive on the system dynamics. For example, it has been shown that no supermartingale exists on a bounded set where the system’s noise does not vanish [11]. In Section III, we present a relaxed version of this theorem with its respective probability bounds for finite-time horizons.

II-C Sum-of-Squares

Definition 3**.**

Define $\mathbb{R}[x]$ as the set of all polynomials in $x\in\mathbb{R}^{n}$. Then

[TABLE]

is the set of SOS polynomials. It is noted that if $s(x)\in\Sigma[x]$ then $s(x)\geq 0$ $\forall$ $x$.

Definition 4**.**

Given $p_{i}(x)\in\mathbb{R}[x]$ for $i=0,\ldots,m$, the problem of finding $q_{i}(x)\in\Sigma[x]$ for $i=1,\ldots,\hat{m}$ and $q_{i}(x)\in\mathbb{R}[x]$ for $i=\hat{m}+1,\ldots,m$ such that

[TABLE]

is a sum-of-squares program (SOSP). SOSPs can be efficiently converted to semidefinite programs using tools such as SOSTOOLS [14].

III Problem Formulation

The problem we address is: how do we create a bound on the probability a stochastic system of form (1) exits a safe region during a finite-time horizon?

Objectives: First, our goal in this paper is to relax the supermartingale condition on the barrier certificate in (5) similar to what is shown in [9]. Second, based on that relaxation, we aim to derive a state-feedback controller ensuring a user-specified upper bound on the probability of exiting a safe region in the state space.

Consider the stochastic process $x$ which satisfies the stochastic differential equation

[TABLE]

where $f:\mathcal{X}\rightarrow\mathbb{R}^{n}$, $g:\mathcal{X}\rightarrow\mathbb{R}^{n\times k}$, $\sigma:\mathcal{X}\rightarrow\mathbb{R}^{n\times m}$ and $w$ is a $m$-dimensional Wiener process. Additionally, $u:\mathcal{X}\rightarrow\mathbb{R}^{k}$ where $u$ is a state dependent control input. We define $F(x)=f(x)+g(x)u(x)$.

Now, we relax the supermartingale condition shown in (5). The following theorem is an immediate corollary of Chapter 3, Theorem 1 in [11].

Theorem 1**.**

Given the stochastic differential equation shown in (7) and the sets $\mathcal{X}\subset\mathbb{R}^{n}$, $\mathcal{X}_{u}\subseteq\mathcal{X},\mathcal{X}_{0}\subseteq\mathcal{X}\setminus\mathcal{X}_{u}$ with $F(x)=f(x)+g(x)u(x)$ and $\sigma(x)$ locally Lipschitz continuous, where $u(x)$ is some feedback control strategy. Consider the stopped process $\tilde{x}$. Suppose there exists a twice differentiable function $B$ such that

[TABLE]

[TABLE]

[TABLE]

[TABLE]

for some $\alpha\geq 0$, $\beta\geq 0$ and $\gamma\in[0,1)$. Define

[TABLE]

Then

• •

If $\alpha>0$ and $\frac{\beta}{\alpha}\leq 1$,

[TABLE]

• •

If $\alpha>0$ and $\frac{\beta}{\alpha}\geq 1$,

[TABLE]

• •

If $\alpha=0$,

[TABLE]

The bound shown in (15) is characterized in [10] and [9] as the upper bound on the probability of being unsafe for a c-martingale.

If $B(x)$ satisfies the conditions of Theorem 1, then $B(x)$ is called a stochastic control barrier function for a given control policy $u(x)$. Relaxing the supermartingale condition on the infinitesimal generator in the fashion of Theorem 1 gives three case-dependent finite time probability bounds on a system’s likelihood of entering an unsafe region in the form of (13), (14), and (15).

Remark 1**.**

If the initial state $x_{0}$ is not known exactly but only known to lie within $\mathcal{X}_{0}$, then $\gamma$ can be substituted for $B(x_{0})$ in the probability bounds in Theorem 1. This provides an upper bound on the probability of failure over the entire set of initial conditions rather than on a particular initial point in $\mathcal{X}_{0}$.

IV Methodology

In this section we present our approach to construct the stochastic control barrier functions based on the problem formulation of Section II. First, we adapt the constraints given in Theorem 1 to be formulated as an SOSP. Second, we cover the algorithms which construct barrier functions and present our method for computing a low-energy control policy $u(x)$.

IV-A SOS Formulation for Safety Verification

Theorem 2**.**

Consider a system of the form of (7) and the sets $\mathcal{X}$, $\mathcal{X}_{0}$, and $\mathcal{X}_{u}$ and assume these sets can be described as $\mathcal{X}=\{x\in\mathbb{R}^{n}:s_{\mathcal{X}}(x)\geq 0\}$, $\mathcal{X}_{0}=\{x\in\mathbb{R}^{n}:s_{\mathcal{X}_{o}}(x)\geq 0\}$, and $\mathcal{X}_{u}=\{x\in\mathbb{R}^{n}:s_{\mathcal{X}_{u}}(x)\geq 0\}$ for some polynomials $s_{\mathcal{X}}$, $s_{\mathcal{X}_{o}}$, and $s_{\mathcal{X}_{u}}$. Suppose there exists a polynomial $B(x)$, a polynomial $u(x)$, and SOS polynomials $\lambda_{\mathcal{X}}(x)$, $\lambda_{\mathcal{X}_{o}}(x)$, and $\lambda_{\mathcal{X}_{u}}(x)$ that satisfy the following

[TABLE]

[TABLE]

[TABLE]

[TABLE]

where $F(x)=f(x)+g(x)u(x)$. Then, the probability of failure, depending on the values of $\alpha$ and $\beta$, is defined by (13), (14) or (15).

We omit the proof due to space constraints, but the proof follows the general approach for relaxing set constraints to SOS programs using the Positivstellensatz condition; see the documentation of [14] for details.

IV-B Barrier Function Numerical Procedure

Next, we present an algorithmic solution to this problem. Algorithm 1 computes the barrier function $B(x)$ used to quantify an upper bound on the failure probability. The input values $l_{\alpha},u_{\alpha},\sigma,u(x),n_{B}$ are the lower $\alpha$ range value, upper $\alpha$ range value, diffusion term, control polynomial, and the order of the $B(x)$ polynomial, respectively. Our algorithm performs a grid search over a range of scalar $\alpha$ with value spacing $d$,which are design parameters. Next, the SOSP is encoded using the constraints shown in Theorem 2. Lastly, as the SOSP is run, the algorithm returns a function, $B(x)$, that is evaluated at any $x_{0}\in\mathcal{X}_{0}$ and utilized to compute the probability, $P$, using (13), (14) or (15). The degree of $B(x)$ is a design parameter; however, higher order polynomials tend to produce tighter bounds. Well refined bounds (i.e. higher order polynomials) present themselves with the trade-off of longer computational times versus probability of failure refinement.

The objective of the SOSP in Algorithm 1 is set to minimize the value, $B(x_{0})+\beta$. Minimizing $B(x_{0})+\beta$ is a consensus objective which may not be the best one but provides a means of avoiding bi-linear programs.

IV-C Controller Synthesis Procedure

In general, when searching for a control policy, we are aiming for a polynomial of the same or lower order of $B(x)$ such that the upper bound on the probability of failure reduces to a designer specified value. First, we write the polynomial $u(x)$ in quadratic form as

[TABLE]

where $z$ is a vector of monomials in $x$ of a specified order and $Q$ is a coefficient matrix of appropriate dimensions. Because there likely exist many feasible controllers ensuring the desired probability of failure, we introduce a cost criterion to choose among them. We approximate the energy of a particular control policy via a proxy measure. In this case, the proxy is the non-negative scalar, $c$, such that the following vector element-wise constraints

[TABLE]

[TABLE]

hold where $\operatorname{vec}(Q)$ is the vector form of matrix $Q$ and $\mathds{1}$ is the vector of ones of appropriate dimension. We choose the cost $\min c$ to minimize the coefficients appearing in the polynomial controller to encourage lower control effort. This objective and procedure are highlighted in Algorithm 2.

Algorithm 3 takes $P_{goal},\sigma,\alpha,n_{B},n_{u}$ and $\epsilon$ as arguments. These variables are the goal probability, diffusion term, $\alpha$ multiplier on $B(x)$, barrier polynomial order, control polynomial order and a small offset, respectively. Once the procedure begins, it runs until the probability of failure is within $\epsilon$ of the predefined goal probability. It is possible to use other conditions to determine whether the algorithm should continue to run such as computing the change in optimal scalar $c$ value, $c^{*}$, between iterations. Additionally, the algorithm may be sped up by using a floor value for $c$. Initially, a polynomial barrier of a specified polynomial power is computed given no control policy (i.e. $u(x)=0$). Generally speaking, as in our case studies, we are interested in systems where the probability of failure with no control action is above the goal probability.

Next, if the probability of failure is greater than $P_{goal}$ then we compute a scaled down $\beta$ value multiplied by $a_{dec}$. If the failure probability is less than $P_{goal}$ then we scale up the $\beta$ by $a_{inc}$. The intuition behind this comes from analyzing the probability bounds (13), (14) or (15). In general, a lower $\beta$ reduces our failure probability, thus when searching for $u(x)$ a scaled version of $\beta$ can be used. The values of $a_{inc}$ and $a_{dec}$ are also design parameters.

V Case Studies

In this section, we first present a simple academic example to illustrate the our technique. Second, we present a nonlinear example to demonstrate the versatility of our approach. Both case studies are compared to a Monte Carlo simulation which is considered ground truth. We utilize SOSTOOLS [14] which converts our SOSP into semidefinite programs. Our choice of solver is the semidefinite program solver SDPT3 [15, 16]. These case studies were conducted on a 2.3 GHz Intel Core i5 computer with 8GB of memory.111The Matlab source code for the two case studies is contained at https://github.com/gtfactslab/stochasticbarrierfunctions

V-A 1-D Stochastic System

Consider a 1-D stochastic control affine system of the form

[TABLE]

This is of the same form as (7) where $f(x)=-x$ and $g(x)=1$. We define our state space as $\mathcal{X}=\{x:-2\leq x\leq 2\}$, $\mathcal{X}_{u}=\{x:x^{2}\geq 1\}$, and $\mathcal{X}_{0}=\{x:x^{2}\leq.2^{2}\}$. First, we benchmark the probability of failure without a control input (i.e. $u(x)=0$) for a finite time horizon of $T=1\ \text{s}$. Thus, to do so, we follow the procedure outlined in Algorithm 1. We grid search over a defined range of values for the constant $\alpha$. In this particular example, our $\alpha\in[0,5]$ with $d=.05$ in Algorithm 1.

We choose to search for $B(x)$ of the 16th degree. Additionally, we reproduce the c-martingale bound presented in [9, Algorithm 3]. Lastly, we benchmark against the true probability of failure created via a 5000 draw Monte Carlo simulation. The results are presented in Fig. The 1.

In Fig. 1, we see that our polynomial bound on the probability of failure performs better than the bound from [9] generated using the c-martingale condition that is not state dependent. The difference is particularly notable at higher noise levels where the exponential bound from [9] becomes trivial, i.e., greater than or equal to one.

Next, we address the control problem of achieving a particular bound on the probability of failure of this system. We choose a desired failure probability $P_{goal}=.30$. We restrict our attention to a linear controller of the form $u(x)=-kx$. Our search for a low-energy controller which successfully fulfills the design requirement follows a modified binary search version of Algorithm 3.

Fig. 2 plots $k^{*}$ achieving the desired failure probability bound for $\sigma\in[1,2]$. Here, we note that the degree of barrier function for which we search greatly affects the control gain needed to achieve the control objective. In some sense, searching for a higher-order polynomial refines the probability of failure bound requiring lower control effort; however, these high order polynomials require more computation time. Eventually, the degree of the polynomial reaches a saturation point where it does not further decrease the $k^{*}$ required.

V-B Nonlinear Dynamics

Consider the stochastic non-linear dynamics

[TABLE]

This system is studied in [17] without the input term $u(x)$.

We define our state space as $\mathcal{X}=\{(x_{1},x_{2})\ |-3\leq x_{1}\leq 2,-2\leq x_{2}\leq 3\}$, $\mathcal{X}_{u}=\{x_{2}\ |\ x_{2}\geq 2.25\}$, and $\mathcal{X}_{0}=\{(x_{1},x_{2})|(x_{1}+2)^{2}+x_{2}^{2}\leq 0.1^{2}\}$. A sample trajectory of (18)–(19) is illustrated in Fig. 3. Additionally, level sets of $B(x)$ are projected onto the state space. In this illustration, $B(x)$ is computed with $u(x)=0$ solely using Algorithm 1. Here, we see that the values for the barrier function abide by the definitions of Theorem 1. In this particular trajectory illustration, the evolution of system noise is enough for the system to enter the predefined unsafe set; however, this is not always the case. To illustrate this, we compute a Monte Carlo simulation of the system dynamics shown. Additionally, an upper bound is computed on the probability of becoming unsafe given our initial condition and illustrated in Fig. 4. While we encode a set of initial conditions into the SOSP, we evaluate the probability bound at the same initial point, $x_{0}\in\mathcal{X}_{0}$, as the Monte Carlo simulation.

The design specification for this example is to reduce the probability of failure bound to $P_{goal}=.10$ for specified noise levels. For this example we create a 2nd order polynomial controller of the form of (16). We look to minimize the constant, $c$, highlighted in Algorithm 2. We run the $u(x)$ search algorithm for select noise levels, specified $\alpha$ values, and present the results in Table 1. The $\alpha$ values in this table originate from the initial (i.e. $u(x)=0$) probability bound computation.

VI Conclusion

We consider control barrier functions whose existence gives a means of quantifying an upper bound on a system’s probability of failure. Additionally, we present a novel, state dependent approach to the problem of finite-time verification which further relaxes the constraint on the evolution of the expected value. Lastly, we synthesize a feedback control strategy $u(x)$ such that a certain probability of failure criteria is met. We illustrate our methods with two case studies which demonstrate our ability to quantify system failure probabilities. In these case studies, we solve for the barrier function polynomials using SOS optimization and demonstrate our proposed approach outperforms existing methods.