# Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees

Đorđe Žikelić⋆1, Mathias Lechner⋆2, Thomas A. Henzinger1, Krishnendu
Chatterjee1

###### Abstract

We study the problem of learning controllers for discrete-time non-linear
stochastic dynamical systems with formal reach-avoid guarantees. This work
presents the first method for providing formal reach-avoid guarantees, which
combine and generalize stability and safety guarantees, with a tolerable
probability threshold $p\in[0,1]$ over the infinite time horizon in general
Lipschitz continuous systems. Our method leverages advances in machine
learning literature and it represents formal certificates as neural networks.
In particular, we learn a certificate in the form of a reach-avoid
supermartingale (RASM), a novel notion that we introduce in this work. Our
RASMs provide reachability and avoidance guarantees by imposing constraints on
what can be viewed as a stochastic extension of level sets of Lyapunov
functions for deterministic systems. Our approach solves several important
problems – it can be used to learn a control policy from scratch, to verify a
reach-avoid specification for a fixed control policy, or to fine-tune a pre-
trained policy if it does not satisfy the reach-avoid specification. We
validate our approach on $3$ stochastic non-linear reinforcement learning
tasks.

## Introduction

Reinforcement learning (RL) has achieved impressive results in solving non-
linear control problems, resulting in an interest to deploy RL algorithms in
safety-critical applications. However, most RL algorithms focus solely on
optimizing expected performance and do not take safety constraints into
account (Sutton and Barto 2018). This raises concerns about their
applicability to safety-critical domains in which unsafe behavior can lead to
catastrophic consequences (Amodei et al. 2016; García and Fernández 2015).
Complicating matters, models are usually imperfect approximations of real
systems that are obtained from observed data, thus models often need to
account for uncertainty which is modelled via stochastic disturbances. Formal
safety verification of policies learned via RL algorithms and design of
learning algorithms that take safety constraints into account have thus become
very active research topics.

Reach-avoid constraints are one of the most common and practically relevant
constraints appearing in safety-critical applications that generalize both
reachability and safety constraints (Summers and Lygeros 2010). Given a target
region and an unsafe region, the reach-avoid constraint requires that a system
controlled by a policy converges to the target region while avoiding the
unsafe region. For instance, a lane-keeping constraint requires a self-driving
car to reach its destination without leaving the allowed car lanes (Vahidi and
Eskandarian 2003). In the case of stochastic control problems, reach-avoid
constraints are also specified by a minimal probability with which the system
controlled by a policy needs to satisfy the reach-avoid constraint.

In this work, we consider discrete-time stochastic control problems under
reach-avoid constraints. Following the recent trend that aims to leverage
advances in deep RL to safe control, we propose a learning method that learns
a control policy together with a formal reach-avoid certificate in the form of
a reach-avoid supermartingale (RASM), a novel notion that we introduce in this
work. Informally, an RASM is a function assigning nonnegative real values to
each state that is required to strictly decrease in expected value until the
target region is reached, but needs to strictly increase for the system to
reach the unsafe region. By carefully choosing the ratio of the initial level
set of the RASM and the least level set that the RASM needs to attain for the
system to reach the unsafe region (here we use the standard level set
terminology of Lyapunov functions (Haddad and Chellaboina 2011)), we obtain a
formal reach-avoid certificate. The name of RASMs is chosen to emphasize the
connection to supermartingale processes in probability theory (Williams 1991).
Our RASMs significantly generalize and unify the stochastic control barrier
functions which are a standard certificate for safe control of stochastic
systems (Prajna, Jadbabaie, and Pappas 2007) and ranking supermartingales that
were introduced to certify probability $1$ reachability and stability in
(Lechner et al. 2022).

Contributions. This work presents the first control method that provides
formal reach-avoid guarantees for control of stochastic systems with a
specified probability threshold over the infinite time horizon in Lipschitz
continuous systems. In contrast, the existing approaches to control under
reach-avoid constraints are only applicable to finite horizon settings,
polynomial stochastic systems or to deterministic systems (see the following
section for an overview of related work). Moreover, our method simultaneously
learns the control policy and the RASM certificate in the form of neural
networks and is applicable to general non-linear systems. This contrasts the
existing methods from the literature that are based on stochastic control
barrier functions, which utilize convex optimization tools to compute control
policies and are restricted to polynomial system dynamics and policies
(Prajna, Jadbabaie, and Pappas 2007; Steinhardt and Tedrake 2012; Santoyo,
Dutreix, and Coogan 2021; Xue et al. 2021). Our algorithm draws insight from
established methods for learning Lyapunov functions for stability in
deterministic control problems (Richards, Berkenkamp, and Krause 2018; Chang,
Roohi, and Gao 2019; Abate et al. 2021), which were demonstrated to be more
efficient than the existing convex optimization methods and were adapted in
(Lechner et al. 2022) for probability $1$ reachability and stability
verification. Finally, our method learns a suitable policy on demand, or
alternatively, verifies reach-avoid properties of a fixed Lipschitz continuous
control policy. We experimentally validate our method on $3$ stochastic RL
tasks and show that it efficiently learns control policies with probabilistic
reach-avoid guarantees in practice.

## Related Work

Deterministic control problems There is extensive literature on safe control,
with most works certifying stability via Lyapunov functions (Haddad and
Chellaboina 2011) or safety via control barrier functions (Ames et al. 2019).
Most early works rely either on hand-designed certificates, or automate their
computation through convex optimization methods such as sum-of-squares (SOS)
programming (Henrion and Garulli 2005; Parrilo 2000; Jarvis-Wloszek et al.
2003). Automation via SOS programming is restricted to problems with
polynomial system dynamics and does not scale well with dimension. A promising
approach to overcome these limitations is to learn a control policy together
with a safety certificate in the form of neural networks, for instance see
(Richards, Berkenkamp, and Krause 2018; Sun, Jha, and Fan 2020; Jin et al.
2020; Chang and Gao 2021; Qin et al. 2021). In particular, (Chang, Roohi, and
Gao 2019; Abate et al. 2021) learn a control policy and a certificate as
neural networks by using a learner-verifier framework which repeatedly learns
a candidate policy and a certificate and then tries to either verify or refine
them. Our method extends some of these ideas to stochastic systems.

Stochastic control problems Safe control of stochastic systems has received
comparatively less attention. Most existing approaches are abstraction based –
they consider finite-time horizon systems and approximate them via a finite-
state Markov decision process (MDP). The constrained control problem is then
solved for the MDP. Due to accumulation of the approximation error in each
time step, the size of the MDP state space needs to grow with the length of
the considered time horizon, making these methods applicable to systems that
evolve over fixed finite time horizons. Notable examples include (Soudjani,
Gevaerts, and Abate 2015; Lavaei et al. 2020; Cauchi and Abate 2019; Vinod,
Gleason, and Oishi 2019; Vaidya 2015; Crespo and Sun 2003). Another line of
work considers polynomial systems and utilizes stochastic control barrier
functions and convex optimization tools to compute polynomial control policies
(Prajna, Jadbabaie, and Pappas 2007; Steinhardt and Tedrake 2012; Santoyo,
Dutreix, and Coogan 2021; Xue et al. 2021).

Constrained MDPs Safe RL has also been studied in the context of constrained
MDPs (CMDPs) (Altman 1999; Geibel 2006). An agent in a CMDP must satisfy hard
constraints on expected cost for one or more auxiliary notions of cost
aggregated over an episode. Several works study RL algorithms for CMDPs
(Uchibe and Doya 2007), notably the Constrained Policy Optimization (CPO)
(Achiam et al. 2017) or the method (Chow et al. 2018) which proposed a
Lyapunov method for solving CMDPs. While these algorithms perform well, their
constraints are satisfied in expectation which makes them less suitable for
safety-critical systems.

Safe RL via shielding Some approaches ensure safety by computing two control
policies – the main policy that optimizes the expected reward, and the backup
policy that the system falls back to whenever a safety constraint may be
violated (Michalska and Mayne 1993; Perkins and Barto 2002; Alshiekh et al.
2018; Elsayed-Aly et al. 2021; Giacobbe et al. 2021). The backup policy can
thus be of simpler form. Shielding for stochastic linear systems with additive
disturbances has been considered in (Wabersich and Zeilinger 2018). (Li and
Bastani 2020; Bastani and Li 2021) are applicable to stochastic non-linear
systems, however their safety guarantees are statistical – their algorithms
are randomized with parameters $\delta,\epsilon\in(0,1)$ and they with
probability $1-\delta$ compute an action that is safe in the current state
with probability at least $1-\epsilon$. The statistical error is accumulated
at each state, hence these approaches are not suitable for infinite or long
time horizons. In contrast, our approach targets formal guarantees for
infinite time horizon problems.

Safe exploration Model-free RL algorithms need to explore the state space in
order to learn high performing actions. Safe exploration RL restricts
exploration in a way which ensures that given safety constraints are
satisfied. The most common approach to ensuring safe exploration is learning
the system dynamics’ uncertainty bounds and limiting the exploratory actions
within a high probability safety region, with the existing methods based on
Gaussian Processes (Koller et al. 2018; Turchetta, Berkenkamp, and Krause
2019; Berkenkamp 2019), linearized models (Dalal et al. 2018), deep robust
regression (Liu et al. 2020), safe padding (Hasanbeig, Abate, and Kroening
2020) and Bayesian neural networks (Lechner et al. 2021). Recent work has also
considered learning stable stochastic dynamics from data (Umlauft and Hirche
2017; Lawrence et al. 2020).

Probabilistic program analysis Supermartingales have also been used for the
analysis of probabilistic programs (PPs). In particular, RSMs were originally
used to prove almost-sure termination in PPs (Chakarov and Sankaranarayanan
2013) and (Abate, Giacobbe, and Roy 2021) learns RSMs in PPs. Supermartingales
were also used for probabilistic termination and safety analysis in PPs
(Chatterjee, Novotný, and Zikelic 2017; Chatterjee et al. 2022).

## Preliminaries

We consider discrete-time stochastic dynamical systems defined by the equation

$\mathbf{x}_{t+1}=f(\mathbf{x}_{t},\mathbf{u}_{t},\omega_{t}),\,\mathbf{x}_{0}\in\mathcal{X}_{0}.$

The function
$f:\mathcal{X}\times\mathcal{U}\times\mathcal{N}\rightarrow\mathcal{X}$
defines system dynamics, where $\mathcal{X}\subseteq\mathbb{R}^{m}$ is the
system state space, $\mathcal{U}\subseteq\mathbb{R}^{n}$ is the control action
space and $\mathcal{N}\subseteq\mathbb{R}^{p}$ is the stochastic disturbance
space. We use $t\in\mathbb{N}_{0}$ to denote the time index,
$\mathbf{x}_{t}\in\mathcal{X}$ the state of the system,
$\mathbf{u}_{t}\in\mathcal{U}$ the action and $\omega_{t}\in\mathcal{N}$ the
stochastic disturbance vector at time $t$. The set
$\mathcal{X}_{0}\subseteq\mathcal{X}$ is the set of initial states. The action
$\mathbf{u}_{t}$ is chosen according to a control policy
$\pi:\mathcal{X}\rightarrow\mathcal{U}$, i.e.
$\mathbf{u}_{t}=\pi(\mathbf{x}_{t})$. The stochastic disturbance vector
$\omega_{t}$ is sampled according to a specified probability distribution $d$
over $\mathbb{R}^{p}$. The dynamics function $f$, control policy $\pi$ and
probability distribution $d$ together define a stochastic feedback loop
system.

A sequence $(\mathbf{x}_{t},\mathbf{u}_{t},\omega_{t})_{t\in\mathbb{N}_{0}}$
of state-action-disturbance triples is a trajectory of the system, if for each
$t\in\mathbb{N}_{0}$ we have $\mathbf{u}_{t}=\pi(\mathbf{x}_{t})$,
$\omega_{t}\in\mathsf{support}(d)$ and
$\mathbf{x}_{t+1}=f(\mathbf{x}_{t},\mathbf{u}_{t},\omega_{t})$. For each
initial state $\mathbf{x}_{0}\in\mathcal{X}$, the system induces a Markov
process which gives rise to the probability space over the set of all
trajectories that start in $\mathbf{x}_{0}$ (Puterman 1994). We denote the
probability measure and the expectation in this probability space by
$\mathbb{P}_{\mathbf{x}_{0}}$ and $\mathbb{E}_{\mathbf{x}_{0}}$.

Assumptions We assume that $\mathcal{X}\subseteq\mathbb{R}^{m}$,
$\mathcal{X}_{0}\subseteq\mathbb{R}^{m}$, $\mathcal{U}\subseteq\mathbb{R}^{n}$
and $\mathcal{N}\subseteq\mathbb{R}^{p}$ are all Borel-measurable, which is a
technical assumption necessary for the system semantics to be mathematically
well-defined. We also assume that $\mathcal{X}\subseteq\mathbb{R}^{m}$ is
compact and that the dynamics function $f$ is Lipschitz continuous, which are
common assumptions in control theory.

Probabilistic reach-avoid problem Let $\mathcal{X}_{t}\subseteq\mathcal{X}$
and $\mathcal{X}_{u}\subseteq\mathcal{X}$ be disjoint Borel-measurable subsets
of $\mathbb{R}^{m}$, which we refer to as the target set and the unsafe set,
respectively. Let $p\in[0,1]$ be a probability threshold. Our goal is to learn
a control policy which guarantees that, with probability at least $p$, the
system reaches the target set $\mathcal{X}_{t}$ without reaching the unsafe
set $\mathcal{X}_{u}$. Formally, we want to learn a control policy $\pi$ such
that, for any initial state $\mathbf{x}_{0}\in\mathcal{X}_{0}$, we have

$\mathbb{P}_{\mathbf{x}_{0}}\Big{[}\textrm{ReachAvoid}(\mathcal{X}_{t},\mathcal{X}_{u})\Big{]}\geq
p$

with
$\textrm{ReachAvoid}(\mathcal{X}_{t},\mathcal{X}_{u})=\\{(\mathbf{x}_{t},\mathbf{u}_{t},\omega_{t})_{t\in\mathbb{N}_{0}}\mid\exists
t\in\mathbb{N}_{0}.\,\mathbf{x}_{t}\in\mathcal{X}_{t}\land(\forall
t^{\prime}\leq t.\,\mathbf{x}_{t^{\prime}}\not\in\mathcal{X}_{u})\\}$ the set
of trajectories that reach $\mathcal{X}_{t}$ without reaching
$\mathcal{X}_{u}$.

We restrict to the cases when either $p<1$, or $p=1$ and
$\mathcal{X}_{u}=\emptyset$. Our approach is not applicable to the case $p=1$
and $\mathcal{X}_{u}\neq\emptyset$ due to technical issues that arise in
defining our formal certificate, which we discuss in the following section. We
remark that probabilistic reachability is a special instance of our problem
obtained by setting $\mathcal{X}_{u}=\emptyset$. On the other hand, we cannot
directly obtain the probabilistic safety problem by assuming any specific form
of the target set $\mathcal{X}_{t}$, however we will show in the following
section that our method implies probabilistic safety with respect to
$\mathcal{X}_{u}$ if we provide it with $\mathcal{X}_{t}=\emptyset$.

## Theoretical Results

We now present our framework for formally certifying a reach-avoid constraint
with a given probability threshold. Our framework is based on the novel notion
of reach-avoid supermartingales (RASMs) that we introduce in this work. Note
that, in this section only, we assume that the policy is fixed. In the next
section, we will present our algorithm for learning policies that provide
formal reach-avoid guarantees in which RASMs will be an integral ingredient.
In what follows, we consider a discrete-time stochastic dynamical system
defined as in the previous section. For now, we assume that the probability
threshold is strictly smaller than $1$, i.e. $p<1$. We will later show that
our approach straightforwardly extends to the case $p=1$ and
$\mathcal{X}_{u}=\emptyset$.

Reach-avoid supermartingales We define a reach-avoid supermartingale (RASM) to
be a continuous function $V:\mathcal{X}\rightarrow\mathbb{R}$ that assigns
real values to system states. The name is chosen to emphasize the connection
to supermartingale processes from probability theory (Williams 1991), which we
will explore later in order to prove the effectiveness of RASMs for verifying
reach-avoid properties. The value of $V$ is required to be nonnegative over
the state space $\mathcal{X}$ (Nonnegativity condition), to be bounded from
above by $1$ over the set of initial states $\mathcal{X}_{0}$ (Initial
condition) and to be bounded from below by $\frac{1}{1-p}$ over the set of
unsafe states $\mathcal{X}_{u}$ (Safety condition). Hence, in order for a
system trajectory to reach an unsafe state and violate the safety
specification, the value of the RASM $V$ needs to increase at least
$\frac{1}{1-p}$ times along the trajectory. Finally, we require the existence
of $\epsilon>0$ such that the value of $V$ decreases in expected value by at
least $\epsilon$ after every one-step evolution of the system from every
system state $\mathbf{x}\in\mathcal{X}\backslash\mathcal{X}_{t}$ for which
$V(\mathbf{x})\leq\frac{1}{1-p}$ (Expected decrease condition). Intuitively,
this last condition imposes that the system has a tendency to strictly
decrease the value of $V$ until either the target set $\mathcal{X}_{t}$ is
reached or a state with $V(\mathbf{x})\geq\frac{1}{1-p}$ is reached. However,
as the value of $V$ needs to increase at least $\frac{1}{1-p}$ times in order
for the system to reach an unsafe state, these four conditions will allow us
to use RASMs to certify that the reach-avoid constraint is satisfied with
probability at least $p$.

######  Definition 1 (Reach-avoid supermartingales).

Let $\mathcal{X}_{t}\subseteq\mathcal{X}$ and
$\mathcal{X}_{u}\subseteq\mathcal{X}$ be the target set and the unsafe set,
and let $p\in[0,1)$ be the probability threshold. A continuous function
$V:\mathcal{X}\rightarrow\mathbb{R}$ is said to be a reach-avoid
supermartingale (RASM) with respect to $\mathcal{X}_{t}$, $\mathcal{X}_{u}$
and $p$ if it satisfies:

  1. 1.

Nonnegativity condition. $V(\mathbf{x})\geq 0$ for each
$\mathbf{x}\in\mathcal{X}$.

  2. 2.

Initial condition. $V(\mathbf{x})\leq 1$ for each
$\mathbf{x}\in\mathcal{X}_{0}$.

  3. 3.

Safety condition. $V(\mathbf{x})\geq\frac{1}{1-p}$ for each
$\mathbf{x}\in\mathcal{X}_{u}$.

  4. 4.

Expected decrease condition. There exists $\epsilon>0$ such that, for each
$\mathbf{x}\in\mathcal{X}\backslash\mathcal{X}_{t}$ at which
$V(\mathbf{x})\leq\frac{1}{1-p}$, we have
$V(\mathbf{x})\geq\mathbb{E}_{\omega\sim
d}[V(f(\mathbf{x},\pi(\mathbf{x}),\omega))]+\epsilon$.

Comparison to Lyapunov functions The defining properties of RASMs hint a
connection to Lyapunov functions for deterministic control systems. However,
the key difference between Lyapunov functions and our RASMs is that Lyapunov
functions deterministically decrease in value whereas RASMs decrease in
expectation. Deterministic decrease ensures that each level set of a Lyapunov
function, i.e. a set of states at which the value of Lyapunov functions is at
most $l$ for some $l\geq 0$, is an invariant of the system. However, it is in
general not possible to impose such a condition on stochastic systems. In
contrast, our RASMs only require expected decrease in the level, and the
Initial and the Unsafe conditions can be viewed as conditions on the maximal
initial level set and the minimal unsafe level set. The choice of a ratio of
these two level values allows us to use existing results from martingale
theory in order to obtain probabilistic avoidance guarantees, while the
Expected decrease condition by $\epsilon>0$ furthermore provides us with
probabilistic reachability guarantees.

Certifying reach-avoid constraints via RASMs We now show that the existence of
an $\epsilon$-RASM for some $\epsilon>0$ implies that the reach-avoid
constraint is satisfied with probability at least $p$.

######  Theorem 1.

Let $\mathcal{X}_{t}\subseteq\mathcal{X}$ and
$\mathcal{X}_{u}\subseteq\mathcal{X}$ be the target set and the unsafe set,
respectively, and let $p\in[0,1)$ be the probability threshold. Suppose that
there exists an RASM $V$ with respect to $\mathcal{X}_{t}$, $\mathcal{X}_{u}$
and $p$. Then, for every $\mathbf{x}_{0}\in\mathcal{X}_{0}$,
$\mathbb{P}_{\mathbf{x}_{0}}[\textrm{ReachAvoid}(\mathcal{X}_{t},\mathcal{X}_{u})]\geq
p$.

The complete proof of Theorem 1 is provided in the Appendix. However, in what
follows we sketch the key ideas behind our proof, in order to illustrate the
applicability of martingale theory to reasoning about stochastic systems which
we believe to have significant potential for applications beyond the scope of
this work. To prove the theorem, we first show that an $\epsilon$-RASM $V$
induces a supermartingale (Williams 1991) in the probability space over the
set of all trajectories that start in an initial state
$\mathbf{x}_{0}\in\mathcal{X}_{0}$. Intuitively, a supermartingale in a
probability space $(\Omega,\mathcal{F},\mathbb{P})$ is a stochastic process
$(X_{t})_{t=0}^{\infty}$ such that, for each $t\in\mathbb{N}_{0}$, the
expected value of $X_{t+1}$ conditioned on the value of $X_{t}$ is less than
or equal to $X_{t}$. We formalize this definition together with the notion of
conditional expectation and provide an overview of definitions and results
form martingale theory that we use in our proof in the Appendix.

Now, let
$(\Omega_{\mathbf{x}_{0}},\mathcal{F}_{\mathbf{x}_{0}},\mathbb{P}_{\mathbf{x}_{0}})$
be the probability space of trajectories that start in $\mathbf{x}_{0}$. Then,
for each time step $t\in\mathbb{N}_{0}$, we define a random variable

$X_{t}(\rho)=\begin{cases}V(\mathbf{x}_{t}),&\text{if
}\mathbf{x}_{i}\not\in\mathcal{X}_{t}\text{ and
}V(\mathbf{x}_{i})<\frac{1}{1-p}\\\ &\text{ for each }0\leq i\leq t\\\
0,&\text{if }\mathbf{x}_{i}\in\mathcal{X}_{t}\text{ for some }0\leq i\leq t\\\
&\text{ and }V(\mathbf{x}_{j})<\frac{1}{1-p}\text{ for each }0\leq j\leq i\\\
\frac{1}{1-p},&\text{otherwise}\end{cases}$

for each trajectory
$\rho=(\mathbf{x}_{t},\mathbf{u}_{t},\omega_{t})_{t\in\mathbb{N}_{0}}\in\Omega_{\mathbf{x}_{0}}$.
In other words, the value of $X_{t}$ is equal to the value of $V$ at
$\mathbf{x}_{t}$, unless either the target set $\mathcal{X}_{t}$ has been
reached first in which case we set all future values of $\mathcal{X}_{t}$ to
$0$, or a state in which $V$ exceeds $\frac{1}{1-p}$ has been reached first in
which case we set all future values of $\mathcal{X}_{t}$ to $\frac{1}{1-p}$.
Then, since $V$ satisfies the Nonnegativity and the Expected decrease
condition of RASMs, we may show that $(X_{t})_{t=0}^{\infty}$ is a
supermartingale. in the probability space
$(\Omega_{\mathbf{x}_{0}},\mathcal{F}_{\mathbf{x}_{0}},\mathbb{P}_{\mathbf{x}_{0}})$.

Next, we show that the nonnegative supermartingale $(X_{t})_{t=0}^{\infty}$
with probability $1$ converges to and reaches $0$ or a value that is greater
than or equal to $\frac{1}{1-p}$. To do this, we first employ the
Supermartingale Convergence Theorem (see the Appendix) which states that every
nonnegative supermartingale converges to some value with probability $1$. We
then use the fact that, in the Expected decrease condition of RASMs, the
decrease in expected value is strict and by at least $\epsilon>0$, in order to
conclude that this value is reached and has to be either $0$ or greater than
or equal to $\frac{1}{1-p}$.

Finally, we use another classical result from martingale theory (see the
Appendix) which states that, given a nonnegative supermartingale
$(X_{t})_{t=0}^{\infty}$ and $\lambda>0$,

$\mathbb{P}\Big{[}\sup_{i\geq
0}X_{i}\geq\lambda\Big{]}\leq\frac{\mathbb{E}[X_{0}]}{\lambda}.$

Plugging $\lambda=\frac{1}{1-p}$ into the above inequality, it follows that
$\mathbb{P}_{\mathbf{x}_{0}}[\sup_{i\geq
0}X_{i}\geq\frac{1}{1-p}]\leq(1-p)\cdot\mathbb{E}_{\mathbf{x}_{0}}[X_{0}]\leq
1-p$. The second inequality follows since $X_{0}(\rho)=V(\mathbf{x}_{0})\leq
1$ for every $\rho\in\Omega_{\mathbf{x}_{0}}$ by the Initial condition of
RASMs. Hence, as $(X_{t})_{t=0}^{\infty}$ with probability $1$ either reaches
$0$ or a value that is greater than or equal to $\frac{1}{1-p}$, we conclude
that $(X_{t})_{t=0}^{\infty}$ reaches $0$ without reaching a value that is
greater than or equal to $\frac{1}{1-p}$ with probability at least $p$. By the
definition of each $X_{t}$ and by the Safety condition of RASMs, this implies
that with probability at least $p$ the system will reach the target set
$\mathcal{X}_{t}$ without reaching the unsafe set $\mathcal{X}_{u}$, i.e. that
$\mathbb{P}_{\mathbf{x}_{0}}[\textrm{ReachAvoid}(\mathcal{X}_{t},\mathcal{X}_{u})]\geq
p$.

Probabilistic safety In order to solve the probabilistic safety problem and
verify that a control policy guarantees that the unsafe set $\mathcal{X}_{u}$
is not reached with probability at least $p$, we may modify the Expected
decrease condition of RASMs by setting $\mathcal{X}_{t}=\emptyset$. Thus,
RASMs are also effective for the probabilistic safety problem. This claim
follows immediately from our proof of Theorem 1. In this case and if we set
$\epsilon=0$, then our RASMs coincide with stochastic barrier functions of
(Prajna, Jadbabaie, and Pappas 2007). However, if $\mathcal{X}_{t}$ is not
empty, then we must have $\epsilon>0$ in order to enforce convergence and
reachability of $\mathcal{X}_{t}$.

Extension to $p=1$ and $\mathcal{X}_{u}=\emptyset$ and comparison to RSMs So
far, we have only considered $p\in[0,1)$. The difficulty in the case $p=1$
arises since the value $\frac{1}{1-p}$ in the Safety and the Expected decrease
conditions in Definition 1 would not be well-defined. However, if
$\mathcal{X}_{u}=\emptyset$, then the Safety condition need not be imposed at
any state. Moreover, it follows directly from our proof that imposing the
expected decrease condition at all states in
$\mathcal{X}\backslash\mathcal{X}_{t}$ makes RASMs sound for certifying
probability $1$ reachability. In fact, in this special case our RASMs reduce
to the RSMs of (Lechner et al. 2022). The key novelty of our RASMs over RSMs
is that we also employ level set reasoning in order to obtain probabilistic
reach-avoid guarantees, thus presenting a true stochastic extension of
Lyapunov functions that allow reasoning both about reach-avoid specifications
as well as quantitative reasoning about the probability with which they are
satisfied. In contrast, RSMs do not reason about level sets and can only
certify probability $1$ reachability.

## Learning Reach-avoid Policies

We now present our algorithm for learning policies with reach-avoid
guarantees, which learns a policy together with an RASM certificate. The
algorithm consists of two modules called learner and verifier, which are
composed into a loop. In each loop iteration, the learner learns a policy
together with an RASM candidate as two neural networks $\pi_{\theta}$ and
$V_{\nu}$, with $\theta$ and $\nu$ being vectors of neural network parameters.
The verifier then formally verifies whether the learned RASM candidate is
indeed an RASM for the system and the learned policy. If the answer is
positive, then the algorithm concludes that the learned policy provides formal
reach-avoid guarantees. Otherwise, the verifier computes a counterexample
which shows that the learned RASM candidate is not an RASM. The counterexample
is passed to the learner and used to modify the loss function towards learning
a new policy and an RASM candidate. The loop is repeated until either a
candidate is successfully verified or the algorithm reaches a specified
timeout. The algorithm is presented in Algorithm 1. We note that our algorithm
can also verify whether a given Lipschitz continuous policy provides reach-
avoid guarantees, by fixing the policy only learning the RASM neural network.

Algorithm 1 Algorithm for learning reach-avoid policies

1:Input $f$, $d$, $\mathcal{X}$,
$\mathcal{X}_{0},\mathcal{X}_{t},\mathcal{X}_{u}$, $L_{f}$, $p\in[0,1]$

2:Parameters mesh $\tau>0$, number of samples $N\in\mathbb{N}$, regularization
constant $\lambda>0$

3:$\pi_{\theta}\leftarrow$ trained by PPO

4:$\tilde{\mathcal{X}}\leftarrow$ discretization of $\mathcal{X}$ with mesh
$\tau$

5:$C_{\text{init}},\,C_{\text{unsafe}},\,C_{\text{decrease}}\leftarrow\tilde{\mathcal{X}}\cap\mathcal{X}_{0},\,\tilde{\mathcal{X}}\cap\mathcal{X}_{u},\,\tilde{\mathcal{X}}\cap(\mathcal{X}\backslash\mathcal{X}_{t})$

6:$V_{\nu}\leftarrow$ trained by minimizing the loss function

7:while timeout not reached do

8: $L_{\pi},L_{V}\leftarrow$ Lipschitz constants of $\pi_{\theta}$, $V_{\nu}$

9: $K\leftarrow L_{V}\cdot(L_{f}\cdot(L_{\pi}+1)+1)$

10: $\tilde{\mathcal{X}_{e}}\leftarrow$ vertices of discr.
$\tilde{\mathcal{X}}$ whose adjacent cells intersect
$\mathcal{X}\backslash\mathcal{X}_{t}$ and contain $\mathbf{x}$ s.t.
$V_{\nu}(\mathbf{x})<\frac{1}{1-p}$

11:
$\text{Cells}_{\mathcal{X}_{0}},\,\text{Cells}_{\mathcal{X}_{u}}\leftarrow$
discr. cells that intersect $\mathcal{X}_{0},\,\mathcal{X}_{u}$

12: if
$\exists\tilde{\mathbf{x}}\in\tilde{\mathcal{X}_{e}}\cap(\mathcal{X}\backslash\mathcal{X}_{t})$
s.t. $\mathbb{E}_{\omega\sim
d}[V_{\nu}(f(\tilde{\mathbf{x}},\pi(\tilde{\mathbf{x}}),\omega))]\geq
V_{\nu}(\tilde{\mathbf{x}})-\tau\cdot K$ and
$V_{\nu}(\tilde{\mathbf{x}})<\frac{1}{1-p}$ then

13: $C_{\text{decrease}}\leftarrow C_{\text{decrease}}\cup\\{\mathbf{x}\\}$

14: else if $\exists\text{cell}\in\text{Cells}_{\mathcal{X}_{0}}$ s.t.
$\sup_{\mathbf{x}\in\text{cell}}V_{\nu}(\mathbf{x})>1$ then

15: $C_{\text{init}}\leftarrow C_{\text{init}}\cup(\\{\text{vertices of
cell}\\}\cap\mathcal{X}_{0})$

16: else if $\exists\text{cell}\in\text{Cells}_{\mathcal{X}_{u}}$ s.t.
$\inf_{\mathbf{x}\in\text{cell}}V_{\nu}(\mathbf{x})<\frac{1}{1-p}$ then

17: $C_{\text{unsafe}}\leftarrow C_{\text{unsafe}}\cup(\\{\text{vertices of
cell}\\}\cap\mathcal{X}_{u})$

18: else

19: Return Reach-avoid guarantee with probability $p$

20: end if

21: $V_{\nu},\pi_{\theta},\leftarrow$ trained by minimizing the loss function

22: $\tilde{\mathcal{X}}\leftarrow$ refined discretization

23:end while

24:Return Unknown

Policy Initialization Learning two networks concurrently with multiple
objectives can be unstable due to dependencies between the two networks and
differences in the scale of the objective loss terms. To mitigate these
instabilities, we propose pre-training of the policy network so that our
algorithm starts from a proper initialization. In particular, from the given
dynamical system and the safety specification, we induce a Markov decision
process (MDP) intending to reach the target set while avoiding the unsafe set.
The reward term $r_{t}$ is given by
$r_{t}:=\mathds{1}[\mathcal{X}_{t}](\mathbf{x}_{t})-\mathds{1}[\mathcal{X}_{u}](\mathbf{x}_{t})$
and we use proximal policy optimization (PPO) (Schulman et al. 2017) to train
the policy.

State Space Discretization When it comes to verifying learned candidates, the
key difficulty lies in checking the Expected decrease condition. This is
because, in general, it is not possible to compute a closed form expression
for the expected value of an RASM over successor system states, as both the
policy and the RASM are neural networks. In order to overcome this difficulty,
our algorithm discretizes the state space of the system. Given a mesh
parameter $\tau>0$, a discretization $\tilde{\mathcal{X}}$ of $\mathcal{X}$
with mesh $\tau$ is a set of states such that, for every
$\mathbf{x}\in\mathcal{X}$, there exists a state
$\tilde{\mathbf{x}}\in\tilde{\mathcal{X}}$ such that
$||\mathbf{x}-\tilde{\mathbf{x}}||_{1}<\tau$. Due to $\mathcal{X}$ being
compact and therefore bounded, for any $\tau>0$ it is possible to compute its
finite discretization with mesh $\tau$ by simply considering vertices of a
grid with sufficiently small cells. Note that $f$, $\pi_{\theta}$ and
$V_{\nu}$ are all continuous, hence due to $\mathcal{X}$ being compact $f$,
$\pi_{\theta}$ and $V_{\nu}$ are also Lipschitz continuous. This will allow us
to verify that the Expected decrease condition is satisfied by checking a
slightly stricter condition only at the vertices of the discretization grid.

Figure 1: Visualization of a neural network RSM (Lechner et al. 2022) and our
RASM on the inverted pendulum task. The RASM provides better probability
bounds of reaching the unsafe states.

The initial discretization $\tilde{\mathcal{X}}$ is also used to initialize
counterexample sets used by the learner. In particular, the learner
initializes three sets
$C_{\text{init}}=\tilde{\mathcal{X}}\cap\mathcal{X}_{0}$,
$C_{\text{unsafe}}=\tilde{\mathcal{X}}\cap\mathcal{X}_{u}$ and
$C_{\text{decrease}}=\tilde{\mathcal{X}}\cap(\mathcal{X}\backslash\mathcal{X}_{t})$.
These sets will later be extended by counterexamples computed by the verifier.
Conversely, the discretization used by the verifier for checking the defining
properties of RASMs will at each iteration of the loop be refined by a
discretization with a smaller mesh, in order to relax the conditions that are
checked by the verifier.

Verifier We now describe the verifier module of our algorithm. Suppose that
the learner has learned a policy $\pi_{\theta}$ and an RASM candidate
$V_{\nu}$. Since $V_{\nu}$ is a neural network, we know that it is a
continuous function. Furthermore, we design the learner to apply a softplus
activation function to the output layer of $V_{\nu}$, which ensures that the
Nonnegativity condition of RASMs is satisfied by default. Thus, the verifier
only needs to check the Initial, Safety and Expected decrease conditions in
Definition 1.

Let $L_{f}$, $L_{\pi}$ and $L_{V}$ be the Lipschitz constants of $f$,
$\pi_{\theta}$ and $V_{\nu}$, respectively. We assume that a Lipschitz
constant for the dynamics function $f$ is provided, and use the method of
(Szegedy et al. 2014) to compute Lipschitz constants of neural networks
$\pi_{\theta}$ and $V_{\nu}$. To verify the Expected decrease condition, the
verifier collects the superset $\tilde{\mathcal{X}_{e}}$ of discretization
points whose adjacent grid cells contain a non-target state and over which
$V_{\nu}$ attains a value that is smaller than $\frac{1}{1-p}$. This set is
computed by first collecting all cells that intersect
$\mathcal{X}\backslash\mathcal{X}_{t}$, then using interval arithmetic
abstract interpretation (IA-AI) (Cousot and Cousot 1977; Gowal et al. 2018)
which propagates interval bounds across neural network layers in order to
bound from below the minimal value that $V_{\nu}$ attains over each collected
cell, and finally collecting vertices of all cells at which this lower bound
is less than $\frac{1}{1-p}$. The verifier then checks a stricter condition
for each state $\tilde{\mathbf{x}}\in\tilde{\mathcal{X}_{e}}$:

$\mathbb{E}_{\omega\sim
d}\Big{[}V_{\nu}\Big{(}f(\tilde{\mathbf{x}},\pi_{\theta}(\tilde{\mathbf{x}}),\omega)\Big{)}\Big{]}<V_{\nu}(\tilde{\mathbf{x}})-\tau\cdot
K,$ (1)

where $K=L_{V}\cdot(L_{f}\cdot(L_{\pi}+1)+1)$. The expected value in eq. (1)
is also bounded from above via IA-AI, where one partitions the support of $d$
into intervals, propagates intervals and multiplies each interval bound by its
probability weight in order to bound the expected value of a neural network
function over a probability distribution. Due to space restrictions, we
provide more details on expected value computation in the Appendix and note
that this method requires that the probability distribution $d$ either has
bounded support or is a product of independent univariate distributions.

In order to verify the Initial condition, the verifier collects the set
$\text{Cells}_{\mathcal{X}_{0}}$ of all cells of the discretization grid that
intersect the initial set $\mathcal{X}_{0}$. Then, for each
$\text{cell}\in\text{Cells}_{\mathcal{X}_{0}}$, it checks whether

$\sup_{\mathbf{x}\,\in\,\text{cell}}V_{\nu}(\mathbf{x})>1,$ (2)

where the supremum of $V_{\nu}$ over the cell is bounded from above by using
IA-AI. Similarly, to verify the Unsafe condition, the verifier collects the
set $\text{Cells}_{\mathcal{X}_{u}}$ of all cells of the discretization grid
that intersect the unsafe set $\mathcal{X}_{u}$. Then, for each
$\text{cell}\in\text{Cells}_{\mathcal{X}_{u}}$, it uses IA-AI to check whether

$\inf_{\mathbf{x}\,\in\,\text{cell}}V_{\nu}(\mathbf{x})<\frac{1}{1-p}.$ (3)

If the verifier shows that $V_{\nu}$ satisfies eq. (1) for each
$\tilde{\mathbf{x}}\in\tilde{\mathcal{X}_{e}}$, eq. (2) for each
$\text{cell}\in\text{Cells}_{\mathcal{X}_{0}}$ and eq. (3) for each
$\text{cell}\in\text{Cells}_{\mathcal{X}_{u}}$, it concludes that $V_{\nu}$ is
an RASM. Otherwise, if a counterexample $\tilde{\mathbf{x}}$ to eq. (1) is
found and we have $\tilde{\mathbf{x}}\in\mathcal{X}\backslash\mathcal{X}_{t}$
and $V_{\nu}(\mathbf{x})<\frac{1}{1-p}$, it is added to $C_{\text{decrease}}$.
Similarly, if counterexample cells to eq. (2) and eq. (3) are found, all their
vertices that are contained in $\mathcal{X}_{0}$ and $\mathcal{X}_{u}$ are
added to $C_{\text{init}}$ and $C_{\text{unsafe}}$, respectively.

The following theorem shows that checking the above conditions is sufficient
to formally verify whether an RASM candidate is indeed an RASM. The proof
follows by exploiting the fact that $f$, $\pi_{\theta}$ and $V_{\nu}$ are all
Lipschitz continuous and that $\mathcal{X}$ is compact, and we include it in
the Appendix.

######  Theorem 2.

Suppose that the verifier verifies that $V_{\nu}$ satisfies eq. (1) for each
$\tilde{\mathbf{x}}\in\tilde{\mathcal{X}_{e}}$, eq. (2) for each
$\text{cell}\in\text{Cells}_{\mathcal{X}_{0}}$ and eq. (3) for each
$\text{cell}\in\text{Cells}_{\mathcal{X}_{u}}$. Then the function $V_{\nu}$ is
an RASM for the system with respect to $\mathcal{X}_{t}$, $\mathcal{X}_{u}$
and $p$.

Learner A policy and an RASM candidate are learned by minimizing the loss
function

$\begin{split}\mathcal{L}(\theta,\nu)=&\mathcal{L}_{\text{Init}}(\nu)+\mathcal{L}_{\text{Unsafe}}(\nu)+\mathcal{L}_{\text{Decrease}}(\theta,\nu)\\\
&+\lambda\cdot\big{(}\mathcal{L}_{\textrm{Lipschitz}}(\theta)+\mathcal{L}_{\textrm{Lipschitz}}(\nu)\big{)}.\end{split}$

The first three loss terms are used to guide the learner towards learning a
true RASM by forcing the learned candidate towards satisfying the Initial,
Safety and Expected decrease conditions in Definition 1. They are defined as
follows:

$\begin{split}&\mathcal{L}_{\text{Init}}(\nu)=\max_{\mathbf{x}\in
C_{\text{init}}}\\{V_{\nu}(\mathbf{x})-1,0\\}\\\
&\mathcal{L}_{\text{Unsafe}}(\nu)=\max_{\mathbf{x}\in
C_{\text{unsafe}}}\\{\frac{1}{1-p}-V_{\nu}(\mathbf{x}),0\\}\\\
&\mathcal{L}_{\text{Decrease}}(\theta,\nu)=\frac{1}{|C_{\text{decrease}}|}\cdot\\\
&\sum_{\mathbf{x}\in
C_{\text{decrease}}}\Big{(}\max\Big{\\{}\sum_{\omega_{1},\dots,\omega_{N}\sim\mathcal{N}}\frac{V_{\nu}\big{(}f(\mathbf{x},\pi_{\theta}(\mathbf{x}),\omega_{i})\big{)}}{N}\\\
&\hskip 28.45274pt-V_{\theta}(\mathbf{x})+\tau\cdot
K,0\Big{\\}}\Big{)}\end{split}$

Each loss term is designed to incur a loss at a state whenever that state
violates the corresponding condition in Definition 1 that needs to be checked
by the verifier. In the expression for
$\mathcal{L}_{\text{Decrease}}(\theta,\nu)$, we approximate the expected value
of $V_{\nu}$ by taking the mean value of $V_{\nu}$ at $N$ sampled successor
states, where $N\in\mathbb{N}$ is an algorithm parameter. This is necessary as
it is not possible to compute a closed form expression for the expected value
of a neural network $V_{\nu}$.

The last loss term
$\lambda\cdot(\mathcal{L}_{\textrm{Lipschitz}}(\theta)+\mathcal{L}_{\textrm{Lipschitz}}(\nu))$
is the regularization term used to guide the learner towards a policy and an
RASM candidate with Lipschitz constants below a tolerable threshold $\rho$,
with $\lambda>0$ being a regularization constant. By preferring networks with
small Lipschitz constants, we allow the verifier to use a wider mesh, which
significantly speeds up the verification process. The regularization term for
$\pi_{\theta}$ (and analogously for $V_{\nu}$) is defined via

$\mathcal{L}_{\text{Lipschitz}}(\theta)=\max\Big{\\{}\prod_{W,b\in\theta}\max_{j}\sum_{i}|W_{i,j}|-\rho,0\Big{\\}},$

where $W$ and $b$ weight matrices and bias vectors for each layer in
$\pi_{\theta}$. Finally, in our implementation we also add an auxiliary loss
term that does not enforce any of the defining conditions of RASMs, however it
is used to guide the learner towards a candidate that attains the global
minimum in a state that is contained within the target set $\mathcal{X}_{t}$.
We empirically observed that this term sometimes helps the updated policy from
diverging from its objective to stabilize the system. Due to space
restrictions, details are provided in the Appendix.

We remark that the loss function is always nonnegative but is not necessarily
equal to $0$ even if $V_{\nu}$ satisfies all conditions checked by the
verifier and if Lipschitz constants are below the specified thresholds. This
is because the expected values in $\mathcal{L}_{\text{Decrease}}(\theta,\nu)$
are approximated via sample means. However, in the following theorem we show
that in this case $\mathcal{L}(\theta,\nu)\rightarrow 0$ with probability $1$
as we add independent samples. The claim follows from the Strong Law of Large
Numbers and the proof can be found in the Appendix.

######  Theorem 3.

Let $N$ be the number of samples used to approximate expected values in
$\mathcal{L}_{\text{Decrease}}(\theta,\nu)$. Suppose that $V_{\nu}$ satisfies
eq. (1) for each $\tilde{\mathbf{x}}\in\tilde{\mathcal{X}_{e}}$, eq. (2) for
each $\text{cell}\in\text{Cells}_{\mathcal{X}_{0}}$ and eq. (3) for each
$\text{cell}\in\text{Cells}_{\mathcal{X}_{u}}$. Suppose that Lipschitz
constants of $\pi_{\theta}$ and $V_{\nu}$ are below the thresholds specified
by $\mathcal{L}_{\text{Lipschitz}}(\theta)$ and
$\mathcal{L}_{\text{Lipschitz}}(\nu)$ and that the samples in
$\mathcal{L}_{\text{Decrease}}(\theta,\nu)$ are independent. Then
$\lim_{N\rightarrow\infty}\mathcal{L}(\theta,\nu)=0$ with probability $1$.

| RSM | RASM
---|---|---
Environment | (reach-avoid extension) | (ours)
2D system | 83.4% | 93.3%
Inverted pendulum | 47.9% | 92.1%
Collision avoidance | Fail | 90.4%
Table 1: Reach-avoid probability obtained by our method and by the naive
extension of RSMs. In each case, we report the largest reach-avoid probability
successfully verified by the respective method.

## Experiments

We experimentally validate our method on 3 non-linear RL environments. Since
no available baseline provides reach-avoid guarantees of stochastic systems
over the infinite time horizon, as well as sampling and discretization
approaches can only reason over finite time horizons, we aim our experiment as
a validation of algorithm 1 in practice. We will make our JAX (Bradbury et al.
2018) implementation publicly available.

Our first two environments are a linear 2D system with non-linear control
bounds and the stochastic inverted pendulum control problem. The linear 2D
system is of the form
$\mathbf{x}_{t+1}=A\mathbf{x}_{t}+Bg(\mathbf{u}_{t})+\omega_{t}$, where
$g:u\mapsto\min(\max(u,-1,1))$ limits the admissible action of the policy and
$\omega_{t}$ is sampled from a triangular noise distribution. The inverted
pendulum environment is taken from the OpenAI Gym (Brockman et al. 2016) and
made more difficult by adding noise perturbations to its state. Our third
environment concerns a collision avoidance task. The objective of this
environment is to navigate an agent to the target region while avoiding
crashing into one of two obstacles. All environments express bounds on the
admissible actions. Further details of all environments can be found in the
Appendix.

The policy and RASM networks consist of two hidden layers (128 units each,
ReLU). The RASM network has a single output unit with a softplus activation.
We run our algorithm with a timeout of 3 hours.

The goal of our first experiment is to empirically evaluate the ability of our
approach to learn probabilistic reach-avoid policies and to understand the
importance of combining reachability with level set reasoning towards safety
in stochastic systems. For all tasks, we pre-train the policy networks using
100 iterations of PPO. To evaluate our approach, we run our algorithm with
several probability thresholds and report the highest threshold for which a
policy together with an RASM is successfully learned. In order to understand
the importance of simultaneous reasoning about reachability and level sets, we
then compare our approach with a much simpler extension of the method of
(Lechner et al. 2022) which learns RSMs to certify probability $1$
reachability but does not consider any form of safety specifications. In
particular, we run the method of (Lechner et al. 2022) without the safety
constraint and, in case a valid RSM is found, we normalize the function such
that the Nonnegativity and the Initial conditions of RASMs are satisfied. We
then bound from below the smallest value that the RSM attains over the unsafe
region, and extract the corresponding reach-avoid probability bound according
to the Safety condition of RASMs. Note that, even though this extension also
exploits the ideas behind the level set reasoning in our RASMs, it first
performs reachability analysis and only afterwards considers safety. We remark
that there is no existing method that provides reach-avoid guarantees of
stochastic systems over the infinite time horizon, i.e. there is no existing
baseline to compare against, thus we compare our level set reasoning with the
extension of (Lechner et al. 2022) which is the closest related work.

Table 1 shows results of our first experiment. In particular, in the third
column we see that our method successfully learns policies that provide high
probability reach-avoid guarantees for all benchmarks. On the other hand,
comparison to the second column shows that simultaneous reasoning about
reachability and safety that is allowed by our RASMs provides significantly
better probabilistic reach-avoid guarantees than when such reasoning is
decoupled. Figure 1 visualizes the RSM computed by the baseline and our RASM.

| $V_{\nu}$ |  $V_{\nu}$ and $\pi_{\theta}$
---|---|---
2D system | Fail (10 iters.) | 96.7% (4 iters.)
Collision avoidance | Fail (9 iters.) | 80.9% (3 iters.)
Inverted pendulum | Fail (7 iters.) | Fail (7 iters.)
Table 2: Reach-avoid probabilities obtained by repairing unsafe policies.
Verifying a policy by only learning the RASM $V_{\nu}$ times out, while
jointly optimizing $V_{\nu}$ and $\pi_{\theta}$ yields a valid RASM. In each
case, we report the largest reach-avoid probability successfully verified by
the respective method.

In our second experiment, we study how well our algorithm can _repair_ (or
_fine-tune_) an unsafe policy. In particular, we pre-train the policy network
using only 20 PPO iterations. We then run our algorithm with fixed policy
parameters $\theta$, i.e. we only learn an RASM in order to verify a
probabilistic reach-avoid guarantee provided by a pre-trained policy. Next, we
run our Algorithm 1 with both $\nu$ and $\theta$ as trainable parameters.
Table 2 shows that, compared to a standalone verification method, our
algorithm is able to repair unsafe policies in practice. However, the
inability to repair the inverted pendulum policy illustrates that a decent
starting policy is necessary for our algorithm, emphasizing the importance of
policy initialization. Since the Policy Initialization step in Algorithm 1
initialises the policy by using PPO with a reward function that encodes the
reach-avoid specification, our second experiment also demonstrates that a
policy initialised by using RL on a tailored reward function is not sufficient
to learn a reach-avoid policy with guarantees and that the learned policy
requires “correction” in order to provide reach-avoid guarantees. The
“correction” is achieved precisely by keeping the policy parameters trainable
in the learner-verifier framework and fine-tuning them.

## Conclusion

In this work, we present a method for learning controllers for discrete-time
stochastic non-linear dynamical systems with formal reach-avoid guarantees.
Our method learns a policy together with a reach-avoid supermartingale (RASM),
a novel notion that we introduce in this work. It solves several important
problems, including control with reach-avoid guarantees, verification of
reach-avoid properties for a fixed policy, or fine-tuning of a given policy
that does not satisfy a reach-avoid property. We demonstrated the
effectiveness of our approach on three RL benchmarks. An interesting future
direction would be to study certified control and verification of more general
properties in stochastic systems. Since the aim of AI safety and formal
verification is to ensure that systems do not behave in undesirable ways and
that safety violating events are avoided, we are not aware of any potential
negative societal impacts of our work.

## References

  * Abate et al. [2021] Abate, A.; Ahmed, D.; Giacobbe, M.; and Peruffo, A. 2021.  Formal Synthesis of Lyapunov Neural Networks.  _IEEE Control. Syst. Lett._ , 5(3): 773–778.
  * Abate, Giacobbe, and Roy [2021] Abate, A.; Giacobbe, M.; and Roy, D. 2021.  Learning Probabilistic Termination Proofs.  In Silva, A.; and Leino, K. R. M., eds., _Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II_ , volume 12760 of _Lecture Notes in Computer Science_ , 3–26. Springer.
  * Achiam et al. [2017] Achiam, J.; Held, D.; Tamar, A.; and Abbeel, P. 2017.  Constrained policy optimization.  In _International Conference on Machine Learning_ , 22–31. PMLR.
  * Alshiekh et al. [2018] Alshiekh, M.; Bloem, R.; Ehlers, R.; Könighofer, B.; Niekum, S.; and Topcu, U. 2018.  Safe Reinforcement Learning via Shielding.  In McIlraith, S. A.; and Weinberger, K. Q., eds., _Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018_ , 2669–2678. AAAI Press.
  * Altman [1999] Altman, E. 1999.  _Constrained Markov decision processes_ , volume 7.  CRC Press.
  * Ames et al. [2019] Ames, A. D.; Coogan, S.; Egerstedt, M.; Notomista, G.; Sreenath, K.; and Tabuada, P. 2019.  Control Barrier Functions: Theory and Applications.  In _17th European Control Conference, ECC 2019, Naples, Italy, June 25-28, 2019_ , 3420–3431. IEEE.
  * Amodei et al. [2016] Amodei, D.; Olah, C.; Steinhardt, J.; Christiano, P. F.; Schulman, J.; and Mané, D. 2016.  Concrete Problems in AI Safety.  _CoRR_ , abs/1606.06565.
  * Bastani and Li [2021] Bastani, O.; and Li, S. 2021.  Safe Reinforcement Learning via Statistical Model Predictive Shielding.  In Shell, D. A.; Toussaint, M.; and Hsieh, M. A., eds., _Robotics: Science and Systems XVII, Virtual Event, July 12-16, 2021_.
  * Berkenkamp [2019] Berkenkamp, F. 2019.  Safe Exploration in Reinforcement Learning: Theory and Applications in Robotics.
  * Bradbury et al. [2018] Bradbury, J.; Frostig, R.; Hawkins, P.; Johnson, M. J.; Leary, C.; Maclaurin, D.; Necula, G.; Paszke, A.; VanderPlas, J.; Wanderman-Milne, S.; and Zhang, Q. 2018.  JAX: composable transformations of Python+NumPy programs.
  * Brockman et al. [2016] Brockman, G.; Cheung, V.; Pettersson, L.; Schneider, J.; Schulman, J.; Tang, J.; and Zaremba, W. 2016.  OpenAI Gym.  _arXiv preprint arXiv:1606.01540_.
  * Cauchi and Abate [2019] Cauchi, N.; and Abate, A. 2019.  StocHy-automated verification and synthesis of stochastic processes.  In _Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control_ , 258–259.
  * Chakarov and Sankaranarayanan [2013] Chakarov, A.; and Sankaranarayanan, S. 2013.  Probabilistic Program Analysis with Martingales.  In Sharygina, N.; and Veith, H., eds., _Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings_ , volume 8044 of _Lecture Notes in Computer Science_ , 511–526. Springer.
  * Chang and Gao [2021] Chang, Y.; and Gao, S. 2021.  Stabilizing Neural Control Using Self-Learned Almost Lyapunov Critics.  In _IEEE International Conference on Robotics and Automation, ICRA 2021, Xi’an, China, May 30 - June 5, 2021_ , 1803–1809. IEEE.
  * Chang, Roohi, and Gao [2019] Chang, Y.; Roohi, N.; and Gao, S. 2019.  Neural Lyapunov Control.  In Wallach, H. M.; Larochelle, H.; Beygelzimer, A.; d’Alché-Buc, F.; Fox, E. B.; and Garnett, R., eds., _Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada_ , 3240–3249.
  * Chatterjee et al. [2022] Chatterjee, K.; Goharshady, A. K.; Meggendorfer, T.; and Zikelic, D. 2022.  Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs.  In Shoham, S.; and Vizel, Y., eds., _Computer Aided Verification \- 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I_ , volume 13371 of _Lecture Notes in Computer Science_ , 55–78. Springer.
  * Chatterjee, Novotný, and Zikelic [2017] Chatterjee, K.; Novotný, P.; and Zikelic, D. 2017.  Stochastic invariants for probabilistic termination.  In Castagna, G.; and Gordon, A. D., eds., _Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017_ , 145–160. ACM.
  * Chow et al. [2018] Chow, Y.; Nachum, O.; Duéñez-Guzmán, E. A.; and Ghavamzadeh, M. 2018.  A Lyapunov-based Approach to Safe Reinforcement Learning.  In Bengio, S.; Wallach, H. M.; Larochelle, H.; Grauman, K.; Cesa-Bianchi, N.; and Garnett, R., eds., _Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada_ , 8103–8112.
  * Cousot and Cousot [1977] Cousot, P.; and Cousot, R. 1977.  Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints.  In Graham, R. M.; Harrison, M. A.; and Sethi, R., eds., _Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977_ , 238–252. ACM.
  * Crespo and Sun [2003] Crespo, L. G.; and Sun, J. 2003.  Stochastic optimal control via Bellman’s principle.  _Autom._ , 39(12): 2109–2114.
  * Dalal et al. [2018] Dalal, G.; Dvijotham, K.; Vecerík, M.; Hester, T.; Paduraru, C.; and Tassa, Y. 2018.  Safe Exploration in Continuous Action Spaces.  _ArXiv_ , abs/1801.08757.
  * Elsayed-Aly et al. [2021] Elsayed-Aly, I.; Bharadwaj, S.; Amato, C.; Ehlers, R.; Topcu, U.; and Feng, L. 2021.  Safe Multi-Agent Reinforcement Learning via Shielding.  In Dignum, F.; Lomuscio, A.; Endriss, U.; and Nowé, A., eds., _AAMAS ’21: 20th International Conference on Autonomous Agents and Multiagent Systems, Virtual Event, United Kingdom, May 3-7, 2021_ , 483–491. ACM.
  * García and Fernández [2015] García, J.; and Fernández, F. 2015.  A comprehensive survey on safe reinforcement learning.  _J. Mach. Learn. Res._ , 16: 1437–1480.
  * Geibel [2006] Geibel, P. 2006.  Reinforcement Learning for MDPs with Constraints.  In Fürnkranz, J.; Scheffer, T.; and Spiliopoulou, M., eds., _Machine Learning: ECML 2006, 17th European Conference on Machine Learning, Berlin, Germany, September 18-22, 2006, Proceedings_ , volume 4212 of _Lecture Notes in Computer Science_ , 646–653. Springer.
  * Giacobbe et al. [2021] Giacobbe, M.; Hasanbeig, M.; Kroening, D.; and Wijk, H. 2021.  Shielding Atari Games with Bounded Prescience.  In Dignum, F.; Lomuscio, A.; Endriss, U.; and Nowé, A., eds., _AAMAS ’21: 20th International Conference on Autonomous Agents and Multiagent Systems, Virtual Event, United Kingdom, May 3-7, 2021_ , 1507–1509. ACM.
  * Gowal et al. [2018] Gowal, S.; Dvijotham, K.; Stanforth, R.; Bunel, R.; Qin, C.; Uesato, J.; Arandjelovic, R.; Mann, T. A.; and Kohli, P. 2018.  On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models.  _CoRR_ , abs/1810.12715.
  * Haddad and Chellaboina [2011] Haddad, W. M.; and Chellaboina, V. 2011.  _Nonlinear dynamical systems and control_.  Princeton university press.
  * Hasanbeig, Abate, and Kroening [2020] Hasanbeig, M.; Abate, A.; and Kroening, D. 2020.  Cautious Reinforcement Learning with Logical Constraints.  In Seghrouchni, A. E. F.; Sukthankar, G.; An, B.; and Yorke-Smith, N., eds., _Proceedings of the 19th International Conference on Autonomous Agents and Multiagent Systems, AAMAS ’20, Auckland, New Zealand, May 9-13, 2020_ , 483–491. International Foundation for Autonomous Agents and Multiagent Systems.
  * Henrion and Garulli [2005] Henrion, D.; and Garulli, A. 2005.  _Positive polynomials in control_ , volume 312.  Springer Science & Business Media.
  * Jarvis-Wloszek et al. [2003] Jarvis-Wloszek, Z.; Feeley, R.; Tan, W.; Sun, K.; and Packard, A. 2003.  Some controls applications of sum of squares programming.  In _42nd IEEE international conference on decision and control (IEEE Cat. No. 03CH37475)_ , volume 5, 4676–4681. IEEE.
  * Jin et al. [2020] Jin, W.; Wang, Z.; Yang, Z.; and Mou, S. 2020.  Neural Certificates for Safe Control Policies.  _CoRR_ , abs/2006.08465.
  * Kingma and Ba [2014] Kingma, D. P.; and Ba, J. 2014.  Adam: A method for stochastic optimization.  _arXiv preprint arXiv:1412.6980_.
  * Koller et al. [2018] Koller, T.; Berkenkamp, F.; Turchetta, M.; and Krause, A. 2018.  Learning-Based Model Predictive Control for Safe Exploration.  _2018 IEEE Conference on Decision and Control (CDC)_ , 6059–6066.
  * Kushner [2014] Kushner, H. J. 2014.  A partial history of the early development of continuous-time nonlinear stochastic systems theory.  _Autom._ , 50(2): 303–334.
  * Lavaei et al. [2020] Lavaei, A.; Khaled, M.; Soudjani, S.; and Zamani, M. 2020.  AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems.  In Lahiri, S. K.; and Wang, C., eds., _Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II_ , volume 12225 of _Lecture Notes in Computer Science_ , 461–474. Springer.
  * Lawrence et al. [2020] Lawrence, N. P.; Loewen, P. D.; Forbes, M. G.; Backström, J. U.; and Gopaluni, R. B. 2020.  Almost Surely Stable Deep Dynamics.  In Larochelle, H.; Ranzato, M.; Hadsell, R.; Balcan, M.; and Lin, H., eds., _Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual_.
  * Lechner et al. [2021] Lechner, M.; Zikelic, D.; Chatterjee, K.; and Henzinger, T. A. 2021.  Infinite Time Horizon Safety of Bayesian Neural Networks.  In Ranzato, M.; Beygelzimer, A.; Dauphin, Y. N.; Liang, P.; and Vaughan, J. W., eds., _Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual_ , 10171–10185.
  * Lechner et al. [2022] Lechner, M.; Zikelic, D.; Chatterjee, K.; and Henzinger, T. A. 2022.  Stability Verification in Stochastic Control Systems via Neural Network Supermartingales.  In _Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 - March 1, 2022_ , 7326–7336. AAAI Press.
  * Li and Bastani [2020] Li, S.; and Bastani, O. 2020.  Robust Model Predictive Shielding for Safe Reinforcement Learning with Stochastic Dynamics.  In _2020 IEEE International Conference on Robotics and Automation, ICRA 2020, Paris, France, May 31 - August 31, 2020_ , 7166–7172. IEEE.
  * Liu et al. [2020] Liu, A.; Shi, G.; Chung, S.-J.; Anandkumar, A.; and Yue, Y. 2020.  Robust Regression for Safe Exploration in Control.  In _L4DC_.
  * Michalska and Mayne [1993] Michalska, H.; and Mayne, D. Q. 1993.  Robust receding horizon control of constrained nonlinear systems.  _IEEE Trans. Autom. Control._ , 38(11): 1623–1633.
  * Murphy [2012] Murphy, K. P. 2012.  _Machine learning - a probabilistic perspective_.  Adaptive computation and machine learning series. MIT Press.  ISBN 0262018020.
  * Parrilo [2000] Parrilo, P. A. 2000.  _Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization_.  California Institute of Technology.
  * Perkins and Barto [2002] Perkins, T. J.; and Barto, A. G. 2002.  Lyapunov Design for Safe Reinforcement Learning.  _J. Mach. Learn. Res._ , 3: 803–832.
  * Prajna, Jadbabaie, and Pappas [2007] Prajna, S.; Jadbabaie, A.; and Pappas, G. J. 2007.  A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates.  _IEEE Trans. Autom. Control._ , 52(8): 1415–1428.
  * Puterman [1994] Puterman, M. L. 1994.  _Markov Decision Processes: Discrete Stochastic Dynamic Programming_.  Wiley Series in Probability and Statistics. Wiley.  ISBN 978-0-47161977-2.
  * Qin et al. [2021] Qin, Z.; Zhang, K.; Chen, Y.; Chen, J.; and Fan, C. 2021.  Learning Safe Multi-agent Control with Decentralized Neural Barrier Certificates.  In _9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021_. OpenReview.net.
  * Richards, Berkenkamp, and Krause [2018] Richards, S. M.; Berkenkamp, F.; and Krause, A. 2018.  The Lyapunov Neural Network: Adaptive Stability Certification for Safe Learning of Dynamical Systems.  In _2nd Annual Conference on Robot Learning, CoRL 2018, Zürich, Switzerland, 29-31 October 2018, Proceedings_ , volume 87 of _Proceedings of Machine Learning Research_ , 466–476. PMLR.
  * Santoyo, Dutreix, and Coogan [2021] Santoyo, C.; Dutreix, M.; and Coogan, S. 2021.  A barrier function approach to finite-time stochastic system verification and control.  _Autom._ , 125: 109439.
  * Schulman et al. [2017] Schulman, J.; Wolski, F.; Dhariwal, P.; Radford, A.; and Klimov, O. 2017.  Proximal policy optimization algorithms.  _arXiv preprint arXiv:1707.06347_.
  * Soudjani, Gevaerts, and Abate [2015] Soudjani, S. E. Z.; Gevaerts, C.; and Abate, A. 2015.  FAUST ${}^{\mbox{ 2}}$ : Formal Abstractions of Uncountable-STate STochastic Processes.  In Baier, C.; and Tinelli, C., eds., _Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings_ , volume 9035 of _Lecture Notes in Computer Science_ , 272–286. Springer.
  * Steinhardt and Tedrake [2012] Steinhardt, J.; and Tedrake, R. 2012.  Finite-time regional verification of stochastic non-linear systems.  _Int. J. Robotics Res._ , 31(7): 901–923.
  * Summers and Lygeros [2010] Summers, S.; and Lygeros, J. 2010.  Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem.  _Autom._ , 46(12): 1951–1961.
  * Sun, Jha, and Fan [2020] Sun, D.; Jha, S.; and Fan, C. 2020.  Learning Certified Control Using Contraction Metric.  In Kober, J.; Ramos, F.; and Tomlin, C. J., eds., _4th Conference on Robot Learning, CoRL 2020, 16-18 November 2020, Virtual Event / Cambridge, MA, USA_ , volume 155 of _Proceedings of Machine Learning Research_ , 1519–1539. PMLR.
  * Sutton and Barto [2018] Sutton, R. S.; and Barto, A. G. 2018.  _Reinforcement learning: An introduction_.  MIT press.
  * Szegedy et al. [2014] Szegedy, C.; Zaremba, W.; Sutskever, I.; Bruna, J.; Erhan, D.; Goodfellow, I. J.; and Fergus, R. 2014.  Intriguing properties of neural networks.  In Bengio, Y.; and LeCun, Y., eds., _2nd International Conference on Learning Representations, ICLR 2014, Banff, AB, Canada, April 14-16, 2014, Conference Track Proceedings_.
  * Turchetta, Berkenkamp, and Krause [2019] Turchetta, M.; Berkenkamp, F.; and Krause, A. 2019.  Safe Exploration for Interactive Machine Learning.  In _NeurIPS_.
  * Uchibe and Doya [2007] Uchibe, E.; and Doya, K. 2007.  Constrained reinforcement learning from intrinsic and extrinsic rewards.  In _2007 IEEE 6th International Conference on Development and Learning_ , 163–168. IEEE.
  * Umlauft and Hirche [2017] Umlauft, J.; and Hirche, S. 2017.  Learning Stable Stochastic Nonlinear Dynamical Systems.  In Precup, D.; and Teh, Y. W., eds., _Proceedings of the 34th International Conference on Machine Learning, ICML 2017, Sydney, NSW, Australia, 6-11 August 2017_ , volume 70 of _Proceedings of Machine Learning Research_ , 3502–3510. PMLR.
  * Vahidi and Eskandarian [2003] Vahidi, A.; and Eskandarian, A. 2003.  Research advances in intelligent collision avoidance and adaptive cruise control.  _IEEE Trans. Intell. Transp. Syst._ , 4(3): 143–153.
  * Vaidya [2015] Vaidya, U. 2015.  Stochastic stability analysis of discrete-time system using Lyapunov measure.  In _American Control Conference, ACC 2015, Chicago, IL, USA, July 1-3, 2015_ , 4646–4651. IEEE.
  * Vinod, Gleason, and Oishi [2019] Vinod, A. P.; Gleason, J. D.; and Oishi, M. M. K. 2019.  SReachTools: a MATLAB stochastic reachability toolbox.  In Ozay, N.; and Prabhakar, P., eds., _Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019_ , 33–38. ACM.
  * Wabersich and Zeilinger [2018] Wabersich, K. P.; and Zeilinger, M. N. 2018.  Linear Model Predictive Safety Certification for Learning-Based Control.  In _57th IEEE Conference on Decision and Control, CDC 2018, Miami, FL, USA, December 17-19, 2018_ , 7130–7135. IEEE.
  * Williams [1991] Williams, D. 1991.  _Probability with Martingales_.  Cambridge mathematical textbooks. Cambridge University Press.  ISBN 978-0-521-40605-5.
  * Xue et al. [2021] Xue, B.; Li, R.; Zhan, N.; and Fränzle, M. 2021.  Reach-avoid Analysis for Stochastic Discrete-time Systems.  In _2021 American Control Conference, ACC 2021, New Orleans, LA, USA, May 25-28, 2021_ , 4879–4885. IEEE.

## Acknowledgments

This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818
(FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.
Research was sponsored by the United States Air Force Research Laboratory and
the United States Air Force Artificial Intelligence Accelerator and was
accomplished under Cooperative Agreement Number FA8750-19-2-1000. The views
and conclusions contained in this document are those of the authors and should
not be interpreted as representing the official policies, either expressed or
implied, of the United States Air Force or the U.S. Government. The U.S.
Government is authorized to reproduce and distribute reprints for Government
purposes notwithstanding any copyright notation herein. The research was also
funded in part by the AI2050 program at Schmidt Futures (Grant G-22-63172) and
Capgemini SE.

Appendix

## Overview of Martingale Theory

### Probability theory

A probability space is a triple $(\Omega,\mathcal{F},\mathbb{P})$, where
$\Omega$ is a non-empty sample space, $\mathcal{F}$ is a $\sigma$-algebra over
$\Omega$ (i.e. a collection of subsets of $\Omega$ that contains the empty set
$\emptyset$ and is closed under complementation and countable union
operations), and $\mathbb{P}$ is a probability measure over $\mathcal{F}$,
i.e. a function $\mathbb{P}:\mathcal{F}\rightarrow[0,1]$ that satisfies
Kolmogorov axioms [64]. We call the elements of $\mathcal{F}$ events. Given a
probability space $(\Omega,\mathcal{F},\mathbb{P})$, a random variable is a
function $X:\Omega\rightarrow\mathbb{R}$ that is $\mathcal{F}$-measurable,
i.e. for each $a\in\mathbb{R}$ we have that $\\{\omega\in\Omega\mid
X(\omega)\leq a\\}\in\mathcal{F}$. We use $\mathbb{E}[X]$ to denote the
expected value of $X$. A (discrete-time) stochastic process is a sequence
$(X_{i})_{i=0}^{\infty}$ of random variables in
$(\Omega,\mathcal{F},\mathbb{P})$.

### Conditional expectation

In order to formally define supermartingales, we need to introduce conditional
expectation. Let $X$ be a random variable in a probability space
$(\Omega,\mathcal{F},\mathbb{P})$. Given a sub-$\sigma$-algebra
$\mathcal{F}^{\prime}\subseteq\mathcal{F}$, a conditional expectation of $X$
given $\mathcal{F}^{\prime}$ is an $\mathcal{F}^{\prime}$-measurable random
variable $Y$ such that, for each $A\in\mathcal{F}^{\prime}$, we have

$\mathbb{E}[X\cdot\mathbb{I}(A)]=\mathbb{E}[Y\cdot\mathbb{I}(A)].$

The function $\mathbb{I}(A):\Omega\rightarrow\\{0,1\\}$ is an indicator
function of $A$, defined via $\mathbb{I}(A)(\omega)=1$ if $\omega\in A$, and
$\mathbb{I}(A)(\omega)=0$ if $\omega\not\in A$. Intuitively, conditional
expectation of $X$ given $\mathcal{F}^{\prime}$ is an
$\mathcal{F}^{\prime}$-measurable random variable that behaves like $X$
whenever its expected value is taken over an event in $\mathcal{F}^{\prime}$.
It is known that a conditional expectation of a random variable $X$ given
$\mathcal{F}^{\prime}$ exists if $X$ is real-valued and nonnegative [64].
Moreover, for any two $\mathcal{F}^{\prime}$-measurable random variables $Y$
and $Y^{\prime}$ which are conditional expectations of $X$ given
$\mathcal{F}^{\prime}$, we have that $\mathbb{P}[Y=Y^{\prime}]=1$. Therefore,
the conditional expectation is almost-surely unique and we may pick any such
random variable as a canonical conditional expectation and denote it by
$\mathbb{E}[X\mid\mathcal{F}^{\prime}]$.

### Supermartingales

We are now ready to define supermartingales. Let
$(\Omega,\mathcal{F},\mathbb{P})$ be a probability space and
$(\mathcal{F}_{i})_{i=0}^{\infty}$ be an increasing sequence of
sub-$\sigma$-algebras in $\mathcal{F}$, i.e.
$\mathcal{F}_{0}\subseteq\mathcal{F}_{1}\subseteq\dots\subseteq\mathcal{F}$. A
nonnegative supermartingale with respect to $(\mathcal{F}_{i})_{i=0}^{\infty}$
is a stochastic process $(X_{i})_{i=0}^{\infty}$ such that each $X_{i}$ is
$\mathcal{F}_{i}$-measurable, and $X_{i}(\omega)\geq 0$ and
$\mathbb{E}[X_{i+1}\mid\mathcal{F}_{i}](\omega)\leq X_{i}(\omega)$ hold for
each $\omega\in\Omega$ and $i\geq 0$. Intuitively, the second condition says
that the expected value of $X_{i+1}$ given the value of $X_{i}$ has to
decrease, and this requirement is formally captured via conditional
expectation.

We now present two results that will be key ingredients in the proof of
Theorem 1. The first is Doob’s Supermartingale Convergence Theorem (see [64],
Section 11) which shows that every nonnegative supermartingale converges
almost-surely to some finite value. The second theorem (see [34], Theorem 7.1)
provides a bound on the probability that the value of the supemartingale ever
exceeds some threshold, and it will allow us to reason about both
probabilistic reachability and safety. This is a less standard result from
martingale theory, so we prove it below. In what follows, let
$(\Omega,\mathcal{F},\mathbb{P})$ be a probability space and
$(\mathcal{F}_{i})_{i=0}^{\infty}$ be an increasing sequence of
sub-$\sigma$-algebras in $\mathcal{F}$.

######  Theorem 4 (Supermartingale convergence theorem).

Let $(X_{i})_{i=0}^{\infty}$ be a nonnegative supermartingale with respect to
$(\mathcal{F}_{i})_{i=0}^{\infty}$. Then, there exists a random variable
$X_{\infty}$ in $(\Omega,\mathcal{F},\mathbb{P})$ to which the supermartingale
converges to with probability $1$, i.e.
$\mathbb{P}[\lim_{i\rightarrow\infty}X_{i}=X_{\infty}]=1$.

######  Theorem 5.

Let $(X_{i})_{i=0}^{\infty}$ be a nonnegative supermartingale with respect to
$(\mathcal{F}_{i})_{i=0}^{\infty}$. Then, for every $\lambda>0$, we have

$\mathbb{P}\Big{[}\sup_{i\geq
0}X_{i}\geq\lambda\Big{]}\leq\frac{\mathbb{E}[X_{0}]}{\lambda}.$

###### Proof.

Fix $\lambda>0$. Define a stopping time
$T:\Omega\rightarrow\mathbb{N}_{0}\cup\\{\infty\\}$ via
$T=\inf_{i\in\mathbb{N}_{0}}\\{X_{i}\geq\lambda\\}$. Then, for each
$n\in\mathbb{N}_{0}$, define a random variable

$X_{T\land n}=X_{T}\cdot\mathbb{I}(T\leq n)+X_{n}\cdot\mathbb{I}(T>n)$

where $X_{T}$ is a random variable defined via
$X_{T}(\omega)=X_{T(\omega)}(\omega)$ for each $\omega\in\Omega$, and
$\mathbb{I}$ is again the indicator function that we defined in Section
Overview of Martingale Theory. It is a classical result from martingale theory
that, for any $n\in\mathbb{N}_{0}$, we have $\mathbb{E}[X_{T\land
n}]\leq\mathbb{E}[X_{0}]$ (see [64], Section 10.9). Hence, in order to prove
the desired inequality, it suffices to prove
$\lambda\cdot\mathbb{P}[\sup_{i\geq
0}X_{i}\geq\lambda]\leq\sup_{n\in\mathbb{N}_{0}}\mathbb{E}[X_{T\land n}]$.

To prove the desired inequality we observe that, for each
$n\in\mathbb{N}_{0}$, we have that

$\begin{split}\mathbb{E}[X_{T\land n}]&=\mathbb{E}[X_{T}\cdot\mathbb{I}(T\leq
n)]+\mathbb{E}[X_{n}\cdot\mathbb{I}(T>n)]\\\
&\geq\mathbb{E}[\lambda\cdot\mathbb{I}(T\leq
n)]+\mathbb{E}[X_{n}\cdot\mathbb{I}(T>n)]\\\ &=\lambda\cdot\mathbb{P}[T\leq
n]+\mathbb{E}[X_{n}\cdot\mathbb{I}(T>n)]\\\ &\geq\lambda\cdot\mathbb{P}[T\leq
n]=\lambda\cdot\mathbb{P}[\sup_{0\leq i\leq n}X_{i}\geq\lambda].\end{split}$
(4)

where in the first inequality we use the fact that $X_{T}\geq\lambda$, in the
second inequality we use the fact that each $X_{n}$ is nonnegative and in the
last equality we use the fact that
$T=\inf_{i\in\mathbb{N}_{0}}\\{X_{i}\geq\lambda\\}$. Finally,
$(\mathbb{P}[\sup_{0\leq i\leq n}X_{i}\geq\lambda])_{n=0}^{\infty}$ is a
sequence of probabilities of events that are increasing with respect to set
inclusion, so by the Monotone Convergence Theorem (see [64], Section 5.3) it
follows that

$\lim_{n\rightarrow\infty}\mathbb{P}[\sup_{1\leq i\leq
n}X_{i}\geq\lambda]=\mathbb{P}[\sup_{i\in\mathbb{N}_{0}}X_{i}\geq\lambda].$

Hence, by taking the supremum over $n\in\mathbb{N}_{0}$ of both sides of eq.
(4), we conclude that $\lambda\cdot\mathbb{P}[\sup_{i\geq
0}X_{i}\geq\lambda]\leq\sup_{n\in\mathbb{N}_{0}}\mathbb{E}[X_{T\land n}]$, as
desired. This concludes the proof of Theorem 5 since

$\mathbb{P}\Big{[}\sup_{i\geq
0}X_{i}\geq\lambda\Big{]}\leq\sup_{n\in\mathbb{N}_{0}}\frac{\mathbb{E}[X_{T\land
n}]}{\lambda}\leq\frac{\mathbb{E}[X_{0}]}{\lambda}.$

∎

## Proof of Theorem 1

We now prove Theorem 1. Fix an initial state
$\mathbf{x}_{0}\in\mathcal{X}_{0}$ so that we need to show
$\mathbb{P}_{\mathbf{x}_{0}}[\textrm{ReachAvoid}(\mathcal{X}_{t},\mathcal{X}_{u})]\geq
p$. Let $V$ be an RASM with respect to $\mathcal{X}_{t}$, $\mathcal{X}_{u}$
and $p\in[0,1)$ whose existence is assumed in the theorem. First, we show that
$V$ gives rise to a supermartingale in the probability space
$(\Omega_{\mathbf{x}_{0}},\mathcal{F}_{\mathbf{x}_{0}},\mathbb{P}_{\mathbf{x}_{0}})$
of all trajectories of the system that start in $\mathbf{x}_{0}$. Then, we use
Theorem 4 and Theorem 5 to prove probabilistic reachability and safety.

For each time step $t\in\mathbb{N}_{0}$, define
$\mathcal{F}_{\mathbf{x}_{0},t}\subseteq\mathcal{F}_{\mathbf{x}_{0}}$ to be a
sub-$\sigma$-algebra that, intuitively, contains events that are defined in
terms of the first $t$ states of the system. Formally, for each
$j\in\mathbb{N}_{0}$, let
$C_{j}:\Omega_{\mathbf{x}_{0}}\rightarrow\mathcal{X}$ assign to each
trajectory
$\rho=(\mathbf{x}_{t},\mathbf{u}_{t},\omega_{t})_{t\in\mathbb{N}_{0}}\in\Omega_{\mathbf{x}_{0}}$
the $j$-th state $\mathbf{x}_{j}$ along the trajectory. We define
$\mathcal{F}_{i}$ to be the smallest $\sigma$-algebra over
$\Omega_{\mathbf{x}_{0}}$ with respect to which $C_{0},C_{1},\dots,C_{i}$ are
all measurable, where $\mathcal{X}\subseteq\mathbb{R}^{m}$ is equipped with
the induced subset Borel-$\sigma$-algebra. The sequence
$(\mathcal{F}_{\mathbf{x}_{0},t})_{t=0}^{\infty}$ is increasing with respect
to set inclusion.

Now, define a stochastic process $(X_{t})_{t=0}^{\infty}$ in the probability
space
$(\Omega_{\mathbf{x}_{0}},\mathcal{F}_{\mathbf{x}_{0}},\mathbb{P}_{\mathbf{x}_{0}})$
via

$X_{t}(\rho)=\begin{cases}V(\mathbf{x}_{t}),&\text{if
}\mathbf{x}_{i}\not\in\mathcal{X}_{t}\text{ and
}V(\mathbf{x}_{i})<\frac{1}{1-p}\\\ &\text{for each }0\leq i\leq t\\\
0,&\text{if }\mathbf{x}_{i}\in\mathcal{X}_{t}\text{ for some }0\leq i\leq
t\text{ and}\\\ &V(\mathbf{x}_{j})<\frac{1}{1-p}\text{ for each }0\leq j\leq
i\\\ \frac{1}{1-p},&\text{otherwise}\end{cases}$

for each $t\in\mathbb{N}_{0}$ and a trajectory
$\rho=(\mathbf{x}_{t},\mathbf{u}_{t},\omega_{t})_{t\in\mathbb{N}_{0}}$. In
other words, the value of $X_{t}$ is equal to the value of $V$ at
$\mathbf{x}_{t}$, unless either the target set $\mathcal{X}_{t}$ has been
reached first in which case we set all future values of $\mathcal{X}_{t}$ to
$0$, or a state in which $V$ exceeds $\frac{1}{1-p}$ has been reached first in
which case we set all future values of $\mathcal{X}_{t}$ to $\frac{1}{1-p}$.
We claim that $(X_{t})_{t=0}^{\infty}$ is a nonnegative supermartingale with
respect to $(\mathcal{F}_{\mathbf{x}_{0},t})_{t=0}^{\infty}$. Indeed, each
$X_{t}$ is $\mathcal{F}_{\mathbf{x}_{0},t}$-measurable as it is defined in
terms of the first $t$ states along a trajectory. It is also nonnegative as
$V$ is nonnegative by the Nonnegativity condition of RASMs. Finally, to see
that
$\mathbb{E}_{\mathbf{x}_{0}}[X_{t+1}\mid\mathcal{F}_{\mathbf{x}_{0},t}](\rho)\leq
X_{t}(\rho)$ holds for each $t\in\mathbb{N}_{0}$ and
$\rho=(\mathbf{x}_{t},\mathbf{u}_{t},\omega_{t})_{t\in\mathbb{N}_{0}}$, we
consider $3$ cases:

  1. 1.

If $\mathbf{x}_{0},\mathbf{x}_{1},\dots,\mathbf{x}_{t}\not\in\mathcal{X}_{t}$
and $V(\mathbf{x}_{i})<\frac{1}{1-p}$ for each $0\leq i\leq t$, then

$\begin{split}&\mathbb{E}_{\mathbf{x}_{0}}[X_{t+1}\mid\mathcal{F}_{\mathbf{x}_{0},t}](\rho)\\\
&=\mathbb{E}_{\mathbf{x}_{0}}\Big{[}X_{t+1}\cdot\Big{(}\mathbb{I}(\mathbf{x}_{t+1}\not\in\mathcal{X}_{t}\land
V(\mathbf{x}_{t+1})<\frac{1}{1-p})\\\
&\,\,\,+\mathbb{I}(\mathbf{x}_{t+1}\in\mathcal{X}_{t})+\mathbb{I}(V(\mathbf{x}_{t+1})\geq\frac{1}{1-p})\Big{)}\mid\mathcal{F}_{\mathbf{x}_{0},t}\Big{]}(\rho)\\\
&=\mathbb{E}_{\mathbf{x}_{0}}[X_{t+1}\cdot\mathbb{I}(\mathbf{x}_{t+1}\not\in\mathcal{X}_{t})\mid\mathcal{F}_{\mathbf{x}_{0},t}](\rho)\\\
&\,\,\,+0+\frac{1}{1-p}\cdot\mathbb{E}[\mathbb{I}(V(\mathbf{x}_{t+1})\geq\frac{1}{1-p})\mid\mathcal{F}_{\mathbf{x}_{0},t}](\rho)\end{split}$
$\begin{split}&\leq\mathbb{E}_{\omega\sim
d}[V(f(\mathbf{x}_{t},\mathbf{u}_{t},\omega_{t}))\cdot\mathbb{I}(\mathbf{x}_{t+1}\not\in\mathcal{X}_{t}\land
V(\mathbf{x}_{t+1})<\frac{1}{1-p})]\\\ &\,\,\,+\mathbb{E}_{\omega\sim
d}[V(f(\mathbf{x}_{t},\mathbf{u}_{t},\omega_{t}))\cdot\mathbb{I}(\mathbf{x}_{t+1}\in\mathcal{X}_{t})]\\\
&\,\,\,+\mathbb{E}_{\omega\sim
d}[V(f(\mathbf{x}_{t},\mathbf{u}_{t},\omega_{t}))\cdot\mathbb{I}(V(\mathbf{x}_{t+1})\geq\frac{1}{1-p})]\\\
&=\mathbb{E}_{\omega\sim d}[V(f(\mathbf{x}_{t},\mathbf{u}_{t},\omega_{t}))]\\\
&\leq V(\mathbf{x}_{t})-\epsilon.\end{split}$

Here, the first equality follows by the law of total probability, the second
equality follows by our definition of each $X_{t}$, the third inequality
follows by observing that $V(\mathbf{x}_{t+1})\geq X_{t+1}(\rho)$ in this
case, the fourth equality is just the sum of expectations over disjoint sets,
and finally the fifth inequality follows by the Expected decrease condition in
Definition 1 since $\mathbf{x}_{t}\not\in\mathcal{X}_{t}$ and
$V(\mathbf{x}_{t})<\frac{1}{1-p}$, by the assumption of this case.

  2. 2.

If $\mathbf{x}_{i}\in\mathcal{X}_{t}$ for some $0\leq i\leq t$ and
$V(\mathbf{x}_{j})<\frac{1}{1-p}$ for all $0\leq j\leq i$, then we have
$\mathbb{E}_{\mathbf{x}_{0}}[X_{t+1}\mid\mathcal{F}_{\mathbf{x}_{0},t}](\rho)=X_{t+1}(\rho)=0$.

  3. 3.

Otherwise, we must have $V(\mathbf{x}_{i})\geq\frac{1}{1-p}$ and
$\mathbf{x}_{0},\dots,\mathbf{x}_{i}\not\in\mathcal{X}_{t}$ for some $-\leq
i\leq t$, thus
$\mathbb{E}_{\mathbf{x}_{0}}[X_{t+1}\mid\mathcal{F}_{\mathbf{x}_{0},t}](\rho)=X_{t+1}(\rho)=\frac{1}{1-p}$.

Hence, we have proved that $(X_{t})_{t=0}^{\infty}$ is a nonnegative
supermartingale.

Now, by Theorem 4 it follows that the value of the nonnegative supermartingale
$(X_{t})_{t=0}^{\infty}$ with probability $1$ converges. In what follows, we
show that $(X_{t})_{t=0}^{\infty}$ with probability $1$ converges to and
reaches either $0$ or a value that is greater than or equal to
$\frac{1}{1-p}$. To do this, we use the fact that the Expected decrease
condition of RASMs enforces the value of $V$ to decrease in expected value by
at least $\epsilon>0$ after every one-step evolution of the system in any non-
target state at which $V(\mathbf{x})<\frac{1}{1-p}$. Define the stopping time
$T:\Omega_{\mathbf{x}_{0}}\rightarrow\mathbb{N}_{0}\cup\\{\infty\\}$ via

$T(\rho)=\inf_{t\in\mathbb{N}_{0}}\Big{\\{}X_{t}(\rho)=0\lor
X_{t}(\rho)\geq\frac{1}{1-p}\Big{\\}}.$

Our goal is then to prove that $\mathbb{P}_{\mathbf{x}_{0}}[T<\infty]=1$.
Using the argument in the proof that $(X_{t})_{t=0}^{\infty}$ is a nonnegative
supermartingale (in particular, the proof of supermartingale property in Case
$1$), we can in fact deduce a stronger inequality

$\mathbb{E}_{\mathbf{x}_{0}}[X_{t+1}\mid\mathcal{F}_{\mathbf{x}_{0},t}](\rho)\leq
X_{t}(\rho)-\epsilon\cdot\mathbb{I}(T(\rho)>t)$

for each $\rho\in\Omega_{\mathbf{x}_{0}}$. But now, we may use Proposition 1
stated below to deduce that
$\mathbb{E}_{\mathbf{x}_{0}}[T]\leq\mathbf{E}_{\mathbf{x}_{0}}[X_{0}]=V(\mathbf{x}_{0})<\infty$,
which in turn implies that $\mathbb{P}_{\mathbf{x}_{0}}[T<\infty]=1$, as
desired. This concludes the proof.

The following proposition states a results on probability $1$ convergence of
ranking supermartingales (RSMs). RSMs are a notion similar to our RASMs that
were first introduced in [13] in order to study termination in probabilistic
programs, and were used in [38] to formally verify almost-sure stability and
reachability in stochastic control systems. We note that RASMs generalize RSMs
in the sense that RSMs coincide with RASMs in the special case when the unsafe
set is empty and we only consider a probability $1$ reachability
specification, i.e. $\mathcal{X}_{u}=\emptyset$.

######  Proposition 1 ([13]).

Let $(\Omega,\mathcal{F},\mathbb{P})$ be a probability space, let
$(\mathcal{F}_{i})_{i=0}^{\infty}$ be an increasing sequence of
sub-$\sigma$-algebras in $\mathcal{F}$ and let $T$ be a stopping time with
respect to $(\mathcal{F}_{i})_{i=0}^{\infty}$. Suppose that
$(X_{i})_{i=0}^{\infty}$ is a stochastic process such that each $X_{i}$ is
nonnegative and we have that

$\mathbb{E}[X_{i+1}\mid\mathcal{F}_{i}](\omega)\leq
X_{i}(\omega)-\epsilon\cdot\mathbb{I}(T(\omega)>i)$

holds for each $i\in\mathbb{N}_{0}$ and $\omega\in\Omega$. Then
$\mathbb{P}[T<\infty]=1$.

Finally, by using Theorem 5 for the nonnegative supermartingale
$(X_{t})_{t=0}^{\infty}$ and $\lambda=\frac{1}{1-p}>0$, it follows that
$\mathbb{P}_{\mathbf{x}_{0}}[\sup_{i\geq
0}X_{i}\geq\frac{1}{1-p}]\leq(1-p)\cdot\mathbb{E}_{\mathbf{x}_{0}}[X_{0}]\leq
1-p$. The second inequality follows since $X_{0}(\rho)=V(\mathbf{x}_{0})\leq
1$ for every $\rho\in\Omega_{\mathbf{x}_{0}}$ by the Initial condition of
RASMs. Hence, as $(X_{t})_{t=0}^{\infty}$ with probability $1$ either reaches
$0$ or a value that is greater than or equal to $\frac{1}{1-p}$, we conclude
that $(X_{t})_{t=0}^{\infty}$ reaches $0$ without reaching a value that is
greater than or equal to $\frac{1}{1-p}$ with probability at least $p$. By the
definition of each $X_{t}$ and by the Safety condition of RASMs, this implies
that with probability at least $p$ the system will reach the target set
$\mathcal{X}_{t}$without reaching the unsafe set $\mathcal{X}_{u}$, i.e. that
$\mathbb{P}_{\mathbf{x}_{0}}[\textrm{ReachAvoid}(\mathcal{X}_{t},\mathcal{X}_{u})]\geq
p$.

## Computation of Expected Values of Neural Networks

We now describe the method for bounding the expected value of a neural network
function over a given probability distribution. Let $\mathbf{x}\in\mathcal{X}$
be a fixed state, and suppose that we want to bound the expected value
$\mathbb{E}_{\omega\sim d}[V(f(\mathbf{x},\pi(\mathbf{x}),\omega))]$. We
partition the disturbance space $\mathcal{N}\subseteq\mathbb{R}^{p}$ into
finitely many cells
$\text{cell}(\mathcal{N})=\\{\mathcal{N}_{1},\dots,\mathcal{N}_{k}\\}$. Let
$\mathrm{maxvol}=\max_{\mathcal{N}_{i}\in\text{cell}(\mathcal{N})}\mathsf{vol}(\mathcal{N}_{i})$
denote the maximal volume of any cell in the partition (with respect to the
Lebesgue measure). The expected value is bounded via

$\mathbb{E}_{\omega\sim
d}\Big{[}V\Big{(}f(\mathbf{x},\pi(\mathbf{x}),\omega)\Big{)}\Big{]}\leq\sum_{\mathcal{N}_{i}\in\text{cell}(\mathcal{N})}\mathrm{maxvol}\cdot\sup_{\omega\in\mathcal{N}_{i}}F(\omega)$

where $F(\omega)=V(f(\mathbf{x},\pi(\mathbf{x}),\omega))$. Each supremum is
then bounded from above via interval arithmetic by using the method of [26].
Note that $\mathrm{maxvol}$ is not finite if $\mathcal{N}$ is unbounded. In
order to allow expected value computation for an unbounded $\mathcal{N}$ under
the assumption that $d$ is a product of univariate distributions, the method
first applies the probability integral transform [42] to each univariate
probability distribution in $d$ in order to reduce the problem to the case of
a probability distribution of bounded support.

## Proof of Theorem 2

Suppose that the verifier verifies that $V$ satisfies eq. (1) for each
$\tilde{\mathbf{x}}\in\tilde{\mathcal{X}_{e}}$, eq. (2) for each
$\text{cell}\in\text{Cells}_{\mathcal{X}_{0}}$ and eq. (3) for each
$\text{cell}\in\text{Cells}_{\mathcal{X}_{u}}$. The fact that the Initial and
the Unsafe conditions in Definition 1 of RASMs are satisfied by $V$ then
follows from the correctness of interval arithmetic abstract interpretation
(IA-AI) of [26]. Thus, we only need to show that $V$ satisfies the Expected
decrease condition in Definition 1.

To show that $V$ satisfies the Expected decrease condition, we need to show
that there exists $\epsilon>0$ such that
$V(\mathbf{x})\geq\mathbb{E}_{\omega\sim
d}[V(f(\mathbf{x},\pi(\mathbf{x}),\omega))]+\epsilon$ holds for all
$\mathbf{x}\in\mathcal{X}\backslash\mathcal{X}_{t}$ at which
$V(\mathbf{x})\leq\frac{1}{1-p}$. We prove that $\epsilon>0$ defined via

$\epsilon=\min_{\tilde{\mathbf{x}}\in\tilde{\mathcal{X}_{\epsilon}}}\Big{(}V(\tilde{\mathbf{x}})-\tau\cdot
K-\mathbb{E}_{\omega\sim
d}\Big{[}V\Big{(}f(\tilde{\mathbf{x}},\pi(\tilde{\mathbf{x}}),\omega)\Big{)}\Big{]}\Big{)}$

satisfies this property. Note that $\epsilon>0$, as each
$\tilde{\mathbf{x}}\in\tilde{\mathcal{X}_{e}}$ satisfies eq. (1).

To show this, fix $\mathbf{x}\in\mathcal{X}\backslash\mathcal{X}_{t}$ with
$V(\mathbf{x})\leq\frac{1}{1-p}$ and let
$\tilde{\mathbf{x}}\in\tilde{\mathcal{X}_{e}}$ be such that
$||\mathbf{x}-\tilde{\mathbf{x}}||_{1}\leq\tau$. By construction, the set
$\tilde{\mathcal{X}_{e}}$ contains vertices of each discretization cell that
intersects $\mathcal{X}\backslash\mathcal{X}_{t}$ and that contains at least
one state at which $V$ is less than or equal to $\frac{1}{1-p}$, hence such
$\tilde{\mathbf{x}}$ exists. We then have

$\begin{split}&\mathbb{E}_{\omega\sim
d}\Big{[}V\Big{(}f(\mathbf{x},\pi(\mathbf{x}),\omega)\Big{)}\Big{]}\\\
&\leq\mathbb{E}_{\omega\sim
d}\Big{[}V\Big{(}f(\tilde{\mathbf{x}},\pi(\tilde{\mathbf{x}}),\omega)\Big{)}\Big{]}\\\
&\hskip
28.45274pt+||f(\tilde{\mathbf{x}},\pi(\tilde{\mathbf{x}}),\omega)-f(\mathbf{x},\pi(\mathbf{x}),\omega)||_{1}\cdot
L_{V}\\\ &\leq\mathbb{E}_{\omega\sim
d}\Big{[}V\Big{(}f(\tilde{\mathbf{x}},\pi(\tilde{\mathbf{x}}),\omega)\Big{)}\Big{]}\\\
&\hskip
28.45274pt+||(\tilde{\mathbf{x}},\pi(\tilde{\mathbf{x}}),\omega)-(\mathbf{x},\pi(\mathbf{x}),\omega)||_{1}\cdot
L_{V}\cdot L_{f}\\\ &\leq\mathbb{E}_{\omega\sim
d}\Big{[}V\Big{(}f(\tilde{\mathbf{x}},\pi(\tilde{\mathbf{x}}),\omega)\Big{)}\Big{]}\\\
&\hskip 28.45274pt+||\tilde{\mathbf{x}}-\mathbf{x}||_{1}\cdot L_{V}\cdot
L_{f}\cdot(1+L_{\pi})\\\ &\leq\mathbb{E}_{\omega\sim
d}\Big{[}V\Big{(}f(\tilde{\mathbf{x}},\pi(\tilde{\mathbf{x}}),\omega)\Big{)}\Big{]}\\\
&\hskip 28.45274pt+\tau\cdot L_{V}\cdot L_{f}\cdot(1+L_{\pi}).\end{split}$ (5)

On the other hand, we also have

$V(\mathbf{x})\geq
V(\tilde{\mathbf{x}})-||\tilde{\mathbf{x}}-\mathbf{x}||_{1}\cdot L_{V}\geq
V(\tilde{\mathbf{x}})-\tau\cdot L_{V}.$ (6)

Combining eq.(5) and (6), we conclude that

$\begin{split}&V(\mathbf{x})-\mathbb{E}_{\omega\sim
d}\Big{[}V\Big{(}f(\mathbf{x},\pi(\mathbf{x}),\omega)\Big{)}\Big{]}\\\ &\geq
V(\tilde{\mathbf{x}})-\tau\cdot L_{V}-\mathbb{E}_{\omega\sim
d}\Big{[}V\Big{(}f(\tilde{\mathbf{x}},\pi(\tilde{\mathbf{x}}),\omega)\Big{)}\Big{]}\\\
&\hskip 28.45274pt-\tau\cdot L_{V}\cdot L_{f}\cdot(1+L_{\pi})\\\
&=V(\tilde{\mathbf{x}})-\tau\cdot K-\mathbb{E}_{\omega\sim
d}\Big{[}V\Big{(}f(\tilde{\mathbf{x}},\pi(\tilde{\mathbf{x}}),\omega)\Big{)}\Big{]}\\\
&\geq\epsilon\end{split}$ (7)

where the equality in the second last row follows by the definition of $K$,
and the inequality in the last row follows by our choice of $\epsilon$. Hence,
$V$ satisfies the Expected decrease condition and is indeed an RASM as in
Definition 1.

## Auxiliary Loss Term

The loss term $\mathcal{L}_{\text{Aux}}(\nu)$ is an auxiliary loss term that
does not enforce any of the defining conditions of RASMs, however it is used
to guide the learner towards a candidate that attains the global minimum in a
state that is contained within the target set $\mathcal{X}_{t}$. We
empirically observed that this term prevents the updated policy from diverging
from its objective to stabilize the system. It is defined via

$\begin{split}\mathcal{L}_{\text{Aux}}(\nu)&=\max\\{V_{\nu}(\hat{\mathbf{x}}_{\text{Target}})-\varepsilon,0\\}\\\
&+\max\\{\min_{\mathbf{x}\in\tilde{X}\cap\mathcal{X}_{t}}V_{\nu}(\mathbf{x})-\min_{\mathbf{x}\in
C_{\text{init}}}V_{\nu}(\mathbf{x}),0\\}\\\
&+\max\\{\min_{\mathbf{x}\in\tilde{X}\cap\mathcal{X}_{t}}V_{\nu}(\mathbf{x})-\min_{\mathbf{x}\in
C_{\text{unsafe}}}V_{\nu}(\mathbf{x}),0\\}\end{split}$

with $\tilde{\mathbf{x}}_{\text{Target}}$ being some state contained in the
target set $\mathcal{X}_{t}$ and $\varepsilon\geq 0$ an algorithm parameter.

## Proof of Theorem 3

Suppose that $V_{\nu}$ satisfies eq. (1) for each
$\tilde{\mathbf{x}}\in\tilde{\mathcal{X}_{e}}$, eq. (2) for each
$\text{cell}\in\text{Cells}_{\mathcal{X}_{0}}$ and eq. (3) for each
$\text{cell}\in\text{Cells}_{\mathcal{X}_{u}}$. Suppose that Lipschitz
constants of $\pi_{\theta}$ and $V_{\nu}$ are below the thresholds specified
by $\mathcal{L}_{\text{Lipschitz}}(\theta)$ and
$\mathcal{L}_{\text{Lipschitz}}(\nu)$ and that the samples in
$\mathcal{L}_{\text{Decrease}}(\theta,\nu)$ are independent. We need to show
that $\lim_{N\rightarrow\infty}\mathcal{L}(\theta,\nu)=0$ with probability
$1$.

Since Lipschitz constants of $\pi_{\theta}$ and $V_{\nu}$ are below the
thresholds specified by $\mathcal{L}_{\text{Lipschitz}}(\theta)$ and
$\mathcal{L}_{\text{Lipschitz}}(\nu)$, we have that
$\lambda\cdot(\mathcal{L}_{\text{Lipschitz}}(\theta)+\mathcal{L}_{\text{Lipschitz}}(\nu))=0$.
Moreover, our initialization of $C_{\text{init}}$ and our design of the
verifier module ensure that $C_{\text{init}}$ contains only states in
$\mathcal{X}_{0}$, hence $\mathcal{L}_{\text{Init}}(\nu)=0$ as $V_{\nu}$
satisfies the Initial condition of RASMs. Note, $V_{\nu}$ satisfies all
conditions checked by the verifier, hence by Theorem 2 we know that it is an
RASM. Similarly, $C_{\text{unsafe}}$ contains only states in
$\mathcal{X}_{u}$, hence $\mathcal{L}_{\text{Unsafe}}(\nu)=0$ as $V_{\nu}$
satisfies the Safety condition of RASMs. Thus, under theorem assumptions we
have that

$\begin{split}&\mathcal{L}(\theta,\nu)=\mathcal{L}_{\text{Decrease}}(\theta,\nu)\\\
&=\frac{1}{|C_{\text{decrease}}|}\sum_{\mathbf{x}\in
C_{\text{decrease}}}\Big{(}\max\\\
&\Big{\\{}\sum_{\omega_{1},\dots,\omega_{N}\sim\mathcal{N}}\frac{V_{\nu}\big{(}f(\mathbf{x},\pi_{\theta}(\mathbf{x}),\omega_{i})\big{)}}{N}-V_{\theta}(\mathbf{x})+\tau\cdot
K,0\Big{\\}}\Big{)}\end{split}$

Hence, in order to prove that
$\lim_{N\rightarrow\infty}\mathcal{L}(\theta,\nu)=0$ with probability $1$, it
suffices to prove that for each $\mathbf{x}\in C_{\text{decrease}}$ with
probability $1$ we have

$\begin{split}&\lim_{N\rightarrow\infty}\max\Big{\\{}\sum_{\omega_{1},\dots,\omega_{N}\sim\mathcal{N}}\frac{V_{\nu}\big{(}f(\mathbf{x},\pi_{\theta}(\mathbf{x}),\omega_{i})\big{)}}{N}\\\
&-V_{\theta}(\mathbf{x})+\tau\cdot K,0\Big{\\}}=0.\end{split}$

The above sum is the mean of $N$ independently sampled successor states of
$\mathbf{x}$, which are sampled according to the probability distribution
defined by the system dynamics and the probability distribution $d$ over
disturbance vectors. Since the state space of the system is assumed to be
compact and $V_{\theta}$ is continuous as it is a neural network, the random
value defined by the value of $V$ at a sampled successor state is bounded and
therefore admits a well-defined and finite first moment. The Strong Law of
Large Numbers [64] then implies that the above sum converges to the expected
value of this distribution as $N\rightarrow\infty$. Thus, with probability
$1$, we have that

$\begin{split}&\lim_{N\rightarrow\infty}\max\Big{\\{}\sum_{\omega_{1},\dots,\omega_{N}\sim\mathcal{N}}\frac{V_{\nu}\big{(}f(\mathbf{x},\pi_{\theta}(\mathbf{x}),\omega_{i})\big{)}}{N}-V_{\theta}(\mathbf{x})+\tau\cdot
K,0\Big{\\}}\\\
&=\max\Big{\\{}\lim_{M\rightarrow\infty}\sum_{\omega_{1},\dots,\omega_{N}\sim\mathcal{N}}\frac{V_{\nu}\big{(}f(\mathbf{x},\pi_{\theta}(\mathbf{x}),\omega_{i})\big{)}}{N}-V_{\theta}(\mathbf{x})+\tau\cdot
K,0\Big{\\}}\\\ &=\max\Big{\\{}\lim_{M\rightarrow\infty}\mathbb{E}_{\omega\sim
d}\Big{[}f(\mathbf{x},\pi_{\theta}(\mathbf{x}),\omega)\big{]}-V_{\theta}(\mathbf{x})+\tau\cdot
K,0\Big{\\}}\\\ &=0.\end{split}$

The first equality holds since a limit may be interchanged with the maximum
function over a finite number of arguments, the second equality holds with
probability $1$ by the Strong Law of Large Numbers, and the third equality
holds since $V_{\nu}$ satisfies eq. (1) for each
$\tilde{\mathbf{x}}\in\tilde{\mathcal{X}_{e}}$ and we have
$C_{\text{decrease}}\subseteq\tilde{\mathcal{X}_{e}}$. This concludes our
proof that $\lim_{N\rightarrow\infty}\mathcal{L}(\theta,\nu)=0$ with
probability $1$.

## Experiment details

The dynamics of the 2D system is given by

$\mathbf{x}_{t+1}=\begin{pmatrix}1&0.045\\\
0&0.9\end{pmatrix}\mathbf{x}_{t}+\begin{pmatrix}0.45\\\
0.5\end{pmatrix}g(\mathbf{u}_{t})+\begin{pmatrix}0.01&0\\\
0&0.005\end{pmatrix}\omega,$ (8)

with $\omega$ being the disturbance vector and
$\omega[1],\omega[2]\sim\text{Triangular}$. Square brackets indicate the
coordinate index, e.g. $\omega[1]$ is the first coordinate of
$\omega\in\mathbb{R}^{2}$. The probability density function of Triangular is
defined by

$\text{Triangular}(x):=\begin{cases}0&\text{if }x<-1\\\ 1-|x|&\text{if }-1\leq
x\leq 1\\\ 0&\text{otherwise}\end{cases}.$ (9)

The function $g$ is defined as $g(u)=\max(\min(u,1),-1)$. The state space of
the 2D system is define as $\mathcal{X}=[-1.5,1.5]^{2}$. We define the target
set as $\mathcal{X}_{t}=[-0.2,0.2]^{2}$, the initial set
$\mathcal{X}_{0}=[-0.25,-0.2]\times[-0.1,0.1]\cup[0.25,0.2]\times[-0.1,0.1]$
and the unsafe set
$\mathcal{X}_{u}=[-1.5,-1.4]\times[-1.5,0]\cup[1.4,1.5]\times[0,1.5]$.

For the inverted pendulum task, the dynamics is given by

$\displaystyle\mathbf{x}_{t+1}[2]$ $\displaystyle:=(1-b)\mathbf{x}_{t}[2]$
$\displaystyle+\Delta\cdot\big{(}\frac{-1.5\cdot
G\cdot\text{sin}(\mathbf{x}_{t}[1]+\pi)}{2l}+\frac{3}{ml^{2}}2g(\mathbf{u}_{t})\big{)}$
$\displaystyle+0.02\omega[1]$ $\displaystyle\mathbf{x}_{t+1}[1]$
$\displaystyle:=\mathbf{x}_{t}[1]+\Delta\cdot\mathbf{x}_{t+1}[2]+0.01\omega[2],$

with $\delta,G,m,l,b$ being defined in Table 3. The state space of the
inverted pendulum environment is define as $\mathcal{X}=[-0.7,0.7]^{2}$. We
define the target set as $\mathcal{X}_{t}=[-0.2,0.2]^{2}$, the initial set
$\mathcal{X}_{0}=[-0.3,0.3]^{2}$ and the unsafe set
$\mathcal{X}_{u}=[-0.7,-0.6]\times[-0.7,0]\cup[0.6,0.7]\times[0,0.7]$.

Parameter | Value
---|---
$\Delta$ | 0.05
$G$ | 10
$m$ | 0.15
$l$ | 0.5
$b$ | 0.1
Table 3: Parameters of the inverted pendulum task.

The dynamics of the collision avoidance task is given by

$\displaystyle d_{1}$
$\displaystyle=\max\\{0.33||\mathbf{x}_{t}-\begin{pmatrix}0\\\
1\end{pmatrix}||,0\\}$ $\displaystyle d_{2}$
$\displaystyle=\max\\{0.33||\mathbf{x}_{t}-\begin{pmatrix}0\\\
-1\end{pmatrix}||,0\\}$ $\displaystyle\mathbf{x}_{t+1}$
$\displaystyle=\mathbf{x}_{t}+0.2\Big{(}d_{2}\big{(}d_{1}\mathbf{u}_{t}+(1-d_{1})\begin{pmatrix}0\\\
1\end{pmatrix}\big{)}$ $\displaystyle+(1-d_{2})\begin{pmatrix}0\\\
-1\end{pmatrix}\Big{)}+0.05\omega_{t}.$

The state space of the collision avoidance environment is define as
$\mathcal{X}=[-1,1]^{2}$. We define the target set as
$\mathcal{X}_{t}=[-0.2,0.2]^{2}$, the initial set
$\mathcal{X}_{0}=[-1,-0.9]\times[-0.6,0.6]\cup[0.9,1.0]\times[-0.6,0.6]$ and
the unsafe set
$\mathcal{X}_{u}=[-0.3,0.3]\times[0.7,1]\cup[-0.3,0.3]\times[-1,-0.7]$.
Similar to the first two environments, $\omega_{t}$ is a triangular
distributed random variable.

We optimize the training objective using stochastic gradient descent. As
mentioned in the main text, the policy and RASM networks consist of two hidden
layers with 128 units each and ReLU activation function. The RASMs network has
single output unit with a softplus activation, while the output dimension of
the policy network depends on the task.

The used hyperparameters of our algorithm used in the experiments are listed
in Table 4. The code is available for review in the supplementary materials.

Hyperparameter | Value
---|---
Optimizer | Adam [32]
Batch size | 4096
$V_{\nu}$ learning rate | 5e-4
$\pi_{\theta}$ learning rate | 5e-5
Lipschitz factor $\gamma$ | 0.001
Lipschitz threshold $\rho_{\theta}$ | 4
Lipschitz threshold $\rho_{\nu}$ | 15
$\tau$ (2D system) | 6e-3
$\tau$ (inverted pendulum) | 2.3e-3
$\tau$ (collision avoidance) | 4e-3
$\varepsilon$ | 0.3
$N$ | 16
Number of cells for expectation | 144
Table 4: List of hyperparameter values used in the experiments.

Normalizing the learned RASM for better bounds

After our algorithm has terminated we can slightly improve the probability
bounds certified by the verifier. In particular, the normalization linearly
transforms $V_{\nu}$ such that the supremum of the new RASM $V^{\prime}_{\nu}$
at the initial set is 1 and the infimum of $V^{\prime}_{\nu}$ on the entire
domain is 0, i.e.,

$V^{\prime}_{\nu}(\mathbf{x})=\frac{V_{\nu}(\mathbf{x})-\inf_{\mathbf{x}^{\prime}\in\mathcal{X}}V_{\nu}(\mathbf{x}^{\prime})}{\sup_{\mathbf{x}^{\prime}\in\mathcal{X}_{0}}V_{\nu}(\mathbf{x}^{\prime})-\inf_{\mathbf{x}^{\prime}\in\mathcal{X}}V_{\nu}(\mathbf{x}^{\prime})}.$
(10)

The improved probability bounds $p^{\prime}$ can then be computed according to
condition 3 by

$p^{\prime}=1-\frac{1}{\inf_{\mathbf{x}\in\mathcal{X}_{u}}V^{\prime}_{\nu}(\mathbf{x})}.$
(11)

The supremum and infimum are computed using our abstract interpretation (IA-
AI) on the cell grids.

PPO Details Here, we list the settings used for the PPO pre-training process
of the policy networks [50]. In every PPO iteration we collect 30 episodes of
the environment as training data in the experience buffer. The policy
$\pi_{\mu}$ is made stochastic using a Gaussian distributed random variable
that is added to the policy’s output, i.e., the policy predicts the mean of
the Gaussian. The standard deviation of the Gaussian is annealed during the
policy training process, starting from 0.5 at first PPO iteration to 0.05 at
PPO iteration 50. We normalize the advantage values, i.e., the difference
between the observed discounted returns and the predicted return by the value
function, by subtracting the mean and dividing by the standard deviation of
the advantage values of the experience buffer. The PPO clipping value
$\varepsilon$ is set to 0.2 and the discount factor $\gamma$ to 0.99. In every
PPO iteration, the policy is trained for 10 epochs, except for the first
iteration where the network is trained for 30 epochs. An epoch corresponds to
a pass over the entire data in the experience buffer, i.e., the data from the
the 30 episodes. The value network is trained for 5 epochs, expect in the
first PPO iteration, where the training is performed for 10 epochs. We apply
the Lipschitz regularization on the policy parameters already during the PPO
pre-training of the policy.