Towards Safe Autonomous Intersection Management: Temporal Logic-based Safety Filters for Vehicle Coordination

TL;DR

This work develops a provably safe AIM framework by combining temporal-logic specifications with Hamilton-Jacobi reachability to generate safe time-state corridors and driving limits for connected vehicles at intersections. The method uses backward reachability to verify that vehicles can satisfy goals while avoiding higher-priority conflicts, and forward reachability to refine entry/exit times, addressing the permissible planning trade-off between safety and efficiency. A driving-limits service then computes least-restrictive acceleration bounds that ensure vehicles remain within their reserved corridors in real time ($A_j(z_j,t)$ derived from $V_{\Phi^4_j}$). Numerical results on a simulated 4-way intersection demonstrate real-time feasibility across multiple scenarios and report sub-millisecond to millisecond compute times for driving limits, indicating practical potential for AIM deployments and inter-region coordination in the future.

Abstract

In this paper, we introduce a temporal logic-based safety filter for Autonomous Intersection Management (AIM), an emerging infrastructure technology for connected vehicles to coordinate traffic flow through intersections. Despite substantial work on AIM systems, the balance between intersection safety and efficiency persists as a significant challenge. Building on recent developments in formal methods that now have become computationally feasible for AIM applications, we introduce an approach that starts with a temporal logic specification for the intersection and then uses reachability analysis to compute safe time-state corridors for the connected vehicles that pass through the intersection. By analyzing these corridors, in contrast to single trajectories, we can make explicit design decisions regarding safety-efficiency trade-offs while taking each vehicle's decision uncertainty into account. Additionally, we compute safe driving limits to ensure that vehicles remain within their designated safe corridors. Combining these elements, we develop a service that provides safety filters for AIM coordination of connected vehicles. We evaluate the practical feasibility of our safety framework using a simulated 4-way intersection, showing that our approach performs in real-time for multiple scenarios.

Figures (4)

• Figure 1: Shown is the conceptual design of our traffic management system. While acting between high-level city-scale route planning and on-board control, this system performs central planning and coordination between vehicles for local regions while accounting for their safe operational limits.
• Figure 2: Conceptual illustration of the four passes in our analysis. (a) shows $\Phi^1_j$, the result of Pass 1, which ensures conformity to invariant constraints, such as road geometries or static obstacles. This is illustrated by its shape on the top. (b) shows $\Phi^2_j$ when non-invariant constraints are added in the form of $\mathcal{D}_j$. (c) shows $\Phi^3_j$ in the first step of refining the trajectories. After this pass, all remaining trajectories that are embedded in $\Phi^3_j$ satisfy the entry conditions $\mathcal{G}^\leftarrow_j$. (d) shows $\Phi^4_j$ after it has similarly pruned trajectories even further, now also considering exit conditions $\mathcal{G}^\rightarrow_j$.
• Figure 3: Two vehicles passing through the 4-way intersection perpendicular to each other. The first vehicle (red) going in the vertical direction, and the second vehicle (blue) going in the horizontal direction. Both vehicles stay within their indicated reserved time-state sets. In more detail, we show important aspects of the second vehicle's safety analyses.
• Figure 4: Shown are scenarios that illustrate the flexibility of our approach. By providing only $\mathcal{G}^\leftarrow_j$ and $\mathbb G^\rightarrow_j$, it is possible to compute these safe corridors.