実時間時相論理のための軌道自動合成
Automatic Trajectory Synthesis for Real-Time Temporal Logic
非凸な実時間時相論理仕様を満たす連続軌道を、SATと線形計画法を組み合わせてオンザフライで合成するスケーラブルかつ完全なアルゴリズムを提案した。
著者: Rafael Rodrigues da Silva, Vince Kurtz, Hai Lin
分類: eess.SY, cs.FL, cs.RO, cs.SY
原文アブストラクト
Many safety-critical systems must achieve high-level task specifications with guaranteed safety and correctness. Much recent progress towards this goal has been made through controller synthesis from temporal logic specifications. Existing approaches, however, have been limited to relatively short and simple specifications. Furthermore, existing methods either consider some prior discretization of the state-space, deal only with a convex fragment of temporal logic, or are not provably complete. We propose a scalable, provably complete algorithm that synthesizes continuous trajectories to satisfy non-convex \gls*{rtl} specifications. We separate discrete task planning and continuous motion planning on-the-fly and harness highly efficient boolean satisfiability (SAT) and \gls*{lp} solvers to find dynamically feasible trajectories that satisfy non-convex \gls*{rtl} specifications for high dimensional systems. The proposed design algorithms are proven sound and complete, and simulation results demonstrate our approach's scalability.
