{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:52:50Z","timestamp":1725490370160},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540741275"},{"type":"electronic","value":"9783540741282"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74128-2_5","type":"book-chapter","created":{"date-parts":[[2007,8,27]],"date-time":"2007-08-27T02:05:15Z","timestamp":1188180315000},"page":"67-83","source":"Crossref","is-referenced-by-count":2,"title":["Real-Time Model Checking on Secondary Storage"],"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":[{"issue":"9","key":"5_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. Journal of the ACM\u00a031(9), 1116\u20131127 (1988)","journal-title":"Journal of the ACM"},{"issue":"2","key":"5_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/3-540-57155-8_238","volume-title":"Algorithms and Data Structures","author":"L. Arge","year":"1993","unstructured":"Arge, L., Knudsen, M., Larsen, K.: Sorting multisets and vectors in-place. In: Dehne, F., Sack, J.-R., Santoro, N. (eds.) WADS 1993. LNCS, vol.\u00a0709, pp. 83\u201394. Springer, Heidelberg (1993)"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"G. Behrman","year":"2000","unstructured":"Behrman, G., Fehnker, A., Vaandrager, F.: Distributed timed model checking - how the search order matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"doi-asserted-by":"crossref","unstructured":"Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Optimal scheduling using priced timed automata. In: ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (2005)","key":"5_CR5","DOI":"10.1145\/1059816.1059823"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_9","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"F. Cassez","year":"2005","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, Springer, Heidelberg (2005)"},{"unstructured":"Dierks, H.: Finding optimal plans for domains with restricted continuous effects with cora. In: ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (2005)","key":"5_CR7"},{"key":"5_CR8","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.) Model Checking Software. LNCS, vol.\u00a03925, pp. 1\u201318. Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Jabbar, S., Schroedl, S.: External A*. In: German Conference on Artificial Intelligence (KI), pp. 226\u2013240 (2004)","key":"5_CR9","DOI":"10.1007\/978-3-540-30221-6_18"},{"doi-asserted-by":"crossref","unstructured":"Ginsberg, M., Harvey, W.: Iterative broadening. Artificial Intelligence, pp. 367\u2013383 (1992)","key":"5_CR10","DOI":"10.1016\/0004-3702(92)90059-7"},{"doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? In: ACM STOC, pp. 373\u2013381 (1995)","key":"5_CR11","DOI":"10.1145\/225058.225162"},{"issue":"6","key":"5_CR12","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":"5_CR13","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":"5_CR14","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)"},{"unstructured":"Korf, R.E.: Divide-and-conquer bidirectional search: First results. In: IJCAI, pp. 1184\u20131191 (1999)","key":"5_CR15"},{"unstructured":"Korf, R.E., Schultze, P.: Large-scale parallel breadth-first search. In: AAAI, pp. 1380\u20131385 (2005)","key":"5_CR16"},{"unstructured":"Korf, R.E., Zhang, W.: Divide-and-conquer frontier search applied to optimal sequence allignment. In: AAAI, pp. 910\u2013916 (2000)","key":"5_CR17"},{"key":"5_CR18","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.: 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":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/11691617_3","volume-title":"Model Checking Software","author":"S. Kupferschmid","year":"2006","unstructured":"Kupferschmid, S., Hoffmann, J., Dierks, H., Behrmann, G.: Adapting an AI planning heuristic for directed model checking. In: Valmari, A. (ed.) Model Checking Software. LNCS, vol.\u00a03925, pp. 35\u201352. Springer, Heidelberg (2006)"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/3-540-44585-4_47","volume-title":"Computer Aided Verification","author":"K.G. Larsen","year":"2001","unstructured":"Larsen, K.G., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T.S., Petterson, P., Romijn, J.: As cheap as possible: Efficient cost-optimal reachability for priced timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 493\u2013505. Springer, Heidelberg (2001)"},{"doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Larsson, F., Petterson, P., Yi, W.: Efficient verification of real-time systems: Compact data structures and state-space reduction. In: IEEE Real Time Systems Symposium, pp. 14\u201324 (1997)","key":"5_CR21","DOI":"10.1109\/REAL.1997.641265"},{"unstructured":"Munagala, K., Ranade, A.: I\/O-complexity of graph algorithms. In: SODA, pp. 687\u2013694 (1999)","key":"5_CR22"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1007\/978-3-540-24730-2_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.I. Rasmussen","year":"2004","unstructured":"Rasmussen, J.I., Larsen, K.G., Subramani, K.: Resource-optimal scheduling using priced timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 220\u2013235. Springer, Heidelberg (2004)"},{"key":"5_CR24","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":"5_CR25","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.: 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)"},{"unstructured":"Zhou, R., Hansen, E.: Breadth-first heuristic search. In: ICAPS, pp. 92\u2013100 (2004)","key":"5_CR26"},{"unstructured":"Zhou, R., Hansen, E.: External-memory pattern databases using structured duplicate detection. In: AAAI (2005)","key":"5_CR27"},{"unstructured":"Zhou, R., Hansen, E.A.: Beam-stack search: Integrating backtracking with beam search. In: ICAPS, pp. 90\u201398 (2005)","key":"5_CR28"}],"container-title":["Lecture Notes in Computer Science","Model Checking and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74128-2_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:11:44Z","timestamp":1619503904000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74128-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540741275","9783540741282"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74128-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}