Weakly acyclic diagrams: A data structure for infinite-state symbolic verification
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.
Cite
@article{arxiv.2411.17250,
title = {Weakly acyclic diagrams: A data structure for infinite-state symbolic verification},
author = {Michael Blondin and Michaël Cadilhac and Xin-Yi Cui and Philipp Czerner and Javier Esparza and Jakob Schulz},
journal= {arXiv preprint arXiv:2411.17250},
year = {2025}
}
Comments
Final version of TACAS'25 with appendix and link to artifact