地面机器人避障与导航的形式化验证
系统与控制
2019-06-20 v2 计算机科学中的逻辑
机器人学
摘要
动态环境中移动机器人的安全性基于确保它们不与障碍物发生碰撞。为支持此类安全性论证，我们分析并形式化验证了一系列逐渐增强的避障控制器安全属性：（i）静态安全，确保与静止障碍物不会发生碰撞；（ii）被动安全，确保机器人在移动时与静止或移动障碍物均不会发生碰撞；（iii）更强的被动友好安全，其中机器人进一步为障碍物保持足够的机动距离以使其也能避免碰撞；（iv）被动朝向安全，其允许机器人传感器覆盖不完美，即机器人意识到其环境中并非一切均可见。我们用活性属性补充这些可证明正确的安全属性：我们证明可证明安全的运动足够灵活，以使机器人仍能导航航点并通过交叉口。我们使用混合系统模型和定理证明技术来描述和形式化验证机器人的离散控制决策及其连续的物理运动。此外，我们形式化证明尽管存在传感器不确定性和执行器扰动，以及引入更激进机动的控制选择，安全性仍可得以保证。我们的验证结果具有通用性，因为它们不限于某一特定控制算法的选择，而是指出了使它们同时适用于广泛类别控制算法的条件。
引用
@article{arxiv.1605.00604,
title = {Formal Verification of Obstacle Avoidance and Navigation of Ground Robots},
author = {Stefan Mitsch and Khalil Ghorbal and David Vogelbacher and André Platzer},
journal= {arXiv preprint arXiv:1605.00604},
year = {2019}
}