Lattice-based Boolean diagrams

Abstract

This paper presents lattice-based Boolean diagrams (LBBDs), a graphical representation of Boolean functions that is not derived from binary decision diagrams (BDDs), as well as symbolic manipulation algorithms. It also identifies a class of Boolean functions where LBBDs are demonstrably more efficient to construct, and reason with, when compared to BDDs. The case studies include ITC99 and MCNC benchmarks, randomly generated cube covers or sum-of-products (SOP) formulas as well as multi-level Boolean formulas. Finally, LBBDs proved to be instrumental to the efficient runtime verification of software over distributed multiprocessor systems.