Formalization of Interstate Traffic Rules in Temporal Logic

To allow autonomous vehicles to safely participate in traffic and to avoid liability claims for car manufacturers, autonomous vehicles must obey traffic rules. However, current traffic rules are not formulated in a precise and mathematical way, so that they cannot be directly applied to autonomous vehicles. Additionally, several legal sources other than national traffic laws must be considered to infer detailed traffic rules. Thus, we formalize traffic rules for interstates based on the German Road Traffic Regulation, the Vienna Convention on Road Traffic, and legal decisions from courts. This makes it possible to automatically and unambiguously check whether traffic rules are being met by autonomous vehicles. Temporal logic is used to express the obtained rules mathematically. Our formalized traffic rules are evaluated for recorded data on more than 2,500 vehicles.