PAC Approximation and DIRECT Optimization for Parametric Markov Models

A new paper on arXiv (2608.02184) introduces a method for parameter synthesis and optimization in parametric Markov decision processes (pMDPs), which extend classical MDPs by replacing exact probabilities with parametric expressions. The authors address the computational challenge of computing the rational function that maps parameter valuations to satisfaction values of a PRCTL property. They employ the scenario approach to efficiently synthesize a probably approximately correct (PAC) approximation of this function. By sampling parameter configurations and solving a linear program, they obtain a polynomial approximation with a guaranteed error margin for all but a small fraction of the parameter domain under the sampling distribution. The paper further demonstrates how this PAC framework can be integrated with DIRECT optimization, a global optimization algorithm, to solve the parameter synthesis problem. The work is relevant to formal verification and probabilistic model checking, offering a scalable approach for systems with parametric uncertainties.