#
Data Structures for Symbolic Multi-Valued Model-Checking

###
Abstract

Multi-valued logics can be effectively used to reason about
incomplete and/or inconsistent systems, e.g. during early
software requirements or as the systems evolve.
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., ~~*a* = *a* for every
element *a* of the logic. Model-checking over this family
of logics allows not only to extend the domain of applicability
of automated reasoning to new problems, but also to speed up some
classical verification problems.
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.