摘要
针对传统的符号模型检测反例生成算法在生成反例时会产生大量的无关变量,使得反例难以理解。提出一种改进的反例生成算法,将反例中的状态扩展为一个状态集,使用零压缩二叉决策图(Zero-Suppressed Binary Decision Diagrams,ZBDD)来存储所求出的状态集。删除了系统中的无关变量,仅保留了相关的变量,实验表明该算法能有效地减少状态的变量数,减少存储反例所需的空间。
Because the traditional symbolic model checking for counterexample generation algorithm to generate counter-examples of a large amount of unrelated variables, making the counter-example is very difficult to understand. An improved counter-example generation algorithm, the state of the anti-expansion case, a state set calculated using zero-suppressed binary decision diagrams(ZBDD)is used to store the state set. Then delete the system independent variables, retain the relevant variables. Experiments show that the algorithm can effectively reduce the number of state variables and reduce the storage space required by counterexample.
出处
《计算机工程与应用》
CSCD
2012年第10期54-58,145,共6页
Computer Engineering and Applications
关键词
有序二叉决策图
模型检测
计算树逻辑(CTL)
反例生成
Ordered Binary Decision Diagram(OBDD)
model checking
Computation Tree Logic(CTL)
counter-example generation
