IEEE Robotics & Automation Magazine - June 2020 - 103

recent tool Verisig, in which the NN is transformed into a
hybrid system to provide guarantees before deployment. In
the case of unverified NNs, the outputs of the verification
are used to retrain the network until verification is
achieved. Two illustrative case studies on a quadrotor
unmanned aerial vehicle (UAV) (a pickup/drop-off operation and navigation in a cluttered environment) are presented to validate the proposed framework in simulations
and experiments.
Safety Predictions
As autonomous vehicles find their way into our society, it
becomes critical to guarantee safety against unpredictable
uncertainties and disturbances during their operations at
runtime. In fact, while model-driven motion planning
and control techniques can be robust against noises and
disturbances, they cannot prevent deviations from the
desired behavior during system operation, potentially
leading to unsafe states (e.g., crashing into an obstacle in
the environment due to excessive wind disturbance). To
assure safety during autonomous operations, it is necessary to take the effect of noises and disturbances into
account during planning. Traditional RA tools, such as
Hamilton-Jacobi reachability [1], and hybrid system RA
techniques [2], [3] have proved to be very effective in providing safety guarantees by leveraging knowledge about
the model of the system. However, their computational
complexity makes them difficult to use at runtime, which
is the subject of this article.
On the other hand, contrary to traditional RA tools,
recent developments in machine learning have considerable
potential to enable fast RA thanks to their efficiency and
accuracy. Unfortunately, since the performance of such
learning enabled components (LECs) depends significantly
on the properties of the training data, it is challenging to
provide guarantees in safety-critical operations. To deal
with these challenges, this article presents a framework to
verify LECs for fast, safe monitoring and planning of
autonomous operations.
An NN trained to predict whether an operation will be
safe or unsafe is verified if its output decision (safe or unsafe)
always concurs with the results obtained by running the operation under the worst case conditions in which it was trained.
Since it is unlikely that an NN with this strong property
exists, in this article, we define one that is conservatively verified; in short, it is verified if, at the least, its safe decision output always concurs with the result obtained by running the
actual operation. In other words, if the NN output is safe, the
system can never reach an unsafe state; however, the NN is
allowed to output unsafe when the system will be safe, since
this is a conservative decision. This definition also holds in
the extreme case that an NN outputs only unsafe decisions,
in which a vehicle will be always safe, although it will not be
able to move anywhere.
In the proposed scheme, an NN is trained to recognize
safe and unsafe trajectories for an autonomous vehicle in an

obstacle-populated environment. Specifically, training is
performed, creating a library of trajectories and computing
their reachable sets to make safety decisions; hence, the
computational burden is limited to the offline stage. A trajectory is labeled safe if its reachable sets do not overlap
with any obstacle in the environment; otherwise, it is
marked unsafe.
Verification of the obtained NN is achieved using our
recent technique Verisig [4], in which the NN is transformed
into a hybrid system and the verification problem is cast as a
hybrid system reachability problem. If the NN is not verified,
meaning that it is not safe to be used, the output of the verification is employed as feedback to retrain the NN more conservatively until it is verified. Once the NN is verified, it is
used at runtime as a safety checker for the planned trajectories from an untrained initial state under the effect of
unknown online disturbances. If unsafe, a new trajectory is
planned and tested until a safety-guaranteed course is
obtained, if possible.
Contributions of the article include the following: with the
proposed framework, we 1) develop a fast safety checking and
replanning approach for autonomous vehicles' operations in
cluttered environments under unknown runtime disturbances and 2) leverage a novel NN verification tool, Verisig, to verify and retrain the used NN as a fast safety monitor, before
its deployment.
As a result, with this framework, it is possible to eliminate
the need for computationally expensive RA tools for planning safe trajectories at runtime, and our verification
method, Verisig, is capable of assessing the validity of the
proposed NN. To better illustrate our proposed framework,
two case studies on a quadrotor UAV are presented with simulations and experiments under the presence of unknown
disturbances during runtime: 1) a pickup/drop-off mission
and 2) safe navigation in a cluttered environment.
Verified Safe Motion Planning
Our verified safe motion planning framework consists of
offline and online stages, as depicted in Figure 1. During the
offline phase, a library of trajectories is generated. We
parametrize the trajectory generation based on the initial
state of the UAV, the desired goal position, the location of
the obstacles on the way to the goal site, and the distance
that must be maintained from these obstacles. These trajectory parameters are labeled safe or unsafe using RA, and an
NN is trained with this set of parameters. To be able to use
the NN in autonomous operations, it should be guaranteed
that the trained network never outputs safe when the trajectory is actually unsafe. To provide this guarantee, we verify
the trained NN using our recent tool Verisig, as outlined in
the "Verification" section. In case the NN is not verified, the
Verisig output is utilized to retrain the NN more conservatively (i.e., it outputs more unsafe decisions) until it is verified. Once the NN is verified, it is used to make decisions
about the safety of a new set of trajectory parameters at runtime. If the NN decides that the trajectory is safe, the UAV
JUNE 2020

IEEE ROBOTICS & AUTOMATION MAGAZINE

103

IEEE Robotics & Automation Magazine - June 2020

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