Automatic Synthesis of Smooth Infinite Horizon Paths Satisfying Linear Temporal Logic Specifications

Abstract Automatically constructing smooth paths that satisfy a formal specification is a challenging problem. Existing methods struggle to scale to long horizon specifications and challenging environments. We present a method that uses abstraction, model checking, and convex optimization to solve for a smooth Bézier spline that is guaranteed to satisfy a Linear Temporal Logic specification. Our approach uses a coarse abstraction to avoid the state explosion of other abstraction based methods, and successfully avoids the computational challenges of directly optimizing the non-convex temporal logic semantics. We prove our method is sound and complete and demonstrate a significant computational advantage relative to state of the art approaches. Generating such smooth paths has natural applications in path planning for autonomous robots, and we demonstrate the applicability of our method on path planning for a quadrotor.