{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T10:41:02Z","timestamp":1768214462571,"version":"3.49.0"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T00:00:00Z","timestamp":1759104000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T00:00:00Z","timestamp":1759104000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100003787","name":"Hebei Natural Science Foundation","doi-asserted-by":"crossref","award":["No. F2024201004"],"award-info":[{"award-number":["No. F2024201004"]}],"id":[{"id":"10.13039\/501100003787","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100003787","name":"Hebei Natural Science Foundation","doi-asserted-by":"crossref","award":["No. F2024201004"],"award-info":[{"award-number":["No. F2024201004"]}],"id":[{"id":"10.13039\/501100003787","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Advanced Talents Incubation Program of the Hebei University","award":["No. 521000981346"],"award-info":[{"award-number":["No. 521000981346"]}]},{"name":"Advanced Talents Incubation Program of the Hebei University","award":["No. 521000981346"],"award-info":[{"award-number":["No. 521000981346"]}]},{"name":"the Innovation Capacity Enhancement Program-Science and Technology Platform Project of Hebei Province","award":["No. 22567638H"],"award-info":[{"award-number":["No. 22567638H"]}]},{"name":"the Innovation Capacity Enhancement Program-Science and Technology Platform Project of Hebei Province","award":["No. 22567638H"],"award-info":[{"award-number":["No. 22567638H"]}]},{"name":"Science Research Project of Hebei Education Department","award":["No. BJK2024095"],"award-info":[{"award-number":["No. BJK2024095"]}]},{"name":"Science Research Project of Hebei Education Department","award":["No. BJK2024095"],"award-info":[{"award-number":["No. BJK2024095"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Software Qual J"],"published-print":{"date-parts":[[2025,12]]},"DOI":"10.1007\/s11219-025-09729-0","type":"journal-article","created":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T05:00:31Z","timestamp":1759122031000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["CPD$$_{\\textrm{LTLf}}$$ : a linear temporal logic over finite traces guided model checking tool"],"prefix":"10.1007","volume":"33","author":[{"given":"Xiangqi","family":"Zeng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meng","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miao","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xu","family":"Lu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,29]]},"reference":[{"key":"9729_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T. & Rajamani, S. K. (2001). Automatically validating temporal safety properties of interfaces. In: International SPIN Workshop on Model Checking of Software (pp. 102\u2013122). Springer.","DOI":"10.1007\/3-540-45139-0_7"},{"key":"9729_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., & Rajamani, S. K. (2001). Automatic predicate abstraction of c programs. In: Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation (pp. 203\u2013213).","DOI":"10.1145\/378795.378846"},{"key":"9729_CR3","doi-asserted-by":"crossref","unstructured":"Baranov\u00e1, Z., Barnat, J., Kejstov\u00e1, K., Ku\u010dera, T., Lauko, H., Mr\u00e1zek, J., Ro\u010dkai, P., & \u0160till, V. (2017). Model checking of c and c++ with divine 4. In: Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3\u20136, 2017, Proceedings 15 (pp. 201\u2013207). Springer.","DOI":"10.1007\/978-3-319-68167-2_14"},{"key":"9729_CR4","first-page":"1","volume-title":"Introduction to runtime verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., & Reger, G. (2018). Introduction to runtime verification (pp. 1\u201333). Lectures on Runtime Verification: Introductory and Advanced Topics."},{"key":"9729_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D., & Keremoglu, M. E. (2011). Cpachecker: A tool for configurable software verification. In: Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings 23 (pp. 184\u2013190). Springer.","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"9729_CR6","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., & Zhu, Y. (1999). Symbolic model checking without bdds. In: Tools and Algorithms for the Construction and Analysis of Systems: 5th International Conference, TACAS\u201999 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS\u201999 Amsterdam, The Netherlands, March 22\u201328, 1999 Proceedings 5 (pp. 193\u2013207). Springer.","DOI":"10.1007\/3-540-49059-0_14"},{"key":"9729_CR7","unstructured":"Cadar, C., Dunbar, D., & Engler, D. R. (2008). Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI (vol. 8, pp. 209\u2013224)."},{"issue":"2","key":"9729_CR8","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/2408776.2408795","volume":"56","author":"C Cadar","year":"2013","unstructured":"Cadar, C., & Sen, K. (2013). Symbolic execution for software testing: three decades later. Communications of the ACM, 56(2), 82\u201390.","journal-title":"Communications of the ACM"},{"key":"9729_CR9","doi-asserted-by":"crossref","unstructured":"Camacho, A., Triantafillou, E., Muise, C., Baier, J., & McIlraith, S. (2017). Non-deterministic planning with temporally extended goals: Ltl over finite and infinite traces. In: Proceedings of the AAAI Conference on Artificial Intelligence (vol. 31).","DOI":"10.1609\/aaai.v31i1.11058"},{"key":"9729_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., & Emerson, E. A. (1981). Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on Logic of Programs (pp. 52\u201371). Springer.","DOI":"10.1007\/BFb0025774"},{"issue":"5","key":"9729_CR11","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., & Veith, H. (2003). Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM (JACM), 50(5), 752\u2013794.","journal-title":"Journal of the ACM (JACM)"},{"key":"9729_CR12","doi-asserted-by":"crossref","unstructured":"De\u00a0Giacomo, G., & Favorito, M. (2021). Compositional approach to translate ltlf\/ldlf into deterministic finite automata. In: Proceedings of the International Conference on Automated Planning and Scheduling (vol. 31, pp. 122\u2013130)","DOI":"10.1609\/icaps.v31i1.15954"},{"key":"9729_CR13","unstructured":"De\u00a0Giacomo, G., & Vardi, M. Y. (2013). Linear temporal logic and linear dynamic logic on finite traces. In: Ijcai (vol. 13, pp. 854\u2013860)."},{"key":"9729_CR14","doi-asserted-by":"crossref","unstructured":"De\u00a0Giacomo, G., De\u00a0Masellis, R., & Montali, M. (2014). Reasoning on ltl on finite traces: Insensitivity to infiniteness. In: Proceedings of the AAAI Conference on Artificial Intelligence (vol. 28).","DOI":"10.1609\/aaai.v28i1.8872"},{"key":"9729_CR15","unstructured":"Fuggitti, F. (2019). Ltlf2dfa. Zenodo, Mar."},{"key":"9729_CR16","doi-asserted-by":"crossref","unstructured":"Godefroid, P. (1997). Model checking for programming languages using verisoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 174\u2013186).","DOI":"10.1145\/263699.263717"},{"issue":"5","key":"9729_CR17","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G. J. (1997). The model checker spin. IEEE Transactions on software engineering, 23(5), 279\u2013295.","journal-title":"IEEE Transactions on software engineering"},{"key":"9729_CR18","unstructured":"Howard, Y., Gruner, S., Gravell, A., Ferreira, C., & Augusto, J. C. (2011). Model-based trace-checking. arXiv preprint arXiv:1111.2825"},{"key":"9729_CR19","doi-asserted-by":"crossref","unstructured":"Kejstov\u00e1, K., Ro\u010dkai, P., & Barnat, J. (2017). From model checking to runtime verification and back. In: Runtime Verification: 17th International Conference, RV 2017, Seattle, WA, USA, September 13-16, 2017, Proceedings 17, (pp. 225\u2013240). Springer.","DOI":"10.1007\/978-3-319-67531-2_14"},{"issue":"3","key":"9729_CR20","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1109\/MRA.2011.942116","volume":"18","author":"H Kress-Gazit","year":"2011","unstructured":"Kress-Gazit, H., Wongpiromsarn, T., & Topcu, U. (2011). Correct, reactive, high-level robot control. IEEE Robotics & Automation Magazine, 18(3), 65\u201374.","journal-title":"IEEE Robotics & Automation Magazine"},{"key":"9729_CR21","unstructured":"Kroening, D., & Tautschnig, M. (2014). Cbmc\u2013c bounded model checker: (competition contribution). In: Tools and Algorithms for the Construction and Analysis of Systems: 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings 20 (pp. 389\u2013391). Springer."},{"key":"9729_CR22","doi-asserted-by":"crossref","unstructured":"Legunsen, O., Hassan, W. U., Xu, X., Ro\u015fu, G., & Marinov, D. (2016). How good are the specs? a study of the bug-finding effectiveness of existing java api specifications. In: Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering (pp. 602\u2013613).","DOI":"10.1145\/2970276.2970356"},{"key":"9729_CR23","doi-asserted-by":"crossref","unstructured":"Li, J., Pu, G., Zhang, Y., Vardi, M. Y., & Rozier, K. Y. (2020). Sat-based explicit ltlf satisfiability checking. Artificial Intelligence,289, 103369.","DOI":"10.1016\/j.artint.2020.103369"},{"key":"9729_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A. (2005). Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. Current Trends in Concurrency: Overviews and Tutorials, 510\u2013584.","DOI":"10.1007\/BFb0027047"},{"key":"9729_CR25","doi-asserted-by":"crossref","unstructured":"Pnueli, A., & Rosner, R. (1989). On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 179\u2013190).","DOI":"10.1145\/75277.75293"},{"key":"9729_CR26","doi-asserted-by":"crossref","unstructured":"Queille, J.-P., & Sifakis, J. (1982). Specification and verification of concurrent systems in cesar. In: International Symposium on Programming (pp. 337\u2013351). Springer.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"9729_CR27","doi-asserted-by":"crossref","unstructured":"Ro\u010dkai, P., Barnat, J., & Brim, L. (2013). Improved state space reductions for ltl model checking of c and c++ programs. In: NASA Formal Methods Symposium (pp. 1\u201315). Springer.","DOI":"10.1007\/978-3-642-38088-4_1"},{"key":"9729_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jss.2018.04.026","volume":"143","author":"P Ro\u010dkai","year":"2018","unstructured":"Ro\u010dkai, P., \u0160till, V., \u010cern\u00e1, I., & Barnat, J. (2018). Divm: model checking with llvm and graph memory. Journal of Systems and Software, 143, 1\u201313.","journal-title":"Journal of Systems and Software"},{"key":"9729_CR29","doi-asserted-by":"crossref","unstructured":"\u0160till, V., Ro\u010dkai, P., & Barnat, J. (2016). Divine: Explicit-state ltl model checker: (competition contribution). In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (pp. 920\u2013922). Springer.","DOI":"10.1007\/978-3-662-49674-9_60"},{"key":"9729_CR30","unstructured":"Vardi, M. Y., & Wolper, P. (1986). An automata-theoretic approach to automatic program verification. In: 1st Symposium in Logic in Computer Science (LICS). IEEE Computer Society."},{"issue":"4","key":"9729_CR31","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1109\/85.238389","volume":"15","author":"J Von Neumann","year":"1993","unstructured":"Von Neumann, J. (1993). First draft of a report on the edvac. IEEE Annals of the History of Computing, 15(4), 27\u201375.","journal-title":"IEEE Annals of the History of Computing"}],"container-title":["Software Quality Journal"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-025-09729-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11219-025-09729-0","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-025-09729-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:47:01Z","timestamp":1768204021000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11219-025-09729-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,29]]},"references-count":31,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["9729"],"URL":"https:\/\/doi.org\/10.1007\/s11219-025-09729-0","relation":{},"ISSN":["0963-9314","1573-1367"],"issn-type":[{"value":"0963-9314","type":"print"},{"value":"1573-1367","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,29]]},"assertion":[{"value":"29 November 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 August 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 September 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing Interests"}}],"article-number":"32"}}