{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T08:15:23Z","timestamp":1773389723362,"version":"3.50.1"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"4","funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["#62372178 and #U21B2015"],"award-info":[{"award-number":["#62372178 and #U21B2015"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"\u201cDigital Silk Road\u201d Shanghai International Joint Lab of Trustworthy Intelligent Software","award":["22510750100"],"award-info":[{"award-number":["22510750100"]}]},{"name":"Shanghai Collaborative Innovation Center of Trusted Industry Internet Software","award":["IIS-1527668, CCF-1704883, IIS-1830549, CNS-2016656"],"award-info":[{"award-number":["IIS-1527668, CCF-1704883, IIS-1830549, CNS-2016656"]}]},{"name":"US DoD MURI","award":["N00014-20-1-2787"],"award-info":[{"award-number":["N00014-20-1-2787"]}]},{"DOI":"10.13039\/501100001459","name":"Ministry of Education, Singapore","doi-asserted-by":"crossref","award":["MOET32020-0004"],"award-info":[{"award-number":["MOET32020-0004"]}],"id":[{"id":"10.13039\/501100001459","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2026,4,30]]},"abstract":"\n We present an on-the-fly synthesis framework for Linear Temporal Logic over Finite Traces (\n LTL<\/jats:sans-serif>\n \n \\({}_{f}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n ) based on top-down deterministic automata construction. Existing approaches rely on constructing a complete Deterministic Finite Automaton (\n DFA<\/jats:sans-serif>\n ) corresponding to the\n LTL<\/jats:sans-serif>\n \n \\({}_{f}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n specification, a process with doubly exponential complexity relative to formula size in the worst case. In this case, the synthesis cannot be conducted until the entire\n DFA<\/jats:sans-serif>\n is constructed. This inefficiency is the main bottleneck of existing approaches. To address this challenge, we first present a method for converting\n LTL<\/jats:sans-serif>\n \n \\({}_{f}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n into Transition-Based\n DFA<\/jats:sans-serif>\n (\n TDFA<\/jats:sans-serif>\n ) by directly leveraging\n LTL<\/jats:sans-serif>\n \n \\({}_{f}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n semantics, incorporating intermediate results as direct components of the final automaton to enable parallelized synthesis and automata construction. We then explore the relationship between\n LTL<\/jats:sans-serif>\n \n \\({}_{f}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n synthesis and\n TDFA<\/jats:sans-serif>\n games and subsequently develop an algorithm for performing\n LTL<\/jats:sans-serif>\n \n \\({}_{f}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n synthesis via on-the-fly\n TDFA<\/jats:sans-serif>\n game solving. This algorithm traverses the state space in a global forward manner combined with a local backward method, along with detecting strongly connected components. Moreover, we introduce two optimization techniques\u2014model-guided synthesis and state entailment\u2014to enhance the practical efficiency of our approach. Experimental results demonstrate that our on-the-fly approach achieves the best performance on the tested benchmarks and effectively complements existing approaches.\n <\/jats:p>","DOI":"10.1145\/3749101","type":"journal-article","created":{"date-parts":[[2025,7,17]],"date-time":"2025-07-17T14:29:49Z","timestamp":1752762589000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["An On-the-Fly Synthesis Framework for LTL over Finite Traces"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3346-6918","authenticated-orcid":false,"given":"Shengping","family":"Xiao","sequence":"first","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-2236-2631","authenticated-orcid":false,"given":"Yongkang","family":"Li","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5922-8750","authenticated-orcid":false,"given":"Shufang","family":"Zhu","sequence":"additional","affiliation":[{"name":"University of Liverpool, Liverpool, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3545-1392","authenticated-orcid":false,"given":"Jun","family":"Sun","sequence":"additional","affiliation":[{"name":"Singapore Management University, Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9286-8285","authenticated-orcid":false,"given":"Jianwen","family":"Li","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9750-8334","authenticated-orcid":false,"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0661-5773","authenticated-orcid":false,"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[{"name":"Rice University, Houston, Texas, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,3,12]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"Artifact for This Article. 2024. Retrieved from https:\/\/drive.google.com\/file\/d\/1JwH-Szs-dJ5KeZqV8159SL4 gQSxL03VM\/view?usp=sharing"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018985923441"},{"key":"e_1_3_2_4_2","article-title":"Compositional safety LTL synthesis","author":"Bansal Suguman","year":"2022","unstructured":"Suguman Bansal, Giuseppe De Giacomo, Antonio Di Stasio, Yong Li, Moshe Y. Vardi, and Shufang Zhu. 2022. Compositional safety LTL synthesis. In Verified Software: Theories, Tools, and Experiments (VSTTE).","journal-title":"Verified Software: Theories, Tools, and Experiments (VSTTE)"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v36i9.21202"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i06.6528"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_27"},{"key":"e_1_3_2_8_2","doi-asserted-by":"crossref","unstructured":"Roderick Bloem Barbara Jobstmann Nir Piterman Amir Pnueli and Yaniv Saar. 2012. Synthesis of reactive(1) designs. Journal of Computer and System Sciences 78 3 (2012) 911\u2013938.","DOI":"10.1016\/j.jcss.2011.08.007"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_45"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1969-0280205-0"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3055399.3055409"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2019\/767"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_9"},{"key":"e_1_3_2_14_2","first-page":"23","volume-title":"the International Congress of Mathematicians","volume":"1962","author":"Church Alonzo","year":"1962","unstructured":"Alonzo Church. 1962. Logic, arithmetics, and automata. In the International Congress of Mathematicians, Vol. 1962. Institut Mittag-Leffler, 23\u201335."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1609\/icaps.v31i1.15954"},{"key":"e_1_3_2_18_2","first-page":"854","volume-title":"23rd International Joint Conference on Artificial Intelligence","author":"Giacomo Giuseppe De","year":"2013","unstructured":"Giuseppe De Giacomo and Moshe Y. Vardi. 2013. Linear temporal logic and linear dynamic logic on finite traces. In 23rd International Joint Conference on Artificial Intelligence. AAAI Press, 854\u2013860."},{"key":"e_1_3_2_19_2","first-page":"1558","volume-title":"24th International Conference on Artificial Intelligence","author":"Giacomo Giuseppe De","year":"2015","unstructured":"Giuseppe De Giacomo and Moshe Y. Vardi. 2015. Synthesis for LTL and LDL on finite traces. In 24th International Conference on Artificial Intelligence. AAAI Press, 1558\u20131564."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1988.21949"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1991.185392"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3417995"},{"key":"e_1_3_2_24_2","unstructured":"Marco Favorito. 2023. Forward LTLf synthesis: DPLL at work. arXiv:2302.13825. Retrieved from https:\/\/arxiv.org\/abs\/2302.13825"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_22"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-627-9-72"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139583923.007"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2022\/359"},{"key":"e_1_3_2_29_2","first-page":"533","volume-title":"26th European Conference on Artificial Intelligence (ECAI \u201923), Including 12th Conference on Prestigious Applications of Intelligent Systems (PAIS \u201923)","author":"De Giacomo Giuseppe","year":"2023","unstructured":"Giuseppe De Giacomo, Gianmarco Parretti, and Shufang Zhu. 2023. LTL \\({}_{f}\\) best-effort synthesis in nondeterministic planning domains. In 26th European Conference on Artificial Intelligence (ECAI \u201923), Including 12th Conference on Prestigious Applications of Intelligent Systems (PAIS \u201923), Vol. 372. Frontiers in Artificial Intelligence and Applications, IOS Press, 533\u2013540."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2017.8206426"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2019.8794170"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Swen Jacobs Guillermo Perez and Philipp Schlehuber-Caissier. 2023. Data Scripts and Results from SYNTCOMP 2023. DOI: 10.5281\/zenodo.8112518","DOI":"10.5281\/zenodo.8112518"},{"key":"e_1_3_2_33_2","unstructured":"Swen Jacobs Guillermo A. P\u00e9rez and Philipp Schlehuber-Caissier. 2023. The Reactive Synthesis Competition. Retrieved from http:\/\/www.syntcomp.org\/"},{"key":"e_1_3_2_34_2","volume-title":"MONA Version 1.4 User Manual","author":"Klarlund Nils","year":"2001","unstructured":"Nils Klarlund and Anders M\u00f8ller. 2001. MONA Version 1.4 User Manual. BRICS, Department of Computer Science, University of Aarhus. Notes Series NS-01-1. Retrieved from http:\/\/www.brics.dk\/mona\/"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.15"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33012946"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055040"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00071"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"e_1_3_2_40_2","volume-title":"7th Workshop on Synthesis (SYNT@CAV \u201918) (Electronic Proceedings in Theoretical Computer Science)","author":"Michaud Thibaud","year":"2018","unstructured":"Thibaud Michaud and Maximilien Colange. 2018. Reactive synthesis from LTL specification with spot. In 7th Workshop on Synthesis (SYNT@CAV \u201918) (Electronic Proceedings in Theoretical Computer Science)."},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_35"},{"key":"e_1_3_2_42_2","unstructured":"Nills J. Nllsson. 1971. Problem Solving Methods in Artificial Intelligence. McGraw-Hill."},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.5555\/646243.681607"},{"key":"e_1_3_2_45_2","first-page":"1","article-title":"Decidability of second order theories and automata on infinite trees","volume":"141","author":"Rabin Michael O.","year":"1969","unstructured":"Michael O. Rabin. 1969. Decidability of second order theories and automata on infinite trees. Transaction of the AMS 141 (1969), 1\u201335.","journal-title":"Transaction of the AMS"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC51365.2020.00008"},{"key":"e_1_3_2_47_2","first-page":"5599","volume-title":"28th International Joint Conference on Artificial Intelligence (IJCAI \u201919)","author":"Tabajara Lucas M.","year":"2019","unstructured":"Lucas M. Tabajara and Moshe Y. Vardi. 2019. Partitioning techniques in LTLf synthesis. In 28th International Joint Conference on Artificial Intelligence (IJCAI \u201919). AAAI Press, 5599\u20135606."},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59126-6_7"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v35i7.16809"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-50524-9_9"},{"key":"e_1_3_2_53_2","first-page":"3631","volume-title":"33rd International Joint Conference on Artificial Intelligence (IJCAI \u201924)","author":"Yu Pian","year":"2024","unstructured":"Pian Yu, Shufang Zhu, Giuseppe De Giacomo, Marta Kwiatkowska, and Moshe Y. Vardi. 2024. The trembling-hand problem for LTLf planning. In 33rd International Joint Conference on Artificial Intelligence (IJCAI \u201924). ijcai.org, 3631\u20133641."},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2017\/189"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3749101","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T05:28:49Z","timestamp":1773379729000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3749101"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,12]]},"references-count":53,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2026,4,30]]}},"alternative-id":["10.1145\/3749101"],"URL":"https:\/\/doi.org\/10.1145\/3749101","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,12]]},"assertion":[{"value":"2025-03-03","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-24","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-03-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}