Model Checking Partial State Spaces with 3-Valued Temporal Logics

We address the problem of relating the result of model checking a partial state space of a system to the properties actually possessed by the system. We represent incomplete state spaces as partial Kripke structures, and give a 3-valued interpretation to modal logic formulas on these structures. The third truth value ? means “unknown whether true or false”. We define a preorder on partial Kripke structures that reflects their degree of completeness. We then provide a logical characterization of this preorder. This characterization thus relates properties of less complete structures to properties of more complete structures. We present similar results for labeled transition systems and show a connection to intuitionistic modal logic. We also present a 3-valued CTL model checking algorithm, which returns ? only when the partial state space lacks information needed for a definite answer about the complete state space.