kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Ensuring Safety at Intelligent Intersections: Temporal Logic Meets Reachability Analysis
KTH, School of Electrical Engineering and Computer Science (EECS), Intelligent systems, Decision and Control Systems (Automatic Control).
KTH, School of Electrical Engineering and Computer Science (EECS), Intelligent systems, Decision and Control Systems (Automatic Control).ORCID iD: 0000-0001-6653-5508
KTH, School of Electrical Engineering and Computer Science (EECS), Intelligent systems, Decision and Control Systems (Automatic Control).ORCID iD: 0000-0001-9940-5929
KTH, School of Electrical Engineering and Computer Science (EECS), Intelligent systems, Decision and Control Systems (Automatic Control).ORCID iD: 0000-0002-3672-5316
2024 (English)In: 2024 35TH IEEE INTELLIGENT VEHICLES SYMPOSIUM, IEEE IV 2024, Institute of Electrical and Electronics Engineers (IEEE) , 2024, p. 292-298Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE) , 2024. p. 292-298
Series
IEEE Intelligent Vehicles Symposium, ISSN 1931-0587
National Category
Robotics and automation
Identifiers
URN: urn:nbn:se:kth:diva-357531DOI: 10.1109/IV55156.2024.10588818ISI: 001275100900046Scopus ID: 2-s2.0-85194437666OAI: oai:DiVA.org:kth-357531DiVA, id: diva2:1919610
Conference
IEEE Intelligent Vehicles Symposium (IV), JUN 02-05, 2024, Jeju, SOUTH KOREA
Note

Part of ISBN 979-8-3503-4881-1; 979-8-3503-4882-8

QC 20241209

Available from: 2024-12-09 Created: 2024-12-09 Last updated: 2025-02-09Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Munhoz Arfvidsson, KajJiang, FrankJohansson, Karl H.Mårtensson, Jonas

Search in DiVA

By author/editor
Munhoz Arfvidsson, KajJiang, FrankJohansson, Karl H.Mårtensson, Jonas
By organisation
Decision and Control Systems (Automatic Control)
Robotics and automation

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 27 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf