Abstract: 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.

Key words: Ordered Binary Decision Diagram（OBDD）, model checking, Computation Tree Logic（CTL）, counterexample generation

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

关键词: 有序二叉决策图, 模型检测, 计算树逻辑（CTL）, 反例生成