{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:15Z","timestamp":1784793795741,"version":"3.55.0"},"publisher-location":"Cham","reference-count":70,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Syntactic obligations are a fragment of LTL formulas that translate\u00a0to deterministic weak\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\omega $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>\u03c9<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -automata (DWA). We show that syntactic obligations can be very efficiently converted to minimal DWA represented using multi-terminal binary decision diagrams (MTBDDs), and that synthesis of such specifications can be solved directly on the MTBDD representation on the fly. Our implementation in Spot shows substantial runtime improvements in translation\u00a0and synthesis.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_17","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:45Z","timestamp":1784791065000},"page":"322-339","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Fast Obligation Translation and\u00a0Synthesis"],"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-0001-9680-7658","authenticated-orcid":false,"given":"Giuseppe","family":"De Giacomo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3640-8481","authenticated-orcid":false,"given":"Marcin","family":"Jurdzinski","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-0002-0661-5773","authenticated-orcid":false,"given":"Moshe Y.","family":"Vardi","sequence":"additional","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"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"870","DOI":"10.1007\/978-3-030-81685-8_41","volume-title":"Computer Aided Verification","author":"G Amram","year":"2021","unstructured":"Amram, G., Bansal, S., Fried, D., Tabajara, L.M., Vardi, M.Y., Weiss, G.: Adapting behaviors via reactive synthesis. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 870\u2013893. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_41"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-21690-4_31","volume-title":"Computer Aided Verification","author":"T Babiak","year":"2015","unstructured":"Babiak, T., et al.: The Hanoi omega-automata format. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479\u2013486. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_31"},{"key":"17_CR3","doi-asserted-by":"publisher","unstructured":"Bansal, S., De\u00a0Giacomo, G., Di\u00a0Stasio, A., Li, Y., Vardi, M.Y., Zhu, S.: Compositional safety LTL synthesis. In: Lal, A., Tonetta, S. (eds.) Proceedings of the 14th International Conference on Verified Software, Theories, Tools and Experiments (VSTTE 2022), pp. 1\u201319. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-25803-9_1","DOI":"10.1007\/978-3-031-25803-9_1"},{"key":"17_CR4","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":"17_CR5","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":"17_CR6","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Technical report 11\/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011). https:\/\/fmv.jku.at\/aiger\/"},{"issue":"3","key":"17_CR7","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/J.JCSS.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012). https:\/\/doi.org\/10.1016\/J.JCSS.2011.08.007","journal-title":"J. Comput. Syst. Sci."},{"key":"17_CR8","doi-asserted-by":"publisher","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","DOI":"10.1109\/TC.1986.1676819"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-030-99527-0_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Casares","year":"2022","unstructured":"Casares, A., Duret-Lutz, A., Meyer, K.J., Renkin, F., Sickert, S.: Practical applications of the alternating cycle decomposition. In: TACAS 2022. LNCS, vol. 13244, pp. 99\u2013117. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_6"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-540-45138-9_26","volume-title":"Mathematical Foundations of Computer Science 2003","author":"I \u010cern\u00e1","year":"2003","unstructured":"\u010cern\u00e1, I., Pel\u00e1nek, R.: Relating hierarchy of temporal properties to model checking. In: Rovan, B., Vojt\u00e1\u0161, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 318\u2013327. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45138-9_26"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/3-540-55719-9_97","volume-title":"Automata, Languages and Programming","author":"E Chang","year":"1992","unstructured":"Chang, E., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 474\u2013486. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55719-9_97"},{"key":"17_CR12","unstructured":"Chatterjee, K.: Linear time algorithm for weak parity games. Technical Report UCB\/EECS-2006-153, Electrical Engineering and Computer Sciences, University of California at Berkeley (2008). https:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2006\/EECS-2006-153.html"},{"key":"17_CR13","doi-asserted-by":"publisher","unstructured":"Cicho\u0144, J., Czubak, A., Jasi\u0144ski, A.: Minimal B\u00fcchi automata for certain classes of LTL formulas. In: Proceedings of the Fourth International Conference on Dependability of Computer Systems (DepCoS 2009), pp. 17\u201324. IEEE Computer Society (2009). https:\/\/doi.org\/10.1109\/DepCoS-RELCOMEX.2009.31","DOI":"10.1109\/DepCoS-RELCOMEX.2009.31"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-48119-2_16","volume-title":"FM\u201999 \u2014 Formal Methods","author":"J-M Couvreur","year":"1999","unstructured":"Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253\u2013271. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48119-2_16"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-75596-8_17","volume-title":"Automated Technology for Verification and Analysis","author":"C Dax","year":"2007","unstructured":"Dax, C., Eisinger, J., Klaedtke, F.: Mechanizing the powerset construction for restricted classes of $$\\omega $$-automata. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 223\u2013236. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75596-8_17"},{"key":"17_CR16","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":"17_CR17","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. AAAI Press (2013). https:\/\/doi.org\/10.5555\/2540128.2540252","DOI":"10.5555\/2540128.2540252"},{"key":"17_CR18","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":"17_CR19","unstructured":"Dijkstra, E.W.: EWD 376: Finding the maximum strong components in a directed graph (1973). http:\/\/www.cs.utexas.edu\/users\/EWD\/ewd03xx\/EWD376.PDF"},{"key":"17_CR20","unstructured":"Dijkstra, E.W.: Finding the maximal strong components in a directed graph. In: A Discipline of Programming, chap.\u00a025, pp. 192\u2013200. Prentice-Hall (1976)"},{"key":"17_CR21","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A.: LTL translation improvements in Spot 1.0. Int. J. Crit. Comput.-Based Syst. 5(1\/2), 31\u201354 (2014). https:\/\/doi.org\/10.1504\/IJCCBS.2014.059594","DOI":"10.1504\/IJCCBS.2014.059594"},{"key":"17_CR22","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A.: Supporting material for \u201cFast Obligation Translation and Synthesis\u201d (2026). https:\/\/doi.org\/10.5281\/zenodo.19812382","DOI":"10.5281\/zenodo.19812382"},{"key":"17_CR23","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., De Giacomo, G., Jurdzinski, M., Piterman, N., Vardi, M.Y., Zhu, S.: Fast obligation translation and synthesis. arXiv (2026). https:\/\/doi.org\/10.48550\/arXiv.2605.12372, extended version of this article, inluding proofs and additional discussions in appendices","DOI":"10.48550\/arXiv.2605.12372"},{"key":"17_CR24","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\u201922). Lecture Notes in Computer Science, 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":"17_CR25","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Zhu, S., Piterman, N., De Giacomo, G., Vardi, M.Y.: Engineering an LTLf synthesis tool. In: Proceedings of the 29th International Conference on Implementation and Applications of Automata (CIAA 2025). Lecture Notes in Computer Science, vol. 15981, pp. 129\u2013147. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-032-02602-6_10","DOI":"10.1007\/978-3-032-02602-6_10"},{"key":"17_CR26","doi-asserted-by":"publisher","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Ardis, M. (ed.) Proceedings of the 2nd Workshop on Formal Methods in Software Practice (FMSP 1998), pp. 7\u201315. ACM Press (1998). https:\/\/doi.org\/10.1145\/298595.298598","DOI":"10.1145\/298595.298598"},{"key":"17_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":"17_CR28","doi-asserted-by":"publisher","unstructured":"Esparza, J., Rubio, R., Sickert, S.: Efficient normalization of linear temporal logic. J. ACM 71(2) (2024). https:\/\/doi.org\/10.1145\/3651152","DOI":"10.1145\/3651152"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-44618-4_13","volume-title":"CONCUR 2000 \u2014 Concurrency Theory","author":"K Etessami","year":"2000","unstructured":"Etessami, K., Holzmann, G.J.: Optimizing B\u00fcchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153\u2013168. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44618-4_13"},{"key":"17_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":"17_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":"17_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":"17_CR33","doi-asserted-by":"publisher","unstructured":"Gaiser, A., Schwoon, S.: Comparison of algorithms for checking emptiness on B\u00fcchi automata. In: Hlinen\u00fd, P., Maty\u00e1s, V., Vojnar, T. (eds.) Proceedings of Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS\u201909). OASICS, vol.\u00a013. Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik, Germany (2009). https:\/\/doi.org\/10.4230\/DROPS.MEMICS.2009.2349","DOI":"10.4230\/DROPS.MEMICS.2009.2349"},{"key":"17_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/11691617_4","volume-title":"Model Checking Software","author":"J Geldenhuys","year":"2006","unstructured":"Geldenhuys, J., Hansen, H.: Larger automata and less work for LTL model checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 53\u201370. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691617_4"},{"key":"17_CR35","doi-asserted-by":"publisher","unstructured":"Geldenhuys, J., Valmari, A.: More efficient on-the-fly LTL verification with Tarjan\u2019s algorithm. Theor. Comput. Sci. 345(1), 60\u201382 (2005). https:\/\/doi.org\/10.1016\/j.tcs.2005.07.004","DOI":"10.1016\/j.tcs.2005.07.004"},{"key":"17_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JG Henriksen","year":"1995","unstructured":"Henriksen, J.G., et al.: Mona: monadic second-order logic in practice. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89\u2013110. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60630-0_5"},{"key":"17_CR37","unstructured":"Hole\u010dek, J., Kratochv\u00edla, T., \u0158eh\u00e1k, V., \u0160afr\u00e1nek, D., \u0160ime\u010dek, P.: Verification results in Liberouter project. Technical Report 03, CESNET (2004). http:\/\/archiv.cesnet.cz\/doc\/techzpravy\/2004\/verificationresults\/"},{"key":"17_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":"17_CR39","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA version 1.4, user manual. Technical report, BRICS (2001). https:\/\/www.brics.dk\/mona\/mona14.pdf"},{"key":"17_CR40","doi-asserted-by":"publisher","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Prokop, M., Zarkhah, A.: SemML: enhancing automata-theoretic LTL synthesis with machine learning. In: Gurfinkel, A., Heule, M. (eds.) Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025), pp. 233\u2013253. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-90643-5_12","DOI":"10.1007\/978-3-031-90643-5_12"},{"key":"17_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-030-01090-4_34","volume-title":"Automated Technology for Verification and Analysis","author":"J K\u0159et\u00ednsk\u00fd","year":"2018","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: a library for $$\\omega $$-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 543\u2013550. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_34"},{"key":"17_CR42","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-642-20674-0_6","volume-title":"Model Checking and Artificial Intelligence","author":"O Kupferman","year":"2011","unstructured":"Kupferman, O., Rosenberg, A.: The blow-up in translating LTL to deterministic automata. In: van der Meyden, R., Smaus, J.-G. (eds.) MoChArt 2010. LNCS (LNAI), vol. 6572, pp. 85\u201394. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20674-0_6"},{"key":"17_CR43","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005), pp. 531\u2013542 (2005). https:\/\/doi.org\/10.1109\/SFCS.2005.66","DOI":"10.1109\/SFCS.2005.66"},{"key":"17_CR44","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312\u2013360 (2000). https:\/\/doi.org\/10.1145\/333979.333987","DOI":"10.1145\/333979.333987"},{"key":"17_CR45","doi-asserted-by":"publisher","unstructured":"Li, Y., Xiao, S., Zhu, S., Li, J., Pu, G.: A compositional framework for on-the-fly LTL$$_f$$ synthesis. In: Proceedings of the 28th European Conference on Artificial Intelligence (ECAI 2025), pp. 1711\u20131718. Frontiers in Artificial Intelligence and Applications (2025). https:\/\/doi.org\/10.3233\/FAIA250999","DOI":"10.3233\/FAIA250999"},{"key":"17_CR46","unstructured":"L\u00f6ding, C.: Methods for the transformation of $$\\omega $$-automata: complexity and connection to second order logic. Diploma thesis, Institute of Computer Science and Applied Mathematics Christian-Albrechts-University of Kiel (1998). https:\/\/www.lics.rwth-aachen.de\/global\/show_document.asp?id=aaaaaaaaabcqdty"},{"issue":"3","key":"17_CR47","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0020-0190(00)00183-6","volume":"79","author":"C L\u00f6ding","year":"2001","unstructured":"L\u00f6ding, C.: Efficient minimization of deterministic weak $$\\omega $$-automata. Inf. Process. Lett. 79(3), 105\u2013109 (2001). https:\/\/doi.org\/10.1016\/S0020-0190(00)00183-6","journal-title":"Inf. Process. Lett."},{"key":"17_CR48","unstructured":"Long, D.: BDD library. https:\/\/www.cs.cmu.edu\/~modelcheck\/bdd.html"},{"issue":"1\u20132","key":"17_CR49","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/S00236-019-00349-3","volume":"57","author":"M Luttenberger","year":"2020","unstructured":"Luttenberger, M., Meyer, P.J., Sickert, S.: Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica 57(1\u20132), 3\u201336 (2020). https:\/\/doi.org\/10.1007\/S00236-019-00349-3","journal-title":"Acta Informatica"},{"key":"17_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-030-31784-3_21","volume-title":"Automated Technology for Verification and Analysis","author":"J Major","year":"2019","unstructured":"Major, J., Blahoudek, F., Strej\u010dek, J., Sasar\u00e1kov\u00e1, M., Zbon\u010d\u00e1kov\u00e1, T.: ltl3tela: LTL to small deterministic or nondeterministic Emerson-lei automata. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 357\u2013365. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_21"},{"key":"17_CR51","doi-asserted-by":"publisher","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing (PODC 1990), pp. 377\u2013410. ACM, New York, NY, USA (1990). https:\/\/doi.org\/10.1145\/93385.93442","DOI":"10.1145\/93385.93442"},{"key":"17_CR52","doi-asserted-by":"publisher","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer (1992). https:\/\/doi.org\/10.1007\/978-1-4612-0931-7","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"17_CR53","doi-asserted-by":"publisher","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer (1995). https:\/\/doi.org\/10.1007\/978-1-4612-4222-2","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"17_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-13754-9_13","volume-title":"Time for Verification","author":"Z Manna","year":"2010","unstructured":"Manna, Z., Pnueli, A.: Temporal verification of reactive systems: response. In: Manna, Z., Peled, D.A. (eds.) Time for Verification. LNCS, vol. 6200, pp. 279\u2013361. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13754-9_13"},{"key":"17_CR55","doi-asserted-by":"publisher","unstructured":"Minato, S.I.: Representation of Multi-Valued Functions, pp. 39\u201347. Springer, Boston (1996). https:\/\/doi.org\/10.1007\/978-1-4613-1303-8_4","DOI":"10.1007\/978-1-4613-1303-8_4"},{"key":"17_CR56","doi-asserted-by":"crossref","unstructured":"Moore, E.F.: Gedanken-experiments on sequential machines. In: Automata Studies. Annals of Mathematical Studies, no. 34, pp. 129\u2013153. Princeton University Press (1956)","DOI":"10.1515\/9781400882618-006"},{"key":"17_CR57","doi-asserted-by":"publisher","unstructured":"M\u00fcller, D., Sickert, S.: LTL to deterministic Emerson-Lei automata. In: Proceedings of the 8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF\u201917). Electronic Proceedings in Theoretical Computer Science, vol.\u00a0256, pp. 180\u2013194. Open Publishing Association (2017). https:\/\/doi.org\/10.4204\/EPTCS.256.13","DOI":"10.4204\/EPTCS.256.13"},{"key":"17_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73370-6_17","volume-title":"Model Checking Software","author":"R Pel\u00e1nek","year":"2007","unstructured":"Pel\u00e1nek, R.: BEEM: benchmarks for explicit model checkers. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263\u2013267. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73370-6_17"},{"key":"17_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N Piterman","year":"2005","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364\u2013380. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11609773_24"},{"key":"17_CR60","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS 1977), pp. 46\u201357 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"17_CR61","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 (POPL 1989). Association for Computing Machinery (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"issue":"3\u20134","key":"17_CR62","doi-asserted-by":"publisher","first-page":"393","DOI":"10.3233\/FI-2012-744","volume":"119","author":"R Redziejowski","year":"2012","unstructured":"Redziejowski, R.: An improved construction of deterministic omega-automaton using derivatives. Fund. Inform. 119(3\u20134), 393\u2013406 (2012). https:\/\/doi.org\/10.3233\/FI-2012-744","journal-title":"Fund. Inform."},{"key":"17_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1007\/978-3-642-45221-5_44","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"E Renault","year":"2013","unstructured":"Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Three SCC-based emptiness checks for generalized B\u00fcchi automata. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 668\u2013682. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_44"},{"key":"17_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-030-59152-6_7","volume-title":"Automated Technology for Verification and Analysis","author":"F Renkin","year":"2020","unstructured":"Renkin, F., Duret-Lutz, A., Pommellet, A.: Practical \u201cparitizing\u2019\u2019 of Emerson-lei automata. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 127\u2013143. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_7"},{"key":"17_CR65","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":"17_CR66","doi-asserted-by":"publisher","unstructured":"Schewe, S.: Beyond hyper-minimisation\u2014minimising DBAs and DPAs is NP-complete. In: Lodaya, K., Mahajan, M. (eds.) Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics, vol.\u00a08, pp. 400\u2013411. Schloss Dagstuhl LZI, Dagstuhl, Germany (2010). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2010.400","DOI":"10.4230\/LIPIcs.FSTTCS.2010.400"},{"key":"17_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248\u2013263. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_21"},{"key":"17_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-642-16612-9_33","volume-title":"Runtime Verification","author":"D Tabakov","year":"2010","unstructured":"Tabakov, D., Vardi, M.Y.: Optimized temporal monitors for SystemC. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 436\u2013451. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_33"},{"key":"17_CR69","doi-asserted-by":"publisher","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite state programs. In: Proceedings of the 26th Annual Symposium on Foundations of Computer Science (SFCS 1985), pp. 327\u2013338. IEEE (1985). https:\/\/doi.org\/10.1109\/SFCS.1985.12","DOI":"10.1109\/SFCS.1985.12"},{"key":"17_CR70","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","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32519-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:48Z","timestamp":1784791068000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":70,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}