We present a model checking algorithm for
$\forall {\it CTL}$ (and full $\CTL$)
which uses an iterative abstraction refinement strategy.
In each iteration we call a standard model checker for the abstract
models ${\cal A}_i$.
If ${\cal A}_i$ does not satisfy $\Phi$ we refine the abstract
model ${\cal A}_i$ yielding another abstract model $\A_{i+1}$
and (re-)call the model checker to $\A_{i+1}$.
Otherwise the formula holds for the original system $\M$.
Our algorithm terminates at least
for all transition systems ${\cal M}$ that
have a finite simulation or bisimulation quotient.
In contrast to other abstraction refinement
algorithms, we always work with abstract models whose size just
depend on the length of the formula $\Phi$ (but not on the size of
the system which might be infinite).
%In particular, our algorithm has the potential to handle
%systems of arbitrary size
%as the proper model checker just has to treat the small
%abstract models ${\cal A}_i$.
