PAC Approximation and DIRECT Optimization for Parametric Markov Models

This paper studies parameter synthesis and optimization for parametric Markov decision processes, where transition probabilities are parametric expressions and optimal policies can vary across the parameter space. It uses a scenario approach to construct a polynomial PAC approximation of a PRCTL satisfaction-value function from sampled configurations and linear programs, and combines the framework with statistical model checking for black-box models. The authors integrate DIRECT, a derivative-free global optimizer, and derive conditional optimality-gap bounds under explicit Lipschitz and PAC-good-set assumptions. Evaluation on 2,997 benchmarks reports fewer solved instances for DIRECT variants than for the scenario optimizer, but better objective values and usually faster runtimes on shared successes.