Autonomous robots must utilize rich sensory data to make safe control decisions. Often, compute-constrained robots require assistance from remote computation (''the cloud'') if they need to invoke compute-intensive Deep Neural Network perception or control models. Likewise, a robot can be remotely teleoperated by a human during risky scenarios. However, this assistance comes at the cost of a time delay due to network latency, resulting in stale/delayed 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 teleoperated robots with stochastic latency. To do so, we use tools from formal verification to construct a shield (i.e., run-time monitor) that provides a list of safe actions for any delayed sensory observation, given the expected and worst-case network latency. Our shield is minimally intrusive and enables networked robots to satisfy key safety constraints, expressed as temporal logic specifications, with high probability. Our approach gracefully improves a teleoperated robot's safety vs. efficiency trade-off as a function of network latency, allowing us to quantify performance gains for WiFi or even future 5G networks. We demonstrate our approach on a real F1/10th autonomous vehicle that navigates in crowded indoor environments and transmits rich LiDAR sensory data over congested WiFi links.

翻译：自主机器人必须利用丰富的感知数据来做出安全的控制决策。通常，计算受限的机器人在需要调用计算密集型深度神经网络感知或控制模型时，需要借助远程计算（即"云端"）的辅助。同样，机器人在高风险场景下可由人类进行远程操控。然而，这种辅助以网络延迟导致的时间延迟为代价，导致云端基于过时/延迟的观测数据为当前机器人状态计算控制指令。此类通信延迟可能引发违反关键安全属性（如避障）的风险。本文开发了确保具有随机延迟的遥操作机器人安全性的方法。为此，我们利用形式化验证工具构建了一个屏蔽（即运行时监控器），该监控器能在给定预期和最坏情况网络延迟下，为任意延迟的感知观测提供安全动作集合。我们的屏蔽具有最小侵入性，能使网络化机器人以高概率满足以时序逻辑规范表述的关键安全约束。该方法能根据网络延迟优雅地改善遥操作机器人的安全性与效率权衡，使我们能够量化WiFi甚至未来5G网络的性能增益。我们在真实F1/10自动驾驶车辆上验证了该方法，该车辆在拥挤室内环境中导航，并通过拥塞的WiFi链路传输丰富的LiDAR感知数据。