Ordered binary decision diagrams (OBDDs) are a fundamental data structure for the manipulation of Boolean functions, with strong applications to finite-state symbolic model checking. OBDDs allow for efficient algorithms using top-down dynamic programming. From an automata-theoretic perspective, OBDDs essentially are minimal deterministic finite automata recognizing languages whose words have a fixed length (the arity of the Boolean function). We introduce weakly acyclic diagrams (WADs), a generalization of OBDDs that maintains their algorithmic advantages, but can also represent infinite languages. We develop the theory of WADs and show that they can be used for symbolic model checking of various models of infinite-state systems.

翻译：有序二元决策图（OBDD）是处理布尔函数的基础数据结构，在有限状态符号模型检测中具有重要应用。OBDD支持基于自顶向下动态规划的高效算法。从自动机理论视角看，OBDD本质上是识别具有固定字长（布尔函数的元数）语言的最小化确定性有限自动机。本文提出弱非循环图（WAD），作为OBDD的泛化形式，在保持其算法优势的同时能够表示无限语言。我们建立了WAD的理论体系，并证明其可用于多种无限状态系统模型的符号模型检测。