# 1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 49 references that are in the map.
- First posted on arXiv 23 Oct 2024.

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

- [Omega-Regular Objectives in Model-Free Reinforcement Learning](https://mlsanity.com/paper/1810.00950/) (2018)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Verification of Markov Decision Processes using Learning Algorithms](https://mlsanity.com/paper/1402.2967/) (2014)
- [dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts](https://mlsanity.com/paper/2101.07202/) (2021)
- [Of Cores: A Partial-Exploration Framework for Markov Decision Processes](https://mlsanity.com/paper/1906.06931/) (2019)
- [Smart Sampling for Lightweight Verification of Markov Decision Processes](https://mlsanity.com/paper/1409.2116/) (2014)
- [Explicit Model Checking of Very Large MDP using Partitioning and Secondary Storage](https://mlsanity.com/paper/1504.02861/) (2015)
- [Scalable Verification of Probabilistic Networks](https://mlsanity.com/paper/1904.08096/) (2019)

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

- [Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC](https://mlsanity.com/paper/2602.14505/) (2026)
- [COOL-MC: Verifying and Explaining RL Policies for Platelet Inventory Management](https://mlsanity.com/paper/2603.02396/) (2026)
- [Explainably Safe Reinforcement Learning](https://mlsanity.com/paper/2606.04634/) (2026)
- [dtControl2+varepsilon: Trading Optimality for Explainability in MDPs via Decision Trees](https://mlsanity.com/paper/2607.25925/) (2026)
- [Bellman-Certified Rounding for Sparse Policy Deployment in MDPs](https://mlsanity.com/paper/2610.00325/) (2026)

## Abstract (arXiv)

Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when instantiating parameterized Markov decision processes (MDPs) even with moderate values. Synthesizing policies for such huge MDPs is beyond the reach of available tools. We propose a learning-based approach to obtain a reasonable policy for such huge MDPs. The idea is to generalize optimal policies obtained by model-checking small instances to larger ones using decision-tree learning. Consequently, our method bypasses the need for explicit state-space exploration of large models, providing a practical solution to the state-space explosion problem. We demonstrate the efficacy of our approach by performing extensive experimentation on the relevant models from the quantitative verification benchmark set. The experimental results indicate that our policies perform well, even when the size of the model is orders of magnitude beyond the reach of state-of-the-art analysis tools.