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.

翻译：自主机器人必须利用丰富的传感器数据做出安全控制决策。为处理这些数据，计算资源受限的机器人通常需要远程计算（即云端）的帮助，由云端运行计算密集型的深度神经网络感知或控制模型。然而，这种帮助会因网络延迟带来时间代价，导致云端基于过去的观测值为当前机器人状态计算控制指令。此类通信延迟可能违反关键安全属性（如避碰）。本文开发了确保在随机延迟通信网络上运行的机器人安全的方法。为此，我们利用形式化验证工具构建一个保护盾（即运行时监控器），该监控器在给定预期和最大网络延迟的情况下，为任何延迟的传感器观测提供一组安全动作。该保护盾干扰性极小，使网络化机器人能够以期望概率满足用时序逻辑规范表达的关键安全约束。我们在真实的F1/10th自动驾驶车辆上展示了该方法，该车辆在室内环境中导航，并通过拥塞的WiFi链路传输丰富的LiDAR传感器数据。