{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:34Z","timestamp":1784793814924,"version":"3.55.0"},"publisher-location":"Cham","reference-count":29,"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                    Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. These systems are typically represented using either Mealy machines or AIGER circuits. We present the second version of\n                    <jats:sc>SemML<\/jats:sc>\n                    , which outperforms all state-of-the-art tools for finding either solution. Aside from implementing the classical automata-theoretic approach, our tool utilizes partial exploration and machine-learning guidance for obtaining solutions efficiently, and numerous heuristics and improvements of classic algorithms for extracting small representations of these solutions. We evaluate our tool against the existing state-of-the-art tools (in particular\n                    <jats:sc>Strix<\/jats:sc>\n                    ,\n                    <jats:sc>LtlSynt<\/jats:sc>\n                    , and the previous version of\n                    <jats:sc>SemML<\/jats:sc>\n                    ) on the dataset of the synthesis competition SYNTCOMP. We show that we solve significantly more instances and do so much faster than other tools, while maintaining state-of-the-art solution quality.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_16","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:57Z","timestamp":1784791077000},"page":"308-321","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["SemML 2.0: Synthesizing Controllers for\u00a0LTL"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8122-2881","authenticated-orcid":false,"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1712-2165","authenticated-orcid":false,"given":"Tobias","family":"Meggendorfer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-6512-8693","authenticated-orcid":false,"given":"Maximilian","family":"Prokop","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","unstructured":"Abel, A., Reineke, J.: Memin: sat-based exact minimization of incompletely specified mealy machines. In: Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design, ICCAD 2015, Austin, TX, USA, 2\u20136 November 2015, pp. 94\u2013101 (2015). https:\/\/doi.org\/10.1109\/ICCAD.2015.7372555","DOI":"10.1109\/ICCAD.2015.7372555"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Azzopardi, S., Stefano, L.D., Piterman, N.: sweap: reactive synthesis for infinite-state integer problems. In: CAV (2026)","DOI":"10.1007\/978-3-031-98685-7_13"},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Azzopardi, S., Stefano, L.D., Piterman, N., Schneider, G.: Full LTL synthesis over infinite-state arenas. In: Piskac, R., Rakamaric, Z. (eds.) Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, 23\u201325 July 2025, Proceedings, Part IV. Lecture Notes in Computer Science, vol. 15934, pp. 274\u2013297. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98685-7_13","DOI":"10.1007\/978-3-031-98685-7_13"},{"key":"16_CR4","unstructured":"Biere, A.: The AIGER And-Inverter Graph (AIG) format version 20071012. Technical report 07\/1, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2007)"},{"key":"16_CR5","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL, Gimsatul, IsaSAT and Kissat entering the SAT competition 2024. In: Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2024 \u2013 Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science Report Series B, vol. B-2024-1, pp. 8\u201310. University of Helsinki (2024)"},{"issue":"8","key":"16_CR6","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."},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"Cosler, M., Hahn, C., Omar, A., Schmitt, F.: Neurosynt: a neuro-symbolic portfolio solver for reactive synthesis. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III. Lecture Notes in Computer Science, vol. 14572, pp. 45\u201367. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_3","DOI":"10.1007\/978-3-031-57256-2_3"},{"key":"16_CR8","doi-asserted-by":"publisher","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Sickert, S.: A unified translation of linear temporal logic to $$\\omega $$-automata. J. ACM 67(6), 33:1\u201333:61 (2020). https:\/\/doi.org\/10.1145\/3417995","DOI":"10.1145\/3417995"},{"key":"16_CR9","doi-asserted-by":"publisher","unstructured":"Fan, L., Wu, C.: FPGA technology mapping with adaptive gate decomposition. In: Ienne, P., Zhang, Z. (eds.) Proceedings of the 2023 ACM\/SIGDA International Symposium on Field Programmable Gate Arrays, FPGA 2023, Monterey, CA, USA, 12\u201314 February 2023, pp. 135\u2013140. ACM (2023). https:\/\/doi.org\/10.1145\/3543622.3573048","DOI":"10.1145\/3543622.3573048"},{"issue":"3","key":"16_CR10","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0016-0032(54)90574-8","volume":"257","author":"D Huffman","year":"1954","unstructured":"Huffman, D.: The synthesis of sequential switching circuits. J. Franklin Inst. 257(3), 161\u2013190 (1954). https:\/\/doi.org\/10.1016\/0016-0032(54)90574-8","journal-title":"J. Franklin Inst."},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Jacobs, S., Klein, F., Schirmer, S.: A high-level LTL synthesis format: TLSF v1.1. In: Piskac, R., Dimitrova, R. (eds.) Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, 17\u201318 July 2016. EPTCS, vol.\u00a0229, pp. 112\u2013132 (2016). https:\/\/doi.org\/10.4204\/EPTCS.229.10","DOI":"10.4204\/EPTCS.229.10"},{"issue":"5","key":"16_CR12","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/S10009-024-00754-1","volume":"26","author":"S Jacobs","year":"2024","unstructured":"Jacobs, S., et al.: The reactive synthesis competition (SYNTCOMP): 2018\u20132021. Int. J. Softw. Tools Technol. Transf. 26(5), 551\u2013567 (2024). https:\/\/doi.org\/10.1007\/S10009-024-00754-1","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"16_CR13","unstructured":"Knuth, D.: The Art of Computer Programming: Combinatorial algorithms, Part 1. Volume 4a. Addison-Wesley (2011). https:\/\/books.google.de\/books?id=jT-30QEACAAJ"},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Prokop, M., Zarkhah, A.: Semml: enhancing automata-theoretic LTL synthesis with machine learning. In: Gurfinkel, A., Heule, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, 3\u20138 May 2025, Proceedings, Part I. Lecture Notes in Computer Science, vol. 15696, 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":"16_CR15","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":"16_CR16","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Prokop, M.: Semml 2.0: synthesizing controllers for LTL (2026). https:\/\/arxiv.org\/abs\/2604.24102"},{"issue":"5","key":"16_CR17","doi-asserted-by":"publisher","first-page":"1045","DOI":"10.1002\/j.1538-7305.1955.tb03788.x","volume":"34","author":"GH Mealy","year":"1955","unstructured":"Mealy, G.H.: A method for synthesizing sequential circuits. Bell Syst. Tech. J. 34(5), 1045\u20131079 (1955). https:\/\/doi.org\/10.1002\/j.1538-7305.1955.tb03788.x","journal-title":"Bell Syst. Tech. J."},{"key":"16_CR18","unstructured":"Meggendorfer, T.: JBDD: a java BDD library (2017). https:\/\/github.com\/incaseoftrouble\/jbdd"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1007\/978-3-319-96145-3_31","volume-title":"Computer Aided Verification","author":"PJ Meyer","year":"2018","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: explicit reactive synthesis strikes back! In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 578\u2013586. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31"},{"key":"16_CR20","doi-asserted-by":"publisher","unstructured":"Piterman, N.: From nondeterministic buchi and streett automata to deterministic parity automata. In: 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12\u201315 August 2006, Seattle, WA, USA, Proceedings, pp. 255\u2013264. IEEE Computer Society (2006). https:\/\/doi.org\/10.1109\/LICS.2006.28","DOI":"10.1109\/LICS.2006.28"},{"key":"16_CR21","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October\u20131 November 1977, pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/BFb0035790","volume-title":"Automata, Languages and Programming","author":"A Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652\u2013671. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/BFb0035790"},{"issue":"2","key":"16_CR23","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/S10703-022-00407-6","volume":"61","author":"F Renkin","year":"2022","unstructured":"Renkin, F., Schlehuber-Caissier, P., Duret-Lutz, A., Pommellet, A.: Dissecting ltlsynt. Formal Methods Syst. Des. 61(2), 248\u2013289 (2022). https:\/\/doi.org\/10.1007\/S10703-022-00407-6","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR24","doi-asserted-by":"publisher","unstructured":"Renkin, F., Schlehuber-Caissier, P., Duret-Lutz, A., Pommellet, A.: Effective reductions of mealy machines. In: Mousavi, M.R., Philippou, A. (eds.) Formal Techniques for Distributed Objects, Components, and Systems 42nd IFIP WG 6.1 International Conference, FORTE 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Lucca, Italy, 13\u201317 June 2022, Proceedings. Lecture Notes in Computer Science, vol. 13273, pp. 114\u2013130. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-08679-3_8","DOI":"10.1007\/978-3-031-08679-3_8"},{"key":"16_CR25","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez, A., Gorostiaga, F., S\u00e1nchez, C.: Counter example guided reactive synthesis for LTL modulo theories. In: Piskac, R., Rakamaric, Z. (eds.) Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, 23\u201325 July 2025, Proceedings, Part IV. Lecture Notes in Computer Science, vol. 15934, pp. 224\u2013248. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98685-7_11","DOI":"10.1007\/978-3-031-98685-7_11"},{"key":"16_CR26","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez, A., S\u00e1nchez, C.: Boolean abstractions for realizability modulo theories. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, 17\u201322 July 2023, Proceedings, Part III, pp. 305\u2013328. Lecture Notes in Computer Science. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_15","DOI":"10.1007\/978-3-031-37709-9_15"},{"key":"16_CR27","doi-asserted-by":"publisher","unstructured":"Safra, S.: On the complexity of omega-automata. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24\u201326 October 1988, pp. 319\u2013327. IEEE Computer Society (1988). https:\/\/doi.org\/10.1109\/SFCS.1988.21948","DOI":"10.1109\/SFCS.1988.21948"},{"key":"16_CR28","doi-asserted-by":"publisher","unstructured":"Schewe, S.: Tighter bounds for the determinisation of b\u00fcchi automata. In: de\u00a0Alfaro, L. (ed.) Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, 22\u201329 March 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05504, pp. 167\u2013181. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-00596-1_13","DOI":"10.1007\/978-3-642-00596-1_13"},{"key":"16_CR29","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: 1st Symposium in Logic in Computer Science (LICS). IEEE Computer Society (1986)"}],"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_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:58Z","timestamp":1784791078000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_16","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"}}]}}