Safe Networked Robotics with Probabilistic Verification

TL;DR

This paper presents a probabilistic verification method to ensure safety in networked autonomous robots by constructing run-time shields that account for stochastic communication delays, validated on a real autonomous vehicle.

Contribution

It introduces a formal verification-based shielding approach that guarantees safety properties for networked robots under stochastic latency conditions.

Findings

The shield ensures safety with high probability despite network delays.

Validated approach on a real autonomous vehicle navigating indoor environments.

Effective handling of WiFi-induced communication delays in safety-critical tasks.

Abstract

Autonomous robots must utilize rich sensory data to make safe control decisions. To process this data, compute-constrained robots often require assistance from remote computation, or the cloud, that runs compute-intensive deep neural network perception or control models. However, this assistance comes at the cost of a time delay due to network latency, resulting in past observations being used in the cloud to compute the control commands for the present robot state. Such communication delays could potentially lead to the violation of essential safety properties, such as collision avoidance. This paper develops methods to ensure the safety of robots operated over communication networks with stochastic latency. To do so, we use tools from formal verification to construct a shield, i.e., a run-time monitor, that provides a list of safe actions for any delayed sensory observation, given the expected and maximum network latency. Our shield is minimally intrusive and enables networked robots to satisfy key safety constraints, expressed as temporal logic specifications, with desired probability. We demonstrate our approach on a real F1/10th autonomous vehicle that navigates in indoor environments and transmits rich LiDAR sensory data over congested WiFi links.