ロボット接触タスクの形式解析のための到達集合適合モデルの効率的生成
Efficiently Obtaining Reachset Conformance for the Formal Analysis of Robotic Contact Tasks
ハイブリッド動力学を持つロボット接触タスクに対し、非決定性を導入した線形ハイブリッドオートマトンで到達集合適合な抽象モデルを生成し、産業応用でのテスト工数を削減する手法を提案。
著者: Chencheng Tang, Matthias Althoff
分類: cs.RO, cs.SY, eess.SY
原文アブストラクト
Formal verification of robotic tasks requires a simple yet conformant model of the used robot. We present the first work on generating reachset conformant models for robotic contact tasks considering hybrid (mixed continuous and discrete) dynamics. Reachset conformance requires that the set of reachable outputs of the abstract model encloses all previous measurements to transfer safety properties. Aiming for industrial applications, we describe the system using a simple hybrid automaton with linear dynamics. We inject non-determinism into the continuous dynamics and the discrete transitions, and we optimally identify all model parameters together with the non-determinism required to capture the recorded behaviors. Using two 3-DOF robots, we show that our approach can effectively generate models to capture uncertainties in system behavior and substantially reduce the required testing effort in industrial applications.
