Standard
An Abstract Model for Proving Safety of Multi-lane Traffic Manoeuvres. / Hilscher, Martin
; Linker, Sven; Olderog, Ernst-Rüdiger et al.
Formal Methods and Software Engineering: Proceedings of the 13th International Conference on Formal Engineering Methods, ICFEM 2011. ed. / Shengchao Qin; Zongyan Qiu. Berlin: Springer, 2011. p. 404-419 (Lecture Notes in Computer Science; Vol. 6991).
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Harvard
Hilscher, M
, Linker, S, Olderog, E-R & Ravn, AP 2011,
An Abstract Model for Proving Safety of Multi-lane Traffic Manoeuvres. in S Qin & Z Qiu (eds),
Formal Methods and Software Engineering: Proceedings of the 13th International Conference on Formal Engineering Methods, ICFEM 2011. Lecture Notes in Computer Science, vol. 6991, Springer, Berlin, pp. 404-419.
https://doi.org/10.1007/978-3-642-24559-6_28APA
Hilscher, M.
, Linker, S., Olderog, E.-R., & Ravn, A. P. (2011).
An Abstract Model for Proving Safety of Multi-lane Traffic Manoeuvres. In S. Qin, & Z. Qiu (Eds.),
Formal Methods and Software Engineering: Proceedings of the 13th International Conference on Formal Engineering Methods, ICFEM 2011 (pp. 404-419). (Lecture Notes in Computer Science; Vol. 6991). Springer.
https://doi.org/10.1007/978-3-642-24559-6_28Vancouver
Author
Bibtex
@inproceedings{39e1f7c391554aeaaa2171bdbca36f2e,
title = "An Abstract Model for Proving Safety of Multi-lane Traffic Manoeuvres",
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.",
author = "Martin Hilscher and Sven Linker and Ernst-R{\"u}diger Olderog and Ravn, {Anders P.}",
year = "2011",
doi = "10.1007/978-3-642-24559-6_28",
language = "English",
isbn = "9783642245589",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "404--419",
editor = "Shengchao Qin and Zongyan Qiu",
booktitle = "Formal Methods and Software Engineering",
}
RIS
TY - GEN
T1 - An Abstract Model for Proving Safety of Multi-lane Traffic Manoeuvres
AU - Hilscher, Martin
AU - Linker, Sven
AU - Olderog, Ernst-Rüdiger
AU - Ravn, Anders P.
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-642-24559-6_28
DO - 10.1007/978-3-642-24559-6_28
M3 - Conference contribution/Paper
SN - 9783642245589
T3 - Lecture Notes in Computer Science
SP - 404
EP - 419
BT - Formal Methods and Software Engineering
A2 - Qin, Shengchao
A2 - Qiu, Zongyan
PB - Springer
CY - Berlin
ER -
