Distributed controllers for provably safe, live and fair autonomous car manoeuvres in urban traffic
Maike Schwammberger · Carl von Ossiezky University of Oldenburg · 2020
While automated driving techniques are increasingly capturing the market, it is particularly important to consider vital functional properties of these systems. We introduce an approach to logically reason about functional properties of crossing manoeuvres at intersections. To this end, we introduce an abstract model for urban traffic situations and extended timed automata crossing controllers using formulae of our traffic logic Urban Multi-lane Spatial Logic (UMLSL) for turn manoeuvres at intersections. We show that even at complex intersections we can use purely spatial reasoning, detached from the underlying car dynamics, to prove safety (collision freedom) of the crossing controllers. We also examine liveness (something good finally happens) and fairness (no queue-jumping) of the controllers with the help of UPPAAL, a model-checker for (extended) timed automata. Furthermore, we introduce a case study, where we adapt the approach to a hazard warning communication protocol.