Verifiable Mission Planning For Space Operations

As space missions become more complex, planning methods must maximize mission performance while rigorously enforcing safety. We develop a probabilistic approach based on a finite-horizon Markov decision process to optimize spacecraft operations planning with safety guarantees. In the model, states capture essential mission parameters, and actions represent the operational adjustments needed to meet mission objectives. By directly incorporating uncertainties from environmental conditions and spacecraft dynamics, an optimal sequence of actions is computed that maximizes expected rewards and strictly enforces safety constraints. Numerical experiments on the GRACE-FO mission demonstrate robust performance under uncertainties while providing probabilistic safety guarantees, offering a reliable solution for autonomous spacecraft operations.