View article

We adapt the Multi-lane Spatial Logic MLSL, introduced in [1] for proving the safety (collision freedom) of traffic manoeuvres on multi-lane motorways, where all cars drive in one direction, to the setting of country roads with two-way traffic. To this end, we need suitably refined sensor functions and length measurement in MLSL. Our main contribution is to show that also here we can separate the purely spatial reasoning from the underlying car dynamics in the safety proof.