Abstract
Model checking is an automatic verification technique for finite state concurrent systems. In this approach to verification, temporal logic specifications are checked by an exhaustive search of the state space of the concurrent system. Since the size of the state space grows exponentially with the number of processes, model checking techniques based on explicit state enumeration can only handle relatively small examples. This phenomenon is commonly called the “State Explosion Problem”. Over the past ten years considerable progress has been made on this problem by (1) representing the state space symbolically using BDDs and by (2) using abstraction to reduce the size of the state space that must be searched. As a result model checking has been used successfully to find extremely subtle errors in hardware controllers and communication protocols. In spite of these successes, however, additional research is needed to handle large designs of industrial complexity. This aim of this paper is to give a succinct survey of symbolic model checking and to introduce the reader to recent advances in abstraction.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
H. Andréka, J. van Benthem, and I. Németi. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27:217–274, 1998.
F. Balarin and A. L. Sangiovanni-Vincentelli. An iterative approach to language containment. In Computer-Aided Verification, volume 697 of LNCS, pages 29–40, 1993.
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transaction on Computers, pages 35(8):677–691, 1986.
R. E. Bryant. On the complexity of VLSI implementations and graph representations of boolean functions with application to integer multiplication. IEEE Transaction on Comput-ers, pages 40:205–213, 1991.
J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transi-tion relations. In A. Halaas and P. B. Denyer, editors, Proceedings of the 1991 International Conference on Very Large Scale Integration, Aug. 1991. Winner of the Sidney Michaelson Best Paper Award.
J. R. Burch, E. M. Clarke, and K. L. McMillan. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142–170, 1992.
P. Chauhan, E. Clarke, S. Jha, and H. Veith. Efficient image computation. Manuscript, 2000.
A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new symbolic model checker. Software Tools for Technology Transfer, 1998.
E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer-Aided Verification (CAV) 2000, volume 1855 of LNCS. Springer, 2000. Full version available as Technical Report CMU-CS-00-103, Carnegie Mellon Uni-versity.
E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Publishers, 1999.
E. Clarke and H. Schlingloff. Model checking. In J. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier, 2000. to appear.
E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs: Workshop, LNCS, 1981.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concur-rent system using temporal logic. In Proceedings of the Tenth Annual ACM Symposium on Principles of Programming Languages (POPL), January 1983.
E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Trans-actions on Programming Languages and System (TOPLAS), 16(5):1512–1542, September 1994.
E. M. Clarke Jr., E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2):244–263, Apr. 1986.
O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In J. Sifakis, editor, Proceedings of the 1989 International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, June 1989.
J. Feigenbaum, S. Kannan, M. Y. Vardi, and M. Viswanathan. Complexity of problems on graphs represented as OBDDs. Chicago Journal of Theoretical Computer Science, 1999.
G. Gottlob, E. Grädel, and H. Veith. Datalog LITE: a deductive query language with linear time model checking. ACM Transactions on Computational Logic (TOCL), 2001. Accepted for publication.
G. Gottlob, N. Leone, and H. Veith. Succinctness as a source of complexity in logical for-malisms. Annals of Pure and Applied Logic, 97(1–3):231–260, 1999.
E. Grädel and I. Walukiewicz. Guarded fixed point logic. In G. Longo, editor, Proc. 14th IEEE Symp. on Logic in Computer Science, pages 45–54, 1999.
R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, 1994.
Y. Lakhnech. personal communication. 2000.
M. Li and P. Vitányi. An introduction to Kolmogorov Complexity and its applications.Spinger Verlag, New York, 1993.
J. Marques-Silva and K. A. Sakallah. GRASP: A search algorithm for propositional satisfi-ability. IEEE Transactions on Computers, 48(5):506–521, 1999.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
I. Moon, J. H. Kukula, K. Ravi, and F. Somenzi. To split or to conjoin: The question in image computation. In Proceedings of the 37th Design Automation Conference (DAC’00), pages 26–28, Los Angeles, June 2000.
I. Moon and F. Somenzi. Border-block triangular form and conjunction schedule in im-age computation. In Proceedings of the Formal Methods in Computer Aided Design (FM-CAD’00), November 2000. To appear.
C. Pixley. A computational theory and implementation of sequential hardware equivalence. In R. Kurshan and E. Clarke, editors, Proc. CAV Workshop (also DIMACS Tech. Report 90-31), Rutgers University, NJ, June 1990.
C. Pixley, G. Beihl, and E. Pacas-Skewes. Automatic derivation of FSM specification to implementation encoding. In Proceedings of the International Conference on Computer Desgin, pages 245–249, Cambridge, MA, Oct. 1991.
C. Pixley, S.-W. Jeong, and G. D. Hachtel. Exact calculation of synchronization sequences based on binary decision diagrams. In Proceedings of the 29th Design Automation Confer-ence, pages 620–623, June 1992.
F. Somenzi. CUDD: CU decision diagram package. http://vlsi.colorado.edu/fabio/.
H. Veith. Languages represented by boolean formulas. Information Processing Letters, 63:251–256, 1997.
H. Veith. How to encode a logical structure as an OBDD. In Proc. 13th Annual IEEE Conference on Computational Complexity (CCC), pages 122–131. IEEE Computer Society, 1998.
H. Veith. Succinct representation, leaf languages and projection reductions. Information and Computation, 142(2):207–236, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H. (2001). Progress on the State Explosion Problem in Model Checking. In: Wilhelm, R. (eds) Informatics. Lecture Notes in Computer Science, vol 2000. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44577-3_12
Download citation
DOI: https://doi.org/10.1007/3-540-44577-3_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41635-7
Online ISBN: 978-3-540-44577-7
eBook Packages: Springer Book Archive