{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T20:44:38Z","timestamp":1783111478799,"version":"3.54.6"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319262864","type":"print"},{"value":"9783319262871","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-26287-1_13","type":"book-chapter","created":{"date-parts":[[2015,10,26]],"date-time":"2015-10-26T05:44:58Z","timestamp":1445838298000},"page":"209-224","source":"Crossref","is-referenced-by-count":18,"title":["SAT-Based Explicit LTL Reasoning"],"prefix":"10.1007","author":[{"given":"Jianwen","family":"Li","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shufang","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,11,28]]},"reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Heidelberg (2014)"},{"key":"13_CR3","unstructured":"Claessen, K., S\u00f6rensson, N.: A liveness checking algorithm that counts. In: Cabodi, G., Singh, S. (ed.) FMCAD, pp. 52\u201359. IEEE (2012)"},{"key":"13_CR4","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"13_CR5","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 Syst. Des. 1, 275\u2013288 (1992)","journal-title":"Formal Methods Syst. Des."},{"key":"13_CR6","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-94-017-1754-0_2","volume-title":"Handbook of Tableau Methods","author":"M D\u2019Agostino","year":"1999","unstructured":"D\u2019Agostino, M.: Tableau methods for classical propositional logic. In: D\u2019Agostino, M., Gabbay, D.M., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 45\u2013123. Springer, Netherlands (1999)"},{"key":"13_CR7","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. 1633, pp. 249\u2013260. Springer, Heidelberg (1999)"},{"key":"13_CR8","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 Modeling, Analysis, and Simulation of Computer and Telecommunication Systems, pp. 76\u201383. IEEE Computer Society (2004)","DOI":"10.1109\/MASCOT.2004.1348184"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"issue":"4","key":"13_CR10","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. Logic Comput. 7(4), 429\u2013456 (1997)","journal-title":"J. Logic Comput."},{"key":"13_CR11","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, Warsaw (1995)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/3-540-61511-3_115","volume-title":"Automated Deduction - Cade-13","author":"F Giunchiglia","year":"1996","unstructured":"Giunchiglia, F., Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures - the case study of modal K. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 583\u2013597. Springer, Heidelberg (1996)"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11513988_10","volume-title":"Computer Aided Verification","author":"K Heljanko","year":"2005","unstructured":"Heljanko, K., Junttila, T.A., Latvala, T.: Incremental and complete bounded model checking for full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 98\u2013111. Springer, Heidelberg (2005)"},{"key":"13_CR14","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-45085-6_21","volume-title":"Automated Deduction \u2013 CADE-19","author":"U Hustadt","year":"2003","unstructured":"Hustadt, U., Konev, B.: TRP++ 2.0: a temporal resolution prover. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 274\u2013278. Springer, Heidelberg (2003)"},{"issue":"1","key":"13_CR16","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1109\/43.108614","volume":"11","author":"T Larrabee","year":"1992","unstructured":"Larrabee, T.: Test pattern generation using Boolean satisfiability. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst 11(1), 4\u201315 (1992)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Li, J., Pu, G., Zhang, L., Vardi, M.Y., He, J.: Fast LTL satisfiability checking by SAT solvers. CoRR, abs\/1401.5677 (2014)","DOI":"10.1109\/TIME.2013.19"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Li, J., Zhang, L., Pu, G., Vardi, M., He, J.: LTL satisfibility checking revisited. In: 20th International Symposium on Temporal Representation and Reasoning, pp. 91\u201398 (2013)","DOI":"10.1109\/TIME.2013.19"},{"issue":"8","key":"13_CR19","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1536616.1536637","volume":"52","author":"S Malik","year":"2009","unstructured":"Malik, S., Zhang, L.: Boolean satisfiability from theoretical hardness to practical success. Commun. ACM 52(8), 76\u201382 (2009)","journal-title":"Commun. ACM"},{"key":"13_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1992)"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-642-21581-0_14","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"J Marques-Silva","year":"2011","unstructured":"Marques-Silva, J., Lynce, I.: On improving MUS extraction algorithms. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 159\u2013173. Springer, Heidelberg (2011)"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"13_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Boston (1993)"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"2","key":"13_CR25","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10009-010-0140-3","volume":"12","author":"KY Rozier","year":"2010","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. Int. J. Softw. Tools Technol. Transf. 12(2), 123\u2013137 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-642-24372-1_28","volume-title":"Automated Technology for Verification and Analysis","author":"V Schuppan","year":"2011","unstructured":"Schuppan, V., Darmawan, L.: Evaluating LTL satisfiability solvers. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 397\u2013413. Springer, Heidelberg (2011)"},{"key":"13_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. 3440, pp. 174\u2013190. Springer, Heidelberg (2005)"},{"key":"13_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. 1855. Springer, Heidelberg (2000)"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/978-3-642-31365-3_42","volume-title":"Automated Reasoning","author":"M Suda","year":"2012","unstructured":"Suda, M., Weidenbach, C.: A PLTL-prover based on labelled superposition with partial model guidance. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 537\u2013543. Springer, Heidelberg (2012)"},{"issue":"3","key":"13_CR30","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/s10703-011-0139-8","volume":"41","author":"D Tabakov","year":"2012","unstructured":"Tabakov, D., Rozier, K.Y., Vardi, M.Y.: Optimized temporal monitors for SystemC. Formal Methods Syst. Des. 41(3), 236\u2013268 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"13_CR31","doi-asserted-by":"crossref","unstructured":"Vardi, M.: On the complexity of epistemic reasoning. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pp. 243\u2013252. IEEE Press, Piscataway (1989)","DOI":"10.1109\/LICS.1989.39179"},{"key":"13_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-51803-7_27","volume-title":"Temporal Logic in Specification","author":"MY Vardi","year":"1989","unstructured":"Vardi, M.Y.: Unified verification theory. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 202\u2013212. Springer, Heidelberg (1989)"},{"key":"13_CR33","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st IEEE Symposium on Logic in Computer Science, pp. 332\u2013344 (1986)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-26287-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:12:54Z","timestamp":1748664774000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-26287-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319262864","9783319262871"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-26287-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}