平面自主混合系统驻留机动的形式化验证
系统与控制
2017-09-11 v1 机器人学
摘要
我们对一种旨在执行平面车辆驻留机动的混合控制律进行了形式化验证。此类机动要求车辆在有限时间内到达其驻留点的邻域，并在等待进一步指令时保持在该邻域内。我们将动力学及控制律建模为混合程序，并形式化验证了所涉及的可达性与安全性属性。我们特别强调了不变区域的自动生成，事实证明这对于执行此类验证至关重要。我们使用定理证明器 Keymaera X 来解除部分生成的证明义务。
引用
@article{arxiv.1709.02561,
title = {Formal Verification of Station Keeping Maneuvers for a Planar Autonomous Hybrid System},
author = {Benjamin Martin and Khalil Ghorbal and Eric Goubault and Sylvie Putot},
journal= {arXiv preprint arXiv:1709.02561},
year = {2017}
}
备注
In Proceedings FVAV 2017, arXiv:1709.02126