Converse Theorems for Safety and Barrier Certificates

TL;DR

This paper establishes that every robustly safe dynamical system possesses a barrier certificate, providing a constructive method based on finite-time reachable states to prove safety.

Contribution

It proves the existence of barrier certificates for all robustly safe ODEs and offers a constructive approach based on finite-time reachability.

Findings

Every robustly safe ODE has a barrier certificate.

Constructive method for barrier certificates based on finite-time reachability.

Bridges safety verification with reachability analysis.

Abstract

An important tool for proving safety of dynamical systems is the notion of a barrier certificate. In this paper we prove that every robustly safe ordinary differential equation has a barrier certificate. Moreover, we show a construction of such a barrier certificate based on a set of states that is reachable in finite time.

Equations

$$\nu (y^{\prime })$$

$$\nu (x^{\prime })-\nu (x)+sgn(\nu (x)-\nu (x^{\prime }))\epsilon$$

$$-(\nu (x)-\nu (x^{\prime }))+\epsilon$$

$$\nu (y^{\prime })$$

$$\nu (x^{\prime })-\nu (x)+sgn(\nu (x)-\nu (x^{\prime }))\epsilon$$

$$-(\nu (x)-\nu (x^{\prime }))-\epsilon$$

$$({\mathcal{L}}_f\nu )(x):=\underset{h\to 0}{\lim }\frac{\nu ({\phi }_f(x,h))-\nu (x)}{h}$$

$$|h(x)-h^{\prime }(x)|<\epsilon$$

$$({\mathcal{L}}_f{h}^{\prime })(x)>({\mathcal{L}}_{f}h)(x)-\epsilon .$$

$$({\mathcal{L}}_f\nu )(x)$$

$$\underset{h\to 0}{\lim }\frac{\nu ({\phi }_f(x,h))-\nu (x)}{h}$$

$$\underset{h\to 0}{\lim }\frac{\nu (x)+h-\nu (x)}{h}$$

$$|\nu (x)-{\nu }^{\prime }(x)|<\frac{\delta }{2}$$

$$({\mathcal{L}}_f{\nu }^{\prime })(x)>({\mathcal{L}}_f\nu )(x)-\frac{\delta }{2},$$

$$\beta_{\alpha}(x):=\left\{\begin{array}[]{ll}{\delta},&\mbox{if }X_{\alpha}\cap\{x\mid\nu(x)\geq\delta\}\neq\emptyset,\\[0.86108pt] {-\delta},&\mbox{if }X_{\alpha}\cap\{x\mid\nu(x)\leq-\delta\}\neq\emptyset,\\[0.86108pt] {\nu^{\prime}(x)},&\mbox{otherwise}.\\[0.86108pt] \end{array}\right.$$

$$\beta (x):=\sum _{\alpha \in A}{\psi }_{\alpha }(x){\beta }_{\alpha }(x).$$

$$R_{f,\epsilon }^{\Delta }(V)\subseteq V.$$

$$R_{f,\epsilon }(R_{f,\epsilon }^{[0,{\Delta }^{\prime }]}(V))\subseteq R_{f,\epsilon }^{[0,{\Delta }^{\prime }]}(V).$$

Full text

1 Introduction

An important property of a control system is safety, that is, the property that the system, when starting from a certain set of initial states, always stays in a set of safe states. The notion of a barrier certificate [10, 15] proves safety by separating the set of initial states from the set of states that are not safe using a transversality condition. This immediately opens the question whether every safe system has a barrier certificate. In this paper we give an affirmative answer for robustly safe ordinary differential equations. The construction is based on an inductive certificate for safety. Every safe system has such a certificate, but it is formed by a set of states reachable in unbounded time. As a second result of this paper, we show that a certain set of states reachable in finite time always forms such an inductive certificate for safety, as well.

Converse theorems for barrier certificates have received attention since their introduction. Prajna and Rantzer [11, 12] proved a converse theorem that holds under some Slater-like condition. Wisniewski and Sloth introduced the idea of exploiting robustness for such a converse theorem [17]. Their result does not need the Slater-like condition, but is restricted to Morse-Smale vector fields.

The result in this paper is based on robustness arguments, too. However, it neither needs a Slater-like condition, nor is restricted to Morse-Smale vector fields. Moreover, unlike the earlier results, which are based on measure theory and Morse-Smale theory, respectively, the proofs in this paper are based on basic mathematical tools, only.

2 Problem Definition

Definition 1**.**

A safety verification problem is a triple $(f,I,U)$ where

• •

$f:\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$, and $f$ is smooth,

• •

$I\subseteq\mathbb{R}^{n}$* (the set of initial states), and*

• •

$U\subseteq\mathbb{R}^{n}$* (the set of unsafe states).*

The vector field $f$ defines an ordinary differential equation whose solution we will describe using the flow of $f$:

Definition 2**.**

For a smooth $f:\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$, and $t\in\mathbb{R}$, we denote the state that system $\dot{x}=f(x)$ reaches after time $t$ from $x$ by $\varphi_{f}(x,t)$.

Note that we also allow $t$ to be negative, and we have $\varphi(x,t)=y$ iff $\varphi(y,-t)=x$.

Based on the flow $\varphi$ we introduce the following notation for sets of reachable states:

Definition 3**.**

For a smooth $f:\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$, for sets $X\subseteq\mathbb{R}^{n}$ and $T\subseteq\mathbb{R}$, $R_{f}^{T}(X):=\{\varphi_{f}(x,t)\mid t\in T,x\in X\}$. For $t\in\mathbb{R}$, $R_{f}^{t}(X):=R_{f}^{\{t\}}(X)$, and $R_{f}(X):=R_{f}^{\mathbb{R}^{\geq 0}}(X)$.

Here, if clear from the context, we will drop the subscript $f$.

Definition 4**.**

A safety verification problem $(f,I,U)$ is safe iff $R_{f}(I)\cap U=\emptyset$.

In this paper, we are interested in objects that can serve as evidence that a given safety verification problem is safe. One possibility of such objects is the following:

Definition 5**.**

A set $V\subseteq\mathbb{R}^{n}$ is a safety certificate of a safety verification problem $(f,I,U)$ iff

• •

$I\subseteq V$**

• •

$R_{f}(V)\subseteq V$**

• •

$V\cap U=\emptyset$**

A set that fulfills the first two conditions is also called inductive invariant by the verification community, and a positively invariant set by the dynamical systems literature [7, 5].

Safety certificates serve as a proof of safety:

Property 1**.**

If a safety verification problem $(f,I,U)$ has a safety certificate, then it is safe.

Safety certificates are also complete, that is, there is a converse of Property 1:

Property 2**.**

If a safety verification problem $(f,I,U)$ is safe, then it has a safety certificate, $R_{f}^{\mathbb{R}^{\geq}0}(I)$.

The definitions presented above are not robust against small changes of the safety verification problem. For example, a safety verification problem might have a safety certificate, but tiny changes of the safety verification problem might result in it not being safe. In order to avoid this, we use robust analogies of the definitions above. Here we measure deviation from nominal behavior by the Euclidean norm, denoted by $||\cdot||$.

Definition 6**.**

A function $x:\mathbb{R}^{\geq 0}\rightarrow\mathbb{R}^{n}$ is an $\varepsilon$-solution of an ordinary differential equations $\dot{x}=f(x)$ iff for all $t\geq 0$, $||f(x(t))-\dot{x}(t)||\leq\varepsilon$.

We use the following robust versions of the reach sets introduced in Definition 3:

Definition 7**.**

For a smooth $f:\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$, for sets $X\subseteq\mathbb{R}^{n}$ and $T\subseteq\mathbb{R}$, $R_{f,\varepsilon}^{T}(X):=\{x(t)\mid t\in T,x\text{ is an }\varepsilon\text{-solution of }f\text{ with }x(0)\in X\}$. For $t\in\mathbb{R}$, $R_{f,\varepsilon}^{t}(X):=R_{f,\varepsilon}^{\{t\}}(X)$, and $R_{f,\varepsilon}(X)=R_{f,\varepsilon}^{\mathbb{R}^{\geq 0}}$.

Again, if clear from the context, we will drop the subscript $f$.

Also Definition 4 has a robust version:

Definition 8**.**

A safety verification problem $(f,I,U)$ is robustly safe iff there is an $\varepsilon>0$ such that $R_{f,\varepsilon}(I)\cap U=\emptyset$. We will call an $\varepsilon>0$ fulfilling this property a robustness margin of $(f,I,U)$.

We also provide a robust version of Definition 5:

Definition 9**.**

A set $V\subseteq\mathbb{R}^{n}$ is an $\varepsilon$-robust safety certificate of a safety verification problem $(f,I,U)$ iff

• •

$I\subseteq V$**

• •

$R_{f,\varepsilon}(V)\subseteq V$**

• •

$V\cap U=\emptyset$**

We call a safety certificate $V$ robust iff there is an $\varepsilon>0$ such that $V$ is a $\varepsilon$-robust safety certificate.

There is a robust version of Property 1:

Property 3**.**

If a safety verification problem $(f,I,U)$ has a robust safety certificate, then it is robustly safe.

Also completeness holds in analogy to Property 2, that is, there is a converse of Property 3:

Property 4**.**

If a safety verification problem $(f,I,U)$ is robustly safe, then it has a robust safety certificate, $R^{\mathbb{R}^{\geq 0}}_{f,\varepsilon}(I)$, where $\varepsilon$ is a robustness margin of $(f,I,U)$.

Safety certificates have the disadvantage that checking them still needs the computation of a reachable set. This can be avoided by the following definition.

Definition 10** (Prajna and Jadbabaie [10]).**

A differentiable function $\beta:\mathbb{R}^{n}\rightarrow\mathbb{R}$ is a barrier certificate of a safety verification problem $(f,I,U)$ iff

• •

$\forall x\;.\;x\in I\Rightarrow\beta(x)\geq 0$**

• •

$\forall x\;.\;\beta(x)=0\Rightarrow L_{f}(\beta)(x)>0$, that is $(\nabla\beta(x))^{T}f(x)>0$

• •

$\forall x\;.\;\beta(x)\geq 0\Rightarrow x\not\in U$**

Also barrier certificates serve as a proof of safety:

Property 5**.**

If a safety verification problem $(f,I,U)$ has a barrier certificate, then it is safe.

Converse theorems for this property are an active area of research [11, 12, 17], and at the same time the main topic of this paper.

Summarizing, Definitions 5, 9, and 10 provide three different forms of certificates for safety verification problems, as ensured by corresponding Properties 1, 3, and 5, respectively. The contributions of this paper are converse theorems for the latter two cases. The state of the art is:

• •

For Definition 9, there is a very simple converse theorem of the corresponding Property 3. This converse theorem is Property 4 which has the disadvantage of being based on an infinite-time reach set.

• •

For Definition 10, it is known that the literal converse of corresponding Property 5 does not hold, that is, that is, there are safety verification problems that are safe, but do not have a barrier certificate [15, Example 3]. Still, there are partial converse theorems [12, 17]. The most general result [17] proves a converse for Morse-Smale vector fields under the assumption of robustness.

The main result of this paper is a converse theorem of Property 5 that still assumes robustness, but is not restricted to Morse-Smale vector fields:

Theorem 1**.**

Assume a safety verification problem $(f,I,U)$ that is robustly safe, such that the closures of $I$ and $U$ are disjoint, and the set of safe states $\mathbb{R}^{n}\setminus U$ is bounded. Then the safety verification problem has a barrier certificate.

The second result is the following converse of Property 4 that is based on a finite time reach set:

Theorem 2**.**

If a safety verification problem $(f,I,U)$ is robustly safe with robustness margin $\varepsilon$ and the set of safe states $\mathbb{R}^{n}\setminus U$ is bounded, then for all $\Delta>0$ there is a $t\geq 0$ such that $R_{f,\frac{\varepsilon}{2}}^{[0,\Delta]}(R_{f,\varepsilon}^{[0,t]}(I))$ is an $\frac{\varepsilon}{2}$-robust safety certificate.

In the following section we first summarize some facts that directly follow from the literature. Then, in Section 4 we prove Theorem 1, and in Section 5, Theorem 2. Section 6 concludes the paper.

3 Preliminaries

In this section we summarize some facts that directly follow from the literature. We first relate the notion of an $\varepsilon$-solution to controllability:

Property 6**.**

Given a smooth $f:\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$ and $\Delta>0$, if there is a control input $u:[0,\Delta]\rightarrow[-\varepsilon,\varepsilon]^{n}$ s.t. $\dot{x}=f(x)+u(t)$ has a solution with $x(0)=p$ and $x(\Delta)=p^{\prime}$, then $p^{\prime}\in R^{\Delta}_{f,\varepsilon}(\{p\})$.

Hence we can apply results from controllability to our context. The following property directly follows from this:

Property 7**.**

Given an ODE $\dot{x}=f(x)$ with smooth $f:\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$, $\varepsilon$, $\hat{\varepsilon}$ with $0\leq\varepsilon<\hat{\varepsilon}$, $\Delta>0$, $p$ and $p^{\prime}$ such that $p^{\prime}\in R^{\Delta}_{f,\varepsilon}(\{p\})$, there is a $\delta>0$ such that every point in the $\delta$-neighborhood of $p^{\prime}$ is in $R_{f,\hat{\varepsilon}}^{\Delta}(\{p\})$.

The usual proof of (a generalization of) this property [9, Proposition 3.3], [14, Proposition 11.2] uses the inverse function theorem to map each point $p^{*}$ in the neighborhood of $p^{\prime}$ to a vector $\xi_{1},\dots,\xi_{n}$ that generates an input of the form needed by Property 6 to steer the system into $p^{*}$. Due to a version of the inverse function theorem [6, Theorem 2.9.4] that bounds the size of this neighborhood from below based on a Lipschitz constant for the derivative of the given function, the size $\delta$ of the neighborhood in Property 7 can be bounded from below over all elements $p$ and $p^{\prime}$ of a compact set:

Lemma 1**.**

Given an ODE $\dot{x}=f(x)$ with smooth $f:\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$, and a compact set $\Omega\subseteq\mathbb{R}^{n}$. Then, for every $\varepsilon>0$, $\Delta>0$ there is a $\delta>0$ such that for all $p,p^{\prime}\in\Omega$ such that $p^{\prime}\in\mathit{cl}(R^{\Delta}_{f,\frac{\varepsilon}{2}}(\{p\}))$, every point in the $\delta$-neighborhood of $p^{\prime}$ is in $R^{\Delta}_{f,\varepsilon}(\{p\})$.

4 Robust Converse Theorem for Barrier Certificates

In this section, we will prove Theorem 1. Throughout the section, we will assume a safety verification problem $(f,I,U)$ that fulfills the premises of this theorem: robust safety, disjointness of the closures of $I$ and $U$, and boundedness of the set of safe states $\mathbb{R}^{n}\setminus U$. We will denote by $\mu$ the robustness margin of $(f,I,U)$, and by $V$ a $\mu$-robust safety certificate whose existence is ensured by Property 4. We will construct a barrier certificate from the boundary ${\partial\mathit{cl}(V)}$ of the closure of $V$. We will first prove that the solutions of $f$ starting in ${\partial\mathit{cl}(V)}$ do not have any further intersection with ${\partial\mathit{cl}(V)}$—even in reverse time:

Lemma 2**.**

For every $x\in R_{f}^{\mathbb{R}}({\partial\mathit{cl}(V)})$ there is precisely one $t\in\mathbb{R}$ such that $\varphi_{f}(x,t)\in{\partial\mathit{cl}(V)}$

Proof.

By the definition of $R_{f}^{\mathbb{R}}({\partial\mathit{cl}(V)})$ there is at least one such $t$. It suffices to prove that there is not more than one. For this we assume that there are $t_{1}$ and $t_{2}$ such that $t_{1}\neq t_{2}$, and both $\varphi_{f}(x,t_{1})$ and $\varphi_{f}(x,t_{2})$ are in ${\partial\mathit{cl}(V)}$. W.l.o.g. assume that $t_{1}<t_{2}$. Let $\hat{t}$ be such that $t_{1}<\hat{t}<t_{2}$.

Then $\varphi(x,t_{2})=\varphi(\varphi(x,\hat{t}),t_{2}-\hat{t})$ and so $\varphi(x,t_{2})\in R^{t_{2}-\hat{t}}_{f,0}(\{\varphi(x,\hat{t})\})$. Therefore, by Property 7, there is a neighborhood of $\varphi(x,t_{2})$ such that every point in this neighborhood is $\mu$-reachable from $\varphi(x,\hat{t})$. The same argument applied in reverse time to $t_{1}$ and $\hat{t}$ ensures a neighborhood of $\varphi(x,t_{1})$ such that $\varphi(x,\hat{t})$ is $\mu$-reachable from every point in this neighborhood. Let $x_{1}$ be in the neighborhood of $\varphi(x,t_{1})$ such that $x_{1}\in V$, and let $x_{2}$ be in the neighborhood of $\varphi(x,t_{2})$ such that $x_{2}\not\in V$. Then there is a $\mu$-solution from $x_{1}\in V$ over $\varphi_{f}(x,\hat{t})$ to $x_{2}\not\in V$. This is in contradiction to the fact that $V$ is a $\mu$-robust safety certificate. ∎

We will now introduce a function $\nu(x)$ from which we will later obtain the barrier certificate by smooth approximation. Let $\nu(x)$ be such that $\nu(x)$ is defined on $R_{f}^{\mathbb{R}}({\partial\mathit{cl}(V)})$ and such that $\nu(x):=-t$ with $t$ being the unique $t$ with $\varphi_{f}(x,t)\in{\partial\mathit{cl}(V)}$ ensured by Lemma 2. Note that $\nu(x)$ is positive for all points of the interior of $V$ for which it is defined and negative for all points of the complement of the closure of $V$ for which it is defined. Moreover, ${\partial\mathit{cl}(V)}$ is in the interior of the domain of definition of $\nu$. Due to the definition of $\nu$ we also have:

Property 8**.**

For $x\in R_{f}^{\mathbb{R}}({\partial\mathit{cl}(V)})$, $\nu(\varphi(x,t))=\nu(x)+t$.

In general, functions defined based on the length of solutions leading to some set are not continuous. But using the robustness of $V$ we will be able to prove continuity:

Lemma 3**.**

The function $\nu$ is continuous in an open neighborhood of ${\partial\mathit{cl}(V)}$.

Before formally proving this lemma, we explain the idea of the proof. We assume that $\nu$ is not continuous let us say at a point $x$, and derive a contradiction. Let $y$ be the point where the solution from $x$ enters $V$. Then, due to non-continuity, the situation shown in Figure 1 arises: There is a point $x^{\prime}$ close to $x$ such that the solution from $x^{\prime}$ enters a close neighborhood of $y$ (point $\hat{y}$), but then enters $V$ at a different point further away. Letting $y^{\prime}$ be close to that entrance point but still outside of $V$ we can perturb the trajectory from $\hat{y}$ to $y^{\prime}$ by moving $\hat{y}$ to $y$. The resulting trajectory leads from $y$ to $y^{\prime}$ and hence leaves $V$ which is a contradiction to $V$ being a robust safety certificate.

The figure illustrates the situation where $x\not\in V$, but we do not assume this in the proof by exploiting the fact that the flow $\varphi$ also allows negative time.

Proof.

The function $\nu$ being continuous in an open neighborhood of ${\partial\mathit{cl}(V)}$ means that for all elements $x$ of this neighborhood, for all $\varepsilon>0$ there exists $\delta>0$ s.t. for all $x^{\prime}$ with $||x^{\prime}-x||<\delta$, $|\nu(x^{\prime})-\nu(x)|<\varepsilon$. We assume non-continuity of $\nu$ in every open neighborhood of ${\partial\mathit{cl}(V)}$, and derive a contradiction.

Since the set of states $\mathbb{R}^{n}\setminus U$ is bounded and the safety verification problem $(f,I,U)$ is robustly safe, the safety certificate $V$ is bounded, too. Let $N$ be an open, but bounded, neighborhood of ${\partial\mathit{cl}(V)}$. Due to our assumption, $\nu$ is non-continuous in $N$, that is, there is an $x\in N$, $\varepsilon>0$ s.t. $\forall\delta>0\exists x^{\prime}$ s.t. $||x-x^{\prime}||\leq\delta$, $|\nu(x)-\nu(x^{\prime})|\geq\varepsilon$. Choose such an $x$ and $\varepsilon$.

Since $N$ is open, but bounded, $\mathit{cl}(N)$ is compact. Now let $\hat{\delta}^{+}$ be the constant ensured by Lemma 1 after choosing $\Omega$ as $\mathit{cl}(N)$, $\varepsilon$ as $\frac{\mu}{2}$, and $\Delta$ as the constant $\varepsilon$ chosen above. Let $\hat{\delta}^{-}$ be the corresponding constant for reverse dynamics $-f$. Choose $\hat{\delta}=\min\{\hat{\delta}^{+},\hat{\delta}^{-}\}$. Then for all $p,p^{\prime}\in N$ such that $p^{\prime}\in\mathit{cl}(R^{\varepsilon}_{f,\frac{\mu}{4}}(\{p\}))$, every point in the $\hat{\delta}$-neighborhood of $p^{\prime}$ is in $R^{\varepsilon}_{f,\frac{\mu}{2}}(\{p\})$. Also for all $p,p^{\prime}\in N$ such that $p^{\prime}\in\mathit{cl}(R^{\varepsilon}_{-f,\frac{\mu}{4}}(\{p\}))$, every point in the $\hat{\delta}$-neighborhood of $p^{\prime}$ is in $R^{\varepsilon}_{-f,\frac{\mu}{2}}(\{p\})$. We note these properties and refer to them below by $(*)^{+}$, and $(*)^{-}$, respectively.

Since the flow $\varphi$ is continuous we can choose a $\delta$ s.t. for all $x^{\prime}$ with $||x-x^{\prime}||<\delta$, $||\varphi(x,-\nu(x))-\varphi(x^{\prime},-\nu(x))||<\hat{\delta}$. Due to our assumption of non-continuity of $\nu$, for this $\delta$ there is an $x^{\prime}$ s.t. $||x-x^{\prime}||\leq\delta$, $|\nu(x)-\nu(x^{\prime})|\geq\varepsilon$.

Let $y:=\varphi_{f}(x,-\nu(x))$, $\hat{y}:=\varphi_{f}(x^{\prime},-\nu(x))$, $y^{\prime}:=\varphi_{f}(\hat{y},\mathit{sgn}(\nu(x)-\nu(x^{\prime}))\varepsilon)$. Then $||y-\hat{y}||<\hat{\delta}$, and $y^{\prime}=\varphi_{f}(\varphi_{f}(x^{\prime},-\nu(x)),\mathit{sgn}(\nu(x)-\nu(x^{\prime}))\varepsilon)=\varphi_{f}(x^{\prime},-\nu(x)+\mathit{sgn}(\nu(x)-\nu(x^{\prime}))\varepsilon)$. Hence, by Property 8, $\nu(y^{\prime})=\nu(\varphi_{f}(x^{\prime},-\nu(x)+\mathit{sgn}(\nu(x)-\nu(x^{\prime}))\varepsilon))=\nu(x^{\prime})-\nu(x)+\mathit{sgn}(\nu(x)-\nu(x^{\prime}))\varepsilon$.

We have two cases:

• •

If $\nu(x)-\nu(x^{\prime})\geq 0$, then $\nu(x)-\nu(x^{\prime})=|\nu(x)-\nu(x^{\prime})|\geq\varepsilon$, and

[TABLE]

Since $y^{\prime}=\varphi_{f}(\hat{y},\mathit{sgn}(\nu(x)-\nu(x^{\prime}))\varepsilon)=\varphi_{f}(\hat{y},\varepsilon)$, $\hat{y}=\varphi_{-f}(y^{\prime},\varepsilon)$, and hence $\hat{y}\in\mathit{cl}(R^{\varepsilon}_{-f,\frac{\mu}{4}}(\{y^{\prime}\}))$. So by Property $(*)^{-}$ noted above, $y\in R^{\varepsilon}_{-f,\frac{\mu}{2}}(\{y^{\prime}\})$, and so $y^{\prime}\in R^{\varepsilon}_{f,\frac{\mu}{2}}(\{y\})$. But $\nu(y)=0$ and $\nu(y^{\prime})\leq 0$. Hence $y\in\mathit{cl}(V)$ and $y^{\prime}\not\in\mathit{int}(V)$.

• •

If $\nu(x)-\nu(x^{\prime})\leq 0$, then $-(\nu(x)-\nu(x^{\prime}))=|\nu(x)-\nu(x^{\prime})|\geq\varepsilon$, and

[TABLE]

Since $y^{\prime}=\varphi_{f}(\hat{y},\mathit{sgn}(\nu(x)-\nu(x^{\prime}))\varepsilon)=\varphi_{f}(\hat{y},-\varepsilon)$, $\hat{y}=\varphi_{f}(y^{\prime},\varepsilon)$, and hence $\hat{y}\in\mathit{cl}(R^{\varepsilon}_{f,\frac{\mu}{4}}(\{y^{\prime}\}))$. So, by Property $(*)^{+}$ noted above, $y\in R^{\varepsilon}_{f,\frac{\mu}{2}}(\{y^{\prime}\})$. But $\nu(y^{\prime})\geq 0$ and $\nu(y)=0$. Hence $y^{\prime}\in\mathit{cl}(V)$ and $y\not\in\mathit{int}(V)$.

In both cases, we have a $\frac{\mu}{2}$-solution from a point in $\mathit{cl}(V)$ to a point not in $\mathit{int}(V)$. Hence, using the same construction as in the second part of the proof of Lemma 2 above, one gets a $\mu$-solution from a point in $V$ to a point not in $V$ which is a contradiction to the fact that $V$ is a $\mu$-robust safety certificate.

∎

Using the notation

[TABLE]

we now remind the reader of a classical result by W. Wilson [16, Theorem 2.5], and for the reader’s convenience, we state here a direct corollary:

Lemma 4**.**

If $h$ is a continuous real-valued function on a compact set $N$, $f$ is a non-singular vector field on $N$, and $\mathcal{L}_{f}h$ is defined on $N$ and continuous, then for every $\varepsilon>0$ there exists a $C^{\infty}$-function $h^{\prime}:N\rightarrow\mathbb{R}$ such that for all $x\in N$,

[TABLE]

and

[TABLE]

Based on this, we can now construct a robust barrier certificate from the robust safety certificate $V$:

Lemma 5**.**

There is a differentiable function $\beta:\mathbb{R}^{n}\rightarrow\mathbb{R}$ and $\varepsilon>0$ such that

• •

$\forall x\;.\;x\in I\Rightarrow\beta(x)>\varepsilon$**

• •

$\forall x\;.\;|\beta(x)|\leq\varepsilon\Rightarrow L_{f}(\beta)(x)>\varepsilon$, that is $(\nabla\beta(x))^{T}f(x)>\varepsilon$

• •

$\forall x\;.\;x\in U\Rightarrow\beta(x)<\varepsilon$**

Proof.

From the $\varepsilon$-robust safety certificate $V$ we can construct a function $\nu$ as above. The zero set $\{x\mid\nu(x)=0\}$ is equal to ${\partial\mathit{cl}(V)}$, and hence it intersects neither $I$ nor $U$. Moreover, $f$ is non-singular on this set. For all $\delta\in\mathbb{R}^{\geq 0}$, let $N_{\delta}:=\{x\mid|\nu(x)|\leq\delta\}$. Now let $0<\delta<\frac{1}{2}$ be such that the $\delta$-sublevel set $N_{\delta}$ still intersects neither $I$ nor $U$, $f$ is non-singular on $N_{\delta}$, and $N_{\delta}$ is contained in the open neighborhood of ${\partial\mathit{cl}(V)}$ for which Lemma 3 ensures continuity of $\nu$.

Now observe that for all $x\in N_{\delta}$,

[TABLE]

Further, due to continuity of $\nu$ we can use Lemma 4 to construct a $C^{\infty}$-function $\nu^{\prime}$ such that for all $x\in N_{\delta}$,

[TABLE]

and

[TABLE]

Then for all $x\in N_{\delta}$, $(\mathcal{L}_{f}\nu^{\prime})(x)>1-\frac{\delta}{2}>0$, and for all $x\not\in N_{\frac{\delta}{2}}$, $\nu^{\prime}(x)\neq 0$.

Now let $\mathcal{X}=(X_{\alpha})_{\alpha\in A}$ be an open cover of $\mathbb{R}^{n}$ indexed by a set $A$. Assume furthermore, that for all $\alpha\in A$, $X_{\alpha}$ contains a common element with at most one of the sets $N_{\frac{\delta}{2}}$, $\{x\mid\nu(x)\geq\delta\}$, and $\{x\mid\nu(x)\leq-\delta\}$. Let $(\beta_{\alpha})_{\alpha\in A}$ be a family of functions s.t. for each $\alpha\in A$, and $x\in\mathbb{R}^{n}$,

[TABLE]

Let $(\psi_{\alpha})_{\alpha\in A}$ be a partition of unity [8, Chapter 2] sub-ordinate to $\mathcal{X}$ and

[TABLE]

Since $(\psi_{\alpha})_{\alpha\in A}$ is a partition of unity, $\beta$ is smooth. Since for all $\alpha\in A$, for all $x\not\in N_{\frac{\delta}{2}}$, $\beta_{\alpha}(x)\neq 0$, $\beta$ is non-zero outside of $N_{\frac{\delta}{2}}$. Since $\beta$ coincides with $\nu^{\prime}$ on $N_{\frac{\delta}{2}}$, for all $x\in N_{\frac{\delta}{2}}$, $(\mathcal{L}_{f}\beta)(x)>0$. Moreover, $\beta$ is strictly positive on $I$, and strictly negative on $U$. The existence of a bound $\varepsilon>0$ follows due to continuity of $\beta$ and compactness of all relevant sets.

∎

Theorem 1 follows as a corollary.

5 Finite Time Converse Theorem for Safety Certificates

The construction in the previous section was based on a robust safety certificate $V$ whose existence is ensured by Property 4. However, this property has the disadvantage of being based on an infinite time reach set. We will remove this disadvantage by proving Theorem 2 in the next section.

The proof extends a technique introduced by M. Fränzle [3], that he originally used for proving existence of a barrier for hybrid systems with polynomial flow: Take the bloated finite-time reach set $R_{f,\varepsilon}^{[0,t]}(I)$, and show that the original dynamics is shrinking on it if the bloated reach set does not grow beyond the bounded complement of $U$. However, here we have additional complications: First, our flow is, in general, not polynomial (note that even linear ODEs usually have a non-polynomial flow), and second, we are not satisfied with a barrier, but we want a robust barrier.

Before the actual proof, we note:

Lemma 6**.**

Let $V\subseteq\mathbb{R}^{n}$, $\Delta>0$ such that

[TABLE]

Then for all $\Delta^{\prime}\geq\Delta$,

[TABLE]

Proof.

Let $p\in R_{f,\varepsilon}(R_{f,\varepsilon}^{[0,\Delta^{\prime}]}(V))$. We prove that $p$ is also in $R_{f,\varepsilon}^{[0,\Delta^{\prime}]}(V)$.

Let $\sigma$ be the $\varepsilon$-solution leading from a point in $V$ to $p$, and let $\tau$ be the length of this solution. So $\sigma(0)\in V$ and $\sigma(\tau)=p$. Since $R_{f,\varepsilon}^{\Delta}(V)\subseteq V$, also $\sigma(\Delta)\in V$. In general, for every $i$, $\sigma(i\Delta)\in V$. Let $b$ be the maximal $i$ with $i\Delta<\tau$. Then $0\leq\tau-b\Delta\leq\Delta\leq\Delta^{\prime}$, and hence $p\in R_{f,\varepsilon}^{\tau-b\Delta}(\{\sigma(b\Delta)\})\subseteq R_{f,\varepsilon}^{[0,\Delta^{\prime}]}(\{\sigma(b\Delta)\})\subseteq R_{f,\varepsilon}^{[0,\Delta^{\prime}]}(V)$. ∎

Now we are ready to prove Theorem 2:

Proof.

We assume that $(f,I,U)$ is robustly safe with robustness margin $\varepsilon$, and the complement of $U$ is bounded. We derive a contradiction from the additional assumption that there exists $\Delta>0$ such that for all $t\geq 0$, $R_{f,\frac{\varepsilon}{2}}^{[0,\Delta]}(R_{f,\varepsilon}^{[0,t]}(I))$ is no $\frac{\varepsilon}{2}$-robust safety certificate.

We first observe that for every $t\geq 0$, $R_{f,\varepsilon}^{[0,t]}(I)\not\supseteq R^{\Delta}_{f,\frac{\varepsilon}{2}}(R_{f,\varepsilon}^{[0,t]}(I))$. Otherwise, due to Lemma 6, $R_{f,\frac{\varepsilon}{2}}(R_{f,\frac{\varepsilon}{2}}^{[0,\Delta]}(R_{f,\varepsilon}^{[0,t]}(I)))\subseteq R_{f,\frac{\varepsilon}{2}}^{[0,\Delta]}(R_{f,\varepsilon}^{[0,t]}(I))$, and $R_{f,\frac{\varepsilon}{2}}^{[0,\Delta]}(R_{f,\varepsilon}^{[0,t]}(I))$ would be a $\frac{\varepsilon}{2}$-robust safety certificate, which would be in contradiction to the assumption above.

We now derive a contradiction from the above by constructing an infinite sequence of points $p_{1},\dots,$ such that

• •

for every $i$, $p_{i}\in R_{f,\varepsilon}^{[0,\infty]}(I)$, and

• •

for every $i,j$, $i\neq j$, we have $||p_{j}-p_{i}||>\delta$,

with $\delta$ being a positive real number. This implies that the maximal distance of two points in the sequence grows over all bounds. Since the complement of $U$ is bounded, this is a contradiction to the fact that $(f,I,U)$ is robustly safe.

We ensure the second property (sufficient distance of points) by constructing at the same time a sequence $t_{1},\dots,$ such that, for all $i$,

• •

every point not $\varepsilon$-reachable in time $t_{i}$, that is, every point not in $R_{f,\varepsilon}^{[0,t_{i}]}(I)$ has distance at least $\delta$ from every point $p_{1},\dots,p_{i}$ (in Figure 2, the $\delta$-balls around $p_{i}$ are inside of the reach sets $R_{f,\varepsilon}^{[0,t_{i}]}(I)$).

• •

$p_{i+1}$ is not $\varepsilon$-reachable in time $t_{i}$, that is, $p_{i+1}\not\in R_{f,\varepsilon}^{[0,t_{i}]}(I)$ (in Figure 2, the points $p^{\prime}=p_{i+1}$ are outside of the reach sets $R_{f,\varepsilon}^{[0,t_{i}]}(I)$).

It remains to construct the sequences $p_{1},\dots,$ and $t_{1},\dots,$ in such a way. Due to the Heine-Borel theorem, the closure of the complement of $U$ is compact. So we can apply Lemma 1: Let $\delta$ be as given by Lemma 1 for $\Omega$ being the closure of the complement of $U$. Let $i$ be an arbitrary, but fixed natural number, and assume that the above properties hold for $p_{1},\dots,p_{i}$ and $t_{1},\dots,t_{i}$. We construct $p_{i+1},t_{i+1}$ together with a proof that the above properties hold for them.

For this, let $p\in R_{f,\varepsilon}^{[0,t_{i}]}(I)$, $p^{\prime}\not\in R_{f,\varepsilon}^{[0,t_{i}]}(I)$ s.t. $p^{\prime}$ is $\frac{\varepsilon}{2}$-reachable in time $\Delta$ from $p$ which exist since for all $t\geq 0$, $R_{f,\varepsilon}^{[0,t]}(I)\not\supseteq R^{\Delta}_{f,\frac{\varepsilon}{2}}(R_{f,\varepsilon}^{[0,t]}(I))$. By Lemma 1 every point in the $\delta$-neighborhood of $p^{\prime}$ is reachable in time $\Delta$ from $p\in R_{f,\varepsilon}^{[0,t_{i}]}(I)$ with $\varepsilon$-perturbed dynamics.

So we choose $p_{i+1}=p^{\prime},t_{i+1}=t_{i}+\Delta$. Then $p_{i+1}\not\in R_{f,\varepsilon}^{[0,t_{i}]}(I)$, and hence has distance at least $\delta$ from $p_{1},\dots,p_{i}$. Moreover, every point not reachable in time $t_{i+1}$ again has distance at least $\delta$ from $p_{1},\dots,p_{i+1}$.

We choose $t_{1}=0$ and $p_{1}$ an initial point that has distance at least $\delta$ from the boundary of the set of initial points $I$ (the case where such a point does not exist can be easily handled by shifting the sequence).

∎

6 Conclusion

In this paper we proved a robust converse theorem for barrier certificates, removing restrictions of such theorems in the literature. Moreover, we proved that a certain finite time reach set of a robustly safe system always forms a robust safety certificate. The literature contains several variants of the notion of a barrier certificate [15, 4]. We propose a comprehensive converse theory covering those variants as a goal for future work in the area.

The actual computation of barrier certificates [1, 2, 18, 13] is an essential question that deserves further attention.