Lattice-valued binary decision diagrams

This work introduces a new data structure, called Lattice-Valued Binary Decision Diagrams (or LVBDD for short), for the compact representation and manipulation of functions of the form θ : 2P → L, where P is a finite set of Boolean propositions and L is a finite distributive lattice. Such functions arise naturally in several verification problems. LVBDD are a natural generalisation of multi-terminal ROBDD which exploit the structure of the underlying lattice to achieve more compact representations. We introduce two canonical forms for LVBDD and present algorithms to symbolically compute their conjunction, disjunction and projection. We provide experimental evidence that this new data structure can outperform ROBDD for solving the finite-word LTL satisfiability problem.