IEEE Robotics & Automation Magazine - June 2020 - 112

was decided offline using Flow* RA [2]. On average, it took
roughly 5 min for Flow* to make a safety decision for one
start-goal position pair under bounded disturbance conditions d x, d y ! [- 0.4, 0.4] m/s, reinforcing the fact that RA is
expensive to perform at runtime.
Using this set of initial-final position pairs, an NN was
trained to predict the safety of an untrained pair of initial-
final goals. The NN was composed of four input nodes (the
x-y initial position and x-y goal position pair), one hidden
layer of 40 nodes, and one output, which determined
whether the label was safe or unsafe. The NN performed
with 0% FPs and roughly 0.2% FNs. In Figure 9, we present
examples of labels and NN decisions for trajectories starting from three different initial positions to all of the final
goals in the training set. Similar to the previous case, a
green (red) dot represents a final position in which the trajectory was labeled safe (unsafe) from a given starting
point, and a green (red) circle represents the NN decision
for the same point.

y (m)

y (m)

0.5
0

Safe Labels
Unsafe Labels
1NN Safe Labels
NN Unsafe Labels
0.5Initial Position
0Obstacles

1
0.5
y (m)

1

NN Verification
Similar to the previous case study, since the results of an NN
could be erroneous, we use Verisig to verify the safety predictions obtained by the trained NN. As a proof of concept, to
demonstrate the procedures explained in the "Verification"
and "NN Retraining" sections, the results of the NN from a
single initial position to all goal positions in the primitive environment are verified. However, the same NN verification and
retraining procedure can be performed for all possible initial
and final regions. The training data for this case are presented
in Figure 9(a), while Figure 10(a) displays the results of the
verification. The gray shaded regions in Figure 10(a) represent
areas where the NN outputs unsafe and where Verisig concurs
without performing the whole verification, since the NN output is already unsafe and thus, in the worst-case scenario, conservative. Green regions represent areas where the NN outputs
safe and where Verisig verifies that the plant is safe, too. In the
yellow regions, the NN outputs safe, but Verisig cannot decide
whether the plant is safe or not.

0

-0.5

-0.5

-0.5

-1

-1

-1

0

1
x (m)

2

0

1
x (m)

(a)

2

0

1
x (m)

(b)

2

(c)

Figure 9. The safe and unsafe trained final goals and NN decisions from various initial positions. (a) Initial position [0.0, −0.2] m.
(b) Initial position [0.2, −1.0] m. (c) Initial position [0.4, 0.4] m.

Verified (NN Output: Safe; Plant: Safe)
Verified (NN Output: Unsafe)
Safe Training Points
Unsafe Training Points
Unsafe Points Added
After Verification
y (m)

y (m)

Verified (NN Output: Safe; Plant: Safe)
Verified (NN Output: Unsafe)
Unknown (NN Output: Safe; Plant: ?)
Not Verified (NN Output: Safe; Plant: Unsafe)
Safe Training Points
Unsafe Training Points
0

-0.5

-1

0

-0.5

0

0.5

1

1.5

2

2.5

-1

0

0.5

1

1.5

x (m)

x (m)

(a)

(b)

2

Figure 10. The NN verification results. (a) The verification of the NN trained with the original data set. (b) The verification of the
retrained NN with the conservative data set.

112

*

IEEE ROBOTICS & AUTOMATION MAGAZINE

*

JUNE 2020

2.5
IEEE Robotics & Automation Magazine - June 2020

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