AI summaryⓘ
The authors study parametric Markov decision processes (pMDPs) where probabilities depend on unknown parameters. They aim to approximate how well certain properties hold across different parameter values, which is usually computationally hard. Using a scenario approach, they create a probably approximately correct (PAC) polynomial approximation with guaranteed error bounds for most parameters. They combine this with statistical model checking and use the DIRECT optimization algorithm to find parameter settings that maximize the property, providing bounds on how close the found solutions are to the true optimum. Their experiments on many benchmarks show that the DIRECT method is often faster and finds similarly good or better solutions than previous approaches within the guaranteed error margin.
parametric Markov decision processPRCTL propertyscenario approachprobably approximately correct (PAC)statistical model checkingDIRECT algorithmglobal optimizationLipschitz continuitypolicy optimizationapproximation error
Authors
Zhiming Chi, Ying Liu, Andrea Turrini, Lijun Zhang, David N. Jansen
Abstract
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 $f_{\lsf}$ 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 \emph{scenario approach} to efficiently synthesize a probably approximately correct (PAC) approximation $\ApproxFunOfProperty{f}$ of $f_{\lsf}$: 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 $f_{\lsf}(\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.