{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T08:58:16Z","timestamp":1783501096498,"version":"3.55.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T00:00:00Z","timestamp":1648771200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T00:00:00Z","timestamp":1648771200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["TRR 248"],"award-info":[{"award-number":["TRR 248"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660"],"award-info":[{"award-number":["389792660"]}],"id":[{"id":"10.13039\/501100001659","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":["TRR 248"],"award-info":[{"award-number":["TRR 248"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660"],"award-info":[{"award-number":["389792660"]}],"id":[{"id":"10.13039\/501100001659","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"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2022,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In contrast to the breakthroughs in reactive synthesis of monolithic systems, distributed synthesis is not yet practical. Compositional approaches can be a key technique for scalable algorithms. Here, the challenge is to decompose a specification of the global system into local requirements on the individual processes. In this paper, we present and extend a sound and complete compositional synthesis algorithm that constructs for each process, in addition to the strategy, a certificate that captures the necessary interface between the processes. The certificates define an assume-guarantee contract that allows for formulating individual process requirements. By bounding the size of the certificates, we then bias the synthesis procedure towards solutions that are desirable in the sense that they have a small interface. We have implemented our approach and evaluated it on scalable benchmarks: It is much faster than standard methods for distributed synthesis as long as reasonably small certificates exist. Otherwise, the overhead of synthesizing additional certificates is small.<\/jats:p>","DOI":"10.1007\/s11334-022-00450-w","type":"journal-article","created":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T20:48:09Z","timestamp":1648846089000},"page":"455-469","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Compositional synthesis of modular systems"],"prefix":"10.1007","volume":"18","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4280-8441","authenticated-orcid":false,"given":"Bernd","family":"Finkbeiner","sequence":"first","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,4,1]]},"reference":[{"key":"450_CR1","doi-asserted-by":"publisher","unstructured":"Alur R, Moarref S, Topcu U (2015) Pattern-based refinement of assume-guarantee specifications in reactive synthesis. In: Baier C, Tinelli C (eds) Tools and algorithms for the construction and analysis of systems - 21st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, Lecture Notes in Computer Science, vol. 9035, pp. 501\u2013516. Springer. https:\/\/doi.org\/10.1007\/978-3-662-46681-0_49","DOI":"10.1007\/978-3-662-46681-0_49"},{"key":"450_CR2","unstructured":"Baumeister JE (2017) Encodings of bounded synthesis for distributed systems. Bachelor\u2019s thesis, Saarland University"},{"key":"450_CR3","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 Tools and algorithms for the construction and analysis of systems - 21st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, Lecture Notes in Computer Science, vol. 9035, pp 517\u2013532. Springer. https:\/\/doi.org\/10.1007\/978-3-662-46681-0_50","DOI":"10.1007\/978-3-662-46681-0_50"},{"issue":"1","key":"450_CR4","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s00236-016-0273-2","volume":"54","author":"R Brenguier","year":"2017","unstructured":"Brenguier R, Raskin J, Sankur O (2017) Assume-admissible synthesis. Acta Inform 54(1):41\u201383. https:\/\/doi.org\/10.1007\/s00236-016-0273-2","journal-title":"Acta Inform"},{"key":"450_CR5","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 Braga, Portugal, March 24 - April 1, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4424, pp 261\u2013275. Springer. https:\/\/doi.org\/10.1007\/978-3-540-71209-1_21","DOI":"10.1007\/978-3-540-71209-1_21"},{"key":"450_CR6","doi-asserted-by":"publisher","unstructured":"Damm W, Finkbeiner B (2011) Does it pay to extend the perimeter of a world model? In FM 2011: formal methods - 17th international symposium on formal methods, Limerick, Ireland, June 20-24, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6664, pp 12\u201326. Springer. https:\/\/doi.org\/10.1007\/978-3-642-21437-0_4","DOI":"10.1007\/978-3-642-21437-0_4"},{"key":"450_CR7","doi-asserted-by":"publisher","unstructured":"Damm W, Finkbeiner B (2014) Automatic compositional synthesis of distributed systems. In: Jones CB, Pihlajasaari P, Sun J (eds) FM 2014: formal methods - 19th international symposium, Singapore, May 12-16, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8442, pp 179\u2013193. Springer. https:\/\/doi.org\/10.1007\/978-3-319-06410-9_13","DOI":"10.1007\/978-3-319-06410-9_13"},{"key":"450_CR8","doi-asserted-by":"publisher","unstructured":"de\u00a0Roever WP, Langmaack H, Pnueli A (eds) (1998) Compositionality: the significant difference, international symposium, COMPOS\u201997, Bad Malente, Germany, September 8-12, 1997. Revised Lectures, Lecture Notes in Computer Science, vol. 1536. Springer. https:\/\/doi.org\/10.1007\/3-540-49213-5","DOI":"10.1007\/3-540-49213-5"},{"key":"450_CR9","doi-asserted-by":"publisher","unstructured":"Faymonville P, Finkbeiner B, Rabe MN, Tentrup L (2017) Encodings of bounded synthesis. In: Legay A, Margaria T (eds) Tools and algorithms for the construction and analysis of systems - 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I, Lecture Notes in Computer Science, vol. 10205, pp 354\u2013370. https:\/\/doi.org\/10.1007\/978-3-662-54577-5_20","DOI":"10.1007\/978-3-662-54577-5_20"},{"key":"450_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 - 29th international conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, Lecture Notes in Computer Science, vol. 10427, pp 325\u2013332. Springer. https:\/\/doi.org\/10.1007\/978-3-319-63390-9_17","DOI":"10.1007\/978-3-319-63390-9_17"},{"key":"450_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 - 8th international symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6252, pp 112\u2013127. Springer. https:\/\/doi.org\/10.1007\/978-3-642-15643-4_10","DOI":"10.1007\/978-3-642-15643-4_10"},{"key":"450_CR12","doi-asserted-by":"publisher","unstructured":"Finkbeiner B, Geier G, Passing N (2021) Specification decomposition for reactive synthesis. In: Dutle A, Moscato MM, Titolo L, Mu\u00f1oz CA, Perez I (eds) NASA formal methods - 13th international symposium, NFM 2021, virtual event, May 24-28, 2021, Proceedings, Lecture Notes in Computer Science, vol. 12673, pp 113\u2013130. Springer. https:\/\/doi.org\/10.1007\/978-3-030-76384-8_8","DOI":"10.1007\/978-3-030-76384-8_8"},{"key":"450_CR13","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 - 18th international symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, Lecture Notes in Computer Science, vol. 12302, pp 447\u2013463. Springer. https:\/\/doi.org\/10.1007\/978-3-030-59152-6_25","DOI":"10.1007\/978-3-030-59152-6_25"},{"key":"450_CR14","doi-asserted-by":"crossref","unstructured":"Finkbeiner B, Passing N (2021) Compositional synthesis of modular systems. In: Automated technology for verification and analysis - 19th international symposium, ATVA 2021, Gold Coast, Australia, October 18-22, 2021","DOI":"10.1007\/978-3-030-88885-5_20"},{"key":"450_CR15","doi-asserted-by":"crossref","unstructured":"Finkbeiner B, Passing N (2021) Compositional synthesis of modular systems (Full Version). CoRR arXiv: abs\/2106.14783","DOI":"10.1007\/s11334-022-00450-w"},{"key":"450_CR16","doi-asserted-by":"crossref","unstructured":"Finkbeiner B, Schewe S (2013) Bounded synthesis. STTT pp 519\u2013539","DOI":"10.1007\/s10009-012-0228-z"},{"key":"450_CR17","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:abs\/1904.07736"},{"key":"450_CR18","doi-asserted-by":"publisher","unstructured":"Kugler H, Segall I (2009) Compositional synthesis of reactive systems from live sequence chart specifications. In: Kowalewski S, Philippou A (eds) Tools and algorithms for the construction and analysis of systems, 15th international conference, TACAS 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5505, pp 77\u201391. Springer. https:\/\/doi.org\/10.1007\/978-3-642-00768-2_9","DOI":"10.1007\/978-3-642-00768-2_9"},{"key":"450_CR19","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, Seattle, WA, USA, August 17-20, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4144, pp 31\u201344. Springer. https:\/\/doi.org\/10.1007\/11817963_6","DOI":"10.1007\/11817963_6"},{"key":"450_CR20","doi-asserted-by":"publisher","unstructured":"Kupferman O, Vardi MY (2005) Safraless decision procedures. In: 46th annual IEEE symposium on foundations of computer science (FOCS 2005), 23-25 October 2005, Pittsburgh, PA, USA, Proceedings, pp 531\u2013542. IEEE Computer Society. https:\/\/doi.org\/10.1109\/SFCS.2005.66","DOI":"10.1109\/SFCS.2005.66"},{"issue":"11","key":"450_CR21","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":"450_CR22","doi-asserted-by":"publisher","unstructured":"Pnueli A (1977) 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. https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"450_CR23","doi-asserted-by":"publisher","unstructured":"Safra S (1988) On the complexity of omega-automata. In: 29th annual symposium on foundations of computer science, White Plains, New York, USA, 24-26 October 1988, pp. 319\u2013327. IEEE Computer Society. https:\/\/doi.org\/10.1109\/SFCS.1988.21948","DOI":"10.1109\/SFCS.1988.21948"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-022-00450-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-022-00450-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-022-00450-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,12]],"date-time":"2022-09-12T06:43:50Z","timestamp":1662965030000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-022-00450-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,1]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,9]]}},"alternative-id":["450"],"URL":"https:\/\/doi.org\/10.1007\/s11334-022-00450-w","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,1]]},"assertion":[{"value":"21 October 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 February 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 April 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}