Abstract
Arguably the two most important techniques that are used in model checking to counter the combinatorial explosion in the number of states are abstraction and guidance. In this work we combine these techniques in a natural way by using (homomorphic) abstractions that reveal an error in the model to guide the model checker in searching for the error state in the original system. The mechanism used to achieve this is based on pattern databases, commonly used in artificial intelligence. A pattern database represents an abstraction and is used as a heuristic to guide the search. In essence, therefore, the same abstraction is used to reduce the size of the model and guide a search algorithm. We implement this approach in NuSMV and evaluate it using 2 well-known circuit benchmarks. The results show that this method can outperform the original model checker by several orders of magnitude, in both time and space.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
McMillan, K.: Symbolic model checking. Kluwer Academic Publishers, Boston (1993)
Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: 1020 states and beyond. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, Washington, D.C., pp. 1–33. IEEE Computer Society Press, Los Alamitos (1990)
Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Formal Methods in System Design 1, 275–288 (1992)
Holzmann, G.J.: The model checker SPIN. Software Engineering 23, 279–295 (1997)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16, 1512–1542 (1994)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Clarke, E., Gupta, A., Kukula, J., Strichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 265–279. Springer, Heidelberg (2002)
Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Proceedings of the 35th Conference on Design Automation, Moscone center, San Francico, California, USA, June 15-19, pp. 599–604. ACM Press, New York (1998)
Alur, R., Wang, B.Y.: ”Next” heuristic for on-the-fly model checking. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 98–113. Springer, Heidelberg (1999)
Bloem, R., Ravi, K., Somenzi, F.: Symbolic guided search for CTL model checking. In: Proceedings of the 37th Conference on Design Automation, Los Angeles, CA, June 5-9, pp. 29–34. ACM, New York (2000)
Edelkamp, S., Lafuente, A.L., Leue, S.: Directed explicit model checking with HSF–SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 57–79. Springer, Heidelberg (2001)
Reffel, F., Edelkamp, S.: Error detection with directed symbolic model checking. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 195–211. Springer, Heidelberg (1999)
Cabodi, G., Nocco, S., Quer, S.: Mixing forward and backward traversals in guidedprioritized bdd-based verification. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 471–484. Springer, Heidelberg (2002)
Santone, A.: Heuristic search + local model checking in selective mu-calculus. IEEE Transactions on Software Engineering 29, 510–523 (2003)
Culberson, J.C., Schaeffer, J.: Searching with pattern databases. In: McCalla, G.I. (ed.) Canadian AI 1996. LNCS, vol. 1081, pp. 402–416. Springer, Heidelberg (1996)
Korf, R.: Finding optimal solutions to to Rubik’s cube using pattern databases. In: Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, Providence, Rhode Island, July 27-31, pp. 700–705. AAAI Press / The MIT Press (1997)
Holte, R.C., Mkadmi, T., Zimmer, R.M., MacDonald, A.J.: Speeding up problem solving by abstraction: A graph oriented approach. Artificial Intelligence 85, 321–361 (1996)
Holte, R., Hernadvolgyi, I.: Experiments with automatically created memory-based heuristics. In: Choueiry, B.Y., Walsh, T. (eds.) SARA 2000. LNCS (LNAI), vol. 1864, pp. 281–290. Springer, Heidelberg (2000)
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35, 677–691 (1986)
Edelkamp, S.: Symbolic pattern databases in heuristic search planning. In: Proceedings of the Sixth International Conference on Artificial Intelligence Planning Systems, Toulouse, France, April 23-27, pp. 274–283. AAAI, Menlo Park (2002)
Pearl, J.: Heuristics: Intelligent Search Strategies for Computer Problem Solving. Addison-Wesley, USA (1984)
Nymeyer, A., Qian, K.: Heuristic search algorithm based on symbolic data structures. In: Gedeon, T(T.) D., Fung, L.C.C. (eds.) AI 2003. LNCS (LNAI), vol. 2903, pp. 966–979. Springer, Heidelberg (2003)
Prieditis, A., Davis, R.: Quantitatively relating abstractness to the accuracy of admissible heuristics. Artificial Intelligence 74, 165–175 (1995)
Dill, D.L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. The MIT Press, MA (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Qian, K., Nymeyer, A. (2004). Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_37
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_37
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive