Ensuring Safety at Intelligent Intersections: Temporal Logic Meets Reachability Analysis

TL;DR

This work addresses safety guarantees for multi-vehicle passage through intelligent intersections with evolving traffic rules. It introduces a framework that formulates intersection requirements in Linear Temporal Logic (LTL) and verifies feasibility by constructing Temporal Logic Trees (TLTs) built from Hamilton-Jacobi (HJ) reachability analyses, accommodating nonlinear vehicle dynamics and complex road geometries. Key contributions include an LTL-based sequential path planning approach, a practical TLT construction method using backward reachable tubes and robust control invariant sets, an offline-online computation scheme to manage conflicting objectives, and a demonstration on a three-vehicle T-intersection showing feasible, safe coordination. The framework enables automatic safety guarantees and flexible adaptation to new intersection specifications, with potential for real-time verification aided by offline computation and V2I-enabled scheduling.

Abstract

In this work, we propose an approach for ensuring the safety of vehicles passing through an intelligent intersection. There are many proposals for the design of intelligent intersections that introduce central decision-makers to intersections for enhancing the efficiency and safety of the vehicles. To guarantee the safety of such designs, we develop a safety framework for intersections based on temporal logic and reachability analysis. We start by specifying the required behavior for all the vehicles that need to pass through the intersection as linear temporal logic formula. Then, using temporal logic trees, we break down the linear temporal logic specification into a series of Hamilton-Jacobi reachability analyses in an automated fashion. By successfully constructing the temporal logic tree through reachability analysis, we verify the feasibility of the intersection specification. By taking this approach, we enable a safety framework that is able to automatically provide safety guarantees on new intersection behavior specifications. To evaluate our approach, we implement the framework on a simulated T-intersection, where we show that we can check and guarantee the safety of vehicles with potentially conflicting paths.

Figures (3)

• Figure 1: T-Intersection example with two vehicles passing through and the safe sets computed for the intersection specification.
• Figure 2: Illustration of the constructed TLT for the $j$th vehicle's individual LTL specification \ref{['eq:spp-ltl']} that ensures safety at intersections.
• Figure 3: Shown are the safe sets for all vehicles over time (left part) and the sliced time snapshots of the safe sets for each vehicle, $\mathcal{V}_1$ (red), $\mathcal{V}_2$ (blue) and $\mathcal{V}_3$ (purple), with priority in the given order (right part). Since the safe sets are computed starting from the goal state, we mark the goal state of each vehicle with an icon. The top row of the right part shows the analysis done for $\mathcal{V}_1$ w.r.t its individual objective $\varphi_1$. Similarly, the second and third rows show the analyses done for $\mathcal{V}_2$ and $\mathcal{V}_3$, respectively, where the gray regions are the reachable sets of higher priority vehicles seen as obstacles.

Theorems & Definitions (2)

• Definition II.1
• Definition II.2