Improving Binary Decision Diagrams for Symbolic Analysis of Discrete State Systems

State space exploration is a fundamental step in the formal verification of discrete state systems. However, the exponential growth of the state space—known as the state space explosion—poses a longstanding challenge. Binary Decision Diagrams (BDDs) have proven effective in mitigating this issue across various industrial applications, including VLSI design and the verification of circuits and protocols.

Among the canonical BDD variants, reduced ordered BDDs (FBDDs) and zero-suppressed BDDs (ZBDDs) are widely used. Each offers unique advantages depending on the structure of the function being represented, though determining the optimal form in advance is often difficult. To address this, we first proposed Reduction-on-Edge Complement-and-Swap BDDs (RexBDDs), which combine key features of FBDDs and ZBDDs while introducing more edge-level abstractions. RexBDDs improve both the size and runtime performance of state space encoding. Building on this, we proposed Edge-Valued Modulo BDDs (EV%BDDs) to represent functions mapping states to quantitative values (e.g., distances) more compactly. We then introduced enhanced abstraction mechanisms into Binary Matrix Diagrams (BMxDs) to efficiently encode transition relations, leveraging saturation techniques for symbolic state space exploration. Finally, to optimize for scenarios involving extensive querying, we employed a heuristic-based method to concretize "undefined" BDD entries—those never queried—by assigning them appropriate values. This post-processing step yields further reductions in diagram size, supporting faster and more memory-efficient query evaluation.

Committee: Gianfranco Ciardo (co-major professor), Andrew Miner (co-major professor), Samik Basu, Nok Wongpiromsarn, and Myra Cohen.