Generalized Model Checking: Reasoning about Partial State Spaces

We discuss the problem of model checking temporal properties on partial Kripke structures, which were introduced in [BG99] for representing 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 fro 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 phi on a partial Kripke structure M returns the third truth value - (read "unknown) only if there exist Kripke structures M sub 1 and M sub 2 that both complete M and such that M sub 1 satisfies phi while M sub 2 violates phi, hence making the value of phi 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 the 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.