{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T21:15:47Z","timestamp":1783545347994,"version":"3.55.0"},"publisher-location":"Cham","reference-count":60,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262196","type":"print"},{"value":"9783032262202","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Team automata were introduced as a flexible extension of I\/O automata to model collaborative behaviour in component-based and distributed systems. Their distinctive features include multi-party communication and a liberal synchronisation mechanism: components may jointly execute shared actions according to synchronisation policies that specify which subsets of components participate as senders or receivers. While this makes team automata well suited for modelling coordination, existing communication is synchronous and therefore insufficient for capturing certain behavioural aspects (e.g., due to message reordering) of modern networks and distributed systems, in which communication is typically asynchronous and message delays are unpredictable.<\/jats:p>\n                  <jats:p>In this paper, we introduce asynchronous team automata (ATeams), which extend team automata\u00a0with buffers to model asynchronous communication, in addition to conventional synchronous interaction. ATeams support individual interactions involving multiple senders and receivers, unlike well-known asynchronous models such as communicating finite-state machines and multi-party session types. We formalise the syntax and operational semantics of ATeams, study well-formedness and well-behavedness conditions, and present the prototypical  tool that supports specification, animation and automated checks. This proposes ATeams as a unifying semantic foundation for modelling and analysis of heterogeneous synchronous\u2013asynchronous multi-party interactions.<\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_2","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:22:37Z","timestamp":1779024157000},"page":"27-49","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Asynchronous Team Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7196-6609","authenticated-orcid":false,"given":"Davide","family":"Basile","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2930-6367","authenticated-orcid":false,"given":"Maurice H.","family":"ter Beek","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0971-8919","authenticated-orcid":false,"given":"Jos\u00e9","family":"Proen\u00e7a","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Aceto, L., Cimini, M., Ing\u00f3lfsd\u00f3ttir, A., Reynisson, A.H., Sigurdarson, S.H., Sirjani, M.: Modelling and simulation of asynchronous real-time systems using timed Rebeca. In: Mousavi, M.R., Ravara, A. (eds.) Proceedings of the 10th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA 2011). EPTCS, vol. 58, pp. 1\u201319 (2011). https:\/\/doi.org\/10.4204\/EPTCS.58.1","DOI":"10.4204\/EPTCS.58.1"},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of the 8th European Software Engineering Conference held jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC\/FSE 2001), pp. 109\u2013120. ACM (2001). https:\/\/doi.org\/10.1145\/503209.503226","DOI":"10.1145\/503209.503226"},{"issue":"3","key":"2_CR3","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1017\/S0960129504004153","volume":"14","author":"F Arbab","year":"2004","unstructured":"Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(3), 329\u2013366 (2004). https:\/\/doi.org\/10.1017\/S0960129504004153","journal-title":"Math. Struct. Comput. Sci."},{"key":"2_CR4","unstructured":"Armstrong, J., Virding, R., Williams, M.: Concurrent Programming in Erlang. Prentice Hall, 2 edn. (1996)"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Attie, P.C., Bensalem, S., Bozga, M., Jaber, M., Sifakis, J., Zaraket, F.A.: Global and local deadlock freedom in BIP. ACM Trans. Softw. Eng. Methodol. 26(3), 9:1\u20139:48 (2018). https:\/\/doi.org\/10.1145\/3152910","DOI":"10.1145\/3152910"},{"key":"2_CR6","doi-asserted-by":"publisher","unstructured":"Barbanera, F., Hennicker, R.: Safe composition of systems of communicating finite state machines. In: Aubert, C., Di\u00a0Giusto, C., Fowler, S., Ka\u00a0I\u00a0Pun, V. (eds.) Proceedings of the 17th Interaction and Concurrency Experience (ICE 2024). EPTCS, vol.\u00a0414, pp. 39\u201357 (2024). https:\/\/doi.org\/10.4204\/EPTCS.414.3","DOI":"10.4204\/EPTCS.414.3"},{"key":"2_CR7","doi-asserted-by":"publisher","unstructured":"Barbanera, F., Lanese, I., Tuosto, E.: Choreography automata. In: Bliudze, S., Bocchi, L. (eds.) COORDINATION 2020. LNCS, vol. 12134, pp. 86\u2013106. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50029-0_6","DOI":"10.1007\/978-3-030-50029-0_6"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Barbanera, F., Lanese, I., Tuosto, E.: A Theory of Formal Choreographic Languages. Log. Meth. Comp. Sci. 19(3), 9:1\u20139:36 (2023). https:\/\/doi.org\/10.46298\/LMCS-19(3:9)2023","DOI":"10.46298\/lmcs-19(3:9)2023"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Bartoletti, M., Cimoli, T., Zunino, R.: Compliance in behavioural contracts: a brief survey. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Programming Languages with Applications to Biology and Security. LNCS, vol. 9465, pp. 103\u2013121. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25527-9_9","DOI":"10.1007\/978-3-319-25527-9_9"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Basile, D., ter Beek, M.H., Degano, P., Legay, A., Ferrari, G.L., Gnesi, S., Di Giandomenico, F.: Controller synthesis of service contracts with variability. Sci. Comput. Program. 187 (2020). https:\/\/doi.org\/10.1016\/j.scico.2019.102344","DOI":"10.1016\/j.scico.2019.102344"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Basile, D., Degano, P., Ferrari, G.L.: Automata for specifying and orchestrating service contracts. Log. Meth. Comp. Sci. 12(4:6), 1\u201351 (2016). https:\/\/doi.org\/10.2168\/LMCS-12(4:6)2016","DOI":"10.2168\/LMCS-12(4:6)2016"},{"key":"2_CR12","doi-asserted-by":"publisher","unstructured":"Basile, D., Degano, P., Ferrari, G., Tuosto, E.: From orchestration to choreography through contract automata. In: Lanese, I., Lluch\u00a0Lafuente, A., Sokolova, A., Torres\u00a0Vieira, H. (eds.) Proceedings of the 7th Interaction and Concurrency Experience (ICE 2014). EPTCS, vol.\u00a0166, pp. 67\u201385 (2014). https:\/\/doi.org\/10.4204\/EPTCS.166.8","DOI":"10.4204\/EPTCS.166.8"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: Proceedings of the 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006), pp. 3\u201312. IEEE (2006). https:\/\/doi.org\/10.1109\/SEFM.2006.27","DOI":"10.1109\/SEFM.2006.27"},{"key":"2_CR14","doi-asserted-by":"publisher","unstructured":"Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On weak modal compatibility, refinement, and the MIO workbench. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 175\u2013189. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_15","DOI":"10.1007\/978-3-642-12002-2_15"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Carmona, J., Hennicker, R., Kleijn, J.: Communication requirements for team automata. In: Jacquet, J.-M., Massink, M. (eds.) COORDINATION 2017. LNCS, vol. 10319, pp. 256\u2013277. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-59746-1_14","DOI":"10.1007\/978-3-319-59746-1_14"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Carmona, J., Kleijn, J.: Conditions for compatibility of components: The case of masters and slaves. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 784\u2013805. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_55","DOI":"10.1007\/978-3-319-47166-2_55"},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Cledou, G., Hennicker, R., Proen\u00e7a, J.: Featured team automata. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 483\u2013502. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_26","DOI":"10.1007\/978-3-030-90870-6_26"},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Cledou, G., Hennicker, R., Proen\u00e7a, J.: Can we communicate? Using dynamic logic to verify team automata. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 122\u2013141. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_9","DOI":"10.1007\/978-3-031-27481-7_9"},{"issue":"1","key":"2_CR19","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1023\/A:1022407907596","volume":"12","author":"MH ter Beek","year":"2003","unstructured":"ter Beek, M.H., Ellis, C.A., Kleijn, J., Rozenberg, G.: Synchronizations in team automata for groupware systems. Comput. Sup. Coop. Work 12(1), 21\u201369 (2003). https:\/\/doi.org\/10.1023\/A:1022407907596","journal-title":"Comput. Sup. Coop. Work"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Hennicker, R., Kleijn, J.: Compositionality of safe communication in systems of team automata. In: Pun, V.K.I., Stolz, V., Simao, A. (eds.) ICTAC 2020. LNCS, vol. 12545, pp. 200\u2013220. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64276-1_11","DOI":"10.1007\/978-3-030-64276-1_11"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-030-50029-0_5","volume-title":"Coordination Models and Languages","author":"MH ter Beek","year":"2020","unstructured":"ter Beek, M.H., Hennicker, R., Kleijn, J.: Team automata@work: on safe communication. In: Bliudze, S., Bocchi, L. (eds.) COORDINATION 2020. LNCS, vol. 12134, pp. 77\u201385. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50029-0_5"},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Hennicker, R., Proen\u00e7a, J.: Realisability of global models of interaction. In: \u00c1brah\u00e1m, E., Dubslaff, C., Tapia Tarifa, S.L. (eds.) ICTAC 2023. LNCS, vol. 14446, pp. 236\u2013255. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-47963-2_15","DOI":"10.1007\/978-3-031-47963-2_15"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Hennicker, R., Proen\u00e7a, J.: Team automata: overview and roadmap. In: Castellani, I., Tiezzi, F. (eds.) COORDINATION 2024. LNCS, vol. 14676, pp. 161\u2013198. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-62697-5_10","DOI":"10.1007\/978-3-031-62697-5_10"},{"issue":"5","key":"2_CR24","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1016\/j.ipl.2005.05.012","volume":"95","author":"MH ter Beek","year":"2005","unstructured":"ter Beek, M.H., Kleijn, J.: Modularity for teams of I\/O automata. Inf. Process. Lett. 95(5), 487\u2013495 (2005). https:\/\/doi.org\/10.1016\/j.ipl.2005.05.012","journal-title":"Inf. Process. Lett."},{"key":"2_CR25","doi-asserted-by":"publisher","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"2_CR26","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2009.06.002","volume":"241","author":"A Bejleri","year":"2008","unstructured":"Bejleri, A., Yoshida, N.: Synchronous multiparty session types. Electr. Notes Theor. Comput. Sci. 241, 3\u201333 (2008). https:\/\/doi.org\/10.1016\/j.entcs.2009.06.002","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"10","key":"2_CR27","doi-asserted-by":"publisher","first-page":"1315","DOI":"10.1109\/TC.2008.26","volume":"57","author":"S Bliudze","year":"2008","unstructured":"Bliudze, S., Sifakis, J.: The algebra of connectors: structuring interaction in BIP. IEEE Trans. Comput. 57(10), 1315\u20131330 (2008). https:\/\/doi.org\/10.1109\/TC.2008.26","journal-title":"IEEE Trans. Comput."},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Bordeaux, L., Sala\u00fcn, G., Berardi, D., Mecella, M.: When are two web services compatible? In: Shan, M.-C., Dayal, U., Hsu, M. (eds.) TES 2004. LNCS, vol. 3324, pp. 15\u201328. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31811-8_2","DOI":"10.1007\/978-3-540-31811-8_2"},{"issue":"2","key":"2_CR29","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). https:\/\/doi.org\/10.1145\/322374.322380","journal-title":"J. ACM"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Brim, L., \u010cern\u00e1, I., Va\u0159ekov\u00e1, P., Zimmerov\u00e1, B.: Component-interaction automata as a verification-oriented component-based system specification. ACM Softw. Eng. Notes 31(2), (2006). https:\/\/doi.org\/10.1145\/1118537.1123063","DOI":"10.1145\/1118537.1123063"},{"key":"2_CR31","doi-asserted-by":"publisher","unstructured":"Carmona, J., Cortadella, J.: Input\/output compatibility of reactive systems. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 360\u2013377. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36126-X_22","DOI":"10.1007\/3-540-36126-X_22"},{"key":"2_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2013.03.006","volume":"484","author":"J Carmona","year":"2013","unstructured":"Carmona, J., Kleijn, J.: Compatibility in a multi-component environment. Theor. Comput. Sci. 484, 1\u201315 (2013). https:\/\/doi.org\/10.1016\/j.tcs.2013.03.006","journal-title":"Theor. Comput. Sci."},{"key":"2_CR33","doi-asserted-by":"publisher","unstructured":"Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. ACM Trans. Program. Lang. Syst. 31(5), 19:1\u201319:61 (2009). https:\/\/doi.org\/10.1145\/1538917.1538920","DOI":"10.1145\/1538917.1538920"},{"key":"2_CR34","doi-asserted-by":"publisher","unstructured":"Clemente, L., Herbreteau, F., Sutre, G.: Decidable topologies for communicating automata with FIFO and bag channels. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 281\u2013296. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44584-6_20","DOI":"10.1007\/978-3-662-44584-6_20"},{"key":"2_CR35","doi-asserted-by":"publisher","unstructured":"Deni\u00e9lou, P.-M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 194\u2013213. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_10","DOI":"10.1007\/978-3-642-28869-2_10"},{"issue":"7\u20138","key":"2_CR36","doi-asserted-by":"publisher","first-page":"870","DOI":"10.1016\/j.scico.2011.03.009","volume":"77","author":"F Dur\u00e1n","year":"2012","unstructured":"Dur\u00e1n, F., Ouederni, M., Sala\u00fcn, G.: A generic framework for $$n$$-protocol compatibility checking. Sci. Comput. Program. 77(7\u20138), 870\u2013886 (2012). https:\/\/doi.org\/10.1016\/j.scico.2011.03.009","journal-title":"Sci. Comput. Program."},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Edixhoven, L., Jongmans, S.S., Proen\u00e7a, J., Castellani, I.: Branching pomsets: design, expressiveness and applications to choreographies. J. Log. Algebr. Methods Program 136, (2024). https:\/\/doi.org\/10.1016\/j.jlamp.2023.100919","DOI":"10.1016\/j.jlamp.2023.100919"},{"key":"2_CR38","doi-asserted-by":"publisher","unstructured":"Ellis, C.S.: Team automata for groupware systems. In: Proceedings of the International ACM SIGGROUP Conference on Supporting Group Work: The Integration Challenge (GROUP 1997), pp. 415\u2013424. ACM (1997). https:\/\/doi.org\/10.1145\/266838.267363","DOI":"10.1145\/266838.267363"},{"key":"2_CR39","doi-asserted-by":"publisher","unstructured":"Ghassemi, F., Sirjani, M., Khamespanah, E., Mirani, M., Hojjat, H.: Transparent actor model. In: Proceedings of the 11th International Conference on Formal Methods in Software Engineering (FormaliSE 2023). pp. 97\u2013107. IEEE (2023). https:\/\/doi.org\/10.1109\/FORMALISE58978.2023.00018","DOI":"10.1109\/FORMALISE58978.2023.00018"},{"key":"2_CR40","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/j.scico.2004.05.014","volume":"55","author":"G G\u00f6ssler","year":"2005","unstructured":"G\u00f6ssler, G., Sifakis, J.: Composition for component-based modeling. Sci. Comput. Program. 55, 161\u2013183 (2005). https:\/\/doi.org\/10.1016\/j.scico.2004.05.014","journal-title":"Sci. Comput. Program."},{"key":"2_CR41","doi-asserted-by":"publisher","unstructured":"Haller, P.: On the integration of the actor model in mainstream technologies: the Scala perspective. In: Agha, G.A., Bordini, R.H., Marron, A., Ricci, A. (eds.) Proceedings of the 2nd edition on Programming systems, languages and applications based on actors, agents, and decentralized control abstractions (AGERE! 2012). pp. 1\u20136. ACM (2012). https:\/\/doi.org\/10.1145\/2414639.2414641","DOI":"10.1145\/2414639.2414641"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Hennicker, R., Bidoit, M.: Compatibility properties of synchronously and asynchronously communicating components. Log. Meth. Comp. Sci. 14(1), 1\u201331 (2018). https:\/\/doi.org\/10.23638\/LMCS-14(1:1)2018","DOI":"10.23638\/LMCS-14(1:1)2018"},{"key":"2_CR43","doi-asserted-by":"publisher","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008), pp. 273\u2013284. ACM (2008). https:\/\/doi.org\/10.1145\/1328438.1328472","DOI":"10.1145\/1328438.1328472"},{"issue":"3","key":"2_CR44","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/S10270-021-00877-Y","volume":"20","author":"I Jahandideh","year":"2021","unstructured":"Jahandideh, I., Ghassemi, F., Sirjani, M.: An actor-based framework for asynchronous event-based cyber-physical systems. Softw. Syst. Model. 20(3), 641\u2013665 (2021). https:\/\/doi.org\/10.1007\/S10270-021-00877-Y","journal-title":"Softw. Syst. Model."},{"key":"2_CR45","doi-asserted-by":"publisher","unstructured":"Ji, Z., Wang, S., Xu, X.: Session types with multiple senders single receiver. In: Hermanns, H., Sun, J., Bu, L. (eds.) SETTA 2023. LNCS, vol. 14464, pp. 112\u2013131. Springer (2023). https:\/\/doi.org\/10.1007\/978-981-99-8664-4_7","DOI":"10.1007\/978-981-99-8664-4_7"},{"key":"2_CR46","doi-asserted-by":"publisher","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: A core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142\u2013164. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25271-6_8","DOI":"10.1007\/978-3-642-25271-6_8"},{"issue":"1","key":"2_CR47","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/S10270-006-0011-2","volume":"6","author":"EB Johnsen","year":"2007","unstructured":"Johnsen, E.B., Owe, O.: An asynchronous communication model for distributed concurrent objects. Softw. Syst. Model. 6(1), 39\u201358 (2007). https:\/\/doi.org\/10.1007\/S10270-006-0011-2","journal-title":"Softw. Syst. Model."},{"key":"2_CR48","doi-asserted-by":"publisher","unstructured":"Jongmans, S., Proen\u00e7a, J.: ST4MP: A blueprint of multiparty session typing for multilingual programming. In: Margaria, T., Steffen, B. (eds.) ISoLA 2022. LNCS, vol. 13701, pp. 460\u2013478. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-19849-6_26","DOI":"10.1007\/978-3-031-19849-6_26"},{"key":"2_CR49","unstructured":"Jonsson, B.: Compositional Verification of Distributed Systems. Ph.D. thesis, Uppsala University (1987)"},{"key":"2_CR50","doi-asserted-by":"publisher","unstructured":"Koehler, C., Clarke, D.: Decomposing port automata. In: Shin, S.Y., Ossowski, S. (eds.) Proceedings of the 24th ACM Symposium on Applied Computing (SAC 2009), pp. 1369\u20131373. ACM (2009). https:\/\/doi.org\/10.1145\/1529282.1529587","DOI":"10.1145\/1529282.1529587"},{"key":"2_CR51","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Nyman, U., W\u0105sowski, A.: Modal I\/O automata for interface and product line theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64\u201379. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_6","DOI":"10.1007\/978-3-540-71316-6_6"},{"key":"2_CR52","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann (1996)"},{"key":"2_CR53","doi-asserted-by":"crossref","unstructured":"Lynch, N.A., Tuttle, M.R.: An Introduction to Input\/Output Automata. CWI Q. 2(3), 219\u2013246 (1989), https:\/\/ir.cwi.nl\/pub\/18164, reprinted in ACM Form. Asp. Comput. (2026). https:\/\/doi.org\/10.1145\/3788687","DOI":"10.1145\/3788687"},{"key":"2_CR54","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall (1989)"},{"key":"2_CR55","doi-asserted-by":"publisher","unstructured":"Oheimb, D.: Interacting state machines: a stateful approach to proving security. In: Abdallah, A.E., Ryan, P., Schneider, S. (eds.) FASec 2002. LNCS, vol. 2629, pp. 15\u201332. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-40981-6_4","DOI":"10.1007\/978-3-540-40981-6_4"},{"key":"2_CR56","doi-asserted-by":"publisher","unstructured":"Pal, S., Guanciale, R., Lanese, I., Tuosto, E., Clo, M.: Pomsets for process management: A healthcare case study. In: Liu, Z., Saoud, A., Wehrheim, H. (eds.) ICTAC 2025. LNCS, vol. 16237, pp. 378\u2013395. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-032-11176-0_22","DOI":"10.1007\/978-3-032-11176-0_22"},{"key":"2_CR57","doi-asserted-by":"publisher","unstructured":"Proen\u00e7a, J., Edixhoven, L.: Caos: a reusable Scala web animator of operational semantics. In: Jongmans, S.S., Lopes, A. (eds.) COORDINATION 2023. LNCS, vol. 13908, pp. 163\u2013171. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-35361-1_9","DOI":"10.1007\/978-3-031-35361-1_9"},{"issue":"3","key":"2_CR58","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s002360100070","volume":"38","author":"A Rensink","year":"2001","unstructured":"Rensink, A., Wehrheim, H.: Process algebra with action dependencies. Acta Inform. 38(3), 155\u2013234 (2001). https:\/\/doi.org\/10.1007\/s002360100070","journal-title":"Acta Inform."},{"key":"2_CR59","doi-asserted-by":"crossref","unstructured":"Scalas, A., Yoshida, N.: Less is more: multiparty session types revisited. Proc. ACM Program. Lang. 3, 30:1\u201330:29 (2019). https:\/\/doi.org\/10.1145\/3290343","DOI":"10.1145\/3290343"},{"issue":"1\u20133","key":"2_CR60","doi-asserted-by":"publisher","first-page":"267","DOI":"10.3233\/FI-2019-1863","volume":"170","author":"P Severi","year":"2019","unstructured":"Severi, P., Dezani-Ciancaglini, M.: Observational equivalence for multiparty sessions. Fundam. Inform. 170(1\u20133), 267\u2013305 (2019). https:\/\/doi.org\/10.3233\/FI-2019-1863","journal-title":"Fundam. Inform."}],"updated-by":[{"DOI":"10.1007\/978-3-032-26220-2_36","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T00:00:00Z","timestamp":1783555200000}}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26220-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:30:26Z","timestamp":1783542626000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"9 July 2026","order":2,"name":"change_date","label":"Change Date","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Correction","order":3,"name":"change_type","label":"Change Type","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"A correction has been published.","order":4,"name":"change_details","label":"Change Details","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}