Specification-Compliant Driving Corridors for Motion Planning of Automated Vehicles

It is crucial for automated vehicles to explicitly comply with specifications, including traffic rules, to ensure their safe and effective participation in road traffic. Such compliance is also essential for vehicle manufacturers to avoid liability claims in the event of accidents. We propose a novel approach addressing the problem of specification-compliant motion planning for automated vehicles. Our approach couples set-based reachability analysis with automata-based model checking and outputs specification-compliant driving corridors. These driving corridors serve as motion planning constraints and expedite the generation of trajectories complying with specifications expressed in metric temporal logic. In contrast to existing works, our approach efficiently and exhaustively verifies all driving corridors of an automated vehicle, leveraging mature model checking techniques. We demonstrate the applicability, effectiveness, and efficiency of our approach using various specifications on scenarios from the CommonRoad benchmark suite. Moreover, we benchmark the performance of our prototype against multiple scenarios, indicating that our approach is real-time capable.