Verifiable Mission Planning For Space Operations

TL;DR

This work reframes spacecraft mission planning under environmental and actuator uncertainty as a finite-horizon, chance-constrained MDP with reach-avoid safety specifications. It provides a two-step solution: first synthesize an unconstrained policy via backward induction on the MDP, then verify and enforce safety probabilistically through a dedicated value function and temporal-logic formulation. The GRACE-FO case study demonstrates how altitude, fuel, and maneuver-spacing constraints can be integrated with stochastic space-weather effects to yield policies that maximize mission return while provably satisfying safety requirements. The results support autonomous, formally certified decision-making for long-duration space operations and outline a path toward higher-fidelity validation with orbital simulators.

Abstract

Spacecraft must operate under environmental and actuator uncertainties while meeting strict safety requirements. Traditional approaches rely on scenario-based heuristics that fail to account for stochastic influences, leading to suboptimal or unsafe plans. We propose a finite-horizon, chance-constrained Markov decision process for mission planning, where states represent mission and vehicle parameters, actions correspond to operational adjustments, and temporal logic specifications encode operational reach-avoid constraints. We synthesize policies that optimize mission objectives while ensuring constraints are met with high probability. Applied to the GRACE-FO mission, the approach accounts for stochastic solar activity and uncertain thrust performance, yielding maneuver schedules that maximize scientific return and provably satisfy safety requirements. We demonstrate how Markov decision processes can be applied to space missions, enabling autonomous operation with formal guarantees.

Figures (9)

• Figure 1: A visualization of a simple finite-horizon MDP with horizon length $H$. The set of states is $\mathcal{S}=\{ s_{1} , s_{2} \}$
• Figure 2: Visualization of the Keplerian orbital elements.
• Figure 3: We construct the discrete representation of the mission environment by sampling a representative set of mean orbits.
• Figure 4: Visualization for the shaping of the reward function $R$.
• Figure 5: Visualization of the set of feasible actions $\mathcal{A}$, which correspond to different instantaneous altitude gains.