We present a model checking algorithm for ∀
CTL (and full
CTL) which uses an iterative abstraction refinement strategy.
It terminates at least for all transition systems M that have a finite simulation or bisimulation quotient. In contrast to other abstraction refinement algorithms, we always
work with abstract models whose sizes depend only on the length of the formula θ (but not on the size of the system, which
might be infinite).