# Supermartingale Certificates for Parametric MDPs

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 28 of its 52 references that are in the map.
- First posted on arXiv 11 Sep 2026.

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

- [Stability Verification in Stochastic Control Systems via Neural Network Supermartingales](https://mlsanity.com/paper/2112.09495/) (2021)
- [Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees](https://mlsanity.com/paper/2210.05308/) (2022)
- [Parameter Synthesis for Markov Models: Covering the Parameter Space](https://mlsanity.com/paper/1903.07993/) (2019)
- [Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees](https://mlsanity.com/paper/2312.01456/) (2023)
- [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)
- [Stochastic Omega-Regular Verification and Control with Supermartingales](https://mlsanity.com/paper/2405.17304/) (2024)
- [Parameter Synthesis in Markov Models: A Gentle Survey](https://mlsanity.com/paper/2207.06801/) (2022)
- [Termination Analysis of Probabilistic Programs through Positivstellensatz's](https://mlsanity.com/paper/1604.07169/) (2016)
- [Stochastic Invariants for Probabilistic Termination](https://mlsanity.com/paper/1611.01063/) (2016)
- [Convex Optimization for Parameter Synthesis in MDPs](https://mlsanity.com/paper/2107.00108/) (2021)
- [Accelerating Parametric Probabilistic Verification](https://mlsanity.com/paper/1312.3979/) (2013)
- [Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs](https://mlsanity.com/paper/1510.08517/) (2015)
- [Sequential Convex Programming for the Efficient Verification of Parametric MDPs](https://mlsanity.com/paper/1702.00063/) (2017)
- [Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems](https://mlsanity.com/paper/2404.01769/) (2024)
- [Quantitative Supermartingale Certificates](https://mlsanity.com/paper/2504.05065/) (2025)
- [Supermartingale Certificates for Quantitative Omega-regular Verification and Control](https://mlsanity.com/paper/2505.18833/) (2025)
- [Quantitative Verification with Neural Networks](https://mlsanity.com/paper/2301.06136/) (2023)
- [Sound and Complete Proof Rules for Probabilistic Termination](https://mlsanity.com/paper/2404.19724/) (2024)
- [PolyQEnt: A Polynomial Quantified Entailment Solver](https://mlsanity.com/paper/2408.03796/) (2024)
- [Sufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time Systems](https://mlsanity.com/paper/2408.15572/) (2024)
- [A Hierarchy of Supermartingales for ω-Regular Verification](https://mlsanity.com/paper/2512.00270/) (2025)
- [A New Proof Rule for Almost-Sure Termination](https://mlsanity.com/paper/1711.03588/) (2017)
- [On Lexicographic Proof Rules for Probabilistic Termination](https://mlsanity.com/paper/2108.02188/) (2021)
- [Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving](https://mlsanity.com/paper/2307.13160/) (2023)
- [Almost-Sure Safety Guarantees of Stochastic Zero-Control Barrier Functions Do Not Hold](https://mlsanity.com/paper/2312.02430/) (2023)
- [Quantitative Analysis of Assertion Violations in Probabilistic Programs](https://mlsanity.com/paper/2011.14617/) (2020)
- [Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification](https://mlsanity.com/paper/2504.04132/) (2025)

## Abstract (arXiv)

We consider the problems of formal verification and synthesis in parametric Markov decision processes (MDPs) with general measurable state and action spaces. The heart of our approach is a parameter flattening transformation, which allows us to transform parametric MDPs into semantically equivalent non-parametric MDPs. Building on this transformation, we introduce the novel notion of parametric supermartingale certificates, which generalize the traditional supermartingale certificates---used for non-parametric MDPs---to the parametric setting. We use our parametric supermartingale certificates to design algorithms for verification and approximate synthesis in polynomial arithmetic parametric MDPs. This leads to the first verification and synthesis algorithms for parametric MDPs with general state and action spaces. We implement our algorithms and experimentally evaluate them on several continuous parametric random walk benchmarks.