# Convex Optimization for Parameter Synthesis in MDPs

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 68 references that are in the map.
- First posted on arXiv 30 Jun 2021.

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

- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)
- [Robust Finite-State Controllers for Uncertain POMDPs](https://mlsanity.com/paper/2009.11459/) (2020)
- [Convergence guarantees for a class of non-convex and non-smooth optimization problems](https://mlsanity.com/paper/1804.09629/) (2018)
- [Parameter Synthesis for Markov Models: Covering the Parameter Space](https://mlsanity.com/paper/1903.07993/) (2019)
- [Parameter Synthesis for Markov Models: Faster Than Ever](https://mlsanity.com/paper/1602.05113/) (2016)
- [Parametric Markov Chains: PCTL Complexity and Fraction-free Gaussian Elimination](https://mlsanity.com/paper/1709.02093/) (2017)
- [Majorization-minimization procedures and convergence of SQP methods for semi-algebraic and tame programs](https://mlsanity.com/paper/1409.8147/) (2014)
- [Synthesis in pMDPs: A Tale of 1001 Parameters](https://mlsanity.com/paper/1803.02884/) (2018)
- [The Complexity of Reachability in Parametric Markov Decision Processes](https://mlsanity.com/paper/2009.13128/) (2020)
- [Successive Convexification: A Superlinearly Convergent Algorithm for Non-convex Optimal Control Problems](https://mlsanity.com/paper/1804.06539/) (2018)
- [Sequential Convex Programming for the Efficient Verification of Parametric MDPs](https://mlsanity.com/paper/1702.00063/) (2017)
- [Are Parametric Markov Chains Monotonic?](https://mlsanity.com/paper/1907.08491/) (2019)
- [Scenario-Based Verification of Uncertain MDPs](https://mlsanity.com/paper/1912.11223/) (2019)
- [Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes](https://mlsanity.com/paper/1706.06875/) (2017)
- [Permissive Finite-State Controllers of POMDPs using Parameter Synthesis](https://mlsanity.com/paper/1710.10294/) (2017)
- [Constrained Spacecraft Relative Motion Planning Exploiting Periodic Natural Motion Trajectories and Invariance](https://mlsanity.com/paper/1703.06313/) (2017)
- [On the Complexity of Reachability in Parametric Markov Decision Processes](https://mlsanity.com/paper/1904.01503/) (2019)

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

- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [Interval Markov Decision Processes with Continuous Action-Spaces](https://mlsanity.com/paper/2211.01231/) (2022)
- [Efficient Sensitivity Analysis for Parametric Robust Markov Chains](https://mlsanity.com/paper/2305.01473/) (2023)
- [Counterfactual Strategies for Markov Decision Processes](https://mlsanity.com/paper/2505.09412/) (2025)
- [Robust Parameter Learning for Uncertain MDPs](https://mlsanity.com/paper/2605.01339/) (2026)
- [Finding an ε-close Variation of Parameters in Bayesian Networks](https://mlsanity.com/paper/2305.10051/) (2023)
- [Robustness Analysis of POMDP Policies to Observation Perturbations](https://mlsanity.com/paper/2604.21256/) (2026)
- [Supermartingale Certificates for Parametric MDPs](https://mlsanity.com/paper/2609.12715/) (2026)

## Abstract (arXiv)

Probabilistic model checking aims to prove whether a Markov decision process (MDP) satisfies a temporal logic specification. The underlying methods rely on an often unrealistic assumption that the MDP is precisely known. Consequently, parametric MDPs (pMDPs) extend MDPs with transition probabilities that are functions over unspecified parameters. The parameter synthesis problem is to compute an instantiation of these unspecified parameters such that the resulting MDP satisfies the temporal logic specification. We formulate the parameter synthesis problem as a quadratically constrained quadratic program (QCQP), which is nonconvex and is NP-hard to solve in general. We develop two approaches that iteratively obtain locally optimal solutions. The first approach exploits the so-called convex-concave procedure (CCP), and the second approach utilizes a sequential convex programming (SCP) method. The techniques improve the runtime and scalability by multiple orders of magnitude compared to black-box CCP and SCP by merging ideas from convex optimization and probabilistic model checking. We demonstrate the approaches on a satellite collision avoidance problem with hundreds of thousands of states and tens of thousands of parameters and their scalability on a wide range of commonly used benchmarks.