# Verifiable Mission Planning For Space Operations

arXiv: https://arxiv.org/abs/2504.11631 · HTML: https://mlsanity.com/paper/2504.11631/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Apr 2025.

## Built on by (most cited first, 1 of 1)

- [Trojan horse hunt in deep forecasting models: Insights from the European Space Agency competition](https://mlsanity.com/paper/2603.20108/) (2026)

## Abstract (arXiv)

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.