# Verified Compositions of Neural Network Controllers
for Temporal Logic Control Objectives

Jun Wang, Samarth Kalluraya and Yiannis Kantaros The authors are with the
Department of Electrical and Systems Engineering, Washington University in St.
Louis, St. Louis, MO. Email<EMAIL_ADDRESS>
###### Abstract

This paper presents a new approach to design verified compositions of Neural
Network (NN) controllers for autonomous systems with tasks captured by Linear
Temporal Logic (LTL) formulas. Particularly, the LTL formula requires the
system to reach and avoid certain regions in a temporal/logical order. We
assume that the system is equipped with a finite set of trained NN
controllers. Each controller has been trained so that it can drive the system
towards a specific region of interest while avoiding others. 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 composite system behaviors that
satisfy a user-specified LTL task for any initial system state belonging to a
given set. To address this problem, we propose a new approach that relies on a
novel integration of automata theory and recently proposed reachability
analysis tools for NN-controlled systems. We note that the proposed method can
be applied to other controllers, not necessarily modeled by NNs, by
appropriate selection of the reachability analysis tool. We focus on NN
controllers due to their lack of robustness. The proposed method is
demonstrated on navigation tasks for aerial vehicles.

##  I INTRODUCTION

Several methods have been proposed recently to train Neural Network (NN)
controllers for autonomous systems. Such training methods include e.g., deep
reinforcement learning (RL) [1] and model predictive control (MPC) [2].
Despite the high real-time performance of NN-driven systems, they typically
lack safety and robustness guarantees as underscored by recent studies [3]. To
address this limitation, various methods have been proposed to verify
robustness properties of trained NN controllers [4, 5]. For instance, [5]
addresses the problem of output range analysis of trained NNs given an input
set. Safety verification of dynamical systems with feedback NN controllers has
been studied as well in [6, 7, 8, 9, 10, 11, 12] and the references therein.
Typically, these methods investigate if a dynamical system with a trained NN
controller can satisfy a reach-avoid property given a set of possible initial
states.

Common in all the above works is that they focus on learning or verifying the
efficiency/safety of a single NN controller for a given task. However, the
sample complexity and computational cost of learning a single NN controller
increases drastically as the task complexity increases. Motivated by these
limitations, compositional RL methods have been proposed recently that aim to
learn a set of base NN controllers which are then composed to satisfy a
complex task captured by temporal logics; see e.g., [13, 14, 15]. The key idea
in these works is to decompose the task into simpler sub-tasks for which NN
controllers can be learned, 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. To address this issue, in
this paper we propose a new method to design verified temporal compositions of
trained NN controllers for temporal logic tasks. Related is also the recent
work in [16] which, however, unlike the above papers and ours, does not
consider temporal logic tasks. For instance, in [16], the sub-tasks are
revealed by the environment while in [13, 14, 15] the sub-tasks are
‘strategically’ selected to satisfy a temporal logic task.

Specifically, in this paper, we consider autonomous systems tasked with
complex high-level missions captured by a fragment of Linear Temporal Logic
(LTL), called co-safe LTL [17]. We assume that the system is governed by
discrete-time linear time-varying dynamics and that the LTL task requires
reaching and avoiding certain regions in a temporal/logical order. Also, the
system has access to a finite set of already trained controllers modeled as
NNs. Each controller is trained so that it can drive the system towards a
specific region of interest while avoiding others. We do not make any
assumptions about how these NNs have been trained; for instance they may have
been trained using RL or MPC-based methods. Our goal is to check if there
exists a temporal composition of these NN controllers - and if so, to compute
it - that will yield composite system behaviors that always satisfy a user-
specified LTL task for any initial system state belonging to a given set. To
address this problem, we leverage automaton representations of LTL formulas as
well as graph-search methods and existing reachability analysis for NN-driven
systems [8]. We note that our approach can handle any other open-loop or
feedback controllers that are not necessarily modeled as NNs by appropriate
selection of the reachability analysis method. In this paper we focus on NN
controllers due to their fragility to imperceptible input perturbations [3].

Contributions: First, we propose a new approach to design verified temporal
compositions of NN controllers for co-safe LTL tasks. Second, we show
correctness of the proposed method and discuss trade-offs between completeness
and computational efficiency. Third, we demonstrate the efficiency of the
proposed approach on several navigation tasks that involve aerial vehicles.

##  II Problem Formulation

Closed-loop system: We consider discrete-time linear systems defined as
follows:

${\mathbf{x}}_{t+1}={\mathbf{f}}({\mathbf{x}}_{t},{\mathbf{u}}_{t})={\mathbf{A}}_{t}{\mathbf{x}}_{t}+{\mathbf{B}}_{t}{\mathbf{u}}_{t}+{\mathbf{c}}_{t},$
(1)

where ${\mathbf{x}}_{t}\in{\mathcal{X}}\subseteq\mathbb{R}^{d}$ and
${\mathbf{u}}_{t}\in{\mathcal{U}}_{t}\subseteq\mathbb{R}^{n}$ denote the state
and the control input of the system at time $t\geq 0$, respectively. Also,
${\mathbf{A}}_{t}\in\mathbb{R}^{d\times
d},{\mathbf{B}}_{t}\in\mathbb{R}^{d\times n}$ are the system matrices while
${\mathbf{c}}_{t}\in\mathbb{R}^{d}$ is an exogenous input. We assume that
state-space ${\mathcal{X}}$ contains $N>0$ sub-spaces denoted by
$\ell_{i}\subset{\mathcal{X}}$ modelling regions of interest or unsafe areas.
Also, 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 assume that the controller $\xi_{i}$ is selected by the
system when, given any initial state in ${\mathcal{X}}$, the system state
${\mathbf{x}}_{t}$ needs to be driven towards the interior of $\ell_{i}$. We
consider cases where the controllers $\xi_{i}({\mathbf{x}}_{t})$ are
parameterized by multi-layer feed-forward fully-connected neural networks
(NNs). Such NN controllers can be implemented using available methods; see
e.g., [18]. Hereafter, with slight abuse of notation, we denote by $\xi(t)$
the controller selected from $\Xi$ at time $t$. To ensure that 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)$. We denote the
closed-loop system with dynamics (1) and the projected NN control policy as:

${\mathbf{x}}_{t+1}={\mathbf{f}}_{\xi}({\mathbf{x}}_{t})$ (2)

Next, we define a high-level NN-based control strategy $\boldsymbol{\xi}$ as a
temporal composition of the controllers in $\Xi$.

######  Definition II.1 (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 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})$, $\forall
t\in\\{0,1,\dots,H_{0}\\}$. Given $\boldsymbol{\xi}$ and an initial state
${\mathbf{x}}_{0}$, the corresponding closed-loop system (2) generates 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}$.

Linear Temporal Logic Properties: We define mission and safety properties for
the system (1) using Linear Temporal Logic (LTL) as it allows to specify a
wide range of high-level tasks [19, 20]. LTL consists of atomic propositions
(i.e., Boolean variables), denoted by $\mathcal{AP}$, 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 [17].
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. Co-safe LTL formulas are
satisfied by discrete finite plans $\tau$ defined as finite sequences of
system states ${\mathbf{x}}_{t}\in{\mathcal{X}}$. i.e.,
$\tau({\mathbf{x}}_{0})={\mathbf{x}}_{0},{\mathbf{x}}_{1},\dots,{\mathbf{x}}_{t},\dots,{\mathbf{x}}_{F}$,
where $F>0$ denotes a finite horizon [17]. Given $\boldsymbol{\xi}$ and an
initial state ${\mathbf{x}}_{0}$, we say that the closed-loop system (2)
satisfies $\phi$, denoted by ${\mathbf{f}}_{\xi}\models\phi$, if (2) generates
a sequence $\tau({\mathbf{x}}_{0})$ that satisfies $\phi$.

###### Example II.2

Examples of co-safe LTL specifications 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}})$
requires the system to eventually reach the regions $\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.

###### Problem 1

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

######  Remark II.3 (Controllers for LTL tasks)

Several reinforcement learning (RL) methods have been proposed that can train
a single controller, that can be parameterized by a NN, to satisfy an LTL task
$\phi$; see e.g., [1, 21, 22, 23] and the references therein. Verification of
a single NN controller (as opposed to the set of controllers considered here)
with respect to an LTL formula can be accomplished by existing reachability
analysis tools for discrete-time systems; see e.g., [8]. Particularly, a
sequence of reachable sets, capturing all possible system states at future
time instants $t$, needs to be computed under the considered NN controller and
a set of initial states ${\mathcal{X}}_{0}$. Then, it suffices to check if the
atomic predicates that are satisfied across this sequence construct a word
that can be accepted by an automaton of $\phi$ [17].

##  III Verified Compositions of NN Controllers for co-safe LTL Tasks

Our approach to solve Problem 1 consists of the following steps. First, we
translate the LTL formula $\phi$ into a Deterministic Finite state Automaton
(DFA); see Section III-A. Second, by leveraging the DFA, we decompose $\phi$
into reach-avoid sub-tasks; 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 ${\mathbf{f}}_{\xi}\models\phi$, for all
${\mathbf{x}}_{0}\in{\mathcal{X}}_{0}$; see Section III-D. Trade-offs between
completeness and computational efficiency are discussed in Section III-E.

###  III-A From LTL formulas to DFA

First, we translate $\phi$, constructed using $\mathcal{AP}$, into a DFA
defined as follows [17]; see also Fig. 1(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) DFA

(b) Reachable sets

Figure 1: Fig 1(a) shows the DFA corresponding to
$\phi=\Diamond(\pi^{\ell_{2}})\wedge(\neg\pi^{\ell_{2}}{\mathcal{U}}\pi^{\ell_{1}})$.
Fig. 1(b) illustrates the reachability analysis over the DFA state space (see
Section III-D).

To interpret a temporal logic formula over a sequence $\tau({\mathbf{x}}_{0})$
generated by (2), we use a labeling function $L:{\mathcal{X}}\rightarrow
2^{\mathcal{AP}}$ that maps system states to symbols $\sigma\in
2^{\mathcal{AP}}$. A finite sequence of states
$\tau({\mathbf{x}}_{0})={\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 element in $w$ yields a DFA transition so that
the final state $q_{D}^{F}$ is reached [17]. Note that a DFA can be
constructed using existing tools such as [24].

###  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$. In math, we have:

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

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}}))\\}$
(4)

In what follows, for simplicity, we assume that for all
$q_{D}\in{\mathcal{Q}}_{D}$ there exists a feasible self-loop around every DFA
state $q_{D}$; later, in Section III-C, we relax this assumption. 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.2 (Reach-Avoid Properties)

Consider the DFA in Fig. 1(a). We have that
${\mathcal{R}}_{q_{D}^{0}}=\\{q_{D}^{0},q_{D}^{1},q_{D}^{F}\\}$. Also, we have
that ${\mathcal{X}}_{q_{D}^{0}\rightarrow
q_{D}^{0}}={\mathcal{X}}\setminus(\ell_{1}\cup\ell_{2})$,
${\mathcal{X}}_{q_{D}^{0}\rightarrow
q_{D}^{1}}=({\mathcal{X}}\setminus\ell_{2})\cap\ell_{1}$,
${\mathcal{X}}_{q_{D}^{0}\rightarrow q_{D}^{F}}=\ell_{2}\cap\ell_{1}$.
Similarly, we have 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_{2}$, and
${\mathcal{X}}_{q_{D}^{1}\rightarrow q_{D}^{F}}=\ell_{2}$.

###  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 verify LTL properties. 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 previously discussed conditions (i)-(ii) can
be satisfied; the detailed construction of ${\mathcal{X}}_{q_{D}}^{0}$ will be
discussed in Section III-D. Notice ${\mathcal{X}}_{q_{D}\rightarrow
q_{D}^{\prime}}$ may contain more than one region of interest $\ell_{i}$. As
discussed in Section II, for each region of interest $\ell_{i}$ in
${\mathcal{X}}_{q_{D}\rightarrow q_{D}^{\prime}}$, the system selects the
corresponding NN controller $\xi_{i}\in\Xi$. 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.3. In math, 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)$ then the
following two conditions hold for all possible initial system states in
${\mathcal{X}}_{q_{D}}^{0}$: (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 (4), we have that within
the time interval $[0,H_{q_{D}}-1]$, the transition from $q_{D}$ to $q_{D}$
(self-loop) is enabled, 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 NN
controller $\xi$.

To reason about safety of a DFA transition, we leverage existing reachability
analysis tools that can compute forward reachable sets
$\mathfrak{R}_{t}({\mathcal{X}}_{q_{D}}^{0},\xi)$ collecting all possible
states ${\mathbf{x}}$ that the system may reach after applying a feedback NN
controller $\xi$ for $t$ time steps while starting anywhere 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: (i)
$\mathfrak{R}_{t}({\mathcal{X}}_{q_{D}}^{0},\xi)\subseteq{\mathcal{X}}_{q_{D}\rightarrow
q_{D}},\forall{t}\in[0,\dots,H_{q_{D}}-1]$ and (ii)
$\mathfrak{R}_{H_{q_{D}}}({\mathcal{X}}_{q_{D}}^{0},\xi)\subseteq{\mathcal{X}}_{q_{D}\rightarrow
q_{D}^{\prime}}.$ 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$[6].

Construction of exact reachable sets is computationally intractable. Thus,
instead, we compute over-approximated reachable sets, denoted hereafter by
$\bar{\mathfrak{R}}_{t}({\mathcal{X}}_{q_{D}}^{0},\xi)\subseteq\mathfrak{R}_{t}({\mathcal{X}}_{q_{D}}^{0},\xi)$,
using tools that can handle systems of the form (1) with NN controllers [8].
If the following two conditions are satisfied

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

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{\mathfrak{R}}_{t}$, for some $t\in\\{0,\dots,\bar{H}\\}$ that satisfies
(6), then we say that the system fails to reach this region of interest. This
is in accordance with related works; see e.g., [8, 6]. 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 (6) holds for $H_{q_{D}}=1$.

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

Consider the DFA in Fig. 1(a) and, specifically, the transition from
$q_{D}^{0}$ to $q_{D}^{1}$. To reach $q_{D}^{1}$ from $q_{D}^{0}$, the
available controllers are $\Xi_{q_{D}^{0}\rightarrow q_{D}^{1}}=\\{\xi_{1}\\}$
by construction of the set ${\mathcal{X}}_{q_{D}^{0}\rightarrow q_{D}^{1}}$;
see Ex. III.2 and Section II. Let
${\mathcal{X}}_{q_{D}^{0}}^{0}={\mathcal{X}}_{0}$. Then, we compute reachable
sets $\bar{\mathfrak{R}}_{t}({\mathcal{X}}_{0},\xi_{1})$; see Fig. 1(b).
Observe that $H_{q_{D}^{0}}=3$, since the sets
$\bar{\mathfrak{R}}_{t}({\mathcal{X}}_{0},\xi_{1})$ for $t=0,1,2$ satisfy (5)
and $\bar{\mathfrak{R}}_{3}({\mathcal{X}}_{0},\xi_{1})$ satisfies (6). 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_{2}\\}$. Verification of this
transition will be discussed in Ex. III.4. Finally, we have
$\Xi_{q_{D}^{0}\rightarrow q_{D}^{0}}=\emptyset$ and
$\Xi_{q_{D}^{1}\rightarrow q_{D}^{1}}=\\{\xi_{1}\\}$.

###  III-D From Verification of Reach-Avoid Properties to Verification of LTL
formulas

To verify that the system satisfies $\phi$, 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; see also Section III-A. To
check this we rely on applying graph-search methods over the DFA state while
verifying on-the-fly safety of DFA transitions using reachability analysis;
see Section III-C. Specifically, 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. As discussed in Section III-C, to verify safety of 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). 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}$.

Algorithm 1 Reach_DFS Algorithm

1:Input: $D^{\prime}$; NN controllers $\Xi$; System dynamics (1)

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 (5)-(6)
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}$;

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.
1. The inputs to this algorithm are the graph $D^{\prime}$, the set $\Xi$ of
NN controllers and the system dynamics (1) (line 1). In what follows, we
denote by $q_{D}^{\text{cur}}$ the currently visited node in $D^{\prime}$. 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 $q_{D}^{\text{cur}}$
as $q_{D}^{\text{cur}}=q_{D}^{0}$ and
${\mathcal{X}}_{q_{D}^{\text{cur}}}^{0}={\mathcal{X}}_{0}$. Also, 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
need only as way store and recover from memory the sets
${\mathcal{X}}_{q_{D}}^{0}$ (lines 2-3). 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);
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). The
corresponding horizon $H_{q_{D}^{\text{cur}}}$ should be stored as well; we
abstain from this for simplicity of presentation. The final reachable set
$\bar{\mathfrak{R}}_{H_{q_{D}^{\text{cur}}}}(q_{D}^{\text{cur}},\xi)$ becomes
the set ${\mathcal{X}}_{q_{D}^{\text{next}}}^{0}$; see Ex. III.4 and Fig. 1(b)
as well (line 8). 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). 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 (3)). Then we keep taking out 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 not
visited yet (lines 12-16). 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). If ${\mathbf{q}}$
is empty yet 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 III-E) (lines 17-18). We note that any other
graph-search method in conjunction with reachability analysis can be used as
well.

######  Example III.4 (LTL Verification (cont))

We continue Ex. III.3; see also Fig. 1(b). 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{\mathfrak{R}}_{3}({\mathcal{X}}_{0},\xi_{1})$.
By computing $\bar{\mathfrak{R}}_{t}({\mathcal{X}}_{q_{D}^{1}}^{0},\xi_{2})$,
we verify that this DFA transition is safe. Thus, there exists
$\boldsymbol{\xi}=\xi_{1},\xi_{2}$ where $\xi_{1}$ and $\xi_{2}$ are applied
for $3$ and $2$ time steps so that ${\mathbf{f}}_{\xi}\models\phi$, for all
${\mathbf{x}}_{0}\in{\mathcal{X}}_{0}$.

###  III-E Correctness & Completeness

######  Proposition III.5 (Correctness)

The proposed method is correct, i.e., the computed $\boldsymbol{\xi}$ solves
Problem 1.

###### Proof:

This result holds by construction of the proposed method. Particularly, we
ensure that the closed-loop system (2) driven by
$\boldsymbol{\xi}=\mu(0),\dots,\mu(K)$, where each $\mu(k)$ is applied for
$H_{k}$ time-steps, generates trajectories
$\tau({\mathbf{x}}_{0})={\mathbf{x}}_{0},\dots,{\mathbf{x}}_{F}$, where
$F=\sum_{t=0}^{H_{k}}$, that satisfy the system dynamics and the LTL formula
$\phi$, $\forall{\mathbf{x}}_{0}\in{\mathcal{X}}_{0}$. ∎

######  Remark III.6 (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$, for all
${\mathbf{x}}_{0}\in{\mathcal{X}}_{0}$, even though such a strategy exists.
This is due to the fact that (a) Alg. 1 computes over-approximated 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. As for (b), for instance, given a initial set of states for
$q_{D}^{\text{cur}}$, Alg. 1 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. Additionally, as soon as
Alg. 1 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. The proposed method can be extended to account for
these additional control actions at the expense of increasing its
computational cost. We note that such trade-offs are quite common in related
works; see e.g., [25]. The proposed method 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.3); (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.

##  IV Experiments

In this section, we demonstrate our framework on an unmanned aerial vehicle
(UAV) with various LTL properties.

System Dynamics: We consider a UAV with dynamics as in (1) where the matrices
${\mathbf{A}}_{t},{\mathbf{B}}_{t},$ and ${\mathbf{c}}_{t}$ are defined as in
[8]. The UAV state is defined as
${\mathbf{x}}=[p_{x};p_{y};p_{z};v_{x};v_{y};v_{z}]\in\mathbb{R}^{6}$
capturing the position and velocity. The control input
${\mathbf{u}}\in\mathbb{R}^{3}$ is a function of pitch, roll and thrust.

NN controllers: In what follows, we define LTL specifications that require the
UAV to visit certain disjoint regions of interest $\ell_{i}\in\mathbb{R}^{3}$.
We highlight that the the regions $\ell_{i}$ are defined only over the UAV
position, i.e., $\ell_{i}\subseteq\Omega$. Also, since we assume disjoint
regions, the DFA can be pruned by removing infeasible DFA transitions reducing
the computational cost for verification [20]. We train the NN controllers
similarly to [8]; nevertheless, any other method (e.g., RL) can be used to
train them. Specifically, to train $\xi_{i}$, we leverage nonlinear Model
Predictive Control (MPC) methods. First we generate a random set of states
${\mathbf{x}}\in\mathbb{R}^{6}$. Starting from each one of these states, we
generate a sequence of pairs of states and control inputs that drive the UAV
towards the interior of $\ell_{i}$ using an off-the-shelf MPC solver [26].
Each pair constitutes a data point in a training dataset. Using this dataset
we train feedforward NN controllers $\xi_{i}$ with $2$ hidden layers, $30$
neurons/layer, and ReLU activation functions.

(a) Case Study 1

(b) Case Study 2

Figure 2: DFA for the LTL formulas in case studies I & II.

Case Study I: In this case study, we consider the following LTL formula
$\phi=(\Diamond\pi^{\ell_{1}})\wedge(\Diamond\pi^{\ell_{2}})\wedge(\neg(\pi^{\ell_{3}}\vee\pi^{\ell_{4}}){\mathcal{U}}\pi^{\ell_{1}})\wedge(\neg(\pi^{\ell_{3}}\vee\pi^{\ell_{4}}){\mathcal{U}}\pi^{\ell_{2}})$
requiring the UAV to eventually visit the regions $\ell_{1}$ and $\ell_{2}$,
in any order, while avoiding the obstacles $\ell_{3}$ and $\ell_{4}$. This
formula corresponds to the DFA shown in Fig. 2(a); notice that the transition
from $q_{D}^{0}$ to $q_{D}^{F}$ was pruned and, therefore, not considered
during verification since it requires the UAV to be present in more than one
region simultaneously. To train $\xi_{1}$ and $\xi_{2}$ we collected $16000$
datapoints for each controller. Given these trained NN controllers and an
initial set ${\mathcal{X}}_{0}$ of states defined as an ellipsoid centered at
$[3.5;3.5;2.9]$ with shape matrix of $\text{diag}[0.5^{2};0.5^{2};0.5^{2}]$.
We check if there exists a sequence of control actions that satisfy $\phi$.
Particularly, first it investigates the DFA transition from $q_{D}^{0}$ to
$q_{D}^{1}$. This transition requires the UAV to stay within the obstacle-free
space (i.e., avoid the obstacles $\ell_{3}$ and $\ell_{4}$) and eventually
reach $\ell_{2}$. The corresponding reachable sets for this DFA transition are
shown in Figure 3(a). Notice that the reachable sets
$\bar{\mathfrak{R}}_{t}({\mathcal{X}}_{0},\xi_{2})$ are fully outside the
obstacle regions for $t=1,2$ while at $t=3$ the corresponding reachable set is
fully inside $\ell_{2}$. Thus, this DFA transition is verified to be safe.
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.
The set of initial states for this transition is
${\mathcal{X}}_{q_{D}^{1}}^{0}=\bar{\mathfrak{R}}_{3}({\mathcal{X}}_{0},\xi_{2})$.
After computing reachable sets
$\bar{\mathfrak{R}}_{t}({\mathcal{X}}_{q_{D}^{1}}^{0},\xi_{1})$ (not shown),
we can see that for $t=1,2$ they are outside the obstacles while
$\bar{\mathfrak{R}}_{3}({\mathcal{X}}_{q_{D}^{1}}^{0},\xi_{1})$ is inside
$\ell_{1}$ verifying that this DFA transition is also safe. Thus, there exists
a control strategy $\boldsymbol{\xi}=\xi_{2},\xi_{1}$ where $H_{1}=H_{2}=3$
such that ${\mathbf{f}}_{\xi}\models\phi$ for all
${\mathbf{x}}_{0}\in{\mathcal{X}}_{0}$.

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

(b) Case II: $q_{D}^{0}\rightarrow q_{D}^{F}$

Figure 3: Verification of a DFA transition for the case studies I and II. The
regions of interest that need to be avoided/reached to enable this DFA
transition are shown with black/blue colour. All other regions are not shown.
All reachable sets that are outside/inside the regions to reach are shown with
orange/green color.

Case Study II: In this case study, we consider an LTL formula
$\phi=\Diamond(\pi^{\ell_{1}}\vee\pi^{\ell_{2}})\wedge(\neg(\pi^{\ell_{3}}\vee\pi^{\ell_{4}}){\mathcal{U}}(\pi^{\ell_{1}}\vee\pi^{\ell_{2}}))$
requiring the UAV to eventually visit either region $\ell_{1}$ or $\ell_{2}$,
while avoiding obstacles $\ell_{3}$ and $\ell_{4}$. This formula corresponds
to the DFA shown in Figure 2(b). The NN controller $\xi_{2}$ is the same as in
the previous case study while $\xi_{1}$ was trained using only $100$
datapoints to mimic a poorly designed controller. The initial set of states
${\mathcal{X}}_{0}$ is defined as an ellipsoid centered at $[0.4;0.4;0.3]$
with shape matrix of $\text{diag}[0.5^{2};0.5^{2};0.5^{2}]$. Given the DFA, we
investigate the transition from $q_{D}^{0}$ to $q_{D}^{F}$ which requires the
UAV to reach either $\ell_{1}$ or $\ell_{2}$ while avoiding both $\ell_{3}$
and $\ell_{4}$. In other words, we have that
${\mathcal{X}}_{q_{D}^{0}\rightarrow
q_{D}^{0}}=\\{\Omega\setminus(\ell_{3}\cup\ell_{4})\\}$ and
${\mathcal{X}}_{q_{D}^{0}\rightarrow q_{D}^{F}}=\\{\ell_{1}\cup\ell_{2}\\}$.
Thus, we have that $\Xi_{q_{D}^{0}\rightarrow
q_{D}^{F}}=\\{\xi_{1},\xi_{2}\\}$. First, we check if this DFA transition is
safe using $\xi_{1}$. The generated reachable sets are shown in Figure 3(b);
only the first $4$ reachable sets are shown. We observed that $\ell_{1}$ could
not be reached within a large enough number of iterations. Thus, we cannot
reason about safety of this DFA transition under $\xi_{1}$. Thus, next we
consider the controller $\xi_{2}$ and we constructed the sets
$\bar{\mathfrak{R}}_{t}({\mathcal{X}}_{0},\xi_{2})$ (not shown) demonstrating
that all obstacles are avoided while at $t=6$ the the reachable set is fully
inside $\ell_{2}$. Thus, we verify that there exists
$\boldsymbol{\xi}=\xi_{2}$, where $\xi_{2}$ is applied for $6$ steps, so that
${\mathbf{f}}_{\xi}\models\phi$, for all
${\mathbf{x}}_{0}\in{\mathcal{X}}_{0}$.

Figure 4: Case Study III: Verification of the DFA transition from $q_{D}^{0}$
to $q_{D}^{1}$. The red ellipsoid corresponds to a reachable set being fully
inside the region to avoid.

Case Study III: We revisit the LTL formula considered in Ex. III.2-III.4 with
DFA shown in Fig. 1(a). The controllers $\xi_{1}$ and $\xi_{2}$ are the same
as in case study I while ${\mathcal{X}}_{0}$ is defined as an ellipsoid
centered at $[3.4;3.4;3.1]$ with shape matrix of
$\text{diag}[0.5^{2};0.5^{2};0.5^{2}]$. To check whether the DFA transition
from $q_{D}^{0}$ to $q_{D}^{1}$ is safe, we check if the system can reach
$\ell_{1}$ while avoiding $\ell_{2}$. By constructing the reachable sets, we
notice that $\ell_{1}$ cannot be reached without entering $\ell_{2}$ first;
see Fig. 4. Thus, we cannot find a $\boldsymbol{\xi}$ for $\phi$; see Rem.
III.6.

##  V Conclusion

This paper proposed a new method to design verified compositions of NN
controllers for co-safe LTL tasks. We showed its efficiency in navigation
tasks for aerial vehicles.

## References

  * [1] 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.
  * [2] 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.
  * [3] S. Huang, N. Papernot, I. Goodfellow, Y. Duan, and P. Abbeel, “Adversarial attacks on neural network policies,” _arXiv preprint arXiv:1702.02284_ , 2017\.
  * [4] M. Fazlyab, M. Morari, and G. J. Pappas, “Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming,” _IEEE Trans on Automatic Control_ , 2020.
  * [5] S. Dutta, S. Jha, S. Sankaranarayanan, and A. Tiwari, “Output range analysis for deep feedforward neural networks,” in _NASA Formal Methods Symposium_. Springer, 2018, pp. 121–138.
  * [6] 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.
  * [7] 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.
  * [8] 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.
  * [9] 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.
  * [10] 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.
  * [11] 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.
  * [12] S. Sun, Y. Zhang, X. Luo, P. Vlantis, M. Pajic, and M. M. Zavlanos, “Formal verification of stochastic systems with relu neural network controllers,” in _2022 International Conference on Robotics and Automation (ICRA)_. IEEE, 2022, pp. 6800–6806.
  * [13] K. Jothimurugan, S. Bansal, O. Bastani, and R. Alur, “Compositional reinforcement learning from logical specifications,” _Advances in Neural Information Processing Systems_ , vol. 34, 2021.
  * [14] G. N. Tasse, D. Jarvis, S. James, and B. Rosman, “Skill machines: Temporal logic composition in reinforcement learning,” _arXiv preprint arXiv:2205.12532_ , 2022.
  * [15] 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.
  * [16] 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
  * [17] C. Baier and J.-P. Katoen, _Principles of model checking_. MIT press Cambridge, 2008, vol. 26202649.
  * [18] S. W. Chen, T. Wang, N. Atanasov, V. Kumar, and M. Morari, “Large scale model predictive control with neural networks and primal active sets,” _Automatica_ , vol. 135, p. 109947, 2022.
  * [19] K. Leahy, D. Zhou, C.-I. Vasile, K. Oikonomopoulos, M. Schwager, and C. Belta, “Persistent surveillance for unmanned aerial vehicles subject to charging and temporal logic constraints,” _Autonomous Robots_ , vol. 40, no. 8, pp. 1363–1378, 2016.
  * [20] Y. Kantaros and M. M. Zavlanos, “Stylus*: A temporal logic optimal control synthesis algorithm for large-scale multi-robot systems,” _International Journal of Robotics Research_ , 2020.
  * [21] E. M. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, and D. Wojtczak, “Omega-regular objectives in model-free reinforcement learning,” _TACAS_ , 2018.
  * [22] Y. Kantaros, “Accelerated reinforcement learning for temporal logic control objectives,” in _IEEE/RSJ International Conference on Intelligent Robots and Systems_ , Kyoto, Japan, October 2022.
  * [23] 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.
  * [24] F. Fuggitti, “Ltlf2dfa,” March 2019. [Online]. Available: https://github.com/whitemech/LTLf2DFA
  * [25] K. Leahy, A. Jones, and C. I. Vasile, “Fast decomposition of temporal logic specifications for heterogeneous teams,” _IEEE Robotics and Automation Letters_ , 2022.
  * [26] N. Andrei, “A sqp algorithm for large-scale constrained optimization: Snopt,” in _Continuous nonlinear optimization for engineering applications in GAMS technology_. Springer, 2017, pp. 317–330.