{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T02:38:00Z","timestamp":1774579080782,"version":"3.50.1"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100010665","name":"H2020 Marie Sklodowska-Curie Actions","doi-asserted-by":"publisher","award":["778233"],"award-info":[{"award-number":["778233"]}],"id":[{"id":"10.13039\/100010665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2021,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study the relationship between session types and behavioural contracts, representing Communicating Finite State Machines (CFSMs), under the assumption that processes communicate asynchronously. Session types represent a syntax-based approach for the description of communication protocols, while behavioural contracts, formally expressing CFSMs, follow an operational approach. We show the existence of a fully abstract interpretation of session types into a fragment of contracts that maps session subtyping into binary compliance-preserving CFSMs\/behavioural contract refinement. In this way, on the one hand, we enrich the theory of session types with an operational characterization and, on the other hand, we use recent undecidability results for asynchronous session subtyping to obtain an original undecidability result for asynchronous CFSMs\/behavioural contract refinement.\n<\/jats:p>","DOI":"10.1007\/s10270-020-00838-x","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T05:03:07Z","timestamp":1609736587000},"page":"311-333","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Asynchronous session subtyping as communicating automata refinement"],"prefix":"10.1007","volume":"20","author":[{"given":"Mario","family":"Bravetti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gianluigi","family":"Zavattaro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"838_CR1","doi-asserted-by":"crossref","unstructured":"Aldini, A., Bravetti, M., Pierro, A.D., Gorrieri, R., Hankin, C., Wiklicky, H.: Two formal approaches for approximating noninterference properties. In: Foundations of Security Analysis and Design II, FOSAD 2001\/2002 Tutorial Lectures, volume 2946 of Lecture Notes in Computer Science, pp. 1\u201343. Springer (2004)","DOI":"10.1007\/978-3-540-24631-2_1"},{"issue":"2\u20133","key":"838_CR2","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1561\/2500000031","volume":"3","author":"D Ancona","year":"2016","unstructured":"Ancona, D., Bono, V., Bravetti, M., Campos, J., Castagna, G., Deni\u00e9lou, P., Gay, S.J., Gesbert, N., Giachino, E., Hu, R., Johnsen, E.B., Martins, F., Mascardi, V., Montesi, F., Neykova, R., Ng, N., Padovani, L., Vasconcelos, V.T., Yoshida, N.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2\u20133), 95\u2013230 (2016)","journal-title":"Found. Trends Program. Lang."},{"issue":"6","key":"838_CR3","doi-asserted-by":"publisher","first-page":"1057","DOI":"10.1017\/S0960129508007111","volume":"18","author":"JCM Baeten","year":"2008","unstructured":"Baeten, J.C.M., Bravetti, M.: A ground-complete axiomatisation of finite-state processes in a generic process algebra. Math. Struct. Comput. Sci. 18(6), 1057\u20131089 (2008)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"6","key":"838_CR4","doi-asserted-by":"publisher","first-page":"1339","DOI":"10.1017\/S096012951400005X","volume":"25","author":"F Barbanera","year":"2015","unstructured":"Barbanera, F., de\u2019Liguoro, U.: Sub-behaviour relations for session-based client\/server systems. Math. Struct. Comput. Sci. 25(6), 1339\u20131381 (2015)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"3","key":"838_CR5","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1017\/S0960129514000243","volume":"26","author":"GT Bernardi","year":"2016","unstructured":"Bernardi, G.T., Hennessy, M.: Modelling session types using contracts. Math. Struct. Comput. Sci. 26(3), 510\u2013560 (2016)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"2","key":"838_CR6","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323\u2013342 (1983)","journal-title":"J. ACM"},{"key":"838_CR7","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.jlamp.2018.01.002","volume":"96","author":"M Bravetti","year":"2018","unstructured":"Bravetti, M.: Reduction semantics in markovian process algebra. J. Log. Algebr. Meth. Program. 96, 41\u201364 (2018)","journal-title":"J. Log. Algebr. Meth. Program."},{"key":"838_CR8","unstructured":"Bravetti, M., Carbone, M., Lange, J., Yoshida, N., Zavattaro, G.: A sound algorithm for asynchronous session subtyping. In: Proceedings of 30th International Conference Concurrency Theory, CONCUR\u201919, volume 140 of Leibniz International Proceedings in Informatics, pp. 38:1\u201338:16. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"838_CR9","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1016\/j.ic.2017.07.010","volume":"256","author":"M Bravetti","year":"2017","unstructured":"Bravetti, M., Carbone, M., Zavattaro, G.: Undecidability of asynchronous session subtyping. Inf. Comput. 256, 300\u2013320 (2017)","journal-title":"Inf. Comput."},{"key":"838_CR10","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.tcs.2018.02.010","volume":"722","author":"M Bravetti","year":"2018","unstructured":"Bravetti, M., Carbone, M., Zavattaro, G.: On the boundary between decidability and undecidability of asynchronous session subtyping. Theor. Comput. Sci. 722, 19\u201351 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"838_CR11","doi-asserted-by":"crossref","unstructured":"Bravetti, M., Lanese, I., Zavattaro, G.: Contract-driven implementation of choreographies. In: Proceedings of 4th International Symposium on Trustworthy Global Computing TGC 2008, volume 5474 of Lecture Notes in Computer Science, pp. 1\u201318. Springer (2009)","DOI":"10.1007\/978-3-642-00945-7_1"},{"key":"838_CR12","doi-asserted-by":"crossref","unstructured":"Bravetti, M., Zavattaro, G.: Contract based multi-party service composition. In: Proceedings of International Symposium on Fundamentals of Software Engineering, FSEN\u201907, volume 4767 of Lecture Notes in Computer Science, pp. 207\u2013222. Springer (2007)","DOI":"10.1007\/978-3-540-75698-9_14"},{"key":"838_CR13","doi-asserted-by":"crossref","unstructured":"Bravetti, M., Zavattaro, G.: Towards a unifying theory for choreography conformance and contract compliance. In: Proceedings of 6th International Symposium Software Composition, SC\u201907, volume 4829 of Lecture Notes in Computer Science, pp. 34\u201350. Springer (2007)","DOI":"10.1007\/978-3-540-77351-1_4"},{"key":"838_CR14","doi-asserted-by":"crossref","unstructured":"Bravetti, M., Zavattaro, G.: Contract compliance and choreography conformance in the presence of message queues. In: Proceedings of 5th International Workshop on Web Services and Formal Methods, WS-FM\u201908, volume 5387 of Lecture Notes in Computer Science, pp. 37\u201354. Springer (2008)","DOI":"10.1007\/978-3-642-01364-5_3"},{"key":"838_CR15","doi-asserted-by":"crossref","unstructured":"Bravetti, M., Zavattaro, G.: Contract-based discovery and composition of web services. In: Formal Methods for Web Services, 9th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2009, Bertinoro, Italy, June 1-6, 2009, Advanced Lectures, volume 5569 of Lecture Notes in Computer Science, pp. 261\u2013295. Springer (2009)","DOI":"10.1007\/978-3-642-01918-0_7"},{"issue":"3","key":"838_CR16","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1017\/S0960129509007683","volume":"19","author":"M Bravetti","year":"2009","unstructured":"Bravetti, M., Zavattaro, G.: On the expressive power of process interruption and compensation. Math. Struct. Comput. Sci. 19(3), 565\u2013599 (2009)","journal-title":"Math. Struct. Comput. Sci."},{"key":"838_CR17","doi-asserted-by":"crossref","unstructured":"Bravetti, M., Zavattaro, G.: Foundations of coordination and contracts and their contribution to session type theory. In: Proceedings of 20th IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2018, volume 10852 of Lecture Notes in Computer Science, pp. 21\u201350. Springer (2018)","DOI":"10.1007\/978-3-319-92408-3_2"},{"key":"838_CR18","doi-asserted-by":"crossref","unstructured":"Bravetti, M., Zavattaro, G.: Relating session types and behavioural contracts: The asynchronous case. In: Proceedings of 17th International Conference on Software Engineering and Formal Methods, SEFM 2019, volume 11724 of Lecture Notes in Computer Science, pp. 29\u201347. Springer (2019)","DOI":"10.1007\/978-3-030-30446-1_2"},{"key":"838_CR19","doi-asserted-by":"publisher","first-page":"100527","DOI":"10.1016\/j.jlamp.2020.100527","volume":"112","author":"M Bravetti","year":"2020","unstructured":"Bravetti, M., Zavattaro, G.: Process calculi as a tool for studying coordination, contracts and session types. J. Log. Algebraic Methods Program. 112, 100527 (2020)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"838_CR20","doi-asserted-by":"crossref","unstructured":"Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. In: Proceedings of 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL\u201908, pp. 261\u2013272. ACM (2008)","DOI":"10.1145\/1328438.1328471"},{"issue":"2","key":"838_CR21","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1016\/j.ic.2005.05.006","volume":"202","author":"G C\u00e9c\u00e9","year":"2005","unstructured":"C\u00e9c\u00e9, G., Finkel, A.: Verification of programs with half-duplex communication. Inf. Comput. 202(2), 166\u2013190 (2005)","journal-title":"Inf. Comput."},{"issue":"2","key":"838_CR22","first-page":"56","volume":"13","author":"T Chen","year":"2017","unstructured":"Chen, T., Dezani-Ciancaglini, M., Scalas, A., Yoshida, N.: On the preciseness of subtyping in session types. Log. Methods Comput. Sci. 13(2), 56 (2017)","journal-title":"Log. Methods Comput. Sci."},{"issue":"3","key":"838_CR23","doi-asserted-by":"publisher","first-page":"197","DOI":"10.3233\/FI-2018-1663","volume":"159","author":"FS de Boer","year":"2018","unstructured":"de Boer, F.S., Bravetti, M., Lee, M.D., Zavattaro, G.: A petri net based modeling of active objects and futures. Fundam. Inform. 159(3), 197\u2013256 (2018)","journal-title":"Fundam. Inform."},{"key":"838_CR24","unstructured":"Deni\u00e9lou, P., Yoshida, N.: Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M.Z., Peleg, D. (eds.) Automata, Languages, and Programming-40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pp. 174\u2013186. Springer, (2013)"},{"key":"838_CR25","unstructured":"Gay, S.J.: Subtyping supports safe session substitution. In: Lindley, S., McBride, C., Trinder, P.W., Sannella, D. (eds.) A List of Successes That Can Change the World-Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, volume 9600 of Lecture Notes in Computer Science, pp. 95\u2013108. Springer, (2016)"},{"issue":"2\u20133","key":"838_CR26","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s00236-005-0177-z","volume":"42","author":"SJ Gay","year":"2005","unstructured":"Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Inf. 42(2\u20133), 191\u2013225 (2005)","journal-title":"Acta Inf."},{"key":"838_CR27","doi-asserted-by":"crossref","unstructured":"Gay, S.J., Thiemann, P., Vasconcelos, V.T.: Duality of session types: The final cut. In: Balzer, S., Padovani, L. (eds.) Proceedings of the 12th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES@ETAPS 2020, Dublin, Ireland, 26th April 2020, volume 314 of EPTCS, pp. 23\u201333 (2020)","DOI":"10.4204\/EPTCS.314.0"},{"key":"838_CR28","doi-asserted-by":"crossref","unstructured":"Hu, R., Yoshida, N.: Hybrid session verification through endpoint API generation. In: Proceedings of 19th International Conference on Fundamental Approaches to Software Engineering FASE 2016, volume 9633 of Lecture Notes in Computer Science, pp. 401\u2013418. Springer (2016)","DOI":"10.1007\/978-3-662-49665-7_24"},{"key":"838_CR29","doi-asserted-by":"crossref","unstructured":"Laneve, C., Padovani, L.: The Must preorder revisited. In: Proceedings of 18th International Conference Concurrency Theory, CONCUR\u201907, volume 4703 of Lecture Notes in Computer Science, pp. 212\u2013225. Springer (2007)","DOI":"10.1007\/978-3-540-74407-8_15"},{"key":"838_CR30","doi-asserted-by":"crossref","unstructured":"Lange, J., Yoshida, N.: On the undecidability of asynchronous session subtyping. In: Proceedings of 20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS\u201917, volume 10203 of Lecture Notes in Computer Science, pp. 441\u2013457 (2017)","DOI":"10.1007\/978-3-662-54458-7_26"},{"key":"838_CR31","doi-asserted-by":"crossref","unstructured":"Lindley, S., Morris, J.G.: Embedding session types in Haskell. In: Proceedings of 9th International Symposium on Haskell, Haskell\u201916, pp. 133\u2013145 (2016)","DOI":"10.1145\/2976002.2976018"},{"key":"838_CR32","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, London (1989)"},{"issue":"1","key":"838_CR33","first-page":"83","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. I\/II. Inf. Comput. 100(1), 83 (1992)","journal-title":"Inf. Comput."},{"key":"838_CR34","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.ic.2015.02.002","volume":"241","author":"D Mostrous","year":"2015","unstructured":"Mostrous, D., Yoshida, N.: Session typing and asynchronous subtyping for the higher-order $$\\pi $$-calculus. Inf. Comput. 241, 227\u2013263 (2015)","journal-title":"Inf. Comput."},{"key":"838_CR35","doi-asserted-by":"crossref","unstructured":"Mostrous, D., Yoshida, N., Honda, K.: Global principal typing in partially commutative asynchronous sessions. In: Proceedings of 18th European Symposium on Programming, ESOP\u201909, volume 5502 of Lecture Notes in Computer Science, pp. 316\u2013332. Springer (2009)","DOI":"10.1007\/978-3-642-00590-9_23"},{"key":"838_CR36","doi-asserted-by":"crossref","unstructured":"Neykova, R., Hu, R., Yoshida, N., Abdeljallal, F.: A Session Type Provider: Compile-time API Generation for Distributed Protocols with Interaction Refinements in F$$\\sharp $$. In: Proceedings of 27th International Conference on Compiler Construction, CC 2018. ACM (2018)","DOI":"10.1145\/3178372.3179495"},{"key":"838_CR37","doi-asserted-by":"crossref","unstructured":"Orchard, D.A., Yoshida, N.: Effects as sessions, sessions as effects. In: Proceedings of 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 568\u2013581 (2016)","DOI":"10.1145\/2837614.2837634"},{"key":"838_CR38","doi-asserted-by":"publisher","first-page":"e4","DOI":"10.1017\/S0956796816000289","volume":"27","author":"L Padovani","year":"2017","unstructured":"Padovani, L.: A simple library implementation of binary sessions. J. Funct. Program. 27, e4 (2017)","journal-title":"J. Funct. Program."},{"key":"838_CR39","unstructured":"Scalas, A., Yoshida, N.: Lightweight session programming in scala. In: Proceedings of 30th European Conference on Object-Oriented Programming, ECOOP 2016, volume\u00a056 of LIPIcs, pp. 21:1\u201321:28. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2016)"},{"key":"838_CR40","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.jlamp.2018.01.001","volume":"97","author":"A Scalas","year":"2018","unstructured":"Scalas, A., Yoshida, N.: Multiparty session types, beyond duality. J. Log. Algebr. Methods Program. 97, 55\u201384 (2018)","journal-title":"J. Log. Algebr. Methods Program."}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00838-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-020-00838-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00838-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,10]],"date-time":"2021-04-10T06:10:37Z","timestamp":1618035037000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-020-00838-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,4]]}},"alternative-id":["838"],"URL":"https:\/\/doi.org\/10.1007\/s10270-020-00838-x","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"27 February 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 July 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 October 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 January 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}