IEEE Robotics & Automation Magazine - June 2020 - 105

*

s x = 1 if R ( p x, t) + p o, j = Q
6t ! [0, T ], 6j ! " 1, f, N o , ,
s x = 0 otherwise

(1)

where p x is the desired positions along the trajectory x,
R ( p x, t) is the corresponding reachable set, s x is the safety
label, p o, j is the jth obstacle position, and N o is the number of
obstacles in the environment. An NN is trained using these
safety-labeled parameters to make decisions for trajectories
with different conditions.
NN Training for Safety Decisions
Following the diagram in Figure 1, after collecting a rich library
of labeled trajectory parameters, we train an NN to provide
safety decisions without having to run computationally expensive RA operations at runtime. The inputs to the NN are the
trajectory parameters, which are the initial and final positions
of the system, and the obstacle-avoidance distance. The output
of the NN is a binary safe/unsafe decision. Since these conclusions are used by a safety-critical system, it is required that the
NN never outputs a decision of safe if the trajectory is unsafe, as
it can lead to dangerous outcomes (e.g., colliding with an obstacle). Therefore, we are interested in training an NN with zero
false positives (FPs). The drawback of reducing the number of
FPs is that the number of false negatives (FNs) (safe trajectories
marked unsafe) may increase. Even a conservatively trained
NN can output a safe decision for a set of untrained, unsafe trajectory parameters. Therefore, the absence of such FPs needs to
be verified prior to its deployment.
Verification
In this article, we use Verisig to verify that the trained NN
does not output safe if the robot plans an unsafe trajectory.
As described in our prior work [4], Verisig was developed to
verify safety properties of closed-loop systems with NN components. Verisig focuses specifically on sigmoid-based NNs

and works by transforming the NN into an equivalent hybrid
system. The NN's hybrid system is then composed with the
plant, resulting in a new hybrid system that describes the
entire closed-loop system, as depicted in Figure 1. This
enables us to cast the verification problem as a hybrid system
reachability problem, which is solved by an optimized hybrid
system verification tool, such as Flow* [2]. Specifically, Verisig transforms the NN S into a hybrid system H S by noting
that the sigmoid derivative can be expressed in terms of the
sigmoid itself, i.e.,
vl(x) = v(x) (1 - v(x)),

where v(x) = 1/ (1 + exp (- x)) is the sigmoid. With this
observation in mind, we introduce a proxy function
v p (t, x) = v (xt) such that v p (1, x) = v (x) and
.

v p (x) = xv p (t,

x) (1 - v p (t, x))

using the chain rule. In other words, vp can be considered as
a state in a dynamical system that starts at v p (0, x) = 0.5 and
is equal to v(x) at time 1. Thus, each neuron in the NN can
be mapped to a state in a hybrid system, and each layer can be
mapped to a mode. Transitions between modes occur when
t = 1. Note that this time is local to the NN; global time does
not progress during the NN's execution.
Although Verisig was originally applied to closed-loop systems with NN controllers, it applies to the setup considered in
this article, as well. In particular, in the verification problem,
the NN's hybrid system does not interact with the plant
directly; rather, for a given set of initial conditions, we compute the reachable set for the NN's output and check whether
it is possible for the robot to crash (when started from that
initial set) while the NN outputs safe.
The composed hybrid system H = H q < H S is shown in
Figure 2, where H q is the hybrid system describing the robot's

t % ts = 0
Input

Controller
u : = g (x,
x xτ)

NN HS

S(x
x0) = Safe

Planner
.
x=0

Trajectory
xτ

Plant
.
x = f (x,
x u, d )
Safe

Obstacle
Collision

Plant
.
x=0
Unsafe

t == T
S(x
x0) = Unsafe

Runtime
Monitoring
Safe

Figure 2. The composed hybrid system
. considered for verifying NNs for runtime monitoring. The plant dynamics evolve as a function
of the state, input, and disturbance x = f(x, u, d ). A controller is designed to follow the desired trajectory xx by generating a control
input with sampling time ts, u = g(x, xx). The goal is to verify that the plant (Unsafe) mode is never reached during the duration T of
the mission, i.e., that the NN never outputs safe when the plant is unsafe.

JUNE 2020

*

IEEE ROBOTICS & AUTOMATION MAGAZINE

*

105
IEEE Robotics & Automation Magazine - June 2020

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