Distributed LTL Model Checking Based on Negative Cycle Detection
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.
KeywordsModel Check Negative Cycle Symbolic Model Check Model Check Problem Source Vertex
Unable to display preview. Download preview PDF.
- 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.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.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.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, http://www...muni.cz/informatics/reports/, 2001.
- 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
- 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
- 11.T. H. Cormen, Ch. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. MIT, 1990.Google Scholar
- 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.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.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.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
- 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.F. Lerda and R. Sisto. Distributed-memory model checking with SPIN. In Proc. SPIN 1999, number 1680 in LNCS. Springer, 1999.Google Scholar
- 19.U. Meyer and P. Sanders. Parallel shortest path for arbitrary graphs. In Proc. EUROPAR 2000. LNCS, 2000.Google Scholar
- 22.S.H. Roosta. Parallel processing and parallel algorithms. Springer, 2000.Google Scholar
- 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.R. Tarjan. Depth first search and linear graph algorithms. SIAM Journal on computing, pages 146–160, 1972.Google Scholar
- 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.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