Automatic Trajectory Synthesis for Real-Time Temporal Logic

TL;DR

This paper introduces a scalable, complete algorithm for synthesizing continuous trajectories that satisfy complex, non-convex real-time temporal logic specifications, advancing controller synthesis for safety-critical systems.

Contribution

It presents a novel, provably complete method that separates discrete planning from continuous motion planning, leveraging SAT and LP solvers for high-dimensional systems.

Findings

Algorithm is sound and complete.

Demonstrates scalability through simulations.

Handles non-convex real-time temporal logic specifications.

Abstract

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.