{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T10:04:21Z","timestamp":1781172261314,"version":"3.54.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030719944","type":"print"},{"value":"9783030719951","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Session types are widely used as abstractions of asynchronous message passing systems. Refinement for such abstractions is crucial as it allows improvements of a given component without compromising its compatibility with the rest of the system. In the context of session types, the most general notion of refinement is the asynchronous session subtyping, which allows to anticipate message emissions but only under certain conditions. In particular, asynchronous session subtyping rules out candidates subtypes that occur naturally in communication protocols where, e.g., two parties simultaneously send each other a finite but unspecified amount of messages before removing them from their respective buffers. To address this shortcoming, we study fair compliance over asynchronous session types and fair refinement as the relation that preserves it. This allows us to propose a novel variant of session subtyping that leverages the notion of controllability from service contract theory and that is a sound characterisation of fair refinement. In addition, we show that both fair refinement and our novel subtyping are undecidable. We also present a sound algorithm, and its implementation, which deals with examples that feature potentially unbounded buffering.<\/jats:p>","DOI":"10.1007\/978-3-030-71995-1_8","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:03:39Z","timestamp":1616432619000},"page":"144-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Fair Refinement for Asynchronous Session Types"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5193-2914","authenticated-orcid":false,"given":"Mario","family":"Bravetti","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9697-1378","authenticated-orcid":false,"given":"Julien","family":"Lange","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3313-6409","authenticated-orcid":false,"given":"Gianluigi","family":"Zavattaro","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"8_CR1","unstructured":"Adam Wiggins. The Twelve Factor methodology. https:\/\/12factor.net, 2017."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"F.\u00a0Barbanera and U.\u00a0de\u2019Liguoro. Two notions of sub-behaviour for session-based client\/server systems. In Proc. of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP\u201910, pages 155\u2013164. ACM, 2010.","DOI":"10.1145\/1836089.1836109"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"G.\u00a0T. Bernardi and M.\u00a0Hennessy. Modelling session types using contracts. Mathematical Structures in Computer Science, 26(3):510\u2013560, 2016.","DOI":"10.1017\/S0960129514000243"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"A.\u00a0Bouajjani, C.\u00a0Enea, K.\u00a0Ji, and S.\u00a0Qadeer. On the completeness of verifying message passing programs under bounded asynchrony. In CAV (2), volume 10982 of Lecture Notes in Computer Science, pages 372\u2013391. Springer, 2018.","DOI":"10.1007\/978-3-319-96142-2_23"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"D.\u00a0Brand and P.\u00a0Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323\u2013342, 1983.","DOI":"10.1145\/322374.322380"},{"key":"8_CR6","unstructured":"M.\u00a0Bravetti, M.\u00a0Carbone, J.\u00a0Lange, N.\u00a0Yoshida, and G.\u00a0Zavattaro. A sound algorithm for asynchronous session subtyping. In CONCUR, volume 140 of LIPIcs, pages 38:1\u201338:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2019."},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"M.\u00a0Bravetti, M.\u00a0Carbone, and G.\u00a0Zavattaro. Undecidability of asynchronous session subtyping. Inf. Comput., 256:300\u2013320, 2017.","DOI":"10.1016\/j.ic.2017.07.010"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"M.\u00a0Bravetti, M.\u00a0Carbone, and G.\u00a0Zavattaro. On the boundary between decidability and undecidability of asynchronous session subtyping. Theor. Comput. Sci., 722:19\u201351, 2018.","DOI":"10.1016\/j.tcs.2018.02.010"},{"key":"8_CR9","unstructured":"M.\u00a0Bravetti, J.\u00a0Lange, and G.\u00a0Zavattaro. Fair refinement for asynchronous session types (extended version). CoRR abs\/2101.08181, 2021."},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"M.\u00a0Bravetti and G.\u00a0Zavattaro. Contract Compliance and Choreography Conformance in the Presence of Message Queues. In WS-FM\u201908, volume 5387 of Lecture Notes in Computer Science, pages 37\u201354. Springer, 2008.","DOI":"10.1007\/978-3-642-01364-5_3"},{"key":"8_CR11","unstructured":"M.\u00a0Bravetti and G.\u00a0Zavattaro. A foundational theory of contracts for multi-party service composition. Fundam. Inform., 89(4):451\u2013478, 2008."},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"M.\u00a0Bravetti and G.\u00a0Zavattaro. A theory of contracts for strong service compliance. Math. Struct. Comput. Sci., 19(3):601\u2013638, 2009.","DOI":"10.1017\/S0960129509007658"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"M.\u00a0Bravetti and G.\u00a0Zavattaro. Relating session types and behavioural contracts: The asynchronous case. In SEFM, volume 11724 of Lecture Notes in Computer Science, pages 29\u201347. Springer, 2019.","DOI":"10.1007\/978-3-030-30446-1_2"},{"key":"8_CR14","unstructured":"T.\u00a0Chen, M.\u00a0Dezani-Ciancaglini, A.\u00a0Scalas, and N.\u00a0Yoshida. On the preciseness of subtyping in session types. Logical Methods in Computer Science, 13(2), 2017."},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"T.-C. Chen, M.\u00a0Dezani-Ciancaglini, and N.\u00a0Yoshida. On the preciseness of subtyping in session types. In PPDP 2014, pages 146\u2013135. ACM Press, 2014.","DOI":"10.1145\/2643135.2643138"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"P.\u00a0Deni\u00e9lou and N.\u00a0Yoshida. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In ICALP 2013, pages 174\u2013186, 2013.","DOI":"10.1007\/978-3-642-39212-2_18"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"S.\u00a0J. Gay and M.\u00a0Hole. Types and subtypes for client-server interactions. In ESOP 1999, pages 74\u201390, 1999.","DOI":"10.1007\/3-540-49099-X_6"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"S.\u00a0J. Gay and M.\u00a0Hole. Subtyping for session types in the pi calculus. Acta Inf., 42(2-3):191\u2013225, 2005.","DOI":"10.1007\/s00236-005-0177-z"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"B.\u00a0Genest, D.\u00a0Kuske, and A.\u00a0Muscholl. A Kleene theorem and model checking algorithms for existentially bounded communicating automata. Inf. Comput., 204(6):920\u2013956, 2006.","DOI":"10.1016\/j.ic.2006.01.005"},{"key":"8_CR20","unstructured":"B.\u00a0Genest, D.\u00a0Kuske, and A.\u00a0Muscholl. On communicating automata with bounded channels. Fundam. Inform., 80(1-3):147\u2013167, 2007."},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"K.\u00a0Honda, N.\u00a0Yoshida, and M.\u00a0Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9, 2016.","DOI":"10.1145\/2827695"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"J.\u00a0Lange and N.\u00a0Yoshida. Characteristic formulae for session types. In TACAS, volume 9636 of Lecture Notes in Computer Science, pages 833\u2013850. Springer, 2016.","DOI":"10.1007\/978-3-662-49674-9_52"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"J.\u00a0Lange and N.\u00a0Yoshida. On the undecidability of asynchronous session subtyping. In Proc. of 20th Int. Conference on Foundations of Software Science and Computation Structures, FOSSACS\u201917, volume 10203 of Lecture Notes in Computer Science, pages 441\u2013457, 2017.","DOI":"10.1007\/978-3-662-54458-7_26"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"J.\u00a0Lange and N.\u00a0Yoshida. Verifying asynchronous interactions via communicating session automata. In CAV (1), volume 11561 of Lecture Notes in Computer Science, pages 97\u2013117. Springer, 2019.","DOI":"10.1007\/978-3-030-25540-4_6"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"N.\u00a0Lohmann. Why does my service have no partners? In WS-FM, volume 5387 of Lecture Notes in Computer Science, pages 191\u2013206. Springer, 2008.","DOI":"10.1007\/978-3-642-01364-5_12"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"D.\u00a0Mostrous, N.\u00a0Yoshida, and K.\u00a0Honda. Global principal typing in partially commutative asynchronous sessions. In ESOP, volume 5502 of Lecture Notes in Computer Science, pages 316\u2013332. Springer, 2009.","DOI":"10.1007\/978-3-642-00590-9_23"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"R.\u00a0D. Nicola and M.\u00a0Hennessy. Testing Equivalences for Processes. Theoretical Computer Science, 34:83\u2013133, 1984.","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"L.\u00a0Padovani. Fair subtyping for open session types. In ICALP, volume 7966 of Lecture Notes in Computer Science, pages 373\u2013384. Springer, 2013.","DOI":"10.1007\/978-3-642-39212-2_34"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"L.\u00a0Padovani. Fair subtyping for multi-party session types. Math. Struct. Comput. Sci., 26(3):424\u2013464, 2016.","DOI":"10.1017\/S096012951400022X"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"A.\u00a0Rensink and W.\u00a0Vogler. Fair testing. Inf. Comput., 205(2):125\u2013198, 2007.","DOI":"10.1016\/j.ic.2006.06.002"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"M.\u00a0Bravetti, J.\u00a0Lange, and G.\u00a0Zavattaro. Fair refinement for asynchronous session types. https:\/\/github.com\/julien-lange\/fair-asynchronous-subtyping, 2020.","DOI":"10.1007\/978-3-030-71995-1_8"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"R.\u00a0van Glabbeek and P.\u00a0H\u00f6fner. Progress, justness, and fairness. ACM Comput. Surv., 52(4):69:1\u201369:38, 2019.","DOI":"10.1145\/3329125"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"D.\u00a0Weinberg. Efficient controllability analysis of open nets. In WS-FM, volume 5387 of Lecture Notes in Computer Science, pages 224\u2013239. Springer, 2008.","DOI":"10.1007\/978-3-642-01364-5_14"}],"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-71995-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,29]],"date-time":"2021-04-29T23:59:45Z","timestamp":1619740785000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-71995-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030719944","9783030719951"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-71995-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","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":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/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":"88","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":"28","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,2","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":"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 changed to an online format due to the COVID-19 pandemic","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)"}}]}}