{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T19:27:27Z","timestamp":1783020447041,"version":"3.54.6"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","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>Interaction models describe distributed systems as algebraic terms, with gates marking interaction points between local views. Composing local models into a coherent global one requires aligning these gates while respecting the algebraic laws of interaction operators. This is achieved via anti-unification techniques. We specialize anti-unification (or generalization) via a special constant-preserving variant, which preserves designated constants while generalizing the remaining structure. We develop a dedicated rule-based procedure, for computing these generalizations, prove its termination, soundness, and completeness, extend it modulo equational theories, and integrate it into a standard anti-unification framework. A prototype tool demonstrates the approach\u2019s ability to recompose global interactions from partial views.<\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_23","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:51:22Z","timestamp":1779033082000},"page":"440-460","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Specializing Anti-unification for\u00a0Interaction Models Composition via\u00a0Gate Connections"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-8904-0073","authenticated-orcid":false,"given":"Joel","family":"Nguetoum","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4943-7807","authenticated-orcid":false,"given":"Boutheina","family":"Bannour","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8955-6835","authenticated-orcid":false,"given":"Pascale","family":"Le Gall","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5322-4337","authenticated-orcid":false,"given":"Erwan","family":"Mahe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"23_CR1","unstructured":"Message Sequence Chart (MSC). https:\/\/www.itu.int\/rec\/T-REC-Z.120\/"},{"key":"23_CR2","unstructured":"Unified Modeling Language (UML). https:\/\/www.omg.org\/spec\/UML\/"},{"key":"23_CR3","unstructured":"https:\/\/github.com\/Ermine516\/UnitAU (2020), GitHub repository"},{"key":"23_CR4","unstructured":"https:\/\/github.com\/erwanM974\/hibou_label (2025), GitHub repository"},{"key":"23_CR5","unstructured":"https:\/\/github.com\/maude-lang\/Maude (2025), GitHub repository"},{"key":"23_CR6","doi-asserted-by":"publisher","unstructured":"Alpuente, M., Escobar, S., Meseguer, J., Sapi\u00f1a, J.: Order-sorted equational generalization algorithm revisited. Ann. Math. Artif. Intell. 1\u201324 (2021). https:\/\/doi.org\/10.1007\/s10472-021-09771-1","DOI":"10.1007\/s10472-021-09771-1"},{"key":"23_CR7","doi-asserted-by":"publisher","unstructured":"Alpuente, M., Escobar, S., Meseguer, J., Ojeda, P.: A modular equational generalization algorithm. In: Logic-Based Program Synthesis and Transformation (2009). https:\/\/doi.org\/10.1007\/978-3-642-00515-2_3","DOI":"10.1007\/978-3-642-00515-2_3"},{"key":"23_CR8","doi-asserted-by":"publisher","unstructured":"Alpuente, M., Escobar, S., Espert, J., Meseguer, J.: A modular order-sorted equational generalization algorithm. Inf. Comput. (2014). https:\/\/doi.org\/10.1016\/j.ic.2014.01.006","DOI":"10.1016\/j.ic.2014.01.006"},{"key":"23_CR9","doi-asserted-by":"publisher","unstructured":"Alur, R., Etessami, K., Yannakakis, M.: Inference of message sequence charts. In: Proceedings of the 2000 International Conference on Software Engineering. (ICSE) (2000). https:\/\/doi.org\/10.1145\/337180.337215","DOI":"10.1145\/337180.337215"},{"key":"23_CR10","doi-asserted-by":"publisher","unstructured":"Bader, J., Scott, A., Pradel, M., Chandra, S.: Getafix: learning to fix bugs automatically. Proc. ACM Program. Lang. (2019). https:\/\/doi.org\/10.1145\/3360585","DOI":"10.1145\/3360585"},{"key":"23_CR11","doi-asserted-by":"publisher","unstructured":"Barbanera, F., de\u2019Liguoro, U., Hennicker, R.: Connecting open systems of communicating finite state machines. J. Logical Algebraic Methods Program. (2019). https:\/\/doi.org\/10.1016\/j.jlamp.2019.07.004","DOI":"10.1016\/j.jlamp.2019.07.004"},{"key":"23_CR12","doi-asserted-by":"publisher","unstructured":"Barbanera, F., Dezani-Ciancaglini, M., Gheri, L., Yoshida, N.: Multicompatibility for multiparty-session composition. Assoc. Comput. Mach. (2023). https:\/\/doi.org\/10.1145\/3610612.3610614","DOI":"10.1145\/3610612.3610614"},{"key":"23_CR13","doi-asserted-by":"publisher","unstructured":"Barbanera, F., Dezani-Ciancaglini, M., Lanese, I., Tuosto, E.: Composition and decomposition of multiparty sessions. J. Logical Algebraic Methods Program. (2021). https:\/\/doi.org\/10.1016\/j.jlamp.2020.100620","DOI":"10.1016\/j.jlamp.2020.100620"},{"key":"23_CR14","doi-asserted-by":"publisher","unstructured":"Barbanera, F., Lanese, I., Tuosto, E.: Composing communicating systems, synchronously. In: Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_3","DOI":"10.1007\/978-3-030-61362-4_3"},{"key":"23_CR15","doi-asserted-by":"publisher","unstructured":"Barbanera, F., Lanese, I., Tuosto, E.: Composition of synchronous communicating systems. J. Logical Algebraic Methods Program. (2023). https:\/\/doi.org\/10.1016\/j.jlamp.2023.100890","DOI":"10.1016\/j.jlamp.2023.100890"},{"key":"23_CR16","doi-asserted-by":"publisher","unstructured":"Barwell, A.D., Brown, C., Hammond, K.: Finding parallel functional pearls: Automatic parallel recursion scheme detection in Haskell functions via anti-unification. Futur. Gener. Comput. Syst. (2018). https:\/\/doi.org\/10.1016\/j.future.2017.07.024","DOI":"10.1016\/j.future.2017.07.024"},{"key":"23_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64276-1_11","author":"MH ter Beek","year":"2020","unstructured":"ter Beek, M.H., Hennicker, R., Kleijn, J.: Compositionality of Safe Communication in Systems of Team Automata (2020). https:\/\/doi.org\/10.1007\/978-3-030-64276-1_11","journal-title":"Compositionality of Safe Communication in Systems of Team Automata"},{"key":"23_CR18","doi-asserted-by":"publisher","unstructured":"Bouma, J., de\u00a0Gouw, S., Jongmans, S.S.: Multiparty Session Typing in Java, deductively. In: Tools and Algorithms for the Construction and Analysis of Systems (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_3","DOI":"10.1007\/978-3-031-30820-8_3"},{"key":"23_CR19","doi-asserted-by":"publisher","unstructured":"Cerna, D.M., Kutsia, T.: Unital anti-unification: type and algorithms. In: Leibniz International Proceedings in Informatics, LIPIcs, vol.\u00a0167 (2020). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2020.26","DOI":"10.4230\/LIPIcs.FSCD.2020.26"},{"key":"23_CR20","doi-asserted-by":"publisher","unstructured":"Chmel\u00edk, M., \u0158eh\u00e1k, V.: Controllable-choice message sequence graphs. In: Mathematical and Engineering Methods in Computer Science (2013). https:\/\/doi.org\/10.1007\/978-3-642-36046-6_12","DOI":"10.1007\/978-3-642-36046-6_12"},{"key":"23_CR21","doi-asserted-by":"publisher","unstructured":"Edixhoven, L., Jongmans, S.S., Proen\u00e7a, J., Castellani, I.: Branching pomsets: Design, expressiveness and applications to choreographies. J. Logical Algebraic Methods Program. (2024). https:\/\/doi.org\/10.1016\/j.jlamp.2023.100919","DOI":"10.1016\/j.jlamp.2023.100919"},{"key":"23_CR22","doi-asserted-by":"publisher","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM (2016). https:\/\/doi.org\/10.1145\/2827695","DOI":"10.1145\/2827695"},{"key":"23_CR23","doi-asserted-by":"publisher","unstructured":"Lange, J., Tuosto, E.: Synthesising choreographies from local session types. In: Concurrency Theory (2012). https:\/\/doi.org\/10.1007\/978-3-642-32940-1_17","DOI":"10.1007\/978-3-642-32940-1_17"},{"key":"23_CR24","doi-asserted-by":"publisher","unstructured":"Lange, J., Tuosto, E., Yoshida, N.: From communicating machines to graphical choreographies. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (2015). https:\/\/doi.org\/10.1145\/2676726.2676964","DOI":"10.1145\/2676726.2676964"},{"key":"23_CR25","doi-asserted-by":"publisher","unstructured":"Lassez, J.L., Maher, M.J., Marriott, K.: Unification revisited. In: Foundations of Logic and Functional Programming (1988). https:\/\/doi.org\/10.1007\/3-540-19129-1_4","DOI":"10.1007\/3-540-19129-1_4"},{"key":"23_CR26","doi-asserted-by":"publisher","unstructured":"Lohrey, M.: Realizability of high-level message sequence charts: closing the gaps. Theoret. Comput. Sci. (2003). https:\/\/doi.org\/10.1016\/j.tcs.2003.08.002","DOI":"10.1016\/j.tcs.2003.08.002"},{"key":"23_CR27","doi-asserted-by":"publisher","unstructured":"Mahe, E., Bannour, B., Gaston, C., Le Gall, P.: Efficient interaction-based offline runtime verification of distributed systems with lifeline removal. Sci. Comput. Program. (2025). https:\/\/doi.org\/10.1016\/j.scico.2024.103230","DOI":"10.1016\/j.scico.2024.103230"},{"key":"23_CR28","doi-asserted-by":"publisher","unstructured":"Mahe, E., Gaston, C., Le Gall, P.: Denotational and operational semantics for interaction languages: application to trace analysis. Sci. Comput. Program. (2024). https:\/\/doi.org\/10.1016\/j.scico.2023.103034","DOI":"10.1016\/j.scico.2023.103034"},{"key":"23_CR29","doi-asserted-by":"publisher","unstructured":"Montesi, F., Yoshida, N.: Compositional choreographies. In: Concurrency Theory (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_30","DOI":"10.1007\/978-3-642-40184-8_30"},{"key":"23_CR30","doi-asserted-by":"publisher","unstructured":"Nguetoum, J., Bannour, B., Le Gall, P., Mahe, E.: Artifact for FM\u201926 paper: specializing anti-unification for interaction models composition via gate connections (2026). https:\/\/doi.org\/10.5281\/zenodo.18636309","DOI":"10.5281\/zenodo.18636309"},{"key":"23_CR31","unstructured":"Plotkin, G.D.: A note on inductive generalization. In: Machine Intelligence, Vol. 5 (1970)"},{"key":"23_CR32","unstructured":"Pottier, L.: Generalisation de termes en th\u00e9orie \u00e9quationnelle. cas associatif-commutatif. Rapport de Recherche RR-1056, INRIA Sophia Antipolis (1989). https:\/\/inria.hal.science\/inria-00075503v1"},{"key":"23_CR33","unstructured":"Reynolds, J.: Transformational systems and the algebraic structure of atomic formulas. In: Machine Intelligence, Vol. 5 (1970)"},{"key":"23_CR34","doi-asserted-by":"publisher","unstructured":"Rocha, M., Sim\u00e3o, A., Sousa, T.: Model-based test case generation from UML sequence diagrams using extended finite state machines. Software Qual. J. 29(3), 597\u2013627 (2021). https:\/\/doi.org\/10.1007\/s11219-020-09531-0","DOI":"10.1007\/s11219-020-09531-0"},{"key":"23_CR35","doi-asserted-by":"publisher","unstructured":"Rolim, R., Soares, G., Gheyi, R., D\u2019Antoni, L.: Learning quick fixes from code repositories. In: Proceedings of the XXXV Brazilian Symposium on Software Engineering (2018). https:\/\/doi.org\/10.1145\/3474624.3474650","DOI":"10.1145\/3474624.3474650"},{"key":"23_CR36","doi-asserted-by":"publisher","unstructured":"Scalas, A., Yoshida, N.: Less is more: multiparty session types revisited. Proc. ACM Program. Lang. (2019). https:\/\/doi.org\/10.1145\/3290343","DOI":"10.1145\/3290343"},{"key":"23_CR37","doi-asserted-by":"publisher","unstructured":"Inductive Synthesis of Functional Programs. LNCS (LNAI), vol. 2654. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/b12055","DOI":"10.1007\/b12055"},{"key":"23_CR38","doi-asserted-by":"publisher","unstructured":"Stolze, C., Miculan, M., Di Gianantonio, P.: Composable partial multiparty session types for open systems. Softw. Syst. Model. (2023). https:\/\/doi.org\/10.1007\/s10270-022-01040-x","DOI":"10.1007\/s10270-022-01040-x"}],"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-26204-2_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T18:03:32Z","timestamp":1783015412000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_23","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":"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"}}]}}