{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T16:54:29Z","timestamp":1742403269128},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540331025"},{"type":"electronic","value":"9783540331032"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11691617_1","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T09:14:13Z","timestamp":1143537253000},"page":"1-18","source":"Crossref","is-referenced-by-count":32,"title":["Large-Scale Directed Model Checking LTL"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Edelkamp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shahid","family":"Jabbar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/3-540-18088-5_40","volume-title":"Automata, Languages and Programming","author":"A. Aggarwal","year":"1987","unstructured":"Aggarwal, A., Vitter, J.S.: Complexity of sorting and related problems. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol.\u00a0267, pp. 467\u2013478. Springer, Heidelberg (1987)"},{"issue":"9","key":"1_CR2","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. Journal of the ACM\u00a031(9), 1116\u20131127 (1988)","journal-title":"Journal of the ACM"},{"key":"1_CR3","unstructured":"Barnat, J., Brim, L., Cerna, I.: Property driven distribution of nested DFS. In: International Workshop on Verification and Computational Logic (VCL), pp. 1\u201310 (2002)"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Chaloupka, J.: Parallel breadth-first search LTL model checking. In: International Conference on Automated Software Engineering (ASE), pp. 106\u2013115 (2003)","DOI":"10.1109\/ASE.2003.1240299"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.entcs.2004.08.056","volume":"133","author":"J. Barnat","year":"2005","unstructured":"Barnat, J., Brim, L., Chaloupka, J.: From distribution memory cycle detection to parallel model checking. Electronic Notes in Theoretical Computer Science\u00a0133, 21\u201339 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"1_CR6","volume-title":"Advances in Computers","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. In: Advances in Computers, vol.\u00a058. Academic Press, London (2003)"},{"key":"1_CR7","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., Cerna, I.: 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":"1_CR8","unstructured":"Buchi, J.R.: On a decision method in restricted second order arithmetic. In: Conference on Logic, Methodology, and Philosophy of Science, pp. 1\u201311 (1962)"},{"key":"1_CR9","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. Cerna","year":"2003","unstructured":"Cerna, I., Palanek, R.: Distributed explicit fair cycle detection. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 49\u201373. Springer, Heidelberg (2003)"},{"key":"1_CR10","unstructured":"Chiang, Y.-J., Goodrich, M.T., Grove, E.F., Tamasia, R., Vengroff, D.E., Vitter, J.S.: External memory graph algorithms. In: Symposium on Discrete Algorithms (SODA), pp. 139\u2013149 (1995)"},{"key":"1_CR11","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"1_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-540-30221-6_18","volume-title":"KI 2004: Advances in Artificial Intelligence","author":"S. Edelkamp","year":"2004","unstructured":"Edelkamp, S., Jabbar, S., Schroedl, S.: External A*. In: Biundo, S., Fr\u00fchwirth, T., Palm, G. (eds.) KI 2004. LNCS (LNAI), vol.\u00a03238, pp. 226\u2013240. Springer, Heidelberg (2004)"},{"issue":"2-3","key":"1_CR13","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10009-002-0104-3","volume":"5","author":"S. Edelkamp","year":"2004","unstructured":"Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. International Journal on Software Tools for Technology\u00a05(2-3), 247\u2013267 (2004)","journal-title":"International Journal on Software Tools for Technology"},{"issue":"4","key":"1_CR14","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s10009-004-0151-z","volume":"6","author":"S. Edelkamp","year":"2004","unstructured":"Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Partial order reduction and trail improvement in directed model checking. International Journal on Software Tools for Technology\u00a06(4), 277\u2013301 (2004)","journal-title":"International Journal on Software Tools for Technology"},{"key":"1_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, Y., Ynag, Y.: Is there a best symbolic cycle detection algorithm. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 420\u2013434. Springer, Heidelberg (2001)"},{"issue":"6","key":"1_CR16","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1145\/360825.360861","volume":"18","author":"D.S. Hirschberg","year":"1975","unstructured":"Hirschberg, D.S.: A linear space algorithm for computing common subsequences. Communications of the ACM\u00a018(6), 341\u2013343 (1975)","journal-title":"Communications of the ACM"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. The SPIN Verification System, 23\u201332 (1972)","DOI":"10.1090\/dimacs\/032\/03"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"1_CR19","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":"2005","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 (2005)"},{"key":"1_CR20","unstructured":"Kautz, H., Selman, B.: Pushing the envelope: Planning propositional logic, and stochastic search. In: AAAI, pp. 1194\u20131201 (1996)"},{"key":"1_CR21","unstructured":"Korf, R.E.: Best-first frontier search with delayed duplicate detection. In: AAAI, pp. 650\u2013657 (2004)"},{"key":"1_CR22","unstructured":"Korf, R.E., Schultze, P.: Large-scale parallel breadth-first search. In: AAAI (2005)"},{"key":"1_CR23","unstructured":"Korf, R.E., Zhang, W.: Divide-and-conquer frontier search applied to optimal sequence allignment. In: AAAI, pp. 910\u2013916 (2000)"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"1_CR25","unstructured":"Lluch-Lafuente, A.: Simplified distributed ltl model checking by localizing cycles. Technical report, Institute of Computer Science, University of Freiburg (2002)"},{"key":"1_CR26","unstructured":"Lluch-Lafuente, A.: Directed Search for the Verification of Communication Protocols. PhD thesis, Institute of Computer Science, University of Freiburg (2003)"},{"key":"1_CR27","unstructured":"Munagala, K., Ranade, A.: I\/O-complexity of graph algorithms. In: Symposium on Discrete Algorithms (SODA), pp. 87\u201388 (2001)"},{"key":"1_CR28","volume-title":"Heuristics","author":"J. Pearl","year":"1985","unstructured":"Pearl, J.: Heuristics. Addison-Wesley, Reading (1985)"},{"key":"1_CR29","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 inherently sequential. Information Processing Letters\u00a020, 229\u2013234 (1985)","journal-title":"Information Processing Letters"},{"key":"1_CR30","first-page":"319","volume-title":"Annual Symposium on Foundations of Computer Science","author":"S. Safra","year":"1998","unstructured":"Safra, S.: On the complexity of omega-automata. In: Annual Symposium on Foundations of Computer Science, pp. 319\u2013327. IEEE Computer Society, Los Alamitos (1998)"},{"key":"1_CR31","volume-title":"Algorithms for Memory Hierarchies","author":"P. Sanders","year":"2002","unstructured":"Sanders, P., Meyer, U., Sibeyn, J.F.: Algorithms for Memory Hierarchies. Springer, Heidelberg (2002)"},{"key":"1_CR32","unstructured":"Schuppan, V., Biere, A.: From distribution memory cycle detection to parallel model checking. International Journal on Software Tools for Technology Transfer\u00a05(2\u20133)"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Schuppan, V., Biere, A.: Liveness checking as safety checking for infinite state spaces (2005) (to appear)","DOI":"10.1016\/j.entcs.2005.11.018"},{"issue":"2-3","key":"1_CR34","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1983","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Buchi automata with applications to temporal logic. Theoretical Computer Science\u00a049(2-3), 217\u2013237 (1983)","journal-title":"Theoretical Computer Science"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Tarjan, R.: Depth-first search and linear graph algorithms. SIAM Journal of Computing\u00a0(1), 146\u2013160 (1972)","DOI":"10.1137\/0201010"},{"key":"1_CR36","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Information and Control\u00a056, 72\u201399 (1983)","journal-title":"Information and Control"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Zhang, W.: Model checking operator procedures. In: Workshop on Model Checking Software (SPIN), pp. 200\u2013215 (1999)","DOI":"10.1007\/3-540-48234-2_16"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11691617_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,17]],"date-time":"2019-04-17T13:18:53Z","timestamp":1555507133000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11691617_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540331025","9783540331032"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/11691617_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}