{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:22:53Z","timestamp":1779074573264,"version":"3.51.4"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377082","type":"print"},{"value":"9783031377099","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we address the problem of the (reactive) realizability of specifications of theories richer than Booleans, including arithmetic theories. Our approach transforms theory specifications into purely Boolean specifications by (1) substituting theory literals by Boolean variables, and (2) computing an additional Boolean requirement that captures the dependencies between the new variables imposed by the literals. The resulting specification can be passed to existing Boolean off-the-shelf realizability tools, and is realizable if and only if the original specification is realizable. The first contribution is a brute-force version of our method, which requires a number of SMT queries that is doubly exponential in the number of input literals. Then, we present a faster method that exploits a nested encoding of the search for the extra requirement and uses SAT solving for faster traversing the search space and uses SMT queries internally. Another contribution is a prototype in Z3-Python. Finally, we report an empirical evaluation using specifications inspired in real industrial cases. To the best of our knowledge, this is the first method that succeeds in non-Boolean LTL realizability.<\/jats:p>","DOI":"10.1007\/978-3-031-37709-9_15","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"305-328","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Boolean Abstractions for\u00a0Realizability Modulo Theories"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-3464-8667","authenticated-orcid":false,"given":"Andoni","family":"Rodr\u00edguez","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3927-4773","authenticated-orcid":false,"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Proceedings of Formal Methods in Computer-Aided Design, (FMCAD) 2013, Portland, OR, USA, October 20\u201323, 2013, pp. 1\u20138. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Bend\u00edk, J., S. Meel, K.S.: Counting maximal satisfiable subsets. In: Proceedings of the 35th AAAI Conference on Artificial Intelligence, (AAAI\u201921), pp. 3651\u20133660. AAAI Press (2021)","DOI":"10.1609\/aaai.v35i5.16481"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-030-81688-9_15","volume-title":"Computer Aided Verification","author":"J Bend\u00edk","year":"2021","unstructured":"Bend\u00edk, J., Meel, K.S.: Counting minimal unsatisfiable subsets. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 313\u2013336. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_15"},{"issue":"3","key":"15_CR4","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/s10703-021-00381-5","volume":"57","author":"R Bloem","year":"2021","unstructured":"Bloem, R., Chockler, H., Ebrahimi, M., Strichman, O.: Vacuity in synthesis. Formal Meth. Syst. Des. 57(3), 473\u2013495 (2021). https:\/\/doi.org\/10.1007\/s10703-021-00381-5","journal-title":"Formal Meth. Syst. Des."},{"issue":"3","key":"15_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":"15_CR6","unstructured":"Caulfield, B., Rabe, M.N., Seshia, S.A., Tripakis, S.: What\u2019s decidable about syntax-guided synthesis? CoRR, abs\/1510.08393 (2015)"},{"key":"15_CR7","unstructured":"Cheng, C.-H., Lee, E.A.: Numerical LTL synthesis for cyber-physical systems. CoRR, abs\/1307.3722 (2013)"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Choi, W., Finkbeiner, B., Piskac, R., Santolucito, M.: Can reactive synthesis and syntax-guided synthesis be friends? In: Proceedings of the 43rd ACM SIGPLAN Int\u2019l Conference on Programming Language Design and Implementation (PLD\u201922), pp. 229\u2013243. ACM (2022)","DOI":"10.1145\/3519939.3523429"},{"issue":"2","key":"15_CR9","first-page":"91","volume":"7","author":"DW Cooper","year":"1972","unstructured":"Cooper, D.W.: Theorem proving in arithmetic without multiplication. Mach. Intell. 7(2), 91\u2013100 (1972)","journal-title":"Mach. Intell."},{"key":"15_CR10","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"},{"issue":"3","key":"15_CR11","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1016\/j.ic.2006.09.006","volume":"205","author":"S Demri","year":"2007","unstructured":"Demri, S., D\u2019Souza, D.: An automata-theoretic approach to constraint LTL. Inf. Comput. 205(3), 380\u2013415 (2007)","journal-title":"Inf. Comput."},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Rachel 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. ), Awassa, Ethiopia, 16\u201321 November 2018, vol. 57 of EPiC Series in Computing, pp. 343\u2013362. EasyChair (2018)","DOI":"10.29007\/wpg3"},{"key":"15_CR13","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":"15_CR14","unstructured":"Finkbeiner, B.: Synthesis of reactive systems. In: Esparza, J., Grumberg, O., Sickert, S., eds, Dependable Software Systems Engineering, vol. 45 of NATO Science for Peace and Security Series - D: Information and Communication Security, pp. 72\u201398. IOS Press (2016)"},{"key":"15_CR15","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":"Bernd Finkbeiner","year":"2022","unstructured":"Finkbeiner, Bernd, Heim, Philippe, Passing, Noemi: 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":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1007\/978-3-030-25540-4_35","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2019","unstructured":"Finkbeiner, B., Klein, F., Piskac, R., Santolucito, M.: Temporal Stream Logic: Synthesis Beyond the Bools. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 609\u2013629. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_35"},{"issue":"5\u20136","key":"15_CR17","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transf. 15(5\u20136), 519\u2013539 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"15_CR18","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":"15_CR19","unstructured":"Gianola, A., Gigante. N.: LTL modulo theories over finite traces: modeling, verification, open questions. In: Proceedings of the 4th Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, vol. 3311 of CEUR Workshop Proceedings, pp. 13\u201319, CEUR-WS.org (2022)"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata Logics, and Infinite Games","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Jacobs, S.: The 4th reactive synthesis competition (SYNTCOMP 2017): Benchmarks, participants & results. In: Proceedings of the 6th Workshop on Synthesis (SYNT@CAV 2017), vol. 260 of EPTCS, pp. 116\u2013143 (2017)","DOI":"10.4204\/EPTCS.260.10"},{"key":"15_CR22","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":"15_CR23","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., Fedyukovich, G., Guo, H., Gacek, A., Backes, J., Gurfinkel, A., Whalen, M.W.: 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"},{"issue":"2","key":"15_CR24","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/s10601-015-9183-0","volume":"21","author":"MH Liffiton","year":"2016","unstructured":"Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints An Int. J. 21(2), 223\u2013250 (2016)","journal-title":"Constraints An Int. J."},{"key":"15_CR25","unstructured":"Maderbacher, B., Bloem, R.:Reactive synthesis modulo theories using abstraction refinement. In: 22nd Formal Methods in Computer-Aided Design, (FMCAD\u201922), pp 315\u2013324. IEEE (2022)"},{"key":"15_CR26","doi-asserted-by":"publisher","unstructured":"Manna, Z., Pnueli, A.: Temporal verification of reactive systems - safety. Springer, Springer New York, NY (1995). https:\/\/doi.org\/10.1007\/978-1-4612-422-2","DOI":"10.1007\/978-1-4612-422-2"},{"key":"15_CR27","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":"15_CR28","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":"15_CR29","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":"15_CR30","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":"15_CR31","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":"15_CR32","unstructured":"Tarski, A.: Theorem proving in arithmetic without multiplication. University of California Press (1951)"},{"key":"15_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"635","DOI":"10.1007\/978-3-540-78127-1_35","volume-title":"Pillars of Computer Science","author":"W Thomas","year":"2008","unstructured":"Thomas, W.: Church\u2019s Problem and a Tour through Automata Theory. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 635\u2013655. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78127-1_35"},{"key":"15_CR34","doi-asserted-by":"crossref","unstructured":"Walker, A., Ryzhyk, L.: Predicate abstraction for reactive synthesis. In Proceedings f the 14th Formal Methods in Computer-Aided Design, (FMCAD 2014), Lausanne, Switzerland, October 21\u201324, 2014, pp.19\u2013226. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987617"}],"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-031-37709-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,24]],"date-time":"2024-10-24T06:56:47Z","timestamp":1729753007000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37709-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377082","9783031377099"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37709-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}