Keeping the Autonomous Vehicles Accountable: Legal and Logic Analysis on Traffic Code

The recent boost of the autonomous vehicles (AV) technology clearly outpaced the related regulating processes. Even for the already existing regulation like Traffic Code, opposable today to the human drivers, supposing to be maintained on medium term without important modifications, a major challenge pops-up. The content should by “translated” to a form enabling the engineers and authorities to keep also the autonomous vehicles accountable against the rules. The formalization methodology is consolidated, containing three major steps, practically implemented for the Overtaking as study case. Firstly, the Legal Analysis aims to eliminate the inherent redundancy of existing legal texts, clearly separate the responsibility of user and AV and finally to logically break them down in “predicate precursors”. The following step, Logic Analysis was conceived as a bridge between legal and engineering aspects, shaping step by step the Overtaking maneuver by using tools like the Modal Logic Flow Chart (sequenced but still untimed events), Atomic Proposition Tables (multi-level hierarchy) and finally Linear Temporal Logic (LTL) Formulas timed over a Temporal Logic Diagram. At this point the goal of this paper has been achieved, the methodology delivering the appropriate preparedness for automation and for further improvements of expressivity using High Order Language (HOL) by performing Engineering Analyses for aspects not yet covered by literature.