Model-Checking Over Multi-Valued Logics
Abstract
Classical logic cannot be used to effectively reason about systems
with uncertainty (lack of essential information) or
inconsistency (contradictory information often occurring
when information is gathered from multiple sources). In this paper we
propose the use of quasi-boolean multi-valued logics for
reasoning about such systems. We also give semantics to a
multi-valued extension of CTL, describe an implementation of a
symbolic multi-valued CTL model-checker, and analyze
its correctness and running time.