In this work, we develop a temporal logic-based safety framework for Autonomous Intersection Management (AIM) to ensure the safety of connected vehicles navigating through intelligent intersections. Traditional AIM systems face challenges in balancing safety and efficiency, often relying on central decision-making to enhance intersection coordination. Our approach addresses this challenge by leveraging formal methods, specifically temporal logic and reachability analysis, to provide rigorous safety guarantees. We begin by specifying the required behavior for vehicles passing through intersections as linear temporal logic formulas. These specifications are then decomposed into a series of Hamilton-Jacobi reachability analyses using temporal logic trees, allowing for the automated verification of intersection behaviors. This method enables the computation of safe time-state corridors for vehicles, facilitating explicit safety-efficiency trade-offs while considering decision uncertainties. Additionally, we determine safe driving limits to ensure vehicles remain within their designated corridors. Our framework is evaluated using simulations of both 3-way and 4-way intersections, demonstrating its ability to verify and enforce safety in real-time across various scenarios.

I detta arbete presenterar vi ett nytt säkerhetssystem för intelligenta regioner som möter utmaningarna med att koordinera uppkopplade och automatiserade fordon. Intelligenta regioner omfattar områden som korsningar, motorvägar och stadsgator, där trafiken hanteras av intelligenta transportsystem som anpassar sig till realtidsförhållanden, regionala trafikmönster och specifika händelser. Med hjälp av temporallogik och nåbarhetsanalys erbjuder vår metod starka säkerhetsgarantier över olika trafiksituationer. Inledningsvis definierar vi det önskade beteendet för alla fordon som navigerar genom korsningen med hjälp av temporallogiska påståenden i form av en säkerhetsspecifikation. Därefter dekonstrueras specifikationen automatiskt till en sekvens av mindre, hanterbara Hamilton-Jacobi nåbarhetsanalyser genom en nyligen utvecklad beräkningsmetod kallad temporala logikträd. Detta möjliggör automatiserad verifiering av fordonsbeteenden och en explicit avvägning mellan säkerhet och effektivitet. I detta steg tilldelas fordonen färdvägskorridorer som garanterar att både traditionella trafikregler och specifika beteendekrav uppfylls. Vi fastställer även säkra körgränser för att säkerställa att fordonen förblir inom sina tilldelade korridorer. Vårt system demonstreras genom simuleringar av trevägs- och fyrvägs-korsningar, där fordon med potentiellt kolliderande färdvägar garanteras säker passage.