Explicit model checking with magnetic disk is prohibitively slow if file input/output (IO) is not carefully managed. We give an empirical analysis of the two published algorithms for model checking with magnetic disk and show that both algorithms minimize file IO time but are dominated by delayed duplicate detection time (which is required to avoid regenerating parts of the transition graph). We present and analyze a more time-efficient algorithm for model checking with magnetic disk that requires more file IO time, but less delayed duplicate detection time and less total execution time. The new algorithm is a variant of parallel partitioned hash table algorithms and uses a time-efficient chained hash table implementation.


Model Check Hash Table Local Algorithm Linear Temporal Logic Total Execution Time 
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.


  1. 1.
    Bao, T.: Emperical comparison of algorithms for model checking with magnetic disk. Technical Report VV-0402, Dept. of Computer Science, Brigham Young U. (2004)Google Scholar
  2. 2.
    Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms, ch. 11. McGraw-Hill, New York (1999)Google Scholar
  3. 3.
    Explicit model checking benchmarks (2004), Available at
  4. 4.
    Jones, M.D., Mercer, E.: Explicit state model checking with Hopper. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 146–150. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Korf, R.E.: Delayed duplicate detection: Extended abstract. In: Gottlob, G., Walsh, T. (eds.) Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence (IJCAI 2003). Morgan Kaufmann, San Francisco (2003)Google Scholar
  6. 6.
    Pelanek, R.: Typical structural properties of state spaces. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 5–23. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  7. 7.
    Della Penna, G., Intrigila, B., Tronci, E., Venturini Zilli, M.: Exploiting transition locality in the disk based Murφ verifier. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 202–219. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. 8.
    Rangarajan, M., Dajani-Brown, S., Schloegel, K., Cofer, D.: Analysis of distributed spin applied to industrial-scale models. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 267–285. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  9. 9.
    Ranjan, R.K., Sanghavi, J.V., Brayton, R.K., Sangiovanni-Vincentelli, A.: High performance BDD package by exploiting memory hierarchy. In: 33rd Annual Conference on Design Automation (DAC 1996), pp. 635–641. ACM Press, New York (1996)Google Scholar
  10. 10.
    Roscoe, A.W.: Model-checking CSP. In: A Classical Mind: Essays in Honor of C. A. R. Hoare, pp. 353–378. Prentic-Hall, Englewood Cliffs (1994)Google Scholar
  11. 11.
    Stern, U., Dill, D.L.: Parallelizing the Murφ verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 256–267. Springer, Heidelberg (1997)Google Scholar
  12. 12.
    Stern, U., Dill, D.L.: Using magnetic disk instead of main memory in the Murφ verifier. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 172–183. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  13. 13.
    Zhou, R., Hansen, E.: Structured duplicate detection in external-memory graph search. In: McGuinness, D.L., Ferguson, G. (eds.) Nineteenth National Conference on Artificial Intelligence (AAAI 2004), San Jose, California, pp. 677–682. AAAI Press / MIT Press (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Tonglaga Bao
    • 1
  • Michael Jones
    • 1
  1. 1.Dept. of Computer ScienceBrigham Young U.ProvoUSA

Personalised recommendations