{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,14]],"date-time":"2026-10-14T22:48:22Z","timestamp":1792018102441,"version":"4.4.0"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032026019","type":"print"},{"value":"9783032026026","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:00:00Z","timestamp":1755907200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:00:00Z","timestamp":1755907200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-02602-6_10","type":"book-chapter","created":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T08:33:55Z","timestamp":1755851635000},"page":"129-147","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Engineering an\u00a0$$\\mathsf {LTL_f}$$ Synthesis Tool"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6623-2512","authenticated-orcid":false,"given":"Alexandre","family":"Duret-Lutz","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5922-8750","authenticated-orcid":false,"given":"Shufang","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8242-5357","authenticated-orcid":false,"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9680-7658","authenticated-orcid":false,"given":"Giuseppe","family":"De Giacomo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0661-5773","authenticated-orcid":false,"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,8,23]]},"reference":[{"key":"10_CR1","unstructured":"Andersen, H.R.: An introduction to binary decision diagrams. Lecture notes for Efficient Algorithms and Programs, Fall 1999 (1999). https:\/\/web.archive.org\/web\/20090530154634\/http:\/\/www.itu.dk:80\/people\/hra\/bdd-eap.pdf"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Antimirov, V.: Partial derivatives of regular expressions and finite automaton constructions. Theoret. Comput. Sci. 155(2), 291\u2013319 (1996). https:\/\/doi.org\/10.1016\/0304-3975(95)00182-4","DOI":"10.1016\/0304-3975(95)00182-4"},{"key":"10_CR3","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1018985923441","volume":"22","author":"F Bacchus","year":"1998","unstructured":"Bacchus, F., Kabanza, F.: Planning for temporally extended goals. Ann. Math. Artif. Intell. 22, 5\u201327 (1998). https:\/\/doi.org\/10.1023\/A:1018985923441","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1\u20132","key":"10_CR4","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/S0004-3702(99)00071-5","volume":"116","author":"F Bacchus","year":"2000","unstructured":"Bacchus, F., Kabanza, F.: Using temporal logics to express search control knowledge for planning. Artif. Intell. 116(1\u20132), 123\u2013191 (2000). https:\/\/doi.org\/10.1016\/S0004-3702(99)00071-5","journal-title":"Artif. Intell."},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Bahar, R.I., et al.: Algebraic decision diagrams and their applications. In: Proceedings of 1993 International Conference on Computer Aided Design (ICCAD 1993), pp. 188\u2013191. IEEE Computer Society Press (1993). https:\/\/doi.org\/10.1109\/ICCAD.1993.580054","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"10_CR6","unstructured":"Baier, J.A., Fritz, C., McIlraith, S.A.: Exploiting procedural domain control knowledge in state-of-the-art planners. In: Proceedings of the International Conference on Automated Planning and Scheduling (ICAPS 2007), pp. 26\u201333. AAAI (2007). https:\/\/aaai.org\/papers\/icaps-07-004"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Baier, J.A., McIlraith, S.A.: Planning with first-order temporally extended goals using heuristic search. In: Proceedings of the 21st International Conference on Artificial intelligence (AAAI 2006), pp. 788\u2013795. AAAI Press (2006).https:\/\/doi.org\/10.5555\/1597538.1597664","DOI":"10.5555\/1597538.1597664"},{"key":"10_CR8","doi-asserted-by":"publisher","unstructured":"Bansal, S., Li, Y., Tabajara, L.M., Vardi, M.Y.: Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications. In: Proceedings of the 34th national conference on Artificial intelligence (AAAI 2020), pp. 9766\u20139774. AAAI Press (2020). https:\/\/doi.org\/10.1609\/AAAI.V34I06.6528","DOI":"10.1609\/AAAI.V34I06.6528"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transfer 21, 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","DOI":"10.1007\/s10009-017-0469-y"},{"key":"10_CR10","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. Rep.\u00a011\/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011). https:\/\/fmv.jku.at\/aiger\/"},{"issue":"8","key":"10_CR11","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986). https:\/\/doi.org\/10.1109\/TC.1986.1676819","journal-title":"IEEE Trans. Comput."},{"issue":"3","key":"10_CR12","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992). https:\/\/doi.org\/10.1145\/136035.136043","journal-title":"ACM Comput. Surv."},{"issue":"4","key":"10_CR13","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"JA Brzozowski","year":"1964","unstructured":"Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481\u2013494 (1964). https:\/\/doi.org\/10.1145\/321239.321249","journal-title":"J. ACM"},{"key":"10_CR14","doi-asserted-by":"publisher","unstructured":"Calvanese, D., De Giacomo, G., Vardi, M.Y.: Reasoning about actions and planning in LTL action theories. In: Proceedings of the Eights International Conference on Principles of Knowledge Representation and Reasoning (KR 2002), pp. 593\u2013602. Morgan Kaufmann (2002). https:\/\/doi.org\/10.5555\/3087093.3087142","DOI":"10.5555\/3087093.3087142"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Camacho, A., Bienvenu, M., McIlraith, S.A.: Towards a unified view of AI planning and reactive synthesis. In: Proceedings of the 29th International Conference on Automated Planning and Scheduling (ICAPS 2019), pp. 58\u201367. AAAI Press (2019). https:\/\/doi.org\/10.1609\/icaps.v29i1.3460","DOI":"10.1609\/icaps.v29i1.3460"},{"issue":"1\u20132","key":"10_CR16","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/S0004-3702(02)00374-0","volume":"147","author":"A Cimatti","year":"2003","unstructured":"Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: Weak, strong, and strong cyclic planning via symbolic model checking. Artif. Intell. 147(1\u20132), 35\u201384 (2003). https:\/\/doi.org\/10.1016\/S0004-3702(02)00374-0","journal-title":"Artif. Intell."},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"Darwiche, A.: SDD: A new canonical representation of propositional knowledge bases. In: Proceedings of the 22nd International Joint Conference on Artificial Intelligence, pp. 819\u2013826. AAAI Press (2011). https:\/\/doi.org\/10.5591\/978-1-57735-516-8\/IJCAI11-143","DOI":"10.5591\/978-1-57735-516-8\/IJCAI11-143"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"De Giacomo, G., Favorito, M.: Compositional approach to translate LTL$$_{f}$$\/LDL$$_{f}$$ into deterministic finite automata. In: Proceedings of the 31st International Conference on Automated Planning and Scheduling (ICAPS 2021), pp. 122\u2013130 (2021). https:\/\/doi.org\/10.1609\/icaps.v31i1.15954","DOI":"10.1609\/icaps.v31i1.15954"},{"key":"10_CR19","doi-asserted-by":"publisher","unstructured":"De Giacomo, G., Favorito, M.: Compositional approach to translate LTLf\/LDLf into deterministic finite automata. In: Biundo, S., Do, M., Goldman, R., Katz, M., Yang, Q., Zhuo, H.H. (eds.) Proceedings of the 31\u2019st International Conference on Automated Planning and Scheduling (ICAPS 2021), pp. 122\u2013130. AAAI Press (2021) https:\/\/doi.org\/10.1609\/icaps.v31i1.15954","DOI":"10.1609\/icaps.v31i1.15954"},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"De\u00a0Giacomo, G., Favorito, M., Li, J., Vardi, M.Y., Xiao, S., Zhu, S.: LTLf synthesis as AND-OR graph search: knowledge compilation at work. In: Raedt, L.D. (ed.) Proceedings of the 31st International Joint Conference on Artificial Intelligence (IJCAI 2022), pp. 2591\u20132598. International Joint Conferences on Artificial Intelligence Organization (2022). https:\/\/doi.org\/10.24963\/ijcai.2022\/359","DOI":"10.24963\/ijcai.2022\/359"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"De Giacomo, G., Rubin, S.: Automata-theoretic foundations of fond planning for LTL$$_{f}$$\/LDL$$_{f}$$ goals. In: Proceedings of the 27th International Joint Conference on Artificial Intelligence (IJCAI 2018), pp. 4729\u20134735 (2018). https:\/\/doi.org\/10.24963\/ijcai.2018\/657","DOI":"10.24963\/ijcai.2018\/657"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"De\u00a0Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI 2013), pp. 854\u2013860. IJCAI 2013, AAAI Press (2013). https:\/\/doi.org\/10.5555\/2540128.2540252","DOI":"10.5555\/2540128.2540252"},{"key":"10_CR23","doi-asserted-by":"publisher","unstructured":"De\u00a0Giacomo, G., Vardi, M.Y.: Synthesis for LTL and LDL on finite traces. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015), pp. 1558\u20131564. AAAI Press (2015). https:\/\/doi.org\/10.5555\/2832415.2832466","DOI":"10.5555\/2832415.2832466"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A.: Supporting material for \u201cEngineering an LTLf Synthetizer Tool\u201d (2025). https:\/\/doi.org\/10.5281\/zenodo.15752968","DOI":"10.5281\/zenodo.15752968"},{"key":"10_CR25","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From Spot 2.0 to Spot 2.10: What\u2019s new? In: Proceedings of the 34th International Conference on Computer Aided Verification (CAV 2022). LNCS, vol. 13372, pp. 174\u2013187. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"10_CR26","doi-asserted-by":"publisher","unstructured":"Ehlers, R., Lafortune, S., Tripakis, S., Vardi, M.Y.: Supervisory control and reactive synthesis: a comparative introduction. Discrete Event Dynamic Systems 27(2), 209\u2013260 (2017). https:\/\/doi.org\/10.1007\/s10626-015-0223-0","DOI":"10.1007\/s10626-015-0223-0"},{"key":"10_CR27","doi-asserted-by":"publisher","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J., Sickert, S.: One theorem to rule them all: a unified translation of LTL into $$\\omega $$-automata. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2018), pp. 384\u2013393. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209161","DOI":"10.1145\/3209108.3209161"},{"key":"10_CR28","unstructured":"Favorito, M.: Forward LTLf synthesis: DPLL at work. In: Benedictis, R.D., et al. (eds.) Proceedings of the 30th Workshop on Experimental evaluation of algorithms for solving problems with combinatorial explosion (RCRA 2023). CEUR Workshop Proceedings, vol.\u00a03585 (2023). https:\/\/ceur-ws.org\/Vol-3585\/paper7_RCRA4.pdf"},{"key":"10_CR29","doi-asserted-by":"publisher","unstructured":"Favorito, M., Zhu, S.: LydiaSyft: a compositional symbolic synthesis framework for LTLf specifications. In: Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025). LNCS, vol. 15696, pp. 295\u2013302. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-90643-5_15","DOI":"10.1007\/978-3-031-90643-5_15"},{"key":"10_CR30","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B.: Synthesis of reactive systems. In: Javier\u00a0Esparza, Orna\u00a0Grumberg, S.S. (ed.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series \u2014 D: Information and Communication Security, vol.\u00a045, pp. 72\u201398. IOS Press (2016). https:\/\/doi.org\/10.3233\/978-1-61499-627-9-72","DOI":"10.3233\/978-1-61499-627-9-72"},{"key":"10_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-030-76384-8_8","volume-title":"NASA Formal Methods","author":"B Finkbeiner","year":"2021","unstructured":"Finkbeiner, B., Geier, G., Passing, N.: Specification decomposition for reactive synthesis. In: Dutle, A., Moscato, M.M., Titolo, L., Mu\u00f1oz, C.A., Perez, I. (eds.) NFM 2021. LNCS, vol. 12673, pp. 113\u2013130. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_8"},{"issue":"2\/3","key":"10_CR32","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1023\/A:1008647823331","volume":"10","author":"M Fujita","year":"1997","unstructured":"Fujita, M., McGeer, P.C., Yang, J.C.: Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Formal Methods Syst. Des. 10(2\/3), 149\u2013169 (1997). https:\/\/doi.org\/10.1023\/A:1008647823331","journal-title":"Formal Methods Syst. Des."},{"key":"10_CR33","doi-asserted-by":"publisher","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of programming languages (POPL 1980), pp. 163\u2013173. Association for Computing Machinery (1980). https:\/\/doi.org\/10.1145\/567446.5674","DOI":"10.1145\/567446.5674"},{"issue":"5\u20136","key":"10_CR34","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1016\/j.artint.2008.10.012","volume":"173","author":"A Gerevini","year":"2009","unstructured":"Gerevini, A., Haslum, P., Long, D., Saetti, A., Dimopoulos, Y.: Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners. Artif. Intell. 173(5\u20136), 619\u2013668 (2009). https:\/\/doi.org\/10.1016\/j.artint.2008.10.012","journal-title":"Artif. Intell."},{"key":"10_CR35","doi-asserted-by":"publisher","unstructured":"Gr\u00e4del, E.: Finite model theory and descriptive complexity. In: Finite Model Theory and Its Applications, chap.\u00a03, pp. 125\u2013230. Texts in Theoretical Computer Science an EATCS Series, Springer Berlin Heidelberg, Heidelberg (2007). https:\/\/doi.org\/10.1007\/3-540-68804-8_3","DOI":"10.1007\/3-540-68804-8_3"},{"key":"10_CR36","doi-asserted-by":"publisher","unstructured":"Henriksen, J.G., t al.: Mona: monadic second-order logic in practice. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) First International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 1995), pp. 89\u2013110. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60630-0_5","DOI":"10.1007\/3-540-60630-0_5"},{"key":"10_CR37","doi-asserted-by":"publisher","unstructured":"Jacobs, S., Perez, G.A., Schlehuber-Caissier, P.: The temporal logic synthesis format TLSF v1.2. arXiV (2023). https:\/\/doi.org\/10.48550\/arXiv.2303.03839","DOI":"10.48550\/arXiv.2303.03839"},{"key":"10_CR38","doi-asserted-by":"publisher","unstructured":"Jacobs, S., et al.: The reactive synthesis competition (SYNTCOMP): 2018\u20132021. arXiV (2022). https:\/\/doi.org\/10.48550\/ARXIV.2206.00251","DOI":"10.48550\/ARXIV.2206.00251"},{"key":"10_CR39","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA version 1.4, user manual. Tech. rep., BRICS (2001). https:\/\/www.brics.dk\/mona\/mona14.pdf"},{"key":"10_CR40","unstructured":"Lind-Nielsen, J.: BuDDy: a binary decision diagram package. User\u2019s manual (1999). https:\/\/web.archive.org\/web\/20040402015529\/, http:\/\/www.itu.dk\/research\/buddy\/"},{"key":"10_CR41","doi-asserted-by":"publisher","unstructured":"Liu, X., Smolka, S.A.: Simple linear-time algorithms for minimal fixed points. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP 1998), pp. 53\u201366. Springer Berlin Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055035","DOI":"10.1007\/BFb0055035"},{"key":"10_CR42","unstructured":"Long, D.: BDD library. source archive. https:\/\/www.cs.cmu.edu\/~modelcheck\/bdd.html"},{"key":"10_CR43","doi-asserted-by":"publisher","unstructured":"Minato, S.: Representation of Multi-Valued Functions, pp. 39\u201347. Springer US, Boston, MA (1996). https:\/\/doi.org\/10.1007\/978-1-4613-1303-8_4","DOI":"10.1007\/978-1-4613-1303-8_4"},{"key":"10_CR44","doi-asserted-by":"publisher","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Proceedings of the 7th international conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2006). LNCS, vol.\u00a03855, pp. 364\u2013380. Springer (2006). https:\/\/doi.org\/10.1007\/11609773_24","DOI":"10.1007\/11609773_24"},{"key":"10_CR45","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL1989). Association for Computing Machinery (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"10_CR46","doi-asserted-by":"publisher","unstructured":"Renkin, F., Schlehuber-Caissier, P., Duret-Lutz, A., Pommellet, A.: Effective reductions of mealy machines. In: Proceedings of the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2022). LNCS, vol. 13273, pp. 170\u2013187. Springer (2022) https:\/\/doi.org\/10.1007\/978-3-031-08679-3_8","DOI":"10.1007\/978-3-031-08679-3_8"},{"key":"10_CR47","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-022-00407-6","author":"F Renkin","year":"2023","unstructured":"Renkin, F., Schlehuber-Caissier, P., Duret-Lutz, A., Pommellet, A.: Dissecting ltlsynt. Formal Methods Syst. Des. (2023). https:\/\/doi.org\/10.1007\/s10703-022-00407-6","journal-title":"Formal Methods Syst. Des."},{"key":"10_CR48","unstructured":"Sickert, S., Meyer, P.: Modernizing strix (2021). https:\/\/www7.in.tum.de\/~sickert\/publications\/MeyerS21.pdf"},{"key":"10_CR49","unstructured":"Somenzi, F.: CUDD: CU decision diagram package release 3.0.0 (2015). https:\/\/web.archive.org\/web\/20171208230728\/, http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/cudd.pdf"},{"key":"10_CR50","doi-asserted-by":"publisher","unstructured":"Xiao, S., Li, J., Zhu, S., Shi, Y., Pu, G., Vardi, M.: On-the-fly synthesis for LTL over finite traces. In: Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI\u201921, Technical Track 7), pp. 6530\u20136537 (2021). https:\/\/doi.org\/10.1609\/aaai.v35i7.16809","DOI":"10.1609\/aaai.v35i7.16809"},{"key":"10_CR51","doi-asserted-by":"publisher","unstructured":"Xiao, S., et al.: Model-guided synthesis for LTL over finite traces. In: Proceedings of the 25th International Conference on Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 14499, pp. 186\u2013207. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-50524-9_9","DOI":"10.1007\/978-3-031-50524-9_9"},{"key":"10_CR52","doi-asserted-by":"publisher","unstructured":"Zhu, S., De Giacomo, G.: Synthesis of maximally permissive strategies for LTLf specifications. In: Raedt, L.D. (ed.) Proceedings of the 31st International Joint Conference on Artificial Intelligence (IJCAI 2022), pp. 2783\u20132789. ijcai.org (2022). https:\/\/doi.org\/10.24963\/IJCAI.2022\/386","DOI":"10.24963\/IJCAI.2022\/386"},{"key":"10_CR53","doi-asserted-by":"publisher","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: Symbolic LTLf synthesis. In: Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI 2017), pp. 1362\u20131369 (2017). https:\/\/doi.org\/10.24963\/ijcai.2017\/189","DOI":"10.24963\/ijcai.2017\/189"}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Automata"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-02602-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,23]],"date-time":"2026-05-23T03:24:52Z","timestamp":1779506692000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-02602-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,23]]},"ISBN":["9783032026019","9783032026026"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-02602-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,23]]},"assertion":[{"value":"23 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CIAA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Implementation and Application of Automata","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Palermo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wia2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ciaa2025.unipa.it","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}