Efficient Multiple-Valued Model-Checking Using Lattice Representations
Multiple-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. We specify
multiple-valued logics using finite lattices. In this paper, we
use lattice representation theory to cast the multiple-valued
model-checking problem in terms of symbolic operations on
classical sets of states, provided the lattices are distributive.
This allows us to partially reuse existing symbolic model-checking
technology and improve efficiency over previous implementations
that were based on multiple-valued decision diagrams.