Enhanced Vacuity Detection in Linear Temporal Logic
Enhanced Vacuity Detection in Linear Temporal Logic
复制标题
线性时态逻辑中增强的真空检测
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Moshe Y. Vardi
中科院分区：
文献类型：
--
作者：
R. Armoni;L. Fix;Alon Flaisher;O. Grumberg;Nir Piterman;A. Tiemeyer;Moshe Y. Vardi
时态逻辑模型检查工具的优点之一是，它们能够伴随着一个否定的答案与一个反例的正确性查询，以满足系统中的规范。另一方面，当正确性查询的答案是肯定的，大多数模型检查工具没有提供证明满足规范。在过去的几年里，人们越来越意识到在模型检查成功的情况下怀疑系统或包含错误的规范的重要性。特别是，最近有几个作品都集中在检测时间逻辑规范的空洞满意度。例如，当验证一个系统是否满足规范F = G（req →Fgrant）（“每个请求最终都有一个授权”）时，我们说在从不发送请求的系统中，F是空洞满足的。目前的工作集中在检测真空方面的子公式出现。在这项工作中，我们研究的真空检测与多次出现的子公式。
One of the advantages of temporal-logic model-checking tools is their ability to accompany a negative answer to a correctness query with a counterexample to the satisfaction of the specification in the system. On the other hand, when the answer to the correctness query is positive, most model-checking tools provide no witness for the satisfaction of the specification. In the last few years there has been growing awareness of the importance of suspecting the system or the specification of containing an error also in cases where model checking succeeds. In particular, several works have recently focused on the detection of the vacuous satisfaction of temporal logic specifications. For example, when verifying a system with respect to the specification ϕ = G(req →Fgrant) (“every request is eventually followed by a grant”), we say that ϕ is satisfied vacuously in systems in which requests are never sent. Current works have focused on detecting vacuity with respect to subformula occurrences. In this work we investigate vacuity detection with respect to subformulas with multiple occurrences.