{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T11:28:49Z","timestamp":1790681329095,"version":"4.1.0"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030452308","type":"print"},{"value":"9783030452315","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study <jats:italic>k<\/jats:italic>-synchronizability: a system is <jats:italic>k<\/jats:italic>-synchronizable if any of its executions, up to reordering causally independent actions, can be divided into a succession of <jats:italic>k<\/jats:italic>-bounded interaction phases. We show two results (both for mailbox and peer-to-peer automata): first, the reachability problem is decidable for <jats:italic>k<\/jats:italic>-synchronizable systems; second, the membership problem (whether a given system is <jats:italic>k<\/jats:italic>-synchronizable) is decidable as well. Our proofs fix several important issues in previous attempts to prove these two results for mailbox automata.<\/jats:p>","DOI":"10.1007\/978-3-030-45231-5_9","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"157-176","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["On the k-synchronizability of Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1563-6581","authenticated-orcid":false,"given":"Cinzia","family":"Di Giusto","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3775-6496","authenticated-orcid":false,"given":"Laetitia","family":"Laversa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8505-585X","authenticated-orcid":false,"given":"Etienne","family":"Lozes","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","unstructured":"Akroun, L., Sala\u00fcn, G.: Automated verification of automata communicating via FIFO and bag buffers. Formal Methods in System Design 52(3), 260\u2013276 (2018). https:\/\/doi.org\/10.1007\/s10703-017-0285-8","DOI":"10.1007\/s10703-017-0285-8"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Basu, S., Bultan, T.: On deciding synchronizability for asynchronously communicating systems. Theor. Comput. Sci. 656, 60\u201375 (2016). https:\/\/doi.org\/10.1016\/j.tcs.2016.09.023","DOI":"10.1016\/j.tcs.2016.09.023"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Basu, S., Bultan, T., Ouederni, M.: Synchronizability for verification of asynchronously communicating systems. In: Kuncak, V., Rybalchenko, A. (eds.) Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7148, pp. 56\u201371. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-27940-9_5","DOI":"10.1007\/978-3-642-27940-9_5"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Enea, C., Ji, K., Qadeer, S.: On the completeness of verifying message passing programs under bounded asynchrony. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10982, pp. 372\u2013391. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_23","DOI":"10.1007\/978-3-319-96142-2_23"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings. Lecture Notes in Computer Science, vol. 3114, pp. 372\u2013386. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_29","DOI":"10.1007\/978-3-540-27813-9_29"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Chaouch-Saad, M., Charron-Bost, B., Merz, S.: A reduction theorem for the verification of round-based distributed algorithms. In: Bournez, O., Potapov, I. (eds.) Reachability Problems, 3rd International Workshop, RP 2009, Palaiseau, France, September 23-25, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5797, pp. 93\u2013106. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-04420-5_10","DOI":"10.1007\/978-3-642-04420-5_10"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Chou, C., Gafni, E.: Understanding and verifying distributed algorithms using stratified decomposition. In: Dolev, D. (ed.) Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing, Toronto, Ontario, Canada, August 15-17, 1988. pp. 44\u201365. ACM (1988). https:\/\/doi.org\/10.1145\/62546.62556","DOI":"10.1145\/62546.62556"},{"key":"9_CR8","doi-asserted-by":"publisher","unstructured":"Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program. 2(3), 155\u2013173 (1982). https:\/\/doi.org\/10.1016\/0167-6423(83)90013-8.","DOI":"10.1016\/0167-6423(83)90013-8."},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Finkel, A., Lozes, \u00c9.: Synchronizability of communicating finite state machines is not decidable. In: Chatzigiannakis, I., Indyk, P., Kuhn, F., Muscholl, A. (eds.) 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland. LIPIcs, vol. 80, pp. 122:1\u2013122:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2017.122, http:\/\/www.dagstuhl.de\/dagpub\/978-3-95977-041-5","DOI":"10.4230\/LIPIcs.ICALP.2017.122"},{"key":"9_CR10","unstructured":"Genest, B., Kuske, D., Muscholl, A.: On communicating automata with bounded channels. Fundam. Inform. 80(1-3), 147\u2013167 (2007), http:\/\/content.iospress.com\/articles\/fundamenta-informaticae\/fi80-1-3-09"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"von Gleissenthall, K., Kici, R.G., Bakst, A., Stefan, D., Jhala, R.: Pretend synchrony: synchronous verification of asynchronous distributed programs. PACMPL 3(POPL), 59:1\u201359:30 (2019). https:\/\/doi.org\/10.1145\/3290372","DOI":"10.1145\/3290372"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Kragl, B., Qadeer, S., Henzinger, T.A.: Synchronizing the asynchronous. In: Schewe, S., Zhang, L. (eds.) 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China. LIPIcs, vol. 118, pp. 21:1\u201321:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.21","DOI":"10.4230\/LIPIcs.CONCUR.2018.21"},{"key":"9_CR13","doi-asserted-by":"publisher","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Context-bounded analysis of concurrent queue systems. 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. Lecture Notes in Computer Science, vol. 4963, pp. 299\u2013314. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_21","DOI":"10.1007\/978-3-540-78800-3_21"},{"key":"9_CR14","doi-asserted-by":"publisher","unstructured":"Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Commun. ACM 18(12), 717\u2013721 (1975). https:\/\/doi.org\/10.1145\/361227.361234","DOI":"10.1145\/361227.361234"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Muscholl, A.: Analysis of communicating automata. In: Dediu, A., Fernau, H., Mart\u00edn-Vide, C. (eds.) Language and Automata Theory and Applications, 4th International Conference, LATA 2010, Trier, Germany, May 24-28, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6031, pp. 50\u201357. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-13089-2_4","DOI":"10.1007\/978-3-642-13089-2_4"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45231-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,7]],"date-time":"2021-01-07T13:33:53Z","timestamp":1610026433000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45231-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452308","9783030452315"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45231-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"98","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}