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 called Χchek, and analyze its correctness and running time. © Springer-Verlag Berlin Heidelberg 2001.