{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T20:44:34Z","timestamp":1783111474458,"version":"3.54.6"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2019,11]]},"DOI":"10.1007\/s10703-018-00326-5","type":"journal-article","created":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T02:02:26Z","timestamp":1546394546000},"page":"164-190","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["SAT-based explicit LTL reasoning and its application to satisfiability checking"],"prefix":"10.1007","volume":"54","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9286-8285","authenticated-orcid":false,"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":"Lijun","family":"Zhang","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":[[2019,1,2]]},"reference":[{"key":"326_CR1","unstructured":"Bertello M, Gigante N, Montanari A, Reynolds M (2016) Leviathan: a new LTL satisfiability checking tool based on a one-pass tree-shaped tableau. In: Proceedings of the twenty-fifth international joint conference on artificial intelligence, IJCAI\u201916, pp 950\u2013956. AAAI Press. \nhttp:\/\/dl.acm.org\/citation.cfm?id=3060621.3060753"},{"key":"326_CR2","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, model checking, and abstract interpretation. Lecture notes in computer science","author":"A Bradley","year":"2011","unstructured":"Bradley A (2011) SAT-based model checking without unrolling. In: Jhala R, Schmidt D (eds) Verification, model checking, and abstract interpretation. Lecture notes in computer science, vol 6538. Springer, Berlin, pp 70\u201387"},{"key":"326_CR3","doi-asserted-by":"crossref","unstructured":"Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S (2014) The nuXmv symbolic model checker. In: CAV, pp 334\u2013342","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"326_CR4","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer aided verification. Lecture notes in computer science","author":"A Cimatti","year":"2002","unstructured":"Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) Nusmv 2: an opensource tool for symbolic model checking. In: Brinksma E, Larsen KG (eds) Computer aided verification. Lecture notes in computer science, vol 2404. Springer, Berlin, pp 359\u2013364"},{"key":"326_CR5","unstructured":"Claessen K, S\u00f6rensson N (2012) A liveness checking algorithm that counts. In: Cabodi G, Singh S (eds) FMCAD, pp 52\u201359. IEEE"},{"key":"326_CR6","volume-title":"Model checking","author":"E Clarke","year":"1999","unstructured":"Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge"},{"key":"326_CR7","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C Courcoubetis","year":"1992","unstructured":"Courcoubetis C, Vardi M, Wolper P, Yannakakis M (1992) Memory efficient algorithms for the verification of temporal properties. Form Methods Syst Des 1:275\u2013288","journal-title":"Form Methods Syst Des"},{"key":"326_CR8","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 (1999) Tableau methods for classical propositional logic. In: D\u2019Agostino M, Gabbay D, Haehnle R, Posegga J (eds) Handbook of tableau methods. Springer, Dordrecht, pp 45\u2013123"},{"key":"326_CR9","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Computer Aided Verification","author":"Marco Daniele","year":"1999","unstructured":"Daniele N, Guinchiglia F, Vardi M (1999) Improved automata generation for linear temporal logic. In: Proceedings of the 11th international conference on computer aided verification. Lecture notes in computer science, vol 1633. Springer, Berlin, pp 249\u2013260"},{"key":"326_CR10","doi-asserted-by":"crossref","unstructured":"Duret-Lutz A, Poitrenaud D (2004) 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. IEEE Computer Society, pp 76\u201383","DOI":"10.1109\/MASCOT.2004.1348184"},{"key":"326_CR11","unstructured":"E\u00e9n N, S\u00f6rensson N (2003) An extensible SAT-solver. In: SAT, pp 502\u2013518"},{"issue":"4","key":"326_CR12","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1093\/logcom\/7.4.429","volume":"7","author":"M Fisher","year":"1997","unstructured":"Fisher M (1997) A normal form for temporal logics and its applications in theorem-proving and execution. J Log Comput 7(4):429\u2013456","journal-title":"J Log Comput"},{"issue":"1","key":"326_CR13","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/371282.371311","volume":"2","author":"M Fisher","year":"2001","unstructured":"Fisher M, Dixon C, Peim M (2001) Clausal temporal resolution. ACM Trans Comput Log 2(1):12\u201356","journal-title":"ACM Trans Comput Log"},{"key":"326_CR14","first-page":"3","volume-title":"Protocol specification, testing, and verification","author":"R Gerth","year":"1995","unstructured":"Gerth R, Peled D, Vardi M, Wolper P (1995) Simple on-the-fly automatic verification of linear temporal logic. In: Dembiski P, Sredniawa M (eds) Protocol specification, testing, and verification. Chapman & Hall, Boca Raton, pp 3\u201318"},{"key":"326_CR15","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/3-540-61511-3_115","volume-title":"Automated Deduction \u2014 Cade-13","author":"Fausto Giunchiglia","year":"1996","unstructured":"Giunchiglia F, Sebastiani R (1996) Building decision procedures for modal logics from propositional decision procedure\u2014the case study of modal K. In: Proceedings of 13th international conference on automated deduction. Lecture notes in computer science, vol 1104. Springer, Berlin, pp 583\u2013597"},{"key":"326_CR16","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11513988_10","volume-title":"Computer aided verification. Lecture notes in computer science","author":"K Heljanko","year":"2005","unstructured":"Heljanko K, Junttila T, Latvala T (2005) Incremental and complete bounded model checking for full PLTL. In: Etessami K, Rajamani S (eds) Computer aided verification. Lecture notes in computer science, vol 3576. Springer, Berlin, pp 98\u2013111"},{"key":"326_CR17","volume-title":"The SPIN model checker: primer and reference manual","author":"G Holzmann","year":"2003","unstructured":"Holzmann G (2003) The SPIN model checker: primer and reference manual. Addison-Wesley, Boston"},{"key":"326_CR18","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-45085-6_21","volume-title":"Automated Deduction \u2013 CADE-19","author":"Ullrich Hustadt","year":"2003","unstructured":"Hustadt U, Konev B (2003) Trp++ 2.0: a temporal resolution prover. In: Proceedings of CADE-19. LNAI. Springer, Berlin, pp 274\u2013278"},{"key":"326_CR19","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-642-38574-2_31","volume-title":"Automated Deduction \u2013 CADE-24","author":"Mark Kaminski","year":"2013","unstructured":"Kaminski M, Tebbi T (2013) Inkresat: modal reasoning via incremental reduction to sat. In: Bonacina MP (ed) International conference on automated deduction\u2014CADE-24. Springer, Berlin, pp 436\u2013442"},{"issue":"1","key":"326_CR20","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1109\/43.108614","volume":"11","author":"T Larrabee","year":"1992","unstructured":"Larrabee T (1992) Test pattern generation using boolean satisfiability. IEEE Trans Comput Aided Des Integr Circuits Syst 11(1):4\u201315","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"key":"326_CR21","unstructured":"Li J, Pu G, Zhang L, Vardi MY, He J (2014) Fast LTL satisfiability checking by SAT solvers. CoRR \narXiv:1401.5677"},{"key":"326_CR22","doi-asserted-by":"crossref","unstructured":"Li J, Zhang L, Pu G, Vardi M, He J (2013) LTL satisfibility checking revisited. In: The 20th international symposium on temporal representation and reasoning, pp 91\u201398","DOI":"10.1109\/TIME.2013.19"},{"key":"326_CR23","first-page":"209","volume-title":"SAT-based explicit LTL reasoning","author":"J Li","year":"2015","unstructured":"Li J, Zhu S, Pu G, Vardi M (2015) SAT-based explicit LTL reasoning. Springer, Berlin, pp 209\u2013224"},{"issue":"8","key":"326_CR24","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1536616.1536637","volume":"52","author":"S Malik","year":"2009","unstructured":"Malik S, Zhang L (2009) Boolean satisfiability from theoretical hardness to practical success. Commun ACM 52(8):76\u201382","journal-title":"Commun ACM"},{"key":"326_CR25","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 (1992) The temporal logic of reactive and concurrent systems: specification. Springer, Berlin"},{"key":"326_CR26","doi-asserted-by":"crossref","unstructured":"Manquinho VM, Flores PF, Silva JPM, Oliveira AL (1997) Prime implicant computation using satisfiability algorithms. In: Proceedings of ninth IEEE international conference on tools with artificial intelligence, pp 232\u2013239","DOI":"10.1109\/TAI.1997.632261"},{"key":"326_CR27","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-642-21581-0_14","volume-title":"Theory and applications of satisfiability testing\u2014SAT 2011. Lecture notes in computer science","author":"J Marques-Silva","year":"2011","unstructured":"Marques-Silva J, Lynce I (2011) On improving MUS extraction algorithms. In: Sakallah K, Simon L (eds) Theory and applications of satisfiability testing\u2014SAT 2011. Lecture notes in computer science, vol 6695. Springer, Berlin, pp 159\u2013173"},{"key":"326_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"K McMillan","year":"1993","unstructured":"McMillan K (1993) Symbolic model checking. Kluwer Academic Publishers, Dordrecht"},{"key":"326_CR29","first-page":"1","volume-title":"Computer Aided Verification","author":"K. L. McMillan","year":"2003","unstructured":"McMillan K (2003) Interpolation and SAT-based model checking. In: Hunt WA Jr., Somenzi F (eds) International conference on computer aided verification. Lecture notes in computer science, vol 2725. Springer, Berlin, pp 1\u201313"},{"key":"326_CR30","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of 18th IEEE symposium on foundations of computer science, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"issue":"2","key":"326_CR31","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10009-010-0140-3","volume":"12","author":"K Rozier","year":"2010","unstructured":"Rozier K, Vardi M (2010) LTL satisfiability checking. Int J Softw Tools Technol Transf 12(2):123\u2013137","journal-title":"Int J Softw Tools Technol Transf"},{"key":"326_CR32","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":"Viktor Schuppan","year":"2011","unstructured":"Schuppan V, Darmawan L (2011) Evaluating LTL satisfiability solvers. In: Proceedings of the 9th international conference on automated technology for verification and analysis, ATVA\u201911. Springer, Berlin, pp 397\u2013413"},{"key":"326_CR33","first-page":"277","volume-title":"Lecture Notes in Computer Science","author":"Stefan Schwendimann","year":"1998","unstructured":"Schwendimann S (1998) A new one-pass tableau calculus for PLTL. In: Proceedings of the international conference on automated reasoning with analytic tableaux and related methods. Springer, Berlin, pp 277\u2013292"},{"key":"326_CR34","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":"Stefan Schwoon","year":"2005","unstructured":"Schwoon S, Esparza J (2005) A note on on-the-fly verification algorithms. In: Proceedings 11th international conference on tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol 3440. Springer, Berlin, pp 174\u2013190"},{"key":"326_CR35","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"Fabio Somenzi","year":"2000","unstructured":"Somenzi F, Bloem R (2000) Efficient B\u00fcchi automata from LTL formulae. In: Proceedings of 12th international conference on computer aided verification. Lecture notes in computer science, vol 1855. Springer, Berlin, pp 248\u2013263"},{"issue":"3","key":"326_CR36","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/s11786-015-0240-2","volume":"9","author":"M Suda","year":"2015","unstructured":"Suda M (2015) Variable and clause elimination for LTL satisfiability checking. Math Comput Sci 9(3):327\u2013344","journal-title":"Math Comput Sci"},{"key":"326_CR37","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/978-3-642-31365-3_42","volume-title":"Automated Reasoning","author":"Martin Suda","year":"2012","unstructured":"Suda M, Weidenbach C (2012) A PLTL-prover based on labelled superposition with partial model guidance. In: International joint conference on automated reasoning. Lecture notes in computer science, vol 7364. Springer, Berlin, pp 537\u2013543"},{"issue":"3","key":"326_CR38","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, Vardi MY (2012) Optimized temporal monitors for SystemC. Form Methods Syst Des 41(3):236\u2013268","journal-title":"Form Methods Syst Des"},{"key":"326_CR39","doi-asserted-by":"crossref","unstructured":"Vardi M (1989) On the complexity of epistemic reasoning. In: Proceedings of the fourth annual symposium on logic in computer science. IEEE Press, Piscataway, pp 243\u2013252","DOI":"10.1109\/LICS.1989.39179"},{"key":"326_CR40","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-51803-7_27","volume-title":"Temporal Logic in Specification","author":"Moshe Y. Vardi","year":"1989","unstructured":"Vardi M (1989) Unified verification theory. In: Banieqbal B, Barringer H, Pnueli A (eds) Proceedings of temporal logic in specification, vol 398. Springer, Berlin, pp 202\u2013212"},{"key":"326_CR41","unstructured":"Vardi M, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: Proceedings of 1st IEEE symposium on logic in computer science, pp 332\u2013344"},{"key":"326_CR42","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-642-38574-2_30","volume-title":"Automated Deduction \u2013 CADE-24","author":"Richard Williams","year":"2013","unstructured":"Williams R, Konev B (2013) Propositional temporal proving with reductions to a sat problem. In: Bonacina MP (ed) International conference on automated deduction\u2014CADE-24. Springer, Berlin, pp 421\u2013435"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-00326-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-018-00326-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-00326-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T19:21:38Z","timestamp":1577906498000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-018-00326-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,11]]}},"alternative-id":["326"],"URL":"https:\/\/doi.org\/10.1007\/s10703-018-00326-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2 January 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}