Formal Verification of Robotic Contact Tasks via Reachability Analysis

要約

接触に関連するモデルの不確実性により、接触タスクにおけるロボットの正しい動作を検証することは困難です。
すべての（数え切れないほどの）解を得ることができないため、標準的なテスト方法では不十分なことがよくあります。
代わりに、到達可能性分析を使用して、接触タスクにおけるロボットの動作を正式かつ効率的に検証することを提案します。これにより、すべての到達可能な状態をユーザーが指定した仕様に対してチェックできるようになります。
この目的を達成するために、離散時間入力軌道に従うハイブリッド (離散と連続の混合) ダイナミクスの到達可能性解析における最先端技術を拡張します。
特に、接触によって引き起こされる複雑な動作を確実に計算するための、新規でスケーラブルなガード交差アプローチを提案します。
接触の対象となるロボットを、重大な時間遅延が含まれるハイブリッド オートマトンとしてモデル化します。
私たちのアプローチの有用性は、既存の方法では不可能であった、制約された衝突の存在下での人間とロボットの安全な相互作用を検証することによって実証されます。

要約(オリジナル)

Verifying the correct behavior of robots in contact tasks is challenging due to model uncertainties associated with contacts. Standard methods for testing often fall short since all (uncountable many) solutions cannot be obtained. Instead, we propose to formally and efficiently verify robot behaviors in contact tasks using reachability analysis, which enables checking all the reachable states against user-provided specifications. To this end, we extend the state of the art in reachability analysis for hybrid (mixed discrete and continuous) dynamics subject to discrete-time input trajectories. In particular, we present a novel and scalable guard intersection approach to reliably compute the complex behavior caused by contacts. We model robots subject to contacts as hybrid automata in which crucial time delays are included. The usefulness of our approach is demonstrated by verifying safe human-robot interaction in the presence of constrained collisions, which was out of reach for existing methods.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google