Synthesizing and verifying controllers for multi-lane traffic maneuvers

Bochmann, Gregor V, Hilscher, Martin, Linker, Sven and Olderog, Ernst-Ruediger (2017) Synthesizing and verifying controllers for multi-lane traffic maneuvers FORMAL ASPECTS OF COMPUTING, 29 (4). pp. 583-600. ISSN 0934-5043, 1433-299X

Text faoc-synthesis.pdf - Author Accepted Manuscript Download (320kB)

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.

Item Type:	Article
Uncontrolled Keywords:	Multi-lane highway traffic, Lane-change maneuver, Collision freedom, Controller synthesis, Interleaving and synchronous concurrency, Assumption-guarantee paradigm
Depositing User:	Symplectic Admin
Date Deposited:	21 Nov 2017 11:25
Last Modified:	16 Jun 2026 04:33
DOI:	10.1007/s00165-017-0424-4
Related Websites:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3007719
Disclaimer:	The University of Liverpool is not responsible for content contained on other websites from links within repository metadata. Please contact us if you notice anything that appears incorrect or inappropriate.