Model-Checking over Multi-valued Logics

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.

• Type: Conference
• Year: 2001
• Where: FM
• Authors: Marsha Chechik, Steve M. Easterbrook, Victor Petrovykh
• Keywords: FM 2001, Formal Methods, Multi-valued, Quasi-boolean Multi-valued Logics, Symbolic Multi-valued Ctl