Synthesizing and verifying controllers for multi-lane traffic maneuvers

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 continu...

Full description

Saved in:
Bibliographic Details
Published in:Formal aspects of computing 2017-07, Vol.29 (4), p.583-600
Main Authors: Bochmann, Gregor V., Hilscher, Martin, Linker, Sven, Olderog, Ernst-Rüdiger
Format: Article
Language:English
Subjects:
Collision avoidance
Collision dynamics
Computer Science
Finite state machines
Hybrid systems
Math Applications in Computer Science
Original Article
Semantics
Theory of Computation
Traffic control
Traffic models
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0934-5043
1433-299X
DOI:10.1007/s00165-017-0424-4