Implementing a Multi-valued Symbolic Model Checker
Implementing a Multi-valued Symbolic Model Checker
复制标题
实现多值符号模型检查器
DOI：
10.1007/3-540-45319-9_28
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
S. Easterbrook
中科院分区：
文献类型：
--
作者：
M. Chechik;B. Devereux;S. Easterbrook
多值逻辑通过在逻辑中允许额外的真值来支持不确定性和不一致性的显式建模。这种逻辑可以用于验证系统的动态特性，其中完整的，商定的系统模型不可用。在本文中，我们提出了一个多值时态逻辑的符号模型检查器的实现。模型检查器适用于任何真值形成拟布尔格的多值逻辑。我们的模型是generalizedKripke结构，其中原子命题和状态之间的转换可以采取给定的多值逻辑的任何真值。要进行模型检查的属性用CTL表示，并使用多值语义进行了推广。模型检查器的设计是基于MDDs的使用，MDDs是二元决策图的多值扩展。我们描述了MDD及其在模型检查器中的使用。我们也给出了它的理论时间复杂度和一些初步的经验性能数据。
Multi-valued logics support the explicit modeling of uncertainty and disagreement by allowing additional truth values in the logic. Such logics can be used for verification of dynamic properties of systems where complete, agreed upon models of the system are not available. In this paper, we present an implementation of a symbolic model checker for multi-valued temporal logics. The model checkerworks for any multi-valued logic whose truth values form a quasiboolean lattice. Our models are generalizedKripke structures, where both atomic propositions and transitions between states may take any of the truth values of a given multi-valued logic. Properties to be model checked are expressed in CTL, generalized with a multi-valued semantics. The design of the model checker is based on the use of MDDs, a multi-valued extension of Binary Decision Diagrams. We describe MDDs and their use in the model checker. We also give its theoretical time complexity and some preliminary empirical performance data.