Anytime Safety Verification of Autonomous Vehicles

We propose a procedure to formally verify the safety of autonomous vehicles online, i.e., during operation, that considers the uniqueness of each traffic situation. A challenging aspect of online verification is the varying number of surrounding traffic participants, which causes significant variations in computational demand. To guarantee timely safe motion plans, we propose an anytime approach that provides rapid conservative verification results based on coarse model abstractions, which are refined continually if computation time is available. Reachability analysis, which over-approximates all possible behaviors of other traffic participants, is performed for each abstraction. We demonstrate the usefulness of the proposed procedure using the CommonRoad benchmark suite.