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/10th自动驾驶车辆进行验证，该车辆在拥挤的室内环境中导航，并通过拥堵的WiFi链路传输丰富的激光雷达传感器数据。