Introduction

RTD-RAX is a Python implementation of Reachability-based Trajectory Design (RTD) augmented with formal reachability verification via immrax.

Source code: github.com/evannsm/rtd-rax

What RTD-RAX Does

Standard RTD computes parameterized Forward Reachable Sets (FRS) offline and uses them online to solve for collision-free trajectory parameters in real time. However, because high-fidelity system models are too expensive to compute reachable sets for, RTD relies on simplified models and must inflate the FRS to account for the resulting tracking error. This introduces conservatism to the planner, meaning that in many scenarios, RTD fails to find a safe trajectory even when one exists. On the other hand, when tracking error is ignored (the noerror variant), the planner has access to more aggressive and safe trajectories, but loses its safety guarantees by failing to account for discrepancies between the simplified model and the true system. Moreover, because offline reachable set computations cannot account for sources of uncertainty and disturbances, for example, unmodeled dynamics and external disturbances such as wind/ice/slippage, etc., RTD's safety guarantees are only as good as the assumptions made in the offline FRS computation, and thus traditional RTD frameworks can only guarantee in negligible disturbance scenarios.

RTD-RAX closes both of these gaps:

1. Plan with the less-conservative noerror FRS to find candidate trajectories.
2. Verify each candidate using immrax interval-arithmetic reachability under the actual uncertainty and disturbance bounds.
3. Repair any candidate flagged as unsafe via speed-backoff and CEGIS-style obstacle buffer tightening, then re-verify.

This produces trajectories that are both less conservative and formally verified safe.

RTD-RAX Gap Case Study With Immrax Verification and Repair

Key Results

1. Safe trajectory planning under a priori unkown disturbances
2. Reduction in conservatism compared to standard RTD, enabling navigation through narrow corridors and around angled obstacles
3. Elimination of needless fail-safe maneuvers in standard RTD
4. Real-time verification and repair of trajectories under measured disturbance bounds
5. Demonstrated on a 4D car model in simulation with multiple case studies

Features

• First fully python implementation of an RTD framework
• Immrax interval-arithmetic reachability verification
• Disturbance-aware verification with measured runtime disturbance bounds
• Repair loop for trajectories flagged as unsafe under real-time disturbance-aware verification
• Fully Dockerized with make command interface
• Open-source implementation with documentation and Docker support and make command interface for easy use and reproducibility

  Documentation Sections

• Installation & Usage
• Case Studies
• API Reference