Formula-Dependent Equivalence for Compositional CTL Model Checking

We present a polytime computable state equivalence that is defined with respect to a given CTL formula. Since it does not attempt to preserve all CTL formulas, like bisimulation does, we can expect to compute coarser equivalences. This equivalence can be used to reduce the complexity of model checking a system of interacting FSMs. Additionally, we show that in some cases our techniques can detect if a formula passes or fails, without forming the entire product machine. The method is exact and fully automatic, and handles full CTL.