{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:23:17Z","timestamp":1779074597178,"version":"3.51.4"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031787492","type":"print"},{"value":"9783031787508","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-78750-8_2","type":"book-chapter","created":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T12:15:34Z","timestamp":1739276134000},"page":"28-50","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Predictable and\u00a0Performant Reactive Synthesis Modulo Theories via\u00a0Functional Synthesis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-3464-8667","authenticated-orcid":false,"given":"Andoni","family":"Rodr\u00edguez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3478-3408","authenticated-orcid":false,"given":"Felipe","family":"Gorostiaga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3927-4773","authenticated-orcid":false,"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,2,12]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Alshiekh, M., Bloem, R., Ehlers, R., K\u00f6nighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: McIlraith, S.A., Weinberger, K.Q. (eds.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), pp. 2669\u20132678. AAAI Press (2018)","DOI":"10.1609\/aaai.v32i1.11797"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Proceedings of the 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2013), pp. 1\u20138. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"2_CR3","unstructured":"Azzopardi, S., Piterman, N., Schneider, G., di\u00a0Stefano, L.: LTL synthesis on infinite-state arenas defined by programs (2023)"},{"key":"2_CR4","unstructured":"Azzopardi, S., Piterman, N., Schneider, G., Stefano, L.D.: LTL synthesis on infinite-state arenas defined by programs. CoRR, abs\/2307.09776 (2023)"},{"issue":"3","key":"2_CR5","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)","journal-title":"J. Comput. Syst. Sci."},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-662-46681-0_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Bloem","year":"2015","unstructured":"Bloem, R., K\u00f6nighofer, B., K\u00f6nighofer, R., Wang, C.: Shield synthesis: runtime enforcement for reactive systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 533\u2013548. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_51"},{"key":"2_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74113-8","volume-title":"The Calculus of Computation","author":"AR Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74113-8"},{"key":"2_CR8","unstructured":"Cheng, C.-H., Lee, E.A.: Numerical LTL synthesis for cyber-physical systems. CoRR, abs\/1307.3722 (2013)"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Choi, W., Finkbeiner, B., Piskac, R., Santolucito, M.: Can reactive synthesis and syntax-guided synthesis be friends? In: Jhala, R., Dillig, I. (eds.) 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022), pp. 229\u2013243. ACM (2022)","DOI":"10.1145\/3519939.3523429"},{"key":"2_CR10","unstructured":"Corsi, D., Amir, G., Rodriguez, A., Sanchez, C., Katz, G., Fox, R.: Verification-guided shielding for deep reinforcement learning. CoRR, abs\/2406.06507 (2024)"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Veanes, M.: Minimization of symbolic automata. In: Procedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201914), pp. 541\u2013554. ACM (2014)","DOI":"10.1145\/2535838.2535849"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-319-63387-9_3","volume-title":"Computer Aided Verification","author":"L D\u2019Antoni","year":"2017","unstructured":"D\u2019Antoni, L., Veanes, M.: The power of symbolic automata and transducers. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017, Part I. LNCS, vol. 10426, pp. 47\u201367. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_3"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Faran, R., Kupferman, O.: LTL with arithmetic and its applications in reasoning about hierarchical systems. In: Proceedings of the 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, (LPAR-22. ). EPiC Series in Computing, vol.\u00a057, pp. 343\u2013362. EasyChair (2018)","DOI":"10.29007\/wpg3"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Farzan, A, Kincaid, Z.: Strategy synthesis for linear arithmetic games. Proc. ACM Program. Lang. 2(POPL), 61:1\u201361:30 (2018)","DOI":"10.1145\/3158149"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-030-11245-5_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G Fedyukovich","year":"2019","unstructured":"Fedyukovich, G., Gurfinkel, A., Gupta, A.: Lazy but effective functional synthesis. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 92\u2013113. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_5"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B. Synthesis of reactive systems. In: Esparza, J., Grumberg, O., Sickert, S. (eds.) Dependable Software Systems Engineering. NATO Science for Peace and Security Series - D: Information and Communication Security, vol.\u00a045, pp. 72\u201398. IOS Press (2016)","DOI":"10.3233\/978-1-61499-627-9-72"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-030-99253-8_17","volume-title":"Foundations of Software Science and Computation Structures","author":"B Finkbeiner","year":"2022","unstructured":"Finkbeiner, B., Heim, P., Passing, N.: Temporal stream logic modulo theories. In: FoSSaCS 2022. LNCS, vol. 13242, pp. 325\u2013346. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99253-8_17"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-319-17524-9_13","volume-title":"NASA Formal Methods","author":"A Gacek","year":"2015","unstructured":"Gacek, A., Katis, A., Whalen, M.W., Backes, J., Cofer, D.: Towards realizability checking of contracts using theories. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 173\u2013187. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_13"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Geatti, L., Gianola, A., Gigante, N.: Linear temporal logic modulo theories over finite traces. In: Proceedings of the 31st International Joint Conference on Artificial Intelligence, (IJCAI 2022), pp. 2641\u20132647. ijcai.org (2022)","DOI":"10.24963\/ijcai.2022\/366"},{"key":"2_CR21","unstructured":"Geatti, L., Gianola, A., Gigante, N.: A general automata model for first-order temporal logics (extended version). CoRR, abs\/2405.20057 (2024)"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Geatti, L., Gianola, A., Gigante, N., Winkler, S.: Decidable fragments of LTLF modulo theories (extended version). CoRR, abs\/2307.16840 (2023)","DOI":"10.3233\/FAIA230348"},{"key":"2_CR23","unstructured":"Gianola, A., Gigante, N.: LTL modulo theories over finite traces: modeling, verification, open questions. In: Short Paper Proceedings of the 4th Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis hosted by the 21st International Conference of the Italian Association for Artificial Intelligence (AIxIA 2022). CEUR Workshop Proceedings, vol. 3311, pp. 13\u201319. CEUR-WS.org (2022)"},{"issue":"POPL","key":"2_CR24","doi-asserted-by":"publisher","first-page":"1696","DOI":"10.1145\/3632899","volume":"8","author":"P Heim","year":"2024","unstructured":"Heim, P., Dimitrova, R.: Solving infinite-state games via acceleration. Proc. ACM Program. Lang. 8(POPL), 1696\u20131726 (2024)","journal-title":"Proc. ACM Program. Lang."},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Hu, Q., D\u2019Antoni, L.: Automatic program inversion using symbolic transducers. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017), pp. 376\u2013389. ACM (2017)","DOI":"10.1145\/3062341.3062345"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Katis, A., Fedyukovich, G., Gacek, A., Backes, J.D., Gurfinkel, A., Whalen, M.W.: Synthesis from assume-guarantee contracts using skolemized proofs of realizability. CoRR, abs\/1610.05867 (2016)","DOI":"10.1145\/2897667.2897675"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-319-89963-3_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Katis","year":"2018","unstructured":"Katis, A., et al.: Validity-guided synthesis of reactive systems from assume-guarantee contracts. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 176\u2013193. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_10"},{"key":"2_CR28","unstructured":"Maderbacher, B., Bloem, R.: Reactive synthesis modulo theories using abstraction refinement. In: 22nd Formal Methods in Computer-Aided Design, (FMCAD 2022), pp. 315\u2013324. IEEE (2022)"},{"key":"2_CR29","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems - Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems - Safety. Springer, New York (1995). https:\/\/doi.org\/10.1007\/978-1-4612-4222-2"},{"key":"2_CR30","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":"2_CR31","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science (FOCS\u201977), pp. 46\u201367. IEEE CS Press (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th Annual ACM Symposium on Principles of Programming Languages (POPL\u201989), pp. 179\u2013190. ACM Press (1989)","DOI":"10.1145\/75277.75293"},{"key":"2_CR33","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"},{"key":"2_CR34","unstructured":"Rodriguez, A., Amir, G., Corsi, D., Sanchez, C., Katz, G.: Shield synthesis for LTL modulo theories. CoRR, abs\/2406.04184 (2024)"},{"key":"2_CR35","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-031-37709-9_15","volume-title":"CAV 2023","author":"A Rodr\u00edguez","year":"2023","unstructured":"Rodr\u00edguez, A., S\u00e1nchez, C.: Boolean abstractions for realizability modulo theories. In: Enea, C., Lal, A. (eds.) CAV 2023. LNCS, vol. 13966, pp. 1\u201324. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_15"},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Rodriguez, A., S\u00e1nchez, C.: Adaptive reactive synthesis for LTL and LTLf modulo theories. In: Proceedings of the 38th AAAI Conference on Artificial Intelligence (AAAI 2024), pp. 10679\u201310686. AAAI Press (2024)","DOI":"10.1609\/aaai.v38i9.28939"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Rodriguez, A., Sanchez, C.: Realizability modulo theories. J. Log. Algebr. Meth. Program. 100971 (2024)","DOI":"10.1016\/j.jlamp.2024.100971"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"Samuel, S., D\u2019Souza, D., Komondoor, R.: Gensys: a scalable fixed-point engine for maximal controller synthesis over infinite state spaces. In: Proceedings of the 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE\u201921), pp. 1585\u20131589. ACM (2021)","DOI":"10.1145\/3468264.3473126"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Samuel, S., D\u2019Souza, D., Komondoor, R.: Symbolic fixpoint algorithms for logical LTL games. In: Proceedings of the 38th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2023), pp. 698\u2013709. IEEE (2023)","DOI":"10.1109\/ASE56229.2023.00212"},{"key":"2_CR40","unstructured":"Veanes, M., Ball, T., Ebner, G., Saarikivi, O.: Symbolic automata: $$\\omega $$-regularity modulo theories. CoRR, abs\/2310.02393 (2023)"},{"key":"2_CR41","doi-asserted-by":"crossref","unstructured":"Walker, A., Ryzhyk, L.: Predicate abstraction for reactive synthesis. In: Proceedings of the 14th Formal Methods in Computer-Aided Design, (FMCAD 2014), pp. 219\u2013226. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987617"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-78750-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T10:08:28Z","timestamp":1769681308000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-78750-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031787492","9783031787508"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-78750-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"12 February 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}