{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214001},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540430025"},{"type":"electronic","value":"9783540452942"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45294-x_9","type":"book-chapter","created":{"date-parts":[[2007,6,12]],"date-time":"2007-06-12T02:45:12Z","timestamp":1181616312000},"page":"96-107","source":"Crossref","is-referenced-by-count":23,"title":["Distributed LTL Model Checking Based on Negative Cycle Detection"],"prefix":"10.1007","author":[{"given":"Lubo\u0161","family":"Brim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ivana","family":"\u010cern\u00e1","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pavel","family":"Kr\u010d\u00e1l","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radek","family":"Pel\u00e1nek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,11,26]]},"reference":[{"key":"9_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/BFb0042303","volume-title":"Discrete Event Systems: Models and Application","author":"S. Aggarwal","year":"1987","unstructured":"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\u201356. Springer, 1987."},{"key":"9_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-45139-0_13","volume-title":"DistributedLTL Model-Checking in SPIN","author":"J. Barnat","year":"2001","unstructured":"J. Barnat, L. Brim, and J. St\u0159\u00edbrn\u00e1. DistributedLTL Model-Checking in SPIN. In Proc. SPIN 2001, volume 2057 of LNCS, pages 200\u2013216. Springer, 2001."},{"key":"9_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/10722167_19","volume-title":"Distributed timed model checking \u2014 how the search order matters","author":"G. Behrmann","year":"2000","unstructured":"G. Behrmann, T. S. Hune, and F. W. Vaandrager. Distributed timed model checking \u2014 how the search order matters. In Proc. CAV 2000, volume 1855 of LNCS, pages 216\u2013231. Springer, 2000."},{"doi-asserted-by":"crossref","unstructured":"S. Ben-David, T. Heyman, O. Grumberg, and A. Schuster. Scalable distributed on-the-fly symbolic model checking. In Proc. FMCAD 2000, 2000.","key":"9_CR4","DOI":"10.1007\/3-540-40922-X_24"},{"key":"9_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1007\/3-540-45319-9_37","volume-title":"Parallel model checking for the alternation free mu-calculus","author":"B. Bollig","year":"2001","unstructured":"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\u2013558. Springer, 2001."},{"unstructured":"L. Brim, I. \u010cern\u00e1, P. Kr\u010d\u00e1l, and R. Pel\u00e1nek. 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.","key":"9_CR6"},{"key":"9_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-60313-1_132","volume-title":"Shortest path queries in digraphs of small treewidth","author":"S. Chaudhuri","year":"1995","unstructured":"S. Chaudhuri and C. D. Zaroliagis. Shortest path queries in digraphs of small treewidth. In Proc. ESA 1995, volume 979 of LNCS, pages 31\u201345. Springer, 1995."},{"key":"9_CR8","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s101070050058","volume":"85","author":"B. V. Cherkassky","year":"1999","unstructured":"B. V. Cherkassky and A. V. Goldberg. Negative-cycle detection algorithms. Mathematical Programming, (85):277\u2013311, 1999.","journal-title":"Mathematical Programming"},{"key":"9_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/3-540-44577-3_12","volume-title":"Informatics-10 Years Back. 10 Years Ahead","author":"E.M. Clarke","year":"2001","unstructured":"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\u2013194. Springer, 2001."},{"issue":"2","key":"9_CR10","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1006\/jagm.1996.0048","volume":"21","author":"E. Cohen","year":"1996","unstructured":"E. Cohen. Efficient parallel shortest-paths in digraphs with a separator decomposition. Journal of Algorithms, 21(2):331\u2013357, 1996.","journal-title":"Journal of Algorithms"},{"unstructured":"T. H. Cormen, Ch. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. MIT, 1990.","key":"9_CR11"},{"key":"9_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"722","DOI":"10.1007\/BFb0055823","volume-title":"A parallelization of Dijkstra\u2019s shortest path algorithm","author":"A. Crauser","year":"1998","unstructured":"A. Crauser, K. Mehlhorn, U. Meyer, and P. Sanders. A parallelization of Dijkstra\u2019s shortest path algorithm. In Proc. MFCS 1998, volume 1450 of LNCS, pages 722\u2013731. Springer, 1998."},{"key":"9_CR13","series-title":"Lect Notes Comput Sci","first-page":"270","volume-title":"Efficient sequential and parallel algorithms for the negative cycle problem","author":"P. Spirakis","year":"1994","unstructured":"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\u2013278. Springer, 1994."},{"key":"9_CR14","series-title":"Lect Notes Comput Sci","volume-title":"Distributed model checking for mucalculus","author":"O. Grumberg","year":"2001","unstructured":"O. Grumberg, T. Heyman, and A. Schuster. Distributed model checking for mucalculus. In Proc. 13th Conference on Computer-Aided Verification CAV01, LNCS. Springer, 2001."},{"key":"9_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/10722167_6","volume-title":"Achieving scalability in parallel reachability analysis of very large circuits","author":"T. Heyman","year":"2000","unstructured":"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\u201335. Springer, 2000."},{"issue":"5","key":"9_CR16","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279\u2013295, 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"doi-asserted-by":"crossref","unstructured":"G.J. Holzmann, D. Peled, and M. Yannakakis. On nested depth first search. In The Spin Verification System, pages 23\u201332. American Mathematical Society, 1996.","key":"9_CR17","DOI":"10.1090\/dimacs\/032\/03"},{"key":"9_CR18","series-title":"Lect Notes Comput Sci","volume-title":"Distributed-memory model checking with SPIN","author":"F. Lerda","year":"1999","unstructured":"F. Lerda and R. Sisto. Distributed-memory model checking with SPIN. In Proc. SPIN 1999, number 1680 in LNCS. Springer, 1999."},{"key":"9_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Parallel shortest path for arbitrary graphs","author":"U. Meyer","year":"2000","unstructured":"U. Meyer and P. Sanders. Parallel shortest path for arbitrary graphs. In Proc. EUROPAR 2000. LNCS, 2000."},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0196-6774(92)90017-7","volume":"13","author":"K. Ramarao","year":"1992","unstructured":"K. Ramarao and S. Venkatesan. On finding and updating shortest paths distributively. Journal of Algorithms, 13:235\u2013257, 1992.","journal-title":"Journal of Algorithms"},{"issue":"5","key":"9_CR21","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/0020-0190(85)90024-9","volume":"20","author":"J.H. Reif","year":"1985","unstructured":"J.H. Reif. Depth-first search is inherrently sequential. Information Processing Letters, 20(5):229\u2013234, 1985.","journal-title":"Information Processing Letters"},{"doi-asserted-by":"crossref","unstructured":"S.H. Roosta. Parallel processing and parallel algorithms. Springer, 2000.","key":"9_CR22","DOI":"10.1007\/978-1-4612-1220-1"},{"key":"9_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/3-540-63166-6_26","volume-title":"Parallelizing the Mur\u03c6 verifier","author":"U. Stern","year":"1997","unstructured":"U. Stern and D.L. Dill. Parallelizing the Mur\u03c6 verifier. In Proc. CAV 1997, volume 1254 of LNCS, pages 256\u2013267. Springer, 1997."},{"doi-asserted-by":"crossref","unstructured":"R. Tarjan. Depth first search and linear graph algorithms. SIAM Journal on computing, pages 146\u2013160, 1972.","key":"9_CR24","DOI":"10.1137\/0201010"},{"key":"9_CR25","series-title":"Lect Notes Comput Sci","first-page":"183","volume-title":"A simple parallel algorithm for the single-source shortest path problem on planar digraphs","author":"J. Tra","year":"1996","unstructured":"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\u2013194S. Springer, 1996."},{"unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. LICS 1986, pages 332\u2013344. Computer Society Press, 1986.","key":"9_CR26"}],"container-title":["Lecture Notes in Computer Science","FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45294-X_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T01:28:02Z","timestamp":1556501282000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45294-X_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540430025","9783540452942"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-45294-x_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}