Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Traffic-Rule-Compliant Trajectory Repair via Satisfiability Modulo Theories and Reachability Analysis

Yuanfei Lin, Zekun Xing, Xuyuan Han, Matthias Althoff

TL;DR

The paper tackles the problem of ensuring traffic-rule compliance in automated driving without resorting to full trajectory replanning. It introduces a trajectory repair framework that couples satisfiability modulo theories (SMT) with set-based reachability, augmented by model predictive robustness (MPR) to guide the SAT solver and a cutting-edge T-solver that computes a specification-compliant repaired trajectory. Key contributions include offline propositional abstraction of STL rules, lazy SMT solving, specification-compliant reachable-set computations, and convex optimization-based trajectory repair, validated across extensive simulations (CARLA/CommonRoad) and real-world deployments. The approach yields real-time repair capabilities in complex rule sets, improves safety and predictability, and demonstrates substantial speedups over traditional replanning methods while maintaining high success rates.

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.

Traffic-Rule-Compliant Trajectory Repair via Satisfiability Modulo Theories and Reachability Analysis

TL;DR

The paper tackles the problem of ensuring traffic-rule compliance in automated driving without resorting to full trajectory replanning. It introduces a trajectory repair framework that couples satisfiability modulo theories (SMT) with set-based reachability, augmented by model predictive robustness (MPR) to guide the SAT solver and a cutting-edge T-solver that computes a specification-compliant repaired trajectory. Key contributions include offline propositional abstraction of STL rules, lazy SMT solving, specification-compliant reachable-set computations, and convex optimization-based trajectory repair, validated across extensive simulations (CARLA/CommonRoad) and real-world deployments. The approach yields real-time repair capabilities in complex rule sets, improves safety and predictability, and demonstrates substantial speedups over traditional replanning methods while maintaining high success rates.

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.

Paper Structure

This paper contains 52 sections, 24 equations, 16 figures, 6 tables.

Table of Contents

  1. Introduction
  2. Literature Overview
  3. Rule-Informed Motion Planning
  4. Trajectory Replanning
  5. Trajectory Repair
  6. Local Trajectory Repair
  7. Branching Off From Trajectories
  8. Contributions and Outline
  9. Preliminaries and Problem Statement
  10. System Description and Notations
  11. Signal Temporal Logic
  12. Definitions for Trajectory Repair
  13. Problem Formulation
  14. Overview of the Trajectory Repair Approach
  15. Propositional Traffic Rule Abstraction
  16. ...and 37 more sections

Figures (16)

  • Figure 1: Snapshot from our real-world driving experiments. Our trajectory repair approach dynamically adjusts planned trajectories that violate traffic rules in real time. For example, it enforces the stop-line rule by requiring the vehicle to halt before the marked line for the specified duration. The motion plans are illustrated by widening the path to be followed for improved visibility and are referenced to the rear axle. The project site, including code and experiment animations, is available at https://commonroad.github.io/repair-to-drive/.
  • Figure 2: Vehicle localization in a curvilinear coordinate system defined with respect to the reference path $\Gamma$, which represents the centerline of $\mathcal{L}_{\mathtt{dir}}$.
  • Figure 3: Example computations of $\mathtt{TV}_{\varphi}$. A circle represents a state, with its marking indicating whether the formula is satisfied or violated. For evaluating $\mathbf{G}_{[0, 5]}(\varphi_1\lor\varphi_2)$, we have $\mathtt{TV}_{\varphi_1\lor\varphi_2} (\boldsymbol{u}_{[0,h-1]}, k')=\infty$ for all $k'>4$.
  • Figure 4: Trajectory repair flowchart for a given nominal planner.
  • Figure 5: Computation of model predictive robustness. (a) illustrates the computation scheme for predicates $p_1$, $p_2$, etc., in both offline and online modes. (b) displays the trajectory sampling results, where the states are labeled according to the predicate $\mathrm{stop\_line\_in\_front}(\boldsymbol{x}_{\mathtt{ego}})$. (c) presents selected feature variables relevant to intersections.
  • ...and 11 more figures

Theorems & Definitions (5)

  • Definition 1: STL Robustness donze2010robust
  • Definition 2: Time-To-Violation yuanfei2022
  • Definition 3: Time-To-Comply yuanfei2022
  • Definition 4: Specification-Compliant Reachable Sets lercher2024specification
  • Remark 1