Automatic Trajectory Synthesis for Real-Time Temporal Logic
This addresses the challenge of ensuring safety and correctness in safety-critical systems by enabling real-time handling of complex specifications, representing a novel method for a known bottleneck.
The paper tackles the problem of synthesizing continuous trajectories for high-dimensional systems to satisfy non-convex real-time temporal logic specifications, achieving scalability and provable completeness with efficient SAT and LP solvers.
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.