Safe Networked Robotics with Probabilistic Verification

要約

自律型ロボットは、安全な制御の決定を行うために豊富な感覚データを利用する必要があります。
このデータを処理するために、コンピューティングに制約のあるロボットは多くの場合、コンピューティング集約型のディープ ニューラル ネットワークの認識モデルや制御モデルを実行するリモート コンピューティング、またはクラウドからの支援を必要とします。
ただし、この支援にはネットワークの遅延による時間遅延が犠牲になり、その結果、現在のロボットの状態に対する制御コマンドを計算するためにクラウドで過去の観察が使用されることになります。
このような通信遅延は、衝突回避などの重要な安全特性の侵害につながる可能性があります。
この論文では、確率的遅延のある通信ネットワーク上で動作するロボットの安全性を確保する方法を開発します。
そのために、形式的検証のツールを使用して、予想される最大のネットワーク遅延を考慮して、遅延した感覚観察に対する安全なアクションのリストを提供するシールド、つまりランタイム モニターを構築します。
当社のシールドは侵入を最小限に抑え、ネットワーク化されたロボットが時相論理仕様として表現される主要な安全制約を希望の確率で満たすことを可能にします。
私たちは、屋内環境でナビゲーションし、混雑した WiFi リンクを介して豊富な LiDAR センサー データを送信する実際の F1/10th 自動運転車でアプローチを実証します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google