IEEE Robotics & Automation Magazine - June 2020 - 115

provide fully accurate models and often rely on specific
operating conditions.
One way to provide verification for systems with model
uncertainties is to consider a conservative abstracted model
and verify that the real system is equivalent to or safer than
this abstraction. Building on the intuition in [21], if the system performance and behavior are verified to be closer to the
desired behavior than the abstraction, verifying the abstraction also verifies the real system. Note that, since these conservative abstractions capture the worst-case behavior of the
system, failing to verify the abstraction may lead to the belief
that the actual system is not safe, which may not necessarily
be true but safe.
Training and verification operations require heavy computation time; although this is a minor problem since these
operations occur offline, it is still a concern, especially
when dealing with high-order dynamical models and large
unknowns in the system. Several services, such as Amazon
Web Services (used in this article), Microsoft Azure
(https://azure.microsoft.com), and Google Cloud Platform
(https://cloud.google.com), are available and projected to
become faster and more accessible in the future.
Lastly, we note that, similar to the approach presented in
the second case study in this article, although verification is
done for a static model, the approach that we presented could
be generalized to other settings where verifying a subset of the
state space can be sufficient for use compositionally to check
safety properties about larger spaces.

y (m)

Initial Position
Final Position
Actual Path
Desired Path
Candidate Goal Positions
Intermediate Goal Positions
Obstacles

2
1

0
-1
-2
-4

Acknowledgment
This material is based upon work supported by the Air Force
Research Laboratory (AFRL) and the Defense Advanced
Research Projects Agency (DARPA) under the Assured
Autonomy program, Contract FA8750-18-C-0090. Any opinions, findings, and conclusions or recommendations
expressed in this material are those of the authors and do not

y (m)

Future Work
The framework proposed in this article enables fast and
assured predictive and proactive monitoring of autonomous
systems operations in cluttered and uncertain environments
at runtime. NNs are leveraged to make decisions about the
safety of planned trajectories at runtime and perform replanning accordingly. RA is used during the training phase and
for verification purposes, bypassing its usage at runtime. In
this way, most of the computation burden is limited to offline
operations, leaving the fast decision-making and replanning
tasks for the online application.
The applicability of the proposed framework was demonstrated in two case studies, and the designed NNs were verified using our recent Verisig tool to produce decisions that
never lead to unsafe states. Safety was the main concern in
this article. Possible future directions include adding energy
constraints while designing safe operations, developing robust
NNs to deal with changes in environments, and, as discussed
in the previous section, diving deeper into the problem of verifying real systems.

Safe

Safe
Wind
0
x (m)

Wind

Wind
2

Wind

Safe

Unsafe

-1

Safe
-2

Initial Position
Final Position
Actual Path
Desired Path
Intermediate Goal Positions
Obstacles

Safe

Wind

-2
-4

-2

0
x (m)

Wind

(a)

Wind
2

Wind

(b)

Figure 13. (a) The experimental results of the navigation of the quadrotor using the trained NN to make safety decisions and replan.
(b) The unsafe navigation in which NN decisions were disregarded. The lower row shows the experiments relative to the upper row.

JUNE 2020

IEEE ROBOTICS & AUTOMATION MAGAZINE

115

https://azure.microsoft.com https://cloud.google.com

IEEE Robotics & Automation Magazine - June 2020

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