{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,18]],"date-time":"2026-07-18T16:32:00Z","timestamp":1784392320436,"version":"3.55.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656323","type":"print"},{"value":"9783031656330","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Information flow guided synthesis is a compositional approach to the automated construction of distributed systems where the assumptions between the components are captured as information-flow requirements. Information-flow requirements are hyperproperties that ensure that if a component needs to act on certain information that is only available in other components, then this information will be passed to the component. We present a new method for the automatic construction of information flow assumptions from specifications given as temporal safety properties. The new method is the first approach to handle situations where the required amount of information is unbounded. For example, we can analyze communication protocols that transmit a stream of messages in a potentially infinite loop. We show that component implementations can then, in principle, be constructed from the information flow requirements using a synthesis tool for hyperproperties. We additionally present a more practical synthesis technique that constructs the components using efficient methods for standard synthesis from trace properties. We have implemented the technique in the prototype tool <jats:sc>FlowSy<\/jats:sc>, which outperforms previous approaches to distributed synthesis on several benchmarks.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_4","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"64-86","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Information Flow Guided Synthesis with\u00a0Unbounded Communication"],"prefix":"10.1007","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-0003-3184-6335","authenticated-orcid":false,"given":"Niklas","family":"Metzger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5549-1781","authenticated-orcid":false,"given":"Yoram","family":"Moses","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-031-57246-3_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Akshay","year":"2024","unstructured":"Akshay, S., Basa, E., Chakraborty, S., Fried, D.: On dependent variables in reactive synthesis. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) ETAPS 2024, pp. 123\u2013143. Springer Nature Switzerland, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_8"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-41540-6_14","volume-title":"Computer Aided Verification","author":"R Alur","year":"2016","unstructured":"Alur, R., Moarref, S., Topcu, U.: Compositional synthesis of reactive controllers for multi-agent systems. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 251\u2013269. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_14"},{"key":"4_CR3","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. (2011). https:\/\/doi.org\/10.1145\/2000799.2000800","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-662-46681-0_50","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Bloem","year":"2015","unstructured":"Bloem, R., Chatterjee, K., Jacobs, S., K\u00f6nighofer, R.: Assume-guarantee synthesis for concurrent reactive programs with partial information. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 517\u2013532. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_50"},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1007\/978-3-319-10575-8_27","volume-title":"Handbook of Model Checking","author":"R Bloem","year":"2018","unstructured":"Bloem, R., Chatterjee, K., Jobstmann, B.: Graph games and reactive synthesis. In: Handbook of Model Checking, pp. 921\u2013962. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_27"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-540-71209-1_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Chatterjee","year":"2007","unstructured":"Chatterjee, K., Henzinger, T.A.: Assume-guarantee synthesis. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 261\u2013275. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_21"},{"key":"4_CR7","unstructured":"Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. In: Summaries of the Summer Institute of Symbolic Logic, vol.\u00a01, pp. 3\u201350. Cornell University, Ithaca, NY (1957)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-54792-8_15","volume-title":"Principles of Security and Trust","author":"MR Clarkson","year":"2014","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265\u2013284. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15"},{"key":"4_CR9","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-319-06410-9_13","volume-title":"FM 2014: Formal Methods","author":"W Damm","year":"2014","unstructured":"Damm, W., Finkbeiner, B.: Automatic compositional synthesis of distributed systems. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 179\u2013193. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_13"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"d\u2019Amorim, Marcelo, Ro\u015fu, Grigore: Efficient Monitoring of \u03c9-Languages. In: Etessami, Kousha, Rajamani, Sriram K.. (eds.) CAV 2005. LNCS, vol. 3576, pp. 364\u2013378. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_36","DOI":"10.1007\/11513988_36"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-319-89960-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Dijk","year":"2018","unstructured":"Dijk, T.: Oink: an implementation and evaluation of modern parity game solvers. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 291\u2013308. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_16"},{"key":"4_CR13","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-031-13188-2_9","volume-title":"Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7\u201310, 2022, Proceedings, Part II","author":"A Duret-Lutz","year":"2022","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, August 7\u201310, 2022, Proceedings, Part II, pp. 174\u2013187. Springer International Publishing, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-15643-4_10","volume-title":"Automated Technology for Verification and Analysis","author":"E Filiot","year":"2010","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: Compositional algorithms for LTL synthesis. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 112\u2013127. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15643-4_10"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: LICS (2005)","DOI":"10.1007\/11562948_21"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-319-96145-3_16","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2018","unstructured":"Finkbeiner, B., Hahn, C., Lukert, P., Stenger, M., Tentrup, L.: Synthesizing reactive systems from hyperproperties. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 289\u2013306. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_16"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Metzger, N., Moses, Y.: Information flow guided synthesis. In: Shoham, S., Vizel, Y. (eds.) CAV 2022, Proceedings, Part II (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_25","DOI":"10.1007\/978-3-031-13188-2_25"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-030-59152-6_25","volume-title":"Automated Technology for Verification and Analysis","author":"B Finkbeiner","year":"2020","unstructured":"Finkbeiner, B., Passing, N.: Dependency-based compositional synthesis. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 447\u2013463. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_25"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-030-88885-5_20","volume-title":"Automated Technology for Verification and Analysis","author":"B Finkbeiner","year":"2021","unstructured":"Finkbeiner, B., Passing, N.: Compositional synthesis of modular systems. In: Hou, Z., Ganesh, V. (eds.) ATVA 2021. LNCS, vol. 12971, pp. 303\u2013319. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88885-5_20"},{"issue":"5\u20136","key":"4_CR20","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transfer 15(5\u20136), 519\u2013539 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0228-z","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"3","key":"4_CR21","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/s10703-008-0064-7","volume":"34","author":"P Gastin","year":"2009","unstructured":"Gastin, P., Sznajder, N., Zeitoun, M.: Distributed synthesis for well-connected architectures. Formal Methods Syst. Des. 34(3), 215\u2013237 (2009)","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-030-31784-3_22","volume-title":"Automated Technology for Verification and Analysis","author":"J Hecking-Harbusch","year":"2019","unstructured":"Hecking-Harbusch, J., Metzger, N.O.: Efficient trace encodings of bounded synthesis for asynchronous distributed systems. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 369\u2013386. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_22"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Jacobs, S., et al.: The reactive synthesis competition (SYNTCOMP): 2018-2021. CoRR (2022). https:\/\/doi.org\/10.48550\/ARXIV.2206.00251","DOI":"10.48550\/ARXIV.2206.00251"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-00768-2_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Kugler","year":"2009","unstructured":"Kugler, H., Segall, I.: Compositional synthesis of reactive systems from live sequence chart specifications. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 77\u201391. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_9"},{"key":"4_CR25","unstructured":"Kupferman, O., Vardi, M.Y.: Synthesizing distributed systems. In: Logic in Computer Science (LICS) (2001)"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11817963_6","volume-title":"Computer Aided Verification","author":"O Kupferman","year":"2006","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 31\u201344. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_6"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/3-540-48224-5_33","volume-title":"Automata, Languages and Programming","author":"P Madhusudan","year":"2001","unstructured":"Madhusudan, P., Thiagarajan, P.S.: Distributed controller synthesis for local specifications. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 396\u2013407. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-48224-5_33"},{"key":"4_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-45694-5_11","volume-title":"CONCUR 2002 \u2014 Concurrency Theory","author":"P Madhusudan","year":"2002","unstructured":"Madhusudan, P., Thiagarajan, P.S.: A decidable class of asynchronous distributed controllers. In: Brim, L., K\u0159et\u00ednsk\u00fd, M., Ku\u010dera, A., Jan\u010dar, P. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 145\u2013160. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45694-5_11"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Majumdar, R., Mallik, K., Schmuck, A., Zufferey, D.: Assume-guarantee distributed synthesis. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. (2020). https:\/\/doi.org\/10.1109\/TCAD.2020.3012641","DOI":"10.1109\/TCAD.2020.3012641"},{"issue":"1","key":"4_CR30","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z Manna","year":"1984","unstructured":"Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. TOPLAS 6(1), 68\u201393 (1984)","journal-title":"TOPLAS"},{"key":"4_CR31","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 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: Distributed Reactive Systems Are Hard to Synthesize. In: 31st Annual Symposium on Foundations of Computer Science, St. Louis, Missouri, USA, October 22-24, 1990, Volume II. pp. 746\u2013757. IEEE Computer Society (1990). https:\/\/doi.org\/10.1109\/FSCS.1990.89597","DOI":"10.1109\/FSCS.1990.89597"},{"issue":"1","key":"4_CR33","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1142\/S0129054107004590","volume":"18","author":"S Schewe","year":"2007","unstructured":"Schewe, S., Finkbeiner, B.: Semi-automatic distributed synthesis. Int. J. Found. Comput. Sci. 18(1), 113\u2013138 (2007)","journal-title":"Int. J. Found. 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-65633-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:40Z","timestamp":1721891020000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","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":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}