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/10自主车辆上验证了所提方法，该车辆在室内环境中导航并通过拥塞的WiFi链路传输丰富的激光雷达传感数据。