id: 01802399
dt: j
an: 01802399
au: Aziz, Adnan; Shiple, Thomas; Singhal, Vigyan; Brayton, Robert;
    Sangiovanni-Vincentelli, Alberto
ti: Formula-dependent equivalence for compositional CTL model checking.
so: Form. Methods Syst. Des. 21, No.2, 193-224 (2002).
py: 2002
pu: Springer, Norwell, MA
la: EN
cc: F.1.2
ut: CTL model checking; bisimulation; compositional minimization
ci: 
li: doi:10.1023/A:1016043502772
ab: Summary: 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.
rv: