# PAC Approximation and DIRECT Optimization for Parametric Markov Models

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 12 of its 47 references that are in the map.
- First posted on arXiv 3 Aug 2026.

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

- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Parameter Synthesis for Markov Models: Faster Than Ever](https://mlsanity.com/paper/1602.05113/) (2016)
- [Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning](https://mlsanity.com/paper/2101.10102/) (2021)
- [Parametric Markov Chains: PCTL Complexity and Fraction-free Gaussian Elimination](https://mlsanity.com/paper/1709.02093/) (2017)
- [The Complexity of Reachability in Parametric Markov Decision Processes](https://mlsanity.com/paper/2009.13128/) (2020)
- [Parameter Synthesis in Markov Models: A Gentle Survey](https://mlsanity.com/paper/2207.06801/) (2022)
- [PAC Model Checking of Black-Box Continuous-Time Dynamical Systems](https://mlsanity.com/paper/2007.10141/) (2020)
- [Scenario-Based Verification of Uncertain Parametric MDPs](https://mlsanity.com/paper/2112.13020/) (2021)
- [Accelerating Parametric Probabilistic Verification](https://mlsanity.com/paper/1312.3979/) (2013)
- [Fast Parametric Model Checking through Model Fragmentation](https://mlsanity.com/paper/2102.01490/) (2021)
- [Accelerated Model Checking of Parametric Markov Chains](https://mlsanity.com/paper/1805.05672/) (2018)
- [Scenario Approach for Parametric Markov Models](https://mlsanity.com/paper/2304.08330/) (2023)

## Abstract (arXiv)

In this paper, we consider the parameter synthesis and optimization problem for parametric Markov decision processes (pMDPs), the extension of classical MDPs where exact probability values are replaced by parametric expressions. Computing the rational function flsf that maps parameter valuations to the satisfaction value of a PRCTL property lsf is a computationally expensive task, particularly for pMDPs where the optimal policy may vary across the parameter space. We adopt the scenario approach to efficiently synthesize a probably approximately correct (PAC) approximation ApproxFunOfPropertyf of flsf: by sampling parameter configurations and solving a linear program, we obtain a polynomial approximation whose error margin margin is guaranteed, with prescribed confidence, for all but an errorRate-fraction of the parameter domain under the sampling distribution. We further show how this PAC framework can be combined with statistical model checking (SMC), enabling the analysis of black-box parametric models. Building on the PAC approximation, we integrate the DIRECT (DIviding RECTangles) algorithm for derivative-free global optimization over the parameter space. We establish conditional optimality-gap guarantees: under explicit Lipschitz and PAC-good-set assumptions, the difference between the true optimum flsf(parameters*) and the value found by DIRECT is bounded by a partition-diameter term and, in the PAC case, an additional approximation-error term. An empirical evaluation on 2997 benchmarks focuses on the new DIRECT-based optimization component. The results show that DIRECT variants solve fewer instances than the scenario optimizer, but on their common successful instances they often return slightly better objective values and usually run faster, while remaining close to the scenario values within the PAC margin.