{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:30:44Z","timestamp":1759638644898},"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_4","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T14:14:13Z","timestamp":1143555253000},"page":"53-70","source":"Crossref","is-referenced-by-count":22,"title":["Larger Automata and Less Work for LTL Model Checking"],"prefix":"10.1007","author":[{"given":"Jaco","family":"Geldenhuys","sequence":"first","affiliation":[]},{"given":"Henri","family":"Hansen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_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":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/3-540-44804-7_7","volume-title":"Process Algebra and Probabilistic Methods. Performance Modelling and Verification","author":"L. Brim","year":"2001","unstructured":"Brim, L., \u010cern\u00e1, I., Ne\u010desal, M.: Randomization helps in LTL model checking. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol.\u00a02165, pp. 105\u2013119. Springer, Heidelberg (2001)"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"J.R. B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.R.: Weak second-order arithmetic and finite automata. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Math.\u00a06, 66\u201392 (1960)","journal-title":"Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Math."},{"key":"4_CR4","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second-order arithmetic. In: Proc. 1960 Intl. Congr. Logic, Method and Philosophy of Science, pp. 1\u201311. Stanford Univ. Press (June 1962)"},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","volume":"8","author":"Y. Choueka","year":"1974","unstructured":"Choueka, Y.: Theories of automata on \u03c9-tapes: a simplified approach. Journal Computer and System Sciences\u00a08, 117\u2013141 (1974)","journal-title":"Journal Computer and System Sciences"},{"key":"4_CR6","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); Journal version: Formal Methods in System Design 1(2\/3), 275\u2013288 (1992)"},{"key":"4_CR7","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":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/11537328_15","volume-title":"Model Checking Software","author":"J.-M. Couvreur","year":"2005","unstructured":"Couvreur, J.-M.: On-the-fly emptiness checks for generalized B\u00fcchi automata. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol.\u00a03639, pp. 169\u2013184. Springer, Heidelberg (2005)"},{"key":"4_CR9","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 temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 249\u2013260. Springer, Heidelberg (1999)"},{"key":"4_CR10","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 Worksh. Formal Methods in Software Practice, pp. 7\u201315 (March 1998)","DOI":"10.1145\/298595.298598"},{"key":"4_CR11","unstructured":"Edelkamp, S., Leue, S., Lluch Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. Technical Report 161, Institut f\u00fcr Informatik, Albert-Ludwigs-Universit\u00e4t Freiburg (October 2001)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/3-540-45694-5_10","volume-title":"CONCUR 2002 - Concurrency Theory","author":"K. Etessami","year":"2002","unstructured":"Etessami, K.: A hierarchy of polynomial-time computable simulations for automata. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 131\u2013144. Springer, Heidelberg (2002)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","first-page":"154","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":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/3-540-45089-0_5","volume-title":"Implementation and Application of Automata","author":"C. Fritz","year":"2003","unstructured":"Fritz, C.: Constructing B\u00fcchi automata from linear temporal logic using simulation relations for alternating B\u00fcchi automata. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol.\u00a02759, pp. 35\u201348. Springer, Heidelberg (2003)"},{"key":"4_CR15","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":"4_CR16","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":"4_CR17","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); Journal version: Theor. Computer Science 345(1), 60-82 (2005)"},{"key":"4_CR18","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 Spec., Testing, and Verif., June 1995, pp. 3\u201318 (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"4_CR19","unstructured":"Godefroid, P., Holzmann, G.J.: On the verification of temporal properties. In: Proc. 13th IFIP Symp. Protocol Spec., Testing, and Verif., May 1993, pp. 109\u2013124 (1993)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"610","DOI":"10.1007\/3-540-45657-0_51","volume-title":"Computer Aided Verification","author":"S. Gurumurthy","year":"2002","unstructured":"Gurumurthy, S., Bloem, R., Somenzi, F.: Fair simulation minimization. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 610\u2013624. Springer, Heidelberg (2002)"},{"key":"#cr-split#-4_CR21.1","doi-asserted-by":"crossref","unstructured":"Hansen, H., Penczek, W., Valmari, A.: Stuttering-insensitive automata for on-the-fly detection of livelock properties. In: Proc. 7th Intl. ERCIM Worksh. Formal Methods for Industrial Critical Systems, July 2002, pp. 185???200 (2002);","DOI":"10.1016\/S1571-0661(04)80411-0"},{"key":"#cr-split#-4_CR21.2","doi-asserted-by":"crossref","unstructured":"Hansen, H., Penczek, W., Valmari, A.: Stuttering-insensitive automata for on-the-fly detection of livelock properties. In: Proc. 7th Intl. ERCIM Worksh. Formal Methods for Industrial Critical Systems, July 2002, pp. 185\u2013200 (2002); Also published in Elec. Notes in Theor. Computer Science 66(2) (December 2002)","DOI":"10.1016\/S1571-0661(04)80411-0"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: Proc. 2nd spin Worksh., August 1996. DIMACS Series, vol.\u00a032, pp. 23\u201332 (1997)","DOI":"10.1090\/dimacs\/032\/03"},{"key":"4_CR23","unstructured":"Kamp, J.A.W.: Tense Logic and the Theory of Linear Order. PhD thesis, Univ. of California (1968)"},{"key":"4_CR24","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"S.A. Kripke","year":"1963","unstructured":"Kripke, S.A.: Semantical analysis of modal logic I, normal propositional calculi. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Math\u00a09, 67\u201396 (1963)","journal-title":"Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Math"},{"key":"4_CR25","volume-title":"Computer-aided Verification of Coordinating Processes: The Automata-theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-aided Verification of Coordinating Processes: The Automata-theoretic Approach. Princeton University Press, Princeton (1994)"},{"key":"4_CR26","first-page":"1","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. of the American Mathemathical Society\u00a0141, 1\u201335 (1969)","journal-title":"Trans. of the American Mathemathical Society"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-31980-1_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Schwoon","year":"2005","unstructured":"Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 174\u2013190. Springer, Heidelberg (2005)"},{"key":"4_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-39724-3_12","volume-title":"Correct Hardware Design and Verification Methods","author":"R. Sebastiani","year":"2003","unstructured":"Sebastiani, R., Tonetta, S.: More deterministic vs. Smaller b\u00fcchi automata for efficient LTL model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 126\u2013140. Springer, Heidelberg (2003)"},{"key":"4_CR29","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":"4_CR30","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":"4_CR31","unstructured":"Tauriainen, H.: A randomized testbench for algorithms translating linear temporal logic formulae. In: Proc. Worksh. Concurrency, Specifications, and Programming, September 1999, pp. 251\u2013262 (1999)"},{"key":"4_CR32","unstructured":"Tauriainen, H.: Nested emptiness search for generalized B\u00fcchi automata. Technical Report HUT\u2013TCS\u2013A79, Laboratory for Theoretical Computer Science, Helsinki Univ. of Technology (July 2003)"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/3-540-56922-7_33","volume-title":"Computer Aided Verification","author":"A. Valmari","year":"1993","unstructured":"Valmari, A.: On-the-fly verification with stubborn sets. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 397\u2013408. Springer, Heidelberg (1993)"},{"key":"4_CR34","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st IEEE Symp. on Logic in Computer Science, June 1986, pp. 332\u2013344 (1986)"},{"key":"4_CR35","first-page":"72","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Information and Computation\u00a056, 72\u201399 (1983)","journal-title":"Information and Computation"},{"key":"4_CR36","first-page":"185","volume-title":"Proc. 24th IEEE Symp. on the Foundations of Computer Science","author":"P. Wolper","year":"1983","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proc. 24th IEEE Symp. on the Foundations of Computer Science, November 1983, pp. 185\u2013194. IEEE Computer Society Press, Los Alamitos (1983)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11691617_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,13]],"date-time":"2020-04-13T11:43:10Z","timestamp":1586778190000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11691617_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540331025","9783540331032"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/11691617_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}