Probabilistic Model Checking and Reliability of Results
Probabilistic Model Checking and Reliability of Results
复制标题
DOI：
10.1109/ddecs.2008.4538787
复制
发表时间：
2008-04
期刊：
影响因子：
--
通讯作者：
Ralf Wimmer;Alexander Kortus;Marc Herbstritt;B. Becker
中科院分区：
文献类型：
--
作者：
Ralf Wimmer;Alexander Kortus;Marc Herbstritt;B. Becker
在形式验证中，可靠的结果至关重要。在数字系统的模型检测中，主要是由于逻辑错误导致的模型检测算法的不正确实现是错误结果的来源。然而，在概率模型检验中，数值不稳定性是不一致结果的另一个来源。我们激励我们的调查与一个例子，其中几个国家的最先进的概率模型检查工具，由于不精确的计算给出了完全错误的结果。然后，我们分析，在模型检查过程中引入的不准确点。我们讨论的第一个想法，尽管这些不准确，可靠的结果可以获得或至少用户被警告潜在的正确性问题：（1）精确的用法（理性）算术，（2）使用区间算术获得实际概率的安全近似值，（3）提供证明结果正确的证书，以及（4）将每个子公式的“置信度”集成到现有的模型检查工具中。
In formal verification, reliable results are of utmost importance. In model checking of digital systems, mainly incorrect implementations of the model checking algorithms due to logical errors are the source of wrong results. In probabilistic model checking, however, numerical instabilities are an additional source for inconsistent results. We motivate our investigations with an example, for which several state-of-the-art probabilistic model checking tools give completely wrong results due to inexact computations. We then analyze, at which points inaccuracies are introduced during the model checking process. We discuss first ideas how, in spite of these inaccuracies, reliable results can be obtained or at least the user be warned about potential correctness problems: (1) usage of exact (rational) arithmetic, (2) usage of interval arithmetic to obtain safe approximations of the actual probabilities, (3) provision of certificates which testify that the result is correct, and (4) integration of a "degree of belief" for each sub-formula into existing model checking tools.