Formalization and Analysis of Traffic Rules

自动道路车辆实现的主要障碍之一是当自动车辆发生事故时尚未解决的责任分配问题。目前的交通法规是为人类驾驶员制定的，往往不准确，有时含糊其辞，甚至不一致。出于这些原因，汽车制造商很难设计出始终遵守交通规则的汽车。当前情况的结果是，在许多可以数学表达的交通情况下，没有对或错的行为。然而，为了预先澄清责任索赔，至关重要的是，制造商以一套自动车辆交通规则的形式制定了明确的指导方针。为此，我们制定了现行交通法的具体化和形式化版本。使用正确行为的可参数化阈值进行具体化，对于明确将故障归因于制造商并使制造商有可能设计车辆以使其正确行为非常重要。在解释交通法时，形式化对于消除歧义很重要。为了方便人类法官和事故评估员的工作，我们的目标是提供算法，使用形式化方法和强制黑盒数据自动确定自动驾驶汽车的行为是否符合形式化法律。特别是，我们将利用定理证明的方法对法律的逻辑和离散方面进行证明，并对涉及交通参与者运动的连续方面进行可达性分析。关于自动汽车在某些情况下应该如何反应的讨论在法理学上才刚刚开始--这种情况需要勇敢和新颖的思维--因此，我们的目标是提出一种全新的方法，消除歧义，并确保检查我们具体和形式化的交通规则的正确实施。我们拟议的研究结果将是一个具有一套具体和正式的交通规则的工具，提供以下好处：a)我们为车辆制造商提出了关于他们的车辆如何遵守交通规则的明确指导方针，b)我们的工具允许制造商离线验证他们的算法，c)我们的自动推理程序可以在自动车辆的操作过程中使用，以维护其决策，d)我们的自动推理支持更结构化的判断，即使只涉及到人类驾驶的车辆。我们开发的工具将在过去的法庭案件以及从真实世界测量获得的交通数据上进行演示。

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.