Model checking partial state spaces with 3-valued temporal logics (Extended abstract)

Abstract

We address the problem of relating the result of model check- ing 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 characte- rization 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 connec- tion 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.