Automatic compositional minimization in CTL model checking

A method for reducing the complexity of CTL model checking on a system of interacting finite state machines is described. The method consists essentially of reducing each component machine with respect to the property to be verified, and then verifying the property on the composition of the reduced components. The procedure is fully automatic and produces an exact result. The potential of the approach is assessed on real-world examples, and the method is demonstrated on a circuit.<>