{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:24Z","timestamp":1760202624424,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642214363"},{"type":"electronic","value":"9783642214370"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-21437-0_31","type":"book-chapter","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T07:33:16Z","timestamp":1308382396000},"page":"417-431","source":"Crossref","is-referenced-by-count":27,"title":["A Multi-encoding Approach for LTL Symbolic Satisfiability Checking"],"prefix":"10.1007","author":[{"given":"Kristin Y.","family":"Rozier","sequence":"first","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"31_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/11560548_20","volume-title":"Correct Hardware Design and Verification Methods","author":"N. Amla","year":"2005","unstructured":"Amla, N., Du, X., Kuehlmann, A., Kurshan, R.P., McMillan, K.L.: An analysis of SAT-based model checking techniques in an industrial environment. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 254\u2013268. Springer, Heidelberg (2005)"},{"issue":"2","key":"31_CR2","first-page":"141","volume":"18","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. FMSD\u00a018(2), 141\u2013162 (2001)","journal-title":"FMSD"},{"key":"31_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. In: FMICS, vol.\u00a066(2) (2002)","DOI":"10.1016\/S1571-0661(04)80410-9"},{"issue":"4","key":"31_CR4","first-page":"727","volume":"18","author":"R. Bloem","year":"2007","unstructured":"Bloem, R., Cimatti, A., Pill, I., Roveri, M.: Symbolic implementation of alternating automata. IJFCS\u00a018(4), 727\u2013743 (2007)","journal-title":"IJFCS"},{"issue":"8","key":"31_CR5","first-page":"677","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean-function manipulation. IEEE TC\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE TC"},{"issue":"2","key":"31_CR6","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. Inform. and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Inform. and Computation"},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"Cichon, J., Czubak, A., Jasinski, A.: Minimal B\u00fcchi automata for certain classes of LTL formulas. In: DepCoS, pp. 17\u201324 (2009)","DOI":"10.1109\/DepCoS-RELCOMEX.2009.31"},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Roveri, M., Semprini, S., Tonetta, S.: From PSL to NBA: A modular symbolic encoding. In: FMCAD (2006)","DOI":"10.1109\/FMCAD.2006.19"},{"key":"31_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/978-3-540-71209-1_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Cimatti","year":"2007","unstructured":"Cimatti, A., Roveri, M., Tonetta, S.: Syntactic optimizations for PSL verification. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 505\u2013518. Springer, Heidelberg (2007)"},{"issue":"1","key":"31_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":"31_CR11","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)"},{"key":"31_CR12","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: Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 253\u2013271. Springer, Heidelberg (1999)"},{"key":"31_CR13","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":"31_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-540-78800-3_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. De Wulf","year":"2008","unstructured":"De Wulf, M., Doyen, L., Maquet, N., Raskin, J.: Antichains: Alternative algorithms for LTL satisfiability and model-checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 63\u201377. Springer, Heidelberg (2008)"},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Poitrenaud, D.: SPOT: An extensible model checking library using Transition-Based Generalized B\u00fcchi Automata. In: MASCOTS, pp. 76\u201383 (2004)","DOI":"10.1109\/MASCOT.2004.1348184"},{"key":"31_CR16","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, vol.\u00a0B, ch. 16, pp. 997\u20131072. Elsevier, MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"31_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11591191_34","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A. Ferrara","year":"2005","unstructured":"Ferrara, A., Pan, G., Vardi, M.Y.: Treewidth in verification: Local vs. Global. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 489\u2013503. Springer, Heidelberg (2005)"},{"issue":"4","key":"31_CR18","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1093\/logcom\/7.4.429","volume":"7","author":"M. Fisher","year":"1997","unstructured":"Fisher, M.: A normal form for temporal logics and its applications in theorem-proving and execution. J. Log. Comput.\u00a07(4), 429\u2013456 (1997)","journal-title":"J. Log. Comput."},{"key":"31_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-642-01702-5_7","volume-title":"Hardware and Software: Verification and Testing","author":"D. Fisman","year":"2009","unstructured":"Fisman, D., Kupferman, O., Sheinvald-Faragy, S., Vardi, M.Y.: A framework for inherent vacuity. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol.\u00a05394, pp. 7\u201322. Springer, Heidelberg (2009)"},{"key":"31_CR20","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":"31_CR21","first-page":"3","volume-title":"PSTV","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: PSTV, pp. 3\u201318. Chapman and Hall, Boca Raton (1995)"},{"key":"31_CR22","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulae to B\u00fcchi automata. In: FORTE (November 2002)","DOI":"10.1007\/3-540-36135-9_20"},{"key":"31_CR23","first-page":"113","volume":"262","author":"V. Goranko","year":"2010","unstructured":"Goranko, V., Kyrilov, A., Shkatov, D.: Tableau tool for testing satisfiability in LTL: Implementation and experimental analysis. ENTCS\u00a0262, 113\u2013125 (2010)","journal-title":"ENTCS"},{"key":"31_CR24","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1109\/DATE.2005.112","volume-title":"Design, Automation and Test in Europe","author":"A. Habibi","year":"2005","unstructured":"Habibi, A., Tahar, S.: Design for verification of SystemC transaction level models. In: Design, Automation and Test in Europe, pp. 560\u2013565. IEEE, Los Alamitos (2005)"},{"key":"31_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-56922-7_9","volume-title":"Computer Aided Verification","author":"Y. Kesten","year":"1993","unstructured":"Kesten, Y., Manna, Z., McGuire, H., Pnueli, A.: A decision algorithm for full propositional temporal logic. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 97\u2013109. Springer, Heidelberg (1993)"},{"key":"31_CR26","unstructured":"Koster, A.M.C.A., Bodlaender, H.L., van Hoesel, S.P.M.: Treewidth: Computational experiments. ZIB-Report 01\u201338, ZIB (2001)"},{"issue":"2","key":"31_CR27","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. STTT\u00a04(2), 224\u2013233 (2003)","journal-title":"STTT"},{"key":"31_CR28","unstructured":"Merz, S., Sezgin, A.: Emptiness of Linear Weak Alternating Automata. Technical report, LORIA (December 2003)"},{"key":"31_CR29","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","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.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 16\u201330. Springer, Heidelberg (2002)"},{"key":"31_CR30","first-page":"821","volume-title":"DAC","author":"I. Pill","year":"2006","unstructured":"Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R., Cimatti, A.: Formal analysis of hardware requirements. In: DAC, pp. 821\u2013826. ACM, New York (2006)"},{"key":"31_CR31","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: IEEE FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"31_CR32","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"issue":"1","key":"31_CR33","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/s10601-008-9051-2","volume":"14","author":"L. Pulina","year":"2009","unstructured":"Pulina, L., Tacchella, A.: A self-adaptive multi-engine solver for quantified Boolean formulas. Constraints\u00a014(1), 80\u2013116 (2009)","journal-title":"Constraints"},{"key":"31_CR34","unstructured":"Roveri, M.: Novel techniques for property assurance. Technical report, PROSYD deliverable 1.2\/2 (2004)"},{"key":"31_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Model Checking Software","author":"K.Y. Rozier","year":"2007","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 149\u2013167. Springer, Heidelberg (2007)"},{"key":"31_CR36","unstructured":"Ruah, S., Fedeli, A., Eisner, C., Moulin, M.: Property-driven specification of VLSI design. Technical report, PROSYD deliverable 1.1\/1 (2005)"},{"key":"31_CR37","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)"},{"key":"31_CR38","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\u201d vs. \u201csmaller\u201d 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":"31_CR39","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of Propositional Linear Temporal Logic. J. ACM\u00a032, 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"31_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":"2","key":"31_CR41","first-page":"145","volume":"66","author":"X. Thirioux","year":"2002","unstructured":"Thirioux, X.: Simple and efficient translation from LTL formulas to B\u00fcchi automata. ENTCS\u00a066(2), 145\u2013159 (2002)","journal-title":"ENTCS"},{"key":"31_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"31_CR43","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, Cambridge, pp. 332\u2013344 (June 1986)"},{"issue":"1","key":"31_CR44","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","FM 2011: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21437-0_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,6]],"date-time":"2025-03-06T09:47:10Z","timestamp":1741254430000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21437-0_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214363","9783642214370"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21437-0_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}