NUSMV, similarly to CMU SMV, uses the algorithms presented in [12] as the basis for fair CTL model checking. These algorithms are essentially based on a fix-point characterization of temporal modalities and they work quite well in practice. If the set of reachable states has already been computed, the set of reachable states is used in the evaluation of CTL formulas. This allows us to restrict the search to reachable states only.
>