为参数化马尔可夫模型设计高效近似与优化方法,兼顾精度与速度。
PAC Approximation and DIRECT Optimization for Parametric Markov Models

- 基于采样和线性规划,构建满足概率保证的近似函数。
- 在2997个基准上验证,该方法比传统优化更快且结果更优。
- 适用于黑箱模型分析,特别适合参数空间大、计算成本高的场景。
本文研究参数化马尔可夫决策过程(pMDPs)的参数合成与优化问题,其中精确概率被参数表达式替代。计算将参数取值映射到PRCTL性质满足度的有理函数 $f_{s}$ 是高复杂度任务,尤其当最优策略在参数空间中变化时。本文采用情景方法,通过采样参数配置并求解线性规划,获得多项式近似 $ ilde{f}_{s}$,其误差边界 $ heta$ 在指定置信度下对超过 $1-eta$ 比例的参数域成立。进一步将此框架与统计模型检测(SMC)结合,支持黑箱模型分析。在此近似基础上,引入无需导数的全局优化算法DIRECT,建立条件最优间隙保证:在显式Lipschitz和PAC好集假设下,真实最优值与DIRECT所得值之差受划分直径项和附加近似误差项控制。2997个基准的实证评估聚焦于新的DIRECT优化组件,结果显示:尽管DIRECT求解实例数少于情景优化器,但在共同成功实例上常获稍优目标值,且运行更快,同时保持在PAC误差范围内。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。