Symbolic model-checking over multi-valued logics 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 logic. 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.