Verifiable Mission Planning For Space Operations

Quentin Rommel, Michael Hibbard, Pavan Shukla, Himanshu Save, Srinivas Bettadpur, Ufuk Topcu

Published: 2025/4/15

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 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. This work demonstrates how Markov decision processes can be applied to space missions, enabling autonomous operation with formal guarantees.

Verifiable Mission Planning For Space Operations | SummarXiv | SummarXiv