Formula dependent model reduction through elimination of invisible transitions for checking fragments of CTL

We present a reduction algorithm which reduces Kripke structures by
eliminating transitions from the model which do not affect the visible
components of the model. These are exactly the variables contained in
the specification formula. The reduction algorithm preserves the truth
of special CTL formulae. In contrast to formula-dependent reduction
algorithms presented so far, which are mostly computationally
expensive, our algorithm needs only one pass through the reachable
states of the model. Nevertheless, preliminary results show that models
are reduced considerably, which is plausible because, in general, the
number of visible components of a reactive system is small compared to
the number of internal components.