Temporal Logic Guided Safe Navigation for Autonomous Vehicles

TL;DR

The paper tackles safety verification for autonomous vehicles operating in uncertain environments by introducing a hybrid framework that blends Linear Temporal Logic (LTL) and Signal Temporal Logic (STL) with a Mixed Integer Linear Program (MILP) to synthesize safe trajectories and optimal controls. A SAT-based model checker generates counterexample paths to obtain a formally safe reference trajectory $\tau_{LTL}$, which the MILP uses to minimize a cost $\mathbb{J}$ while enforcing a robustness bound $\rho_{min}(\phi)$ and obeying dynamics $\mathbf{x}(k+1)=A\mathbf{x}(k)+B\mathbf{u}(k)$. The approach relies on a linearized AV model via feedback linearization and a symbolic path planner (NuSMV) to guarantee both safety and liveness, with subsequent MILP-based tracking yielding safe, efficient trajectories $\tau_{MILP}$. Simulations in simple and complex 2D environments show that the LTL+MILP method delivers formally safe trajectories with competitive computation times and greater robustness than baseline planners like A* and RRT*, demonstrating strong potential for safe autonomous navigation. Future work points to extending the framework to higher-dimensional systems and multi-signal STL specifications.

Abstract

Safety verification for autonomous vehicles (AVs) and ground robots is crucial for ensuring reliable operation given their uncertain environments. Formal language tools provide a robust and sound method to verify safety rules for such complex cyber-physical systems. In this paper, we propose a hybrid approach that combines the strengths of formal verification languages like Linear Temporal Logic (LTL) and Signal Temporal Logic (STL) to generate safe trajectories and optimal control inputs for autonomous vehicle navigation. We implement a symbolic path planning approach using LTL to generate a formally safe reference trajectory. A mixed integer linear programming (MILP) solver is then used on this reference trajectory to solve for the control inputs while satisfying the state, control and safety constraints described by STL. We test our proposed solution on two environments and compare the results with popular path planning algorithms. In contrast to conventional path planning algorithms, our formally safe solution excels in handling complex specification scenarios while ensuring both safety and comparable computation times.

Figures (5)

• Figure 1: NuSMV file for $\phi_2$
• Figure 2: Simple Environment with ($\phi_1$) LTL specification
• Figure 3: Complex Environment with ($\phi_2$) LTL specification
• Figure 4: STL Robustness for Simple Environment
• Figure 5: STL Robustness for Complex Environment