ABSTRACT. Machine learning (ML) is increasingly adopted in space missions to enable on-board autonomy under strict constraints on power, compute, and communication. However, the deployment of ML in mission-critical satellite subsystems remains limited by the lack of rigorous verification and validation (V&V) approaches that can provide trust in model behavior under specified conditions. This work presents the study of the formal verification methods for satellite telemetry anomaly detection on the OPS-SAT mission benchmark. Specifically, we formally verify critical properties, scenarios, and robustness of the trained fully-connected neural network model using the pyNeVer and αβCrown libraries. We also discuss key benefits, challenges and limitations pertaining to the potential on-board deployment of formal verification methods in this use case. This integrated approach supports both pre-flight qualification and in-flight monitoring of ML components, aligning with emerging standards for ML assurance in aerospace systems.

ABSTRACT. Creating meaningful interpretations for black-box machine learning models involves balancing two often conflicting objectives: ac- curacy and explainability. Exploring the trade-off between these objec- tives is essential for developing trustworthy interpretations. While many techniques for multi-objective interpretation synthesis have been devel- oped, they typically lack formal guarantees on the Pareto-optimality of the results. Methods that do provide such guarantees, on the other hand, often face severe scalability limitations when exploring the Pareto- optimal space. To address this, we develop a framework based on local optimality guarantees that enables more scalable synthesis of interpre- tations. Specifically, we consider the problem of synthesizing a set of Pareto-optimal interpretations with local optimality guarantees, within the immediate neighborhood of each solution. Our approach begins with a multi-objective learning or search technique, such as Multi-Objective Monte Carlo Tree Search, to generate a best-effort set of Pareto-optimal candidates with respect to accuracy and explainability. We then verify local optimality for each candidate as a Boolean satisfiability problem, which we solve using a SAT solver. We demonstrate the efficacy of our approach on a set of benchmarks, comparing it against previous methods for exploring the Pareto-optimal front of interpretations. In particular, we show that our approach yields interpretations that closely match those synthesized by methods offering global guarantees. This work was accepted at ATVA 2025. We believe that our work and approach potentially has applications in autonomous space vehicles that use complex ML models.

ABSTRACT. We perform uncertainty propagation on an event manifold for Guidance & Control Networks (G&CNETs), aiming to enhance the certification tools for neural networks in this field. This work utilizes three previously solved optimal control problems with varying levels of dynamics nonlinearity and event manifold complexity. The G&CNETs are trained to represent the optimal control policies of a time-optimal interplanetary transfer, a mass-optimal landing on an asteroid and energy-optimal drone racing, respectively. For each of these problems, we describe analytically the terminal conditions on an event manifold with respect to initial state uncertainties. Crucially, this expansion does not depend on time but solely on the initial conditions of the system, thereby making it possible to study the robustness of the G&CNET at any specific stage of a mission defined by the event manifold. Once this analytical expression is found, we provide confidence bounds by applying the Cauchy-Hadamard theorem and perform uncertainty propagation using moment generating functions. While Monte Carlo-based (MC) methods can yield the results we present, this work is driven by the recognition that MC simulations alone may be insufficient for future certification of neural networks in guidance and control applications.

ABSTRACT. The Plan Execution Interchange Language (PLEXIL) is an event-driven synchronous language developed by NASA to support autonomous spacecraft operations. Due to the safety- and mission-critical applications of PLEXIL, its semantics has been formalized and key properties of the language have been formally verified. Two of the properties explored in the formalization are operational determinism, which states that the only source of non-determinism in a PLEXIL execution is the external environment, and run-to-completion, which states that under well-defined assumptions, external events trigger a chain of internal computations that eventually terminate. This paper presents an overview of the formal semantics of the current version of the language, PLEXIL 6.

ABSTRACT. Observation planning is the task of scheduling the operations of a satellite constellation to take pictures of a set of regions of interest and sending these observations down to Earth. With large constellations, uncertain observation conditions, e.g. due to clouds, and limited availability of downstream capacity, it becomes increasingly hard to coordinate the operations. We address the setting where satellites have limited memory, and pictures need to be sent through the constellation to a satellite that can transmit them to a ground station. A key challenge in this problem is the highly dynamic environment, which requires a robust planning system that can quickly adapt to changes. We propose a framework based on facet reasoning, which, unlike traditional planners that provide a single fixed solution, allows for dynamic updates to the current solution without replanning from scratch. We show empirically that facets offer a scalable approach for constellation planning and illustrate the robustness in a case study.

ABSTRACT. Driven by the surmounting interest for dedicated infrastructure in cislunar space, this work considers the satellite constellation design for cislunar space situational awareness (CSSA). We propose a mixed-integer linear programming (MILP)-based formulation that simultaneously tackles the constellation design and sensor-tasking subproblems surrounding CSSA. Our approach generates constellation designs that provide coverage with considerations for the field of view of observers. We propose a time-expanded p-median problem (TE-p-MP) that considers the optimal placement of p space-based observers into discretized locations based on orbital slots along libration point orbits, simultaneously with observer pointing directions across discretized time. We further develop a Lagrangian method for the TE-p -MP, where a relaxed problem with an analytical solution is derived, and customized heuristics leveraging the orbital structure of candidate observer locations are devised. The performance of the proposed formulation is demonstrated with several case studies for CSSA constellations monitoring the cislunar Cone of Shame and a periodic time-varying transit window for low-energy transfers located in the Earth–Moon L2 neck region. The proposed problem formulation, along with the Lagrangian method, is demonstrated to enable a fast assessment of near-optimal CSSA constellations, equipping decision-makers with a critical technique for exploring the design trade space.

ABSTRACT. Space logistics and mission planning are becoming increasingly critical as humankind expands its presence in space. While simulation and analysis tools such as SpaceNet have been widely used to explore feasible architectures, their limited optimization capabilities make it difficult to fully avoid the cost of extensive trade space exploration. This paper presents a new open-source optimization toolbox for space mission planning, developed to automatically formulate and solve or find feasible solutions to mixed-integer nonlinear programs (MINLPs) that integrate discreteness of mission profiles and nonlinearity of systems design. The toolbox is designed for accessibility: users specify mission requirements and parameters, after which the corresponding optimization problem is generated and addressed by a solution approach of the user's choice, including state-of-the-art solvers and built-in heuristic algorithms. Current capabilities include integrated space mission planning and spacecraft design, support for both commercial and open-source mixed-integer solver options, and initial visualization of optimized network flows. The planned extensions focus on interactive visualization, expanded mission domains beyond the Earth–Moon system, and surface logistics integration. This rigorous yet accessible optimization toolbox aims to enable more efficient and optimal mission design processes to support future space exploration.

ABSTRACT. There are a number of types of space mission concepts that feature a single spacecraft visiting multiple targets through its mission. Such “tour” missions are commonly modelled as travelling-salesman problems (TSPs). However, the typical TSP modelling methods are complicated by the fact that the “customers” – the satellites that require servicing, for example – are in orbit, rather than stationary. Previous works resolve this issue either by representing entire orbits as single nodes in the salesman’s – for example, the servicer satellite’s - route, or by expanding orbits into multiple discrete time steps. Both of these methods therefore lose some fidelity in the time dimension, and consequently must make worst-case assumptions about the time-dependent cost of moving between nodes in order to maintain the feasibility of solutions. These worst-case assumptions can be inherently avoided by maintaining the time dimension of the problem as a continuous quantity, as opposed to constructing discrete time windows. Therefore, this paper constructs the Keplerian travelling salesman problem as a time-dependent travelling salesman problem and implements a dynamic programming approach to finding orbital tour schedules with exact, continuous time solutions. We present preliminary results and make comparisons with a state-of-the-art integer programming method.

ABSTRACT. Target selection for large-scale space survey missions requires selecting a scientifically valuable subset from a much larger pool of available targets. This represents a high-stakes combinatorial optimisation problem, since the final sample directly shapes the scientific return of the mission. Current operational approaches mainly rely on heuristic stratified sampling over low-dimensional parameter subspaces. While this paradigm captures key quantities of interest to astronomers, it becomes increasingly limited as the dimensionality and complexity of the planetary feature space grow. More importantly, there is currently no formal evaluation framework for comparing target-selection strategies against scientifically grounded criteria, leaving mission planners without principled tools for assessing representativeness or survey leverage. This problem is particularly relevant for ESA's Ariel mission, which aims to observe approximately 1,000 exoplanets selected from a much larger Mission Candidate Sample (MCS). Ariel will therefore be used in this work as a case study for developing and evaluating target-selection strategies. We propose a multi-objective subset selection framework that formalises target selection as the simultaneous optimisation of three core objectives: distributional similarity to the full candidate catalogue, quantified via the Wasserstein distance; internal subset diversity, maximised over the planetary feature space; and scheduling practicality, subject to mission lifetime and transit window constraints. A key contribution is the evaluation protocol itself, a fair, metric-grounded benchmarking arena for comparing arbitrary selection strategies, which the community currently lacks.