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: paths are represented with continuous Bezier curves, avoiding clipping and pass-through; computational complexity is polynomial (not exponential) in the number of sample points; global optimality can be certified; soundness and 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)运动规划列为Convex Set(GCS)图中最短的路径问题,并用convex优化来解决这个问题。 这种方法汇集了以现代优化为基础的最佳时间逻辑规划器和较老的自动数据理论方法,解决了每一种方法的局限性:路径代表着连续的贝塞尔曲线,避免了剪切和通过;计算复杂性在抽样点数量上是多数值的(非指数性);全球最佳性可以得到验证;在轻度假设下保证稳妥和完整;最重要的是,复杂的规格和高维系统的方法尺度,包括30-DoF人类结构。 开放源代码可在https://github.com/vincekurtz/ltl_gcs上查阅。