为机器人接触任务生成符合可达集的简化模型，提升验证效率
Efficiently Obtaining Reachset Conformance for the Formal Analysis of Robotic Contact Tasks
- 用线性混合自动机建模，注入非确定性以匹配实测行为
- 参数与非确定性联合优化，确保模型覆盖所有实测输出
- 在3-DOF机器人上验证，显著减少工业测试工作量
机器人任务的形式化验证需要一个简单但符合实际的机器人模型。本文首次提出针对具有混合（连续与离散）动态特性的机器人接触任务，生成可达集符合的模型。可达集符合要求抽象模型的可达输出集必须包含所有历史测量值，以传递安全性质。为适配工业应用，系统采用具有线性动态的简化混合自动机描述，通过在连续动态和离散跳变中引入非确定性，并联合最优识别所有模型参数与所需非确定性，以捕获记录的行为。在两台3-DOF机器人上验证表明，该方法能有效生成涵盖系统不确定性的模型，并大幅降低工业应用中的测试需求。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。