IEEE Robotics & Automation Magazine - June 2020 - 106

dynamics. H contains the union of modes and states of H q
and H S . H starts in the initial mode of H S and adds a transition from the last mode of H S to the initial mode of H q ,
at which point the H q execution begins. The goal is to
verify that H does not enter the plant (Unsafe) mode when
S (x 0) = Safe.
Given a hybrid system description of the closed-loop
system, one could use a tool such as Flow* to verify the
system's safety. Note that, since hybrid system verification is undecidable in general, the typical approach used
in these tools is to overapproximate the reachable sets. If
the overapproximation does not contain any unsafe
states, the system is safe. If the overapproximation contains safe and unsafe states, the outcome is unknown,
since the unsafe states could be spurious; i.e., they do
not exist in the true reachable set but only in the overapproximated one. Finally, if all states are unsafe, the system is unsafe. Various shapes have been explored to
overapproximate the reachable sets, including polytopes,
ellipsoids, and hyperrectangles. Flow* uses a Taylor
model approximation, which is a Taylor series approximation with worst case error bounds. Taylor models
scale well when used with interval analysis and are
shown to have a low approximation error for a large
class of nonlinear systems [2].
NN Retraining
At the end of the verification, Verisig specifies the
regions in which 1) the NN is safe to be used (i.e., the
plant is not unsafe when the NN output is safe), 2) the
NN is not safe to be used (i.e., the plant is unsafe when
the NN output is safe), and 3) the system is not able to
make a decision due to the approximation errors
introduced in the hybrid system RA during verification (i.e., the NN output is "unknown"). In case there
are regions in which the NN is not safe to be used or
Verisig cannot decide, the NN needs to be retrained.
The output of Verisig can be leveraged to retrain the
NN in several ways. One is to collect more data around
those regions where Verisig is not able to make a decision, followed by NN retraining. An increased density
of data around previously untrained regions may help
with the verification.
However, how much data needs to be collected in
those regions is not known a priori and is hard to predict,
so the process could require multiple iterations of data
collection and retraining. In addition, collecting new data
to improve the training set may not always be possible.
Instead, we propose adding points from the unsafe/
unknown regions obtained from the Verisig output to
the existing training set, marking them with unsafe labels,
and finally retraining the NN. By retraining the NN
with more unsafe points, a more conservative version is
obtained in which unsafe regions are inflated, helping
with the verification process. This retraining process is
repeated until the NN is verified.
106

IEEE ROBOTICS & AUTOMATION MAGAZINE

JUNE 2020

Case Studies
As a proof of concept, our verified safe monitoring and
planning approach is applied to two case studies of quadrotor motion planning: 1) a pickup/drop-off mission and 2) a
navigation operation in a cluttered environment. Both case
studies use similar NNs to predict whether the vehicle trajectory will be safe or unsafe (and thus require offline training and verification). At runtime, the verified NN is used
for different purposes. The pickup/drop-off task requires
the UAV to go from one side of a static environment to the
other, resembling operations that could happen inside a
warehouse or factory. The UAV makes decisions about the
safety of the planned trajectory based on the NN results
and replans by adjusting the obstacle-avoidance distance
until it finds a longer but safe course to its goal position. In
the latter case study, the UAV is tasked with navigating a
previously unknown cluttered area. Training is executed in
a smaller environment with only one obstacle, acting as a
primitive scenario that can appear and be composed multiple times at runtime. Training in a primitive environment
enables the NN and verification to be generalized to different settings with the same type of obstacles located in previously unknown positions. Replanning here is executed by
querying different waypoints along the path to the goal
until the NN outputs a safe decision. In both case studies,
we use the same vehicle, controller, planner, and disturbances, whose models are briefly summarized in the following section.
System Models
Quadrotor UAV and Controller Model
A quadrotor can be modeled using the following simplified
sixth-order state vector x = 6x y z v x v y v z@ R, where x, y,
and z are the world frame positions and vx, vy, and vz are the
world frame velocities. The quadrotor dynamics can be
.
defined as x = f (x, u, d ), where u = 6F z i@R is the input
vector with thrust, roll, and pitch commands and
d = 6d x d y d z@ R is the external disturbance vector. The
dynamics can be described as
6xo yo zo @ R = 6v x v y v z@ R

vo x R gi V
dx - vx
S
W
>vo yH = S - gz W + k d >d y - v yH,
vo z SS F - g WW
dz - vz
m
T
X

where m is the mass of the quadrotor, g is gravity, and k d is
the drag coefficient. It should be noted that, in this article, a
simplified quadrotor UAV model is used to alleviate the
verification problem. Validating a high-fidelity model [13]
is left for future work. To generate the necessary roll, pitch,
and thrust inputs to follow the desired trajectory, a cascaded set of PID controllers is used [14].

IEEE Robotics & Automation Magazine - June 2020

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