Safe Networked Robotics with Probabilistic Verification

TL;DR

Shankar et al. address safety for networked robotics under stochastic communication delays by modeling the remote-in-the-loop control as a Delayed Communication MDP (DC-MDP) and synthesizing an ε-shield that guarantees a target safety probability $\\delta$. The approach offline constructs a run-time shield $C_{\\epsilon}$ that restricts the cloud controller’s actions to a safe subset, ensuring the safety property $\\varphi=\\square \\neg S_{unsafe}$ with probability at least $\\delta$, even when delays $\\tau_t$ are random with upper bound $\\tau_{max}$. The DC-MDP integrates the delay dynamics $\\mathbb{P}_{\\tau}$ and an action buffer to capture the information available at the robot, enabling accurate safety analysis and shield synthesis. The method is validated in simulation and on an F1/10th vehicle over congested WiFi, showing improved safety guarantees and tunable safety-efficiency trade-offs via $\\delta$ and the known delay distribution.

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.

Figures (3)

• Figure 1: Safe Networked Control for Robotics: A resource-constrained robot transfers sensor observations (RGB-D images or LiDAR point clouds) through a wireless network with stochastic latency. At the receiving end, a control module or a human teleoperator processes the observation to generate the corresponding action. The action is filtered by the shield, which enforces a particular safety specification that the robot has to maintain. The filtered, "safe" action is then executed by the robot.
• Figure 2: Shielding leads to safe networked control in simulations. Top row - Car following simulation results; Bottom row - Gridworld simulation results. Figs. \ref{['fig:simulation_results_a']} and \ref{['fig:simulation_results_d']} show the set of safe initial states with maximum safety probability greater than $0.95$ for the Delayed CommunicationMDP for the constant delay case. The set of safe states expands as the maximum delay ($\mathrm{\tau_{max}}$) decreases. This is depicted by the legend that has multiple colors attributed to lower latencies. Figs. \ref{['fig:simulation_results_b']} and \ref{['fig:simulation_results_e']} compares the set of safe initial states with maximum safety probability greater than $0.95$ for the random and constant delay cases with $\mathrm{\tau_{max}}=3$ in both the cases. The set of safe states is larger in the case of random delay as the shield exploits the knowledge of the delay transitions to allow the agent to act more aggressively. The white color represents initial states that have maximum safety probability less than $0.95$. For the gridworld setup, the obstacle is located at (4,4). Figs. \ref{['fig:simulation_results_c']} and \ref{['fig:simulation_results_f']} show that as latency increases, the system tends to be conservative, leading to increased distances in the car-following scenario, and an increased number of ties in the gridworld case.
• Figure 3: Real World Demonstration Results. Fig. \ref{['fig:demo_results_qualitative']} shows recorded trajectories from our hardware setup. Without our safe networked control approach, the system fails to satisfy the safety specification "always remain at least $0.2$ meters away". However, our approach can satisfy the safety specification for constant and random delays. Also, as seen in Fig. \ref{['fig:demo_results_quantitative']}, the shield for the random delay case exploits the knowledge of delay transitions in Wi-Fi rather than assuming only the maximum latency, which allows the ego robot to follow the leader car at a closer distance. We set $\epsilon=0.95$ to construct the $\epsilon$-$\mathrm{shield}$. In Fig. \ref{['fig:wifi_traces']} and Fig. \ref{['fig:delay_transition_matrix']}, we show how the delay transition probability function, $\mathbb{P_\tau}$, is estimated using multiple runs of the Wi-Fi latency time-series data. Here, $\mathbb{P_\tau}$ is a conditional probability distribution with $3$ possible delays ($0,1,2$), where each delay is a bin of size $100$ ms.

Theorems & Definitions (8)

• Definition 1
• Definition 2
• Proposition 1
• proof
• Remark 1
• Theorem 1
• proof
• Remark 2