Model Checking with Multi-Valued Temporal Logics
Abstract
Multi-valued logics support the explicit modeling of uncertainty
and disagreement by allowing additional truth values in the
logic. Such logics can be used for verification of dynamic
properties of systems even where complete, agreed upon models of
the system are not available. In this paper, we present
a symbolic model checker for multi-valued
temporal logics. The model checker works for any multi-valued
logic whose truth values form a quasi-boolean lattice. Our models
are generalized Kripke structures, where both atomic propositions
and transitions between states may take any of the truth values
of a given multi-valued logic. Properties to be model checked are
expressed in CTL, generalized with a multi-valued semantics. The
design of the model checker is based on the use of MDDs, a
multi-valued extension of Binary Decision Diagrams.