为地面机器人路径跟随提供形式安全网
A Formal Safety Net for Waypoint Following in Ground Robots
AI总结：
本文提出一个可重用的形式验证安全网，为具有容差和加速度的Dubins型地面机器人提供端到端的安全性和活跃性保证，通过形式化方法验证安全性和活跃性属性，并合成监控器以确保运行时的模型合规性。
摘要：
我们提出一个可重用的形式验证安全网，为具有容差和加速度的Dubins型地面机器人提供端到端的安全性和活跃性保证。我们：i) 用微分动态逻辑（dL）建模机器人，并对控制器和机器人运动学制定假设；ii) 证明具有速度限制的路径跟随形式安全性和活跃性属性；iii) 合成一个监控器，该监控器被自动证明在运行时强制执行模型合规性；iv) 我们使用VeriPhy工具链使这些保证延伸到不受信任的控制器、环境和计划的机器代码层面。安全网的保证适用于任何机器人，只要路径被安全选择且其模型中的物理假设成立。实验表明这些假设在实践中成立，存在合规性与性能之间的内在权衡。
英文摘要：
We present a reusable formally verified safety net that provides end-to-end safety and liveness guarantees for 2D waypoint-following of Dubins-type ground robots with tolerances and acceleration. We: i) Model a robot in differential dynamic logic (dL), and specify assumptions on the controller and robot kinematics, ii) Prove formal safety and liveness properties for waypoint-following with speed limits, iii) Synthesize a monitor, which is automatically proven to enforce model compliance at runtime, and iv) Our use of the VeriPhy toolchain makes these guarantees carry over down to the level of machine code with untrusted controllers, environments, and plans. The guarantees for the safety net apply to any robot as long as the waypoints are chosen safely and the physical assumptions in its model hold. Experiments show these assumptions hold in practice, with an inherent trade-off between compliance and performance.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
