Traffic-Rule-Compliant Trajectory Repair via Satisfiability Modulo Theories and Reachability Analysis
Abstract
Complying with traffic rules is challenging for automated vehicles, as numerous rules need to be considered simultaneously. If a planned trajectory violates traffic rules, it is common to replan a new trajectory from scratch. We instead propose a trajectory repair technique to save computation time. By coupling satisfiability modulo theories with set-based reachability analysis, we determine if and in what manner the initial trajectory can be repaired. Experiments in high-fidelity simulators and in the real world demonstrate the benefits of our proposed approach in various scenarios. Even in complex environments with intricate rules, we efficiently and reliably repair rule-violating trajectories, enabling automated vehicles to swiftly resume legally safe operation in real time.
Related Papers
- → SMT-COMP: Satisfiability Modulo Theories Competition(2005)97 cited
- Linear arithmetic satisfiability via strategy improvement(2016)
- → Goal-Directed Invariant Synthesis for Model Checking Modulo Theories(2009)14 cited
- → Unification Modulo Builtins(2018)5 cited
- Solving quantified first order formulas in Satisfiability Modulo Theories(2010)