{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T09:10:43Z","timestamp":1774775443128,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540733690","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73370-6_11","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T00:03:26Z","timestamp":1188432206000},"page":"149-167","source":"Crossref","is-referenced-by-count":68,"title":["LTL Satisfiability Checking"],"prefix":"10.1007","author":[{"given":"Kristin Y.","family":"Rozier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Ammons, G., Mandelin, D., Bodik, R., Larus, J.R.: Debugging temporal specifications with concept analysis. In: PLDI. Proc. ACM Conf., pp. 182\u2013195 (2003)","DOI":"10.1145\/781131.781152"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"R. Armoni","year":"2003","unstructured":"Armoni, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A., Vardi, M.Y.: Enhanced vacuity detection for linear temporal logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, Springer, Heidelberg (2003)"},{"issue":"2","key":"11_CR3","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. Formal Methods in System Design\u00a018(2), 141\u2013162 (2001)","journal-title":"Formal Methods in System Design"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Computer Aided Verification","author":"R.K. Brayton","year":"1996","unstructured":"Brayton, R.K., Hachtel, G.D., Sangiovanni-Vincentelli, A., Somenzi, F., Aziz, A., Cheng, S.-T., Edwards, S., Khatri, S., Kukimoto, T., Pardo, A., Qadeer, S., Ranjan, R.K., Sarwary, S., Shiple, T.R., Swamy, G., Villa, T.: VIS: a system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 428\u2013432. Springer, Heidelberg (1996)"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean-function manipulation. IEEE Trans. on Computers, vol. C-35(8) (1986)","DOI":"10.1109\/TC.1986.1676819"},{"issue":"2","key":"11_CR7","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/11560548_16","volume-title":"Correct Hardware Design and Verification Methods","author":"D. Bustan","year":"2005","unstructured":"Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 191\u2013206. Springer, Heidelberg (2005)"},{"issue":"4","key":"11_CR9","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. It\u2019l J. on Software Tools for Tech. Transfer\u00a02(4), 410\u2013425 (2000)","journal-title":"It\u2019l J. on Software Tools for Tech. Transfer"},{"issue":"1","key":"11_CR10","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1008615614281","volume":"10","author":"E.M. Clarke","year":"1997","unstructured":"Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Formal Methods in System Design\u00a010(1), 47\u201371 (1997)","journal-title":"Formal Methods in System Design"},{"key":"11_CR11","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"11_CR12","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, 275\u2013288 (1992)","journal-title":"Formal Methods in System Design"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/3-540-48119-2_16","volume-title":"FM 1999 - 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":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Computer Aided Verification","author":"N. Daniele","year":"1999","unstructured":"Daniele, N., Guinchiglia, 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":"11_CR15","first-page":"76","volume-title":"MASCOTS, Proc. 12th Int\u2019l Workshop","author":"A. Duret-Lutz","year":"2004","unstructured":"Duret-Lutz, A., Poitrenaud, D.: SPOT: An extensible model checking library using transition-based generalized b\u00fcchi automata. In: MASCOTS, Proc. 12th Int\u2019l Workshop, pp. 76\u201383. IEEE Computer Society, Los Alamitos (2004)"},{"key":"11_CR16","first-page":"997","volume-title":"Handbook of Theoretical Computer Science","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: Van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, ch. 16, pp. 997\u20131072. Elsevier, MIT Press, Cambridge (1990)"},{"key":"11_CR17","unstructured":"Emerson, E.A., Lei, C.L.: Efficient model checking in fragments of the propositional \u03bc-calculus. In: LICS, 1st Symp., Cambridge, pp. 267\u2013278 (1986)"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"153","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. 153\u2013167. Springer, Heidelberg (2000)"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"11_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"728","DOI":"10.1007\/11591191_50","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Fritz","year":"2005","unstructured":"Fritz, C.: Concepts of automata construction from LTL. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 728\u2013742. Springer, Heidelberg (2005)"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/11691617_4","volume-title":"Model Checking Software","author":"J. Geldenhuys","year":"2006","unstructured":"Geldenhuys, J., Hansen, H.: Larger automata and less work for LTL model checking. In: Valmari, A. (ed.) Model Checking Software. LNCS, vol.\u00a03925, pp. 53\u201370. Springer, Heidelberg (2006)"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"11_CR24","first-page":"3","volume-title":"Protocol Specification, Testing, and Verification","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembiski, P., Sredniawa, M. (eds.) Protocol Specification, Testing, and Verification, August 1995, pp. 3\u201318. Chapman & Hall, Sydney, Australia (1995)"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36135-9_20","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"D. Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulae to B\u00fcchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, Springer, Heidelberg (2002)"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/978-3-540-30494-4_22","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Gurfinkel","year":"2004","unstructured":"Gurfinkel, A., Chechik, M.: Extending extended vacuity. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 306\u2013321. Springer, Heidelberg (2004)"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/978-3-540-24730-2_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Gurfinkel","year":"2004","unstructured":"Gurfinkel, A., Chechik, M.: How vacuous is vacuous. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 451\u2013466. Springer, Heidelberg (2004)"},{"issue":"5","key":"11_CR28","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN (Special issue on Formal Methods in Software Practice). IEEE Trans. on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/11817949_3","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O.: Sanity checks in formal verification. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol.\u00a04137, pp. 37\u201351. Springer, Heidelberg (2006)"},{"issue":"2","key":"11_CR30","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O. Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. J. on Software Tools For Technology Transfer\u00a04(2), 224\u2013233 (2003)","journal-title":"J. on Software Tools For Technology Transfer"},{"key":"11_CR31","unstructured":"Kurshan, R.P.: FormalCheck User\u2019s Manual. Cadence Design, Inc. (1998)"},{"key":"11_CR32","unstructured":"McMillan, K.: The SMV language. Technical report, Cadence Berkeley Lab (1999)"},{"key":"11_CR33","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Boston (1993)"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/978-3-540-27813-9_5","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2004","unstructured":"Namjoshi, K.S.: An efficiently checkable, proof-based formulation of vacuity in model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 57\u201369. Springer, Heidelberg (2004)"},{"key":"11_CR35","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/3-540-45620-1_2","volume-title":"Automated Deduction - CADE-18","author":"G. Pan","year":"2002","unstructured":"Pan, G., Sattler, U., Vardi, M.Y.: BDD-based decision procedures for K. In: Voronkov, A. (ed.) Automated Deduction - CADE-18. LNCS (LNAI), vol.\u00a02392, pp. 16\u201330. Springer, Heidelberg (2002)"},{"issue":"1\u20133","key":"11_CR36","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1016\/S0304-3975(02)00410-3","volume":"295","author":"N. Piterman","year":"2003","unstructured":"Piterman, N., Vardi, M.Y.: From bidirectionality to alternation. Theoretical Computer Science\u00a0295(1\u20133), 295\u2013321 (2003)","journal-title":"Theoretical Computer Science"},{"key":"11_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/3-540-45657-0_39","volume-title":"Computer Aided Verification","author":"M. Purandare","year":"2002","unstructured":"Purandare, M., Somenzi, F.: Vacuum cleaning CTL formulae. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 485\u2013499. Springer, Heidelberg (2002)"},{"key":"11_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 126\u2013140. Springer, Heidelberg (2003)"},{"key":"11_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1007\/11513988_35","volume-title":"Computer Aided Verification","author":"R. Sebastiani","year":"2005","unstructured":"Sebastiani, R., Tonetta, S., Vardi, M.Y.: Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 350\u2013373. Springer, Heidelberg (2005)"},{"key":"11_CR40","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":"1","key":"11_CR41","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s100090200070","volume":"4","author":"H. Tauriainen","year":"2002","unstructured":"Tauriainen, H., Heljanko, K.: Testing LTL formula translation into B\u00fcchi automata. STTT - Int\u2019l J. on Software Tools for Tech. Transfer\u00a04(1), 57\u201370 (2002)","journal-title":"STTT - Int\u2019l J. on Software Tools for Tech. Transfer"},{"key":"11_CR42","doi-asserted-by":"crossref","unstructured":"Thirioux, X.: Simple and efficient translation from LTL formulas to B\u00fcchi automata. Electr. Notes Theor. Comput. Sci., vol.\u00a066(2) (2002)","DOI":"10.1016\/S1571-0661(04)80409-2"},{"key":"11_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"575","DOI":"10.1007\/3-540-57887-0_116","volume-title":"Theoretical Aspects of Computer Software","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y.: Nontraditional applications of automata theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol.\u00a0789, pp. 575\u2013597. Springer, Heidelberg (1994)"},{"key":"11_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/978-3-540-69738-1_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M.Y. Vardi","year":"2007","unstructured":"Vardi, M.Y.: Automata-theoretic model checking revisited. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 137\u2013150. Springer, Heidelberg (2007)"},{"key":"11_CR45","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st LICS, pp. 332\u2013344 (1986)"},{"issue":"1","key":"11_CR46","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115(1), 1\u201337 (1994)","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73370-6_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:08:43Z","timestamp":1619518123000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73370-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733690"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73370-6_11","relation":{},"subject":[]}}