This paper presents two frameworks for abstraction-refinement in model checking. The first one handles ACTL specification. The abstraction is conservative for ACTL verification, but not for falsification. Spurious counterexamples in the abstract model are used to guide a refinement that eliminates these counterexamples.

The other framework handles full CTL. On abstract models, CTL formulas are interpreted with respect to the 3-valued semantics and can be evaluated to either true, false, or the indefinite value ⊥. The abstraction is conservative for CTL verification as well as falsification. Only if a formula is evaluated to ⊥ in the abstract model, its value in the concrete model is unknown and refinement is needed. However, now the goal of the refinement is to eliminate indefinite results and to turn them into either definite true or definite false.