Explainable and Scalable Planning with Probabilistic Temporal Logic Specifications

Human spaceflight operations challenge currently available planning technology. They typically rely on a large number of integrated functions including mission planning, crew planning, solar array management, power and thermal management and system health monitoring. These functions serve under heterogeneous uncertainties (stemming from anomalies and faults in equipment and intrinsic unknowns about the environment), time-varying requirements and multiple, possibly competing objectives. Co-work with the crew introduces unique difficulties as well. Humans’ capabilities and limitations in these capabilities add to the uncertainties. Humans’ preferences and need for compatibility between the humans and autonomous control protocols introduce unconventional constraints. The emphasis of this project is particularly on unambiguous, formal specifications and compilation of executable control software with provable guarantees and systematic sensitivity analysis diffuses the critical concern of reliability throughout the planning execution loop. The resulting algorithms incorporate models with stochastic as well as nondeterministic uncertainties and rich specifications with temporal and logical relations as well as probabilistic and real-time modalities as needed. Integrated planning for the coupled functions introduces possibilities for system-level optimization, e.g., in performance, weights and overall cost. Finally, the algorithms improve not only the scalability of the resulting synthesis algorithms but also their interpretability by and explainability to the crew and designers. The project developed theory, algorithms and case studies for formal specifications and automated synthesis of policies for autonomous decision-making in mission, resource and contingency management. The work has evolved in three main streams. The first stream focused on policy synthesis under probabilistic uncertainties captured by (parametric or uncertain) Markov decision processes, policy synthesis in so-called structured Markov decision processes, and generation of explainable policies and/or counterexamples in Markov decision processes. The second one focused on generation of schedules and explanations of core reasons for the lack of feasible schedules based on SAT and SMT encodings. Additionally, we developed algorithms for maximum realizability based on similar encodings. The third stream was on developing and demonstrating the algorithmic advances of the project on a case study relevant for planning for human space missions with salient specifications, requirements and practices for planning of the activities on the International Space Center.