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

• 作者: 刘姣 雷丽晖
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 三值逻辑 模型检测 扩展的不完全Kripke结构
• 年，卷（期）: 2015,（10）
• 所属期刊栏目: 软件工程
• 页码范围: 1884-1889
• 页数: 6页
• 分类号: TP301.6
• 字数: 6426字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2015.10.014

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	雷丽晖	陕西师范大学计算机科学学院	9	25	4.0	4.0
2	刘姣	陕西师范大学计算机科学学院	2	0	0.0	0.0