平面ハイブリッドシステムのステーションキーピング操作の形式検証
Formal Verification of Station Keeping Maneuvers for a Planar Autonomous Hybrid System
平面車両のステーションキーピング制御則をハイブリッドプログラムとしてモデル化し、到達性と安全性を定理証明器KeYmaera Xで形式的に検証した。不変領域の自動生成が検証の鍵となることを示した。
著者: Benjamin Martin, Khalil Ghorbal, Eric Goubault, Sylvie Putot
分類: eess.SY, cs.RO, cs.SY
原文アブストラクト
We formally verify a hybrid control law designed to perform a station keeping maneuver for a planar vehicle. Such maneuver requires that the vehicle reaches a neighborhood of its station in finite time and remains in it while waiting for further instructions. We model the dynamics as well as the control law as a hybrid program and formally verify both the reachability and safety properties involved. We highlight in particular the automated generation of invariant regions which turns out to be crucial in performing such verification. We use the theorem prover Keymaera X to discharge some of the generated proof obligations.
