{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T06:37:55Z","timestamp":1759991875431},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540253334"},{"type":"electronic","value":"9783540319801"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31980-1_12","type":"book-chapter","created":{"date-parts":[[2010,7,11]],"date-time":"2010-07-11T18:44:59Z","timestamp":1278873899000},"page":"174-190","source":"Crossref","is-referenced-by-count":80,"title":["A Note on On-the-Fly Verification Algorithms"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Schwoon","sequence":"first","affiliation":[]},{"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","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":"12_CR2","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 linear 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":"12_CR3","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"Clarke, E., Emerson, A., Sistla, P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. TOPLAS\u00a08, 244\u2013263 (1986)","journal-title":"TOPLAS"},{"key":"12_CR4","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"2\/3","key":"12_CR5","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(2\/3), 275\u2013288 (1992)","journal-title":"Formal Methods in System Design"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-48119-2_16","volume-title":"FM\u201999 - Formal Methods","author":"J.-M. Couvreur","year":"1999","unstructured":"Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 253\u2013271. Springer, Heidelberg (1999)"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed explicit-state model checking in the validation of communication protocols. In: STTT (2004)","DOI":"10.1007\/s10009-002-0104-3"},{"key":"12_CR8","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.) TACAS 2001. LNCS, vol.\u00a02031, pp. 420\u2013434. Springer, Heidelberg (2001)"},{"issue":"3\u20134","key":"12_CR9","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/S0020-0190(00)00051-X","volume":"74","author":"H.N. Gabow","year":"2000","unstructured":"Gabow, H.N.: Path-based depth-first search for strong and biconnected components. Information Processing Letters\u00a074(3\u20134), 107\u2013114 (2000)","journal-title":"Information Processing Letters"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-540-24732-6_7","volume-title":"Model Checking Software","author":"P. Gastin","year":"2004","unstructured":"Gastin, P., Moro, P., Zeitoun, M.: Minimization of counterexamples in SPIN. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 92\u2013108. Springer, Heidelberg (2004)"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-540-24730-2_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Geldenhuys","year":"2004","unstructured":"Geldenhuys, J., Valmari, A.: Tarjan\u2019s algorithm makes on-the-fly LTL verification more efficient. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 205\u2013219. Springer, Heidelberg (2004)"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D.A., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proc. of PSTV. IFIP, pp. 3\u201318 (1996)","DOI":"10.1007\/978-0-387-34892-6_1"},{"issue":"3","key":"12_CR13","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1023\/A:1008696026254","volume":"13","author":"G.J. Holzmann","year":"1998","unstructured":"Holzmann, G.J.: An analysis of bitstate hashing. Formal Methods in System Design\u00a013(3), 289\u2013307 (1998)","journal-title":"Formal Methods in System Design"},{"key":"12_CR14","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":"12_CR15","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Peled, D.A., Yannakakis, M.: On nested depth first search. In: Proc. 2nd SPIN Workshop, pp. 23\u201332 (1996)","DOI":"10.1090\/dimacs\/032\/03"},{"key":"12_CR16","first-page":"81","volume-title":"Proc. of LICS","author":"O. Kupferman","year":"1998","unstructured":"Kupferman, O., Vardi, M.Y.: Freedom, weakness, and determinism: From linear-time to branching-time. In: Proc. of LICS, pp. 81\u201392. IEEE, Los Alamitos (1998)"},{"key":"12_CR17","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1016\/0020-0190(94)90047-7","volume":"49","author":"E. Nuutila","year":"1994","unstructured":"Nuutila, E., Soisalon-Soininen, E.: On finding the strongly connected components in a directed graph. Information Processing Letters\u00a049, 9\u201314 (1994)","journal-title":"Information Processing Letters"},{"issue":"1","key":"12_CR18","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"D.A. Peled","year":"1996","unstructured":"Peled, D.A.: Combining partial order reductions with on-the-fly model-checking. Formal Methods in System Design\u00a08(1), 39\u201364 (1996)","journal-title":"Formal Methods in System Design"},{"key":"12_CR19","unstructured":"Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. Technical Report 2004\/06, Universit\u00e4t Stuttgart (November 2004)"},{"issue":"1","key":"12_CR20","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0898-1221(81)90008-0","volume":"7","author":"M. Sharir","year":"1981","unstructured":"Sharir, M.: A strong-connectivity algorithm and its applications in data flow analysis. Computers and Mathematics with Applications\u00a07(1), 67\u201372 (1981)","journal-title":"Computers and Mathematics with Applications"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 248\u2013263. Springer, Heidelberg (2000)"},{"issue":"2","key":"12_CR22","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R. Tarjan","year":"1972","unstructured":"Tarjan, R.: Depth-first search and linear graph algorithms. SIAM Journal on Computing\u00a01(2), 146\u2013160 (1972)","journal-title":"SIAM Journal on Computing"},{"key":"12_CR23","unstructured":"Tauriainen, H.: Nested emptiness search for generalized B\u00fcchi automata. Technical Report A79, Helsinki University of Technology (July 2003)"},{"key":"12_CR24","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: Automata theoretic techniques for modal logics of programs. Journal of Computer and System Sciences\u00a032, 183\u2013221 (1986)","journal-title":"Journal of Computer and System Sciences"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31980-1_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:32:41Z","timestamp":1605742361000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31980-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540253334","9783540319801"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31980-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}