Home > Research > Publications & Outputs > An Abstract Model for Proving Safety of Multi-l...

Links

Text available via DOI:

View graph of relations

An Abstract Model for Proving Safety of Multi-lane Traffic Manoeuvres

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Published
  • Martin Hilscher
  • Sven Linker
  • Ernst-Rüdiger Olderog
  • Anders P. Ravn
Close
Publication date2011
Host publicationFormal Methods and Software Engineering: Proceedings of the 13th International Conference on Formal Engineering Methods, ICFEM 2011
EditorsShengchao Qin, Zongyan Qiu
Place of PublicationBerlin
PublisherSpringer
Pages404-419
Number of pages16
ISBN (electronic)9783642245596
ISBN (print)9783642245589
<mark>Original language</mark>English

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume6991
ISSN (Print)0302-9743
ISSN (electronic)1611-3349

Abstract

We present an approach to prove safety (collision freedom) of multi-lane motorway traffic with lane-change manoeuvres. This is ultimately a hybrid verification problem due to the continuous dynamics of the cars. We abstract from the dynamics by introducing a new spatial interval logic based on the view of each car. To guarantee safety, we present two variants of a lane-change controller, one with perfect knowledge of the safety envelopes of neighbouring cars and one which takes only the size of the neighbouring cars into account. Based on these controllers we provide a local safety proof for unboundedly many cars by showing that at any moment the reserved space of each car is disjoint from the reserved space of any other car.