{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T08:40:42Z","timestamp":1780562442032,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540733676","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_32","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T22:29:34Z","timestamp":1188426574000},"page":"281-293","source":"Crossref","is-referenced-by-count":18,"title":["I\/O Efficient Accepting Cycle Detection"],"prefix":"10.1007","author":[{"given":"Jiri","family":"Barnat","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lubos","family":"Brim","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pavel","family":"\u0160ime\u010dek","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"9","key":"32_CR1","doi-asserted-by":"publisher","first-page":"1116","DOI":"10.1145\/48529.48535","volume":"31","author":"A. Aggarwal","year":"1988","unstructured":"Aggarwal, A., Vitter, J.S.: The Input\/Output Complexity of Sorting and Related Problems. Communications of the ACM\u00a031(9), 1116\u20131127 (1988)","journal-title":"Communications of the ACM"},{"key":"32_CR2","unstructured":"Barnat, J.: Distributed Memory LTL Model Checking. PhD thesis, Faculty of Informatics, Masaryk University Brno (2004)"},{"key":"32_CR3","first-page":"106","volume-title":"ASE 2003","author":"J. Barnat","year":"2003","unstructured":"Barnat, J., Brim, L., Chaloupka, J.: Parallel Breadth-First Search LTL Model-Checking. In: ASE 2003. Automated Software Engineering, pp. 106\u2013115. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"32_CR4","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.) Model Checking Software. LNCS, vol.\u00a02057, pp. 200\u2013216. Springer, Heidelberg (2001)"},{"key":"32_CR5","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I., \u0160ime\u010dek, P.: DiVinE \u2013 The Distributed Verification Environment. In: PDMC 2005, pp. 89\u201394 (2005)"},{"key":"32_CR6","unstructured":"Barnat, J., Brim, L., \u0160ime\u010dek, P.: LTL Model Checking with I\/O-Efficient Accepting Cycle Detection. Technical Report FIMU-RS-2007-01, Faculty of Informatics, Masaryk University (2007)"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness Checking as Safety Checking. Electr. Notes Theor. Comput. Sci. 66(2) (2002)","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"32_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"32_CR9","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.) FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science. LNCS, vol.\u00a02245, pp. 96\u2013107. Springer, Heidelberg (2001)"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. In: Ball, T., Rajamani, S.K. (eds.) Model Checking Software. LNCS, vol.\u00a02648, pp. 49\u201373. Springer, Heidelberg (2003)"},{"key":"32_CR11","unstructured":"Chiang, Y., Goodrich, M., Grove, E., Tamassia, R., Vengroff, D., Vitter, J.: External-Memory Graph Algorithms. In: SODA 1995, pp. 139\u2013149. Society for Industrial and Applied Mathematics (1995)"},{"key":"32_CR12","volume-title":"Model Checking","author":"E. Clarke Jr.","year":"1999","unstructured":"Clarke Jr., E., Grumberg, O., Peled, D.: Model Checking. MIT press, Cambridge (1999)"},{"key":"32_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/11561071_57","volume-title":"Algorithms \u2013 ESA 2005","author":"R. Dementiev","year":"2005","unstructured":"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.\u00a03669, pp. 640\u2013651. Springer, Heidelberg (2005)"},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Jabbar, S.: Large-Scale Directed Model Checking LTL. In: SPIN 2006, pp. 1\u201318 (2006)","DOI":"10.1007\/11691617_1"},{"key":"32_CR15","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":"32_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-70952-7_4","volume-title":"Formal Methods: Applications and Technology","author":"M. Hammer","year":"2006","unstructured":"Hammer, M., Weber, M.: To Store Or Not To Store Reloaded: Reclaiming Memory On Demand. In: FMICS 2006 and PDMC 2006. LNCS, vol.\u00a04346, pp. 51\u201366. Springer, Heidelberg (2006)"},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On Nested Depth First Search. In: The SPIN Verification System, pp. 23\u201332. American Mathematical Society (1996)","DOI":"10.1090\/dimacs\/032\/03"},{"key":"32_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/978-3-540-30579-8_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Jabbar","year":"2005","unstructured":"Jabbar, S., Edelkamp, S.: I\/O Efficient Directed Model Checking. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 313\u2013329. Springer, Heidelberg (2005)"},{"key":"32_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/978-3-540-24732-6_10","volume-title":"Model Checking Software","author":"M. Jones","year":"2004","unstructured":"Jones, M., Mercer, E.: Explicit State Model Checking with Hopper. In: Graf, S., Mounier, L. (eds.) Model Checking Software. LNCS, vol.\u00a02989, pp. 146\u2013150. Springer, Heidelberg (2004)"},{"key":"32_CR20","doi-asserted-by":"crossref","unstructured":"Katriel, I., Meyer, U.: Elementary Graph Algorithms in External Memory. In: Algorithms for Memory Hierarchies, pp. 62\u201384 (2002)","DOI":"10.1007\/3-540-36574-5_4"},{"key":"32_CR21","first-page":"650","volume-title":"AAAI 2004","author":"R. Korf","year":"2004","unstructured":"Korf, R.: Best-First Frontier Search with Delayed Duplicate Detection. In: AAAI 2004, pp. 650\u2013657. AAAI Press \/ The MIT Press, Cambridge, MA (2004)"},{"key":"32_CR22","first-page":"1380","volume-title":"AAAI 2005","author":"R. Korf","year":"2005","unstructured":"Korf, R., Schultze, P.: Large-Scale Parallel Breadth-First Search. In: AAAI 2005, pp. 1380\u20131385. AAAI Press \/ The MIT Press, Cambridge, MA (2005)"},{"key":"32_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/978-3-540-39893-6_19","volume-title":"Formal Methods and Software Engineering","author":"L. Kristensen","year":"2003","unstructured":"Kristensen, L., Mailund, T.: Efficient Path Finding with the Sweep-Line Method Using External Storage. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol.\u00a02885, pp. 319\u2013337. Springer, Heidelberg (2003)"},{"key":"32_CR24","volume-title":"SPDP 1996","author":"V. Kumar","year":"1996","unstructured":"Kumar, V., Schwabe, E.: Improved Algorithms and Data Structures for Solving Graph Problems in External Memory. In: SPDP 1996. 8th IEEE Symposium on Parallel and Distributed Processing, IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"32_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"723","DOI":"10.1007\/3-540-45749-6_63","volume-title":"Algorithms - ESA 2002","author":"K. Mehlhorn","year":"2002","unstructured":"Mehlhorn, K., Meyer, U.: External-Memory Breadth-First Search with Sublinear I\/O. In: M\u00f6hring, R.H., Raman, R. (eds.) ESA 2002. LNCS, vol.\u00a02461, pp. 723\u2013735. Springer, Heidelberg (2002)"},{"key":"32_CR26","unstructured":"Munagala, K., Ranade, A.: I\/O-Complexity of Graph Algorithms. In: SODA 1999, pp. 687\u2013694, Philadelphia, PA, USA, Society for Industrial and Applied Mathematics (1999)"},{"key":"32_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.) Model Checking Software. LNCS, vol.\u00a02989, pp. 5\u201322. Springer, Heidelberg (2004)"},{"key":"32_CR28","unstructured":"Pel\u00e1nek, R.: BEEM: BEnchmarks for Explicit Model checkers (February 2007), http:\/\/anna.fi.muni.cz\/models\/index.html"},{"key":"32_CR29","series-title":"Lecture Notes in Computer Science","first-page":"143","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":"32_CR30","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/0020-0190(85)90024-9","volume":"20","author":"J.H. Reif","year":"1985","unstructured":"Reif, J.H.: Depth-First Search is Inherrently Sequential. Information Processing Letters\u00a020(5), 229\u2013234 (1985)","journal-title":"Information Processing Letters"},{"issue":"2\u20133","key":"32_CR31","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-003-0121-x","volume":"5","author":"V. Schuppan","year":"2004","unstructured":"Schuppan, V., Biere, A.: Efficient Reduction of Finite State Model Checking to Reachability Analysis. International Journal on Software Tools for Technology Transfer (STTT)\u00a05(2\u20133), 185\u2013204 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"32_CR32","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 Disk Instead of Main Memory in the Murphi Verifier. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 172\u2013183. Springer, Heidelberg (1998)"},{"key":"32_CR33","first-page":"332","volume-title":"LICS 1986","author":"M. Vardi","year":"1986","unstructured":"Vardi, M., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification. In: LICS 1986. Logic in Computer Science, pp. 332\u2013344. IEEE Computer Society Press, Los Alamitos (1986)"},{"issue":"2","key":"32_CR34","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/384192.384193","volume":"33","author":"J. Vitter","year":"2001","unstructured":"Vitter, J.: External Memory Algorithms and Data Structures: Dealing with Massive Data. ACM Comput. Surv.\u00a033(2), 209\u2013271 (2001)","journal-title":"ACM Comput. Surv."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73368-3_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:08:32Z","timestamp":1619518112000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_32","relation":{},"subject":[]}}