Abstract
The aim of this paper is to show how big model checking problems for Computation Tree Logic (CTL) can be handled by using current powerful vector processors. Although efficient recursive model checking algorithms for CTL, which run in time proportional to both the size of Kripke structures and the length of formulas, have been already proposed [7, 2], their algorithms cannot be vectorized due to recursive procedure calls. In this paper we propose a new model checking algorithm, called a vectorized model checking algorithm, for CTL which is suitable for the execution on vector processors. It can handle more than 1 million state Kripke structure derived from a deterministic sequential machine.
Chapter PDF
References
A. V. Aho, J. E. Hopcroft, and J. D. Ullman. The Design and Analysis of Computer Algorithms. Addison Wesley, 1974.
M. C. Browne. An improved algorithm for the automatic verification of finite state systems using temporal logic. Technical Report CMU-CS-86-156, Carnegie Mellon University, 1986.
M. C. Browne, E. M. Clarke, D. L. Dill, and B. Mishra. Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computers, C-35(12):1035–1044, December 1986.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. Logic in Computer Science, 1990.
E. M. Clarke, S. Bose, M. C. Browne, and O. Grumberg. The design and verification of finite state hardware controllers. Technical Report CMU-CS-87-145, Carnegie Mellon University, July 1987.
E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Proc. Workshop on Logic of Programs, pages 52–71. Springer-Verlag, 1981.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. Technical Report CMU-CS-83-152, Carnegie Mellon University, 1983.
E. M. Clarke and O. Grumberg. Avoiding the state explosion problem in temporal logic model checking algorithms. In Proc. 6th Annual ACM Symposium of Principles of Distributed Computing, pages 294–303, August 1987.
E. M. Clarke and O. Grumberg. Research on automatic verification of finite-state concurrent systems. Technical Report CMU-CS-87-105, Carnegie Mellon University, January 1987.
E. M. Clarke, D. E. Long, and K. L. McMillan. A language for compositional specification and verification of finite state hardware controllers. In Proc. 9th IFIP Symposium on Computer Hardware Description Languages and their Applications, pages 281–295, June 1989.
S. Graf, J. L. Richier, C. Rodriguez, and J. Voiron. What are the limits of model checking methods for the verification of real life protocols? In Proc. Workshop on Automatic Verification Methods for Finite State Systems, June 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hiraishi, H., Meki, S., Hamaguchi, K. (1991). Vectorized model checking for computation tree logic. In: Clarke, E.M., Kurshan, R.P. (eds) Computer-Aided Verification. CAV 1990. Lecture Notes in Computer Science, vol 531. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023718
Download citation
DOI: https://doi.org/10.1007/BFb0023718
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54477-7
Online ISBN: 978-3-540-38394-9
eBook Packages: Springer Book Archive