Formula-dependent abstraction for CTL model checking

We present a state abstraction that is defined with respect to a given CTL formula. Since it does not attempt to preserve all ACTL formula, like simulation does, we can expect to compute coarser abstraction. Specifically, the abstraction is used to reduce the size of each Kripke structure, so that their product will be smaller. When the abstraction is too coarse, we show how refinement can be applied to produce a more precise abstract model. We also extend the notion of formula-dependent abstraction to Kripke structure with fairness, and define the coarsest abstraction that preserves the given CTL formula interpreted with respect to the fair paths. The method is exact and fully automatic, and handles full CTL.