Automatic Trajectory Synthesis for Real-Time Temporal Logic

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 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 non-convex gls*rtl specifications. We separate discrete task planning and continuous motion planning on-the-fly and harness highly efficient boolean satisfiability (SAT) and gls*lp solvers to find dynamically feasible trajectories that satisfy non-convex gls*rtl specifications for high dimensional systems. The proposed design algorithms are proven sound and complete, and simulation results demonstrate our approach's scalability.