参数马尔可夫模型的PAC近似与DIRECT优化

中文摘要 AI 辅助

本文研究参数马尔可夫决策过程（pMDPs）的参数综合与优化问题，pMDPs是经典马尔可夫决策过程（MDPs）的扩展，其中精确概率值被参数表达式取代。计算将参数赋值映射到PRCTL性质φ满足度的有理函数f_φ是计算开销极大的任务，尤其是对于最优策略可能在参数空间中变化的pMDPs。本文采用“场景方法”高效综合f_φ的可能近似正确（PAC）近似ApproxFunOfProperty{f}：通过采样参数配置并求解线性规划，得到多项式近似，在指定置信度下，其误差margin保证适用于采样分布下除errorRate分数的参数域外的所有参数。本文进一步展示该PAC框架如何与统计模型检查（SMC）结合，实现黑盒参数模型的分析。基于PAC近似，本文集成DIRECT（DIviding RECTangles）算法，用于参数空间上的无导数全局优化。本文建立条件最优性间隙保证：在显式Lipschitz和PAC良态集假设下，真实最优值f_φ(parameters*)与DIRECT求得的值之差受划分直径项约束，在PAC情形下还受额外近似误差项约束。对2997个基准的实证评估聚焦于新的基于DIRECT的优化组件，结果显示DIRECT变体解决的实例数少于场景优化器，但在两者共同成功的实例中，DIRECT变体通常返回略优的目标值且运行更快，同时保持在PAC误差margin内接近场景值。

英文摘要

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.

发表机构

• Key Laboratory of System Software (Chinese Academy of Sciences)（中国科学院系统软件重点实验室）
• Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）
• University of Chinese Academy of Sciences（中国科学院大学）
• Institute of Optics and Electronics, Chinese Academy of Sciences（中国科学院光电技术研究所）
• Institute of Intelligent Software Guangzhou（广州智能软件研究所）

机构由 AI 辅助整理，请以论文原文为准。