论文研究基于OBDD的SMC反例生成研究.pdf

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