信号時相論理仕様からのスケーラブルな統合タスク・動作計画
Scalable Integrated Task and Motion Planning from Signal Temporal Logic Specifications
信号時相論理(STL)仕様を満たす連続軌道を、離散タスク計画と連続動作計画をオンザフライで分離しSMTとLPソルバを活用して合成する、健全かつ完全なスケーラブル手法を提案した。
著者: Rafael Rodrigues da Silva, Hai Lin
分類: cs.RO, cs.SY, eess.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 signal temporal logic (STL) specifications. Existing approaches, however, either consider some a priori discretization of the state-space, deal only with a convex fragment of STL, or are not provably complete. We propose a scalable, provably complete algorithm that directly synthesizes continuous trajectories to satisfy non-convex STL specifications. We separate discrete task planning and continuous motion planning on the fly and harness highly efficient satisfiability modulo theories (SMT) and linear programming (LP) solvers to find dynamically feasible trajectories for high dimensional systems that satisfies non-convex STL specifications. The proposed design algorithms are proved sound and complete, and simulation results demonstrate the scalability of our approach.
