Formalization of Intersection Traffic Rules in Temporal Logic

Intersections are difficult to navigate for both human drivers and autonomous vehicles because several diverse traffic rules must be considered. In addition, current traffic rules are ambiguous and cannot be applied directly by autonomous vehicles. Therefore, national traffic rules must be concretized and formalized so that they are machine-interpretable. We present formalized intersection traffic rules in temporal logic and use the German traffic regulations as a concrete example. Our formalization considers different types of intersections, i.e., signalized, traffic-sign-regulated, and unregulated intersections. We also define predicates and functions that can be easily reused for other national traffic laws. We evaluate our formalized traffic rules on recorded real-world scenarios and manually-created test scenarios. Our evaluation validates the formalization from different legal sources.