# Sequential Convex Programming for the Efficient Verification of Parametric MDPs

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

## Key facts

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

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

- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [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)
- [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)
- [Supermartingale Certificates for Parametric MDPs](https://mlsanity.com/paper/2609.12715/) (2026)

## Abstract (arXiv)

Multi-objective verification problems of parametric Markov decision processes under optimality criteria can be naturally expressed as nonlinear programs. We observe that many of these computationally demanding problems belong to the subclass of signomial programs. This insight allows for a sequential optimization algorithm to efficiently compute sound but possibly suboptimal solutions. Each stage of this algorithm solves a geometric programming problem. These geometric programs are obtained by convexifying the nonconvex constraints of the original problem. Direct applications of the encodings as nonlinear pro- grams are model repair and parameter synthesis. We demonstrate the scalability and quality of our approach by well-known benchmarks