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.
Original language | English |
---|---|
Book series | Lecture Notes in Computer Science |
Volume | 6991 |
Pages (from-to) | 404-419 |
Number of pages | 16 |
ISSN | 0302-9743 |
DOIs | |
Publication status | Published - 2011 |
Event | 13th International Conference on Formal Engineering Methods - Durham, United Kingdom Duration: 26 Oct 2011 → 28 Oct 2011 Conference number: 13 |
Conference
Conference | 13th International Conference on Formal Engineering Methods |
---|---|
Number | 13 |
Country/Territory | United Kingdom |
City | Durham |
Period | 26/10/2011 → 28/10/2011 |
Keywords
- motorway traffic
- lane change
- collision freedom
- abstract model
- modal logic
- timed automata