Specification-Compliant Reachability Analysis for Autonomous Vehicles Using On-the-Fly Model Checking

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. I. INTRODUCTIONIf autonomous vehicles are to be accepted by the broad public, they need to drive safely and thus comply with the rules of the road.To provide formal guarantees that an autonomous vehicle does not violate the rules of the road, they need to be formally specified.For the formalization of complex traffic rules, temporal logics have emerged as the language of choice 1.In particular, 2, 3 formalize parts of the German traffic law in metric temporal logic (MTL); 4 uses linear temporal logic (LTL) for the same purpose.