Generalized Model Checking: Reasoning about Partial State Spaces

We discuss the problem of model checking temporal properties on partial Kripke structures, which were used in [BG99] to represent incomplete state spaces. We first extend the results of [BG99] by showing that the model-checking problem for any 3-valued temporal logic can be reduced to two model-checking problems for the corresponding 2-valued temporal logic. We then introduce a new semantics for 3-valued temporal logics that can give more definite answers than the previous one. With this semantics, the evaluation of a formula φ on a partial Kripke structure M returns the third truth value ⊥ (read “unknown”) only if there exist Kripke structures M₁ and M₂ that both complete M and such that M₁ satisfies φ while M₂ violates φ, hence making the value of φ on M truly unknown. The partial Kripke structure M can thus be viewed as a partial solution to the satisfiability problem which reduces the solution space to complete Kripke structures that are more complete than M with respect to a completeness preorder. This generalized model-checking problem is thus a generalization of both satisfiability (all Kripke structures are potential solutions) and model checking (a single Kripke structure needs to be checked). We present algorithms and complexity bounds for the generalized model-checking problem for various temporal logics.