{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:11Z","timestamp":1776333491031,"version":"3.51.2"},"publisher-location":"Cham","reference-count":25,"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>The synthesis of infinite-state reactive systems from temporal logic specifications or infinite-state games has attracted significant attention in recent years, leading to the emergence of novel solving techniques. Most approaches are accompanied by an implementation showcasing their viability on an increasingly larger collection of benchmarks. Those implementations are \u2013often simple\u2013 prototypes. Furthermore, differences in specification formalisms and formats make comparisons difficult, and writing specifications is a tedious and error-prone task.<\/jats:p>\n          <jats:p>To address this, we present , a tool for specification, realizability, and synthesis of infinite-state reactive systems.  comes with an expressive specification language that allows for combining infinite-state games and temporal formulas, thus encompassing the current formalisms. The realizability checking and synthesis methods implemented in  build upon recently developed approaches and extend them with newly engineered efficient techniques, offering a portfolio of solving algorithms. We evaluate  on an extensive set of benchmarks, demonstrating its competitiveness with the state of the art. Furthermore,  provides tooling for a general high-level format designed to make specification easier for users. It also includes a compiler to a more machine-readable format that other tool developers can easily use, which we hope will lead to a broader adoption and advances in infinite-state reactive synthesis.<\/jats:p>","DOI":"10.1007\/978-3-031-98685-7_14","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:32:51Z","timestamp":1753155171000},"page":"298-312","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Issy: A Comprehensive Tool for Specification and Synthesis of Infinite-State Reactive Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5433-8133","authenticated-orcid":false,"given":"Philippe","family":"Heim","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0006-2494-8690","authenticated-orcid":false,"given":"Rayna","family":"Dimitrova","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","unstructured":"Azzopardi, S., Piterman, N., Schneider, G., Stefano, L.D.: Symbolic infinite-state LTL synthesis (2024). https:\/\/doi.org\/10.48550\/ARXIV.2307.09776","DOI":"10.48550\/ARXIV.2307.09776"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Choi, W., Finkbeiner, B., Piskac, R., Santolucito, M.: Can reactive synthesis and syntax-guided synthesis be friends? In: Jhala, R., Dillig, I. (eds.) PLDI 2022: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, 13\u201317 June 2022, pp. 229\u2013243. ACM (2022). https:\/\/doi.org\/10.1145\/3519939.3523429","DOI":"10.1145\/3519939.3523429"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From spot 2.0 to spot 2.10: what\u2019s new? In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, 7\u201310 August 2022, Proceedings, Part II, LNCS, vol. 13372, pp. 174\u2013187. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"14_CR4","doi-asserted-by":"publisher","unstructured":"Farzan, A., Kincaid, Z.: Strategy synthesis for linear arithmetic games. Proc. ACM Program. Lang. 2(POPL), 61:1\u201361:30 (2018). https:\/\/doi.org\/10.1145\/3158149","DOI":"10.1145\/3158149"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Heim, P., Passing, N.: Temporal stream logic modulo theories. In: Bouyer, P., Schr\u00f6der, L. (eds.) Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, 2\u20137 April 2022, Proceedings, LNCS, vol. 13242, pp. 325\u2013346. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99253-8_17","DOI":"10.1007\/978-3-030-99253-8_17"},{"key":"14_CR6","doi-asserted-by":"publisher","unstructured":"Gu, Y., Tsukada, T., Unno, H.: Optimal CHC solving via termination proofs. Proc. ACM Program. Lang. 7(POPL), 604\u2013631 (2023). https:\/\/doi.org\/10.1145\/3571214","DOI":"10.1145\/3571214"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Heim, P., Dimitrova, R.: Solving infinite-state games via acceleration. Proc. ACM Program. Lang. 8(POPL), 1696\u20131726 (2024). https:\/\/doi.org\/10.1145\/3632899","DOI":"10.1145\/3632899"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Heim, P., Dimitrova, R.: Issy: a comprehensive tool for specification and synthesis of infinite-state reactive systems (2025). https:\/\/doi.org\/10.48550\/ARXIV.2502.03013","DOI":"10.48550\/ARXIV.2502.03013"},{"key":"14_CR9","doi-asserted-by":"publisher","unstructured":"Heim, P., Dimitrova, R.: Translation of temporal logic for efficient infinite-state reactive synthesis. Proc. ACM Program. Lang. 9(POPL) (2025). https:\/\/doi.org\/10.1145\/3704888","DOI":"10.1145\/3704888"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Jacobs, S., et al.: The reactive synthesis competition (SYNTCOMP): 2018\u20132021. CoRR abs\/2206.00251 (2022). https:\/\/doi.org\/10.48550\/ARXIV.2206.00251","DOI":"10.48550\/ARXIV.2206.00251"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Jacobs, S., P\u00e9rez, G.A., Schlehuber-Caissier, P.: The temporal logic synthesis format TLSF v1.2. CoRR abs\/2303.03839 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2303.03839","DOI":"10.48550\/ARXIV.2303.03839"},{"key":"14_CR12","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, Part II. LNCS, vol. 10806, pp. 176\u2013193. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_10"},{"key":"14_CR13","doi-asserted-by":"publisher","unstructured":"Maderbacher, B., Bloem, R.: Reactive synthesis modulo theories using abstraction refinement. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, 17\u201321 October 2022, pp. 315\u2013324. IEEE (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":"14_CR14","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, October 27-31, 2024, Proceedings, Part IV, LNCS, vol. 15222, pp. 281\u2013301. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-75387-9_17","DOI":"10.1007\/978-3-031-75387-9_17"},{"key":"14_CR15","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, LNCS, vol.\u00a04963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"14_CR16","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 - 1 November 1977, pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez, A., Gorostiaga, F., S\u00e1nchez, C.: Predictable and performant reactive synthesis modulo theories via functional synthesis. In: Akshay, S., Niemetz, A., Sankaranarayanan, S. (eds.) Automated Technology for Verification and Analysis - 22nd International Symposium, ATVA 2024, Kyoto, Japan, October 21-25, 2024, Proceedings, Part II. Lecture Notes in Computer Science, vol. 15055, pp. 28\u201350. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-78750-8_2","DOI":"10.1007\/978-3-031-78750-8_2"},{"key":"14_CR18","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, July 17-22, 2023, Proceedings, Part III. Lecture Notes in Computer Science, 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":"14_CR19","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, February 20-27, 2024, Vancouver, Canada. pp. 10679\u201310686. AAAI Press (2024). https:\/\/doi.org\/10.1609\/AAAI.V38I9.28939","DOI":"10.1609\/AAAI.V38I9.28939"},{"key":"14_CR20","doi-asserted-by":"publisher","unstructured":"Samuel, S., D\u2019Souza, D., Komondoor, R.: Gensys: a scalable fixed-point engine for maximal controller synthesis over infinite state spaces. In: Spinellis, D., Gousios, G., Chechik, M., Penta, M.D. (eds.) ESEC\/FSE \u201921: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Athens, Greece, August 23-28, 2021. pp. 1585\u20131589. ACM (2021). https:\/\/doi.org\/10.1145\/3468264.3473126","DOI":"10.1145\/3468264.3473126"},{"key":"14_CR21","doi-asserted-by":"publisher","unstructured":"Samuel, S., D\u2019Souza, D., Komondoor, R.: Symbolic fixpoint algorithms for logical LTL games. In: 38th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2023, Luxembourg, September 11-15, 2023. pp. 698\u2013709. IEEE (2023). https:\/\/doi.org\/10.1109\/ASE56229.2023.00212","DOI":"10.1109\/ASE56229.2023.00212"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Schmuck, A., Heim, P., Dimitrova, R., Nayak, S.P.: Localized attractor computations for infinite-state games. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III. Lecture Notes in Computer Science, vol. 14683, pp. 135\u2013158. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_7","DOI":"10.1007\/978-3-031-65633-0_7"},{"key":"14_CR23","unstructured":"Unno, H., Satake, Y., Terauchi, T., Koskinen, E.: Program verification via predicate constraint satisfiability modulo theories (2020), https:\/\/arxiv.org\/abs\/2007.03656"},{"key":"14_CR24","doi-asserted-by":"publisher","unstructured":"Unno, H., Terauchi, T., Gu, Y., Koskinen, E.: Modular primal-dual fixpoint logic solving for temporal verification. Proc. ACM Program. Lang. 7(POPL), 2111\u20132140 (2023). https:\/\/doi.org\/10.1145\/3571265","DOI":"10.1145\/3571265"},{"issue":"1\u20132","key":"14_CR25","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W Zielonka","year":"1998","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1\u20132), 135\u2013183 (1998). https:\/\/doi.org\/10.1016\/S0304-3975(98)00009-7","journal-title":"Theor. Comput. Sci."}],"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_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T08:54:58Z","timestamp":1760086498000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98685-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986840","9783031986857"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98685-7_14","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":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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"}}]}}