{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:06Z","timestamp":1776333486406,"version":"3.51.2"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986840","type":"print"},{"value":"9783031986857","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Recently, interest has increased in applying reactive synthesis to richer-than-Boolean domains. A major (undecidable) challenge in this area is to establish when certain repeating behaviour terminates in a desired state when the number of steps is unbounded. Existing approaches struggle with this problem, or can handle at most deterministic games with B\u00fcchi goals. This work goes beyond by contributing the first effectual approach to synthesis with full LTL objectives, based on Boolean abstractions that encode both safety and liveness properties of the underlying infinite arena. We take a CEGAR approach: attempting synthesis on the Boolean abstraction, checking spuriousness of abstract counterstrategies through invariant checking, and refining the abstraction based on counterexamples. We reduce the complexity, when restricted to predicates, of abstracting and synthesising by an exponential through an efficient binary encoding. This also allows us to eagerly identify useful fairness properties. Our discrete synthesis tool outperforms the state-of-the-art on linear integer arithmetic (LIA) benchmarks from literature, solving almost double as many syntesis problems as the current state-of-the-art. It also solves slightly more problems than the second-best realisability checker, in one-third of the time. We also introduce benchmarks with richer objectives that other approaches cannot handle, and evaluate our tool on them.<\/jats:p>","DOI":"10.1007\/978-3-031-98685-7_13","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:32:31Z","timestamp":1753155151000},"page":"274-297","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Full LTL Synthesis over\u00a0Infinite-State Arenas"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2165-3698","authenticated-orcid":false,"given":"Shaun","family":"Azzopardi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1922-3151","authenticated-orcid":false,"given":"Luca","family":"Di Stefano","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8242-5357","authenticated-orcid":false,"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0629-6853","authenticated-orcid":false,"given":"Gerardo","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-540-74407-8_6","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"L de Alfaro","year":"2007","unstructured":"de Alfaro, L., Roy, P.: Solving games via three-valued abstraction refinement. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 74\u201389. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_6"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Azzopardi, S., Piterman, N., Stefano, L.D., Schneider, G.: Full LTL synthesis over infinite-state arenas (2025). https:\/\/arxiv.org\/abs\/2307.09776","DOI":"10.1007\/978-3-031-98685-7_13"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"894","DOI":"10.1007\/978-3-030-81685-8_42","volume-title":"Computer Aided Verification","author":"C Baier","year":"2021","unstructured":"Baier, C., Coenen, N., Finkbeiner, B., Funke, F., Jantsch, S., Siber, J.: Causality-based game solving. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 894\u2013917. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_42"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11562436_1","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2005","author":"I Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Ranking abstraction as companion to predicate abstraction. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 1\u201312. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11562436_1"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Beyene, T.A., Chaudhuri, S., Popeea, C., Rybalchenko, A.: A constraint-based approach to solving games on infinite graphs. In: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 221\u2013234. ACM (2014)","DOI":"10.1145\/2535838.2535860"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: Cpachecker: A tool for configurable software verification. In: Computer Aided Verification - 23rd International Conference, CAV 2011. LNCS, vol.\u00a06806, pp. 184\u2013190. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuxmv symbolic model checker. In: Computer Aided Verification - 26th International Conference, CAV 2014. LNCS, vol.\u00a08559, pp. 334\u2013342. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"13_CR8","doi-asserted-by":"publisher","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 International Conference on Programming Language Design and Implementation, pp. 229\u2013243. PLDI 2022, Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3519939.3523429","DOI":"10.1145\/3519939.3523429"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathsat5 SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013. LNCS, vol.\u00a07795, pp. 93\u2013107. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"13_CR10","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, London, Cambridge (1999)"},{"key":"13_CR11","doi-asserted-by":"publisher","unstructured":"Di\u00a0Stefano, L., Azzopardi, S., Piterman, N., Schneider, G.: Software artifact for \u201cfull LTL synthesis over infinite-state arenas\u201d (2025). https:\/\/doi.org\/10.5281\/zenodo.15189175","DOI":"10.5281\/zenodo.15189175"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Ehlers, R., Khalimov, A.: Fully generalized reactivity(1) synthesis. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024. LNCS, vol. 14570, pp. 83\u2013102. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_6","DOI":"10.1007\/978-3-031-57246-3_6"},{"key":"13_CR13","doi-asserted-by":"publisher","unstructured":"Farzan, A., Kincaid, Z.: Strategy synthesis for linear arithmetic games. Proc. ACM Program. Lang. 2(POPL) (2017). https:\/\/doi.org\/10.1145\/3158149","DOI":"10.1145\/3158149"},{"key":"13_CR14","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"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Olderog, E.: Ten years of petri games. In: Jansen, N., Junges, S., Kaminski, B.L., Matheja, C., Noll, T., Quatmann, T., Stoelinga, M., Volk, M. (eds.) Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III. LNCS, vol. 15262, pp. 399\u2013422. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-75778-5_19","DOI":"10.1007\/978-3-031-75778-5_19"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10","DOI":"10.1007\/3-540-63166-6_10"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Hausmann, D., Lehaut, M., Piterman, N.: Symbolic solution of Emerson-Lei games for reactive synthesis. In: Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024. LNCS, vol. 14574, pp. 55\u201378. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57228-9_4","DOI":"10.1007\/978-3-031-57228-9_4"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Heim, P., Dimitrova, R.: Solving infinite-state games via acceleration. Proc. ACM Program. Lang. 8(POPL) (2024). https:\/\/doi.org\/10.1145\/3632899","DOI":"10.1145\/3632899"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Heim, P., Dimitrova, R.: Translation of temporal logic for efficient infinite-state reactive synthesis. Proc. ACM Program. Lang. 9(POPL) (2025)","DOI":"10.1145\/3704888"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"886","DOI":"10.1007\/3-540-45061-0_69","volume-title":"Automata, Languages and Programming","author":"TA Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Counterexample-guided control. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 886\u2013902. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-45061-0_69"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, 16-18 January 2002, pp. 58\u201370. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503279","DOI":"10.1145\/503272.503279"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Maderbacher, B., Bloem, R.: Reactive synthesis modulo theories using abstraction refinement. In: 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022, pp. 315\u2013324. TU Wien Academic Press (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_38","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_38"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Maderbacher, B., Windisch, F., Bloem, R.: Synthesis from infinite-state generalized reactivity(1) specifications. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies - 12th International Symposium, ISoLA 2024, Crete, Greece, 27-31 October 2024, Proceedings, Part IV. LNCS, vol. 15222, pp. 281\u2013301. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-75387-9_17","DOI":"10.1007\/978-3-031-75387-9_17"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Martin, D.A.: Borel determinacy. Ann. Math. 102(2), 363\u2013371 (1975). http:\/\/www.jstor.org\/stable\/1971035","DOI":"10.2307\/1971035"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Computer Aided Verification, 18th International Conference, CAV 2006. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer (2006). https:\/\/doi.org\/10.1007\/11817963_14","DOI":"10.1007\/11817963_14"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: explicit reactive synthesis strikes back! In: Computer Aided Verification - 30th International Conference, CAV 2018. LNCS, vol. 10981, pp. 578\u2013586. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Neider, D., Markgraf, O.: Learning-based synthesis of safety controllers. In: 2019 Formal Methods in Computer Aided Design (FMCAD), pp. 120\u2013128. IEEE (2019). https:\/\/doi.org\/10.23919\/FMCAD.2019.8894254","DOI":"10.23919\/FMCAD.2019.8894254"},{"key":"13_CR28","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-319-10575-8_2","volume-title":"Handbook of Model Checking","author":"N Piterman","year":"2018","unstructured":"Piterman, N., Pnueli, A.: Temporal logic and fair discrete systems. In: Handbook of Model Checking, pp. 27\u201373. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_2"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190. ACM Press (1989)","DOI":"10.1145\/75277.75293"},{"key":"13_CR30","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-22 July 2023, Proceedings, Part III. LNCS, vol. 13966, pp. 305\u2013328. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_15","DOI":"10.1007\/978-3-031-37709-9_15"},{"key":"13_CR31","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez, A., S\u00e1nchez, C.: Adaptive reactive synthesis for LTL and LTLF modulo theories. In: Wooldridge, M.J., Dy, J.G., Natarajan, S. (eds.) Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2014, 20-27 February 2024, Vancouver, Canada, pp. 10679\u201310686. AAAI Press (2024). https:\/\/doi.org\/10.1609\/AAAI.V38I9.28939","DOI":"10.1609\/AAAI.V38I9.28939"},{"key":"13_CR32","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2024.100971","volume":"140","author":"A Rodr\u00edguez","year":"2024","unstructured":"Rodr\u00edguez, A., S\u00e1nchez, C.: Realizability modulo theories. J. Log. Algebraic Methods Program. 140, 100971 (2024). https:\/\/doi.org\/10.1016\/J.JLAMP.2024.100971","journal-title":"J. Log. Algebraic Methods Program."},{"key":"13_CR33","doi-asserted-by":"publisher","unstructured":"Samuel, S., D\u2019Souza, D., Komondoor, R.: Symbolic fixpoint algorithms for logical LTL games. In: 2023 38th IEEE\/ACM International Conference on Automated Software Engineering (ASE) pp. 698\u2013709 (2023). https:\/\/doi.org\/10.1109\/ASE56229.2023.00212","DOI":"10.1109\/ASE56229.2023.00212"},{"key":"13_CR34","doi-asserted-by":"publisher","unstructured":"Schmuck, A.K., Heim, P., Dimitrova, R., Nayak, S.P.: Localized attractor computations for infinite-state games. In: Gurfinkel, A., Ganesh, V. (eds.) 36th International Conference on Computer Aided Verification (CAV). LNCS, vol. 14683, pp. 135\u2013158. Springer, Montreal, QC, Canada (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_7","DOI":"10.1007\/978-3-031-65633-0_7"},{"key":"13_CR35","unstructured":"Unno, H., Satake, Y., Terauchi, T., Koskinen, E.: Program verification via predicate constraint satisfiability modulo theories. CoRR abs\/2007.03656 (2020). https:\/\/arxiv.org\/abs\/2007.03656"},{"key":"13_CR36","doi-asserted-by":"publisher","unstructured":"Walker, A., Ryzhyk, L.: Predicate abstraction for reactive synthesis. In: 2014 Formal Methods in Computer-Aided Design (FMCAD), pp. 219\u2013226 (2014). https:\/\/doi.org\/10.1109\/FMCAD.2014.6987617","DOI":"10.1109\/FMCAD.2014.6987617"},{"issue":"2","key":"13_CR37","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1006\/INCO.2000.2894","volume":"164","author":"I Walukiewicz","year":"2001","unstructured":"Walukiewicz, I.: Pushdown processes: games and model-checking. Inf. Comput. 164(2), 234\u2013263 (2001). https:\/\/doi.org\/10.1006\/INCO.2000.2894","journal-title":"Inf. Comput."}],"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-98685-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T08:54:43Z","timestamp":1760086483000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98685-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986840","9783031986857"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98685-7_13","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":"23 July 2025","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":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","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":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}