{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:20:52Z","timestamp":1781893252346,"version":"3.54.5"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2019,3,1]],"date-time":"2019-03-01T00:00:00Z","timestamp":1551398400000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"},{"start":{"date-parts":[[2018,3,1]],"date-time":"2018-03-01T00:00:00Z","timestamp":1519862400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,3,1]],"date-time":"2018-03-01T00:00:00Z","timestamp":1519862400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["91118007"],"award-info":[{"award-number":["91118007"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61021004"],"award-info":[{"award-number":["61021004"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61361136002"],"award-info":[{"award-number":["61361136002"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS 1049862"],"award-info":[{"award-number":["CNS 1049862"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2018,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We propose a novel algorithm for the satisfiability problem for linear temporal logic (LTL). Existing automata-based approaches first transform the LTL formula into a B\u00fcchi automaton and then perform an emptiness checking of the resulting automaton. Instead, our approach works on-the-fly by inspecting the formula directly, thus enabling to find a satisfying model quickly without constructing the full automaton. This makes our algorithm particularly fast for satisfiable formulas. We construct experiments on different pattern formulas, the experimental results show that our approach is superior to other solvers under automata-based framework.<\/jats:p>","DOI":"10.1007\/s00165-017-0442-2","type":"journal-article","created":{"date-parts":[[2017,11,9]],"date-time":"2017-11-09T13:00:27Z","timestamp":1510232427000},"page":"193-217","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["An explicit transition system construction approach to LTL satisfiability checking"],"prefix":"10.1145","volume":"30","author":[{"given":"Jianwen","family":"Li","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5922-8750","authenticated-orcid":false,"given":"Shufang","family":"Zhu","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[{"name":"Computer Science, Rice University, Houston, TX, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jifeng","family":"He","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Biere A Cimatti A Clarke EM Zhu Y (1999) Symbolic model checking without BDDs. In: Proceedings of the 5th international conference on tools and algorithms for the construction and analysis of systems volume 1579 of Lecture notes in computer science. Springer","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Bradley A (2011) Sat-based model checking without unrolling. In: Jhala R Schmidt D (eds) Verification model checking and abstract interpretation volume 6538 of Lecture notes in computer science pp 70\u201387. Springer Berlin","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bryant RE (1986) Graph-based algorithms for Boolean-function manipulation. IEEE Trans Comput C-35(8):677\u2013691","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Cimatti A Clarke EM Giunchiglia E Giunchiglia F Pistore M Roveri M Sebastiani R Tacchella A (2002) Nusmv 2: an opensource tool for symbolic model checking. In: Computer aided verification Lecture notes in computer science 2404 pp 359\u2013364. Springer","DOI":"10.1007\/3-540-45657-0_29"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"key":"e_1_2_1_2_9_2","volume-title":"Model checking","author":"Clarke EM","year":"1999"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Cimatti A Pistore M Roveri M Sebastiani R (2002) Improving the encoding of ltl model checking into sat. In: Revised papers from the third international workshop on verification model checking and abstract interpretation VMCAI \u201902 pp 196\u2013207. Springer London","DOI":"10.1007\/3-540-47813-2_14"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Cimatti A Roveri M Schuppan V Tonetta S (2007) Boolean abstraction for temporal logic satisfiability. In: Proceedings of the 15th international conference on computer aided verification volume 4590 of Lecture notes in computer science pp 532\u2013546. Springer","DOI":"10.1007\/978-3-540-73368-3_53"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121128"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Dwyer MB Avrunin GS Corbett JC (1998) Property specification patterns for finite-state verification. In: Proceedings of the 2nd workshop on formal methods in software practice pp 7\u201315. ACM","DOI":"10.1145\/298595.298598"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"De Wulf M Doyen L Maquet N Raskin J-F (2008) Antichains: alternative algorithms for ltl satisfiability and model-checking. In: Tools and algorithms for the construction and analysis of systems volume 4963 of Lecture notes in computer science pp 63\u201377. Springer","DOI":"10.1007\/978-3-540-78800-3_6"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Daniele N Guinchiglia F Vardi MY (1999) Improved automata generation for linear temporal logic. In: Proceedings of the 11th intenational conference on computer aided verification volume 1633 of Lecture notes in computer science pp 249\u2013260. Springer","DOI":"10.1007\/3-540-48683-6_23"},{"key":"e_1_2_1_2_16_2","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 pp 76\u201383. IEEE Computer Society","DOI":"10.1109\/MASCOT.2004.1348184"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-007-0062-z"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"E\u00e9n N S\u00f6rensson N (2003) An extensible sat-solver. In: SAT pp 502\u2013518","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/371282.371311"},{"key":"e_1_2_1_2_20_2","unstructured":"Fisher M (1991) A resolution method for temporal logic. In: In proceedings of the twelfth international joint conference on artificial intelligence pp 99\u2013104. IJCAI Morgan Kaufman"},{"key":"e_1_2_1_2_21_2","volume-title":"Assertion-based design","author":"Foster HD","year":"2004"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Kesten Y Manna Z McGuire H Pnueli A (1993) A decision algorithm for full propositional temporal logic. In: Courcoubeti C (ed) Proceedings of the 5th conference on computer aided verification volume 697 of Lecture notes in computer science pp 97\u2013109. Springer","DOI":"10.1007\/3-540-56922-7_9"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Li J Pu G Zhang L Wang Z He J Larsen KG (2013) On the relationship between ltl normal forms and b\u00fcchi automata. In: Liu Z Jim W Zhu H (eds) Theories of programming and formal methods volume 8051 of Lecture notes in computer science pp 256\u2013270. Springer","DOI":"10.1007\/978-3-642-39698-4_16"},{"key":"e_1_2_1_2_25_2","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":"e_1_2_1_2_26_2","unstructured":"McMillan K (1999) The SMV language. Technical report Cadence Berkeley Lab"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"McMillan K (2003) Interpolation and sat-based model checking. In: Jr. Hunt WarrenA Somenzi Fabio (eds) Computer aided verification volume 2725 of Lecture notes in computer science pp 1\u201313. Springer Berlin","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Pill I Semprini S Cavada R Roveri M Bloem R Cimatti A (2006) Formal analysis of hardware requirements. In: Proceedings of the 43rd design automation conference pp 821\u2013826. ACM","DOI":"10.1145\/1146909.1147119"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Rozier KY Vardi MY (2007) LTL satisfiability checking. In: Proceedings of the 14th international SPIN workshop volume 4595 of Lecture notes in computer science pp 149\u2013167. Springer","DOI":"10.1007\/978-3-540-73370-6_11"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Rozier KY Vardi MY (2010) LTL satisfiability checking. Int J Softw Tools Technol Transf 12(2): 1230\u2013137","DOI":"10.1007\/s10009-010-0140-3"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Rozier KY Vardi MY (2011) A multi-encoding approach for LTL symbolic satisfiability checking. In: Proceedings of the 17th International symposium on formal methods volume 6664 of Lecture notes in computer science pp 417\u2013431. Springer","DOI":"10.1007\/978-3-642-21437-0_31"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Sistla AP Clarke EM (1982) The complexity of propositional linear temporal logics. In: Proceedings of the 14th annual ACM symposium on theory of computing pp 159\u2013168","DOI":"10.1145\/800070.802189"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","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 pp 277\u2013292. Springer","DOI":"10.1007\/3-540-69778-0_28"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Schuppan V (2010) Towards a notion of unsatisfiable cores for ltl. In: Fundamentals of software engineering pp 129\u2013145","DOI":"10.1007\/978-3-642-11623-0_7"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Schuppan V Darmawan L (2011) Evaluating ltl satisfiability solvers. In: Proceedings of the 9th international conference on Automated technology for verification and analysis AVTA\u201911 pp 397\u2013413. Springer","DOI":"10.1007\/978-3-642-24372-1_28"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Vardi MY (2007) Automata-theoretic model checking revisited. In: Proceedings of the 8th international conference on verification model checking and abstract interpretation volume 4349 of Lecture notes in computer science pp 137\u2013150. Springer","DOI":"10.1007\/978-3-540-69738-1_10"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.04.009"},{"key":"e_1_2_1_2_40_2","unstructured":"Vardi MY Wolper P (1986) An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st IEEE symposium on logic in computer science pp 332\u2013344"},{"issue":"111","key":"e_1_2_1_2_41_2","first-page":"119","article-title":"The tableau method for temporal logic: an overview","volume":"110","author":"Wolper P","year":"1985","journal-title":"Logique Anal"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0442-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0442-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0442-2","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0442-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0442-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T23:16:18Z","timestamp":1750979778000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0442-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,3]]}},"alternative-id":["10.1007\/s00165-017-0442-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0442-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,3]]},"assertion":[{"value":"14 June 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 September 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 November 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}