{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T18:57:07Z","timestamp":1783018627226,"version":"3.54.6"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","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,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"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>Non-well-separation is a common quality issue in reactive synthesis specifications, where the synthesized system can avoid satisfying its guarantees by preventing the environment from satisfying its assumptions. Kind realizability extends the usual GR(1) by additionally requiring the system to always enable the environment to satisfy its assumptions, thereby addressing this issue, and is expected to replace the usual GR(1) realizability checking. Kind realizability relies on a reduction and a 4-nested fixed-point algorithm, whose runtime typically exceeds that of the usual GR(1) realizability checking algorithm by more than 3 times, creating a significant performance bottleneck in specification development processes that require frequent realizability checks. This paper presents a framework designed to accelerate kind realizability checking, comprising: (1) a multi-level incremental checking framework that sequentially integrates approximate computation with the complete 4FP algorithm, reusing previously computed sound bounds at each stage to eliminate redundant state-space exploration; and (2) two accompanying approximation algorithms with lower asymptotic time complexity, which efficiently compute sound upper and lower bounds of the system winning region. Experiments on benchmarks comprising hundreds of specifications demonstrate significant performance improvements.<\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_13","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:49:46Z","timestamp":1779032986000},"page":"240-258","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Accelerating Kind Realizability: A Multi-stage Incremental Realizability Checking Framework"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-4708-914X","authenticated-orcid":false,"given":"Sirui","family":"Liu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8033-7943","authenticated-orcid":false,"given":"Wei","family":"Dong","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Moarref, S., Topcu, U.: Counter-strategy guided refinement of gr (1) temporal logic specifications. In: 2013 Formal Methods in Computer-Aided Design, pp. 26\u201333. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679387"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Amram, G., Ma\u2019ayan, D., Maoz, S., Pistiner, O., Ringert, J.O.: Triggers for reactive synthesis specifications. In: 2023 IEEE\/ACM 45th International Conference on Software Engineering (ICSE), pp. 729\u2013741. IEEE (2023)","DOI":"10.1109\/ICSE48619.2023.00070"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-642-14295-6_37","volume-title":"Computer Aided Verification","author":"R Bloem","year":"2010","unstructured":"Bloem, R., et al.: RATSY \u2013 a new requirements analysis tool with synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 425\u2013429. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_37"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic hardware synthesis from specifications: a case study. In: 2007 Design, Automation & Test in Europe Conference & Exhibition, pp.\u00a01\u20136. IEEE (2007)","DOI":"10.1109\/DATE.2007.364456"},{"issue":"4","key":"13_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2007.09.004","volume":"190","author":"R Bloem","year":"2007","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: hardware from PSL. Electron. Notes Theoret. Comput. Sci. 190(4), 3\u201316 (2007)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"issue":"3","key":"13_CR6","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":"13_CR7","doi-asserted-by":"crossref","unstructured":"Cavezza, D.G., Alrajeh, D., Gy\u00f6rgy, A.: Minimal assumptions refinement for realizable specifications. In: Proceedings of the 8th International Conference on Formal Methods in Software Engineering, pp. 66\u201376 (2020)","DOI":"10.1145\/3372020.3391557"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"D\u2019ippolito, N., Braberman, V., Piterman, N., Uchitel, S.: Synthesizing nonanomalous event-based controllers for liveness goals. ACM Trans. Software Eng. Methodol. (TOSEM) 22(1), 1\u201336 (2013)","DOI":"10.1145\/2430536.2430543"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, pp. 411\u2013420 (1999)","DOI":"10.1145\/302405.302672"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-319-41540-6_18","volume-title":"Computer Aided Verification","author":"R Ehlers","year":"2016","unstructured":"Ehlers, R., Raman, V.: Slugs: extensible GR(1) synthesis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 333\u2013339. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_18"},{"issue":"1","key":"13_CR11","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s00236-019-00351-9","volume":"57","author":"E Firman","year":"2020","unstructured":"Firman, E., Maoz, S., Ringert, J.O.: Performance heuristics for gr (1) synthesis and related algorithms. Acta Informatica 57(1), 37\u201379 (2020)","journal-title":"Acta Informatica"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Gorenstein, A., Maoz, S., Ringert, J.O.: Kind controllers and fast heuristics for non-well-separated gr (1) specifications. In: Proceedings of the 46th IEEE\/ACM International Conference on Software Engineering, pp. 1\u201312 (2024)","DOI":"10.1145\/3597503.3608131"},{"issue":"5","key":"13_CR13","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. Transfer 26(5), 551\u2013567 (2024)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-642-19583-9_16","volume-title":"Hardware and Software: Verification and Testing","author":"U Klein","year":"2011","unstructured":"Klein, U., Pnueli, A.: Revisiting synthesis of GR(1) specifications. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) HVC 2010. LNCS, vol. 6504, pp. 161\u2013181. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19583-9_16"},{"issue":"6","key":"13_CR15","doi-asserted-by":"publisher","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","volume":"25","author":"H Kress-Gazit","year":"2009","unstructured":"Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-logic-based reactive mission and motion planning. IEEE Trans. Rob. 25(6), 1370\u20131381 (2009)","journal-title":"IEEE Trans. Rob."},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Liu, S.: Fm segsyn ae (2026). https:\/\/doi.org\/10.5281\/zenodo.18590272","DOI":"10.5281\/zenodo.18590272"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Ma\u2019Ayan, D., Maoz, S.: Using reactive synthesis: an end-to-end exploratory case study. In: 2023 IEEE\/ACM 45th International Conference on Software Engineering (ICSE), pp. 742\u2013754. IEEE (2023)","DOI":"10.1109\/ICSE48619.2023.00071"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-030-17465-1_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Majumdar","year":"2019","unstructured":"Majumdar, R., Piterman, N., Schmuck, A.-K.: Environmentally-friendly GR(1) synthesis. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 229\u2013246. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_13"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Piterman, N., Schmuck, A.: Environmentally-friendly GR(1) synthesis (2019). CoRR abs\/1902.05629. http:\/\/arxiv.org\/abs\/1902.05629","DOI":"10.1007\/978-3-030-17465-1_13"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Maoz, S., Ringert, J.O.: Gr (1) synthesis for LTL specification patterns. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pp. 96\u2013106 (2015)","DOI":"10.1145\/2786805.2786824"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Maoz, S., Ringert, J.O.: On well-separation of gr (1) specifications. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 362\u2013372 (2016)","DOI":"10.1145\/2950290.2950300"},{"issue":"5","key":"13_CR22","doi-asserted-by":"publisher","first-page":"1553","DOI":"10.1007\/s10270-021-00868-z","volume":"20","author":"S Maoz","year":"2021","unstructured":"Maoz, S., Ringert, J.O.: Spectra: a specification language for reactive systems. Softw. Syst. Model. 20(5), 1553\u20131586 (2021)","journal-title":"Softw. Syst. Model."},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Maoz, S., Sa\u2019ar, Y.: Aspectltl: an aspect language for LTL specifications. In: Proceedings of the tenth international conference on Aspect-oriented software development, pp. 19\u201330 (2011)","DOI":"10.1145\/1960275.1960280"},{"key":"13_CR24","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":"13_CR25","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Ryzhyk, L., Walker, A.: Developing a practical reactive synthesis tool: experience and lessons learned. arXiv preprint arXiv:1611.07624 (2016)","DOI":"10.4204\/EPTCS.229.8"},{"key":"13_CR27","unstructured":"Somenzi, F.: Cudd: Cu decision diagram package release 2.3. 0. University of Colorado at Boulder 621 (1998)"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Yatskan, R., Shevrin, I., Maoz, S.: Performance heuristics for gr (1) realizability checking and related analyses. In: Gurfinkel, A., Heule, M. (eds.) TACAS 2025. LNCS, vol. 15696, pp. 40\u201359. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-90643-5_3","DOI":"10.1007\/978-3-031-90643-5_3"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26204-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T17:51:21Z","timestamp":1783014681000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_13","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":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","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":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}