基于SAT工具的限界模型检测归约方法

• 作者: 喻超 毋国庆
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 模型检测 形式化验证 归约
• 年，卷（期）: 2010,（17）
• 页码范围: 60-62
• 分类号: TP311
• 字数: 3499字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2010.17.021

摘要

限界模型检测主要对路径上的属性进行检测,基于此给出一种编码方法,将LTL公式在路径上展开,从而将限界模型检测转换为命题逻辑的可满足性问题,使用SAT求解工具来完成模型检测过程.阐述归约过程的正确性与完全性,通过一个具体例子证明了该方法的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	毋国庆	武汉大学计算机学院	72	470	12.0	17.0
2	喻超	成都东软信息技术学院科研管理部	4	5	1.0	2.0