{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T22:20:17Z","timestamp":1757629217228,"version":"3.44.0"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T00:00:00Z","timestamp":1749600000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T00:00:00Z","timestamp":1749600000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key Research and Development Program of China","doi-asserted-by":"publisher","award":["2022YFB4501704"],"award-info":[{"award-number":["2022YFB4501704"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62302306"],"award-info":[{"award-number":["62302306"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2025,11]]},"DOI":"10.1007\/s10515-025-00511-x","type":"journal-article","created":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T22:33:36Z","timestamp":1749594816000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On-the-fly unfolding with optimal exploration for linear temporal logic model checking of concurrent software and systems"],"prefix":"10.1007","volume":"32","author":[{"given":"Shuo","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Li\u2019ao","family":"Zheng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ru","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhijun","family":"Ding","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,6,11]]},"reference":[{"key":"511_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P., Aronis, S., Jonsson, B., et\u00a0al.: Optimal dynamic partial order reduction. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Association for Computing Machinery, POPL \u201914, pp. 373\u2013384 (2014). https:\/\/doi.org\/10.1145\/2535838.2535845","DOI":"10.1145\/2535838.2535845"},{"key":"511_CR2","doi-asserted-by":"publisher","unstructured":"Barnat, J., Brim, L., Havel, V., et\u00a0al.: DiVinE 3.0\u2014an explicit-state model checker for multithreaded C & C++ Programs. In: Computer Aided Verification, pp. 863\u2013868. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_60","DOI":"10.1007\/978-3-642-39799-8_60"},{"issue":"1","key":"511_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10703-020-00350-4","volume":"57","author":"C Coti","year":"2021","unstructured":"Coti, C., Petrucci, L., Rodr\u00edguez, C., et al.: Quasi-optimal partial order reduction. Form. Methods Syst. Des. 57(1), 3\u201333 (2021). https:\/\/doi.org\/10.1007\/s10703-020-00350-4","journal-title":"Form. Methods Syst. Des."},{"key":"511_CR4","doi-asserted-by":"publisher","unstructured":"Dietsch, D., Heizmann, M., Langenfeld, V., et\u00a0al.: Fairness modulo theory: a new approach to LTL software model checking. In: Computer Aided Verification, pp. 49\u201366. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_4","DOI":"10.1007\/978-3-319-21690-4_4"},{"key":"511_CR5","doi-asserted-by":"publisher","unstructured":"Dietsch, D., Heizmann, M., Klumpp, D., et\u00a0al.: Verification of concurrent programs using petri net unfoldings. In: Verification, Model Checking, and Abstract Interpretation, pp. 174\u2013195. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_9","DOI":"10.1007\/978-3-030-67067-2_9"},{"key":"511_CR6","doi-asserted-by":"publisher","unstructured":"Ding, Z., He, C., Li, S.: EnPAC: petri net model checking for linear temporal logic. In: 2023 IEEE International Conference on Networking, Sensing and Control, pp. 1\u20136 (2023). https:\/\/doi.org\/10.1109\/ICNSC58704.2023.10318998","DOI":"10.1109\/ICNSC58704.2023.10318998"},{"key":"511_CR7","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2024.112221","volume":"219","author":"Z Ding","year":"2025","unstructured":"Ding, Z., Li, S., Chen, C., et al.: Program dependence net and on-demand slicing for property verification of concurrent system and software. J. Syst. Softw. 219, 112221 (2025). https:\/\/doi.org\/10.1016\/j.jss.2024.112221","journal-title":"J. Syst. Softw."},{"key":"511_CR8","doi-asserted-by":"publisher","unstructured":"Esparza, J., Heljanko, K.: Implementing LTL model checking with net unfoldings. In: Model Checking Software, pp. 37\u201356. Springer, Berlin (2001). https:\/\/doi.org\/10.1007\/3-540-45139-0_4","DOI":"10.1007\/3-540-45139-0_4"},{"issue":"3","key":"511_CR9","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1023\/A:1014746130920","volume":"20","author":"J Esparza","year":"2002","unstructured":"Esparza, J., R\u00f6mer, S., Vogler, W.: An improvement of McMillan\u2019s unfolding algorithm. Form. Methods Syst. Des. 20(3), 285\u2013310 (2002). https:\/\/doi.org\/10.1023\/A:1014746130920","journal-title":"Form. Methods Syst. Des."},{"issue":"1","key":"511_CR10","doi-asserted-by":"publisher","first-page":"195","DOI":"10.31577\/cai_2021_1_195","volume":"40","author":"C He","year":"2021","unstructured":"He, C., Ding, Z.: More efficient on-the-fly verification methods of colored Petri nets. Comput. Inform. 40(1), 195\u2013215 (2021). https:\/\/doi.org\/10.31577\/cai_2021_1_195","journal-title":"Comput. Inform."},{"issue":"4","key":"511_CR11","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1109\/TSE.2002.995426","volume":"28","author":"G Holzmann","year":"2002","unstructured":"Holzmann, G., Smith, M.: An automated verification method for distributed systems software based on model extraction. IEEE Trans. Softw. Eng. 28(4), 364\u2013377 (2002). https:\/\/doi.org\/10.1109\/TSE.2002.995426","journal-title":"IEEE Trans. Softw. Eng."},{"key":"511_CR12","doi-asserted-by":"publisher","unstructured":"K\u00e4hk\u00f6nen, K., Heljanko, K.: Lightweight state capturing for automated testing of multithreaded programs. In: Tests and Proofs, pp. 187\u2013203. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-09099-3_15","DOI":"10.1007\/978-3-319-09099-3_15"},{"key":"511_CR13","doi-asserted-by":"publisher","DOI":"10.1145\/2810000","author":"K K\u00e4hk\u00f6nen","year":"2017","unstructured":"K\u00e4hk\u00f6nen, K., Heljanko, K.: Testing programs with contextual unfoldings. ACM Trans. Embed. Comput. Syst. (2017). https:\/\/doi.org\/10.1145\/2810000","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"511_CR14","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10515-014-0150-6","volume":"22","author":"K K\u00e4hk\u00f6nen","year":"2015","unstructured":"K\u00e4hk\u00f6nen, K., Saarikivi, O., Heljanko, K.: Unfolding based automated testing of multithreaded programs. Autom. Softw. Eng. 22, 475\u2013515 (2015). https:\/\/doi.org\/10.1007\/s10515-014-0150-6","journal-title":"Autom. Softw. Eng."},{"key":"511_CR15","doi-asserted-by":"publisher","unstructured":"Kant, G., Laarman, A., Meijer, J., et\u00a0al.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 692\u2013707. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_61","DOI":"10.1007\/978-3-662-46681-0_61"},{"issue":"6","key":"511_CR16","doi-asserted-by":"publisher","DOI":"10.1002\/smr.2626","volume":"36","author":"S Li","year":"2024","unstructured":"Li, S., Chen, C., Huang, Z., et al.: Change-aware model checking for evolving concurrent programs based on Program Dependence Net. J. Softw. Evol. Process 36(6), e2626 (2024a). https:\/\/doi.org\/10.1002\/smr.2626","journal-title":"J. Softw. Evol. Process"},{"issue":"5","key":"511_CR17","doi-asserted-by":"publisher","first-page":"1161","DOI":"10.31577\/cai_2024_5_1161","volume":"43","author":"S Li","year":"2024","unstructured":"Li, S., Ding, Z., Pan, M.: Formal modelling of Program Dependence Net for software model checking. Comput. Inform. 43(5), 1161\u20131184 (2024b). https:\/\/doi.org\/10.31577\/cai_2024_5_1161","journal-title":"Comput. Inform."},{"key":"511_CR18","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: Computer Aided Verification, pp. 164\u2013177. Springer, Berlin (1993). https:\/\/doi.org\/10.1007\/3-540-56496-9_14","DOI":"10.1007\/3-540-56496-9_14"},{"key":"511_CR19","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez, C., Schwoon, S.: An improved construction of petri net unfoldings. In: French Singaporean Workshop on Formal Methods and Applications (2013). https:\/\/doi.org\/10.4230\/OASIcs.FSFMA.2013.47","DOI":"10.4230\/OASIcs.FSFMA.2013.47"},{"key":"511_CR20","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez, C., Sousa, M., Sharma, S., et\u00a0al.: Unfolding-based partial order reduction. In: 26th International Conference on Concurrency Theory, Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a042, pp. 456\u2013469. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik (2015). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2015.456","DOI":"10.4230\/LIPIcs.CONCUR.2015.456"},{"key":"511_CR21","doi-asserted-by":"publisher","DOI":"10.1145\/3012281","author":"O Saarikivi","year":"2017","unstructured":"Saarikivi, O., Ponce-De-Le\u00f3n, H., K\u00e4hk\u00f6nen, K., et al.: Minimizing test suites with unfoldings of multithreaded programs. ACM Trans. Embed. Comput. Syst. (2017). https:\/\/doi.org\/10.1145\/3012281","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"511_CR22","doi-asserted-by":"publisher","unstructured":"Schemmel, D., B\u00fcning, J., Rodr\u00edguez, C., et\u00a0al.: Symbolic partial-order execution for testing multi-threaded programs. In: Computer Aided Verification, pp. 376\u2013400 (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_18","DOI":"10.1007\/978-3-030-53288-8_18"},{"key":"511_CR23","doi-asserted-by":"publisher","unstructured":"Schr\u00f6ter, C., Khomenko, V.: Parallel LTL-X model checking of high-level Petri nets based on unfoldings. In: Computer Aided Verification, pp. 109\u2013121. Springer, Berlin (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_9","DOI":"10.1007\/978-3-540-27813-9_9"},{"key":"511_CR24","unstructured":"SV-COMP: software verification competition (2023). https:\/\/sv-comp.sosy-lab.org\/2023\/"},{"key":"511_CR25","doi-asserted-by":"publisher","unstructured":"Wallner, F.: Model checking LTL using net unforldings. In: Computer Aided Verification, pp. 207\u2013218. Springer, Berlin (1998). https:\/\/doi.org\/10.1007\/BFb0028746","DOI":"10.1007\/BFb0028746"},{"issue":"3","key":"511_CR26","doi-asserted-by":"publisher","first-page":"3047","DOI":"10.1109\/TII.2022.3181669","volume":"19","author":"D Xiang","year":"2023","unstructured":"Xiang, D., Lin, S., Wang, X., et al.: Checking missing-data errors in cyber-physical systems based on the merged process of Petri nets. IEEE Trans. Ind. Inf. 19(3), 3047\u20133056 (2023). https:\/\/doi.org\/10.1109\/TII.2022.3181669","journal-title":"IEEE Trans. Ind. Inf."}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-025-00511-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10515-025-00511-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-025-00511-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T13:58:01Z","timestamp":1757512681000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10515-025-00511-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,11]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,11]]}},"alternative-id":["511"],"URL":"https:\/\/doi.org\/10.1007\/s10515-025-00511-x","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"type":"print","value":"0928-8910"},{"type":"electronic","value":"1573-7535"}],"subject":[],"published":{"date-parts":[[2025,6,11]]},"assertion":[{"value":"23 June 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 March 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 June 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 that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"Not applicable.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethics approval and consent to participate"}}],"article-number":"60"}}