{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T22:34:28Z","timestamp":1784241268343,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540367499","type":"print"},{"value":"9783540367505","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11804192_13","type":"book-chapter","created":{"date-parts":[[2006,9,29]],"date-time":"2006-09-29T04:20:46Z","timestamp":1159503646000},"page":"259-279","source":"Crossref","is-referenced-by-count":18,"title":["Cluster-Based LTL Model Checking of Large Systems"],"prefix":"10.1007","author":[{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lubo\u0161","family":"Brim","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ivana","family":"\u010cern\u00e1","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/978-3-540-31980-1_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Bao","year":"2005","unstructured":"Bao, T., Jones, M.: Time-Efficient Model Checking with Magnetic Disks. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 526\u2013540. Springer, Heidelberg (2005)"},{"key":"13_CR2","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1109\/ASE.2003.1240299","volume-title":"Proc. 18th IEEE International Conference on Automated Software Engineering","author":"J. Barnat","year":"2003","unstructured":"Barnat, J., Brim, L., Chaloupka, J.: Parallel Breadth-First Search LTL Model-Checking. In: Proc. 18th IEEE International Conference on Automated Software Engineering, pp. 106\u2013115. IEEE Computer Society, Los Alamitos (2003)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-45139-0_13","volume-title":"Model Checking Software","author":"J. Barnat","year":"2001","unstructured":"Barnat, J., Brim, L., St\u0159\u00edbrn\u00e1, J.: Distributed LTL model-checking in SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 200\u2013216. Springer, Heidelberg (2001)"},{"key":"13_CR4","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I., \u0160ime\u010dek, P.: DiVinE \u2013 The Distributed Verification Environment. In: Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation, pp. 89\u201394 (2005)"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Barnat, J., \u010cern\u00e1, I.: Distributed Breadth-First Search LTL Model Checking. Formal Methods in System Design (to appear, 2006)","DOI":"10.1007\/s10703-006-0009-y"},{"key":"13_CR6","unstructured":"Barnat, J.: Distributed Memory LTL Model Checking. PhD thesis, Faculty of Informatics, Masaryk University Brno (2004)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/10722167_19","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"2000","unstructured":"Behrmann, G., Hune, T.S., Vaandrager, F.W.: Distributed Timed Model Checking \u2013 How the Search Order Matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 216\u2013231. Springer, Heidelberg (2000)"},{"issue":"1","key":"13_CR8","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s10009-003-0129-2","volume":"7","author":"A. Bell","year":"2005","unstructured":"Bell, A., Haverkort, B.R.: Sequential and distributed model checking of petrinet specifications. Int. J. Softw. Tools Technol. Transfer\u00a07(1), 43\u201360 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"1","key":"13_CR9","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1090\/qam\/102435","volume":"16","author":"R. Bellman","year":"1958","unstructured":"Bellman, R.: On a Routing Problem. Quarterly of Applied Mathematics\u00a016(1), 87\u201390 (1958)","journal-title":"Quarterly of Applied Mathematics"},{"issue":"1","key":"13_CR10","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/s10009-004-0159-4","volume":"7","author":"S. Blom","year":"2005","unstructured":"Blom, S., Orzan, S.: A Distributed Algorithm for Strong Bisimulation Reduction Of State Spaces. Int. J. Softw. Tools Technol. Transfer\u00a07(1), 74\u201386 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/3-540-45319-9_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Bollig","year":"2001","unstructured":"Bollig, B., Leucker, M., Weber, M.: Parallel Model Checking for the Alternation Free \u03bc-Calculus. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 543\u2013558. Springer, Heidelberg (2001)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-45294-X_9","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"L. Brim","year":"2001","unstructured":"Brim, L., \u010cern\u00e1, I., Kr\u010d\u00e1l, P., Pel\u00e1nek, R.: Distributed LTL Model Checking Based on Negative Cycle Detection. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, pp. 96\u2013107. Springer, Heidelberg (2001)"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/3-540-45627-9_16","volume-title":"SOFSEM 2001: Theory and Practice of Informatics","author":"L. Brim","year":"2001","unstructured":"Brim, L., \u010cern\u00e1, I., Kr\u010d\u00e1l, P., Pel\u00e1nek, R.: How to Employ Reverse Search in Distributed Single-Source Shortest Paths. In: Pacholski, L., Ru\u017ei\u010dka, P. (eds.) SOFSEM 2001. LNCS, vol.\u00a02234, pp. 191\u2013200. Springer, Heidelberg (2001)"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-540-30494-4_25","volume-title":"Formal Methods in Computer-Aided Design","author":"L. Brim","year":"2004","unstructured":"Brim, L., \u010cern\u00e1, I., Moravec, P., \u0160im\u0161a, 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.\u00a03312, pp. 352\u2013366. Springer, Heidelberg (2004)"},{"key":"13_CR15","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/j.entcs.2004.10.019","volume":"128","author":"L. Brim","year":"2005","unstructured":"Brim, L., \u010cern\u00e1, I., Moravec, P., \u0160im\u0161a, J.: Distributed Partial Order Reduction. Electronic Notes in Theoretical Computer Science\u00a0128, 63\u201374 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"13_CR16","unstructured":"Brim, L., \u010cern\u00e1, I., Moravec, P., \u0160im\u0161a, J.: How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. In: 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2005) (July 2005)"},{"key":"13_CR17","series-title":"Advances in Parallel Computing","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/S0927-5452(04)80040-6","volume-title":"Proc. Parallel Computing: Software Technology, Algorithms, Architectures & Applications","author":"L. Brim","year":"2004","unstructured":"Brim, L., \u010cern\u00e1, I., Hejtm\u00e1nek, L.: Distributed Negative Cycle Detection Algorithms. In: Proc. Parallel Computing: Software Technology, Algorithms, Architectures & Applications. Advances in Parallel Computing, vol.\u00a013, pp. 297\u2013305. Elsevier, Amsterdam (2004)"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-44829-2_4","volume-title":"Model Checking Software","author":"I. \u010cern\u00e1","year":"2003","unstructured":"\u010cern\u00e1, I., Pel\u00e1nek, R.: Distributed Explicit Fair cycle Detection (Set Based Approach). In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 49\u201373. Springer, Heidelberg (2003)"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-540-45138-9_26","volume-title":"Mathematical Foundations of Computer Science 2003","author":"I. \u010cern\u00e1","year":"2003","unstructured":"\u010cern\u00e1, I., Pel\u00e1nek, R.: Relating Hierarchy of Temporal Properties to Model Checking. In: Rovan, B., Vojt\u00e1\u0161, P. (eds.) MFCS 2003. LNCS, vol.\u00a02747, pp. 318\u2013327. Springer, Heidelberg (2003)"},{"key":"13_CR20","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s101070050058","volume":"85","author":"B.V. Cherkassky","year":"1999","unstructured":"Cherkassky, B.V., Goldberg, A.V.: Negative-Cycle Detection Algorithms. Mathematical Programming\u00a085, 277\u2013311 (1999)","journal-title":"Mathematical Programming"},{"key":"13_CR21","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT, Cambridge (1999)"},{"key":"13_CR22","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-Efficient Algorithms for the Verification of Temporal Properties. Formal Methods in System Design\u00a01, 275\u2013288 (1992)","journal-title":"Formal Methods in System Design"},{"key":"13_CR23","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/298595.298598","volume-title":"Proc. Workshop on Formal Methods in Software Practice","author":"M.B. Dwyer","year":"1998","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property Specification Patterns for Finite-State Verification. In: Proc. Workshop on Formal Methods in Software Practice, pp. 7\u201315. ACM Press, New York (1998)"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11691617_1","volume-title":"Model Checking Software","author":"S. Edelkamp","year":"2006","unstructured":"Edelkamp, S., Jabbar, S.: Large-Scale Directed Model Checking LTL. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 1\u201318. Springer, Heidelberg (2006)"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-31980-1_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Esparza","year":"2005","unstructured":"Esparza, J., Schwoon, S.: A note on on-the-fly verification algorithms. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 174\u2013190. Springer, Heidelberg (2005)"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-45319-9_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Fisler","year":"2001","unstructured":"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.\u00a02031, pp. 420\u2013434. Springer, Heidelberg (2001)"},{"key":"13_CR27","volume-title":"Network Flow Theory","author":"L.R. Ford","year":"1956","unstructured":"Ford, L.R.: Network Flow Theory. Rand Corp., Santa Monica (1956)"},{"key":"13_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/3-540-45139-0_14","volume-title":"Model Checking Software","author":"H. Garavel","year":"2001","unstructured":"Garavel, H., Mateescu, R., Smarandache, I.: Parallel State Space Construction for Model-Checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 216\u2013234. Springer, Heidelberg (2001)"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/11560548_12","volume-title":"Correct Hardware Design and Verification Methods","author":"O. Grumberg","year":"2005","unstructured":"Grumberg, O., Heyman, T., Ifergan, N., Schuster, A.: achieving speedups in distributed symbolic reachability analysis through asynchronous computation. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 129\u2013145. Springer, Heidelberg (2005)"},{"key":"13_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/3-540-44585-4_32","volume-title":"Computer Aided Verification","author":"O. Grumberg","year":"2001","unstructured":"Grumberg, O., Heyman, T., Schuster, A.: Distributed Model Checking for \u03bc-calculus. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 350\u2013362. Springer, Heidelberg (2001)"},{"key":"13_CR31","first-page":"12","volume-title":"Proc. 8th Int. Workshop on Petri Net and Performance Models","author":"B.R. Haverkort","year":"1999","unstructured":"Haverkort, B.R., Bell, A., Bohnenkamp, H.C.: On the Efficient Sequential and Distributed Generation of Very Large Markov Chains From Stochastic Petri Nets. In: Proc. 8th Int. Workshop on Petri Net and Performance Models, pp. 12\u201321. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"13_CR32","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"13_CR33","first-page":"23","volume-title":"Proc. SPIN Workshop on Model Checking of Software","author":"G.J. Holzmann","year":"1996","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On Nested Depth First Search. In: Proc. SPIN Workshop on Model Checking of Software, pp. 23\u201332. American Mathematical Society, Providence (1996)"},{"key":"13_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/11609773_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Jabbar","year":"2006","unstructured":"Jabbar, S., Edelkamp, S.: Parallel External Directed Model Checking with Linear I\/O. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 237\u2013251. Springer, Heidelberg (2006)"},{"key":"13_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-48234-2_3","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"F. Lerda","year":"1999","unstructured":"Lerda, F., Sisto, R.: Distributed-Memory Model Checking with SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 22\u201339. Springer, Heidelberg (1999)"},{"key":"13_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-24732-6_2","volume-title":"Model Checking Software","author":"R. Pel\u00e1nek","year":"2004","unstructured":"Pel\u00e1nek, R.: Typical Structural Properties of State Spaces. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 5\u201322. Springer, Heidelberg (2004)"},{"key":"13_CR37","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"Pnueli, A.: The Temporal Logic of Concurrent Programs. Theoretical Computer Science\u00a013, 45\u201360 (1981)","journal-title":"Theoretical Computer Science"},{"key":"13_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-40922-X_10","volume-title":"Formal Methods in Computer-Aided Design","author":"K. Ravi","year":"2000","unstructured":"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.\u00a01954, pp. 143\u2013160. Springer, Heidelberg (2000)"},{"issue":"5","key":"13_CR39","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/0020-0190(85)90024-9","volume":"20","author":"J. Reif","year":"1985","unstructured":"Reif, J.: Depth-first Search is Inherently Sequential. Information Proccesing Letters\u00a020(5), 229\u2013234 (1985)","journal-title":"Information Proccesing Letters"},{"key":"13_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/BFb0028743","volume-title":"Computer Aided Verification","author":"U. Stern","year":"1998","unstructured":"Stern, U., Dill, D.L.: Using magnetic disc instead of main memory in the mur\u03d5 verifier. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 172\u2013183. Springer, Heidelberg (1998)"},{"key":"13_CR41","doi-asserted-by":"crossref","unstructured":"Tarjan, R.: Depth First Search and Linear Graph Algorithms. SIAM Journal on Computing, 146\u2013160 (January, 1972)","DOI":"10.1137\/0201010"},{"key":"13_CR42","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. IEEE Symposium on Logic in Computer Science, pp. 322\u2013331. Computer Society Press (1986)"},{"key":"13_CR43","unstructured":"\u0160ime\u010dek, P.: DiVinE \u2013 Distributed Verification Environment. Master\u2019s thesis, Masaryk Univeristy Brno (2006)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11804192_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,11]],"date-time":"2019-03-11T08:24:16Z","timestamp":1552292656000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11804192_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540367499","9783540367505"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/11804192_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}