Temporal Logic Guided Safe Navigation for Autonomous Vehicles

TL;DR

This paper introduces a hybrid formal verification approach combining LTL and STL to generate safe, optimal trajectories for autonomous vehicles, ensuring safety in complex environments with efficient computation.

Contribution

It presents a novel hybrid method integrating LTL and STL for safe trajectory generation and control in autonomous vehicle navigation, outperforming traditional algorithms.

Findings

Outperforms conventional path planning in safety and complexity handling

Ensures safety constraints are met with formal guarantees

Maintains comparable computation times to existing methods

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.