Model Checking wiht Multi-Valued Logics

In this paper we simplify and extend existing work on algorithms for multi-valued model checking. We show how to reduce multi-valued model checking with any distributive DeMorgan lattice to standard, two-valued model checking. From this reduction we derive complexity bounds for multi-valued model checking for various temporal logics.