This paper presents two frameworks for abstraction-refinement in model checking. The first is the CounterExample-Guided Abstraction-Refinement (CEGAR) which can verify universal fragments of temporal logics and is based on a 2-valued semantics of temporal logics. The other is the Three-valued Abstraction-Refinement (TVAR) and is based on a 3-valued semantics of these logics.

We also present an application of the 3-valued framework for fully automatic compositional model checking. Based on this and other successful applications of the 3-valued framework we conclude that the additional power it provides is worth the extra efforts of having non-standard definitions and algorithms.