An abstract model for proving safety of autonomous urban traffic

With Multi-lane Spatial Logic (MLSL), we can prove safety (collision freedom) on multi-lane motorways and country roads. In this work, we consider an extension of MLSL to deal with urban traffic scenarios, thereby focusing on crossing manoeuvres at intersections. To this end, we modify the existing abstract model by introducing a generic topology of urban traffic networks. We then show that even at intersections we can use purely spatial reasoning, detached from the underlying car dynamics, to prove safety of controllers modelled as extended timed automata.