地面机器人航点跟踪的形式化安全网
机器人学
2019-06-20 v3 计算机科学中的逻辑
系统与控制
摘要
我们提出一个可复用的形式化验证安全网，为具有容差和加速度的 Dubins 型地面机器人的二维航点跟踪提供端到端的安全性和活性保证。我们：i) 在微分动态逻辑(dL)中对机器人建模，并指定对控制器和机器人运动学的假设；ii) 证明带速度限制的航点跟踪的形式化安全性和活性性质；iii) 综合一个监视器，该监视器被自动证明在运行时强制模型合规；iv) 我们对 VeriPhy 工具链的使用使这些保证一直传递到机器码层面，且适用于不可信的控制器、环境和规划。只要航点被安全选择且其模型中的物理假设成立，该安全网的保证适用于任何机器人。实验表明这些假设在实践中成立，且在合规性与性能之间存在固有的权衡。
引用
@article{arxiv.1903.05073,
title = {A Formal Safety Net for Waypoint Following in Ground Robots},
author = {Brandon Bohrer and Yong Kiam Tan and Stefan Mitsch and Andrew Sogokon and André Platzer},
journal= {arXiv preprint arXiv:1903.05073},
year = {2019}
}