Distributed LTL Model Checking Based on Negative Cycle Detection

  • Luboš Brim
  • Ivana Černá
  • Pavel Krčál
  • Radek Pelánek
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2245)


This paper addresses the state explosion problem in automata based LTL model checking. To deal with large space requirements we turn to use a distributed approach. All the known methods for automata based model checking are basedon depth first traversal of the state space which is difficult to parallelise as the ordering in which vertices are visited plays an important role. We come up with entirely different approach which is dependent on locating cycles with negative length in a directed graph with real number length of edges. Our method allows reasonable distribution and the experimental results confirm its usefulness for distributed model checking.


Model Check Negative Cycle Symbolic Model Check Model Check Problem Source Vertex 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    S. Aggarwal, R. Alonso, and C. Courcoubetis. Distributed reachability analysis for protocol verification environments. In Discrete Event Systems: Models and Application, volume 103 of LNCS, pages 40–56. Springer, 1987.CrossRefGoogle Scholar
  2. 2.
    J. Barnat, L. Brim, and J. Stříbrná. DistributedLTL Model-Checking in SPIN. In Proc. SPIN 2001, volume 2057 of LNCS, pages 200–216. Springer, 2001.CrossRefGoogle Scholar
  3. 3.
    G. Behrmann, T. S. Hune, and F. W. Vaandrager. Distributed timed model checking — how the search order matters. In Proc. CAV 2000, volume 1855 of LNCS, pages 216–231. Springer, 2000.Google Scholar
  4. 4.
    S. Ben-David, T. Heyman, O. Grumberg, and A. Schuster. Scalable distributed on-the-fly symbolic model checking. In Proc. FMCAD 2000, 2000.Google Scholar
  5. 5.
    B. Bollig, M. Leucker, and M Weber. Parallel model checking for the alternation free mu-calculus. In Proc. TACAS 2001, volume 2031 of LNCS, pages 543–558. Springer, 2001.Google Scholar
  6. 6.
    L. Brim, I. Černá, P. Krčál, and R. Pelánek. Distributed shortest path for directed graphs with negative edge lengths. Technical Report FIMU-RS-2001-01, Faculty of Informatics, Masaryk University Brno,, 2001.
  7. 7.
    S. Chaudhuri and C. D. Zaroliagis. Shortest path queries in digraphs of small treewidth. In Proc. ESA 1995, volume 979 of LNCS, pages 31–45. Springer, 1995.Google Scholar
  8. 8.
    B. V. Cherkassky and A. V. Goldberg. Negative-cycle detection algorithms. Mathematical Programming, (85):277–311, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Progress on the state explosion problem in model checking. In Informatics-10 Years Back. 10 Years Ahead, volume 2000 of LNCS, pages 176–194. Springer, 2001.Google Scholar
  10. 10.
    E. Cohen. Efficient parallel shortest-paths in digraphs with a separator decomposition. Journal of Algorithms, 21(2):331–357, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    T. H. Cormen, Ch. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. MIT, 1990.Google Scholar
  12. 12.
    A. Crauser, K. Mehlhorn, U. Meyer, and P. Sanders. A parallelization of Dijkstra’s shortest path algorithm. In Proc. MFCS 1998, volume 1450 of LNCS, pages 722–731. Springer, 1998.Google Scholar
  13. 13.
    P. Spirakis D. Kavvadias, G. Pantziou and C. Zaroliagis. Efficient sequential and parallel algorithms for the negative cycle problem. In Proc. ISAAC 1994, volume 834 of LNCS, pages 270–278. Springer, 1994.Google Scholar
  14. 14.
    O. Grumberg, T. Heyman, and A. Schuster. Distributed model checking for mucalculus. In Proc. 13th Conference on Computer-Aided Verification CAV01, LNCS. Springer, 2001.Google Scholar
  15. 15.
    T. Heyman, D. Geist, O. Grumberg, and A. Schuster. Achieving scalability in parallel reachability analysis of very large circuits. In Proc. CAV 2000, volume 1855 of LNCS, pages 20–35. Springer, 2000.Google Scholar
  16. 16.
    G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–295, 1997.CrossRefMathSciNetGoogle Scholar
  17. 17.
    G.J. Holzmann, D. Peled, and M. Yannakakis. On nested depth first search. In The Spin Verification System, pages 23–32. American Mathematical Society, 1996.Google Scholar
  18. 18.
    F. Lerda and R. Sisto. Distributed-memory model checking with SPIN. In Proc. SPIN 1999, number 1680 in LNCS. Springer, 1999.Google Scholar
  19. 19.
    U. Meyer and P. Sanders. Parallel shortest path for arbitrary graphs. In Proc. EUROPAR 2000. LNCS, 2000.Google Scholar
  20. 20.
    K. Ramarao and S. Venkatesan. On finding and updating shortest paths distributively. Journal of Algorithms, 13:235–257, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    J.H. Reif. Depth-first search is inherrently sequential. Information Processing Letters, 20(5):229–234, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    S.H. Roosta. Parallel processing and parallel algorithms. Springer, 2000.Google Scholar
  23. 23.
    U. Stern and D.L. Dill. Parallelizing the Murφ verifier. In Proc. CAV 1997, volume 1254 of LNCS, pages 256–267. Springer, 1997.Google Scholar
  24. 24.
    R. Tarjan. Depth first search and linear graph algorithms. SIAM Journal on computing, pages 146–160, 1972.Google Scholar
  25. 25.
    J. Tra. and C.D. Zaroliagis. A simple parallel algorithm for the single-source shortest path problem on planar digraphs. In Proc. IRREGULAR-3 1996, volume 1117 of LNCS, pages 183–194S. Springer, 1996.Google Scholar
  26. 26.
    M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. LICS 1986, pages 332–344. Computer Society Press, 1986.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Luboš Brim
    • 1
  • Ivana Černá
    • 1
  • Pavel Krčál
    • 1
  • Radek Pelánek
    • 1
  1. 1.Department of Computer Science, Faculty of InformaticsMasaryk University BrnoCzech Republic

Personalised recommendations