PAC Approximation and DIRECT Optimization for Parametric Markov Models

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.