Set-based computation of vehicle behaviors for the online verification of autonomous vehicles

We compute the set of all possible behaviors of an autonomous vehicle using reachability analysis. A reachable set is the set of states a system can reach for a given set of initial states, disturbances, and sensor noise values. We consider autonomous vehicles which plan trajectories for a certain look-ahead horizon which are followed using feedback control. While a perfectly followed trajectory might not violate specified safety properties (e.g. lane departures or vehicle collisions), a violating deviation from the planned trajectory might exist. Given the mathematical model of the controlled vehicle and bounds on uncertainty, our approach detects any possible violation. In addition, the approach provides results faster than the time required to finish the planned maneuvers of the autonomous vehicle.