Formally Guaranteed Tight Dynamic Future Occupancy of Autonomous Vehicles

Autonomous Vehicles (AVs) must be able to navigate complex traffic environments without collisions with other traffic participants. Formal methods can be used to guarantee collision avoidance by using reachability analysis techniques to verify if a planned trajectory is safe or unsafe. To prevent the formal collision avoidance system from being overly conservative, a tight reachable set of the AV must be calculated. Computing the tight reachable set of an AV is a difficult and computationally expensive process. Motion primitives are used to provide tight dynamic future occupancy of autonomous systems. Motion primitives are short segments of trajectories that are precomputed along with their reachable sets. By replacing a reference trajectory with a sequence of motion primitives, the computational requirements during vehicle operation can be greatly reduced. In this paper, we provide a treatment on motion primitives, and develop an algorithm to match motion primitives to a reference trajectory in a computationally efficient manner.