Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking

  • J. Barnat
  • L. Brim
  • P. Šimeček
  • M. Weber
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)


Revisiting resistant graph algorithms are those, whose correctness is not vulnerable to repeated edge exploration. Revisiting resistant I/O efficient graph algorithms exhibit considerable speed-up in practice in comparison to non-revisiting resistant algorithms. In the paper we present a new revisiting resistant I/O efficient LTL model checking algorithm. We analyze its theoretical I/O complexity and we experimentally compare its performance to already existing I/O efficient LTL model checking algorithms.


Main Memory External Memory Internal Memory Cycle Detection Single Source Short Path 
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.
    Aggarwal, A., Vitter, J.S.: The input/output complexity of sorting and related problems. Commun. ACM 31(9), 1116–1127 (1988)CrossRefMathSciNetGoogle Scholar
  2. 2.
    Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification. In: Proc. of LICS 1986, pp. 332–344. Computer Society Press (1986)Google Scholar
  3. 3.
    Edelkamp, S., Jabbar, S.: Large-Scale Directed Model Checking LTL. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 1–18. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  4. 4.
    Barnat, J., Brim, L., Šimeček, P.: I/O Efficient Accepting Cycle Detection. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 281–293. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. 5.
    Korf, R.E., Schultze, P.: Large-Scale Parallel Breadth-First Search. In: Proc. of AAAI, pp. 1380–1385. AAAI Press / The MIT Press (2005)Google Scholar
  6. 6.
    Korf, R.E.: Best-First Frontier Search with Delayed Duplicate Detection. In: Proc. of AAAI, pp. 650–657 (2004)Google Scholar
  7. 7.
    Stern, U., Dill, D.L.: Using Magnetic Disk Instead of Main Memory in the Murphi Verifier. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 172–183. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  8. 8.
    Munagala, K., Ranade, A.: I/O-complexity of graph algorithms. In: Proc. of SODA, Society for Industrial and Applied Mathematics, pp. 687–694 (1999)Google Scholar
  9. 9.
    Brim, L., Černá, I., Moravec, P., Šimša, J.: Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-Checking. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 352–366. Springer, Heidelberg (2004)Google Scholar
  10. 10.
    Korf, R.E.: Best-First Frontier Search with Delayed Duplicate Detection. In: Proc. of AAAI, pp. 650–657. AAAI Press / The MIT Press (2004)Google Scholar
  11. 11.
    Zhou, R., Hansen, E.A.: Structured Duplicate Detection in External-Memory Graph Search. In: Proc. of AAAI, pp. 683–689 (2004)Google Scholar
  12. 12.
    Hammer, M., Weber, M.: To Store or Not To Store. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 51–66. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  13. 13.
    Černá, I., Pelánek, R.: Distributed Explicit Fair Cycle Detection. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 49–73. Springer, Heidelberg (2003)Google Scholar
  14. 14.
    Fisler, K., Fraer, R., Kamhi, G., Vardi, M.Y., Yang, Z.: Is There a Best Symbolic Cycle-Detection Algorithm? In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 420–434. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  15. 15.
    Ravi, K., Bloem, R., Somenzi, F.: A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 143–160. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  16. 16.
    Brim, L., Černá, I., Moravec, P., Šimša, J.: How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. In: Proc. of PDMC (2005)Google Scholar
  17. 17.
    Holzmann, G., Peled, D., Yannakakis, M.: On Nested Depth First Search. In: The SPIN Verification System, American Mathematical Society, pp. 23–32 (1996)Google Scholar
  18. 18.
    Vitter, J.S.: External memory algorithms and data structures: dealing with massive data. ACM Comput. Surv. 33(2), 209–271 (2001)CrossRefGoogle Scholar
  19. 19.
    Barnat, J., Brim, L., Černá, I., Šimeček, P.: DiVinE – The Distributed Verification Environment. In: Proc. of PDMC, pp. 89–94 (2005)Google Scholar
  20. 20.
    Dementiev, R., Kettner, L., Sanders, P.: STXXL: Standard Template Library for XXL Data Sets. In: Brodal, G.S., Leonardi, S. (eds.) ESA 2005. LNCS, vol. 3669, pp. 640–651. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  21. 21.
    Schuppan, V., Biere, A.: Efficient Reduction of Finite State Model Checking to Reachability Analysis. International Journal on Software Tools for Technology Transfer (STTT) 5(2–3), 185–204 (2004)CrossRefGoogle Scholar
  22. 22.
    Pelánek, R.: BEEM: Benchmarks for Explicit Model Checkers. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263–267. Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • J. Barnat
    • 1
  • L. Brim
    • 1
  • P. Šimeček
    • 1
  • M. Weber
    • 2
  1. 1.Masaryk University BrnoCzech Republic
  2. 2.University of TwenteThe Netherlands

Personalised recommendations