{'fraction_non_alphanumeric': 0.027663934426229508, 'fraction_numerical': 0.004610655737704918, 'mean_word_length': 5.08411214953271, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Hybrid Multi-Lane Spatial Logic

We present a semantic embedding of a spatio-temporal multi-modal logic, specifically defined to reason about motorway traffic, into Isabelle/HOL. The semantic model is an abstraction of a motorway, emphasising local spatial properties, and parameterised by the types of sensors deployed in the vehicles. We use the logic to define controller constraints to ensure safety, i.e., the absence of collisions on the motorway. After proving safety with a restrictive definition of sensors, we relax these assumptions and show how to amend the controller constraints to still guarantee safety. Published in iFM 2017 [4]. Formal verification of autonomous vehicles on motorways is a challenging problem, due to the complex interactions between dynamical behaviours and controller choices of the vehicles. To overcome the complexities of proving safety properties, we proposed to separate the dynamical behaviour from the concrete changes in space [2]. To that end, we defined Multi-Lane Spatial Logic (MLSL), which was used to express guards and invariants of controller automata defining a protocol for safe lane-change manoeuvres. Under the assumption that all vehicles adhere to this protocol, we proved that collisions were avoided. Subsequently, we presented an extension of MLSL to reason about changes in space over time, a system of natural deduction, and formally proved a safety theorem [5, 3]. This proof was carried out manually and dependent on strong assumptions about the vehicles’ sensors. We define a semantic embedding of a further extension of MLSL, inspired by Hybrid Logic [1]. Subsequently, we show how the safety theorem can be proved within this embedding. Finally, we alter this formal embedding by relaxing the assumptions on the sensors. We show that the previously proven safety theorem does not ensure safety in this case, and how the controller constraints can be strengthened to guarantee safety.