{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:44:54Z","timestamp":1725561894744},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540212997"},{"type":"electronic","value":"9783540247302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24730-2_18","type":"book-chapter","created":{"date-parts":[[2010,8,2]],"date-time":"2010-08-02T11:00:15Z","timestamp":1280746815000},"page":"205-219","source":"Crossref","is-referenced-by-count":28,"title":["Tarjan\u2019s Algorithm Makes On-the-Fly LTL Verification More Efficient"],"prefix":"10.1007","author":[{"given":"Jaco","family":"Geldenhuys","sequence":"first","affiliation":[]},{"given":"Antti","family":"Valmari","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","volume-title":"The Design and Analysis of Computer Algorithms","author":"A.V. Aho","year":"1974","unstructured":"Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading (1974)"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BFb0023737","volume-title":"Computer-Aided Verification","author":"C. Courcoubetis","year":"1991","unstructured":"Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531, pp. 233\u2013242. Springer, Heidelberg (1991)"},{"issue":"2\/3","key":"18_CR3","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":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Computer Aided Verification","author":"M. Daniele","year":"1999","unstructured":"Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear time temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 249\u2013260. Springer, Heidelberg (1999)"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proc. 2nd ACM Workshop Formal Methods in Software Practice, March 1998, pp. 7\u201315 (1998), Related site: http:\/\/www.cis.ksu.edu\/santos\/spec-patterns (Last updated September 1998)","DOI":"10.1145\/298595.298598"},{"key":"18_CR6","unstructured":"Edelkamp, S., Leue, S., Lluch Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. Tech. Rep. 161, Institut f\u00fcr Informatik, Albert-Ludwigs-Universit\u00e4t Freiburg (October 2001)"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/3-540-44618-4_13","volume-title":"CONCUR 2000 - Concurrency Theory","author":"K. Etessami","year":"2000","unstructured":"Etessami, K., Holzmann, G.J.: Optimizing B\u00fcchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 154\u2013167. Springer, Heidelberg (2000)"},{"key":"18_CR8","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/BF00271339","volume":"8","author":"J. Eve","year":"1977","unstructured":"Eve, J., Kurki-Suonio, R.: On computing the transitive closure of a relation. Acta Informatica\u00a08, 303\u2013314 (1977)","journal-title":"Acta Informatica"},{"key":"18_CR9","unstructured":"Gabow, H.N.: Path-based depth-first search for strong and biconnected components. Tech. Rep. CU\u2013CS\u2013890\u201399, Dept. Computer Science, Univ. of Colorado at Boulder (February 2000)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proc. 15th IFIP Symp. Protocol Specification, Testing, and Verification, June 1995, pp. 3\u201318 (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"#cr-split#-18_CR12.1","unstructured":"Godefroid, P.: Partial-order Methods for the Verification of Concurrent Systems, An Approach to the State-explosion Problem. PhD thesis, University of Li\u00e8ge (December 1994);"},{"key":"#cr-split#-18_CR12.2","doi-asserted-by":"crossref","unstructured":"Also published as Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)","DOI":"10.1007\/3-540-60761-7"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","first-page":"175","volume-title":"Computer Aided Verification","author":"P. Godefroid","year":"1993","unstructured":"Godefroid, P., Holzmann, G.J., Pirottin, D.: State space caching revisited. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 175\u2013186. Springer, Heidelberg (1993)"},{"key":"18_CR14","unstructured":"Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall Software Series (1991)"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: Proc. 2nd Spin Workshop, August 1996, pp. 23\u201332 (1996)","DOI":"10.1090\/dimacs\/032\/03"},{"issue":"5","key":"18_CR16","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1145\/55483.55496","volume":"17","author":"F.J. Lin","year":"1987","unstructured":"Lin, F.J., Chu, P.M., Liu, M.T.: Protocol verification using reachability analysis: the state space explosion problem and relief strategies. Computer Communication Review\u00a017(5), 126\u2013135 (1987)","journal-title":"Computer Communication Review"},{"issue":"1","key":"18_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(1), 9\u201314 (1994)","journal-title":"Information Processing Letters"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification","author":"D. Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all: On model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 409\u2013423. Springer, Heidelberg (1993)"},{"key":"18_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-45653-8_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K. Schneider","year":"2001","unstructured":"Schneider, K.: Improving automata generation for linear temporal logic by considering the automaton hierarchy. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 39\u201354. Springer, Heidelberg (2001)"},{"issue":"1","key":"18_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 application in data flow analysis. Computer and Mathematics with Applications\u00a07(1), 67\u201372 (1981)","journal-title":"Computer and Mathematics with Applications"},{"key":"18_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\u2013267. Springer, Heidelberg (2000)"},{"issue":"2","key":"18_CR22","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R.E. Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM Journal of Computing\u00a01(2), 146\u2013160 (1972)","journal-title":"SIAM Journal of Computing"},{"key":"18_CR23","unstructured":"Tauriainen, H.: A randomized testbench for algorithms translating linear temporal logic formulae into B\u00fcchi automata. In: Proc. Workshop Concurrency, Specifications, and Programming, September 1999, pp. 251\u2013262 (1999)"},{"key":"18_CR24","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168724","volume-title":"Introduction to Distributed Algorithms","author":"G. Tel","year":"2000","unstructured":"Tel, G.: Introduction to Distributed Algorithms, 2nd edn. Cambridge University Press, Cambridge (2000)","edition":"2"},{"issue":"1","key":"18_CR25","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A. Valmari","year":"1992","unstructured":"Valmari, A.: A stubborn attack on state explosion. Formal Methods in System Design\u00a01(1), 297\u2013322 (1992)","journal-title":"Formal Methods in System Design"},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proc. Symp. Foundations of Computer Science, November 1983, pp. 185\u2013194 (1983)","DOI":"10.1109\/SFCS.1983.51"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Proc. 35th ACM\/IEEE Conf. Design Automation, June 1998, pp. 599\u2013604 (1998)","DOI":"10.1145\/277044.277201"}],"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-24730-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T23:18:19Z","timestamp":1559344699000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24730-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540212997","9783540247302"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24730-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}