基于OBDD的SMC反例生成研究

摘要：

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

关键词：有序二叉决策图、模型检测、计算树逻辑(CTL)、反例生成

所属期刊栏目：48

分类号：TP311(计算技术、计算机技术)

在线出版日期：2012-06-26（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：54-58,145