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.