In this paper, we propose an approximating framework for analyzing parametric Markov models. Instead of computing complex rational functions encoding the reachability probability and the reward values of the parametric model, we exploit the scenario approach to synthesize a relatively simple polynomial approximation. The approximation is probably approximately correct (PAC), meaning that with high confidence, the approximating function is close to the actual function with an allowable error. With the PAC approximations, one can check properties of the parametric Markov models. We show that the scenario approach can also be used to check PRCTL properties directly, without synthesizing the polynomial at first hand. We have implemented our algorithm in a prototype tool and conducted thorough experiments. The experimental results demonstrate that our tool is able to compute polynomials for more benchmarks than state of the art tools such as PRISM and Storm, confirming the efficacy of our PAC-based synthesis.

翻译：本文提出了一种用于分析参数化马尔可夫模型的近似框架。我们无需计算编码参数化模型可达概率与奖励值的复杂有理函数，而是利用场景方法综合出相对简单的多项式近似。该近似具有概率近似正确（PAC）性质，即在高置信度下，近似函数与真实函数的误差在允许范围内。基于PAC近似，可对参数化马尔可夫模型的属性进行验证。我们进一步证明，场景方法无需预先合成多项式，便可直接用于验证PRCTL属性。我们在原型工具中实现了该算法并进行了充分实验。实验结果表明，与PRISM、Storm等现有先进工具相比，本工具能为更多基准模型计算多项式，验证了基于PAC综合方法的有效性。