# Verified Compositional Neuro-Symbolic Control for Stochastic Systems with
Temporal Logic Tasks

Jun Wang1, Haojun Chen2, Zihe Sun2, and Yiannis Kantaros1 1J. Wang and Y.
Kantaros are with the Department of Electrical and Systems Engineering,
Washington University in St. Louis (WashU), St. Louis, MO, USA.
<EMAIL_ADDRESS>Chen and Z. Sun are with the Department of
Mechanical Engineering, Washington University in St. Louis (WashU), St. Louis,
MO, USA. {c.haojun<EMAIL_ADDRESS>work was supported in part by the
NSF award CNS $\\#2231257$.

###### Abstract

Several methods have been proposed recently to learn neural network (NN)
controllers for autonomous agents, with unknown and stochastic dynamics,
tasked with complex missions captured by Linear Temporal Logic (LTL). Due to
the sample-inefficiency of the majority of these works, compositional learning
methods have been proposed decomposing the LTL specification into smaller sub-
tasks. Then, separate controllers are learned and composed to satisfy the
original task. A key challenge within these approaches is that they often lack
safety guarantees or the provided guarantees are impractical. This paper aims
to address this challenge. Particularly, we consider autonomous systems with
unknown and stochastic dynamics and LTL-encoded tasks. We assume that the
system is equipped with a finite set of base skills modeled by trained NN
feedback controllers. Our goal is to check if there exists a temporal
composition of the trained NN controllers - and if so, to compute it - that
will yield a composite system behavior that satisfies the assigned LTL task
with probability one. We propose a new approach that relies on a novel
integration of automata theory and data-driven reachability analysis tools for
NN-controlled stochastic systems. The resulting neuro-symbolic controller
allows the agent to generate safe behaviors for unseen complex temporal logic
tasks in a zero-shot fashion by leveraging its base skills. We show
correctness of the proposed method and we provide conditions under which it is
complete. To the best of our knowledge, this is the first work that designs
verified temporal compositions of NN controllers for unknown and stochastic
systems. Finally, we provide extensive numerical simulations and hardware
experiments on robot navigation tasks to demonstrate the proposed method.

###### Index Terms:

Autonomous Systems, Neural Network Control, Verification, Temporal Logic
Control Synthesis

##  I Introduction

Machine learning (ML) techniques have been successfully applied to learn
controllers for systems with highly nonlinear, stochastic or unknown dynamics
and complex tasks including reach-avoid, sequencing, surveillance, and
delivery. Linear Temporal Logic (LTL) formulas has been used extensively
recently to formally define temporal and logical requirements that exist in
such complex tasks [1]. Learning controllers for LTL specifications has been
studied in [2, 3, 4, 5, 6, 7, 8, 9, 10, 11] and the references therein. The
learned controllers are typically modelled using neural networks (NN) to
account for continuous state and action spaces. Despite the impressive
empirical performance of NN-driven systems, they are characterized by the
following limitations: (i) they often lack safety and robustness guarantees,
especially, when applied to unseen tasks; and (ii) they are sample-inefficient
to learn which becomes more pronounced as the task complexity increases.

To address the first limitation, several verification and analysis methods
have been proposed for NN-controlled systems. These works can be categorized
into open-loop [12, 13, 14, 15, 16, 17, 18] and closed-loop [19, 20, 21, 22,
23, 24, 25, 26, 27]. Open-loop verification methods aim to verify properties
of a trained NN. For instance, [14] addresses the problem of output range
analysis of trained NNs given an input set. Closed-loop ones verification
algorithms investigate if a dynamical system with a trained NN controller can
satisfy a reach-avoid property given a set of possible initial states. For
instance, [24] considers hybrid systems driven by feedforward NN controllers
with sigmoid or tanh activation functions. Similarly, [21] considers discrete-
time linear time-varying systems with NN feedback controllers with arbitrary
non-linear activation functions. Shielding mechanisms have also been proposed
to ensure safety during the training and/or the deployment phase [28, 29]. The
main idea in the latter set of works is to compute a backup policy (called
shield) that overrides the nominal control policy when the system is about to
violate safety constraints. Although safety is ensured in these works,
liveness guarantees are not provided.

To address the second limitation, compositional learning methods have been
proposed recently [30, 31, 32, 33]. The key idea in these works is to
decompose the overarching LTL-encoded mission into simpler sub-tasks for which
NN controllers can be learned (e.g., using RL) more efficiently. Then, these
NN controllers are composed to satisfy the original task. Nevertheless, the
resulting controllers often either lack safety guarantees or the provided
guarantees are impractical (e.g., lower bounds on satisfaction probability)
for safety-critical applications; also, these guarantees are typically
specific to a fixed and given initial system state. Related is also the recent
work in [34] where, unlike [31, 32, 30, 33], selection of sub-tasks remain
outside the robot control and, instead, they are revealed by the environment;
e.g., a ‘turn left’ sub-task is revealed as a robot navigates a hallway. To
the contrary, in [31, 32, 30, 33] sub-tasks are ‘strategically’ selected by
the system to satisfy a temporal logic task. We note that guarantees for a
given composite controller can possibly be provided using the above
verification methods. Nevertheless, the latter would require knowledge of the
system dynamics is known. Additionally, even if the system dynamics is known,
these verification methods cannot provide guidance in terms of how the base NN
controllers should be composed to ensure verified task satisfaction.

To bridge this gap, in this paper, we propose a new method to design verified
temporal compositions of trained NN controllers for temporal logic tasks for
agents with unknown and stochastic dynamics. Specifically, we consider
autonomous systems/agents that are governed by unknown discrete-time nonlinear
dynamics while being subject to unknown, but upper-bounded, exogenous
disturbances. We assume that we have access to a simulator that can generate
system trajectories; this is a standard assumption e.g., in RL algorithms. The
agent is tasked with complex high-level missions captured by a fragment of
LTL, called co-safe LTL [1]. The LTL formula requires the agent to reach and
avoid certain system states in a temporal/logical order. For instance, an LTL
formula may model an aerial delivery task requiring a drone to deliver
packages in location A, B, and C, in this specific order, while avoiding
collisions with phone poles and flying over residential areas. We assume that
the agent is equipped with a finite set of trained NN controllers where each
controller can lead the agent towards a specific state while avoiding certain
sub-spaces. We emphasize that we do not make any assumptions about how these
NNs have been trained or about their accuracy and architecture. For instance,
they may have been trained using RL [35] or MPC-based methods [36]. Our goal
is to check if there exists a temporal composition of the trained NN
controllers - and if so, to compute it - that will yield a composite system
behavior satisfying the LTL task with probability one, for all initial states
belonging to a given set.

To address this problem, we propose a new approach that relies on a novel
integration of existing tools such as automata, graph-search methods, and
data-driven reachability analysis for NN-driven systems. Particularly,
inspired by recent compositional temporal logic planning methods [37, 38, 31],
we propose a symbolic reasoning method that leverages automaton
representations of LTL formulas and graph-search methods to decompose LTL
tasks into sequences of reach-avoid tasks. Then, we employ a recently proposed
reachability analysis tool [39] to check if there exists at least one temporal
composition of the NN controllers that can satisfy with probability one all
sub-tasks captured by at least one sequence of tasks. The resulting neuro-
symbolic controller allows the agent to generate verified behaviours for
unseen complex temporal logic tasks in a zero-shot fashion by leveraging its
current NN-based skills. We show that our proposed algorithm is correct, i.e.,
the controller generated by the proposed method accomplishes the assigned task
with probability one. We note that, in general, the proposed algorithm is not
complete in the sense that it may not find a control policy satisfying the
assigned task with probability one, even though such a policy exists. We
provide conditions under which our approach is complete and we discuss trade-
offs between completeness and computational efficiency. We highlight that our
method can handle any other open-loop or feedback controllers that are not
necessarily modeled as NNs. In this paper, we consider NN controllers due to
their brittleness to small input perturbations [40, 41] and their lack of safe
generalization to unseen tasks. We demonstrate the efficiency of the proposed
method using extensive numerical experiments that involve navigation tasks for
ground vehicles. Also, we perform hardware experiments with ground robots to
investigate the benefits and limitations of the proposed method with respect
to the sim2real gap, i.e., the difference between modeled and real
performance. Specifically, we evaluate performance of the designed composite
controllers against un-modeled sources of uncertainty, such as floor
slipperiness.

A preliminary version of this work was presented in our previous work [42]
which, however, considers deterministic discrete-time linear systems. We
extend our previous work by (i) considering stochastic and unknown system
dynamics; (ii) proving correctness of the proposed method and providing
conditions under which the proposed algorithm is complete; (iii) conducting
numerical simulations and hardware experiments that do not exist in [42]
demonstrating the sim2real gap. To the best of our knowledge, this is the
first work that designs verified compositions of NN controllers for systems
with unknown and stochastic dynamics that yield system behaviors satisfying
complex tasks captured by LTL.

Contributions: First, we propose a new approach to design verified temporal
compositions of trained NN controllers for systems with stochastic or even
unknown dynamics and co-safe LTL control objectives. Second, we show
correctness of the proposed algorithm and we discuss trade-offs between
completeness and computational efficiency. Third, we demonstrate the
efficiency of the proposed approach on several case studies that involve
complex navigation tasks for ground robots. Fourth, we perform hardware
experiments to investigate the benefits and limitations of the proposed method
with respect to the sim2real gap, i.e., the difference between modeled and
real performance.

##  II Problem Formulation

###  II-A Systems with Neural Network Controllers

We consider discrete-time nonlinear systems defined as:

${\mathbf{x}}_{t+1}={\mathbf{f}}({\mathbf{x}}_{t},{\mathbf{u}}_{t},\boldsymbol{\nu}_{t}),$
(1)

where ${\mathbf{x}}_{t}\in{\mathcal{X}}\subseteq\mathbb{R}^{d}$,
${\mathbf{u}}_{t}\in{\mathcal{U}}_{t}\subseteq\mathbb{R}^{n}$ and
$|\boldsymbol{\nu}_{t}|\leq V$ denote the state, the control input, and
bounded exogenous disturbance of the system at time $t\geq 0$. Notice that we
do not assume the knowledge of the systems, i.e., ${\mathbf{f}}$ can be a
simulator of the real system. We consider $N>0$ sub-spaces of interest,
denoted by $\ell_{i}\subset{\mathcal{X}}$, that are inside ${\mathcal{X}}$. We
assume that at any time $t$ the system can apply control inputs selected from
a finite set of feedback controllers collected in the set
$\Xi=\\{\xi_{i}\\}_{i=1}^{N}$, where
$\xi_{i}({\mathbf{x}}_{t}):{\mathcal{X}}\to\mathbf{R}^{n}$ maps system states
to control actions. We consider controllers $\xi_{i}({\mathbf{x}}_{t})$ that
are parameterized by multi-layer neural networks (NNs). We make the following
assumption about the controllers $\xi_{i}({\mathbf{x}}_{t})$:

######  Assumption II.1 (NN Controllers).

Every NN controller $\xi_{i}$ has been trained so that it can drive the system
state ${\mathbf{x}}_{t}$ towards the interior of $\ell_{i}$ for any initial
state in ${\mathcal{X}}$.

We do not make any assumption about the performance and architecture of the
trained NN controllers or how they have been trained. Hereafter, with slight
abuse of notation, we denote by $\xi(t)$ the controller selected from $\Xi$ at
time $t$. To ensure that the NN output respects the input constraint, we
consider a projection operator, denoted by $\text{Proj}_{{\mathcal{U}}_{t}}$,
and define the control input as
${\mathbf{u}}_{t}=\text{Proj}_{{\mathcal{U}}_{t}}\xi(t)$ [21]. Next, we define
a NN-based control strategy $\boldsymbol{\xi}$ as a temporal composition of
the controllers in $\Xi$.

######  Definition II.2 (Control Strategy).

A NN-based control strategy $\boldsymbol{\xi}$ is defined as a finite sequence
of NN controllers selected from $\Xi$, i.e.,
$\boldsymbol{\xi}=\mu(0),\mu(1),\mu(2),\dots,\mu(K)$, for some finite $K>0$,
where $\mu(k)\in\Xi$, for all $k\in\\{0,1,\dots,K\\}$, and $\mu(k)$ is applied
for a finite horizon $H_{k}$.

We highlight that in the above definition, the index $k$ is different from the
time instants $t$ used in (1). In fact, $k$ is an index, initialized as $k=0$
and increased by $1$ every $H_{k}$ time instants, pointing to the next NN
controller in the sequence $\boldsymbol{\xi}$. Also, we note again that
$\mu(k)$ is a feedback controller from $\Xi$. For instance, if
$\mu(0)=\xi_{i}$, for some $i\in\\{1,\dots,N\\}$, then the system applies the
controller $\xi_{i}({\mathbf{x}}_{t})$, for all time instants
$t\in\\{0,1,\dots,H_{0}\\}$. Under a NN-based control strategy
$\boldsymbol{\xi}$, an initial state ${\mathbf{x}}_{0}$, the corresponding
closed-loop system can generate a finite sequence of system states, denoted by
$\tau({\mathbf{x}}_{0})=\\{{\mathbf{x}}_{0},{\mathbf{x}}_{1},\dots,{\mathbf{x}}_{t},\dots,{\mathbf{x}}_{F}\\}$,
where $F=\sum_{k=0}^{K}H_{k}$ is a finite horizon. In fact,
$\tau({\mathbf{x}}_{0})$ is a stochastic sequence due to the noise
$\boldsymbol{\nu}_{t}$ in the system dynamics.

###  II-B Linear Temporal Logic Properties

We define mission and safety properties for the system (1) using Linear
Temporal Logic (LTL). LTL is a type of formal logic whose basic ingredients
are a set of atomic propositions (i.e., Boolean variables), denoted by
$\mathcal{AP}$, the Boolean operators, i.e., conjunction $\wedge$, and
negation $\neg$, and two temporal operators, next $\bigcirc$ and until
$\mathcal{U}$. LTL formulas over a set $\mathcal{AP}$ can be constructed based
on the following grammar:
$\phi::=\text{true}~{}|~{}\pi~{}|~{}\phi_{1}\wedge\phi_{2}~{}|~{}\neg\phi~{}|~{}\bigcirc\phi~{}|~{}\phi_{1}~{}\mathcal{U}~{}\phi_{2}$,
where $\pi\in\mathcal{AP}$. For brevity, we abstain from presenting the
derivations of other Boolean and temporal operators, e.g., always $\square$,
eventually $\lozenge$, implication $\Rightarrow$, which can be found in [1].
Hereafter, we define the set $\mathcal{AP}$ as
$\mathcal{AP}=\cup_{i}\\{\pi^{\ell_{i}}\\}$, where $\pi^{\ell_{i}}$ is an
atomic predicate that is true when the system state ${\mathbf{x}}_{t}$ is
within region $\ell_{i}$. We restrict our attention to co-safe LTL properties
that exclude the use of the ‘always’ operator; see also Example II.1. Co-safe
LTL formulas are satisfied by finite sequences of states
$\tau({\mathbf{x}}_{0})=\\{{\mathbf{x}}_{0},{\mathbf{x}}_{1},\dots,{\mathbf{x}}_{t},\dots,{\mathbf{x}}_{F}\\}$
where $F$ is a finite horizon [1] that can be generated by (1) for some
control strategy $\boldsymbol{\xi}$. Due to the noisy system dynamics,
satisfaction of $\phi$ can only be reasoned probabilistically. Given a control
strategy $\boldsymbol{\xi}$ and a set ${\mathcal{X}}_{0}$ of initial states,
hereafter, we denote by $\mathbb{P}_{\tau({\mathbf{x}}_{0})\sim
D}(\tau({\mathbf{x}}_{0})\models\phi|\boldsymbol{\xi},{\mathcal{X}}_{0})$ the
probability that the corresponding closed-loop system will generate a sequence
$\tau({\mathbf{x}}_{0})$ that satisfies $\phi$ for any initial state
${\mathbf{x}}_{0}\in{\mathcal{X}}_{0}$, where $D$ is the distribution over an
infinite number of trajectories generated by (1).

Figure 1: A drone is tasked with a delivery task over the campus of Washington
University in St. Louis. This mission is captured by an LTL formula
$\phi=(\Diamond\pi^{\ell_{1}})\wedge(\Diamond\pi^{\ell_{2}})\wedge(\neg\pi^{\ell_{1}}{\mathcal{U}}\pi^{\ell_{2}})\wedge(\neg(\pi^{\ell_{3}}\vee\pi^{\ell_{4}}\vee\pi^{\ell_{5}}){\mathcal{U}}\pi^{\ell_{1}})$
requiring to eventually reach region $\ell_{2}$ and then eventually reach
region $\ell_{1}$ (green rectangles) in this order to deliver packages.
Meanwhile, the drone is also required to avoid flying over buildings located
in $\ell_{3}$, $\ell_{4}$, and $\ell_{5}$ (red rectangles) until all packages
are delivered. The drone can start from a range of initial locations (orange
disk) and is equipped with trained controllers $\xi_{i}$ for each region-to-
reach $\ell_{i}$ (i.e., $\Xi=\\{\xi_{1},\xi_{2},\xi_{3},\xi_{4},\xi_{5}\\}$).
The drone is subject to bounded exogenous disturbances such as wind gusts. Our
goal in this paper is to design verified temporal compositions of the NN
controllers $\xi_{i}$ that satisfy the assigned LTL task with probability $1$.

######  Example II.1.

Examples of co-safe LTL specifications $\phi$ follow: (i)
$\phi=\Diamond(\pi^{\ell_{1}})\wedge(\neg\pi^{\ell_{2}}{\mathcal{U}}\pi^{\ell_{1}})$
captures a common reach-avoid property requiring the system to eventually
reach the region of interest $\ell_{1}$ while avoiding in the meantime the
unsafe region $\ell_{2}$; (ii)
$\phi=(\Diamond\pi^{\ell_{1}})\wedge(\Diamond\pi^{\ell_{2}})\wedge(\Diamond\pi^{\ell_{3}})\wedge(\Diamond\pi^{\ell_{4}})\wedge(\neg\pi^{\ell_{4}}{\mathcal{U}}\pi^{\ell_{1}})$,
which requires the system to eventually reach the regions of interest
$\ell_{1}$, $\ell_{2}$, $\ell_{3}$, and $\ell_{4}$, in any order, as long as
$\ell_{4}$ is avoided until region $\ell_{1}$ is reached; (iii)
$\phi=(\Diamond\pi^{\ell_{1}})\wedge(\Diamond\pi^{\ell_{2}})\wedge(\neg\pi^{\ell_{1}}{\mathcal{U}}\pi^{\ell_{2}})\wedge(\neg(\pi^{\ell_{3}}\vee\pi^{\ell_{4}}\vee\pi^{\ell_{5}}){\mathcal{U}}\pi^{\ell_{1}})$
, which requires the system to eventually reach regions $\ell_{2}$ and
$\ell_{1}$ in this order, as long as $\ell_{3},\ell_{4},\ell_{5}$ are avoided
until region $\ell_{1}$ is reached; see also Fig 1.

###  II-C Problem Statement

The problem addressed in this paper can be summarized as follows:

######  Problem 1 (Verification Problem).

Given (i) a set of initial states ${\mathcal{X}}_{0}\subseteq{\mathcal{X}}$;
(ii) the system dynamics (1) (or a simulator); (iii) a co-safe LTL property
$\phi$; (iv) a finite set $\Xi$ of NN controllers; and (v) disturbance bound
$V$, check if there exists a NN-based control strategy $\boldsymbol{\xi}$
(Definition II.2), so that $\mathbb{P}_{\tau({\mathbf{x}}_{0})\sim
D}(\tau({\mathbf{x}}_{0})\models\phi|\boldsymbol{\xi},{\mathcal{X}}_{0})=1$,
for all initial states ${\mathbf{x}}_{0}\in{\mathcal{X}}_{0}$; if there exists
such a $\boldsymbol{\xi}$, compute it, as well.

##  III Neuro-Symbolic Control
for Temporal Logic Tasks

We propose a new method to design verified compositions of NN controllers for
co-safe LTL tasks; see Alg. 1. First, we translate the LTL formula $\phi$ into
a Deterministic Finite state Automaton (DFA) [line 2, Alg. 1]; see Section
III-A. Second, building upon [38, 43], we leverage the DFA to decompose $\phi$
into reach-avoid properties [line 3, Alg. 1]; see Sections III-B-III-C. Then,
we apply graph-search methods combined with reachability analysis to check if
there exists $\boldsymbol{\xi}$ so that
$\mathbb{P}_{\tau({\mathbf{x}}_{0})\sim
D}(\tau({\mathbf{x}}_{0})\models\phi|\boldsymbol{\xi},{\mathcal{X}}_{0})=1$,
for all ${\mathbf{x}}_{0}\in{\mathcal{X}}_{0}$ [line 4, Alg. 1]; see Section
III-D. Then, the proposed algorithm returns either False if such a control
strategy $\boldsymbol{\xi}$ does not exist or, otherwise, True along with
$\boldsymbol{\xi}$ [line 5, Alg. 1]. Trade-offs between completeness and
computational efficiency are discussed in Section IV.

Algorithm 1 Verified Compositional Neuro-Symbolic Control for Stochastic
Systems with Temporal Logic Tasks

1:Input: Formula $\phi$; System Dynamics/Simulator (1); Controllers $\Xi$;
Disturbance Bound $V$

2:Translate $\phi$ into DFA $D$ (Section III-A)

3:Using $D$, decompose $\phi$ into reach-avoid properties (Sections III-B-
III-C)

4:Apply graph-search & reachability analysis over the DFA state-space (Section
III-D)

5:Output: Verification result
$R\in\\{[\texttt{True},\boldsymbol{\xi}],\texttt{False}\\}$

###  III-A From LTL formulas to DFA

First, we translate $\phi$, constructed using $\mathcal{AP}$, into a DFA
defined as follows [1]; see also Fig. 2(a).

######  Definition III.1 (DFA).

A Deterministic Finite state Automaton (DFA) $D$ over
$\Sigma=2^{\mathcal{AP}}$ is defined as a tuple
$D=\left({\mathcal{Q}}_{D},q_{D}^{0},\Sigma,\delta_{D},q_{D}^{F}\right)$,
where ${\mathcal{Q}}_{D}$ is the set of states,
$q_{D}^{0}\in{\mathcal{Q}}_{D}$ is the initial state, $\Sigma$ is an alphabet,
$\delta_{D}:{\mathcal{Q}}_{D}\times\Sigma\rightarrow{\mathcal{Q}}_{D}$ is a
deterministic transition relation, and $q_{D}^{F}\in{\mathcal{Q}}_{D}$ is the
accepting/final state.

(a)

(b)

Figure 2: (a) DFA corresponding to
$\phi=(\Diamond\pi^{\ell_{1}})\wedge(\Diamond\pi^{\ell_{2}})\wedge(\neg\pi^{\ell_{1}}{\mathcal{U}}\pi^{\ell_{2}})\wedge(\neg(\pi^{\ell_{3}}\vee\pi^{\ell_{4}}\vee\pi^{\ell_{5}}){\mathcal{U}}\pi^{\ell_{1}})$.
(b) Illustration of the reachable sets over the DFA state space (see Section
III-D)

To interpret a temporal logic formula over a realization of
$\tau({\mathbf{x}}_{0})$ generated by (1), we use a labeling function
$L:{\mathcal{X}}\rightarrow 2^{\mathcal{AP}}$ that maps system states to
symbols $\sigma\in\Sigma$. A realization of $\tau({\mathbf{x}}_{0})$, denoted
by ${\mathbf{x}}_{0},{\mathbf{x}}_{1},\dots,{\mathbf{x}}_{F}$ satisfies $\phi$
if the word $w=L({\mathbf{x}}_{0})L({\mathbf{x}}_{1})\dots
L({\mathbf{x}}_{F})$ yields an accepting DFA run, i.e., if starting from the
initial state $q_{D}^{0}$, each symbol/element in $w$ yields a DFA transition
so that eventually the final state $q_{D}^{F}$ is reached [1].

###  III-B From DFA to Reach-Avoid Properties

Given any DFA state $q_{D}\in{\mathcal{Q}}_{D}$, we compute a set
${\mathcal{R}}_{q_{D}}$ that collects all DFA states that can be reached, in
one hop, from $q_{D}$ using a symbol $\sigma$. This set is defined as:

${\mathcal{R}}_{q_{D}}=\\{q_{D}^{\prime}~{}|~{}q_{D}^{\prime}=\delta_{D}(q_{D},\sigma),\sigma\in\Sigma\\}.$
(2)

Then, given $q_{D}$ and for each DFA state
$q_{D}^{\prime}\in{\mathcal{R}}_{q_{D}}$, we introduce the following
definitions. We construct a set that collects the states
${\mathbf{x}}\in{\mathcal{X}}$, so that if the system state coincides with one
of these states, then a symbol $\sigma=L({\mathbf{x}})\in\Sigma$ enabling this
DFA transition will be generated. We collect these states in the set
${\mathcal{X}}_{q_{D}\rightarrow q_{D}^{\prime}}$, i.e.,

${\mathcal{X}}_{q_{D}\rightarrow
q_{D}^{\prime}}=\\{{\mathbf{x}}\in{\mathcal{X}}~{}|~{}q_{D}^{\prime}=\delta_{D}(q_{D},L({\mathbf{x}}))\\}$
(3)

Starting from any system state ${\mathbf{x}}\in{\mathcal{X}}$ and a DFA state
$q_{D}$, transition from $q_{D}$ to
$q_{D}^{\prime}\in{\mathcal{R}}_{q_{D}}\setminus q_{D}$ will eventually occur
after $H_{q_{D}}\geq 0$ discrete time steps, if (i) the system state
${\mathbf{x}}_{t}$ remains within ${\mathcal{X}}_{q_{D}\rightarrow q_{D}}$ for
the next $H_{q_{D}}-1$ steps, and (ii) at time $t=H_{q_{D}}$, we have that
${\mathbf{x}}_{H_{q_{D}}}\in{\mathcal{X}}_{q_{D}\rightarrow q_{D}^{\prime}}$.
Essentially, (i)-(ii) model a reach-avoid requirement. For instance, (i) may
require a robot to stay within the obstacle-free space and (ii) may require a
robot to eventually enter a region.

######  Example III.1 (Reach-Avoid Properties).

Consider the DFA shown in Fig. 2(a) that corresponds to the LTL formula
$\phi=(\Diamond\pi^{\ell_{1}})\wedge(\Diamond\pi^{\ell_{2}})\wedge(\neg\pi^{\ell_{1}}{\mathcal{U}}\pi^{\ell_{2}})\wedge(\neg(\pi^{\ell_{3}}\vee\pi^{\ell_{4}}\vee\pi^{\ell_{5}}){\mathcal{U}}\pi^{\ell_{1}})$.
Since there exists a DFA transitions from $q_{D}^{0}$ to the states
$q_{D}^{0},q_{D}^{1},q_{D}^{F}$, we have that
${\mathcal{R}}_{q_{D}^{0}}=\\{q_{D}^{0},q_{D}^{1},q_{D}^{F}\\}$. Also, the
Boolean formulas on top of the DFA transitions capture the conditions under
which these transitions can be enabled. For instance, the self loop in
$q_{D}^{0}$ is enabled if the robot is outside the regions {$\ell_{1}$,
$\ell_{2}$, $\ell_{3}$, $\ell_{4}$, $\ell_{5}$}. Thus, we have that
${\mathcal{X}}_{q_{D}^{0}\rightarrow
q_{D}^{0}}={\mathcal{X}}\setminus(\ell_{1}\cup\ell_{2}\cup\ell_{3}\cup\ell_{4}\cup\ell_{5})$.
Similarly, we have that ${\mathcal{X}}_{q_{D}^{0}\rightarrow
q_{D}^{1}}=({\mathcal{X}}\setminus(\ell_{1}\cup\ell_{3}\cup\ell_{4}\cup\ell_{5}))\cap\ell_{2}$,
${\mathcal{X}}_{q_{D}^{0}\rightarrow q_{D}^{F}}=\ell_{2}\cap\ell_{1}$ and that
${\mathcal{R}}_{q_{D}^{1}}=\\{q_{D}^{1},q_{D}^{F}\\}$,
${\mathcal{X}}_{q_{D}^{1}\rightarrow
q_{D}^{1}}={\mathcal{X}}\setminus(\ell_{1}\cup\ell_{3}\cup\ell_{4}\cup\ell_{5})$,
and ${\mathcal{X}}_{q_{D}^{1}\rightarrow q_{D}^{F}}=\ell_{1}$.

###  III-C Verifying Reach-Avoid Properties

In what follows, we discuss how to check whether a transition from a DFA state
$q_{D}$ to $q_{D}^{\prime}\neq q_{D}$ can be enabled; later, we will discuss
how this can be used to design verified control policies that satisfy the LTL
formula with probability 1. Specifically, we want to verify that given an
initial set of system states associated with $q_{D}$, denoted by
${\mathcal{X}}_{q_{D}}^{0}$, the conditions (i)-(ii), discussed in Section
III-B, can be satisfied with probability 1; the detailed construction of
${\mathcal{X}}_{q_{D}}^{0}$ will be discussed in Section III-D. Notice that
${\mathcal{X}}_{q_{D}\rightarrow q_{D}^{\prime}}$ may contain more than one
region of interest $\ell_{i}$. As mentioned in Assumption II.1, for every
region of interest $\ell_{i}$ in ${\mathcal{X}}_{q_{D}\rightarrow
q_{D}^{\prime}}$, there exists a NN controller $\xi_{i}\in\Xi$ that has been
trained to drive the system towards $\ell_{i}$. Hereafter, we collect all NN
controllers associated with ${\mathcal{X}}_{q_{D}\rightarrow q_{D}^{\prime}}$
in a set denoted by $\Xi_{q_{D}\rightarrow q_{D}^{\prime}}\subseteq\Xi$.111In
case ${\mathcal{X}}_{q_{D}\rightarrow q_{D}^{\prime}}$ does not contain any
region $\ell_{i}$, then $\Xi_{q_{D}\rightarrow q_{D}^{\prime}}=\emptyset$ by
definition of $\Xi$; see Ex. III.2. Specifically, we want to show that there
exists a finite horizon $H_{q_{D}}$ and at least one NN controller
$\xi\in\Xi_{q_{D}\rightarrow q_{D}^{\prime}}$, so that if the system evolves
as per
${\mathbf{x}}_{t+1}={\mathbf{f}}({\mathbf{x}}_{t},\xi,\boldsymbol{\nu}_{t})$
then the following two conditions hold for all possible initial system states
in ${\mathcal{X}}_{q_{D}}^{0}$ and all possible noise values
$\boldsymbol{\nu}_{t},|\boldsymbol{\nu}_{t}|\leq V$: (i)
${\mathbf{x}}_{t}\in{\mathcal{X}}_{q_{D}\rightarrow q_{D}},\forall
t\in[0,H_{q_{D}}-1]$ and (ii)
${\mathbf{x}}_{H_{q_{D}}}\in{\mathcal{X}}_{q_{D}\rightarrow q_{D}^{\prime}}$.
If such a horizon $H_{q_{D}}$ and controller $\xi\in\Xi_{q_{D}\rightarrow
q_{D}^{\prime}}$ exist, then by definition of the set
${\mathcal{X}}_{q_{D}\rightarrow q_{D}^{\prime}}$ in (3), we have that with
probability one the transition from $q_{D}$ to $q_{D}$ (self-loop) is enabled
within the time interval $[0,H_{q_{D}}-1]$, and at the time step $t=H_{q_{D}}$
the transition from $q_{D}$ to $q_{D}^{\prime}$ occurs. In this case, we say
that the DFA transition from $q_{D}$ to $q_{D}^{\prime}$ is verified to be
safe when the system starts anywhere within ${\mathcal{X}}_{q_{D}}^{0}$ and
applies the controller $\xi$.

To reason about safety of a DFA transition, we leverage existing reachability
analysis tools that can compute forward reachable sets, denoted by
${\mathcal{R}}_{t}({\mathcal{X}}_{q_{D}}^{0},\xi,V)$, collecting all possible
states ${\mathbf{x}}$ that the system may reach after applying a feedback NN
controller $\xi$ for $t$ time steps in the presence of noise, upper bounded by
$V$, for any possible initial state in ${\mathcal{X}}_{q_{D}}^{0}$. Given such
reachable sets, it suffices to check if there exists a finite horizon
$H_{q_{D}}$ and at least one controller $\xi\in\Xi_{q_{D}\rightarrow
q_{D}^{\prime}}$ such that the reachable sets satisfy the following two
conditions:

${\mathcal{R}}_{t}({\mathcal{X}}_{q_{D}}^{0},\xi,V)\subseteq{\mathcal{X}}_{q_{D}\rightarrow
q_{D}},\forall{t}\in[0,\dots,H_{q_{D}}-1],$ (4)

and

${\mathcal{R}}_{H_{q_{D}}}({\mathcal{X}}_{q_{D}}^{0},\xi,V)\subseteq{\mathcal{X}}_{q_{D}\rightarrow
q_{D}^{\prime}}.$ (5)

If both conditions hold, we verify that the DFA transition from $q_{D}$ to
$q_{D}^{\prime}$ is safe given the initial set of states
${\mathcal{X}}_{q_{D}}^{0}$ and the controller $\xi$ [19].

Construction of exact reachable sets is computationally intractable. Thus,
instead, we compute over-approximated reachable sets, denoted by
$\bar{{\mathcal{R}}}_{t}({\mathcal{X}}_{q_{D}}^{0},\xi,V)$, where
${\mathcal{R}}_{t}({\mathcal{X}}_{q_{D}}^{0},\xi,V)\subseteq\bar{{\mathcal{R}}}_{t}({\mathcal{X}}_{q_{D}}^{0},\xi,V)$,
using recently proposed reachability tools for stochastic systems [39]. If the
following two conditions are satisfied

$\bar{{\mathcal{R}}}_{t}({\mathcal{X}}_{q_{D}}^{0},\xi,V)\subseteq{\mathcal{X}}_{q_{D}\rightarrow
q_{D}},\forall{t}\in[0,\dots,H_{q_{D}}-1]$ (6)
$\bar{{\mathcal{R}}}_{H_{q_{D}}}({\mathcal{X}}_{q_{D}}^{0},\xi,V)\subseteq{\mathcal{X}}_{q_{D}\rightarrow
q_{D}^{\prime}},$ (7)

then we say that the considered DFA transition is verified to be safe given
the initial set of states ${\mathcal{X}}_{q_{D}}^{0}$ and a feedback NN
controller $\xi$.222In practice, reachable sets over a large enough horizon
$\bar{H}$ are computed. If there is not reachable set
$\bar{{\mathcal{R}}}_{t}$, for some $t\in\\{0,\dots,\bar{H}\\}$ that satisfies
(7), then we say that the system fails to reach this region of interest. This
is in accordance with related works; see e.g., [21, 19]. Finally, if there is
no self-loop for $q_{D}$, then ${\mathcal{X}}_{q_{D}\rightarrow q_{D}}$ cannot
be defined. In this case, such a transition from $q_{D}$ to $q_{D}^{\prime}$
is verified to be safe if (7) holds for $H_{q_{D}}=1$.

In what follows, we discuss how the over-approximated reachable sets are
computed using the reachability analysis algorithm for stochastic systems
proposed in [39]. This algorithm estimates reachable sets in a sampling-based
manner. Consider a set of (initial) states ${\mathcal{X}}_{q_{D}}^{0}$ that
the system state may be in at $t=0$. Our goal is to compute the reachable sets
at the next $H$ time steps, for some $H\geq 1$. To compute the reachable at
time $t=1$, first, $M$ system states ${\mathbf{x}}_{1}$ are sampled from
${\mathcal{X}}_{q_{D}}^{0}$. Then, using a given NN controller $\xi$ the
corresponding next states ${\mathbf{x}}_{1}$ are computed using a simulator of
the system dynamics (1). Then, we compute a convex hull over all (simulated)
system states ${\mathbf{x}}_{1}$ and we apply padding of size $\epsilon$ to
this convex hull. The padded convex hull is the estimated reachable set at
$t=1$, denoted by $\bar{{\mathcal{R}}}_{1}$. Using $\bar{{\mathcal{R}}}_{t}$
as a set of possible initial states at time $t\geq 1$, we repeat the above
steps to compute the subsequent reachable sets $\bar{{\mathcal{R}}}_{t+1}$,
for all $t\in\\{2,\dots,H\\}$. As per [39], the probability that
$\bar{{\mathcal{R}}}_{t}$ over-approximates the corresponding true reachable
set ${\mathcal{R}}_{t}$ is at least $1-\delta_{M}$, where $\delta_{M}$ depends
on system state dimension $d$, the padding size $\epsilon$, and the number $M$
of sampled points,
$\mathcal{P}({\mathcal{R}}_{t}\subseteq\bar{{\mathcal{R}}}_{t})\geq
1-\delta_{M}$. Notice that the probability that
${\mathcal{R}}_{t}\subseteq\bar{{\mathcal{R}}}_{t}$ for all
$t\in\\{1,\dots,H\\}$ is
$\mathcal{P}_{H}=\prod_{t=1}^{H}\mathcal{P}({\mathcal{R}}_{t}\subseteq\bar{{\mathcal{R}}}_{t})\geq(1-\delta_{M})^{H}$.

######  Example III.2 (Verifying Reach-Avoid Properties (cont)).

Consider the DFA in Fig. 2(a) and, specifically, the transition from
$q_{D}^{0}$ to $q_{D}^{1}$. To reach $q_{D}^{1}$ starting from $q_{D}^{0}$,
the available controllers are $\Xi_{q_{D}^{0}\rightarrow
q_{D}^{1}}=\\{\xi_{2}\\}$ by construction of the set
${\mathcal{X}}_{q_{D}^{0}\rightarrow q_{D}^{1}}$; see Ex. III.1 and Section
II. Let ${\mathcal{X}}_{q_{D}^{0}}^{0}={\mathcal{X}}_{0}$. Then, we compute
reachable sets $\bar{{\mathcal{R}}}_{t}({\mathcal{X}}_{0},\xi_{2},V)$. These
reachable sets are shown in Fig. 2. Observe that $H_{q_{D}^{0}}=3$, since the
sets $\bar{{\mathcal{R}}}_{t}({\mathcal{X}}_{0},\xi_{2},V)$ for $t=0,1,2$
satisfy (6) and $\bar{{\mathcal{R}}}_{3}({\mathcal{X}}_{0},\xi_{2},V)$
satisfies (7). Thus, the transition from $q_{D}^{0}$ to $q_{D}^{1}$ is
verified to be safe. For the transition from $q_{D}^{1}$ to $q_{D}^{F}$, we
have that $\Xi_{q_{D}^{1}\rightarrow q_{D}^{F}}=\\{\xi_{1}\\}$. Verification
of this transition will be discussed in Ex. III.3. Finally, we have
$\Xi_{q_{D}^{0}\rightarrow q_{D}^{0}}=\emptyset$ and
$\Xi_{q_{D}^{1}\rightarrow q_{D}^{1}}=\\{\xi_{2}\\}$.

###  III-D Designing Verified Compositions of NN Controllers

Algorithm 2 Reach_DFS Algorithm

1:Input: $D^{\prime}$; NN controllers $\Xi$; System dynamics/Simulator (1);
Disturbance bound $V$

2:Output: Verification output
$R\in\\{[\texttt{True},\boldsymbol{\xi}],\texttt{False}\\}$

3:Initialize $q_{D}^{\text{cur}}\leftarrow q_{D}^{0}$;
${\mathcal{X}}_{q_{D}^{\text{cur}}}^{0}={\mathcal{X}}_{0}$;
${\mathbf{q}}=q_{D}^{\text{cur}}$;
${\mathcal{V}}_{\text{vis}}=\\{q_{D}^{\text{cur}}\\}$;
$g(q_{D}^{\text{cur}})\leftarrow{\mathcal{X}}_{q_{D}^{\text{cur}}}^{0}$;
$\boldsymbol{\xi}\leftarrow\emptyset$; $E=\texttt{False}$;

4:while $E\neq\texttt{True}$ do

5: Randomly select $q_{D}^{\text{next}}\in{\mathcal{R}}_{q_{D}^{\text{cur}}}$;
${\mathcal{V}}_{\text{vis}}\leftarrow{\mathcal{V}}_{\text{vis}}\cup
q_{D}^{\text{next}}$

6: Compute set of available controllers $\Xi_{q_{D}^{\text{cur}}\rightarrow
q_{D}^{\text{cur}}}$

7: if $\exists$ $H_{q_{D}^{\text{cur}}}$ and
$\xi\in\Xi_{q_{D}^{\text{cur}}\rightarrow q_{D}^{\text{next}}}$ for (6)-(7)
then

8: ${\mathbf{q}}={\mathbf{q}}|q_{D}^{\text{cur}}$;
$\boldsymbol{\xi}\leftarrow\boldsymbol{\xi}|\xi$;
${\mathcal{X}}_{q_{D}^{\text{next}}}^{0}\leftarrow\bar{\mathfrak{R}}_{H_{q_{D}^{\text{cur}}}}(q_{D}^{\text{cur}})$;

9: $q_{D}^{\text{cur}}\leftarrow q_{D}^{\text{next}}$;
$g(q_{D}^{\text{next}})\leftarrow{\mathcal{X}}_{q_{D}^{\text{next}}}^{0}$;

10: if $q_{D}^{\text{cur}}=q_{D}^{F}$ then

11: $R=[\texttt{True},\boldsymbol{\xi}]$; $E=\texttt{True}$;

12: else

13:
${\mathcal{R}}_{q_{D}^{\text{cur}}}\leftarrow{\mathcal{R}}_{q_{D}^{\text{cur}}}\setminus
q_{D}^{\text{next}}$

14: while
${\mathcal{R}}_{q_{D}^{\text{cur}}}\setminus{\mathcal{V}}_{\text{vis}}=\emptyset\wedge{\mathbf{q}}\neq\emptyset$
do

15: $q_{D}^{\text{cur}}\leftarrow{\mathbf{q}}(\text{end})$;
${\mathcal{X}}_{q_{D}^{\text{cur}}}^{0}\leftarrow g(q_{D}^{\text{cur}})$;

16: ${\mathbf{q}}\leftarrow{\mathbf{q}}\setminus{\mathbf{q}}(\text{end})$;
$\boldsymbol{\xi}\leftarrow\boldsymbol{\xi}\setminus\boldsymbol{\xi}(\text{end})$

17: if
${\mathcal{R}}_{q_{D}^{\text{cur}}}\setminus{\mathcal{V}}_{\text{vis}}=\emptyset\wedge{\mathbf{q}}=\emptyset$
then

18: $R\leftarrow\texttt{False}$; $E\leftarrow\texttt{True}$;

To check if there exists a composed NN control strategy $\boldsymbol{\xi}$
that satisfies $\phi$ with probability 1, it suffices to check that the final
DFA state can be reached from the initial state by enabling a sequence of DFA
transitions that are verified to be safe as shown in Section III-A. To check
this, first we view the DFA as a directed graph
$D=\\{{\mathcal{V}},{\mathcal{E}}\\}$ with vertices ${\mathcal{V}}$ and edges
${\mathcal{E}}$ that are determined by the set of states and transitions of
the DFA. Then, by applying a depth-first search algorithm over the DFA, we
check if it is possible to reach the final DFA state from the initial state by
following a sequence of DFA transitions that are verified to be safe as shown
in Section III-C. In what follows, we discuss this process in detail.

As discussed in Section III-C, to verify safety of a DFA transition, an
initial set of states is needed denoted by ${\mathcal{X}}_{q_{D}}^{0}$. This
set captures all possible states in ${\mathcal{X}}$ that the system may have
when it reaches a DFA state $q_{D}$. As a result, ${\mathcal{X}}_{q_{D}}^{0}$
depends on the previous DFA states that the system has gone through to reach
$q_{D}$. To simplify the proposed algorithm, we pre-process $D$ so that each
node in $D$ that can be reached through multiple paths (excluding self-loops)
originating from $q_{D}^{0}$ is replicated so that each replica can be reached
through a unique path (excluding self-loops).333Otherwise,
${\mathcal{X}}_{q_{D}}^{0}$ should depend on both the state $q_{D}$ and the
path to reach $q_{D}$ which may complicate the notations as well as the
description of Alg. 2. We pre-process the graph as follows. For each vertex
$q_{D}\in{\mathcal{V}}$, we define sets that collect its incoming and outgoing
edges denoted by ${\mathcal{E}}_{q_{D}}^{\text{in}}$ and
${\mathcal{E}}_{q_{D}}^{\text{out}}$, respectively. If the number of incoming
edges (excluding self-loops) for $q_{D}$ is greater than $1$, i.e.,
$|{\mathcal{E}}_{q_{D}}^{\text{in}}|>1$ we create
$|{\mathcal{E}}_{q_{D}}^{\text{in}}|$ copies of $q_{D}$ denoted by
$q_{D}^{i}$. Each node $q_{D}^{i}$ has only one incoming edge which is
selected to be the $i$-th edge in ${\mathcal{E}}_{q_{D}}^{\text{in}}$, denoted
by ${\mathcal{E}}_{q_{D}}^{\text{in}}(i)$, while its outgoing edges remain the
same as in the original node $q_{D}$. Then we add all copies to the graph and
remove the original nodes $q_{D}$. We denote the resulting graph by
$D^{\prime}$. An example illustrating this step is shown in Fig. 3.

Figure 3: Illustration of the DFA pre-processing step, discussed in Section
III-D, for the DFA shown in Fig. 2(a). Notice in Fig. 2(a) that that there are
two paths (excluding self-loops) to reach $q_{D}^{F}$ from $q_{D}^{0}$.

Next, we apply a depth-first search (DFS) method over $D^{\prime}$ to see if
$q_{D}^{F}$ can be reached from $q_{D}^{0}$ through a sequence of DFA
transitions that are verified to be safe. This process is summarized in Alg.
2. We note that the only difference with the standard DFS algorithm is that
here reachability analysis is applied to check if a node $q_{D}$ can be
reached from another node $q_{D}^{\prime}$. The inputs to Alg. 2 are the graph
$D^{\prime}$, the set $\Xi$ of NN controllers and the system
dynamics/simulator (1) [line 1, Alg. 2]. In what follows, we describe in
detail how DFS is applied.

Let $q_{D}^{\text{cur}}$ denote the currently visited node in $D^{\prime}$. We
initialize $q_{D}^{\text{cur}}$ as $q_{D}^{\text{cur}}=q_{D}^{0}$. The set of
all possible states in ${\mathcal{X}}$ that the system can be when it reaches
$q_{D}^{\text{cur}}$ is denoted by ${\mathcal{X}}_{q_{D}^{\text{cur}}}^{0}$.
We initialize ${\mathcal{X}}_{q_{D}^{\text{cur}}}^{0}={\mathcal{X}}_{0}$. As
required in the DFS algorithm, we define a set ${\mathcal{V}}_{\text{vis}}$
that collects all nodes in $D^{\prime}$ that have been visited and a sequence
${\mathbf{q}}$ of nodes that points to the current path from $q_{D}^{0}$
towards $q_{F}$. They are initialized as
${\mathcal{V}}_{\text{vis}}=\\{q_{D}^{0}\\}$ and ${\mathbf{q}}=q_{D}^{0}$.
Also we initialize the control strategy $\boldsymbol{\xi}$ as an empty
sequence. We also define a function $g:{\mathcal{V}}\rightarrow{\mathcal{X}}$
that maps a DFA state $q_{D}\in{\mathcal{V}}$ to the corresponding set
${\mathcal{X}}_{q_{D}}^{0}$. This function that is constructed on-the-fly is
needed only as way to store and recover from memory the sets
${\mathcal{X}}_{q_{D}}^{0}$ [lines 2-3, Alg. 2]. Given $q_{D}^{\text{cur}}$,
we randomly select a next state
$q_{\text{next}}\in{\mathcal{R}}_{q_{D}^{\text{cur}}}$. Then we apply
reachability analysis over the transition from $q_{D}^{\text{cur}}$ to
$q_{D}^{\text{next}}$ using the NN controllers
$\Xi_{q_{D}^{\text{cur}}\rightarrow q_{D}^{\text{next}}}\subseteq\Xi$ and the
initial set of states ${\mathcal{X}}_{q_{D}^{\text{cur}}}^{0}$ [lines 5-6,
Alg. 2]; see Section III-C. If the transition is verified to be safe, then we
append $q_{D}^{\text{cur}}$ to ${\mathbf{q}}$. Also, we append the controller
$\xi\in\Xi_{q_{D}^{\text{cur}}\rightarrow q_{D}^{\text{next}}}$ for which this
transition is safe to $\boldsymbol{\xi}$ that denotes the current control
strategy to reach $q_{D}^{\text{next}}$ from $q_{D}^{0}$ [lines 7-8, Alg. 2].
The corresponding horizon $H_{q_{D}^{\text{cur}}}$ should be stored as well,
as it determines for how long the controller should be applied for; we abstain
from this for simplicity of presentation. The final reachable set
$\bar{{\mathcal{R}}}_{H_{q_{D}^{\text{cur}}}}(q_{D}^{\text{cur}},\xi,V)$
becomes the set ${\mathcal{X}}_{q_{D}^{\text{next}}}^{0}$; see Ex. III.3 and
Fig. 2 as well [line 8, Alg. 2]. Also, $g(q_{D}^{\text{next}})$ is constructed
on-the-fly as $g(q_{D}^{\text{next}})={\mathcal{X}}_{q_{D}^{\text{next}}}^{0}$
and we replace $q_{D}^{\text{cur}}$ with $q_{D}^{\text{next}}$ [line 9, Alg.
2]. If the transition $q_{D}^{\text{cur}}\rightarrow q_{D}^{\text{next}}$ is
not verified to be safe, we remove $q_{D}^{\text{next}}$ from the set
${\mathcal{R}}_{q_{D}^{\text{cur}}}$ (see (2)). Then we remove the last
element in ${\mathbf{q}}$ and $\boldsymbol{\xi}$, denoted by
${\mathbf{q}}(\text{end})$ and $\boldsymbol{\xi}(\text{end})$, while
${\mathbf{q}}(\text{end})$ is assigned to $q_{D}^{\text{cur}}$ until we find
another state in ${\mathcal{R}}_{q_{D}^{\text{cur}}}$ that has not been
visited yet [lines 12-16, Alg. 2]. The above process is repeated until
$q_{D}^{\text{cur}}$ is updated to be $q_{D}^{F}$. In this case, we have found
a NN control strategy $\boldsymbol{\xi}$ that satisfies $\phi$ for all initial
states ${\mathbf{x}}_{0}\in{\mathcal{X}}_{0}$ [line 10-11, Alg. 2]. If
${\mathbf{q}}$ is empty and we fail to find another state in
${\mathcal{R}}_{q_{D}^{\text{cur}}}$ that is not visited, then the proposed
method cannot find a feasible path from $q_{D}^{0}$ to $q_{D}^{F}$ (even
though it may exist; see Section IV) [lines 17-18, Alg. 2]. Any other graph-
search method in conjunction with reachability analysis can be used as well.

######  Example III.3 (Verified Compositional Control Synthesis ).

We continue Ex. III.2; see also Fig. 2. To verify the DFA transition from
$q_{D}^{\text{cur}}=q_{D}^{1}$ to $q_{D}^{\text{next}}=q_{D}^{F}$, we
initialize
${\mathcal{X}}_{q_{D}^{1}}^{0}=\bar{{\mathcal{R}}}_{3}({\mathcal{X}}_{0},\xi_{2},V)$.
By computing
$\bar{{\mathcal{R}}}_{t}({\mathcal{X}}_{q_{D}^{1}}^{0},\xi_{1},V)$, we verify
that this DFA transition is safe. Thus, there exists
$\boldsymbol{\xi}=\xi_{2},\xi_{1}$ where $\xi_{2}$ and $\xi_{1}$ are applied
for $3$ and $2$ time steps, respectively, so that
$\mathbb{P}_{\tau({\mathbf{x}}_{0})\sim
D}(\tau({\mathbf{x}}_{0})\models\phi|\boldsymbol{\xi},{\mathcal{X}}_{0})=1$,
for all ${\mathbf{x}}_{0}\in{\mathcal{X}}_{0}$.

##  IV Correctness & Completeness

In this section, first we show correctness of the proposed algorithm is
probabilistically correct. Additionally, we provide conditions under which the
proposed algorithm is complete and discuss trade-offs between completeness and
computational efficiency.

######  Proposition IV.1 (Correctness).

Algorithm 1 is probabilistically correct, i.e., if it computes a NN control
strategy $\boldsymbol{\xi}$ with horizon $F=\sum_{k=0}^{K}H_{k}$, as defined
in Definition II.2, then $\boldsymbol{\xi}$ satisfies $\phi$ with probability
that is at least equal to $(1-\delta_{M})^{F}$.

###### Proof.

This result holds by construction of Alg. 1. To show this, assume that Alg. 2
returns a control strategy $\boldsymbol{\xi}$. Each feedback controller
$\mu(k)$ in $\boldsymbol{\xi}$ is applied for $H_{k}\geq 1$ time-steps, i.e.,
$\mu(k)$ is applied for all time instants $t\in[t_{k},t_{k}+H_{k}]$, where
$t_{0}=0$ and $t_{k}=\sum_{n=0}^{k-1}H_{n}$ for all $k\geq 1$. Consider the
sequence of the computed reachable sets that correspond to $\boldsymbol{\xi}$,
generated after applying every $\mu(k)$ in $\boldsymbol{\xi}$ for $H_{k}$ time
units for $k=0,1,\dots,K$ in this specific order. By construction of the
algorithm, these reachable sets satisfy (6)-(7). If the computed reachable
sets over-approximate the true ones, then satisfaction of (6)-(7) implies that
the conditions (4)-(5) hold as well. The condition in (4) implies that, given
a fixed $k$, when the system applies $\mu(k)$ for all time instants
$t\in[t_{k},t_{k}+H_{k}-1]$, it remains in a DFA state, denoted by $q_{D}^{k}$
with probability one for all $t\in[t_{k},t_{k}+H_{k}-1]$ (when $k=0$ this DFA
state is the initial one). In other words, the system, driven by $\mu(k)$,
generates observations (i.e., $L({\mathbf{x}}_{t})$) that allow it to stay in
$q_{D}^{k}$ for all $t\in[t_{k},t_{k}+H_{k}-1]$. The condition in (5) implies
that at time $t_{k+1}=t_{k}+H_{k}$, a new DFA state, denoted by $q_{D}^{k+1}$
will be reached with probability one.444Note that if $H_{k}=1$, this means
that the system will stay at $q_{D}^{k}$ only at the time instant $t_{k}$.
This can be the case e.g., because there is no self-loop at $q_{D}^{k}$ or
because the self-loop transition at $q_{D}^{k}$ is not activated once the
system reaches this DFA state. The above holds for all $k=0,1,\dots,K$, and,
therefore, a new DFA state $q_{D}^{k}$ is reached with probability one at
every time instant $t_{k}$. This results in a sequence of DFA states
${\mathbf{q}}=q_{D}^{0},q_{D}^{1},\dots,q_{D}^{k},\dots,q_{D}^{K}$. By
construction of Alg. 2, a policy $\boldsymbol{\xi}$ is returned when the final
DFA state is included in ${\mathbf{q}}$. Thus, at time instant $t_{K}$ the DFA
state $q_{D}^{K}$ that is reached is the final one. As a result, the resulting
policy ensures that if the system executes the control strategy
$\boldsymbol{\xi}$, then a sequence of DFA transitions leading to the final
state will be activated with probability one only if the computed reachable
sets over-approximate the true reachable sets. Since the latter holds with
probability of at least $(1-\delta_{M})^{F}$ (see Sec.III-C), this
equivalently means that the LTL formula is satisfied with probability that is
at least equal to $(1-\delta_{M})^{F}$ completing the proof. ∎

######  Remark 1 (Computational Efficiency vs Completeness).

In general, our method is not complete in the sense that it may not find a
control strategy $\boldsymbol{\xi}$ that satisfies $\phi$ with probability
one, for all ${\mathbf{x}}_{0}\in{\mathcal{X}}_{0}$, even though such a
strategy exists. This is due to the fact that (a) Alg. 2 computes over-
approximated (instead of exact) reachable sets and that (b) it does not
exhaustively search over all possible combinations of NN control actions that
the system can apply when a new DFA state is reached. To elaborate more on
(b), consider the following cases. (b.i) Given an initial set of states for
$q_{D}^{\text{cur}}$, Alg. 2 reasons about safety of a transition from
$q_{D}^{\text{cur}}$ to $q_{D}^{\text{next}}$, using only controllers selected
from $\Xi_{q_{D}^{\text{cur}}\rightarrow q_{D}^{\text{next}}}$. If this
transition is unsafe, then it is discarded. However, this transition may
become feasible if the initial set of states changes, which can happen by
applying a controller from $\Xi_{q_{D}^{\text{cur}}\rightarrow
q_{D}^{\text{cur}}}$ for some $\hat{H}$ time steps. Searching over all
possible values of $\hat{H}$ that may result in safe transitions is
computationally intractable as $\hat{H}$ is not upper bounded. This can
possibly be alleviated by considering bounded LTL formulas [44]. (b.ii)
Additionally, as soon as Alg. 2 finds a
$\xi\in\Xi_{q_{D}^{\text{cur}}\rightarrow q_{D}^{\text{next}}}$ for which the
corresponding transition is safe, it proceeds to new DFA transitions. However,
that transition may be safe for other controllers in
$\xi\in\Xi_{q_{D}^{\text{cur}}\rightarrow q_{D}^{\text{next}}}$ as well, where
each one yields a different initial set for subsequent DFA transitions
affecting their safety. This can be tackled by exhaustively searching over all
possible controllers that the system can apply to enable the transition from
$q_{D}^{\text{cur}}$ to $q_{D}^{\text{next}}$. Addressing the challenges
discussed in (b.i)-(b.ii) will increase the computational cost of Alg. 2.
Similar trade-offs between completeness and computational efficiency are quite
common in related works; see e.g., [45]. The proposed method in its current
form is complete if (i) there are no self-loops in the DFA states, or if
$\Xi_{q_{D}\rightarrow q_{D}}=\emptyset$ for all states (see e.g., Ex. III.2);
(ii) $|\Xi_{q_{D}\rightarrow q_{D}^{\prime}}|=1$, for all
$q_{D}\in{\mathcal{Q}}_{D}\setminus\\{q_{D}^{F}\\}$; (iii) the reachable sets
are accurately computed. Conditions (i)-(ii) trivially address (b.i)-(b.ii)
while (iii) trivially tackles (a).

##  V Experiments

In this section, we demonstrate our method on complex navigation tasks for
ground robots. In Section V-A, we define the dynamics of the considered robots
and we discuss how we design the sets $\Xi$ of NN controllers. Using this set
of base controllers, in Sections V-B-Section V-C, we design new composite
controllers that can accomplish more complex tasks, with temporal and logical
requirements, in a zero-shot fashion. Particularly, in Section V-B we
illustrate the performance of the proposed algorithm in simulated settings.
Next, in Section V-C, we present hardware experiments that demonstrate the
benefits and limitations of our approach with respect to the sim2real gap. All
simulations have been run on a computer with 64 GB RAM and a GeForce RTX 3080
graphic card.

###  V-A Experiment Setup: Robot Dynamics, NN Control Design, and Reachability
Analysis

Ground Robot Dynamics: We consider a ground robot with the following
differential drive dynamics:

$\begin{bmatrix}x_{t+1}^{1}\\\ x_{t+1}^{2}\\\
\theta_{t+1}\end{bmatrix}=\begin{bmatrix}x_{t}^{1}\\\ x_{t}^{2}\\\
\theta_{t}\end{bmatrix}+\begin{bmatrix}u_{1}\operatorname{sinc}(\frac{u_{2}\tau}{2})\cos(\theta_{t}+\frac{u_{2}\tau}{2})\\\
u_{1}\operatorname{sinc}(\frac{u_{2}\tau}{2})\sin(\theta_{t}+\frac{u_{2}\tau}{2})\\\
\tau u_{2}\end{bmatrix}+\begin{bmatrix}\nu_{1}\\\ \nu_{2}\\\
\nu_{3}\end{bmatrix}$ (8)

The ground robot state is defined as
${\mathbf{x}}=[x_{t}^{1};x_{t}^{2};\theta_{t}]\in\mathbb{R}^{3}$ capturing the
position and direction of the robot at time $t$. The vector control input
${\mathbf{u}}\in\mathbb{R}^{2}$ consists of the linear velocity $u_{1}$ and
angular velocity $u_{2}$, where $u_{1}\in[-0.22,0.22]$ and
$u_{2}\in[-0.15,0.15]$ for any $t>0$. The noise signal
$\boldsymbol{\nu}=[\nu_{1};\nu_{2};\nu_{3}]\in\mathbb{R}^{3}$ is bounded such
that $\forall i\in\\{1,\dots,3\\},\nu_{i}\in[-0.002,0.002]$.

NN Control Design: Next, we discuss how we train the NN controllers for the
ground robot using Model Predictive Control (MPC) methods. As it will be
discussed later, the LTL tasks require the robot to reach/avoid disjoint
regions interests $\ell_{i}\in\mathbb{R}^{2}$ that belong to the physical
workspace. To train a NN controller $\xi_{i}$, first we generate a random set
of states ${\mathbf{x}}\in\mathbb{R}^{3}$. Starting from each one of these
states, we generate a sequence of pairs of states and control inputs that
drive the robot towards the interior of $\ell_{i}$ using an off-the-shelf MPC
solver [46]. Using the resulting training dataset, we train a feedforward NN
controller $\xi_{i}$ with $2$ hidden layers, $40$ neurons per layer and ReLU
activation functions that imitates MPC. The performance of trained NN
controllers can be found in Appendix A.

###  V-B Numerical Simulations

(a) $q_{D}^{0}\rightarrow q_{D}^{1}$ ($\epsilon=0.03$)

(b) $q_{D}^{1}\rightarrow q_{D}^{F}$ ($\epsilon=0.03$)

Figure 4: Verification of DFA transitions for Section V-B ($M=600,000$) . The
regions of interest that need to be avoided/reached to enable this DFA
transition are shown with red/green color. All other regions are not shown.
All reachable sets that are outside/inside the regions to reach are shown with
yellow/green color.

(a)

(b)

Figure 5: (a) DFA for the numerical experiment; (b) DFA for hardware
experiment. The red dashed transition corresponds to an infeasible transition.

In what follows, we demonstrate the proposed algorithm in an LTL-encoded
navigation task. Additional simulations can be found in Appendix B.
Specifically, we consider a ground robot residing in an environment shown in
Fig. 4 and tasked with the following LTL formula

$\phi=(\Diamond\pi^{\ell_{1}})\wedge(\Diamond\pi^{\ell_{3}})\wedge(\neg(\pi^{\ell_{4}}\vee\pi^{\ell_{5}}){\mathcal{U}}\pi^{\ell_{1}})\wedge(\neg(\pi^{\ell_{4}}\vee\pi^{\ell_{5}}){\mathcal{U}}\pi^{\ell_{3}}).$

This task requires the robot to eventually visit the regions $\ell_{1}$ and
$\ell_{3}$, in any order, while avoiding the obstacles $\ell_{4}$ and
$\ell_{5}$. This LTL formula corresponds to a DFA with 4 states and 5
transitions as shown in Fig. 5(a). Notice that the transition from $q_{D}^{0}$
to $q_{D}^{F}$ is pruned and, therefore, not considered during verification,
since it requires the robot to be present in more than one region
simultaneously [47]. The initial set ${\mathcal{X}}_{0}$ is defined as
$\\{{\mathbf{x}}_{0}\in{\mathcal{X}}|x_{0}^{1},x_{0}^{2}\in[3.2,3.3],\theta_{0}\in[4.24,4.26]\\}$.
To compute the reachable sets, we apply $\epsilon$-RandUP using $M=600,000$
sampled points for the initial set of states with padding size of
$\epsilon=0.03$. This guarantees that each reachable set at $t\geq 1$ is the
outer-approximation of its true reachable set with a probability greater than
$0.9996$ given ${\mathcal{X}}_{0}$ [39]. Our method, first, investigates the
DFA transition from $q_{D}^{0}$ to $q_{D}^{1}$. This transition requires the
ground robot to stay within the obstacle-free space (i.e., avoid the obstacles
$\ell_{1}$, $\ell_{4}$ and $\ell_{5}$) and eventually reach $\ell_{3}$.
Therefore, we have that $\Xi_{q_{D}^{0}\rightarrow q_{D}^{1}}=\\{\xi_{3}\\}$.
The corresponding reachable sets for this DFA transition, constructed using
the controller $\xi_{3}$, are shown in Figure 4(a). Observe that the reachable
sets
$\bar{{\mathcal{R}}}_{1}({\mathcal{X}}_{0},\xi_{3},V),\dots,\bar{{\mathcal{R}}}_{6}({\mathcal{X}}_{0},\xi_{3},V)$
are fully outside the obstacle regions (as required by the self-loop
transition of $q_{D}^{0}$) while
$\bar{{\mathcal{R}}}_{7}({\mathcal{X}}_{0},\xi_{3},V)$ is fully inside
$\ell_{3}$. Thus, the transition for $q_{D}^{0}$ to $q_{D}^{1}$ is verified to
be safe with probability that is at least equal to $0.9996^{7}$. Once the DFA
state $q_{D}^{1}$ is reached, its self-loop transition is satisfied since the
system state is outside $\ell_{1}$, $\ell_{4}$ and $\ell_{5}$. Next, the DFA
transition from $q_{D}^{1}$ to $q_{D}^{F}$ is considered requiring the robot
to reach $\ell_{1}$ while avoiding the obstacle regions. Thus, in this case,
we have that $\Xi_{q_{D}^{1}\rightarrow q_{D}^{F}}=\\{\xi_{1}\\}$. The set of
initial states for this transition is
${\mathcal{X}}_{q_{D}^{1}}^{0}=\bar{{\mathcal{R}}}_{7}({\mathcal{X}}_{0},\xi_{3},V)$.
We again sample $M=600,000$ points within ${\mathcal{X}}_{q_{D}^{1}}^{0}$ in
our reachability analysis. After computing the reachable sets
$\bar{{\mathcal{R}}}_{t}({\mathcal{X}}_{q_{D}^{1}}^{0},\xi_{1},V)$ shown in
Figure 4(b), we can see that the reachable sets over next $25$ time steps are
outside the obstacles while
$\bar{{\mathcal{R}}}_{26}({\mathcal{X}}_{q_{D}^{1}}^{0},\xi_{1},V)$ is inside
$\ell_{1}$ verifying that this DFA transition is also safe with probability at
least equal to $(0.9996)^{26}$. Thus, there exists a control strategy
$\boldsymbol{\xi}=\xi_{3},\xi_{1}$ where $H_{1}=7,H_{2}=26$ such that
$\mathbb{P}_{\tau({\mathbf{x}}_{0})\sim
D}(\tau({\mathbf{x}}_{0})\models\phi|\boldsymbol{\xi},{\mathcal{X}}_{0})\geq(0.9996)^{33}=0.9869$.

Next, we discuss how the conservativeness of reachability analysis (arising
due to overapproximation of reachable sets) can affect control design. To this
end, we decrease the number of sampled points from $M=600,000$ to $M=50,000$.
Using $M=50,000$, $\epsilon$-RandUP requires the padding size $\epsilon$ to
increase from $0.03$ to $0.1$ to ensure that the generated reachable sets
over-approximate the true ones with probability greater than $0.9999$. This
essentially results in larger reachable sets which may affect the output of
Algorithm 1. Specifically, using $\epsilon=0.1$, the transition from
$q_{D}^{0}$ to $q_{D}^{1}$ is still verified to be safe. However, the
transition from $q_{D}^{1}$ to $q_{D}^{F}$ is verified to be unsafe as the
reachable sets intersect with the obstacles. The latter reachable sets are
illustrated in Figure 8 in Appendix A. Notice that decreasing the number of
sampled points can decrease the total runtime required for reachability
analysis. Specifically, the runtime to compute all reachable sets for
verification when $M=50,000$ and $M=600,000$ is $12$ and $66$ seconds,
respectively. In summary, although decreasing the total number $M$ of sampled
points can result in shorter runtimes, it increases the conservativeness of
reachability analysis which may not allow Algorithm 1 to compute a feasible
controller even if it exists.

###  V-C Hardware Experiments

(a) TurtleBot3 Waffle Pi

(b) Experiment Environment

Figure 6: Turtlebot and environment setup for hardware experiment

Next, we demonstrate the proposed algorithm on hardware experiments.
Specifically, we consider a TurtleBot3 Waffle Pi ground robot operating in an
indoor environment shown in Fig. 6. The robot is responsible for accomplishing
the following LTL-encoded task

$\displaystyle\phi=(\Diamond\pi^{\ell_{1}})\wedge(\Diamond\pi^{\ell_{2}})\wedge(\neg\pi^{\ell_{1}}{\mathcal{U}}\pi^{\ell_{2}})\wedge$
$\displaystyle(\neg(\pi^{\ell_{4}}\vee\pi^{\ell_{5}}\vee\pi^{\ell_{6}}){\mathcal{U}}\pi^{\ell_{1}})\wedge(\neg(\pi^{\ell_{4}}\vee\pi^{\ell_{5}}\vee\pi^{\ell_{6}}){\mathcal{U}}\pi^{\ell_{2}}),$

requiring it to visit region $\ell_{2}$ and $\ell_{1}$ in this order while
avoiding obstacles $\ell_{4}$, $\ell_{5}$ and $\ell_{6}$. This formula
corresponds to the DFA shown in Fig. 5(b). In what follows, we consider the
same NN controllers used for the numerical experiments in Section V-B. We
apply $\epsilon$-RandUP using $\epsilon=0.03$ and $M=600,000$. As discussed in
Section V-B, this ensures that the constructed reachable sets over-approximate
the true ones with a probability greater than $0.9996$. The set
${\mathcal{X}}_{0}$ is designed so that it collects all possible robot states
with $x^{1}_{0}\in[2.95,3.05]$, $x^{2}_{0}\in[2.95,3.05]$, and
$\theta_{0}\in[3.92,3.94]$. To account for the robot size, in our reachability
analysis, we shrink and inflate the regions of interest and obstacles,
respectively, by the radius of the robot.

Our method, first, investigates DFA transition from $q_{D}^{0}$ to
$q_{D}^{1}$. This transition requires the ground robot to reach region
$\ell_{2}$ while avoiding regions $\ell_{1}$, $\ell_{4}$, $\ell_{5}$, and
$\ell_{6}$. Thus, we have $\Xi_{q_{D}^{0}\rightarrow
q_{D}^{1}}=\\{\xi_{2}\\}$. The reachable sets
$\bar{{\mathcal{R}}}_{t}({\mathcal{X}}_{0},\xi_{2},V)$, corresponding to this
DFA transition, are fully outside the obstacle regions over the next 22 time
steps (satisfying the self-loop transition of $q_{D}^{0}$) and go fully inside
$\ell_{2}$ at the $23$ time step; see Fig. 9(a) in Appendix A. As a result,
this DFA transition is verified to be safe with probability at least equal to
$0.9996^{23}$. Next, we investigate the transition from $q_{D}^{1}$ to
$q_{D}^{F}$ which is activated if the robot avoids $\ell_{1}$, $\ell_{4}$,
$\ell_{5}$, and $\ell_{6}$ until it reaches $\ell_{1}$ where
$\Xi_{q_{D}^{1}\rightarrow q_{D}^{F}}=\\{\xi_{1}\\}$. The set of initial
states for this transition will be
${\mathcal{X}}_{q_{D}^{1}}^{0}=\bar{{\mathcal{R}}}_{23}({\mathcal{X}}_{0},\xi_{2},V)$
where we sample $M=600,000$ points again within
${\mathcal{X}}_{q_{D}^{1}}^{0}$. The reachable sets over the next $19$ time
steps are outside the obstacles and reach $\ell_{1}$ at time step $20$; see
Fig. 9(b) in Appendix A. Hence, the DFA transition from $q_{D}^{1}$ to
$q_{D}^{F}$ is also verified with probability that is at least equal to
$0.9996^{20}$. Using these simulated results, the robot will satisfy the
assigned LTL task if it applies controller $\xi_{2}$ for $23$ time units and
then $\xi_{1}$ for $20$ time units with probability
$\mathbb{P}_{\tau({\mathbf{x}}_{0})\sim
D}(\tau({\mathbf{x}}_{0})\models\phi|\boldsymbol{\xi},{\mathcal{X}}_{0}){\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\geq}(0.9996)^{23+20}=0.9829$.

To validate this result in real-world settings, we select at test time $11$
initial robot states and apply the designed control strategy
$\boldsymbol{\xi}$ on the actual robot platform. In our experiments, the robot
localizes itself using existing SLAM algorithms [48]. The robot trajectories
show that the LTL task is indeed satisfied for all selected initial states
${\mathbf{x}}_{0}\in{\mathcal{X}}_{0}$; see Figures 9(a) and 9(b) in Appendix
A. Observe also in these figures (especially in Fig. 9(b)) that some robot
trajectories are slightly outside the reachable sets. We conjecture that this
happens due to potential sim-to-real gap arising from imperfect robot
localization and model inaccuracies; recall that the controller
$\boldsymbol{\xi}$ is designed using a simulator of the robot dynamics as
defined in (8).

Next, we further investigate how the sim-to-real gap may affect robot
performance with respect to satisfaction of the LTL task. Specifically, to
simulate a hard-to-model source of uncertainty in the environment, we put oil
on one of the robot wheels. We select the initial state of the robot to be
${\mathbf{x}}_{0}=[3;3;3.925]$. Notice that the upper bound for the noise
$V=0.002$, used in our simulations, may not be enough to capture such a
potentially unknown source of uncertainty. This may violate the probabilistic
guarantees of the controller $\boldsymbol{\xi}$ designed above. The latter was
validated in our experiments as the robot trajectory was outside the reachable
sets, computed earlier using simulated data, leading to collision with the
obstacle $\ell_{4}$; see Fig. 11 in Appendix A.

##  VI Conclusion

In this paper, we propose a new verified neuro-symbolic control approach for
autonomous systems with stochastic and unknown dynamics with temporal logic
tasks. The proposed method enables systems to compose base skills, modeled by
NN controllers, to verifiably satisfy unseen and complex tasks captured by LTL
formulas. We evaluated the proposed method on robot navigation tasks though
extensive experiments.

## References

  * [1] C. Baier and J.-P. Katoen, _Principles of model checking_. MIT press Cambridge, 2008, vol. 26202649.
  * [2] J. Wang, X. Ding, M. Lahijanian, I. C. Paschalidis, and C. A. Belta, “Temporal logic motion control using actor–critic methods,” _The International Journal of Robotics Research_ , vol. 34, no. 10, pp. 1329–1344, 2015.
  * [3] E. M. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, and D. Wojtczak, “Omega-regular objectives in model-free reinforcement learning,” _TACAS_ , 2018.
  * [4] Q. Gao, D. Hajinezhad, Y. Zhang, Y. Kantaros, and M. M. Zavlanos, “Reduced variance deep reinforcement learning with temporal logic specifications,” in _10th ACM/IEEE International Conference on Cyber-Physical Systems_ , 2019, pp. 237–248.
  * [5] M. Bouton, J. Karlsson, A. Nakhaei, K. Fujimura, M. J. Kochenderfer, and J. Tumova, “Reinforcement learning with probabilistic guarantees for autonomous driving,” _arXiv preprint arXiv:1904.07189_ , 2019.
  * [6] M. Hasanbeig, Y. Kantaros, A. Abate, D. Kroening, G. J. Pappas, and I. Lee, “Reinforcement learning for temporal logic control synthesis with probabilistic satisfaction guarantees,” in _Proc. of the 58th IEEE Conference on Decision and Control (CDC)_ , Nice, France, December 2019.
  * [7] A. K. Bozkurt, Y. Wang, M. M. Zavlanos, and M. Pajic, “Control synthesis from linear temporal logic specifications using model-free reinforcement learning,” in _2020 IEEE International Conference on Robotics and Automation (ICRA)_. IEEE, 2020, pp. 10 349–10 355.
  * [8] A. Lavaei, F. Somenzi, S. Soudjani, A. Trivedi, and M. Zamani, “Formal controller synthesis for continuous-space mdps via model-free reinforcement learning,” in _ACM/IEEE 11th International Conference on Cyber-Physical Systems (ICCPS)_ , 2020, pp. 98–107.
  * [9] M. Hasanbeig, D. Kroening, and A. Abate, “Lcrl: Certified policy synthesis via logically-constrained reinforcement learning,” in _Quantitative Evaluation of Systems: 19th International Conference, QEST 2022, Warsaw, Poland, September 12–16, 2022, Proceedings_. Springer, 2022, pp. 217–231.
  * [10] M. Cai, S. Xiao, B. Li, Z. Li, and Z. Kan, “Reinforcement learning based temporal logic control with maximum probabilistic satisfaction,” in _IEEE International Conference on Robotics and Automation (ICRA)_ , 2021, pp. 806–812.
  * [11] Y. Kantaros, “Accelerated reinforcement learning for temporal logic control objectives,” _arXiv preprint arXiv:2205.04424_ , 2022.
  * [12] M. Fazlyab, M. Morari, and G. J. Pappas, “Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming,” _IEEE Transactions on Automatic Control_ , 2020.
  * [13] G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: An efficient smt solver for verifying deep neural networks,” in _International conference on computer aided verification_. Springer, 2017, pp. 97–117.
  * [14] S. Dutta, S. Jha, S. Sankaranarayanan, and A. Tiwari, “Output range analysis for deep feedforward neural networks,” in _Proceedings of NASA Formal Methods Symposium (NFM)_ , ser. Lecture Notes In Computer Science, vol. 10811. Springer-Verlag, 2018, pp. 121–138.
  * [15] W. Ruan, X. Huang, and M. Kwiatkowska, “Reachability analysis of deep neural networks with provable guarantees,” in _International Joint Conference on Artificial Intelligence_ , 7 2018, pp. 2651–2659.
  * [16] B. Batten, P. Kouvaros, A. Lomuscio, and Y. Zheng, “Efficient neural network verification via layer-based semidefinite relaxations and linear cuts,” in _International Joint Conference on Artificial Intelligence (IJCAI21)_ , 2021, pp. 2184–2190.
  * [17] S. Chen, E. Wong, J. Z. Kolter, and M. Fazlyab, “Deepsplit: Scalable verification of deep neural networks via operator splitting,” _arXiv preprint arXiv:2106.09117_ , 2021.
  * [18] T. Baluta, Z. L. Chua, K. S. Meel, and P. Saxena, “Scalable quantitative verification for deep neural networks,” in _2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE)_. IEEE, 2021, pp. 312–323.
  * [19] C. Huang, J. Fan, W. Li, X. Chen, and Q. Zhu, “Reachnn: Reachability analysis of neural-network controlled systems,” _ACM Transactions on Embedded Computing Systems (TECS)_ , vol. 18, no. 5s, pp. 1–22, 2019.
  * [20] X. Sun, H. Khedr, and Y. Shoukry, “Formal verification of neural network controlled autonomous systems,” in _International Conference on Hybrid Systems: Computation and Control_ , 2019, pp. 147–156.
  * [21] H. Hu, M. Fazlyab, M. Morari, and G. J. Pappas, “Reach-sdp: Reachability analysis of closed-loop systems with neural network controllers via semidefinite programming,” _59th IEEE Conference on Decision and Control (CDC)_ , pp. 5929–5934, December 2020.
  * [22] H.-D. Tran, X. Yang, D. M. Lopez, P. Musau, L. V. Nguyen, W. Xiang, S. Bak, and T. T. Johnson, “NNV: The neural network verification tool for deep neural networks and learning-enabled cyber-physical systems,” _Computer Aided Verification_ , vol. 12224, pp. 3 – 17, 2020.
  * [23] S. Dutta, X. Chen, and S. Sankaranarayanan, “Reachability analysis for neural feedback systems using regressive polynomial rule inference,” in _Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control_ , 2019, pp. 157–168.
  * [24] R. Ivanov, T. Carpenter, J. Weimer, R. Alur, G. Pappas, and I. Lee, “Verisig 2.0: Verification of neural network controllers using taylor model preconditioning,” in _International Conference on Computer Aided Verification_. Springer, 2021, pp. 249–262.
  * [25] H. Sibai, Y. Li, and S. Mitra, “SceneChecker: Boosting scenario verification using symmetry abstractions,” in _International Conference on Computer Aided Verification_. Springer, 2021, pp. 580–594.
  * [26] R. Ivanov, T. J. Carpenter, J. Weimer, R. Alur, G. J. Pappas, and I. Lee, “Verifying the safety of autonomous systems with neural network controllers,” _ACM Transactions on Embedded Computing Systems (TECS)_ , vol. 20, no. 1, pp. 1–26, 2020.
  * [27] H.-D. Tran, F. Cai, M. L. Diego, P. Musau, T. T. Johnson, and X. Koutsoukos, “Safety verification of cyber-physical systems with reinforcement learning control,” _ACM Transactions on Embedded Computing Systems (TECS)_ , vol. 18, no. 5s, pp. 1–22, 2019.
  * [28] S. Carr, N. Jansen, S. Junges, and U. Topcu, “Safe reinforcement learning via shielding for pomdps,” _arXiv preprint arXiv:2204.00755_ , 2022.
  * [29] O. Bastani and S. Li, “Safe reinforcement learning via statistical model predictive shielding,” _Robotics: Science and Systems XVII_ , 2021.
  * [30] G. N. Tasse, D. Jarvis, S. James, and B. Rosman, “Skill machines: Temporal logic composition in reinforcement learning,” _arXiv preprint arXiv:2205.12532_ , 2022.
  * [31] K. Jothimurugan, S. Bansal, O. Bastani, and R. Alur, “Compositional reinforcement learning from logical specifications,” _Advances in Neural Information Processing Systems_ , vol. 34, 2021.
  * [32] Y.-L. Kuo, B. Katz, and A. Barbu, “Compositional rl agents that follow language commands in temporal logic,” _Frontiers in Robotics and AI_ , vol. 8, 2021.
  * [33] C. Neary, C. Verginis, M. Cubuktepe, and U. Topcu, “Verifiable and compositional reinforcement learning systems,” in _Proceedings of the International Conference on Automated Planning and Scheduling_ , vol. 32, 2022, pp. 615–623.
  * [34] R. Ivanov, K. Jothimurugan, S. Hsu, S. Vaidya, R. Alur, and O. Bastani, “Compositional learning and verification of neural network controllers,” _ACM Trans. Embed. Comput. Syst._ , vol. 20, no. 5s, sep 2021. [Online]. Available: https://doi.org/10.1145/3477023
  * [35] R. S. Sutton and A. G. Barto, _Reinforcement learning: An introduction_ , 2018.
  * [36] V. Rubies-Royo, D. Fridovich-Keil, S. Herbert, and C. J. Tomlin, “A classification-based approach for approximate reachability,” in _2019 International Conference on Robotics and Automation (ICRA)_. IEEE, 2019, pp. 7697–7704.
  * [37] A. Bisoffi and D. V. Dimarogonas, “A hybrid barrier certificate approach to satisfy linear temporal logic specifications,” in _2018 Annual American Control Conference (ACC)_ , 2018, pp. 634–639.
  * [38] Y. Kantaros, M. Malencia, V. Kumar, and G. Pappas, “Reactive temporal logic planning for multiple robots in unknown environments,” in _IEEE International Conference on Robotics and Automation (ICRA)_ , June 2020, pp. 11 479–11 485.
  * [39] T. Lew, L. Janson, R. Bonalli, and M. Pavone, “A simple and efficient sampling-based algorithm for general reachability analysis,” in _Learning for Dynamics and Control Conference_. PMLR, 2022, pp. 1086–1099.
  * [40] P. L. Donti, M. Roderick, M. Fazlyab, and J. Z. Kolter, “Enforcing robust control guarantees within neural network policies,” _arXiv preprint arXiv:2011.08105_ , 2020.
  * [41] Z. Xiong, J. Eappen, H. Zhu, and S. Jagannathan, “Robustness to adversarial attacks in learning-enabled controllers,” _arXiv preprint arXiv:2006.06861_ , 2020.
  * [42] J. Wang, S. Kalluraya, and Y. Kantaros, “Verified compositions of neural network controllers for temporal logic control objectives,” _arXiv preprint arXiv:2209.06130_ , 2022.
  * [43] V. Vasilopoulos, Y. Kantaros, G. J. Pappas, and D. E. Koditschek, “Reactive planning for mobile manipulation tasks in unexplored semantic environments,” in _IEEE International Conference on Robotics and Automation (ICRA)_ , 2021, pp. 6385–6392.
  * [44] T. Latvala, A. Biere, K. Heljanko, and T. Junttila, “Simple bounded ltl model checking,” in _Formal Methods in Computer-Aided Design: 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004. Proceedings 5_. Springer, 2004, pp. 186–200.
  * [45] K. Leahy, A. Jones, and C. I. Vasile, “Fast decomposition of temporal logic specifications for heterogeneous teams,” _IEEE Robotics and Automation Letters_ , 2022.
  * [46] P. E. Gill, W. Murray, and M. A. Saunders, “SNOPT: An SQP algorithm for large-scale constrained optimization,” _SIAM review_ , vol. 47, no. 1, pp. 99–131, 2005.
  * [47] Y. Kantaros and M. M. Zavlanos, “Stylus*: A temporal logic optimal control synthesis algorithm for large-scale multi-robot systems,” _The International Journal of Robotics Research_ , vol. 39, no. 7, pp. 812–836, 2020. [Online]. Available: https://doi.org/10.1177/0278364920913922
  * [48] S. P. Thale, M. M. Prabhu, P. V. Thakur, and P. Kadam, “Ros based slam implementation for autonomous navigation using turtlebot,” in _ITM Web of conferences_ , vol. 32. EDP Sciences, 2020, p. 01011.

##  Appendix A Additional Details for Experiments of Section V

In this Appendix, we provide additional details regarding the experimental
validation discussed in Section V.

###  A-A NN Controller Performance

In Table I, we report the performance of the NN controllers used throughout
Section V over a test set collecting initial system states. Specifically, we
apply the NN controller over these initial test-time system states and we
check if the system state can reach the desired region within the same horizon
length as we used for the MPC solver. If so, we treat these test-time
scenarios as successful. The accuracy reported in Table I refers to the
percentage of successful test-time scenarios.

| Controller | Training Set | Test Set | Accuracy
---|---|---|---|---
Ground Robot | $\xi_{1}$ | 4800 | 1200 | $99.8\%$
$\xi_{2}$ | $83.3\%$
$\xi_{3}$ | $79.2\%$
TABLE I: NN Controller Performance

###  A-B Reachable Sets for Numerical Experiment

Next, in Fig. 8, we graphically illustrate the verification of DFA transitions
corresponding to the task of Section V-B when $M=50,000$. Recall that to
maintain the same probabilistic guarantees as in $M=600,000$, the padding size
$\epsilon$ increased to $0.1$. This resulted in larger reachable sets compared
to the ones in Fig. 4(a).

Figure 7: $q_{D}^{1}\rightarrow q_{D}^{F}$ ($\epsilon=0.1$) Figure 8:
Verification of a DFA transition for Section V-B \- $M=50,000$. All reachable
sets that are outside/inside the regions-to-reach are shown with yellow/green
color. Reachable sets that are hitting the regions-to-avoid are shown with red
color. The red line captures robot trajectory. This figure shows that
$q_{D}^{1}\rightarrow q_{D}^{F}$ is verified as unsafe when $\epsilon$
increases.

###  A-C Reachable Sets for Hardware Experiments

Next, in Figure 9, we present the reachable sets computed for the hardware
experiment discussed in Section V-C. Observe that both DFA transitions are
verified to be safe using the robot simulator. Also, observe in this Figure
that the trajectories generated by the actual robot platform remain inside the
reachable sets (with small deviations as discussed in Section V-C). Figure 11
shows a robot trajectory when the robot is subject to exogenous disturbances
(oily wheels) that are not modeled by the system simulator violating the
probabilistic safety guarantees computed using simulated data.

(a) $q_{D}^{0}\rightarrow q_{D}^{1}$

(b) $q_{D}^{1}\rightarrow q_{D}^{F}$

Figure 9: Verification of DFA transitions for the hardware experiment with
$\theta_{0}\in[3.92,3.94]$; The regions of interest that need to be
avoided/reached to enable a DFA transition are shown with red/blue color. All
other regions are not shown. All reachable sets that are outside/inside the
regions to reach are shown with yellow/green color. The green lines capture
robot trajectories corresponding to various initial states. Figure 10:
$q_{D}^{0}\rightarrow q_{D}^{1}$ ($\theta_{0}\in[3.92,3.94]$)  Figure 11:
Verification of a DFA transition for the hardware experiment when the robot is
subject to unmodeled disturbances. All reachable sets that are outside/inside
the region-to-reach are shown with yellow/green color. Reachable sets that are
hitting the regions-to-avoid are shown with red color. The red line captures
robot trajectory when the robot is subject to exogenous disturbances that are
not captured by the system model/simulator. Observe that the actual trajectory
of the robot is outside the reachable sets and eventually leads to collision
with obstacle $\ell_{4}$.

##  Appendix B Additional Numerical Experiment

In this appendix, we provide an additional numerical experiment. We consider
the following LTL formula

$\displaystyle\phi=(\Diamond\pi^{\ell_{1}})\wedge(\Diamond\pi^{\ell_{2}})\wedge(\Diamond\pi^{\ell_{3}})\wedge(\neg\pi^{\ell_{2}}{\mathcal{U}}\pi^{\ell_{3}})\wedge(\neg\pi^{\ell_{1}}{\mathcal{U}}\pi^{\ell_{2}})\wedge$
$\displaystyle(\neg\pi^{\ell_{4}}{\mathcal{U}}\pi^{\ell_{1}})\wedge(\neg\pi^{\ell_{5}}{\mathcal{U}}\pi^{\ell_{1}}),$

requiring the ground robot to eventually visit the regions $\ell_{1}$,
$\ell_{2}$ and $\ell_{3}$, in the order of
$\ell_{3}\rightarrow\ell_{2}\rightarrow\ell_{1}$, while avoiding the obstacles
$\ell_{4}$ and $\ell_{5}$. This formula corresponds to the DFA shown in Fig.
12; notice that the transition from $q_{D}^{0}$ to $q_{D}^{F}$, $q_{D}^{1}$ to
$q_{D}^{F}$, and $q_{D}^{0}$ to $q_{D}^{2}$ were pruned. The initial set
${\mathcal{X}}_{0}$ of system states is defined as
$\\{{\mathbf{x}}_{0}\in{\mathcal{X}}|x_{0}^{1}\in[3.7,3.8];~{}x_{0}^{2}\in[3.5,3.6];~{}\theta_{0}\in[4.02,4.04]\\}$.
To compute the reachable sets, we apply $\epsilon$-RandUP using $M=600,000$
sampled points for the initial set of states with padding size of
$\epsilon=0.03$.

Figure 12: DFA for the case study in Appendix B. The red dashed transitions
correspond to infeasible transitions.

Our method, first, investigates the DFA transition from $q_{D}^{0}$ to
$q_{D}^{1}$. This transition requires the ground robot to stay within the
obstacle-free space (i.e., avoid the obstacles $\ell_{1}$, $\ell_{2}$,
$\ell_{4}$ and $\ell_{5}$) and eventually reach $\ell_{3}$. Therefore, we have
that $\Xi_{q_{D}^{0}\rightarrow q_{D}^{1}}=\\{\xi_{3}\\}$. The corresponding
reachable sets for this DFA transition are shown in Figure 13(a). Notice that
the reachable sets $\bar{{\mathcal{R}}}_{t}({\mathcal{X}}_{0},\xi_{3},V)$ are
fully outside the obstacle regions for
$\bar{{\mathcal{R}}}_{1}({\mathcal{X}}_{0},\xi_{3},V)\sim\bar{{\mathcal{R}}}_{10}({\mathcal{X}}_{0},\xi_{3},V)$
while $\bar{{\mathcal{R}}}_{11}({\mathcal{X}}_{0},\xi_{3},V)$ is fully inside
$\ell_{3}$. Thus, this DFA transition is verified to be safe with the
probability at least equal to $(0.9996)^{11}$. Next, the DFA transition from
$q_{D}^{1}$ to $q_{D}^{2}$ is considered requiring the robot to reach
$\ell_{2}$ while avoiding the obstacle regions $\ell_{1}$, $\ell_{4}$ and
$\ell_{5}$. Thus, we have that $\Xi_{q_{D}^{1}\rightarrow
q_{D}^{2}}=\\{\xi_{2}\\}$. The set of initial states for this transition is
${\mathcal{X}}_{q_{D}^{1}}^{0}=\bar{{\mathcal{R}}}_{11}({\mathcal{X}}_{0},\xi_{3},V)$.
After computing the padded reachable convex hulls
$\bar{{\mathcal{R}}}_{t}({\mathcal{X}}_{q_{D}^{1}}^{0},\xi_{2},V)$ shown in
Figure 13(b), this transition is verified to be safe with the probability of
$(0.9996)^{15}$. Similarly, we can show that the transition from $q_{D}^{2}$
to $q_{D}^{F}$ is also safe with probability at least equal to
$(0.9996)^{11}$; see Figure 14. We conclude that there exists a control
strategy $\boldsymbol{\xi}=\xi_{3},\xi_{2},\xi_{1}$ with $H_{0}=11,H_{1}=15,$
and $H_{3}=11$, such that $\mathbb{P}_{\tau({\mathbf{x}}_{0})\sim
D}(\tau({\mathbf{x}}_{0})\models\phi|\boldsymbol{\xi},{\mathcal{X}}_{0})=(0.9996)^{11+15+11}\geq
0.9853$.

(a) $q_{D}^{0}\rightarrow q_{D}^{1}$ ($\epsilon=0.03$)

(b) $q_{D}^{1}\rightarrow q_{D}^{2}$ ($\epsilon=0.03$)

Figure 13: Verification of DFA transition $q_{D}^{0}\rightarrow q_{D}^{1}$ and
$q_{D}^{1}\rightarrow q_{D}^{2}$ for the numerical experiment discussed in
Appendix B. Figure 14: Verification of DFA transition $q_{D}^{2}\rightarrow
q_{D}^{F}$ for the numerical experiment discussed in Appendix B.