基于OBDD的SMC反例生成研究

• 作者: 姚全珠 苗永军
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 有序二叉决策图 模型检测 计算树逻辑(CTL) 反例生成
• 年，卷（期）: 2012,（10）
• 所属期刊栏目: 研究探讨
• 页码范围: 54-58,145
• 分类号: TP311
• 字数: 5054字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.2012.10.013

摘要

针对传统的符号模型检测反例生成算法在生成反例时会产生大量的无关变量,使得反例难以理解.提出一种改进的反例生成算法,将反例中的状态扩展为一个状态集,使用零压缩二叉决策图(Zero-Suppressed Binary Decision Diagrams,ZBDD)来存储所求出的状态集.删除了系统中的无关变量,仅保留了相关的变量,实验表明该算法能有效地减少状态的变量数,减少存储反例所需的空间.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	姚全珠	西安理工大学计算机科学与工程学院	84	918	15.0	26.0
2	苗永军	西安理工大学计算机科学与工程学院	1	1	1.0	1.0