Ensuring Safety at Intelligent Intersections: Temporal Logic Meets Reachability Analysis

Fuente: arXiv
Salvato in:
Dettagli Bibliografici
Autori principali: Arfvidsson, Kaj Munhoz, Jiang, Frank J., Johansson, Karl H., Mårtensson, Jonas
Natura: Preprint
Pubblicazione: 2024
Soggetti:
Accesso online:
Tags: Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
_version_ 1866916251449688064
author Arfvidsson, Kaj Munhoz
Jiang, Frank J.
Johansson, Karl H.
Mårtensson, Jonas
author_facet Arfvidsson, Kaj Munhoz
Jiang, Frank J.
Johansson, Karl H.
Mårtensson, Jonas
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2405_11300
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle Ensuring Safety at Intelligent Intersections: Temporal Logic Meets Reachability Analysis
Arfvidsson, Kaj Munhoz
Jiang, Frank J.
Johansson, Karl H.
Mårtensson, Jonas
Systems and Control
Robotics
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.
title Ensuring Safety at Intelligent Intersections: Temporal Logic Meets Reachability Analysis
topic Systems and Control
Robotics
url https://arxiv.org/abs/2405.11300