{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,10]],"date-time":"2026-09-10T23:14:35Z","timestamp":1789082075692,"version":"build-2803163510"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,7,18]],"date-time":"2022-07-18T00:00:00Z","timestamp":1658102400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,7,18]],"date-time":"2022-07-18T00:00:00Z","timestamp":1658102400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["683300"],"award-info":[{"award-number":["683300"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["683300"],"award-info":[{"award-number":["683300"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792669"],"award-info":[{"award-number":["389792669"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792669"],"award-info":[{"award-number":["389792669"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2023,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Reactive synthesis is the task of automatically deriving a correct implementation from a specification. It is a promising technique for the development of verified programs and hardware. Despite recent advances in terms of algorithms and tools, however, reactive synthesis is still not practical when the specified systems reach a certain bound in size and complexity. In this paper, we present a sound and complete modular synthesis algorithm that automatically decomposes the specification into smaller subspecifications. For them, independent synthesis tasks are performed, significantly reducing the complexity of the individual tasks. Our decomposition algorithm guarantees that the subspecifications are independent in the sense that completely separate synthesis tasks can be performed for them. Moreover, the composition of the resulting implementations is guaranteed to satisfy the original specification. Our algorithm is a preprocessing technique that can be applied to a wide range of synthesis tools. We evaluate our approach with state-of-the-art synthesis tools on established benchmarks: the runtime decreases significantly when synthesizing implementations modularly.<\/jats:p>","DOI":"10.1007\/s11334-022-00462-6","type":"journal-article","created":{"date-parts":[[2022,7,18]],"date-time":"2022-07-18T21:02:37Z","timestamp":1658178157000},"page":"339-357","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Specification decomposition for reactive synthesis"],"prefix":"10.1007","volume":"19","author":[{"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gideon","family":"Geier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7781-043X","authenticated-orcid":false,"given":"Noemi","family":"Passing","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,7,18]]},"reference":[{"key":"462_CR1","unstructured":"Biere A, Heljanko K, Wieringa S (2011) AIGER 1.9 And Beyond. Tech. Rep. 11\/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria"},{"key":"462_CR2","doi-asserted-by":"publisher","unstructured":"Bloem R, Chatterjee K, Jacobs S, K\u00f6nighofer R (2015) Assume-guarantee synthesis for concurrent reactive programs with partial information. In: Baier C, Tinelli C (eds) Tools and algorithms for the construction and analysis of systems\u201421st international conference, TACAS 2015, Held as Part of the European joint conferences on theory and practice of software, ETAPS 2015. Proceedings, Lecture notes in computer science, vol 9035. Springer, Berlin, pp 517\u2013532. https:\/\/doi.org\/10.1007\/978-3-662-46681-0_50","DOI":"10.1007\/978-3-662-46681-0_50"},{"key":"462_CR3","doi-asserted-by":"publisher","unstructured":"Chatterjee K, Henzinger TA (2007) Assume-guarantee synthesis. In: Grumberg O, Huth M (eds) Tools and algorithms for the construction and analysis of systems, 13th international conference, TACAS 2007, held as part of the joint European conferences on theory and practice of software, ETAPS 2007. Proceedings, Lecture notes in computer science, vol 4424. Springer, Berlin, pp 261\u2013275. https:\/\/doi.org\/10.1007\/978-3-540-71209-1_21","DOI":"10.1007\/978-3-540-71209-1_21"},{"key":"462_CR4","doi-asserted-by":"publisher","unstructured":"Clarke EM, Long DE, McMillan KL (1989) Compositional model checking. In: Proceedings of the fourth annual symposium on logic in computer science, LICS 1989. IEEE Computer Society, pp 353\u2013362. https:\/\/doi.org\/10.1109\/LICS.1989.39190","DOI":"10.1109\/LICS.1989.39190"},{"key":"462_CR5","doi-asserted-by":"publisher","unstructured":"Damm W, Finkbeiner B (2011) Does it pay to extend the perimeter of a world model? In: Butler MJ, Schulte W (eds) Formal methods\u201417th international symposium on formal methods, FM 2011. Proceedings, lecture notes in computer science, vol 6664. Springer, Berlin, pp 12\u201326. https:\/\/doi.org\/10.1007\/978-3-642-21437-0_4","DOI":"10.1007\/978-3-642-21437-0_4"},{"key":"462_CR6","doi-asserted-by":"publisher","unstructured":"de\u00a0Roever WP, Langmaack H, Pnueli A (eds) (1998) Compositionality: the significant difference, COMPOS 1997, Lecture notes in computer science, vol 1536. Springer, Berlin. https:\/\/doi.org\/10.1007\/3-540-49213-5","DOI":"10.1007\/3-540-49213-5"},{"key":"462_CR7","doi-asserted-by":"publisher","unstructured":"Dureja R, Rozier KY (2018) More scalable LTL model checking via discovering design-space dependencies ($${D}^3$$). In: Beyer D, Huisman M (eds) Tools and algorithms for the construction and analysis of systems\u201424th international conference, TACAS 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018. Proceedings, Part I, Lecture notes in computer science, vol 10805. Springer, Berlin, pp 309\u2013327. https:\/\/doi.org\/10.1007\/978-3-319-89960-2_17","DOI":"10.1007\/978-3-319-89960-2_17"},{"key":"462_CR8","doi-asserted-by":"publisher","unstructured":"Duret-Lutz A, Lewkowicz A, Fauchille A, Michaud T, Renault E, Xu L (2016) Spot 2.0\u2014A framework for LTL and $$\\omega $$-automata manipulation. In: Artho C, Legay A, Peled D (eds) Automated technology for verification and analysis\u201414th international symposium, ATVA 2016. Proceedings, Lecture notes in computer science, vol 9938, pp 122\u2013129. https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"462_CR9","doi-asserted-by":"publisher","unstructured":"Ehlers R (2011) Unbeast: Symbolic bounded synthesis. In: Tools and algorithms for the construction and analysis of systems\u201417th international conference, TACAS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011. Proceedings, Lecture notes in computer science, vol 6605. Springer, Berlin, pp 272\u2013275. https:\/\/doi.org\/10.1007\/978-3-642-19835-9_25","DOI":"10.1007\/978-3-642-19835-9_25"},{"key":"462_CR10","doi-asserted-by":"publisher","unstructured":"Faymonville P, Finkbeiner B, Tentrup L (2017) BoSy: an experimentation framework for bounded synthesis. In: Majumdar R, Kuncak V (eds) Computer aided verification\u201429th international conference, CAV 2017. Proceedings, Part II, Lecture notes in computer science, vol 10427. Springer, Berlin, pp 325\u2013332. https:\/\/doi.org\/10.1007\/978-3-319-63390-9_17","DOI":"10.1007\/978-3-319-63390-9_17"},{"key":"462_CR11","doi-asserted-by":"publisher","unstructured":"Filiot E, Jin N, Raskin J (2010) Compositional algorithms for LTL synthesis. In: Bouajjani A, Chin W (eds) Automated technology for verification and analysis\u20148th international symposium, ATVA 2010. Proceedings, Lecture notes in computer science, vol 6252. Springer, Berlin, pp 112\u2013127. https:\/\/doi.org\/10.1007\/978-3-642-15643-4_10","DOI":"10.1007\/978-3-642-15643-4_10"},{"key":"462_CR12","doi-asserted-by":"publisher","unstructured":"Finkbeiner B (2016) 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. IOS Press, pp 72\u201398. https:\/\/doi.org\/10.3233\/978-1-61499-627-9-72","DOI":"10.3233\/978-1-61499-627-9-72"},{"key":"462_CR13","doi-asserted-by":"crossref","unstructured":"Finkbeiner B, Geier G, Passing N (2021) Specification decomposition for reactive synthesis. In: NASA Formal Methods, NFM 2021. Proceedings","DOI":"10.1007\/978-3-030-76384-8_8"},{"key":"462_CR14","doi-asserted-by":"publisher","unstructured":"Finkbeiner B, Passing N (2020) Dependency-based compositional synthesis. In: Hung DV, Sokolsky O (eds) Automated technology for verification and analysis\u201418th international symposium, ATVA 2020. Proceedings, Lecture notes in computer science, vol 12302. Springer, Berlin, pp 447\u2013463. https:\/\/doi.org\/10.1007\/978-3-030-59152-6_25","DOI":"10.1007\/978-3-030-59152-6_25"},{"key":"462_CR15","doi-asserted-by":"publisher","unstructured":"Finkbeiner B, Passing N (2021) Compositional synthesis of modular systems. In: Hou Z, Ganesh V (eds) Automated technology for verification and analysis\u201419th international symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18\u201322, 2021, Proceedings, Lecture notes in computer science, vol 12971. Springer, Berlin, pp 303\u2013319. https:\/\/doi.org\/10.1007\/978-3-030-88885-5_20","DOI":"10.1007\/978-3-030-88885-5_20"},{"key":"462_CR16","doi-asserted-by":"publisher","unstructured":"Geier G, Heim P, Klein F, Finkbeiner B (2019) Syntroids: synthesizing a game for fpgas using temporal logic specifications. In: Barrett CW, Yang J (eds) 2019 formal methods in computer aided design, FMCAD 2019. Proceedings. IEEE, pp 138\u2013146. https:\/\/doi.org\/10.23919\/FMCAD.2019.8894261","DOI":"10.23919\/FMCAD.2019.8894261"},{"key":"462_CR17","unstructured":"Giannakopoulou D, Pressburger T, Mavridou A, Rhein J, Schumann J, Shi N (2020) Formal requirements elicitation with FRET. In: Sabetzadeh M, Vogelsang A, Abualhaija S, Borg M, Dalpiaz F, Daneva M, Condori-Fern\u00e1ndez N, Franch X, Fucci D, Gervasi V, Groen EC, Guizzardi RSS, Herrmann A, Horkoff J, Mich L, Perini A, Susi A (eds) Joint Proceedings of REFSQ-2020 Workshops, Doctoral Symposium, Live Studies Track, and Poster Track co-located with the 26th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2020), Pisa, Italy, March 24, 2020, CEUR Workshop Proceedings, vol 2584. CEUR-WS.org. http:\/\/ceur-ws.org\/Vol-2584\/PT-paper4.pdf"},{"key":"462_CR18","doi-asserted-by":"publisher","unstructured":"Jacobs S, Bloem R (2016) The reactive synthesis competition: SYNTCOMP 2016 and beyond. In: Piskac R, Dimitrova R (eds) Fifth workshop on synthesis, SYNT@CAV 2016. Proceedings, EPTCS, vol 229, pp 133\u2013148. https:\/\/doi.org\/10.4204\/EPTCS.229.11","DOI":"10.4204\/EPTCS.229.11"},{"key":"462_CR19","unstructured":"Jacobs S, Bloem R, Colange M, Faymonville P, Finkbeiner B, Khalimov A, Klein F, Luttenberger M, Meyer PJ, Michaud T, Sakr M, Sickert S, Tentrup L, Walker A (2019) The 5th reactive synthesis competition (SYNTCOMP 2018): Benchmarks, Participants & Results. CoRR arXiv:1904.07736"},{"key":"462_CR20","doi-asserted-by":"publisher","unstructured":"Jacobs S, Klein F, Schirmer S (2016) A high-level LTL synthesis format: TLSF v1.1. In: Piskac R, Dimitrova R (eds) Fifth workshop on synthesis, SYNT@CAV 2016. Proceedings, EPTCS, vol 229, pp 112\u2013132. https:\/\/doi.org\/10.4204\/EPTCS.229.10","DOI":"10.4204\/EPTCS.229.10"},{"key":"462_CR21","doi-asserted-by":"crossref","unstructured":"Jobstmann B (2007) Applications and optimizations for LTL synthesis. Ph.D. thesis, Graz University of Technology","DOI":"10.1109\/FMCAD.2006.22"},{"key":"462_CR22","doi-asserted-by":"publisher","unstructured":"Kupferman O, Piterman N, Vardi MY (2006) Safraless compositional synthesis. In: Ball T, Jones RB (eds) Computer aided verification, 18th international conference, CAV 2006. Proceedings, Lecture notes in computer science, vol 4144. Springer, Berlin, pp 31\u201344. https:\/\/doi.org\/10.1007\/11817963_6","DOI":"10.1007\/11817963_6"},{"key":"462_CR23","doi-asserted-by":"crossref","unstructured":"Kupferman O, Vardi MY (2005) Safraless decision procedures. In: 46th annual IEEE symposium on foundations of computer science (FOCS). Proceedings. IEEE Computer Society, pp 531\u2013542 (2005)","DOI":"10.1109\/SFCS.2005.66"},{"issue":"11","key":"462_CR24","doi-asserted-by":"publisher","first-page":"3215","DOI":"10.1109\/TCAD.2020.3012641","volume":"39","author":"R Majumdar","year":"2020","unstructured":"Majumdar R, Mallik K, Schmuck A, Zufferey D (2020) Assume-guarantee distributed synthesis. IEEE Trans Comput Aided Des Integr Circuits Syst 39(11):3215\u20133226. https:\/\/doi.org\/10.1109\/TCAD.2020.3012641","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"key":"462_CR25","doi-asserted-by":"publisher","unstructured":"Mavridou A, Katis A, Giannakopoulou D, Kooi D, Pressburger T, Whalen MW (2021) From partial to global assume-guarantee contracts: compositional realizability analysis in FRET. In: Huisman M, Pasareanu CS, Zhan N (eds) Formal methods\u201424th international symposium, FM 2021, virtual event, November 20\u201326, 2021, Proceedings, Lecture notes in computer science, vol 13047. Springer, Berlin, pp 503\u2013523 (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_27","DOI":"10.1007\/978-3-030-90870-6_27"},{"key":"462_CR26","doi-asserted-by":"publisher","unstructured":"Meyer PJ, Sickert S, Luttenberger M (2018) Strix: explicit reactive synthesis strikes back! In: Chockler H, Weissenbacher G (eds) Computer aided verification\u201430th international conference, CAV 2018, held as part of the federated logic conference, FloC 2018. Proceedings, Part I, Lecture notes in computer science, vol 10981. Springer, Berlin, pp 578\u2013586 (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"462_CR27","unstructured":"Michaud T, Colange M (2018) Reactive synthesis from LTL specification with Spot. In: 7th workshop on synthesis, SYNT@CAV. https:\/\/www.lrde.epita.fr\/dload\/papers\/michaud.18.synt.pdf"},{"key":"462_CR28","unstructured":"P\u00e9rez GA (2019) The extended HOA format for synthesis. CoRR arXiv:1912.05793"},{"key":"462_CR29","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Annual symposium on foundations of computer science. IEEE Computer Society, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"462_CR30","doi-asserted-by":"publisher","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Conference record of the sixteenth annual ACM symposium on principles of programming languages. ACM Press, pp 179\u2013190. https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"462_CR31","unstructured":"Renkin F, Duret-Lutz A, Schlehuber P, Pommellet A (2021) Improvements to ltlsynt. In: 10th workshop on synthesis, SYNT@CAV. https:\/\/www.lrde.epita.fr\/~frenkin\/publications\/syntcomp21.pdf"},{"issue":"5\u20136","key":"462_CR32","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/s10009-012-0224-3","volume":"15","author":"S Sohail","year":"2013","unstructured":"Sohail S, Somenzi F (2013) Safety first: a two-stage algorithm for the synthesis of reactive systems. Int J Softw Tools Technol Transf 15(5\u20136):433\u2013454. https:\/\/doi.org\/10.1007\/s10009-012-0224-3","journal-title":"Int J Softw Tools Technol Transf"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-022-00462-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-022-00462-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-022-00462-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,29]],"date-time":"2024-09-29T10:14:14Z","timestamp":1727604854000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-022-00462-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,18]]},"references-count":32,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,12]]}},"alternative-id":["462"],"URL":"https:\/\/doi.org\/10.1007\/s11334-022-00462-6","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,7,18]]},"assertion":[{"value":"16 November 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 June 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 July 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}