# Robust Almost-Sure Reachability in Multi-Environment MDPs

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Jan 2023.

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

- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [Multi-Environment POMDPs: Discrete Model Uncertainty Under Partial Observability](https://mlsanity.com/paper/2510.23744/) (2025)
- [Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking](https://mlsanity.com/paper/2511.08078/) (2025)
- [Multi-Environment POMDPs with Finite-Horizon Objectives](https://mlsanity.com/paper/2605.07537/) (2026)
- [On the Complexity Gap Between POMDPs and Multi-Environment POMDPs](https://mlsanity.com/paper/2610.15010/) (2026)

## Abstract (arXiv)

Multiple-environment MDPs (MEMDPs) capture finite sets of MDPs that share the states but differ in the transition dynamics. These models form a proper subclass of partially observable MDPs (POMDPs). We consider the synthesis of policies that robustly satisfy an almost-sure reachability property in MEMDPs, that is, one policy that satisfies a property for all environments. For POMDPs, deciding the existence of robust policies is an EXPTIME-complete problem. In this paper, we show that this problem is PSPACE-complete for MEMDPs, while the policies in general require exponential memory. We exploit the theoretical results to develop and implement an algorithm that shows promising results in synthesizing robust policies for various benchmarks.