Automatic Trajectory Synthesis for Real-Time Temporal Logic

• 成果类型: Article
• 署名作者: da Silva, Rafael Rodrigues; Kurtz, Vince; Lin, Hai
• 署名单位: University of Notre Dame
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2021.3058068
• 发表日期: 2022
• 页码: 780-794
• 关键词: planning; trajectory; Task analysis; scalability; Real-time systems; simulation; semantics; Automata; Automatic control; control systems; Formal language; linear programming; Linear systems; Motion control; natural languages; State-space methods; Trajectory optimization

摘要

Many safety-critical systems, such as autonomous vehicles and service robots, must achieve high-level task specifications with performance guarantees. Much recent progress toward this goal has been made through an automatic 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 nonconvex temporal logic over reals (RTL) specifications. We separate discrete task planning and continuous motion planning on-the-fly and harness highly efficient Boolean satisfiability and linear programming solvers to find dynamically feasible trajectories that satisfy nonconvex RTL specifications for high-dimensional systems. The proposed design algorithms are proven sound and complete, and simulation results demonstrate our approach's scalability.