Formalization and Analysis of Traffic Rules

• Applicants: Professor Dr.-Ing. Matthias Althoff; Professor Dr. Eric Hilgendorf; Professor Tobias Nipkow, Ph.D.
• Subject Area: Security and Dependability, Operating-, Communication- and Distributed Systems ; Principles of Law and Jurisprudence ; Traffic and Transport Systems, Intelligent and Automated Traffic
• Term: from 2018 to 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 397785447

One of the main barriers for making automated road vehicles a reality is the unsolved problem of assigning responsibilities when an automated vehicle is involved in an accident. Current traffic laws are written for human drivers and often imprecise, sometimes ambiguous, or even inconsistent. For those reasons, it is difficult for vehicle manufacturers to design vehicles that always comply with traffic rules. The consequence of the current situation is that there exist no right or wrong behavior in numerous traffic situations that can be mathematically formulated. However, in order to clarify liability claims upfront, it is of utmost importance, that the manufacturers have a clear guideline in form of a set of traffic rules for automated vehicles. For this reason, we develop a concretized and formalized version of the current traffic law. Concretization with parameterizable thresholds for correct behavior is important to clearly assign the fault to a manufacturer and to give manufacturers the possibility to design the vehicles such that they behave correctly. Formalization is important to remove ambiguity when it comes to interpreting traffic law. To facilitate the work of human judges and accident assessors, we aim at providing algorithms that automatically determine whether the behavior of the automated car complies with the formalized law using formal methods and the data of mandatory blackboxes. In particular, we will leverage methods from theorem proving for logical and discrete aspects of the law and reachability analysis for the continuous aspects, involving the motion of traffic participants. Discussion on how an automated car should react in certain situations is only just beginning in jurisprudence -- a situation that requires courageous and novel thinking -- hence, we aim at suggesting a fundamentally new approach that removes ambiguity and ensures correct implementation for checking our concretized and formalized traffic rules. The result of our proposed research will be a tool with a set of concretized and formalized traffic rules providing the following benefits: a) we propose a clear guideline for vehicle manufacturers on how their vehicles comply with traffic regulations, b) our tool allows manufacturers to offline verify their algorithms, c) our automated reasoning procedure can be used during the operation of the automated vehicle to safeguard its decisions, d) our automated reasoning supports more structured judgments, even when only human-driven vehicles are involved. Our developed tool will be demonstrated on past court cases as well as on traffic data obtained from real-world measurements.

• DFG Programme: Research Grants