Safe Networked Robotics via Formal Verification

要約

自律型ロボットは、安全な制御の決定を下すために、豊富な感覚データを利用する必要があります。
多くの場合、計算に制約のあるロボットは、計算集約型のディープ ニューラル ネットワークの認識モデルまたは制御モデルを呼び出す必要がある場合、リモート計算 (「クラウド」) の支援を必要とします。
同様に、危険なシナリオでは、人間がロボットを遠隔操作することもできます。
ただし、この支援にはネットワーク遅延による時間遅延という代償が伴い、その結果、現在のロボット状態の制御コマンドを計算するためにクラウドで使用される古い/遅延した観測が発生します。
このような通信遅延は、衝突回避などの重要な安全特性の侵害につながる可能性があります。
この論文では、確率的待ち時間を伴う遠隔操作ロボットの安全性を確保する方法を開発します。
そのために、予想されるネットワーク遅延と最悪の場合のネットワーク遅延を考慮して、正式な検証のツールを使用して、遅延した感覚観察に対する安全なアクションのリストを提供するシールド (つまり、ランタイム モニター) を構築します。
私たちのシールドは侵入を最小限に抑え、ネットワーク化されたロボットが時相論理仕様として表される主要な安全制約を高い確率で満たすことを可能にします。
私たちのアプローチは、ネットワーク遅延の関数として遠隔操作ロボットの安全性と効率のトレードオフを適切に改善し、WiFi または将来の 5G ネットワークのパフォーマンスの向上を定量化できるようにします。
混雑した屋内環境でナビゲートし、混雑した WiFi リンクを介して豊富な LiDAR センサー データを送信する、実際の F1/10th 自動運転車両でアプローチを示します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google