Synthesizing and verifying controllers for multi-lane traffic maneuvers

Gregor V. Bochmann, Martin Hilscher, Sven Linker, Ernst-Rüdiger Olderog

Research output: Contribution to journalArticlepeer-review


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.
Original languageEnglish
JournalFormal Aspects of Computing
Publication statusPublished - 13 Jul 2017


Dive into the research topics of 'Synthesizing and verifying controllers for multi-lane traffic maneuvers'. Together they form a unique fingerprint.

Cite this