Hamilton--Jacobi Reachability for Spacecraft Collision Avoidance

Technical Summary: Hamilton–Jacobi Reachability for Spacecraft Collision Avoidance

Problem Statement
The rapid expansion of Low-Earth Orbit (LEO) constellations, such as SpaceX's Starlink, challenges existing space traffic management (STM) architectures. Traditional ground-based deconfliction and strategic maneuver planning are insufficient for the scale of future constellations (potentially 42,000 spacecraft). The paper addresses the need for automated, mathematically grounded safety layers to handle collision avoidance between a controlled satellite and an uncooperative or secondary satellite within the same circular orbit. The core challenge is determining when evasive maneuvers must be initiated to guarantee safety despite the unknown intent and bounded disturbances of the uncooperative satellite.

Methodology
The authors propose a formal framework based on Hamilton–Jacobi (HJ) reachability analysis, formulated as a zero-sum differential game.

1. Dynamics and Modeling:

   • Relative motion is modeled in the Radial–Tangential–Normal (RTN) frame using planar Hill–Clohessy–Wiltshire (HCW) dynamics, providing a locally linear approximation of orbital motion.
   • The system state $X = [x, y, \dot{x}, \dot{y}]^\top$ represents tangential and radial positions and velocities.
   • Player 1 (Controlled Satellite): Applies bounded control inputs (accelerations $u$) to avoid collisions.
   • Player 2 (Uncooperative Satellite): Modeled as a bounded adversarial disturbance $d$ with unknown intent, representing worst-case relative acceleration.

2. Hybrid System Architecture:
   The decision-making process is modeled as a hybrid automaton with three discrete modes:

   • $q_{nom}$: Nominal station-keeping or orbiting.
   • $q_{eva}$: Execution of active collision-avoidance maneuvers.
   • $q_{ret}$: Trajectory recovery phase.
     Transitions between these modes are governed by "guard conditions" based on the system's state relative to the Backward Reachable Set (BRS) and safe recovery regions.

3. Reachability Formulation:

   • Target Set ($T$): Defined as the set of unsafe relative configurations violating Federal Communications Commission (FCC) minimum separation standards (a physical collision zone).
   • Backward Reachable Set (BRS): Computed via the Hamilton–Jacobi–Isaacs (HJI) partial differential equation. The BRS characterizes all initial states from which a collision is inevitable under worst-case disturbances, regardless of Player 1's optimal control.
   • Safety Guarantee: States outside the BRS admit provably collision-free trajectories. The boundary of the BRS serves as the critical switching surface; if the system state approaches this boundary, the hybrid automaton triggers a transition to the evasive mode ($q_{eva}$).

4. Control Strategies:

   • Nominal/Recovery: Uses Proportional-Derivative (PD) control laws to drive the satellite to desired relative positions and velocities.
   • Evasive Maneuvers: Four specific escape modes are defined based on RTN geometry:
     1. Positive radial thrust (drifts backward).
     2. Negative radial thrust (accelerates forward).
     3. Pure tangential braking.
     4. Pure tangential acceleration.

Key Contributions

• Formal Safety Framework: The paper integrates HJ reachability with hybrid supervisory control logic to provide rigorous, worst-case safety guarantees for spacecraft collision avoidance.
• Adversarial Modeling: Unlike probabilistic screening methods, this approach treats the uncooperative satellite as a bounded disturbance, ensuring safety even under the most aggressive (within bounds) maneuvers by the other party.
• Hybrid Automaton Design: The authors define a specific switching logic that determines exactly when to abandon nominal operations for evasive maneuvers and when to return to station-keeping, based on the computed reachable sets.
• Scalability Considerations: The framework is designed with decentralized architectures in mind, suitable for individual vehicle-level deconfliction in large constellations.

Results
The authors validated the framework using numerical simulations with a modified Level Set Methods Toolbox.

• Simulation Parameters: The simulations assumed a 500 km LEO orbit, symmetric thrust limits of $\pm 0.1 \, \text{m/s}^2$ for the controlled satellite, and bounded disturbances of $\pm 0.05 \, \text{m/s}^2$ for the uncooperative satellite.
• Verification: The study successfully computed 2D and 3D capture sets and backward reachable tubes. The results demonstrate that the hybrid automaton correctly identifies the switching boundaries between nominal, evasive, and recovery modes.
• Safety Validation: The computed sets confirm that states outside the BRS allow for collision-free trajectories under the defined control laws and disturbance bounds.

Significance and Claims
The paper claims to offer a mathematically rigorous alternative to purely probabilistic collision avoidance methods. By utilizing HJ reachability, the framework provides explicit worst-case safety margins, which is critical for the sustainability of future large-scale satellite constellations. The authors emphasize that their approach enables "provably safe behaviors" and "mathematically grounded supervisory decisions."

The paper remains modest regarding its current scope, noting that:

• The analysis is restricted to planar (2D) HCW dynamics, omitting out-of-plane motion, secular perturbations (like $J_2$), and nonlinear orbital effects.
• The computed reachable sets are formal guarantees specific to the adopted linearized model.
• The current formulation is conservative; it assumes all admissible disturbance realizations are possible, which may overapproximate unsafe states.

Future work identified by the authors includes extending the framework to full 3D relative motion, incorporating more realistic orbital perturbations, and developing scalable approximations (such as decomposition or learned value functions) to address the computational complexity of high-dimensional reachable set calculations.