# Lyapunov-Barrier Characterization of Robust Reach-Avoid-Stay Specifications
for Hybrid Systems111This paper was not presented at any IFAC meeting.

Yiming Meng<EMAIL_ADDRESS>Jun Liu<EMAIL_ADDRESS>
###### Abstract

Stability, reachability, and safety are crucial properties of dynamical
systems. While verification and control synthesis of reach-avoid-stay
objectives can be effectively handled by abstraction-based formal methods,
such approaches can be computationally expensive due to the use of state-space
discretization. In contrast, Lyapunov methods qualitatively characterize
stability and safety properties without any state-space discretization. Recent
work on converse Lyapunov-barrier theorems also demonstrates an approximate
completeness for verifying reach-avoid-stay specifications of systems modelled
by nonlinear differential equations. In this paper,  based on the topology of
hybrid arcs, we extend the Lyapunov-barrier characterization to more general
hybrid systems described by differential and difference inclusions. We show
that Lyapunov-barrier functions are not only sufficient to guarantee reach-
avoid-stay specifications for well-posed hybrid systems, but also necessary
for arbitrarily slightly perturbed systems under mild conditions.  Numerical
examples are provided to illustrate the main results.

###### keywords:

Hybrid systems; Reach-avoid-stay specifications; Stability with safety;
Robustness; Converse Lyapunov-barrier functions theorems.

††journal: Nonlinear Analysis: Hybrid Systems

organization=Department of Applied Mathematics, University of Waterloo, city=
Ontario, country=Canada

##  1 Introduction

The reach-avoid-stay property is one of the building blocks for specifying
more complex temporal logic objectives. States (or controlled states) of
dynamical systems with reach-avoid-stay properties are always within the safe
region and, moreover, reach a target set within a finite time and stay inside
it afterwards.

For hybrid systems modelled by differential and difference equations with
possibly small perturbations, verification and control synthesis of various
linear temporal logic properties are achievable via abstraction-based formal
methods [1, 2, 3] and model checking algorithms [4], where state space
discretization and abstraction analysis are needed to guarantee the soundness
and (approximated) completeness [5, 6, 7, 8] of the generated symbolic models.
Regardless of the potentially heavy computational efforts, formal methods are
guaranteed to return the set of initial states from which the specification
are satisfied. The current literature that pertains to formal methods focuses
on developing algorithms to reduce the computational complexity [9, 10, 11,
12]. However, case studies in [13] have shown that for systems that also
continuously depend on tunable parameters and undergo bifurcations, challenges
arose regarding the sampling time for constructing abstractions under the non-
uniform rates of state evolution.

Compared to formal methods, Lyapunov-like functions are able to characterize
stability and safety related attributes without state space discretization
[14, 15, 16]. The flexible quadratic programming framework [17] with Lyapunov
and barrier constraints also shows effectiveness in the control synthesis of
stabilization and safety objectives. The work in [18] developed sufficient
conditions for stabilization with safety guarantees by uniting Lyapunov and
barrier functions (see [18, Proposition 1] for details). However, the
conditions imply that the unsafe set has to be unbounded [19]. The authors in
[20] further made an interesting observation that the derived control
Lyapunov-barrier conditions proposed in [18, Section 4, 5] are topologically
invalid. They instead proposed sufficient conditions for safe stabilization
using non-smooth control Lyapunov functions [21].

The recent work [22] improved the Lyapunov-barrier approach and showed that it
is possible to construct united Lyapunov and barrier functions, or even a
single Lyapunov function, that are defined on the entire set of initial
conditions from which stabilization with safety guarantees is satisfied. The
connection between stabilization with safety guarantees and reach-avoid-stay
was also established via robustness. The work [13] proposed control Lyapunov-
barrier functions and provided sufficient conditions for control synthesis
with reach-avoid-stay specifications. Such a method has been numerically shown
to outperform abstraction-based algorithms in a system that undergoes a Hopf-
bifurcation.

The latest research [23] has shown that the existence of the stochastic
analogue of Lyapunov-barrier functions is also sufficient for characterizing
probabilistic reach-avoid-stay specifications for stochastic systems with
point-mass uncertainties. However, due to the effects of diffusion and the
concept of weak solutions, probabilistic reach-avoid-stay specifications,
other than strong reach-avoid-stay with probability one, may fail to be
related to probabilistic stability with safety guarantees w.r.t. some subset
of the target set, and hence the (approximated) necessity of Lyapunov-barrier
characterization for probabilistic reach-avoid-stay does not hold for
stochastic dynamical systems.

In this paper, we show that the Lyapunov-barrier approach can be extended to
verification of reach-avoid-stay specifications for hybrid systems with
differential and difference inclusions. Unlike systems with diffusion, reach-
avoid-stay properties of solutions to hybrid systems can be converted to
stabilization with safety guarantees under mild conditions. The approximate
equivalence of these two types of specifications can be established via
robustness. We show that smooth Lyapunov-barrier functions can be constructed
given the compactness of target set and the set of initial states.  Note that
even though the idea follows the previous work in [22] and [23], the
underlying topology of the solutions to hybrid systems are different. Hence,
the previous results are not directly applicable. We aim to leverage the rich
results on stability theory of hybrid systems [24] to unify Lyapunov and
barrier conditions in the context of converse Lyapunov-barrier theorems.

We mention that the latest converse barrier theorems for differential
inclusions [25, 26, 27], in comparison to the previous works [28, 29, 30],
provide a possibility to construct less smooth Lyapunov-barrier functions
under less restricted topological requirement, e.g., unbounded reachable set.
In this paper, we only consider the case where the uniformly asymptotically
stable set is compact, which seems already satisfactory in practice. For this
reason, we stick with the compactness assumption on the target set and the set
of initial states, and discuss the possible relaxation of safe conditions
based on [25, 26, 27] in Section 4.

The rest of this paper is organized as follows. In Section 2, we present the
preliminaries for the systems, concepts of solutions, as well as other
important definitions. In Section 3, we show the connections between robust
reach-avoid-stay and stability with safety guarantees. In Section 4, we
provide the converse Lyapunov-barrier functions theorem for both stability
with safety guarantees and reach-avoid-stay specifications. We illustrate the
results with examples in Section 5 and conclude the paper in Section 6.

Notation: We denote by $\mathbb{R}^{n}$ the Euclidean space of dimension
$n>1$, by $\mathbb{R}$ the set of real numbers, by $\mathbb{R}_{>0}$ the set
of positive real numbers, and by $\mathbb{R}_{\geq 0}$ the set of nonnegative
real numbers. For $x\in\mathbb{R}^{n}$ and $r\geq 0$, we denote the ball of
radius $r$ centered at $x$ by
$x+r\mathcal{B}=\left\\{y\in\mathbb{R}^{n}:\,\left|y-x\right|\leq r\right\\}$,
where $\left|\;\cdot\;\right|$ is the Euclidean norm. For a closed set
$A\subseteq\mathbb{R}^{n}$ and $x\in\mathbb{R}^{n}$, we denote the distance
from $x$ to $A$ by $\left|x\right|_{A}=\inf_{y\in A}\left|x-y\right|$ and
$r$-neighborhood of $A$ by $A+r\mathcal{B}=\cup_{x\in
A}(x+r\mathcal{B})=\left\\{x\in\mathbb{R}^{n}:\,\left|x\right|_{A}\leq
r\right\\}$. For a set $A\subseteq\mathbb{R}^{n}$, $\overline{A}$ denotes its
closure, $\operatorname{int}(A)$ denotes its interior, and $\partial A$
denotes its boundary. For two sets $A,B\subseteq\mathbb{R}^{n}$, the set
difference is defined by $A\setminus B=\left\\{x:\,x\in A,\,x\not\in
B\right\\}$.

We denote by $F:\mathbb{R}^{m}\rightrightarrows\mathbb{R}^{n}$ a set-valued
map. We say a function $\alpha:\,\mathbb{R}_{\geq
0}\rightarrow\mathbb{R}_{\geq 0}$ belongs to class $\mathcal{K}$ if it is
continuous, zero at zero, and strictly increasing. It is said to belong to
$\mathcal{K}_{\infty}$ if it belongs to class $\mathcal{K}$ and is unbounded.
A function $\beta:\,\mathbb{R}_{\geq 0}\times\mathbb{R}_{\geq
0}\rightarrow\mathbb{R}_{\geq 0}$ is said to belong to class $\mathcal{KL}$
if, for each $t\geq 0$, $\beta(\cdot,t)$ belongs to class $\mathcal{K}$ and,
for each $s\geq 0$, $\beta(s,\cdot)$ is decreasing and satisfies
$\lim_{t\rightarrow\infty}\beta(s,t)=0$.

##  2 Preliminaries

###  2.1 Hybrid systems

Consider a hybrid system $\mathbf{H}=(C,F,D,G)$ with dynamics

$\displaystyle\dot{x}\in F(x),\;\;\;\;\;x\in C,$ (1a) $\displaystyle x^{+}\in
G(x),\;\;\;x\in D,$ (1b)

where $C,D\subseteq\mathbb{R}^{n}$ represent the flow set and the jump set
respectively, and the set-valued maps
$F:\mathbb{R}^{n}\rightrightarrows\mathbb{R}^{n}$,
$G:\mathbb{R}^{n}\rightrightarrows\mathbb{R}^{n}$ represent the flow and jump
maps respectively.

Given a scalar $\delta\geq 0$, the (additive) $\delta$-perturbation of
$\mathbf{H}$, denoted by $\mathbf{H}_{\delta}$, is described as

$\displaystyle\dot{x}\in F(x)+\delta\mathcal{B},\;\;\;\;\;x\in C_{\delta},$
(2a) $\displaystyle x^{+}\in G(x)+\delta\mathcal{B},\;\;\;x\in D_{\delta},$
(2b)

where $C_{\delta}=C+\delta\mathcal{B}$ and $D_{\delta}=D+\delta\mathcal{B}$. A
hybrid time domain is a subset $E\subseteq\mathbb{R}_{\geq 0}\times\mathbb{N}$
of the form $\cup_{j=0}^{J}[t_{j},t_{j+1}]\times\left\\{j\right\\}$, where
$J\in\mathbb{N}\cup\left\\{\infty\right\\}$ and $0=t_{0}\leq t_{1}\leq
t_{2}\leq\dots$. Given $(t,j),(t^{\prime},j^{\prime})\in E$, the natural
ordering is such that $t+j\leq t^{\prime}+j^{\prime}$ if $t\leq t^{\prime}$
and $j\leq j^{\prime}$. A hybrid arc is a function
$\phi:E\rightarrow\mathbb{R}^{n}$ from a hybrid domain $E$ to $\mathbb{R}^{n}$
and, for each fixed $j$, $t\mapsto\phi(t,j)$ is locally absolutely continuous
on the interval $I^{j}=\\{t:(t,j)\in\operatorname{dom}(\phi)\\}$.

######  Definition 2.1 (Solution concept)

A hybrid arc $\phi$ is a solution to (1) if

  1. (i)

$\phi(0,0)\in\overline{C}\cup D$;

  2. (ii)

for all $j\in\mathbb{N}$ such that $\operatorname{int}(I^{j})\neq\emptyset$,
we have

$\begin{split}&\phi(t,j)\in C\;\;\text{for
all}\;t\in\operatorname{int}(I^{j}),\\\ &\dot{\phi}(t,j)\in
F(\phi(t,j))\;\;\text{for almost all}\;t\in I^{j};\end{split}$

  3. (iii)

for all $(t,j)\in\operatorname{dom}(\phi)$ such that
$(t,j+1)\in\operatorname{dom}(\phi)$, we have $\phi(t,j)\in D$ and
$\phi(t,j+1)\in G(\phi(t,j))$.

Solutions to $\mathbf{H}_{\delta}$ for $\delta>0$ are defined in a similar
way. Furthermore, a solution $\phi$ to $\mathbf{H}_{\delta}$ is maximal if
there is no other $\psi$ to $\mathbf{H}_{\delta}$ such that
$\phi(t,j)=\psi(t,j)$ for all $(t,j)\in\operatorname{dom}(\phi)$ and
$\operatorname{dom}(\phi)$ is a proper subset of $\operatorname{dom}(\psi)$
[24, Definition 2.7].

We also define the range of a solution arc $\phi$ as
$\operatorname{rge}(\phi)=\\{\phi(t,j):(t,j)\in\operatorname{dom}(\phi)\\}$
for convenience. For $\delta\geq 0$, we denote by
$\mathfrak{S}_{\mathbf{H}}^{\delta}(x)$ the set of all maximal solutions
starting from $x\in\mathbb{R}^{n}$ for a hybrid system $\mathbf{H}_{\delta}$;
we denote by $\mathfrak{S}_{\mathbf{H}}^{\delta}(K)$ the set of all maximal
solutions starting from the set $K\subseteq\mathbb{R}^{n}$ for
$\mathbf{H}_{\delta}$.

We introduce correspondingly some notations for reachable sets of
$\mathbf{H}_{\delta}$ from some $K\subseteq\mathbb{R}^{n}$. For $T\geq 0$, we
define

$\mathcal{R}^{\delta}_{\leq
T}(K)=\left\\{\phi(t,j):\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(K),\phi(0,0)\in
K,t+j\leq T\right\\}.$

The reachable sets $\mathcal{R}^{\delta}_{<T}(K)$ and
$\mathcal{R}^{\delta}_{\geq T}(K)$ are defined in a similar way. The infinite-
horizon reachable set from $K$ for $\mathbf{H}_{\delta}$ is
$\mathcal{R}^{\delta}(K)=\left\\{\phi(t,j):\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(K),\;(t,j)\in\operatorname{dom}(\phi)\right\\}$.

###### Assumption 2.2

We make the standing assumption that $\mathbf{H}$ should satisfy the basic
conditions:

  1. (C1)

$C,D\in\mathbb{R}^{n}$ are closed;

  2. (C2)

$F$ is outer semicontinuous, locally bounded, and convex for all $x\in C$;

  3. (C3)

$G$ is outer semicontinuous and locally bounded for all $x\in D$.

We also introduce the following concept of closeness of hybrid arcs that will
be frequently used in proofs.

###### Definition 2.3

[24, Definition 5.23] Given $\tau,\varepsilon>0$, two hybrid arcs $\phi_{1}$
and $\phi_{2}$ are $(\tau,\varepsilon)$-close if

  1. (a)

for all $(t,j)\in\operatorname{dom}(\phi_{1})$ with $t+j\leq\tau$ there exists
$s$ such that $(s,j)\in\operatorname{dom}(\phi_{2})$,
$\left|t-s\right|<\varepsilon$ and
$\left|\phi_{1}(t,j)-\phi_{2}(s,j)\right|<\varepsilon$;

  2. (b)

for all $(t,j)\in\operatorname{dom}(\phi_{2})$ with $t+j\leq\tau$ there exists
$s$ such that $(s,j)\in\operatorname{dom}(\phi_{1})$,
$\left|t-s\right|<\varepsilon$ and
$\left|\phi_{2}(t,j)-\phi_{1}(s,j)\right|<\varepsilon$.

###  2.2 Properties pertaining to stability and safety

In this subsection, we define properties that are related to stability and
safety of solutions to (2). Particularly, we formally introduce the concepts
of stability with safety guarantees and reach-avoid-stay type specifications.

######  Definition 2.4 (Forward (pre-) invariance)

A set $\mathfrak{I}\subseteq\mathbb{R}^{n}$ is said to be forward pre-
invariant for $\mathbf{H}_{\delta}$ if for every
$\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(\mathfrak{I})$,
$\operatorname{rge}(\phi)\subseteq\mathfrak{I}$. The set $\mathfrak{I}$ is
said to be forward invariant for $\mathbf{H}_{\delta}$ if for every forward
complete $\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(\mathfrak{I})$,
$\operatorname{rge}(\phi)\subseteq\mathfrak{I}$, i.e.,
$\mathcal{R}^{\delta}(\mathfrak{I})\subseteq\mathfrak{I}$.

###### Remark 2.5

The term ‘pre’ is in the sense that non-complete maximal solutions are not
excluded. This concept allows us to describe the completeness and dynamical
behaviors separately for general maximal solutions. For future references, we
only define the ‘pre’ properties of solutions to keep the relevant definitions
succinct.

We next consider stability for solutions of $\mathbf{H}_{\delta}$ w.r.t. a
closed set.

######  Definition 2.6 (Uniform pre-asymptotic stability)

A closed set $A\subseteq\mathbb{R}^{n}$ is said to be uniformly pre-
asymptotically stable (UpAS) for $\mathbf{H}_{\delta}$ if the following two
conditions are met:

  1. (i)

(uniform stability) for every $\varepsilon>0$, there exists a
$\delta_{\varepsilon}>0$ such that every solution to $\mathbf{H}_{\delta}$
with $\left|\phi(0,0)\right|_{A}<\delta_{\varepsilon}$ satisfies
$\left|\phi(t,j)\right|_{A}<\varepsilon$ for all
$(t,j)\in\operatorname{dom}(\phi)$;

  2. (ii)

(uniform pre-attractivity) there exists some $\rho>0$ such that, for every
$\varepsilon>0$, there exist some $T>0$ such that, for every solution $\phi$
to $\mathbf{H}_{\delta}$, $|\phi(t,j)|_{A}<\varepsilon$ whenever
$|\phi(0,0)|_{A}<\rho$, $(t,j)\in\operatorname{dom}(\phi)$, and $t+j\geq T$.

######  Definition 2.7 (Basin of pre-attraction)

If a closed set $A\subseteq\mathbb{R}^{n}$ is UpAS for $\mathbf{H}_{\delta}$,
we further define the basin of pre-attraction of $A$, denoted by
$\mathfrak{B}_{\delta}(A)$, as the set of initial states $x\in\mathbb{R}^{n}$
such that every solution $\phi$ to $\mathbf{H}_{\delta}$ with $\phi(0,0)=x$ is
bounded and, if it is complete, then also converges to the set $A$, i.e.,
$\lim_{t+j\rightarrow\infty}|\phi(t,j)|_{A}=0$.

We define two closely-related properties of our interests in the following
definitions.

######  Definition 2.8 (Stability with safety guarantee)

Let $\mathcal{X}_{0},U,A\subseteq\mathbb{R}^{n}$ and $A$ is a closed set. We
say that $\mathbf{H}_{\delta}$ satisfies a stability with safety guarantee
specification $(\mathcal{X}_{0},U,A)$ if

  1. (i)

(pre-asymptotic stability w.r.t. $A$) the set $A$ is UpAS for
$\mathbf{H}_{\delta}$ and $\mathcal{X}_{0}\subseteq\mathfrak{B}_{\delta}(A)$;

  2. (ii)

(safety w.r.t. $U$) $\operatorname{rge}(\phi)\cap U=\emptyset$ for all
$\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(\mathcal{X}_{0})$.

######  Definition 2.9 (Reach-avoid-stay specification)

Let $\mathcal{X}_{0},U,\mathfrak{I}\subseteq\mathbb{R}^{n}$. We say that
$\mathbf{H}_{\delta}$ satisfies a reach-avoid-stay specification
$(\mathcal{X}_{0},U,\mathfrak{I})$ if

  1. (i)

(reach and stay w.r.t. $\mathfrak{I}$) there exists some $T\geq 0$ such that
$\mathcal{R}^{\delta}_{\geq T}(\mathcal{X}_{0})\subseteq\mathfrak{I}$;

  2. (ii)

(safety w.r.t. $U$) $\operatorname{rge}(\phi)\cap U=\emptyset$ for all
$\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(\mathcal{X}_{0})$.

##  3 Connection between Stability with Safety Guarantees and Reach-avoid-stay
Specifications

###  3.1  Stability with safety implies reach-avoid-stay

Throughout this section, we suppose that $\mathbf{H}_{\delta}$ satisfies a
stability with safety guarantee specification $(\mathcal{X}_{0},U,A)$ for some
fixed $\delta\geq 0$.

We first show some basic properties of solutions to $\mathbf{H}_{\delta}$ with
a fixed $\delta\geq 0$. The following proposition combines the results from
[24, Proposition 7.4, Lemma 7.8].

###### Proposition 3.10

Given a hybrid system $\mathbf{H}_{\delta}$, let $A\subseteq\mathbb{R}^{n}$ be
a compact set that is uniform stable for $\mathbf{H}_{\delta}$ (condition (i)
of Definition 2.6 holds). Suppose $K\subseteq\mathfrak{B}_{\delta}(A)$ is
compact. Then

  1. (i)

$\mathfrak{B}_{\delta}(A)$ is open and $A\subseteq\mathfrak{B}_{\delta}(A)$;

  2. (ii)

For every $\varepsilon>0$, there exists some $T=T(\varepsilon)>0$ such that
$|\phi(t,j)|_{A}\leq\varepsilon$ for all
$\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(K)$ and
$(t,j)\in\operatorname{dom}(\phi)$ with $t+j\geq T$;

  3. (iii)

$A\cup\mathcal{R}(K)$ is a compact subset of $\mathfrak{B}_{\delta}(A)$.

By (ii) of Proposition 3.10, the uniform attraction for solutions to
$\mathbf{H}_{\delta}$, the reach-avoid-stay property can be shown
straightforwardly. The statement is given in the following proposition.

###### Proposition 3.11

Let $A,\mathcal{X}_{0}\subseteq\mathbb{R}^{n}$ be compact sets. Suppose that
$\mathbf{H}_{\delta}$ satisfies a stability with safety guarantee
specification $(\mathcal{X}_{0},U,A)$. Then for every $\varepsilon>0$, the
system $\mathbf{H}_{\delta}$ also satisfies the reach-avoid-stay specification
$(\mathcal{X}_{0},U,A+\varepsilon\mathcal{B})$.

###  3.2 The converse side

Throughout this subsection, we suppose that $\mathbf{H}_{\delta}$ satisfies a
reach-avoid-stay specification $(\mathcal{X}_{0},U,\mathfrak{I})$. We make an
additional assumption on the local Lipschitz property of $F$ and $G$ to prove
the converse connection.

######  Definition 3.12 (Locally Lipschitz set-valued maps)

Let $\mathcal{O}\subseteq\mathbb{R}^{n}$ be an open set. A set-valued flow map
$F$ is also locally Lipschitz on $\mathcal{O}$; that is, for each
$x\in\mathcal{O}$, there exists a neighborhood $\mathcal{N}\subset\mathcal{O}$
of $x$ and an $L>0$ such that for any $x_{1},x_{2}\in\mathcal{N}$,

$F(x_{1})\subseteq F(x_{2})+L|x_{2}-x_{1}|\mathcal{B}.$

The following fact is a direct consequence of $F$ being locally Lipschitz [31,
Lemma 9].

###### Lemma 3.13

If $F:\mathcal{O}\rightrightarrows\mathbb{R}^{n}$ is locally Lipschitz, then
for any compact subset $K\subseteq\mathcal{O}$ there exists an $L_{K}>0$ such
that for any $x_{1},x_{2}\in K$, we have

$F(x_{1})\subseteq F(x_{2})+L_{K}|x_{2}-x_{1}|\mathcal{B}.$

###### Assumption 3.14

We assume in this section that $F$ and $G$ in (2) are locally Lipschitz on
some open subset of $C$ and $D$ respectively.

######  Lemma 3.15 (Perturbed solutions)

For any $\delta>0$, fix a $\delta^{\prime}\in[0,\delta)$ and a $\tau>0$. Let
$T\geq\tau$ and $K\subseteq\mathbb{R}^{n}$ be a compact set such that
$K\cap(C_{\delta}\cup D_{\delta})\neq\emptyset$. Then there exists an
$r=r(K,\tau,\delta^{\prime},\delta)>0$ such that for every solution
$\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta^{\prime}}(K)$ with
$\phi(t^{\prime},j^{\prime})\in K$ for all
$(t^{\prime},j^{\prime})\in\operatorname{dom}(\phi)$ and
$t^{\prime}+j^{\prime}\leq T$, and for all $x\in\phi(0,0)+r\mathcal{B}$, there
exists a $\psi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x)$ with
$\operatorname{dom}(\psi)=\operatorname{dom}(\phi)$ and

$\psi(t,j)=\phi(t,j),\;\;t+j=T.$ (3)

Proof  We suppose the total number of jumps before $T$ is $N$, thereby
$N\in[0,T]$. Now, set

$\psi(t^{\prime},j^{\prime})=\phi(t^{\prime},j^{\prime})+\left(1-\frac{t^{\prime}+j^{\prime}}{T}\right)\cdot(\psi(0,0)-\phi(0,0))$

for all $(t^{\prime},j^{\prime})\in\operatorname{dom}(\phi)$ and
$t^{\prime}+j^{\prime}\in[0,T]$. Then the constructed $\psi$ satisfies (3) and

$\left|\psi(t^{\prime},j^{\prime})-\phi(t^{\prime},j^{\prime})\right|\leq|\psi(0,0)-\phi(0,0)|\leq
r.$

In particular, for $N>0$, for each jump $j^{\prime}\in\\{0,1,\cdots,N-1\\}$ at
the end point $t_{j}^{\prime}$ of $I^{j^{\prime}}$, we have

$|\psi(t_{j}^{\prime},j^{\prime}+1)-\phi(t_{j}^{\prime},j^{\prime}+1)|\leq r.$

Similarly, suppose $N<T$ (i.e., flows exist), then for any fixed
$j^{\prime}\in\\{0,1,\cdots,N\\}$ and $t^{\prime}\in I^{j^{\prime}}$, we have

$\left|\dot{\psi}(t^{\prime},j^{\prime})-\dot{\phi}(t^{\prime},j^{\prime})\right|\leq\frac{1}{T}\left|\psi(0,0)-\phi(0,0)\right|=\frac{r}{T}.$

We show that this $\psi$ is a solution to $\mathbf{H}_{\delta}$. On the flow
set $C_{\delta}$, let $\widehat{C}:=C_{\delta}\cap(K+r\mathcal{B})$. Then for
$x\in\widehat{C}$, for all $t^{\prime}\in I^{j^{\prime}}$, we have

$\begin{split}\dot{\psi}(t^{\prime},j^{\prime})\subseteq&\dot{\phi}(t^{\prime},j^{\prime})+\frac{r}{T}\mathcal{B}\subseteq
F(\phi(t^{\prime},j^{\prime}))+\left(\delta^{\prime}+\frac{r}{T}\right)\mathcal{B}\\\
\subseteq&F(\psi(t^{\prime},j^{\prime}))+\left(\delta^{\prime}+\frac{r}{T}\right)\mathcal{B}+L_{\widehat{C}}|\psi(t^{\prime},j^{\prime})-\phi(t^{\prime},j^{\prime})|\mathcal{B}\\\
\subseteq&F(\psi(t^{\prime},j^{\prime}))+\left(\delta^{\prime}+\frac{r}{T}+rL_{\widehat{C}}\right)\mathcal{B}\\\
\subseteq&F(\psi(t^{\prime},j^{\prime}))+\left(\delta^{\prime}+\frac{r}{\tau}+rL_{\widehat{C}}\right)\mathcal{B},\end{split}$

where the constant $L_{\widehat{C}}$ in line 4 of the above inclusions is
obtained by Lemma 3.13.

Similarly, for each end point $t^{\prime}$ of some $I^{j^{\prime}}$, the jump
should satisfy

$\psi(t^{\prime},j^{\prime}+1)\subseteq
G(\psi(t^{\prime},j^{\prime}))+\left(\delta^{\prime}+r+rL_{\widehat{D}}\right)\mathcal{B},$

where $\widehat{D}:=D_{\delta}\cap(K+r\mathcal{B})$ and $L_{\widehat{D}}$ is
obtained based on Lemma 3.13 for $G$.

Now we are able to bound the above by $\delta$ such that $\psi$ is a solution
to $\mathbf{H}_{\delta}$. The $r$ can be selected accordingly such that all of
the followings are satisfied: $r\leq\delta-\delta^{\prime}$,
$\frac{r}{\tau}+\delta^{\prime}+rL_{\widehat{C}}\leq\delta$ and
$r+\delta^{\prime}+rL_{\widehat{D}}\leq\delta$.

Note that the above choice of $r$ should work for every possible case: the
extreme cases when only flows ($N=0$) or jumps ($N=T$) happen, as well as the
mixed flow/jump case ($N\in(0,T)$).

###### Remark 3.16

The above result shows that for any compact solution $\phi$ to
$\mathbf{H}_{\delta^{\prime}}$ (that exists till $t+j=\tau$), there exists a
solution $\psi$ to a slightly more perturbed system $\mathbf{H}_{\delta}$ such
that the endpoints of $\phi$ and $\psi$ are related within some time period.
The construction and estimation rely on the local Lipschitz continuity of $F$
and $G$. The proof states that no matter how conservative the estimation is,
we are able to find the small neighborhood with radius $r$ such that for any
initial condition within $\phi(0,0)+r\mathcal{B}$, there exists a $\psi$ as a
solution to $\mathbf{H}_{\delta}$ converging to $\phi$ within finite time. The
requirement that $\delta^{\prime}$ should be strictly less than $\delta$ is
necessary. Unlike the robustness concept given in [24, Lemma 7.37], the
perturbed systems $\mathbf{H}_{\delta}$ need inflation of $C$ and $D$ whose
intensities increase as $\delta$ increases. This subtle difference is in
consideration of when $\phi(0,0)\in\partial(C_{\delta^{\prime}}\cup
D_{\delta^{\prime}})$ whilst the constructed $\psi$ is still well posed.

Applying the preceding results, we show in the next proposition a hybrid-
system version of [22, Proposition 17]. The proof is completed in Appendix.

###### Proposition 3.17

Any nonempty, compact, forward pre-invariant set $A$ for $\mathbf{H}_{\delta}$
is UpAS for $\mathbf{H}_{\delta^{\prime}}$ with any
$\delta^{\prime}\in[0,\delta)$.

The existence of such a nonempty, compact, and forward pre-invariant set for
$\mathbf{H}_{\delta}$ is guaranteed by the following proposition.

######  Proposition 3.18 (Existence of compact invariant set)

Suppose that $\mathfrak{I}$ is compact and $\mathcal{X}_{0}$ is nonempty.
Suppose that $\mathbf{H}_{\delta}$ satisfies a reach-avoid-stay specification
$(\mathcal{X}_{0},U,\mathfrak{I})$. Then the set

$A=\left\\{x\in\mathfrak{I}:\forall\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x),\operatorname{rge}(\phi)\subseteq\mathfrak{I}\right\\}$
(4)

is nonempty, compact, and forward pre-invariant for $\mathbf{H}_{\delta}$.

To prove Proposition 3.18, we need the following lemma.

###### Lemma 3.19

Let the hypothesis in Proposition 3.18 be satisfied. Let $x_{0}\in
A\subseteq\mathfrak{I}$ be fixed. Then for every $\varepsilon>0$ and $\tau\geq
0$, there exists $\kappa>0$ such that, for every solution
$\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x_{0}+\kappa\mathcal{B})$ there
exists a solution $\psi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x_{0})$ such that
$\phi$ and $\psi$ are $(\tau,\varepsilon)$-close.

Proof  Without loss of generality, we assume that $\varepsilon$ and $\tau$ are
arbitrarily small such that $x_{0}+\kappa\mathcal{B}\subseteq\mathfrak{I}$. By
the reach-avoid-stay property of $\mathbf{H}_{\delta}$, the solution starting
from $\mathfrak{I}$ should be either eventually bounded or complete. Suppose
the statement were to fail, then for some arbitrarily small $\varepsilon$ and
$\tau$, for each $n\in\mathbb{N}$ and
$\phi_{n}\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x_{0}+1/n\mathcal{B})$ with
$x_{0}+1/n\mathcal{B}\subseteq\mathfrak{I}$, there exists no solution
$\psi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x_{0})$ is
$(\tau,\varepsilon)$-close to $\phi_{n}$. However, $\\{\phi_{n}\\}_{n}$ is
(locally eventually) bounded. By [24, Theorem 6.1], we can extract a
subsequence, still denoted by $\\{\phi_{n}\\}_{n}$, that is graphically
convergent to some $\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x)$. This
implies that there exists some sufficiently large $n$ such that $\phi_{n}$ and
$\phi$ are $(\tau,\varepsilon)$-close as a consequence of graphical
convergence of bounded sequences, which leads to a contradiction.
Proof of Proposition 3.18: By Definition 2.9, there exists some $T\geq 0$ such
that $\mathcal{R}_{\geq T}^{\delta}(\mathcal{X}_{0})\subseteq\mathfrak{I}$. It
is easy to verify that for any $x\in\mathcal{R}_{\geq
T}^{\delta}(\mathcal{X}_{0})\subseteq\mathfrak{I}$, $x\in\mathfrak{I}$, and
for all $\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x)$, we have
$\phi(t,j)\in\mathcal{R}_{\geq T}^{\delta}(\mathcal{X}_{0})$ for all
$(t,j)\in\operatorname{dom}(\phi)$. This shows that $A$ is nonempty. The
forward pre-invariance is verified by setting $T=0$ and
$\mathcal{X}_{0}\subseteq\mathfrak{I}$.

It suffices to show the closedness of $A$, which will imply the compactness
due to the boundedness assumption on $\mathfrak{I}$. Pick any sequence
$\left\\{x_{n}\right\\}_{n}\subseteq A$ such that $x_{n}\rightarrow x$. Then
for all $\phi_{n}\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x_{n})$, we have
$\operatorname{rge}(\phi_{n})\subseteq\mathfrak{I}$ and hence bounded. Suppose
that $x\notin A$, then there exists a
$\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x)$ such that
$\phi(t,j)\notin\mathfrak{I}$ for some $(t,j)\in\operatorname{dom}(\phi)$.
Select sufficiently small $\tau$ and $\varepsilon$ as in Lemma 3.19, then
there exists some $\kappa=\kappa(\tau,\varepsilon)>0$ and sufficiently large
$n\in\mathbb{N}$ (with $x\in x_{n}+\kappa\mathcal{B}$) such that
$\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x_{n}+\kappa\mathcal{B})$. However,
by Lemma 3.19, there exists a solution
$\phi_{n}\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x_{n})$ such that $\phi$ and
$\phi_{n}$ are arbitrarily $(\tau,\varepsilon)$-close. Since
$\mathbb{R}^{n}\setminus{\mathfrak{I}}$ is open, we have
$\phi_{n}(s,j)\in\mathbb{R}^{n}\setminus{\mathfrak{I}}$ for some $s+j\leq\tau$
with $|t-s|<\varepsilon$. This contradicts the forward pre-invariance property
of $\phi_{n}$. Hence, $x\in A$ and $A$ depicts compactness.

Combining Proposition 3.17 and Proposition 3.18, we immediately obtain the
following connection between reach-avoid-stay specifications and stability
with safety guarantees.

###### Proposition 3.20

Let Assumption 3.14 be satisfied. Let $\mathcal{X}_{0}$ be a nonempty set and
$\mathfrak{I}$ be a compact set. Suppose that $\mathbf{H}_{\delta}$ satisfies
a reach-avoid-stay specification $(\mathcal{X}_{0},U,\mathfrak{I})$. Then
there exists a compact set $A\subseteq\mathfrak{I}$ such that any less
perturbed system $\mathbf{H}_{\delta^{\prime}}$ with
$\delta^{\prime}\in[0,\delta)$ satisfies the stability with safety guarantee
specification $(\mathcal{X}_{0},U,A)$.

##  4 Lyapunov-Barrier Functions for Reach-Avoid-Stay Specifications

In this section, we provide Lyapunov-barrier characterizations for stability
with safety guarantee specifications as well as reach-avoid-stay
specification. In particular, such characterizations are (robustly) complete
in the sense that Lyapunov-barrier functions exist based on the specified
dynamical behavior of the solutions.

We focus on the Lyapunov-barrier functions for stability with safety
guarantees, the result for reach-avoid-stay comes after the connection given
in Proposition 3.20. Since the uniform asymptotic stability or reachability of
a closed set strongly relies the set initial conditions and may not hold
globally, the point-to-set distance becomes inadequate on the topology of
basin of pre-attraction. We use a proper indicator to characterize the
distance instead.

######  Definition 4.21 (Proper indicator)

Let $A\subseteq\mathbb{R}^{n}$ be a compact set and
$\mathfrak{O}\subseteq\mathbb{R}^{n}$ be an open set containing $A$. A
continuous function $\omega:\mathfrak{O}\rightarrow\mathbb{R}_{\geq 0}$ is
said to be a proper indicator for $A$ on $\mathfrak{O}$ if

  1. (i)

$\omega(x)=0\iff x\in A$;

  2. (ii)

$\lim_{n\rightarrow\infty}\omega(x_{n})=\infty$ for any sequence
$\left\\{x_{n}\right\\}_{n}\subseteq\mathfrak{O}$ such that either
$x_{n}\rightarrow p\in\partial\mathfrak{O}$ or $|x_{n}|\rightarrow\infty$ when
$n\rightarrow\infty$.

We also refine the basin of pre-attraction and introduce the following
constraint set.

######  Definition 4.22 (Basin of pre-attraction with safety)

The extracted basin of pre-attraction with safety is a subset of
$\mathfrak{B}_{\delta}(A)$ defined by

$\widehat{\mathfrak{B}}_{\delta}(A):=\\{x\in\mathfrak{B}_{\delta}(A):\forall\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x),\;\;\operatorname{rge}(\phi)\cap
U=\emptyset\\},$ (5)

where $A,U$ are given in the specification $(\mathcal{X}_{0},U,A)$.

The following lemma verifies basic topological properties of
$\widehat{\mathfrak{B}}_{\delta}(A)$, which will be later utilized for the
Lyapunov-barrier function theorems.

###### Lemma 4.23

Suppose that $A$ is compact, $U$ is closed, and $A\cap U=\emptyset$. If
$\mathbf{H}_{\delta}$ satisfies the stability with safety guarantee
specification $(\mathcal{X}_{0},U,A)$, then

  1. (i)

$\mathcal{X}_{0}\subseteq\widehat{\mathfrak{B}}_{\delta}(A)\subseteq\mathfrak{B}_{\delta}(A)$;

  2. (ii)

$\widehat{\mathfrak{B}}_{\delta}(A)$ is open and forward pre-invariant.

Proof  The first claim can be easily verified by Definition 2.8 and 4.22. The
forward pre-invariance of (ii) comes after Definition 2.4. It suffices to show
that $\widehat{\mathfrak{B}}_{\delta}(A)$ is also open given $U$ is closed.

Suppose the opposite, then pick any $x\in\widehat{\mathfrak{B}}_{\delta}(A)$.
There exists a sequence of points
$\left\\{x_{n}\right\\}_{n}\subseteq\mathfrak{B}_{\delta}\setminus\widehat{\mathfrak{B}}_{\delta}(A)$
with $x_{n}\rightarrow x$. Note that for each $n$, there exists
$\phi_{n}\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x_{n})$ that is either bounded
or complete with convergence to $A$. Either way, we have $\phi_{n}$ bounded
for each $n$ by Proposition 3.10. By [24, Theorem 6.1], we can extract a
subsequence, still denoted by $\left\\{\phi_{n}\right\\}_{n}$, that is
graphically convergent. By Assumption 2.2, the limit satisfies
$\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x)$, and is again either bounded or
complete with convergence to $A$.

Suppose the graphical limit $\phi$ is complete. Let $r>0$ be given by
condition (ii) from Definition 2.6. Pick $\varepsilon<r$ such that
$(A+\varepsilon\mathcal{B})\cap U=\emptyset$. Choose
$\delta_{\varepsilon}\leq\varepsilon$ according to condition (i) of Definition
2.6 by the uniform stability. Then there exists a
$T=T(\delta_{\varepsilon})>0$ such that
$|\widehat{\phi}(t,j)|_{A}\leq\delta_{\varepsilon}$ for all
$\widehat{\phi}\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x)$ and
$t+j\geq\operatorname{dom}(\widehat{\phi})$ with $t+j\geq T$. Note that the
reachable set $\mathcal{R}_{\leq T}^{\delta}(x)$ is compact and we can select
some $\varepsilon^{\prime}<\varepsilon/2$ such that $(\mathcal{R}_{\leq
T}^{\delta}(x)+\varepsilon^{\prime}\mathcal{B})\cap U=\emptyset$. Let
$\varepsilon^{\prime\prime}=\min\\{\varepsilon^{\prime},\delta_{\varepsilon}\\}$.
As the consequence of graphical convergence, there exists a sufficiently large
$n\in\mathbb{N}$ such that for each $\tau>0$, the solution $\phi_{n}$ and
$\phi$ are $(\tau,\varepsilon^{\prime\prime})$-close. No matter $\tau\geq T$
or $\tau<T$, we can verify by the choice of $\varepsilon^{\prime\prime}$ and
$n$ that
$\phi_{n}(t,j)\in(\mathcal{R}^{\delta}(x)+\varepsilon^{\prime}\mathcal{B})\cup(A+\varepsilon\mathcal{B})$
for all $(t,j)\in\operatorname{dom}(\phi_{n})$, which contradicts the property
of $\phi_{n}\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x_{n})$ with
$x_{n}\in\mathfrak{B}_{\delta}(A)\setminus\widehat{\mathfrak{B}}_{\delta}(A)$.
For the case that $\phi$ is bounded, we can proceed and show the contradiction
by a similar way. Combining the above, we have
$\widehat{\mathfrak{B}}_{\delta}(A)$ is open.

The following result shows that, based on the reachable region of solutions
with stability and safety guarantees, a single Lyapunov-like function exists
which is also effective as a barrier function to guarantee the safety.

###### Theorem 4.24

Suppose that $A$ is compact, $U$ is closed, and $A\cap U=\emptyset$. Then the
following two statements are equivalent:

  1. (i)

$\mathbf{H}_{\delta}$ satisfies the stability with safety guarantee
specification $(\mathcal{X}_{0},U,A)$.

  2. (ii)

There exists an open and forward pre-invariant set $\mathfrak{O}$ such that
$(A\cup\mathcal{X}_{0})\subseteq\mathfrak{O}$ and $\mathfrak{O}\cap
U=\emptyset$, a smooth function $V:\mathfrak{O}\rightarrow\mathbb{R}_{\geq 0}$
and class $\mathcal{K}_{\infty}$ functions $\alpha_{1},\alpha_{2}$ such that,

$\alpha_{1}(\omega(x))\leq V(x)\leq\alpha_{2}(\omega(x)),\;\;\forall
x\in(C_{\delta}\cup D_{\delta}\cup G(D_{\delta}))\cap\mathfrak{O},$ (6)
$\nabla V(x)\cdot f\leq-V(x),\;\;\forall x\in
C_{\delta}\cap\mathfrak{O},\;f\in F(x)+\delta\mathcal{B},$ (7)

and

$V(g)\leq V(x)/e,\;\;\forall x\in D_{\delta}\cap\mathfrak{O},\;g\in
G(x)+\delta\mathcal{B},$ (8)

where $\omega$ is a proper indicator for $A$ on $\mathfrak{O}$.

Proof  (i) $\implies$ (ii): By [24, Corollary 7.33], the existence of smooth
Lyapunov-like function holds on forward pre-invariant open subsets of
$\mathfrak{B}_{\delta}(A)$. The result follows immediately by Lemma 4.23 for
$\mathfrak{O}=\widehat{\mathfrak{B}}_{\delta}(A)$.

(ii) $\implies$ (i): By a standard Lyapunov argument for hybrid systems, we
are able to show that for any $\phi$ to $\mathbf{H}_{\delta}$ with
$\phi(0,0)\in\mathfrak{O}$,

$V(\phi(t,j))\leq V(\phi(0,0))e^{-(t+j)/3},$

which implies the forward pre-invariance of $\mathfrak{O}$ and the UpAS
property of any $\phi$ starting within $\mathfrak{O}$. Now that
$\mathfrak{O}\cap U=\emptyset$, for any
$\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(\mathcal{X}_{0})$ with
$\mathcal{X}_{0}\subseteq\mathfrak{O}$, we have $\operatorname{rge}(\phi)\cap
U=\emptyset$, which implies the safety.

###### Remark 4.25

Note that to use [24, Corollary 7.33], we need to verify that the UpAS holds
for the following system of the following modifications:

$\displaystyle\dot{x}\in F_{\rho}(x),\;\;\;\;\;x\in(C_{\delta})_{\rho},$ (9a)
$\displaystyle x^{+}\in G_{\rho}(x),\;\;\;x\in(D_{\delta})_{\rho},$ (9b)

where

$(C_{\delta})_{\rho}=\left\\{x\in\mathbb{R}^{n}:(x+\rho(x)\mathcal{B}\cap
C_{\delta}\neq\emptyset\right\\},$
$F_{\rho}(x)=\overline{\operatorname{con}}F((x+\rho(x)\mathcal{B})\cap
C_{\delta})+(\rho(x)+\delta)\mathcal{B},$
$(D_{\delta})_{\rho}=\left\\{x\in\mathbb{R}^{n}:(x+\rho(x)\mathcal{B}\cap
D_{\delta}\neq\emptyset\right\\},$

and $G_{\rho}(x)=\left\\{v\in\mathbb{R}^{n}:v\in
g+(\rho(g)+\delta)\mathcal{B}\right\\}$, for $g\in G(x+\rho(x)\mathcal{B})\cap
D_{\delta}$. However, this is guaranteed by Assumption 2.2 for each
$\delta\geq 0$.

The proof for [24, Corollary 7.33] relies on the conversion from UpAS to the
$\mathcal{KL}$ pre-asymptotic stability222The definition is omitted. We kindly
refer readers to [32, Definition 31] for more details. based on changing the
basin of attraction. In contrast, for robust systems driven by differential
equations with $F$ being a single-valued function, [32, Proposition 10]
provides a more explicit way of constructing the $\mathcal{KL}$-function
$\beta$ such that $\omega(\phi(t))\leq\beta(\omega(x),t)$ for all solutions
with initial conditions $x\in\mathfrak{O}$. The argument is based on the
reachable set properties as well as a connection between the solution-to-set
distance and the proper indicator. The extension of the explicit construction
from [32, Proposition 10] to the general hybrid systems should be similar.

By the connection obtained in Section 3, the following results follow.

###### Corollary 4.26

Suppose that $A,\mathcal{X}_{0}$ are compact sets and (ii) of Theorem 4.24
holds. Then $\mathbf{H}_{\delta}$ satisfies the reach-avoid-stay specification
$(\mathcal{X}_{0},U,A+\varepsilon\mathcal{B})$ for any $\varepsilon>0$.

###### Theorem 4.27

Let Assumption 3.14 be satisfied. Suppose that $\mathfrak{I}$ is compact, $U$
is closed and $\mathfrak{I}\cap U=\emptyset$. Suppose that
$\mathbf{H}_{\delta^{\prime}}$ satisfies the reach-avoid-stay specification
$(\mathcal{X}_{0},U,\mathfrak{I})$. Then there exists a compact set
$A\subseteq\mathfrak{I}$ such that (ii) of Theorem 4.24 holds for any
$\mathbf{H}_{\delta}$ with $\delta\in[0,\delta^{\prime})$.

The above constructed Lyapunov functions for the stability with safety
guarantees and reach-avoid-stay specifications play an implicit role as a
barrier function. As though it appears more succinct to have both Lyapunov and
barrier functions merged into one single Lyapunov function, it may not be easy
to design in practice. We provide an equivalent characterization as in Theorem
4.24 with separate Lyapunov-barrier functions to complete this section. The
separate Lyapunov-barrier functions for reach-avoid-stay specifications are
omitted due to the similarity.

###### Theorem 4.28

Suppose that $A$ is compact, $U$ is closed and $A\cap U=\emptyset$. If there
exists an open set $\mathfrak{O}$ such that
$A\cup\mathcal{X}_{0}\subseteq\mathfrak{O}$, a smooth function
$V:\mathfrak{O}\rightarrow\mathbb{R}_{\geq 0}$ satisfying

  1. (i)

there exist $\alpha_{1},\alpha_{2}\in\mathcal{K}$ and a continuous positive
function $\varrho$ such that

$\displaystyle\alpha_{1}(|x|_{A})\leq V(x)\leq\alpha_{2}(|x|_{A}),\;\;\forall
x\in(C_{\delta}\cup D_{\delta}\cup G(D_{\delta}))\cap\mathfrak{O},$ (10)
$\nabla V(x)\cdot f\leq-\varrho(|x|_{A}),\;\;\forall x\in C_{\delta},\;f\in
F(x)+\delta\mathcal{B},$ (11) $V(g)-V(x)\leq-\varrho(|x|_{A}),\;\;\forall x\in
D_{\delta},\;g\in G(x)+\delta\mathcal{B};$ (12)

and $B:\mathbb{R}^{n}\rightarrow\mathbb{R}$ that is smooth in
$C\cap\mathfrak{O}$ such that

  1. (ii)

the set $S:=\left\\{x\in\mathbb{R}^{n}:B(x)\geq
0\right\\}\subseteq\mathfrak{O}$ and $\mathcal{X}_{0}\subseteq S$;

  2. (iii)

$x\in U$ implies $B(x)<0$;

  3. (iv)

$\nabla B(x)\cdot f\geq 0,\;\;\forall x\in C_{\delta}\cap\mathfrak{O},\;f\in
F(x)+\delta\mathcal{B},$ (13) $B(g)-B(x)\geq 0,\;\;\forall x\in
D_{\delta}\cap\mathfrak{O},\;g\in G(x)+\delta\mathcal{B},$ (14)

then $\mathbf{H}_{\delta}$ satisfies the stability with safety guarantee
specification $(\mathcal{X}_{0},U,A)$.

If $\mathcal{X}_{0}$ is also compact, then the converse side also holds, i.e.,
the existence of smooth $V$ and $B$ with conditions (i)-(iv) is necessary for
$\mathbf{H}_{\delta}$ satisfying the stability with safety guarantee
specification $(\mathcal{X}_{0},U,A)$.

Proof  For the sufficient part, we start with the stability. Note that by a
standard Lyapunov argument for hybrid systems, the existence of $V$ with
condition (i) is sufficient to guarantee the UpAS property of $A$ for
$\mathbf{H}_{\delta}$. The condition (ii)-(iv) of $B$ intends to separate the
set $S$ and $U$, such that all the solutions starting from $S$ will stay
within it.

We show formally the mechanism of $B$. Suppose the opposite, then there exists
some $x\in S$, a solution $\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(x)$, and
some hybrid time such that $B(\phi(t,j))<0$. Then we are able to define a
finite time

$\tau:=\sup\\{t+j\geq 0:\phi(t,j)\in S\\}.$

As a consequence, there exist $t^{\prime}$ and $j^{\prime}$ with
$t^{\prime}+j^{\prime}=\tau$ such that $B(\phi(t^{\prime},j^{\prime}))=0$.
Note that since the $\phi$ exists till $B(\phi(t,j))<0$. For a small
perturbation $\varepsilon$ of $t^{\prime}$, $\phi$ is either a flow such that
$t^{\prime}+\varepsilon\in I^{j^{\prime}}$, or triggers a jump such that
$t^{\prime}+\varepsilon\in I^{j^{\prime}+1}$. For the first case, since
$\mathfrak{O}$ is open, for arbitrary $\varepsilon>0$, we still have
$\phi(t^{\prime\prime},j^{\prime})\in C_{\delta}\cap\mathfrak{O}$ for almost
$t^{\prime\prime}\in[t^{\prime},t^{\prime}+\varepsilon]$. Thus, we have
$\dot{B}(\phi(t^{\prime\prime},j^{\prime}))=\nabla
B(\phi(t^{\prime\prime},j))\cdot f\geq 0$ for all $f\in
F(x)+\delta\mathcal{B}$ and almost all
$t^{\prime\prime}\in[t^{\prime},t^{\prime}+\varepsilon]$, which means
$t^{\prime\prime}+j^{\prime}\geq\tau$ but
$\phi(t^{\prime\prime},j^{\prime})\in S$. This contradicts the definition of
$\tau$. For the second case, by a similar argument, we have
$B(\phi(t^{\prime},j^{\prime}+1))\geq 0$, which also leads to a contradiction.
Hence $S$ is forward pre-invariant. This verifies condition (ii) of Definition
2.8.

A direct consequence of $B$ is that, for any
$\mathcal{X}_{0}\subseteq\mathfrak{O}$, any solution
$\phi\in\mathfrak{S}_{\mathbf{H}}^{\delta}(\mathcal{X}_{0})$ stays within $S$
and hence $\mathfrak{O}$. Condition (i) guarantees that
$\phi\in\mathfrak{B}_{\delta}(A)$. This verifies condition (i) of Definition
2.8.

Now we show the converse side. The existence of $V$ is derived from the
existing converse Lyapunov theorems given the UpAS property of the compact set
$A$. The construction of $B$ is also based on the compactness of $A$ and
$\mathcal{X}_{0}$. Let $c=\sup_{x\in\mathcal{X}_{0}}V(x)$. Then,
$\mathcal{X}_{0}\subseteq K:=\\{x\in\mathfrak{O}:V(x)\leq c\\}$.  We aim to
unite locally smooth functions of the form $B_{i}(x)=c-V(x)$ into a globally
smooth function $B$. The rest of the proof falls in the exact procedure as in
the proof of [22, Proposition 12]. We choose $c_{2}>c_{1}>c$ and let
$\mathfrak{O}_{i}=\\{x\in\mathfrak{O}:V(x)<c_{i}\\}$ for $i\in\\{1,2\\}$. Then
$\\{\mathfrak{O}_{1},\mathfrak{O}_{2}\setminus
K,\mathbb{R}^{n}\setminus\overline{\mathfrak{O}_{1}}\\}$ is an open cover of
$\mathbb{R}^{n}$. On these converings, let $B_{1}(x)=c-V(x)$ for
$x\in\mathfrak{O}_{1}$, $B_{2}(x)=c-V(x)$ for $x\in\mathfrak{O}_{2}\setminus
K$, and $B_{3}(x)=c-c_{1}$ for
$x\in\mathbb{R}^{n}\setminus\overline{\mathfrak{O}_{1}}$. The above functions
are defined to be $0$ elsewhere. Let ${\psi_{1},\psi_{2},\psi_{3}}$ be a
smooth partition of unity [33, p.43] subordinate to
$\\{\mathfrak{O}_{1},\mathfrak{O}_{2}\setminus
K,\mathbb{R}^{n}\setminus\overline{\mathfrak{O}_{1}}\\}$. Then,
$B(x)=\sum_{i=1}^{3}\psi_{i}(x)B_{i}(x)$ for $x\in\mathbb{R}^{n}$ can be
verified to satisfy condition (ii)-(iv).

###### Remark 4.29

For the sufficient part, condition (iv) intends to regulate the safe direction
of solutions on the entire open set $\mathfrak{O}$ rather than directly on its
subset $S:=\left\\{x\in\mathbb{R}^{n}:B(x)\geq 0\right\\}$. This condition
seems stronger but also necessary. Imposing condition (iv) on $S$ can only
guarantee the invariance of the interior of $S$, for counters examples see
e.g. [34, Remark 4].

###### Remark 4.30

The necessity of the existence of $B$ given the satisfaction of a stability
with safety guarantee specification $(\mathcal{X}_{0},U,A)$ is majorly based
on the compactness of reachable set from $\mathcal{X}_{0}$, which does not
intersect with $U$ by the a priori safety assumption. This compactness in turn
makes it easier to construct $B$ via the Lyapunov function $V$. The latest
converse barrier function theorems by [25, 26, 27], however, does not depend
on the boundedness of $\mathbb{R}^{n}\setminus U$, and hence does not require
the compactness of $\mathcal{X}_{0}$. The construction of barrier function
given the safety of robust systems relies on the ‘time-to-impact’ function
$B_{\mathcal{R}}$ w.r.t. the reachable set $\mathcal{R}$ of robust systems.
This $B_{\mathcal{R}}$ turns out to satisfy condition (ii) and (iii) of
Theorem 4.28 as well as a weaker certificate333Note that we have adapted the
notion to be consistent with the notation used in this paper.

$\nabla B\cdot f>0,\;\;\forall x\in\partial S,f\in F(x)+\delta\mathcal{B}.$

The results in [25, 26, 27] are of great theoretical interest in the sense of
constructing barrier functions with relaxed topological requirement and
barrier conditions. Their construction relies on the seemingly less intuitive
time-to-impact functions, whereas our approach aims to unify Lyapunov and
barrier functions. It would be interesting to investigate in future work
whether the Lyapunov-barrier approach can be extended to handle unbounded
reachable sets.

##  5 Examples

We provide two examples in this subsection to validate our results.

###  5.1 Bouncing ball

As a classical mechanical system with impulse-momentum change, the model of
bouncing balls is frequently used to illustrate dynamical behaviors of hybrid
systems. We model a tennis ball as a point-mass, and consider dropping it from
a fixed height with a constant horizontal speed. The vertical direction is
forced by the gravity. As the ball hits the horizontal surface, the
instantaneous vertical velocity is reversed with a small dissipation of
energy.

To describe the hybrid dynamics, the state of the ball is given as

$\mathfrak{x}=(x,y,z)^{T}\in\mathbb{R}^{3},$

where $x$ is the horizontal position, $y$ represents the height above the
surface, and $z$ is the vertical velocity. The flow set is given as
$C=\\{\mathfrak{x}:y>0\;\text{or}\;y=0,z\geq 0\\}.$ We consider the flow444As
in [24], it is natural to set $f(\mathbf{0})=\mathbf{0}$ regardless of the
noncontinuity at $\mathbf{0}$. as

$\dot{\mathfrak{x}}=f(\mathfrak{x}):=\begin{bmatrix}1\\\ z\\\
-a\end{bmatrix},\;\;\mathfrak{x}\in C,$

where $a=9.8$ is the acceleration due to the gravity. The jump set captures
the domain when the vertical velocity flips the sign, which is geiven as
$D=\\{\mathfrak{x}:y=0\;\text{and}\;z<0\\}.$ The jump dynamic is such that

$\mathfrak{x}^{+}=g(\mathfrak{x}):=\begin{bmatrix}x\\\ 0\\\ -\varsigma
z\end{bmatrix},\;\;\mathfrak{x}\in D,$

for some dissipation coefficient $\varsigma\in(0,1)$.

Now fix $\varsigma=0.8$, let the initial condition to be
$\mathfrak{x}(0)=(0,9,0.8)^{T}\in C$, and model a block (the unsafe set) by
$U:=\\{\mathfrak{x}:y>10\\}.$ We consider the target set as
$\mathfrak{I}:=\\{\mathfrak{x}:y\in[0,0.1]\\}.$

It can be shown analytically and numerically (see Figure 1) that the system
satisfies the reach-avoid-stay specification
$(\\{\mathfrak{x}(0)\\},U,\mathfrak{I})$. We now validate the existence of
Lyapunov-barrier functions $(V,B)$.

Figure 1: Snapshot of bouncing ball in $xy$-plane.

Note that, the function

$V(\mathfrak{x})=\left(1+\frac{1-\varsigma^{2}}{\pi(1+\varsigma^{2})}\arctan(z)\right)\cdot\left(\frac{1}{2}z^{2}+ay\right)$

has been verified in [24, Example 3.19] to be a valid Lyapunov function w.r.t.
the set $\\{\mathfrak{x}:y=0\\}$. It suffices to find valid candidate of the
barrier function $B$. Consider a sigmoid function

$\sigma(x)=\frac{1}{1+\exp(-5x)}$

and let

$B(\mathfrak{x})=\frac{1}{2}\sigma(x)-y-\frac{1}{2a}z^{2}+9.5.$

It can be verified that $B(\mathfrak{x})<0$ for $\mathfrak{x}\in U$,

$\nabla B(\mathfrak{x})\cdot
f(\mathfrak{x})=\frac{1}{2}\sigma(x)(1-\sigma(x))-z+z\geq
0,\;\;\mathfrak{x}\in C,$

and

$B(g(\mathfrak{x}))-B(\mathfrak{x})=\frac{1}{2a}(z^{2}-\varsigma^{2}z^{2})>0,\;\;\mathfrak{x}\in
D,$

Therefore, the above $B(\mathfrak{x})$ is a valid barrier function. Let
$S:=\\{\mathfrak{x}:B(\mathfrak{x})\geq 0\\}$ be the set as in Theorem 4.28,
then it is also clear that $\mathfrak{x}(0)\in S$. The evolution of the state
$\mathfrak{x}\in\mathbb{R}^{3}$ as well as the graph of barrier function $B$
are provided in Figure 2. It can be seen that for all $t\geq 0$,
$\mathfrak{x}(t)\in S$ and therefore remain safety w.r.t. $U$.

Figure 2: Solution of bouncing ball (the green dots) and barrier function $B$
(the grey surface) in $xyz$-plane.

###  5.2 Sample-and-hold control

In this example, we revisit the case study in [13, Section V] from the
perspective of hybrid system.

We consider the reduced Moore-Greitzer ODE model with an additive control
input $[v,0]^{T}$ and no extra perturbations:

$\dfrac{d}{dt}\begin{bmatrix}\Phi(t)\\\
\Psi(t)\end{bmatrix}=\begin{bmatrix}\frac{1}{\mathfrak{l}_{c}}(\psi_{c}-\Psi(t))\\\
\frac{1}{16\mathfrak{l}_{c}}\left(\Phi(t)-\gamma\sqrt{\Psi(t)}\right)\end{bmatrix}+\begin{bmatrix}v(t)\\\
0\end{bmatrix},$ (15)

where
$\psi_{c}=\mathfrak{a}+\iota\cdot[1+\frac{3}{2}\left(\frac{\Phi}{\Theta}-1\right)-\frac{1}{2}\left(\frac{\Phi}{\Theta}-1\right)^{3}]$,
and $\gamma$ is the throttle coefficient. The other parameters are as follows:

$\mathfrak{l}_{c}=8,\;\iota=0.18,\;\Theta=0.25,\;\mathfrak{a}=1.67\iota.$

As $\gamma$ decreases, surge instability occurs and generates a pumping
oscillation (Hopf-bifurcation) that can cause flameout and engine damage. The
physical meanings of variables, parameters and the description of this model
can be found in [13, Section V].

###### Problem 1

We aim to manipulate the throttle coefficient $\gamma$ and $v$ simultaneously
such that the state $(\Phi,\Psi)$ are regulated to satisfy reach-avoid-stay
specification $(\mathcal{X}_{0},U,\Gamma)$. We require that
$\gamma:\mathbb{R}_{\geq 0}\rightarrow[0.5,1]$ is time-varied with
$\gamma(0)\in[0.62,0.66]$ and $|\gamma(t+\tau)-\gamma(t)|\leq 0.01\tau$ for
any $\tau>0$. We define
$\mathcal{X}_{0}=\\{(\Phi_{e}(\gamma(0)),\Psi_{e}(\gamma(0)))\\}$ (i.e. a sub-
region of stable equilibrium points, also see [13, Fig. 1]); $\Gamma$ to be
the ball that centered at $\zeta=(0.4519,0.6513)$ with radius $r=0.003$, i.e.
$\Gamma=\zeta+r\mathcal{B}$;
$U=\\{(x,y):x\in(0.497,0.503),y\in(0.650,0.656)\\}$. We set
$v(t)\in\mathcal{U}=[-0.05,0.05]\cap\mathbb{R}$ for all $t$.

Note that, the system (15) can be rewritten as

$\dfrac{d}{dt}\begin{bmatrix}\Phi(t)\\\
\Psi(t)\end{bmatrix}=\begin{bmatrix}\frac{1}{\mathfrak{l}_{c}}(\psi_{c}-\Psi(t))\\\
\frac{1}{16\mathfrak{l}_{c}}\Phi(t)\end{bmatrix}+\begin{bmatrix}v(t)\\\
-\gamma(t)\sqrt{\Psi(t)}\end{bmatrix}.$ (16)

Let $\mathfrak{u}(t)=[v(t),\gamma(t)]^{T}$ and

$g(x(t))=\begin{bmatrix}1&0\\\ 0&-\sqrt{\Psi(t)}\end{bmatrix},$

then (16) fits in the general form of flow dynamics. We make a little abuse of
notation here to define $\mathcal{U}=[-0.05,0.05]\times[0.5,1]$.

Due to the issues of less frequent and inaccurate state measurement, the
errors inject into the closed-loop control system and may cause unsatisfactory
performance. We are motivated by the above issues to convert the system (16)
into a hybrid system. We then apply the conditions of the Lyapunov-barrier
functions in Theorem 4.28 to synthesize valid sample-and-hold controllers
aiming at fulfilling the task in Problem 1.

For simplicity, we define the state $\mathfrak{x}=(\Phi,\Psi)^{T}$ and the
control input $\mathfrak{u}=(v,\gamma)$. We write

$\tilde{f}(\mathfrak{x},u)=\begin{bmatrix}\frac{1}{\mathfrak{l}_{c}}(\psi_{c}-\Psi(t))\\\
\frac{1}{16\mathfrak{l}_{c}}\Phi(t)\end{bmatrix}+\begin{bmatrix}v(t)\\\
-\gamma(t)\sqrt{\Psi(t)}\end{bmatrix},$

which is the r.h.s. of (16).

We then introduce $\tau\in[0,0.5)$ as a timer variable and set

$\mathfrak{z}=\begin{bmatrix}\mathfrak{x}\\\ \mathfrak{u}\\\
\tau\end{bmatrix}\in\mathbb{R}^{2}\times\mathbb{R}^{2}\times\mathbb{R}.$

The flow set of the sample-and-hold hybrid system is given as
$C=\mathbb{R}^{2}\times\mathbb{R}^{2}\times[0,0.5)$, on which the flow
dynamics are such that

$\dot{\mathfrak{z}}=f(\mathfrak{z})=\begin{bmatrix}\tilde{f}(\mathfrak{x},\mathfrak{u})\\\
0\\\ 1\end{bmatrix},\;\;\mathfrak{z}\in C.$

The jumps happen when the timer is up to $0.5$ and decisions are made, i.e.,
$D=\mathbb{R}^{2}\times\mathbb{R}^{2}\times\\{0.5\\}$ and

$\mathfrak{z}^{+}=g(\mathfrak{z})=\begin{bmatrix}\mathfrak{x}\\\
\kappa(\mathfrak{x})\\\ 0\end{bmatrix},\;\;\mathfrak{z}\in D.$ (17)

We choose Lyapunov-barrier functions $(V,B)$ to be such that

  * (1)

$V(x)=\|x-\zeta\|^{2}$ for all $x\in D\setminus\\{\zeta\\}$,

  * (2)

and $B(x)=-\log\left(\frac{h(x)}{1+h(x)}\right)$ for
$h(x)=\|x-(0.500,0.653)\|_{\infty}-r$.

We then define a set of high-gain robust control policy as follows:

$\begin{split}\mathfrak{K}(x)=&\\{u\in\mathcal{U}:L_{f}V(x)+L_{g}V(x)u+V(x)\leq-\varsigma\;\text{and}\;L_{f}B(x)+L_{g}B(x)u\geq\varsigma,\;\forall
x\in D\\},\end{split}$ (18)

where $\varsigma>0$ is intended to compensate the error that is generated when
the same control input is imposed on the flow dynamics. Since $L_{f}V$,
$L_{g}V$, $L_{f}B$ and $L_{g}B$ are locally Lipschitz continuous, and the
quantity $|\mathfrak{x}(\tau)-\mathfrak{x}(0)|$ for any fixed
$\mathfrak{x}(0)\in D$ is locally bounded given
$\mathfrak{x}(\tau)=\mathfrak{x}(0)+\int_{0}^{\tau}\tilde{f}(\mathfrak{x}(s),u)ds$
and $\tau\in[0,0.05)$, it is clear that both

$\begin{split}&|L_{f}V(\mathfrak{x}(\tau))+L_{g}V(\mathfrak{x}(\tau))u+V(\mathfrak{x}(\tau))-L_{f}V(\mathfrak{x}(0))+L_{g}V(\mathfrak{x}(0))u+V(\mathfrak{x}(0))|\end{split}$

and

$|L_{f}B(\mathfrak{x}(\tau))+L_{g}B(\mathfrak{x}(\tau))u-L_{f}B(\mathfrak{x}(0))+L_{g}B(\mathfrak{x}(0))u|$

are locally bounded. We set the bound for both of the above quantities to be
$\varsigma$, such that for any
$\mathfrak{u}=\kappa(\mathfrak{x})\in\mathfrak{K}(\mathfrak{x})$ and
$\mathfrak{x}\in D$, then the Lyapunov-barrier conditions are satisfied in the
flow, i.e.,

$L_{f}V(\mathfrak{x})+L_{g}V(\mathfrak{x})u+V(\mathfrak{x})\leq
0,\;\forall\mathfrak{x}\in C,$

and

$L_{f}B(\mathfrak{x})+L_{g}B(\mathfrak{x})\mathfrak{u}\geq
0,\;\forall\mathfrak{x}\in C.$

This in turn guarantees the reach-avoid-stay property of the system.

In the numerical experiments, we empirically set $\varsigma=0.07$ and impose
an extra set of constraints for the control input as

$\begin{split}\mathcal{M}&:=\\{\gamma\in[0.5,1]:\gamma(0)\in[0.62,0.66],\;|\gamma(t+\tau)-\gamma(t)|\leq
0.01\tau,\;\forall\tau>0\\}.\end{split}$ (19)

The $\mathfrak{u}$ is selected such that the control effort

$|\mathfrak{u}(t)|^{2}+\frac{2\mathfrak{u}(t)}{\mathfrak{l}_{c}}(\psi_{c}-\Psi(t))+\left(\frac{1}{4\mathfrak{l}_{c}}(\Phi(t)-\gamma(t))\sqrt{\Psi(t)}\right)^{2}$
(20)

is minimized for each $\mathfrak{z}\in D$. The results are shown in Figure 3
and 4. It can be seen that given the robust correction in the decision making,
the high-gain controller can still fulfill the goal apart from the intensively
fluctuating trajectory along the $\Phi$ direction in between $t=20$ and
$t=80$.

Figure 3: Control signal $v$ and $\gamma$ solved by the quadratic programming
for the hybrid conversion of (16).

Figure 4: Phase portraits and evolution of $\Phi$ and $\Psi$ given the sample-
and-hold control signal $v$ and $\gamma$.

##  6 Conclusion

In this paper, we showed that under mild conditions, the connection can be
made, via a robustness argument, between stability with safety guarantees and
reach-avoid-stay specifications for robust hybrid systems driven by
differential and difference inclusions. We further extended the Lyapunov-
barrier function theorems to robust hybrid systems that satisfy stability with
safety guarantees and reach-avoid-stay specifications. Under the concept of
solutions to hybrid systems, as well as natural requirements on the
compactness of target set and the set of initial conditions, we showed that
the existence of Lyapunov-barrier functions is necessary to the two
specifications of our interests.

In particular, two versions of Lyapunov-barrier functions are provided and
discussed in Section 4. The single Lyapunov-like function that also plays a
role as a barrier function appears to be succinct but may be difficult to
design in practice. We discussed the construction of separate Lyapunov-barrier
functions in particular for stability with safety guarantee specifications.
Numerical simulations are provided to validate our results. It is interesting
to compare with the latest converse theorems on barrier functions for systems
driven by differential inclusions [25, 26, 27]. The mentioned reference
provides a construction based on time-to-impact functions w.r.t. the robust
reachable sets, which in turn to be qualified as barrier functions. In terms
of safety, this method allows us to consider relaxations for the topological
set-ups of target sets and the set of initial conditions, however, at the cost
of not relying on the existing converse Lyapunov theorems and possibly
sacrificing the smoothness of barrier functions.

Nonetheless, we provide the theoretical results of converse theorems and hope
to shed some light on designing powerful algorithms, e.g. learning techniques
[35, 36, 37], for constructing Lyapunov-barrier functions with respect to
stability with safety guarantee or reach-avoid-stay specifications.

For future work, it would be an interesting application in using the current
Lypunov-barrier characterizations as abstractions for linear temporal logic
specifications for hybrid systems. It is also valuable to design algorithms
based on this theoretical work to construct Lyapunov-like functions that
improves the estimated region of attractions. Another interesting direction is
to explore the stochastic analogue of Lyapunov-barrier function theorems,
particularly the converse theorems, for stochastic hybrid systems.

## References

  * Kloetzer and Belta [2008] M. Kloetzer, C. Belta,  A fully automated framework for control of linear systems from temporal logic specifications,  IEEE Transactions on Automatic Control 53 (2008) 287–297.
  * Tabuada and Pappas [2006] P. Tabuada, G. J. Pappas,  Linear time logic control of discrete-time linear systems,  IEEE Transactions on Automatic Control 51 (2006) 1862–1877.
  * Nilsson et al. [2017] P. Nilsson, N. Ozay, J. Liu,  Augmented finite transition systems as abstractions for control synthesis,  Discrete Event Dynamic Systems 27 (2017) 301–340.
  * Baier and Katoen [2008] C. Baier, J.-P. Katoen, Principles of model checking, MIT press, 2008.
  * Girard et al. [2009] A. Girard, G. Pola, P. Tabuada,  Approximately bisimilar symbolic models for incrementally stable switched systems,  IEEE Transactions on Automatic Control 55 (2009) 116–126.
  * Pola et al. [2008] G. Pola, A. Girard, P. Tabuada,  Approximately bisimilar symbolic models for nonlinear control systems,  Automatica 44 (2008) 2508–2516.
  * Liu [2017] J. Liu,  Robust abstractions for control synthesis: Completeness via robustness for linear-time properties,  in: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, 2017, pp. 101–110.
  * Liu [2021] J. Liu,  Closing the gap between discrete abstractions and continuous control: Completeness via robustness and controllability,  in: International Conference on Formal Modeling and Analysis of Timed Systems, Springer, 2021, pp. 67–83.
  * Gao et al. [2014] S. Gao, S. Kong, W. Chen, E. Clarke,  Delta-complete analysis for bounded reachability of hybrid systems,  arXiv preprint arXiv:1404.7171 (2014).
  * Girard et al. [2015] A. Girard, G. Gössler, S. Mouelhi,  Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models,  IEEE Transactions on Automatic Control 61 (2015) 1537–1549.
  * Li and Liu [2020] Y. Li, J. Liu,  Robustly complete synthesis of memoryless controllers for nonlinear systems with reach-and-stay specifications,  IEEE Transactions on Automatic Control 66 (2020) 1199–1206.
  * Li and Liu [2022] Y. Li, J. Liu,  Robustly complete synthesis of sampled-data control for continuous-time nonlinear systems with reach-and-stay objectives,  Nonlinear Analysis: Hybrid Systems 44 (2022) 101170.
  * Meng et al. [2021] Y. Meng, Y. Li, J. Liu,  Control of nonlinear systems with reach-avoid-stay specifications: A Lyapunov-barrier approach with an application to the Moore-Greizer model,  in: 2021 American Control Conference (ACC), IEEE, 2021, pp. 2284–2291.
  * Agrawal and Sreenath [2017] A. Agrawal, K. Sreenath,  Discrete control barrier functions for safety-critical control of discrete systems with application to bipedal robot navigation.,  in: Robotics: Science and Systems, volume 13, Cambridge, MA, USA, 2017\.
  * Hsu et al. [2015] S.-C. Hsu, X. Xu, A. D. Ames,  Control barrier function based quadratic programs with application to bipedal robotic walking,  in: 2015 American Control Conference (ACC), IEEE, 2015, pp. 4542–4548.
  * Nguyen et al. [2020] Q. Nguyen, X. Da, J. Grizzle, K. Sreenath,  Dynamic walking on stepping stones with gait library and control barrier functions,  in: Algorithmic Foundations of Robotics XII, Springer, 2020, pp. 384–399.
  * Ames et al. [2016] A. D. Ames, X. Xu, J. W. Grizzle, P. Tabuada,  Control barrier function based quadratic programs for safety critical systems,  IEEE Transactions on Automatic Control 62 (2016) 3861–3876.
  * Romdlony and Jayawardhana [2016] M. Z. Romdlony, B. Jayawardhana,  Stabilization with guaranteed safety using control Lyapunov–barrier function,  Automatica 66 (2016) 39–47.
  * Braun and Kellett [2017] P. Braun, C. M. Kellett,  On (the existence of) control Lyapunov barrier functions (2017).
  * Braun and Kellett [2020] P. Braun, C. M. Kellett,  Comment on “stabilization with guaranteed safety using control Lyapunov–barrier function”,  Automatica 122 (2020) 109225.
  * Braun et al. [2019] P. Braun, C. M. Kellett, L. Zaccarian,  Complete control Lyapunov functions: Stability under state constraints,  IFAC-PapersOnLine 52 (2019) 358–363.
  * Meng et al. [2022] Y. Meng, Y. Li, M. Fitzsimmons, J. Liu,  Smooth converse Lyapunov-barrier theorems for asymptotic stability with safety constraints and reach-avoid-stay specifications,  Automatica 144 (2022) 110478.
  * Meng and Liu [2022] Y. Meng, J. Liu,  Sufficient conditions for robust probabilistic reach-avoid-stay specifications using stochastic lyapunov-barrier functions,  in: 2022 American Control Conference (ACC), 2022, pp. 2283–2288.
  * Goebel et al. [2012] R. Goebel, R. G. Sanfelice, A. R. Teel, Hybrid dynamical systems, Princeton University Press, 2012.
  * Ghanbarpour and Maghenem [2021] M. Ghanbarpour, M. Maghenem,  Barrier functions for robust safety in differential inclusions, part ii: The converse problem,  in: 2021 60th IEEE Conference on Decision and Control (CDC), IEEE, 2021, pp. 5344–5349.
  * Maghenem and Ghanbarpour [2022] M. Maghenem, M. Ghanbarpour,  A converse robust-safety theorem for differential inclusions,  arXiv preprint arXiv:2208.11364 (2022).
  * Maghenem and Karaki [2022] M. Maghenem, D. Karaki,  On a strong robust-safety notion for differential inclusions,  arXiv preprint arXiv:2208.12520 (2022).
  * Wisniewski and Sloth [2015] R. Wisniewski, C. Sloth,  Converse barrier certificate theorems,  IEEE Transactions on Automatic Control 61 (2015) 1356–1361.
  * Ratschan [2018] S. Ratschan,  Converse theorems for safety and barrier certificates,  IEEE Transactions on Automatic Control 63 (2018) 2628–2632.
  * Liu [2021] J. Liu,  Converse barrier functions via lyapunov functions,  IEEE Transactions on Automatic Control 67 (2021) 497–503.
  * Teel and Praly [2000] A. R. Teel, L. Praly,  A smooth Lyapunov function from a class-estimate involving two positive semidefinite functions,  ESAIM: Control, Optimisation and Calculus of Variations 5 (2000) 313–367.
  * Liu et al. [2020] J. Liu, Y. Meng, Y. Li, M. Fitzsimmons,  Smooth converse lyapunov-barrier theorems for asymptotic stability with safety constraints and reach-avoid-stay specifications,  arXiv preprint arXiv:2009.04432 (2020).
  * Lee [2013] J. M. Lee,  Smooth manifolds,  in: Introduction to smooth manifolds, Springer, 2013, pp. 1–31.
  * Wang et al. [2021] C. Wang, Y. Meng, S. L. Smith, J. Liu,  Safety-critical control of stochastic systems using stochastic control barrier functions,  in: 2021 IEEE Conference on Decision and Control (CDC), 2021, pp. 5924–5931.
  * Ravanbakhsh and Sankaranarayanan [2017] H. Ravanbakhsh, S. Sankaranarayanan,  Learning Lyapunov (potential) functions from counterexamples and demonstrations,  arXiv preprint arXiv:1705.09619 (2017).
  * Zhao et al. [2020] H. Zhao, X. Zeng, T. Chen, Z. Liu,  Synthesizing barrier certificates using neural networks,  in: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, 2020, pp. 1–11.
  * Berkenkamp et al. [2016] F. Berkenkamp, R. Moriconi, A. P. Schoellig, A. Krause,  Safe learning of regions of attraction for uncertain, nonlinear systems with gaussian processes,  in: 2016 IEEE 55th Conference on Decision and Control (CDC), IEEE, 2016, pp. 4661–4666.

##  Appendix A Proof of Proposition 3.17

Proof: The proof is similar to [32, Proposition 16]. We need to verify
condition (i) and (ii) of Definition 2.6.

(i) For any $\varepsilon>0$, there exists a $\tau>0$ such that for any
solution $\phi$ of $\mathbf{H}_{\delta^{\prime}}$ with $\phi(0,0)\in
A+\frac{\varepsilon}{2}\mathcal{B}$ and $|\phi(t,j)|_{A}\geq\varepsilon$, we
have $t+j\geq\tau$. Now let
$r=r(A+\varepsilon\mathcal{B},\tau,\delta^{\prime},dt)$ from Lemma 3.15 and
set $\delta_{\varepsilon}=\min(r,\varepsilon/2)$. Let $\phi$ be any solution
of $\mathbf{H}_{\delta^{\prime}}$ with $|\phi(0,0)|_{A}<\delta_{\varepsilon}$.
It suffices to show that $|\phi(t,j)|_{A}<\varepsilon$ for all
$(t,j)\in\operatorname{dom}(\phi)$. Suppose the opposite, then there exists
$(t,j)\in\operatorname{dom}(\phi)$ and $t+j\geq\tau>0$ such that
$|\phi(t,j)|_{A}\geq\varepsilon$. Since $A$ is compact, by the selection of
$\delta_{\varepsilon}$, we can always find an $x\in
A\cap(\phi(0,0)+r\mathcal{B})$. By Lemma 3.15, there exists a
$\psi\in\mathfrak{S}_{\mathbf{H}}^{\delta^{\prime}}(x)$ with
$\operatorname{dom}(\psi)=\operatorname{dom}(\phi)$ and
$\psi(t,j)=\phi(t,j)\notin A$, which violates the invariance assumption of $A$
for $\mathbf{H}_{\delta}$.

(ii)For any $\vartheta>0$, by the proof of (i), the uniform stability for
$\mathbf{H}_{\delta}$, we can find a $\delta_{\vartheta}$ such that for any
solution $\phi$ of $\mathbf{H}_{\delta}^{\prime}$, we have
$|\phi(t,j)|_{A}<\vartheta$ for all $(t,j)\in\operatorname{dom}(\phi)$
whenever $|\phi(0,0)|_{A}<\delta_{\vartheta}$. Let
$r=r(A+\vartheta\mathcal{B},\tau,\delta^{\prime},\delta)$ from Lemma 3.15 for
some well-posed $\tau>0$. Choose $\rho\in(0,r)$, we now show that, for any
solution $\phi$ of $\mathbf{H}_{\delta^{\prime}}$, $\phi(t,j)\in A$ for all
$(t,j)\in\operatorname{dom}(\phi)$ and $t+j\geq\tau$ whenever
$|\phi(0,0)|_{A}<\rho$. Suppose the opposite. Then there exists some
$(t,j)\in\operatorname{dom}(\phi)$ and $t+j\geq\tau$ such that
$\phi(t,j)\notin A$. Note that we can always find an $x\in
A\cap(\phi(0,0)+r\mathcal{B})$ based on the choice of $\rho$. By Lemma 3.15,
there exists a $\psi\in\mathfrak{S}_{\mathbf{H}}^{\delta^{\prime}}(x)$ with
$\operatorname{dom}(\psi)=\operatorname{dom}(\phi)$ and
$\psi(t,j)=\phi(t,j)\notin A$, which violates the invariance assumption of $A$
for $\mathbf{H}_{\delta}$.