This C++ was used for the formal verification of planned trajectories of an automated vehicle developed at Carnegie Mellon University, USA (CMU's Autonomous Car
). The algorithm computed the reachable set of a vehicle model in order to determine the future occupancy considering measurement noise, disturbances, and model inaccuracies. Given occupancies of obstacles and the road boundaries, it can be verified whether the vehicle can possibly crash within a user-defined time horizon. For the verification of infinite time horizons the trajectory planner has to attach maneuvers that bring the vehicle to a stop.
- Kartik Gupta
- Alok Sharma
- Matthias Althoff