Ensuring drivability of planned motions using formal methods

Motion planning of automated vehicles requires dynamical models to ensure that obtained trajectories are drivable. An often overlooked aspect is that motion planning is usually done using simplified models, which do not always sufficiently conform to the real behavior of vehicles. Thus, collision avoidance and drivability is not necessarily ensured. We address this problem by modeling vehicles as differential inclusions composed of simple dynamics and set-based uncertainty; conformance testing is used to determine the required uncertainty. To quickly provide the set of solutions for these uncertain models, we use pre-computed reachable sets (i.e., the union of all possible solutions) for pre-selected motion primitives. The reachable sets of vehicles are obtained through the novel combination of optimization techniques and reachability analysis in the controller synthesis - they enable us to guarantee safety by checking their mutual non-intersection for consecutive time intervals. The benefits of our approach are demonstrated by numerical experiments.