# Accelerating Policy Synthesis in Large-Scale MDPs via Hierarchical Adaptive Refinement

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 59 references that are in the map.
- First posted on arXiv 21 Jun 2025.

## Builds on (most cited first, 10 of 10)

- [AI Safety Gridworlds](https://mlsanity.com/paper/1711.09883/) (2017)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Probabilistic Model Checking of Robots Deployed in Extreme Environments](https://mlsanity.com/paper/1812.04128/) (2018)
- [Abstract Value Iteration for Hierarchical Reinforcement Learning](https://mlsanity.com/paper/2010.15638/) (2020)
- [Uncertainty in Self-Adaptive Systems: A Research Community Perspective](https://mlsanity.com/paper/2103.02717/) (2021)
- [Abstraction-Refinement for Hierarchical Probabilistic Models](https://mlsanity.com/paper/2206.02653/) (2022)
- [Compositional Probabilistic Model Checking with String Diagrams of MDPs](https://mlsanity.com/paper/2307.08765/) (2023)
- [Explicit Model Checking of Very Large MDP using Partitioning and Secondary Storage](https://mlsanity.com/paper/1504.02861/) (2015)
- [Controller Synthesis for Omega-Regular and Steady-State Specifications](https://mlsanity.com/paper/2106.02951/) (2021)
- [MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints](https://mlsanity.com/paper/2305.16752/) (2023)

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

- [Leveraging System-Level Observations to Inform Bayesian Learning of Model Parameters for Quantitative Verification](https://mlsanity.com/paper/2608.03489/) (2026)

## Abstract (arXiv)

Software-intensive systems, such as software product lines and robotics, utilise Markov decision processes (MDPs) to capture uncertainty and analyse sequential decision-making problems. Despite the usefulness of conventional policy synthesis methods, they fail to scale to large state spaces. Our approach addresses this issue and accelerates policy synthesis in large MDPs by dynamically refining the MDP and iteratively selecting the most fragile MDP regions for refinement. This iterative procedure offers a balance between accuracy and efficiency, as refinement occurs only when necessary. We formally show that the composed policy is near-optimal under standard assumptions, with error bounded by the local solver tolerance and boundary mismatch. Across diverse case studies and MDPs up to 1M states, we demonstrate that our approach achieves up to 2× speedup over PRISM, offering a competitive solution for real-world policy synthesis in large MDPs.