Imagine an automated vehicle violating a traffic rule and, by that, causing an accident. This would not only be devastating for a responsible operator, but more importantly, each such incident would erode the trust of the public in automated vehicles. Fortunately, compliance with traffic rules can be fully controlled, unless other traffic participants breach them—this causality obviously makes it possible for responsible operators to avoid liability claims. Traffic rules can be seen as guardrails for automated driving and should take center stage. Unfortunately, this is currently not the case. Many traffic rules are typically implicitly embedded in various fragments of the software stack of automated vehicles. Instead, the considered traffic rules should be explicitly and centrally provided. Adherence to traffic rules should also be ensured by formal methods to gain the trust needed in the public. This article provides all the steps required to achieve this goal. Due to the interdisciplinary nature of this topic (law, engineering, and computer science), we aim to address a broad audience by focusing on the governing principles of the presented methods, and we refer to more technical works for details.

Autonomous vehicles must obey the rules of the road to safely participate in road traffic. To enforce these rules during motion planning, they are often formalized in temporal logic. Such formalizations need to be very general to cover all possible traffic situations, resulting in large and complex logic formulas. During motion planning, however, we are usually confronted with a concrete scenario in which parts of the formulas may be irrelevant. Since specification-compliant motion planning under complex specifications is computationally challenging, we aim to simplify the traffic rules by removing these irrelevant parts. To this end, we first present a general algorithm that augments linear temporal logic formulas with scenario-specific knowledge. Then, we provide a method for extracting knowledge from traffic scenarios to augment traffic rules. We can formally guarantee that the augmented specification is equivalent to the original formula in the given scenario. Therefore, subsequent motion planning modules that handle temporal logic specifications need only consider the augmented formulas. We benchmark our approach in recorded real-world scenarios to demonstrate that it can significantly accelerate specification-compliant motion planning.

Abstract Hybrid systems are often safety-critical and at the same time difficult to formally verify due to their mixed discrete and continuous behavior. To address this issue, we propose a novel incremental verification algorithm for hybrid systems based on online monitoring techniques and reachability analysis. To this end, we develop a four-valued semantics for signal temporal logic that allows us to distinguish two types of uncertainty: one arising from set-based evaluation and another one from the incremental nature of our algorithm. Using these semantics to continuously update the verification verdict, our verification algorithm is the first to run alongside the reachability analysis of the system to be verified. This makes it possible to stop the reachability analysis as soon as we obtain a conclusive verdict. We demonstrate the usefulness of our novel approach by several experiments.

Compliance with the rules of the road is crucial for the safe operation of autonomous vehicles. Previous work has shown that one can expedite rule-compliant motion planning by constraining the search space based on the reachable states of the vehicle. We propose an algorithm to overapproximate the states that a vehicle can reach while adhering to a linear temporal logic specification. By integrating model checking into reachability analysis, we can exclude many non-compliant states early. Moreover, we only have to semantically split the reachable set when necessary to decide the validity of the specification. This significantly reduces the computation time compared to existing approaches. We benchmark our approach in recorded real-world scenarios to demonstrate its real-time capability.