Weakly acyclic diagrams: A data structure for infinite-state symbolic verification
Michael Blondin, Michaël Cadilhac, Xin-Yi Cui, Philipp Czerner, Javier Esparza, Jakob Schulz
TL;DR
This work generalizes binary decision diagrams to weakly acyclic languages, enabling compact, top-down symbolic representations of infinite-state sets. By introducing the master automaton and a table-based weakly acyclic diagram (WAD) data structure, it preserves the efficient DP-style algorithms of OBDDs while handling infinite languages. It defines essential operations (complement, intersection, Pre/Post) and proves correctness and complexity bounds under memoization and a pre-compatibility condition, enabling practical backward reachability for well-structured systems. A prototype wadl library demonstrates competitive performance on lossy channel systems, Petri nets, and broadcast protocols, suggesting broad applicability to infinite-state symbolic verification. The work also sketches extensions and provides experimental evidence that weakly acyclic languages are common in regular model checking tasks.
Abstract
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.