{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:47:35Z","timestamp":1760586455902},"publisher-location":"Berlin, Heidelberg","reference-count":115,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642004308"},{"type":"electronic","value":"9783642004315"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-00431-5_5","type":"book-chapter","created":{"date-parts":[[2009,2,24]],"date-time":"2009-02-24T01:14:35Z","timestamp":1235438075000},"page":"65-89","source":"Crossref","is-referenced-by-count":27,"title":["Survey on Directed Model Checking"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Edelkamp","sequence":"first","affiliation":[]},{"given":"Viktor","family":"Schuppan","sequence":"additional","affiliation":[]},{"given":"Dragan","family":"Bo\u0161na\u010dki","sequence":"additional","affiliation":[]},{"given":"Anton","family":"Wijs","sequence":"additional","affiliation":[]},{"given":"Ansgar","family":"Fehnker","sequence":"additional","affiliation":[]},{"given":"Husain","family":"Aljazzar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"5_CR1","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1016\/j.tcs.2005.11.018","volume":"354","author":"Y. Abdedda\u00efm","year":"2006","unstructured":"Abdedda\u00efm, Y., Asarin, E., Maler, O.: Scheduling With Timed Automata. Theoretical Computer Science\u00a0354(2), 272\u2013300 (2006)","journal-title":"Theoretical Computer Science"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-540-68552-4_16","volume-title":"Experimental Algorithms","author":"D. Ajwani","year":"2008","unstructured":"Ajwani, D., Malinger, I., Meyer, U., Toledo, S.: Characterizing the performance of flash memory storage devices and its impact on algorithm design. In: McGeoch, C.C. (ed.) WEA 2008. LNCS, vol.\u00a05038, pp. 208\u2013219. Springer, Heidelberg (2008)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/11603009_15","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"H. Aljazzar","year":"2005","unstructured":"Aljazzar, H., Hermanns, H., Leue, S.: Counterexamples for timed probabilistic reachability. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol.\u00a03829, pp. 177\u2013195. Springer, Heidelberg (2005)"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/11867340_4","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"H. Aljazzar","year":"2006","unstructured":"Aljazzar, H., Leue, S.: Extended directed search for probabilistic timed reachability. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol.\u00a04202, pp. 33\u201351. Springer, Heidelberg (2006)"},{"key":"5_CR5","unstructured":"Aljazzar, H., Leue, S.: Counterexamples for model checking of markov decision processes. Technical Report soft-08-01, Chair for Software Engineering, University of Konstanz, Gemany (December 2007) (submitted for publication)"},{"key":"5_CR6","volume-title":"QEST 2008","author":"H. Aljazzar","year":"2008","unstructured":"Aljazzar, H., Leue, S.: Debugging of dependability models using interactive visualization of counterexamples. In: QEST 2008. IEEE Computer Society Press, Los Alamitos (2008)"},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1023\/A:1008767206905","volume":"18","author":"R. Alur","year":"2001","unstructured":"Alur, R., Brayton, R., Henzinger, T., Qadeer, S., Rajamani, S.: Partial-order reduction in symbolic state-space exploration. Formal Methods in System Design\u00a018, 97\u2013116 (2001)","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"5_CR8","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"},{"issue":"1","key":"5_CR9","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A. Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic\u00a01(1), 162\u2013170 (2000)","journal-title":"ACM Trans. Comput. Logic"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng.\u00a029(7) (2003)","DOI":"10.1109\/TSE.2003.1205180"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Edelkamp, S., \u0160ime\u010dek, P., Sulewski, D.: Can flash memory help in model checking? In: FMICS, pp. 159\u2013174 (2008)","DOI":"10.1007\/978-3-642-03240-0_14"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-78800-3_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Barnat","year":"2008","unstructured":"Barnat, J., Brim, L., \u0160ime\u010dek, P., Weber, M.: Revisiting resistance speeds up I\/O-efficient LTL model checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 48\u201362. Springer, Heidelberg (2008)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/3-540-45319-9_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Behrmann","year":"2001","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.M.T.: Efficient guiding towards cost-optimality in UPPAAL. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 174. Springer, Heidelberg (2001)"},{"issue":"4","key":"5_CR14","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1145\/1059816.1059823","volume":"32","author":"G. Behrmann","year":"2005","unstructured":"Behrmann, G., Larsen, K., Rasmussen, J.: Optimal scheduling using priced timed automata. SIGMETRICS Performance Evaluation Review\u00a032(4), 34\u201340 (2005)","journal-title":"SIGMETRICS Performance Evaluation Review"},{"issue":"1","key":"5_CR15","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1090\/qam\/102435","volume":"16","author":"R. Bellman","year":"1958","unstructured":"Bellman, R.: On a routing problem. Quaterly of Applied Mathematics\u00a016(1), 87\u201390 (1958)","journal-title":"Quaterly of Applied Mathematics"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","volume-title":"Lectures on Concurrency and Petri Nets","author":"J.E. Bengtsson","year":"2004","unstructured":"Bengtsson, J.E., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol.\u00a03098, pp. 87\u2013124. Springer, Heidelberg (2004)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_50","volume-title":"Computer Aided Verification","author":"A. Biere","year":"1997","unstructured":"Biere, A.: \u03bccke \u2014 efficient \u03bc-calculus model checking. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. In: FMICS (2002)","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"5_CR19","unstructured":"Bisiani, R.: Beam search. In: Shapiro [99], pp. 1467\u20131568"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/3-540-48683-6_21","volume-title":"Computer Aided Verification","author":"R. Bloem","year":"1999","unstructured":"Bloem, R., Ravi, K., Somenzi, F.: Efficient decision procedures for model checking of linear time logic properties. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 222\u2013235. Springer, Heidelberg (1999)"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Bloem, R., Ravi, K., Somenzi, F.: Symbolic guided search for CTL model checking. In: DAC, pp. 29\u201334 (2000)","DOI":"10.1145\/337292.337306"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-27813-9_29","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2004","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 372\u2013386. Springer, Heidelberg (2004)"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Bo\u0161na\u010dki, D., Leue, S., Lluch-Lafuente, A.: Partial-order reduction for general state exploring algorithms. In: SPIN (2006)","DOI":"10.1007\/11691617_16"},{"key":"5_CR24","first-page":"208","volume-title":"RTSS","author":"M. Bozga","year":"2004","unstructured":"Bozga, M., Kerbaa, A., Maler, O.: Scheduling Acyclic Branching Programs on Parallel Machines. In: RTSS, pp. 208\u2013215. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_5","volume-title":"SPIN Model Checking and Software Verification","author":"E. Brinksma","year":"2000","unstructured":"Brinksma, E., Mader, A.: Verification and Optimization of a PLC Control Schedule. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885. Springer, Heidelberg (2000)"},{"issue":"5","key":"5_CR26","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. Clarke","year":"1994","unstructured":"Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. ACM Trans. Program. Lang. Syst.\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR27","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"5_CR28","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M., 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":"5_CR29","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"5_CR30","unstructured":"Dechter, R., Pearl, J.: The optimality of A* revisited. In: AAAI (1983)"},{"key":"5_CR31","doi-asserted-by":"publisher","first-page":"1275","DOI":"10.1057\/palgrave.jors.2601389","volume":"53","author":"F. Della Croce","year":"2002","unstructured":"Della Croce, F., T\u2019kindt, V.: A recovering beam search algorithm for the one-machine dynamic total completion time scheduling problem. J. of the Operational Research Society\u00a053, 1275\u20131280 (2002)","journal-title":"J. of the Operational Research Society"},{"issue":"11","key":"5_CR32","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1145\/363269.363610","volume":"12","author":"R. Dial","year":"1969","unstructured":"Dial, R.: Shortest-path forest with topological ordering. Communications of the ACM\u00a012(11), 632\u2013633 (1969)","journal-title":"Communications of the ACM"},{"key":"5_CR33","unstructured":"Dierks, H.: Time, abstraction and heuristics \u2013 automatic verification and planning of timed systems using abstraction and heuristics. Habilitation thesis (July 2005)"},{"key":"5_CR34","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/BF01386390","volume":"1","author":"E. Dijkstra","year":"1959","unstructured":"Dijkstra, E.: A note on two problems in connection with graphs. Numerische Mathematik\u00a01, 269\u2013271 (1959)","journal-title":"Numerische Mathematik"},{"issue":"1","key":"5_CR35","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/0004-3702(94)90040-X","volume":"65","author":"J. Dillenburg","year":"1994","unstructured":"Dillenburg, J., Nelson, P.: Perimeter search. Artificial Intelligence\u00a065(1), 165\u2013178 (1994)","journal-title":"Artificial Intelligence"},{"key":"5_CR36","unstructured":"Edelkamp, S.: Symbolic pattern databases in heuristic search planning. In: AIPS (2002)"},{"key":"5_CR37","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":"5_CR38","unstructured":"Edelkamp, S., Jabbar, S., Lluch-Lafuente, A.: Cost-algebraic heuristic search. In: AAAI (2005)"},{"key":"5_CR39","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. STTT\u00a05, 247\u2013267 (2004)","journal-title":"STTT"},{"key":"5_CR40","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. STTT\u00a06, 277\u2013301 (2004)","journal-title":"STTT"},{"key":"5_CR41","unstructured":"Edelkamp, S., Lluch-Lafuente, A.: Abstraction in directed model checking. In: ICAPS-Workshop on Connecting Planning Theory with Practice (2004)"},{"key":"5_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-540-70545-1_50","volume-title":"Computer Aided Verification","author":"S. Edelkamp","year":"2008","unstructured":"Edelkamp, S., Sanders, P., \u0160ime\u010dek, P.: Semi-external LTL model checking. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 530\u2013542. Springer, Heidelberg (2008)"},{"key":"5_CR43","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Sulewski, D.: Flash-efficient LTL model checking with minimal counterexamples. In: SEFM (2008)","DOI":"10.1109\/SEFM.2008.34"},{"key":"5_CR44","unstructured":"Edelkamp, S., Sulewski, D.: Model checking via delayed duplicate detection on the GPU. Technical Report 821, Dortmund University of Technology (2008)"},{"key":"5_CR45","doi-asserted-by":"crossref","unstructured":"Emerson, A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, pp. 995\u20131072. Elsevier and MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"5_CR46","unstructured":"Emerson, E., Lei, C.: Efficient model checking in fragments of the propositional mu-calculus (extended abstract). In: LICS, pp. 267\u2013278 (1986)"},{"key":"5_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-85114-1_8","volume-title":"Model Checking Software","author":"S. Evangelista","year":"2008","unstructured":"Evangelista, S.: Dynamic delayed duplicate detection for external memory model checking. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 77\u201394. Springer, Heidelberg (2008)"},{"key":"5_CR48","volume-title":"Proc. RTCSA 1999","author":"A. Fehnker","year":"1999","unstructured":"Fehnker, A.: Scheduling a Steel Plant with Timed Automata. In: Proc. RTCSA 1999, IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"5_CR49","unstructured":"Felner, A.: Improving Search Techniques and using them in Different Environments. PhD thesis, Bar-Ilan University (2001)"},{"key":"5_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_30","volume-title":"Computer Aided Verification","author":"R. Fraer","year":"2000","unstructured":"Fraer, R., Kamhi, G., Ziv, B., Vardi, M., Fix, L.: Prioritized traversal: Efficient reachability analysis for verification and falsification. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"5_CR51","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1016\/0004-3702(92)90059-7","volume":"55","author":"M. Ginsberg","year":"1992","unstructured":"Ginsberg, M., Harvey, W.: Iterative broadening. Artificial Intelligence\u00a055, 367\u2013383 (1992)","journal-title":"Artificial Intelligence"},{"key":"5_CR52","series-title":"Lecture Notes in Computer Science","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems","year":"1996","unstructured":"Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)"},{"key":"5_CR53","series-title":"Lecture Notes in Computer Science","volume-title":"25 Years of Model Checking","year":"2008","unstructured":"Grumberg, O., Veith, H. (eds.): 25 Years of Model Checking. LNCS, vol.\u00a05000. Springer, Heidelberg (2008)"},{"key":"5_CR54","unstructured":"Hajek, J.: Self-synchronization and blocking in data transfer protocols. Technical Report THE-RC29286 (1977)"},{"key":"5_CR55","unstructured":"Hajek, J.: Automatically verified data transfer protocols. In: Proceedings 4th International Computer Communications Conference (1978)"},{"key":"5_CR56","unstructured":"Hajek, J. (2002), http:\/\/www.humintel.com\/hajek\/"},{"key":"5_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-540-71209-1_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Han","year":"2007","unstructured":"Han, T., Katoen, J.-P.: Counterexamples in probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 72\u201386. Springer, Heidelberg (2007)"},{"key":"5_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-540-75596-8_24","volume-title":"Automated Technology for Verification and Analysis","author":"T. Han","year":"2007","unstructured":"Han, T., Katoen, J.-P.: Providing evidence of likely being on time: Counterexample generation for CTMC model checking. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 331\u2013346. Springer, Heidelberg (2007)"},{"key":"5_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/3-540-45622-8_7","volume-title":"Abstraction, Reformulation, and Approximation","author":"E. Hansen","year":"2002","unstructured":"Hansen, E., Zhou, R., Feng, Z.: Symbolic heuristic search using decision diagrams. In: Koenig, S., Holte, R.C. (eds.) SARA 2002. LNCS, vol.\u00a02371, p. 83. Springer, Heidelberg (2002)"},{"issue":"5","key":"5_CR60","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput.\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Asp. Comput."},{"key":"5_CR61","unstructured":"Helmert, M., Geffner, H.: Unifying the causal graph and additive heuristic. In: ICAPS, pp. 140\u2013147 (2008)"},{"key":"5_CR62","unstructured":"Helmert, M., Haslum, P., Hoffmann, J.: Flexible abstraction heuristics in optimal sequential planning. In: ICAPS, pp. 176\u2013183 (2007)"},{"key":"5_CR63","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G. Holzmann","year":"2004","unstructured":"Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"issue":"10","key":"5_CR64","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/TSE.2007.70724","volume":"33","author":"G. Holzmann","year":"2007","unstructured":"Holzmann, G., Bosnacki, D.: The design of a multicore extension of the SPIN model checker. IEEE Trans. Software Eng.\u00a033(10), 659\u2013674 (2007)","journal-title":"IEEE Trans. Software Eng."},{"key":"5_CR65","doi-asserted-by":"crossref","unstructured":"Holzmann, G., Peled, D., Yannakakis, M.: On nested depth first search. In: SPIN (1996)","DOI":"10.1090\/dimacs\/032\/03"},{"key":"5_CR66","unstructured":"Jensen, R., Bryant, R., Veloso, M.: SetA*: An efficient BDD-based heuristic search algorithm. In: AAAI (2002)"},{"issue":"1","key":"5_CR67","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"R. Korf","year":"1985","unstructured":"Korf, R.: Depth-first iterative-deepening: An optimal admissible tree search. Artificial Intelligence\u00a027(1), 97\u2013109 (1985)","journal-title":"Artificial Intelligence"},{"issue":"5","key":"5_CR68","doi-asserted-by":"publisher","first-page":"715","DOI":"10.1145\/1089023.1089024","volume":"52","author":"R. Korf","year":"2005","unstructured":"Korf, R., Zhang, W., Thayer, I., Hohwald, H.: Frontier search. Journal of the ACM\u00a052(5), 715\u2013748 (2005)","journal-title":"Journal of the ACM"},{"key":"5_CR69","unstructured":"Kumar, V.: Branch-and-bound search. In: Shapiro [99], pp. 1468\u20131472"},{"key":"5_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/11817949_33","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O., Sheinvald-Faragy, S.: Finding shortest witnesses to the nonemptiness of automata on infinite words. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol.\u00a04137, pp. 492\u2013508. Springer, Heidelberg (2006)"},{"key":"5_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"679","DOI":"10.1007\/978-3-540-71209-1_52","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Kupferschmid","year":"2007","unstructured":"Kupferschmid, S., Dr\u00e4ger, K., Hoffmann, J., Finkbeiner, B., Dierks, H., Podelski, A., Behrmann, G.: uppaal\/DMC \u2013 abstraction-based heuristics for directed model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 679\u2013682. Springer, Heidelberg (2007)"},{"key":"5_CR72","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.) SPIN 2006. LNCS, vol.\u00a03925, pp. 35\u201352. Springer, Heidelberg (2006)"},{"key":"5_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1007\/978-3-540-70545-1_53","volume-title":"Computer Aided Verification","author":"S. Kupferschmid","year":"2008","unstructured":"Kupferschmid, S., Wehrle, M., Nebel, B., Podelski, A.: Faster than uppaal? In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 552\u2013555. Springer, Heidelberg (2008)"},{"key":"5_CR74","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R. Kurshan","year":"1994","unstructured":"Kurshan, R.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)"},{"key":"5_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-85114-1_13","volume-title":"Model Checking Software","author":"P. Lamborn","year":"2008","unstructured":"Lamborn, P., Hansen, E.A.: Layered duplicate detection in external-memory model checking. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 160\u2013175. Springer, Heidelberg (2008)"},{"key":"5_CR76","unstructured":"Lluch-Lafuente, A.: Directed Search for the Verification of Communication Protocols. PhD thesis, Albert-Ludwigs-Universit\u00e4t Freiburg im Breisgau (2003)"},{"key":"5_CR77","unstructured":"Lowerre, B.T.: The HARPY speech recognition system. PhD thesis, CMU (1976)"},{"key":"5_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"5_CR79","volume-title":"Heuristics","author":"J. Pearl","year":"1985","unstructured":"Pearl, J.: Heuristics. Addison-Wesley, Reading (1985)"},{"key":"5_CR80","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"D. Peled","year":"1996","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. Formal Methods in System Design\u00a08, 39\u201364 (1996)","journal-title":"Formal Methods in System Design"},{"key":"5_CR81","unstructured":"Qian, K.: Formal Symbolic Verification Using Heuristic Search and Abstraction Techniques. PhD thesis, University of New South Wales (2006)"},{"key":"5_CR82","doi-asserted-by":"crossref","unstructured":"Qian, K., Nymeyer, A.: Heuristic search algorithms based on symbolic data structures. In: ACAI (2003)","DOI":"10.1007\/978-3-540-24581-0_83"},{"key":"5_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-3-540-24730-2_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Qian","year":"2004","unstructured":"Qian, K., Nymeyer, A.: Guided invariant model checking based on abstraction and symbolic pattern databases. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 497\u2013511. Springer, Heidelberg (2004)"},{"key":"5_CR84","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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_CR85","doi-asserted-by":"crossref","unstructured":"Ravi, K., Somenzi, F.: High-density reachability analysis. In: ICCAD (1995)","DOI":"10.1109\/ICCAD.1995.480006"},{"key":"5_CR86","doi-asserted-by":"crossref","unstructured":"Ravi, K., Somenzi, F.: Efficient fixpoint computation for invariant checking. In: ICCD (1999)","DOI":"10.1109\/ICCD.1999.808582"},{"key":"5_CR87","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-48153-2_19","volume-title":"Correct Hardware Design and Verification Methods","author":"K. Ravi","year":"1999","unstructured":"Ravi, K., Somenzi, F.: Hints to accelerate symbolic traversal. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 250\u2013266. Springer, Heidelberg (1999)"},{"key":"5_CR88","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/3-540-48119-2_13","volume-title":"FM\u201999 - Formal Methods","author":"F. Reffel","year":"1999","unstructured":"Reffel, F., Edelkamp, S.: Error detection with directed symbolic model checking. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, p. 195. Springer, Heidelberg (1999)"},{"key":"5_CR89","doi-asserted-by":"crossref","unstructured":"Rubin, S.: The ARGOS Image Understanding System. PhD thesis, CMU (1978)","DOI":"10.21236\/ADA066736"},{"key":"5_CR90","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-540-73370-6_5","volume-title":"Model Checking Software","author":"N. Rungta","year":"2007","unstructured":"Rungta, N., Mercer, E.G.: Generating counter-examples through randomized guided search. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 39\u201357. Springer, Heidelberg (2007)"},{"key":"5_CR91","volume-title":"European Conference on Artificial Intelligence (ECAI)","author":"S. Russell","year":"1992","unstructured":"Russell, S.: Efficient memory-bounded search methods. In: European Conference on Artificial Intelligence (ECAI). Wiley, Chichester (1992)"},{"key":"5_CR92","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44829-2_1","volume-title":"Model Checking Software","author":"T.C. Ruys","year":"2003","unstructured":"Ruys, T.C.: Optimal scheduling using branch and bound with SPIN 4.0. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 1\u201317. Springer, Heidelberg (2003)"},{"key":"5_CR93","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1016\/S0377-2217(98)00319-1","volume":"118","author":"I. Sabuncuoglu","year":"1999","unstructured":"Sabuncuoglu, I., Bayiz, M.: Job shop scheduling with beam search. European Journal of Operational Research\u00a0118, 390\u2013412 (1999)","journal-title":"European Journal of Operational Research"},{"key":"5_CR94","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_CR95","doi-asserted-by":"crossref","unstructured":"Schuppan, V.: Liveness Checking as Safety Checking to Find Shortest Counterexamples to Linear Time Properties. PhD thesis, ETH Z\u00fcrich (2006)","DOI":"10.1016\/j.entcs.2005.11.018"},{"issue":"2-3","key":"5_CR96","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. STTT\u00a05(2-3), 185\u2013204 (2004)","journal-title":"STTT"},{"key":"5_CR97","doi-asserted-by":"crossref","unstructured":"Schuppan, V., Biere, A.: Liveness checking as safety checking for infinite state spaces. In: INFINITY (2005)","DOI":"10.1016\/j.entcs.2005.11.018"},{"key":"5_CR98","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-540-31980-1_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V. Schuppan","year":"2005","unstructured":"Schuppan, V., Biere, A.: Shortest counterexamples for symbolic model checking of LTL with past. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 493\u2013509. Springer, Heidelberg (2005)"},{"volume-title":"Encyclopedia of Artificial Intelligence","year":"1992","key":"5_CR99","unstructured":"Shapiro, S. (ed.): Encyclopedia of Artificial Intelligence. Wiley Interscience, Hoboken (1992)"},{"issue":"1-4","key":"5_CR100","first-page":"85","volume":"12","author":"P. Si Ow","year":"1988","unstructured":"Si Ow, P., Smith, S.F.: Viewing scheduling as an opportunistic problem-solving process. Annals of Operations Research\u00a012(1-4), 85\u2013108 (1988)","journal-title":"Annals of Operations Research"},{"key":"5_CR101","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/TNET.2002.801397","volume":"10","author":"J.L. Sobrinho","year":"2002","unstructured":"Sobrinho, J.L.: Algebra and algorithms for QoS path computation and hop-by-hop routing in the internet. IEEE\/ACM Transactions on Networking\u00a010, 541\u2013550 (2002)","journal-title":"IEEE\/ACM Transactions on Networking"},{"key":"5_CR102","volume-title":"Introduction to the Numerical Solution of Markov Chains","author":"W. Stewart","year":"1994","unstructured":"Stewart, W.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, New Jersey (1994)"},{"key":"5_CR103","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-540-75596-8_39","volume-title":"Automated Technology for Verification and Analysis","author":"M. Torabi Dashti","year":"2007","unstructured":"Torabi Dashti, M., Wijs, A.J.: Pruning State Spaces with Extended Beam Search. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 543\u2013552. Springer, Heidelberg (2007)"},{"key":"5_CR104","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-51285-3_35","volume-title":"PARLE \u201989 - Parallel Architectures and Languages Europe","author":"A. Valmari","year":"1989","unstructured":"Valmari, A.: Eliminating redundant interleavings during concurrent program verification. In: Odijk, E., Rem, M., Syre, J.-C. (eds.) PARLE 1989. LNCS, vol.\u00a0366, pp. 89\u2013103. Springer, Heidelberg (1989)"},{"key":"5_CR105","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1016\/0020-0255(84)90009-4","volume":"34","author":"M. Valtorta","year":"1984","unstructured":"Valtorta, M.: A result on the computational complexity of heuristic estimates for the A* algorithm. Information Sciences\u00a034, 48\u201359 (1984)","journal-title":"Information Sciences"},{"key":"5_CR106","unstructured":"Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS (1986)"},{"issue":"4","key":"5_CR107","first-page":"493","volume":"3","author":"B. Wah","year":"1995","unstructured":"Wah, B., Shang, Y.: Study of IDA*-style searches. Artificial Intelligence\u00a03(4), 493\u2013523 (1995)","journal-title":"Artificial Intelligence"},{"issue":"1","key":"5_CR108","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10703-006-4617-3","volume":"28","author":"C. Wang","year":"2006","unstructured":"Wang, C., Bloem, R., Hachtel, G., Ravi, K., Somenzi, F.: Compositional SCC analysis for language emptiness. Formal Methods in System Design\u00a028(1), 5\u201336 (2006)","journal-title":"Formal Methods in System Design"},{"key":"5_CR109","unstructured":"Wehrle, M., Kupferschmidt, S., Podelski, A.: Useful actions are useful. In: ICAPS, pp. 388\u2013395 (2008)"},{"key":"5_CR110","unstructured":"Wijs, A.J.: What to Do Next: Analysing and Optimising System Behaviour in Time. PhD thesis, Vrije Universiteit Amsterdam (2007)"},{"key":"5_CR111","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-540-74128-2_11","volume-title":"Model Checking and Artificial Intelligence","author":"A.J. Wijs","year":"2007","unstructured":"Wijs, A.J., Lisser, B.: Distributed Extended Beam Search for Quantitative Model Checking. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS (LNAI), vol.\u00a04428, pp. 165\u2013182. Springer, Heidelberg (2007)"},{"key":"5_CR112","unstructured":"Wijs, A.J., van de Pol, J.C., Bortnik, E.: Solving Scheduling Problems by Untimed Model Checking. In: STTT (to appear, 2008)"},{"key":"5_CR113","doi-asserted-by":"crossref","unstructured":"Yang, C., Dill, D.: Validation with guided search of the state space. In: DAC (1998)","DOI":"10.1145\/277044.277201"},{"key":"5_CR114","unstructured":"Zhou, R., Hansen, E.: Breadth-first heuristic search. In: ICAPS (2004)"},{"key":"5_CR115","unstructured":"Zhou, R., Hansen, E.: Beam-stack search: Integrating backtracking with beam search. In: ICAPS (2005)"}],"container-title":["Lecture Notes in Computer Science","Model Checking and Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00431-5_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,18]],"date-time":"2019-05-18T02:33:48Z","timestamp":1558146828000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00431-5_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642004308","9783642004315"],"references-count":115,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00431-5_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}