Temporal logic is a concise way of specifying complex tasks. But motion planning to achieve temporal logic specifications is difficult, and existing methods struggle to scale to complex specifications and high-dimensional system dynamics. In this paper, we cast Linear Temporal Logic (LTL) motion planning as a shortest path problem in a Graph of Convex Sets (GCS) and solve it with convex optimization. This approach brings together the best of modern optimization-based temporal logic planners and older automata-theoretic methods, addressing the limitations of each: we avoid clipping and passthrough by representing paths with continuous Bezier curves; computational complexity is polynomial (not exponential) in the number of sample points; global optimality can be certified (though it is not guaranteed); soundness and probabilistic completeness are guaranteed under mild assumptions; and most importantly, the method scales to complex specifications and high-dimensional systems, including a 30-DoF humanoid. Open-source code is available at https://github.com/vincekurtz/ltl_gcs.

翻译：时间逻辑是一种简洁表达复杂任务的方式。但实现时间逻辑规约的运动规划十分困难，现有方法难以扩展到复杂规约和高维系统动力学。本文提出将线性时间逻辑(LTL)运动规划转化为凸集图(GCS)中的最短路径问题，并通过凸优化求解。该方法融合了现代基于优化时间逻辑规划器与经典自动机理论方法的优势，同时克服了各自的局限：通过连续贝塞尔曲线表示路径避免截断与穿透；计算复杂度在采样点数量上呈多项式（而非指数）增长；可验证全局最优性（虽不能保证）；在温和假设条件下保证可靠性和概率完备性；最关键的是，该方法能扩展到复杂规约和高维系统，包括30自由度人形机器人。开源代码见https://github.com/vincekurtz/ltl_gcs。