Title :
Automatic compositional minimization in CTL model checking
Author :
Chiodo, M. ; Shiple, T.R. ; Sangiovanni-Vincentelli, A.L. ; Brayton, R.K.
Author_Institution :
Magneti Marelli, Pavia, Italy
Abstract :
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.<>
Keywords :
computational complexity; finite automata; CTL model checking; automatic compositional minimisation; complexity; computation tree logic; interacting finite state machines; Complexity theory; Finite automata;
Conference_Titel :
Computer-Aided Design, 1992. ICCAD-92. Digest of Technical Papers., 1992 IEEE/ACM International Conference on
Conference_Location :
Santa Clara, CA, USA
Print_ISBN :
0-8186-3010-8
DOI :
10.1109/ICCAD.1992.279379
