Efficient Patterns for Model Checking Partial State Spaces in CTL intersection LTL
Efficient Patterns for Model Checking Partial State Spaces in CTL intersection LTL
复制标题
CTL 交集 LTL 中模型检查部分状态空间的有效模式
DOI：
10.1016/j.entcs.2006.04.004
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
M. Huth
中科院分区：
文献类型：
--
作者：
Adam Antonik;M. Huth
部分Kripke结构的组合模型检查是有效的，但不完整，因为它们可能无法识别所有实现都满足checked属性。但是如果一个属性对于这样的检查成立，那么它在所有实现中都成立。因此，这种检查是欠近似的。在本文中，我们确定哪些流行的规范模式，记录在社区主导的模式库，这种近似是精确的，因为匡威关系以及所有的模型检查。我们发现，许多这样的模式确实是精确的。那些没有失去精确性的，因为在混合极性中只有一个命题原子。因此，我们可以仅使用线性爆破来计算相同时态逻辑中的语义最小化，其有效检查为原始不精确模式提供精确结果。因此，能够以低成本确保所有图案的精度。
Compositional model checks of partial Kripke structures are efficient but incomplete as they may fail to recognize that all implementations satisfy the checked property. But if a property holds for such checks, it will hold in all implementations. Such checks are therefore under-approximations. In this paper we determine for which popular specification patterns, documented at a communityled pattern repository, this under-approximation is precise in that the converse relationship holds as well for all model checks. We find that many such patterns are indeed precise. Those that aren't lose precision because of a sole propositional atom in mixed polarity. Hence we can compute, with linear blowup only, a semantic minimization in the same temporal logic whose efficient check renders the precise result for the original imprecise pattern. Thus precision can be secured for all patterns at low cost.