一种基于扩展不完全Kripke结构的三值逻辑模型检测方法

来源：计算机工程与科学杂志2015年第10期北京时间：

作者：刘姣，雷丽晖

单位：陕西师范大学计算机科学学院，陕西 西安 710119

摘要：多值模型检测是解决形式化验证中状态爆炸问题的一种重要方法，三值模型检测是多值模型检测的基础，其中如何检验不确定状态的真值是一难点。针对不确定状态检验，提出了一种模型检测方法，首先对不完全Kripke结构PKS进行了扩展，然后在扩展后的模型上给出了检测不确定状态真值的方法，最后给出了基于扩展不完全Kripke结构的三值逻辑模型检测算法。与已有的三值逻辑模型检测算法相比，该算法降低了算法复杂度，完善了对于不确定或不一致信息的处理，从而增强了三值逻辑模型检测的实用性。

关键词：三值逻辑,模型检测,扩展的不完全Kripke结构,

基金资助：国家自然科学基金资助项目（61003061,11271237）