Home > Research > Publications & Outputs > Synthesizing and verifying controllers for mult...

Research

Associated organisational unit

Links

Text available via DOI:

View graph of relations

Synthesizing and verifying controllers for multi-lane traffic maneuvers

Research output: Contribution to Journal/Magazine › Journal article › peer-review

Published

Standard

Synthesizing and verifying controllers for multi-lane traffic maneuvers. / Bochmann, Gregor V.; Hilscher, Martin; Linker, Sven et al.
In: Formal Aspects of Computing, Vol. 29, 13.07.2017, p. 583–600.

Research output: Contribution to Journal/Magazine › Journal article › peer-review

Harvard

Bochmann, GV, Hilscher, M, Linker, S & Olderog, E-R 2017, 'Synthesizing and verifying controllers for multi-lane traffic maneuvers', Formal Aspects of Computing, vol. 29, pp. 583–600. https://doi.org/10.1007/s00165-017-0424-4

APA

Bochmann, G. V., Hilscher, M., Linker, S., & Olderog, E.-R. (2017). Synthesizing and verifying controllers for multi-lane traffic maneuvers. Formal Aspects of Computing, 29, 583–600. https://doi.org/10.1007/s00165-017-0424-4

Vancouver

Bochmann GV, Hilscher M, Linker S, Olderog ER. Synthesizing and verifying controllers for multi-lane traffic maneuvers. Formal Aspects of Computing. 2017 Jul 13;29:583–600. Epub 2017 Mar 13. doi: 10.1007/s00165-017-0424-4

Author

Bochmann, Gregor V. ; Hilscher, Martin ; Linker, Sven et al. / Synthesizing and verifying controllers for multi-lane traffic maneuvers. In: Formal Aspects of Computing. 2017 ; Vol. 29. pp. 583–600.

Bibtex

@article{aef848db2b43427482583fca1a8c51ec,
title = "Synthesizing and verifying controllers for multi-lane traffic maneuvers",
abstract = "The dynamic behavior of a car can be modeled as a hybrid system involving continuous state changes and discrete state transitions. We show that the control of safe (collision free) lane change maneuvers in multi-lane traffic on highways can be described by finite state machines extended with continuous variables coming from the environment. We use standard theory for controller synthesis to derive the dynamic behavior of a lane-change controller. Thereby, we contrast the setting of interleaving semantics and synchronous concurrent semantics. We also consider the possibility of exchanging knowledge between neighboring cars in order to come up with the right decisions. Finally, we address compositional verification using an assumption-guarantee paradigm.",
author = "Bochmann, {Gregor V.} and Martin Hilscher and Sven Linker and Ernst-R{\"u}diger Olderog",
year = "2017",
month = jul,
day = "13",
doi = "10.1007/s00165-017-0424-4",
language = "English",
volume = "29",
pages = "583–600",
journal = "Formal Aspects of Computing",

}

RIS

TY - JOUR

T1 - Synthesizing and verifying controllers for multi-lane traffic maneuvers

AU - Bochmann, Gregor V.

AU - Hilscher, Martin

AU - Linker, Sven

AU - Olderog, Ernst-Rüdiger

PY - 2017/7/13

Y1 - 2017/7/13

N2 - The dynamic behavior of a car can be modeled as a hybrid system involving continuous state changes and discrete state transitions. We show that the control of safe (collision free) lane change maneuvers in multi-lane traffic on highways can be described by finite state machines extended with continuous variables coming from the environment. We use standard theory for controller synthesis to derive the dynamic behavior of a lane-change controller. Thereby, we contrast the setting of interleaving semantics and synchronous concurrent semantics. We also consider the possibility of exchanging knowledge between neighboring cars in order to come up with the right decisions. Finally, we address compositional verification using an assumption-guarantee paradigm.

AB - The dynamic behavior of a car can be modeled as a hybrid system involving continuous state changes and discrete state transitions. We show that the control of safe (collision free) lane change maneuvers in multi-lane traffic on highways can be described by finite state machines extended with continuous variables coming from the environment. We use standard theory for controller synthesis to derive the dynamic behavior of a lane-change controller. Thereby, we contrast the setting of interleaving semantics and synchronous concurrent semantics. We also consider the possibility of exchanging knowledge between neighboring cars in order to come up with the right decisions. Finally, we address compositional verification using an assumption-guarantee paradigm.

U2 - 10.1007/s00165-017-0424-4

DO - 10.1007/s00165-017-0424-4

M3 - Journal article

VL - 29

SP - 583

EP - 600

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

ER -