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.

翻译：验证机器人在接触任务中的正确行为因接触相关模型不确定性而具有挑战性。标准测试方法往往难以奏效，因为无法获取所有（不可数无穷多个）解。为此，我们提出利用可达性分析对机器人接触任务中的行为进行形式化且高效的验证，该方法能够对照用户提供的规格检查所有可达状态。为实现此目标，我们拓展了针对受离散时间输入轨迹影响的混合（离散与连续混合）动力系统的可达性分析技术的最新成果。具体而言，我们提出一种新颖且可扩展的守卫交集方法，以可靠计算由接触引发的复杂行为。我们将受接触影响的机器人建模为包含关键时间延迟的混合自动机。通过验证在受限碰撞场景下安全人机交互的可行性（该场景此前方法无法处理），充分证明了我们方法的实用性。