{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T02:42:47Z","timestamp":1772505767343,"version":"3.50.1"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,3,11]],"date-time":"2010-03-11T00:00:00Z","timestamp":1268265600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2010,5]]},"DOI":"10.1007\/s10009-010-0140-3","type":"journal-article","created":{"date-parts":[[2010,3,10]],"date-time":"2010-03-10T02:56:47Z","timestamp":1268189807000},"page":"123-137","source":"Crossref","is-referenced-by-count":57,"title":["LTL satisfiability checking"],"prefix":"10.1007","volume":"12","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","published-online":{"date-parts":[[2010,3,11]]},"reference":[{"key":"140_CR1","doi-asserted-by":"crossref","unstructured":"Ammons, G., Mandelin, D., Bodik, R., Larus, J.R.: Debugging temporal specifications with concept analysis. In: Proceedings of the ACM Conference on PLDI, pp. 182\u2013195 (2003)","DOI":"10.1145\/781131.781152"},{"key":"140_CR2","doi-asserted-by":"crossref","unstructured":"Armoni, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A., Vardi, M.Y.: Enhanced vacuity detection for linear temporal logic. In: Proceedings of the 15th International Conference on CAV. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45069-6_35"},{"issue":"2","key":"140_CR3","doi-asserted-by":"crossref","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 Syst. Des. 18(2), 141\u2013162 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"140_CR4","first-page":"187","volume-title":"LFM 2000: Fifth NASA Langley Formal Methods Workshop","author":"S. Bensalem","year":"2000","unstructured":"Bensalem S., Ganesh V., Lakhnech Y., Mu\u00f1oz C., Owre S., Rue\u00df H., Rushby J., Rusu V., Sa\u00efdi H., Shankar N., Singerman E., Tiwari A.: An overview of SAL. In: Michael Holloway, C. (eds) LFM 2000: Fifth NASA Langley Formal Methods Workshop, pp. 187\u2013196. NASA Langley Research Center, Hampton, VA (2000)"},{"key":"140_CR5","doi-asserted-by":"crossref","unstructured":"Bloem, R., Ravi, K., Somenzi, F. (1999) Efficient decision procedures for model checking of linear time logic properties. In: Proceedings of the 11th International Conference on CAV. Lecture Notes in Computer Science, vol. 1633, pp. 222\u2013235. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48683-6_21"},{"key":"140_CR6","doi-asserted-by":"crossref","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: Proceedings of the 8th International Conference on CAV. Lecture Notes in Computer Science, vol. 1102, pp. 428\u2013432. Springer, Berlin (1996)","DOI":"10.1007\/3-540-61474-5_95"},{"issue":"8","key":"140_CR7","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant R.E.: Graph-based algorithms for boolean-function manipulation. IEEE Trans. Comput. C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"140_CR8","doi-asserted-by":"crossref","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. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"140_CR9","doi-asserted-by":"crossref","unstructured":"Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: CHARME. LNCS, vol. 3725, pp. 191\u2013206. Springer, Berlin (2005)","DOI":"10.1007\/11560548_16"},{"issue":"4","key":"140_CR10","doi-asserted-by":"crossref","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. Int. J. Softw. Tools Technol. Transf. 2(4), 410\u2013425 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1","key":"140_CR11","doi-asserted-by":"crossref","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 Syst. Des. 10(1), 47\u201371 (1997)","journal-title":"Formal Methods Syst. Des."},{"key":"140_CR12","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":"140_CR13","doi-asserted-by":"crossref","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 Syst. Des. 1, 275\u2013288 (1992)","journal-title":"Formal Methods Syst. Des."},{"key":"140_CR14","doi-asserted-by":"crossref","unstructured":"Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Proceedings of FM, pp. 253\u2013271 (1999)","DOI":"10.1007\/3-540-48119-2_16"},{"key":"140_CR15","doi-asserted-by":"crossref","unstructured":"Daniele, N., Guinchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Proceedigs of the 11th International Conference on CAV. LNCS, vol. 1633, pp. 249\u2013260. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48683-6_23"},{"key":"140_CR16","doi-asserted-by":"crossref","unstructured":"de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D. (eds.) Computer-Aided Verification, CAV 2004. Lecture Notes in Computer Science, vol. 3114, pp. 496\u2013500. Springer, Boston (2004)","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"140_CR17","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Poitrenaud, D.: SPOT: An extensible model checking library using transition-based generalized b\u00fcchi automata. In: Proceedings of the 12th International Workshop on MASCOTS, pp. 76\u201383. IEEE Computer Society, USA (2004)","DOI":"10.1109\/MASCOT.2004.1348184"},{"key":"140_CR18","first-page":"997","volume-title":"Handbook of Theoretical Computer Science, vol. B, ch. 16","author":"E.A. Emerson","year":"1990","unstructured":"Emerson E.A.: Temporal and modal logic. In: Van Leeuwen, J. (eds) Handbook of Theoretical Computer Science, vol. B, ch. 16, pp. 997\u20131072. Elsevier MIT Press, Amsterdam (1990)"},{"key":"140_CR19","unstructured":"Emerson, E.A., Lei, C.L.: Efficient model checking in fragments of the propositional\u00a0\u03bc-calculus. In: LICS, 1st Symp. pp. 267\u2013278, Cambridge (1986)"},{"key":"140_CR20","doi-asserted-by":"crossref","unstructured":"Etessami, K., Holzmann, G.J.: Optimizing B\u00fcchi automata. In: Proceedings of the 11th International Conference on CONCUR. Lecture Notes in CS 1877, pp. 153\u2013167. Springer, Berlin (2000)","DOI":"10.1007\/3-540-44618-4_13"},{"key":"140_CR21","doi-asserted-by":"crossref","unstructured":"Fritz, C.: Constructing B\u00fcchi automata from linear temporal logic using simulation relations for alternating b\u00fcchi automata. In: Proceedings of the 8th International conference on CIAA. Lecture Notes in Computer Science, vol. 2759, pp. 35\u201348. Springer, Berlin (2003)","DOI":"10.1007\/3-540-45089-0_5"},{"key":"140_CR22","doi-asserted-by":"crossref","unstructured":"Fritz, C.: Concepts of automata construction from LTL. In: Proceedings of the 12th International Conference on LPAR. Lecture Notes in Computer Science, vol. 3835, pp. 728\u2013742. Springer, Berlin (2005)","DOI":"10.1007\/11591191_50"},{"key":"140_CR23","doi-asserted-by":"crossref","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Proceedings of the 13th International Conference on CAV. LNCS, vol. 2102, pp. 53\u201365. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44585-4_6"},{"key":"140_CR24","doi-asserted-by":"crossref","unstructured":"Geldenhuys, J., Hansen, H.: Larger automata and less work for LTL model checking. In: Model Checking Software, 13th Int\u2019l SPIN Workshop. LNCS, vol. 3925, pp. 53\u201370. Springer, Berlin (2006)","DOI":"10.1007\/11691617_4"},{"key":"140_CR25","doi-asserted-by":"crossref","unstructured":"Geldenhuys, J., Valmari, A.: Tarjan\u2019s algorithm makes on-the-fly LTL verification more efficient. In: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2988, pp. 205\u2013219. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24730-2_18"},{"key":"140_CR26","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, pp. 3\u201318. Chapman & Hall, London (1995)"},{"key":"140_CR27","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulae to B\u00fcchi automata. In: Proceedings of 22 IFIP International Conference on FORTE (2002)","DOI":"10.1007\/3-540-36135-9_20"},{"key":"140_CR28","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Chechik, M.: Extending extended vacuity. In: 5th International Conferene on FMCAD. Lecture Notes in Computer Science, vol. 3312, pp 306\u2013321. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30494-4_22"},{"key":"140_CR29","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Chechik, M.: How vacuous is vacuous. In: 10th International Conference on TACAS. Lecture Notes in Computer Science, vol. 2988, pp. 451\u2013466. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24730-2_34"},{"issue":"5","key":"140_CR30","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997) Special issue on Formal Methods in Software Practice","journal-title":"IEEE Trans. Softw. Eng."},{"key":"140_CR31","doi-asserted-by":"crossref","unstructured":"Kupferman, O.: Sanity checks in formal verification. In: Proceedings of the 17th International Conference on CONCUR. Lecture Notes in Computer Science, vol. 4137, pp. 37\u201351. Springer, Berlin (2006)","DOI":"10.1007\/11817949_3"},{"issue":"2","key":"140_CR32","doi-asserted-by":"crossref","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. Softw. Tools Technol. Transf. 4(2), 224\u2013233 (2003)","journal-title":"J. Softw. Tools Technol. Transf."},{"key":"140_CR33","volume-title":"FormalCheck User\u2019s Manual","author":"R.P. Kurshan","year":"1998","unstructured":"Kurshan R.P.: FormalCheck User\u2019s Manual. Cadence Design, Inc., San Jose (1998)"},{"key":"140_CR34","unstructured":"McMillan, K.: The SMV language. Technical report, Cadence Berkeley Lab (1999)"},{"key":"140_CR35","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, Dordrecht (1993)"},{"key":"140_CR36","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.S.: An efficiently checkable, proof-based formulation of vacuity in model checking. In: 16th CAV. LNCS, vol. 3114, pp. 57\u201369. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27813-9_5"},{"key":"140_CR37","doi-asserted-by":"crossref","unstructured":"Pan, G., Sattler, U.,Vardi, M.Y.: BDD-based decision procedures for K. In: Proceedings of the 18th International conference on CADE. LNCS, vol. 2392, pp. 16\u201330. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45620-1_2"},{"issue":"1\u20133","key":"140_CR38","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 295(1\u20133), 295\u2013321 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"140_CR39","doi-asserted-by":"crossref","unstructured":"Purandare, M., Somenzi, F.: Vacuum cleaning CTL formulae. In: Proceeding of the 14th Conference on CAV. Lecture Notes in Computer Science, pp. 485\u2013499. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0_39"},{"key":"140_CR40","doi-asserted-by":"crossref","unstructured":"Sebastiani, R., Tonetta, S.: \u201cmore deterministic\u201d vs. \u201csmaller\u201d b\u00fcchi automata for efficient LTL model checking. In: CHARME, pp. 126\u2013140. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-39724-3_12"},{"key":"140_CR41","doi-asserted-by":"crossref","unstructured":"Sebastiani, R., Tonetta, S., Vardi, M.Y.: Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking. In: Proceedings of the 17th International Conference on CAV. Lecture Notes in Computer Science, vol. 3576, pp. 350\u2013373. Springer, Berlin (2005)","DOI":"10.1007\/11513988_35"},{"key":"140_CR42","doi-asserted-by":"crossref","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Proceedings of the 12th International Conference on CAV. LNCS, vol. 1855, pp. 248\u2013263. Springer, Berlin (2000)","DOI":"10.1007\/10722167_21"},{"issue":"1","key":"140_CR43","doi-asserted-by":"crossref","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. J. Softw. Tools Technol. Transf. 4(1), 57\u201370 (2002)","journal-title":"STTT Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"140_CR44","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/S1571-0661(04)80409-2","volume":"66","author":"X. Thirioux","year":"2002","unstructured":"Thirioux X.: Simple and efficient translation from LTL formulas to B\u00fcchi automata. Electr. Notes Theor. Comput. Sci. 66(2), 145\u2013159 (2002)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"140_CR45","doi-asserted-by":"crossref","unstructured":"Vardi M.Y.: Nontraditional applications of automata theory. In: Proceedings of the International conference on STACS. LNCS, vol. 789, pp. 575\u2013597. Springer, Berlin (1994)","DOI":"10.1007\/3-540-57887-0_116"},{"key":"140_CR46","doi-asserted-by":"crossref","unstructured":"Vardi M.Y.: Automata-theoretic model checking revisited. In: Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 4349, pp. 137\u2013150. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-69738-1_10"},{"key":"140_CR47","unstructured":"Vardi M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceeding of the 1st LICS, pp. 332\u2013344, Cambridge (1986)"},{"issue":"1","key":"140_CR48","doi-asserted-by":"crossref","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. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0140-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-010-0140-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0140-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T10:35:21Z","timestamp":1739961321000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-010-0140-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3,11]]},"references-count":48,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,5]]}},"alternative-id":["140"],"URL":"https:\/\/doi.org\/10.1007\/s10009-010-0140-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,3,11]]}}}