# Synthesis in pMDPs: A Tale of 1001 Parameters

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

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Mar 2018.

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

- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [Verifiable and Compositional Reinforcement Learning Systems](https://mlsanity.com/paper/2106.05864/) (2021)
- [Convex Optimization for Parameter Synthesis in MDPs](https://mlsanity.com/paper/2107.00108/) (2021)
- [Fine-Tuning the Odds in Bayesian Networks](https://mlsanity.com/paper/2105.14371/) (2021)
- [Verifiable Reinforcement Learning Systems via Compositionality](https://mlsanity.com/paper/2309.06420/) (2023)
- [What should be observed for optimal reward in POMDPs?](https://mlsanity.com/paper/2405.10768/) (2024)
- [Counterfactual Strategies for Markov Decision Processes](https://mlsanity.com/paper/2505.09412/) (2025)
- [Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems](https://mlsanity.com/paper/2110.02125/) (2021)
- [Finding an ε-close Variation of Parameters in Bayesian Networks](https://mlsanity.com/paper/2305.10051/) (2023)
- [A Multifidelity Sim-to-Real Pipeline for Verifiable and Compositional Reinforcement Learning](https://mlsanity.com/paper/2312.01249/) (2023)

## Abstract (arXiv)

This paper considers parametric Markov decision processes (pMDPs) whose transitions are equipped with affine functions over a finite set of parameters. The synthesis problem is to find a parameter valuation such that the instantiated pMDP satisfies a specification under all strategies. We show that this problem can be formulated as a quadratically-constrained quadratic program (QCQP) and is non-convex in general. To deal with the NP-hardness of such problems, we exploit a convex-concave procedure (CCP) to iteratively obtain local optima. An appropriate interplay between CCP solvers and probabilistic model checkers creates a procedure --- realized in the open-source tool PROPhESY --- that solves the synthesis problem for models with thousands of parameters.