IEEE Robotics & Automation Magazine - June 2020 - 104

Avoidance
Distance

Obstacles

Goal Position

IEEE ROBOTICS & AUTOMATION MAGAZINE

JUNE 2020

Figure 1. The architecture of the proposed framework for verifying NNs for runtime monitoring and planning autonomous operations. (a) During the offline stage, an NN is trained and
verified, followed by its deployment at runtime for monitoring and replanning purposes. (b) The online stage.

(a)

Labeled
Inputs

Safe

Unsafe
Safe
Unsafe

NN Training

Verisig

Avoidance
Distance
Verified?

Goal Position

(b)

Updated Inputs

Replanning
Unsafe

Execution
Safe
Trained NN
Initial Position
Yes
Hybrid System
Reachability
Conversion Into Hybrid System
Plant
Initial Position
104

executes the course. If the decision is unsafe, the trajectory is replanned by changing the parameters until a safe
choice is obtained.
Reachability Analysis
As mentioned previously, RA is a very powerful method for
computing the sets that a system could reach starting
from an initial set. A hybrid system RA tool, Flow* [2],
uses Taylor models to compute flowpipe overapproximations of the dynamics, while dReach [3] encodes the
reachability problem as first-order formulas across real
numbers and solves the problem using d- decision procedures. Hamilton-Jacobi RA is also a widely used approach
to provide guarantees for the safety of safety-critical systems' optimal system trajectories [5]. It performs well in
terms of the generality of system dynamics, flexibility in
the representation of sets, and control policy computation; however, it suffers from computational scalability
[6]. A significant effort has been made to overcome the
scalability problem for high-dimensional systems, such as
decomposing the system dynamics [7] and using NNs to
approximate the reachable sets [6], [8]. Other types of
reachable sets, such as robust control invariant tubes [9],
have also been proposed for safety-guaranteed UAV planning. All these traditional RA tools are very effective in
providing safety assurances, although their computational
complexity makes them difficult to use in making runtime
safety decisions.
In the literature, there have been some efforts to make
RA more usable for runtime applications. For example, in
[10], the authors precomputed a library of trajectories and
funnels (analogous to reachable sets) offline and combined
these trajectories online to navigate in a priori unknown
environments under disturbance effects. However, with
this approach, the system is restricted to a discrete set of
motion primitives. In [11], using Hamilton-Jacobi reachability, a lookup table is computed offline to find the
bounds on the planned trajectory that are used to augment
the obstacles to guarantee collision-free behavior under
bounded disturbances in unknown environments. Similarly, in [12], forward reachable sets are computed offline for
parameterized trajectories, and at runtime, safe trajectory
parameters are picked to avoid the sensed obstacles in
unknown environments with model uncertainties. Different from these works, our framework solves this problem
of safe navigation in known and unknown environments
under the presence of external disturbances by using verified NNs to perform safety decisions at runtime, leaving
the RA computation offline. Our framework is also general
and modular, meaning that any type of control and planning method can be considered. It is also independent
from the choice of reachability analysis tool. Specifically,
during the offline stage, reachable sets are generated for a
given trajectory, and if they do not intersect with obstacles, the corresponding trajectory parameters are labeled
as safe:

IEEE Robotics & Automation Magazine - June 2020

Table of Contents for the Digital Edition of IEEE Robotics & Automation Magazine - June 2020