Efficient computation of exact solutions for quantitative model checking
Efficient computation of exact solutions for quantitative model checking
复制标题
有效计算定量模型检查的精确解
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Sergio Giro
中科院分区：
文献类型：
--
作者：
Sergio Giro
马尔可夫决策过程的定量模型检查器通常使用有限精度算术。如果过程中的所有系数都是有理数，则模型检验结果也是有理数，可以准确计算。然而，精确技术通常过于昂贵或可扩展性有限。在本文中，我们提出了一种从有限精度算术中的近似解开始获得精确结果的方法。该方法的输入是调度器的描述，可以通过模型检查器使用有限精度来获得。给定一个调度器，我们展示了如何在线性规划问题中获得相应的基，使得每当调度器达到最坏情况概率时基都是最优的。这种对应关系对于折扣 MDP 来说是已知的，我们展示了如何在未折扣的情况下应用它，前提是完成了一些预处理。利用该对应关系，可以从所获得的基开始以精确算术求解线性规划问题。因此，即使模型检查器提供的调度器不是最优的，该方法也能找到最坏情况的概率。在我们的实验中，从候选调度程序计算精确解的速度明显快于使用单纯形法在从默认基础开始的精确算术下的计算。
Quantitative model checkers for Markov Decision Processes typically use finite-precision arithmetic. If all the coefficients in the process are rational numbers, then the model checking results are rational, and so they can be computed exactly. However, exact techniques are generally too expensive or limited in scalability. In this paper we propose a method for obtaining exact results starting from an approximated solution in finite-precision arithmetic. The input of the method is a description of a scheduler, which can be obtained by a model checker using finite precision. Given a scheduler, we show how to obtain a corresponding basis in a linear-programming problem, in such a way that the basis is optimal whenever the scheduler attains the worst-case probability. This correspondence is already known for discounted MDPs, we show how to apply it in the undiscounted case provided that some preprocessing is done. Using the correspondence, the linear-programming problem can be solved in exact arithmetic starting from the basis obtained. As a consequence, the method finds the worst-case probability even if the scheduler provided by the model checker was not optimal. In our experiments, the calculation of exact solutions from a candidate scheduler is significantly faster than the calculation using the simplex method under exact arithmetic starting from a default basis.