基于OBDD的简化SMC反例生成算法优化

本篇论文主要关注于改进符号模型检测中的反例生成算法，针对传统方法存在的问题，即在生成反例时可能引入大量无关变量导致反例难以理解。论文提出了一种基于有序二叉决策图（OBDD）的反例生成策略。OBDD，由Bryant提出的高效表示布尔函数的方法，利用其结构特性，能够有效地压缩和存储状态集。 传统的反例生成算法往往采用穷举搜索，这可能导致冗余状态和复杂的反例，难以快速定位问题。作者的新算法通过将反例状态扩展为一个状态集，并利用ZBDD（零压缩二叉决策图）来存储这些状态，显著减少了无关变量的影响。ZBDD只保留与问题相关的关键变量，从而优化了存储空间，提高了反例的可读性和定位效率。 论文首先介绍了模型检测方法作为复杂系统验证的重要工具，强调了其优点如基于模型、无需激励码和自动验证，但也指出了生成复杂反例的问题。为了改善这一现状，论文重点介绍了算法改进的具体实现，包括状态集的构建和ZBDD的应用。作者通过实验对比展示了新算法相较于传统方法在减少变量数和节省存储空间方面的显著优势。 因此，本文的研究内容涵盖了模型检测、反例生成、OBDD理论及其在反例生成中的应用，旨在提高复杂系统验证的效率和结果的可解释性，是计算机工程与应用领域的一个重要研究进展。