地面机器人的障碍回避与导航的正式验证
Formal Verification of Obstacle Avoidance and Navigation of Ground Robots
AI总结：
本文研究了移动机器人在动态环境中安全性的核心问题，通过形式化验证方法验证了控制器在回避静态和移动障碍物时的安全性、被动安全性、主动友好安全性及被动方向安全性，并证明了在传感器不确定性和执行器扰动下仍能保证安全性的结论。
摘要：
移动机器人在动态环境中的安全性依赖于确保其不与障碍物碰撞。为了支持此类安全论证，我们分析并形式化验证了一系列日益强大的控制器安全属性：(i) 静态安全性，确保不会与静态障碍物发生碰撞；(ii) 被动安全性，确保在机器人移动时不会与静态或移动障碍物发生碰撞；(iii) 更强的被动友好安全性，其中机器人进一步保持足够的机动距离以避免障碍物碰撞；(iv) 被动方向安全性，允许机器人传感器覆盖不完美，即机器人意识到其环境并非所有内容都可见。我们补充了这些可证明正确的安全属性以活化属性：我们证明可证明安全的运动足够灵活，使机器人仍能导航航点并通过交叉口。我们使用混合系统模型和定理证明技术，描述并形式化验证机器人离散的控制决策及其连续的物理运动。此外，我们正式证明了在传感器不确定性和执行器扰动，以及引入更激进的操控选择时，安全性仍能得到保证。我们的验证结果是通用的，因为它们不限于特定控制算法的选择，而是识别出使它们同时适用于广泛控制算法类别的条件。
英文摘要：
The safety of mobile robots in dynamic environments is predicated on making sure that they do not collide with obstacles. In support of such safety arguments, we analyze and formally verify a series of increasingly powerful safety properties of controllers for avoiding both stationary and moving obstacles: (i) static safety, which ensures that no collisions can happen with stationary obstacles, (ii) passive safety, which ensures that no collisions can happen with stationary or moving obstacles while the robot moves, (iii) the stronger passive friendly safety in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well, and (iv) passive orientation safety, which allows for imperfect sensor coverage of the robot, i. e., the robot is aware that not everything in its environment will be visible. We complement these provably correct safety properties with liveness properties: we prove that provably safe motion is flexible enough to let the robot still navigate waypoints and pass intersections. We use hybrid system models and theorem proving techniques that describe and formally verify the robot's discrete control decisions along with its continuous, physical motion. Moreover, we formally prove that safety can still be guaranteed despite sensor uncertainty and actuator perturbation, and when control choices for more aggressive maneuvers are introduced. Our verification results are generic in the sense that they are not limited to the particular choices of one specific control algorithm but identify conditions that make them simultaneously apply to a broad class of control algorithms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
