Memory Constrained Algorithms for Multi-valued Decision Diagrams
MDDs (multi-valued decision diagrams) are a generalization of binary decision diagrams (BDDs). In formal method verification tools, efficient MDD manipulation is critical. Despite the usefulness of MDDs in real-world tasks such as discovering the reachability set of a model, hardware resource limitations limit the efficacy of manipulation algorithms. Previous methodologies, such as variable ordering, demonstrate that choosing the right variable order has an influence on the size of the MDDs. Other studies on approximation and manipulation of high-density (finite but large) state systems shows the importance of efficient under-approximation techniques. Such studies have been conducted with an emphasis on binary decision diagrams. These algorithms function with limited memory, making them ideal for any hardware with limited memory. In this thesis, we focus on memory constrained algorithms, especially under-approximations, for MDDs.
We present a novel quadratic-time under-approximation technique for MDDs in this work. The method obtains the information by traversing an MDD and selecting either a node or a collection of nodes with the lowest density. The former is more accurate, but more time-consuming, whereas the latter has a better execution time, but it is more eager in deleting nodes, which may result in deleting too many nodes from the MDD.
The primary conclusion of this study is that selecting a collection of nodes for deletion performs better in larger real-world problems in terms of execution time, although selecting one node for removal at a time delivers a more precise outcome. This work highlights the effectiveness of using an under-approximation approach when manipulating multi-valued decision diagrams.
Committee: Gianfranco Ciardo (major professor), Samik Basu, Andrew Miner, James Lathrop