An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking
An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking
复制标题
模型检查中有效可检查的、基于证明的真空公式
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Kedar S. Namjoshi
中科院分区：
文献类型：
--
作者：
Kedar S. Namjoshi
模型检查算法可以报告一个属性为真的原因，可能被认为是空洞的。目前的算法检测真空需要检查一个二次规模见证公式，或多个模型检查运行，任何替代方案在实践中可能是相当昂贵的。从本质上讲，不确定性是模型检查器在将属性视为真时所使用的合理性的问题。我们认为，从这个角度来看，目前的真空定义过于宽泛，并给出了一个新的，更窄的，制定。新的配方导致一个简单的检测方法，检查只从模型检查器中提取的理由，在自动生成的证明的形式。在对属性运行一次验证后，这种检查需要少量的计算，因此它比以前的方法效率高得多。虽然新的配方是强大的，因此报告真空不经常，我们表明，它同意目前的配方表示为自动机的线性时间属性。固有的支化特性会产生差异，但在当前制剂报告的真空度值得商榷的情况下。
Model checking algorithms can report a property as being true for reasons that may be considered vacuous. Current algorithms for detecting vacuity require either checking a quadratic size witness formula, or multiple model checking runs; either alternative may be quite expensive in practice. Vacuity is, in its essence, a problem with the justification used by the model checker for deeming the property to be true. We argue that current definitions of vacuity are too broad from this perspective and give a new, narrower, formulation. The new formulation leads to a simple detection method that examines only the justification extracted from the model checker in the form of an automatically generated proof. This check requires a small amount of computation after a single verification run on the property, so it is significantly more efficient than the earlier methods. While the new formulation is stronger, and so reports vacuity less often, we show that it agrees with the current formulations for linear temporal properties expressed as automata. Differences arise with inherently branching properties but in instances where the vacuity reported with current formulations is debatable.