In our earlier work, we identified a useful family of multi-valued logics: those specified over finite distributive lattices where negation preserves involution, i.e., for every element a of the logic. Such structures are called quasi-boolean algebras, and model-checking over these not only extends the domain of applicability of automated reasoning to new problems, but can also speed up solutions to some classical verification problems.

Symbolic model-checking over quasi-boolean algebras can be cast in terms of operations over multi-valued sets: sets whose membership functions are multi-valued. In this paper, we propose and empirically evaluate several choices for implementing multi-valued sets with decision diagrams. In particular, we describe two major approaches: (1) representing the multi-valued membership function canonically, using MDDs or ADDs; (2) representing multi-valued sets as a collection of classical sets, using a vector of either MBTDDs or BDDs. The naive implementation of (2) includes having a classical set for each value of the algebra. We exploit a result of lattice theory to reduce the number of such sets that need to be represented.

The major contribution of this paper is the evaluation of the different implementations of multi-valued sets, done via a series of experiments and using several case studies.