# On the use of generalisation and unification for composing interactions via gate connection

Joel Nguetoum Kenne, Boutheina Bannour, Pascale Le Gall

## ► To cite this version:

Joel Nguetoum Kenne, Boutheina Bannour, Pascale Le Gall. On the use of generalisation and unification for composing interactions via gate connection. UNIF 2025 - 39th International Workshop on Unification, Jul 2025, Birmingham, United Kingdom. hal-05148680

HAL Id: hal-05148680

https://hal.science/hal-05148680v1

Submitted on 7 Jul 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# On the use of generalisation and unification for composing interactions via gate connection

Joel Nguetoum Kenne¹, Boutheina Bannour², and Pascale Le Gall³

¹ Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France
christian.nguetoumkenne@cea.fr

² Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France
boutheina.bannour@cea.fr

³ Université Paris-Saclay, CentraleSupélec, MICS Fr-91192 Gif-sur-Yvette Cedex, France.
pascale.legall@centralesupelec.fr

**Interactions defined as a term algebra** An Interaction Language (IL) offers an intuitive graphical notation, akin to UML Sequence Diagrams [2] or Message Sequence Charts [1], for specifying distributed systems. Let us consider Figure 1a describing a simple scenario for a system comprising a server and a broker. Each component of the system, in the present case, a broker and a server, is represented by a vertical line called *lifeline*. The broker mediates requests from a remote device to the server, which can either accept or deny them. Specifically, upon receiving a message *auth* (representing an access request) from a remote machine, the broker forwards this to the server as a message *authReq*. The server then evaluates the request and responds to the broker with an acknowledgement message *ack*, followed by either a message granted, prompting the broker to reply to the remote machine with a message labelled *success*, or by a message *denied*, leading the broker to send a message *failure* to the remote machine. So, lifelines are used to identify the interface of the systems. In our case, the broker and server lifelines define the system in Figure 1a, and the client lifeline defines the system in Figure 1b.

An IL specifies two types of message exchanges: *value-passings* for exchanges between lifelines within the system, and *actions* for emissions (resp. receptions) to (resp. from) the environment. Communication with the environment is associated with an artefact called *gate*, which serves as a bridge to connect the models of distinct systems. In the sequel, we designate by $\mathcal{L}$, $\mathcal{M}$ and $\mathcal{G}$ the universes of lifelines, messages and gates, respectively. The emission (resp. reception) of a message is designated by $l!m[g]$ (resp. $l?m[g]$) where $l \in \mathcal{L}$, $m \in \mathcal{M}$ and $g \in \mathcal{G}$. For our example, $a_1 = \text{broker?auth}[1]$ represents the reception of the message *auth* by broker on the gate 1. This reception is represented by an incoming horizontal arrow with the gate 1 highlighted by a red square. Similarly, the emission *broker!success*[2] is represented by an outgoing arrow from the lifeline broker with a purple square for the gate 2. We refer to $\mathcal{A}$ the set of all *actions*, whether they be emissions or receptions. For an action $a = l\Delta m[g]$ in $\mathcal{A}$, we write $\theta(a) = l$, $\delta(a) = \Delta$, $\mu(a) = m$, and $\gamma(a) = g$. Two actions $a$ and $b$ in $\mathcal{A}$ are *complementary* if they convey the same message ($\mu(a) = \mu(b)$), have the same gate ($\gamma(a) = \gamma(b)$), are of a different type (reception vs emission) ($\delta(a) \neq \delta(b)$), and are anchored in different lifelines ($\theta(a) \neq \theta(b)$). Given an action $a$, we denote by $\bar{a}$ the set of actions complementary to $a$. Exchanges of messages between lifelines, or *value-passings*, can be seen as a coupling between two complementary actions, encapsulating information about the gate used to connect them. The set $\mathbb{VP}$ of value-passings is defined as $\{\text{vp}(a, b) \mid a, b \in \mathcal{A}, b \in \bar{a}\}$. The value-passings are represented with horizontal arrows: $\text{vp}(\text{broker!authReq}[\cdot], \text{server?authReq}[\cdot])$ is the value passing placed highest out of the four present in the interaction in Figure 1a. We use by default the identifier `.` to represent a gate that occurs in a value-passing and anonymise it. Indeed, gates often become useless information for value-passings. In particular, on graphical representations,
<figure><img src="image_2.png" /><figcaption>(a) Sequence diagram of the term $i_0$</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>(b) Sequence diagram of the term $j_0$</figcaption></figure>

<caption>Figure 1: Examples of two interactions designed to be composed by gate sharing.</caption>

a gate in an action is marked by a coloured square, while a gate is not visually present for a value-passing.

In addition to actions and value-passings, interaction languages provide scheduling operators specifying more complex behaviours. It includes a few binary operators, such as alt, which expresses the alternative between behaviours. Figure 1a includes a box labelled by alt and containing the two alternative behaviours specified in each sub-box. The set of interactions will be represented as a set of terms whose actions and value-passings, as well as the empty interaction $\emptyset$ specifying the absence of behaviours, are the constants and, whose scheduling operators are the n-ary operators for $n > 0$. With $\mathcal{F} = \cup \mathcal{F}_u$ where $\mathcal{F}_u$ is a finite set of operation symbols of arity $u \ge 0$ and with the set $\mathcal{X}$ of variables disjoint from $\mathcal{F}$, the term algebra $T_{\mathcal{F}}(\mathcal{X})$ is the smallest set verifying $\mathcal{X} \cup \mathcal{F}_0 \subseteq T_{\mathcal{F}}(\mathcal{X})$ and for $f \in \mathcal{F}_u$ with $u > 0$, and $t_1, \dots, t_u \in T_{\mathcal{F}}(\mathcal{X})$, $f(t_1, \dots, t_u) \in T_{\mathcal{F}}(\mathcal{X})$. Ground terms are terms without variables.

**Definition 1 (Interactions).** The set $\mathbb{I}$ of interactions consists of the ground terms associated with $\mathcal{F} = \cup \mathcal{F}_u$, where:

$$ \mathcal{F}_0 = \{\emptyset\} \cup \mathbb{A} \cup \mathbb{V}\mathbb{P}, $$

$$ \mathcal{F}_2 = \{\text{seq}, \text{alt}, \text{par}\}, $$

$$ \mathcal{F}_1 = \{\text{loop}\}, $$

$$ \mathcal{F}_u = \emptyset \quad \forall u > 2. $$

For an interaction i, we denote by $\theta(i)$ (resp. $\gamma(i)$) the set of lifelines involved in i (resp. the set of gates occurring outside value-passings).

The interaction term associated with the sequence diagram of Figure 1a is given by:

$$ i_0 = \text{seq}(\text{broker?auth}[1], \text{seq}(\text{vp}(\text{broker!authReq}[-]), \text{server?authReq}[-]), \text{vp}(\text{server!ack}[-]), \text{broker?ack}[-]), \\ \text{alt}(\text{seq}(\text{vp}(\text{server!granted}[-]), \text{broker?granted}[-]), \text{broker!success}[2]), \\ \text{seq}(\text{vp}(\text{server!denied}[-]), \text{broker?denied}[-]), \text{broker!failure}[3])) $$

We have $\theta(i_0) = \{\text{broker, server}\}$ and $\gamma(i_0) = \{1, 2, 3\}$. In Figure 1a, the operator seq is not explicitly represented. For two interactions i and j, the term seq(i, j) is depicted as the representation of i on top of the representation of j, without any specific box.
Each interaction i in I denotes a set of traces<fnref n="1" /> $[[i]] \subseteq A^*$, i.e. a set of finite sequences of elements in A. $[[i]]$ is the semantics of i, defined inductively according to the structure of i. Table 1 summarises the different cases. Note that the 3 types of constants ($\mathcal{F}_0 = \{\emptyset\} \cup A \cup VP$) directly characterise 3 different semantics, respectively, the empty sequence $\varepsilon$, the action itself a for $a \in A$, and the sequence $l!m[g].l'?!m[g]$ for a value-passing of the form $vp(l!m[g], l'?!m[g])$. Semantics of alt and loop are obvious, resp. using the set union $\cup$ and the Kleene star defined as:

$$T^0 = \{\varepsilon\}, \quad T^{n+1} = \{t_1.t_2 \mid t_1 \in T, t_2 \in T^n\}.$$

The operator $\parallel$ captures standard interleaving, as in process algebras (e.g., CSP [11], CCS [15]) or regular expressions with shuffle [7]. For traces $t_1, t_2 \in A^*$, we have $\varepsilon \parallel t_1 = t_1 \parallel \varepsilon = \{t_1\}$, and

$$(a.t_1) \parallel (b.t_2) = \{a.t_3 \mid t_3 \in t_1 \parallel (b.t_2)\} \cup \{b.t_3 \mid t_3 \in (a.t_1) \parallel t_2\}$$

While these operators are standard in many specification languages, weak sequencing is specific to IL and accounts for partially ordered execution subject to conflict. The conflict predicate $\times$ detects whether a trace interferes with a lifeline $l$: $\varepsilon \times l = \bot$, $(a.t) \times l = (\theta(a) = l) \lor (t \times l)$. Using this, weak sequencing on traces is defined by: $\varepsilon;_\ast t_1 = t_1;_\ast \varepsilon = \{t_1\}$ and by: $(a.t_1);_\ast (b.t_2)$ is

$$\begin{cases} \{a.t_3 \mid t_3 \in t_1;_\ast (b.t_2)\} & \text{if } a.t_1 \times \theta(b) \\ \{a.t_3 \mid t_3 \in t_1;_\ast (b.t_2)\} \cup \{b.t_3 \mid t_3 \in (a.t_1);_\ast t_2\} & \text{otherwise.} \end{cases}$$

To illustrate how the semantics of weak sequencing differ from those of parallel composition, consider the following examples.

Weak sequencing in interaction seq($vp(l_1!m_1[g_1], l_2?m_1[g_1])$, $vp(l_1!m_2[g_2], l_2?m_2[g_2]$)) forces the sequencing of actions that share the same lifeline and leaves the order free between actions carried by different lifelines. The resulting set is $\{l_1!m_1[g_1].l_2?m_1[g_1]\};_\ast \{l_1!m_2[g_2].l_2?m_2[g_2]\}$ which contains exactly two traces:

$$\{l_1!m_1[g_1].l_2?m_1[g_1].l_1!m_2[g_2].l_2?m_2[g_2], l_1!m_1[g_1].l_1!m_2[g_2].l_2?m_1[g_1].l_2?m_2[g_2]\}$$

The interaction par($vp(l_1!m_1[g_1], l_2?m_1[g_1])$, $vp(l_1!m_2[g_2], l_2?m_2[g_2]$)) allows the two value-passing interactions to occur simultaneously, with interleaved execution. The resulting trace set $\{l_1!m_1[g_1].l_2?m_1[g_1]\} \parallel \{l_1!m_2[g_2].l_2?m_2[g_2]\}$ contains 4 traces:

$$\{l_1!m_1[g_1].l_2?m_1[g_1].l_1!m_2[g_2].l_2?m_2[g_2], l_1!m_2[g_2].l_2?m_2[g_2].l_1!m_1[g_1].l_2?m_1[g_1], \dots\}$$

All operator semantics are extended to sets of traces in the standard way. The semantics of interaction operators naturally inherit algebraic properties from the underlying operations defined on traces and sets. What interests us in the following is that the operators in question satisfy some standard algebraic properties such as associativity, commutativity, etc. The equational theory E considered in this work is presented in Table 2. A more detailed presentation of the trace-based semantics of the scheduling operators and the associated equational theory can be found in [14].

Note that the axioms do not translate all the properties present in IL. For example, none of the axioms exploits the knowledge of lifelines: for example, we know that for $l_1 \neq l_2$, $seq(l_1\Delta_1m_1[g_1], l_2\Delta_2m_2[g_2]) = seq(l_2\Delta_2m_2[g_2], l_1\Delta_1m_1[g_1])$ holds whereas it is not true that

<footnote n="1">¹Given a set S, $S^*$ is the set of all finite sequences of elements in S with $\varepsilon$ denoting the empty sequence and with "." denoting the associative law concatenating two sequences.</footnote>
<table><caption>Table 1: Denotational semantics of interaction constructs</caption><thead><tr><th>Interaction</th><th colspan="2">Semantics</th></tr></thead><tbody><tr><td>Ø</td><td colspan="2">{ε}</td></tr><tr><td>a</td><td>{a}</td><td>a ∈ A</td></tr><tr><td>vp(a, b)</td><td>{a.b}</td><td>a, b ∈ A, b ∈ a</td></tr><tr><td>alt(i, j)</td><td>[i] ∪ [j]</td><td>i, j ∈ I</td></tr><tr><td>par(i, j)</td><td>[i] || [j]</td><td></td></tr><tr><td>seq(i, j)</td><td>[i] ;* [j]</td><td></td></tr><tr><td>loop(i)</td><td>∪<sub>n∈N</sub> [i]<sup>n</sup></td><td>i ∈ I</td></tr></tbody></table>

<table><caption>Table 2: Equational theory E on scheduling operators.</caption><thead><tr><th>Property</th><th>Operator</th><th>Equation</th></tr></thead><tbody><tr><td>Associativity</td><td>f ∈ {seq, par, alt}</td><td>f(f(x, y), z) ≈ f(x, f(y, z))</td></tr><tr><td>Commutativity</td><td>f ∈ {par, alt}</td><td>f(x, y) ≈ f(y, x)</td></tr><tr><td>Idempotence</td><td>alt</td><td>alt(x, x) ≈ x</td></tr><tr><td>Unit element Ø</td><td>f ∈ {seq, par}</td><td>f(x, Ø) ≈ x, f(Ø, x) ≈ x</td></tr><tr><td>Ø-fixpoint</td><td>loop</td><td>loop(Ø) ≈ Ø</td></tr></tbody></table>

$seq(l_1Δ_1m_1[g_1], l_1Δ_2m_2[g_2]) = seq(l_1Δ_2m_2[g_2], l_1Δ_1m_1[g_1])$. These properties, which are cor- related with the lifelines in play, are not included in Table 2. As a result, the properties do not reflect the scheduling rules, either along the same lifeline or the precedence between the emission and the reception occurring in a value-passing. Thus, the properties in Table 2 only partially translate the algebraic properties of the semantics associated with interactions in I. Needless to say, the properties mentioned in Table 2 are valid for all interaction terms, whatever the lifelines involved.

**Gate-based Interaction composition** Scheduling operators enable interactions to be composed vertically as long as they share the same lifelines. The gates, highlighted by coloured squares, represent hooks for horizontally composing interactions defined on disjoint sets of lifelines: complementary actions are combined together to build a value-passing and, by indirect effect, to erase the gates in the representation of the resulting interaction. Let us illustrate our point with the interaction $j_0$ given in Figure 1b. It describes a client component that asks for access authorisation by sending a message auth and then expecting in return to receive success or failure. $j_0$ is given by the term:

$$j_0 = \text{seq}(\text{client!auth}[1], \text{alt}(\text{client?failure}[3], \text{client?success}[2]))$$

Composing $i_0$ and $j_0$ horizontally means matching complementary actions to build a single interaction from the two interactions. More precisely, composing interactions into a global interaction involves reconstructing a coherent global view from independently specified local behaviours. This composition operation combines complementary actions to reconstitute value-passings, while preserving the semantics of interactions in arguments. The first actions of the two interactions $i_0$ and $j_0$ are respectively reception broker?auth[1] and emission client!auth[1]
defined on the same gate 1 and carrying the same message auth. It is therefore natural to anticipate that the composition of $i_0$ and $j_0$ will include the connection of these two complementary actions, in a value-passing vp(Client!auth[1], broker?auth[1]). Intuitively, the composition of two interactions $i_0$ and $j_0$ will connect complementary actions, and will respect a principle of minimality, i.e. if we reduce the composition to the lifelines of $i_0$ (resp. $j_0$), then we should retrieve the initial interaction $i_0$. That's why, we introduce a projection operator on a subset $L$ of lifelines that extracts a local interaction from a global and breaks value-passings that enter or exit $L$:

**Definition 2.** The projection of $i \in \mathbb{I}$ onto a subset of lifelines $L \subset \mathcal{L}$, denoted $\pi_L(i)$, is:

$$ \pi_L(\emptyset) = \emptyset; \quad \pi_L(a) = a \text{ if } \theta(a) \in L, \text{ otherwise } \emptyset; \\ \pi_L(vp(a, b)) = \begin{cases} a & \text{if } \theta(a) \in L \text{ and } \theta(b) \notin L \\ b & \text{if } \theta(a) \notin L \text{ and } \theta(b) \in L \\ vp(a, b) & \text{if } \theta(a) \in L \text{ and } \theta(b) \in L \\ \emptyset & \text{otherwise} \end{cases} \\ \pi_L(loop(j)) = loop(\pi_L(j)); \quad \pi_L(f(j, k)) = f(\pi_L(j), \pi_L(k)) $$

for $a, b \in \mathbb{A}$, $j, k \in \mathbb{I}$ and $f \in \{\text{seq, alt, par}\}$.

In [13], we have showed that projection onto $L$ is compatible with semantics, i.e. the semantics of $\pi_L(i)$ is simply the set of traces of $i$, only keeping actions on $L$. Using the $\pi_L$ operator, we define the composition of two interactions as:

**Definition 3.** (E-Composition) For interactions $i, j \in \mathbb{I}$ with $\theta(i) \cap \theta(j) = \emptyset$ and $G = \gamma(i) \cap \gamma(j)$, an interaction $k \in \mathbb{I}$ is called an E-composition of $i$ and $j$ if the following conditions hold:

$$ \pi_{\theta(i)}(k) \approx_E i \quad (1) \qquad \pi_{\theta(j)}(k) \approx_E j \quad (2) \qquad \gamma(k) \cap G = \emptyset \quad (3) $$

By default, the composition of two interactions is defined relative to the set $E$ of equations given in Table 2. Conditions (1) and (2) require that projections of the composition are congruent with the initial interactions according to $E$. While conditions (1) and (2) preserve the interactions $i$ and $j$ to be composed, condition (3) forces the composition to connect all the gates common to $i$ and $j$ with new value-passings. Let us remark that the only way to preserve an action $a$ defined on a gate in $G$ (ensuring condition (1)) is to associate it with a complementary action in $j$, to form a value-passing vp($a, b$) (ensuring condition (3)).

Figure 2 shows $k_0$, a possible interaction for the composition of $i_0$ and $j_0$, both graphically and as a term. The complementary actions associated with the gates 1, 2, and 3 are glued into value-passings in the model $k_0$. Also, $\pi_{\{broker,server\}}(k_0) \approx_E j_0$ and $\pi_{\{client\}}(k_0) \approx_E j_0$ by the commutativity of alt and the unit element equation of seq. Notably, the commutativity of the alt operator is essential for successfully glueing gates 2 and 3, as their order differs across the instances of alt.

Our definition of projection-based composition is inspired by the one proposed in [12] for Multiparty Session Types, a process algebra-based formalism where the synthesis of a so-called global type is obtained with inference rules based on compatibility conditions with local session types. Their work has been extended by Barbanera et al. [4] and adapted to Communicating Finite State Machines [5].
<figure><img src="image_4.png" /><figcaption>Figure 2: A possible interaction for the composition of the two interactions shown in Figure 1.</figcaption></figure>

**Our research question:** Can interaction composition be expressed in terms of generalisation and unification? The background to this question comes from the observation that successfully composing two interactions consists of connecting the gates of the interactions and superimposing the scheduling operators structuring the two interactions so as to identify a structure common to both interactions which will serve as a structure for the composition. First of all, provided that we ensure that the gates involved in the new value-passings necessarily concern complementary actions of the two interactions *i* and *j* to be composed, we can simply replace these actions by their gates, so that they become simple constants. Generalisation and unification are two techniques associated with equational theories dedicated to the analysis of similarities between two terms.

As far as **generalisation** is concerned, the main idea is that the generalising term *t* associated with two substitutions *σ*₁ and *σ*₂ captures the common structure of *i* and *j* by ensuring *tσ*₁ = *i* and *tσ*₂ = *j*, and to compute the composition, all you have to do is construct a new substitution *σ* which combines the two substitutions *σ*₁ and *σ*₂. In the degenerate case with *G* = ∅ for which there is nothing to connect, the generalising term can be reduced to a unique variable *x* with *xσ*₁ = *i* and *xσ*₂ = *j*, it will then suffice to take *xσ* = **seq**(*xσ*₁, *xσ*₂) = **seq**(*i*, *j*).

As far as **unification** is concerned, the main idea is that each of the terms *i* and *j* is folded so as to keep only the gates and structuring operators placed above it, reducing the subterms with no gates to variables. Substitutions *σ* ensuring the unification of these two folded terms then allow the composition to be constructed: either term *iσ* or *jσ* defines the composition of *i* and *j* by replacing the variables with the subterms they have folded, provided that all the folded subterms of *i* and *j* remain present in the composition.

As explained above, the computations for generalisation and unification should be carried out modulo the equational theory *E*. In the following, using the interaction $k_0$ in Figure 2, we outline how the composition of two interactions can be characterised or constructed using generalisation and unification.

**Using generalisation** Generalisation, or anti-unification, is the process of deriving a symbolic expression that captures the commonalities among a set of terms. For instance, $t = \mathbf{par}(x, y)$ is a generalisation of $s_1 = \mathbf{par}(a, b_1)$ and $s_2 = \mathbf{par}(b_2, a)$, since there exist substitutions $\sigma_1$ and $\sigma_2$ such that $t\sigma_1 = s_1$ and $t\sigma_2 = s_2$. Under a theory $E_1$ expressing the commutativity of $\mathbf{par}$, the term $t' = \mathbf{par}(x, a)$ becomes an $E_1$-generalizer of $s_1$ and $s_2$. Generalisation modulo
equations has been studied in various settings: [16] for empty theory, [3] for combinations of associative, commutative, and unit axioms under specific constraints, [8] for idempotence.

To enable generalisation, the interactions to be composed i and j are first folded. The folding (1) replaces actions whose gates are in $G = \gamma(i) \cap \gamma(j)$ by the corresponding gate symbols, and (2) hides the largest subterms not containing any action whose gate belongs to $G$, under fresh constants, as they are irrelevant to composition. The original content is implicitly memorised during folding and can be recovered for later unfolding. For instance, folding the models $i_0$ and $j_0$ yields:

$$i_0^* = \text{seq}(1, \text{seq}(c_1, \text{alt}(\text{seq}(c_2, 2), \text{seq}(c_3, 3)))), \quad j_0^* = \text{seq}(1, \text{alt}(3, 2))$$

Given the equations $E$ from Table 2, we compute an $E$-generaliser $t$ of $i_0^*$ and $j_0^*$, along with substitutions $\sigma_1$ and $\sigma_2$ such that $i_0^* \approx_E t\sigma_1$ and $j_0^* \approx_E t\sigma_2$. A generaliser $t$ is considered well-formed if, for each variable $x$, the terms $x\sigma_1$ and $x\sigma_2$ contain no gates, thereby ensuring that all gates reside exclusively within $t$. The primary aim of the composition process is, in fact, the glueing of complementary actions into value-passing interactions. Since these complementary actions are represented solely as gates within the folded terms, the intuition behind a well-formed generalisation is to identify such representations at corresponding positions within the generaliser, thus providing a foundation for constructing the composition. In our approach, a generaliser that does not contain a given gate cannot be used to glue the corresponding complementary actions. One such well-formed generaliser is:

$$t_0 = \text{seq}(1, \text{seq}(x_1, \text{alt}(\text{seq}(x_2, 2), \text{seq}(x_3, 3)))))$$

with $\sigma_1 = \{x_1 \mapsto c_1, x_2 \mapsto c_2, x_3 \mapsto c_3\}$ and $\sigma_2 = \{x_1 \mapsto \emptyset, x_2 \mapsto \emptyset, x_3 \mapsto \emptyset\}$. The generaliser $t_0$ is well-formed, as all gates 1, 2, and 3 occur in $t_0$, not in the values of $\sigma_1$ or $\sigma_2$.

From the well-formed generaliser $t$, the composition is constructed by: (1) replacing each gate $g$ by the value passing $\text{vp}(a, b)$ associated with complementary actions from $i$ and $j$, and (2) replacing each variable $x$ by $\text{seq}(x\sigma_1, x\sigma_2)$.

In our example, this process, called *merging*, produces the composed term $k_0^*$, where complementary actions are aligned as value passings and folded parts are rejoined using seq. Unfolding the constants in $k_0^*$ yields the final $E$-composition $k_0$, shown in Figure 2.

**Using unification** Unification finds a substitution that renders two symbolic expressions identical. For example, the substitution $\sigma = \{x \mapsto b, y \mapsto a\}$ unifies $t_1 = \text{par}(x, a)$ and $t_2 = \text{par}(b, y)$, since $t_1\sigma = t_2\sigma = \text{par}(b, a)$. In the presence of a theory $E_1$ expressing commutativity of $\text{par}$, $t_3 = \text{par}(y, b)$ becomes unifiable with $t_1$ via $\sigma' = \{x \mapsto b, y \mapsto a\}$, since $t_1\sigma' = \text{par}(b, a) \approx_{E_1} \text{par}(a, b) = t_3\sigma'$. Such a substitution is called an $E_1$-unifier. Unification modulo equational theories has been widely studied since Robinson's work, with significant contributions by Boudet et al. [6], Escobar et al. [10], and implementations in tools such as Maude [9].

To facilitate unification, interactions $i$ and $j$ intended for composition are folded in a manner similar to that described earlier in the paper: subterms that do not contain gates from $G = \gamma(i) \cap \gamma(j)$ are replaced with variables, while actions associated with gates in $G$ are abstracted as gates. For instance, folding $i_0$ and $j_0$ gives:

$$i_0^\ddagger = \text{seq}(1, \text{seq}(x_1, \text{alt}(\text{seq}(x_2, 2), \text{seq}(x_3, 3)))), \quad j_0^\ddagger = \text{seq}(1, \text{alt}(3, 2))$$

We then compute an $E$-unifier $\sigma$ of $i_0^\ddagger$ and $j_0^\ddagger$ such that, for each variable $x$, the term $x\sigma$ contains no gates, and either $i_0^\ddagger\sigma$ subsumes all variables in $j_0^\ddagger$ or vice versa. We refer to such a unifier as *well-formed*. As with the well-formed generalisation, the objective is to align complementary
actions at corresponding positions, though in this case, the alignment occurs at the positions of the gates in $i^2$ or $j^2$. The subsumption condition ensures that no information from the original model is lost, as the variables originate from the folding of concrete subterms. One such well-formed unifier is:

$$ \sigma_0 = \{x_1 \mapsto \emptyset, x_2 \mapsto \emptyset, x_3 \mapsto \emptyset\} $$

The composed term $k_0^2$ is then built by merging $i_0^2$ and $j_0^2$ using $\sigma_0$: each gate is replaced by the corresponding value passing, and each variable $x$ by $\text{seq}(x, x\sigma_0)$. Unfolding $k_0^2$ yields the final E-composition $k_0$ shown in Figure 2.

**Discussion** This work has explored generalisation (or anti-unification) and unification for composing interactions. Our gate-based composition proceeds modulo equations and uses folding to abstract away the internals of gate-free segments, allowing both techniques to focus on relevant interaction structure without interference from composition-irrelevant details. We observe that when unification succeeds, it suggests the possible existence of a composition aligning gates and operators, even if it does not yield its structure. In contrast, generalisation can reveal the actual structure; however, not all generalisers are suitable. Only *well-formed* generalisers -those ensuring that gates common to interactions to be composed appear in the generalizer expression itself, not in variable substitutions -preserve the intended structure.

To illustrate, consider the terms $i^2 = \text{seq}(1, x)$ and $j^2 = \text{seq}(y, 1)$, where $x$ and $y$ are folding variables for some hypothetical interactions $i$ and $j$ to be composed. These can be unified modulo the unit element equation of $\text{seq}$ (see Table 2) with the substitution $\sigma = \{x \mapsto \emptyset, y \mapsto \emptyset\}$, but the result does not reveal the structure of a composition. In contrast, a generaliser exists and captures that structure: let $i^* = \text{seq}(1, c)$ and $j^* = \text{seq}(d, 1)$, where $c$ and $d$ are folding constants (still referring to interactions $i$ and $j$). A well-formed generalisation modulo the unit element equation of $\text{seq}$ is:

$$ t = \text{seq}(x, \text{seq}(1, y)) $$

with substitutions $\sigma_1 = \{x \mapsto \emptyset, y \mapsto c\}$ and $\sigma_2 = \{x \mapsto d, y \mapsto \emptyset\}$. Here, the generaliser explicitly represents the gate 1 within its structure and thus reflects the intended composition. Designing such generalisers and supporting algorithms is therefore essential.

Interestingly, in unification, the same example admits an infinite minimal complete set of unifiers, such as $\{x \mapsto \emptyset, y \mapsto \emptyset\}$, $\{x \mapsto 1, y \mapsto 1\}$, $\{x \mapsto \text{seq}(1, 1), y \mapsto \text{seq}(1, 1)\}$, and so on. These solutions differ in their compositional informativeness: substitutions like $\{x \mapsto 1, y \mapsto 1\}$ or $\{x \mapsto \text{seq}(1, 1), y \mapsto \text{seq}(1, 1)\}$ are less interesting as they include gates explicitly, while the trivial solution $\{x \mapsto \emptyset, y \mapsto \emptyset\}$ is of greater interest because it suggests that gates can be aligned. Although preliminary, this approach shows how local models can be merged into a coherent global view by aligning complementary actions and preserving interaction semantics. Future work will formalise correctness guarantees and explore algorithmic aspects.

## Acknowledgements

The authors would like to acknowledge the support of the TWIN-LOOP Project (Grant Agreement No. 101192649), which is funded by the European Union. Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or CINEA. Neither the European Union nor the granting authority can be held responsible for them.
References

[1] Message Sequence Chart (MSC). https://www.itu.int/rec/T-REC-Z.120/.

[2] Unified Modeling Language (UML). https://www.omg.org/spec/UML/.

[3] M. Alpuente, S. Escobar, J. Meseguer, and J. Sapiña. Order-sorted equational generalization algorithm revisited. *Annals of Mathematics and Artificial Intelligence*, 2022.

[4] F. Barbanera, M. Dezani-Ciancaglini, I. Lanese, and E. Tuosto. Composition and decomposition of multiparty sessions. *Journal of Logical and Algebraic Methods in Programming*, 2021.

[5] F. Barbanera, I. Lanese, and E. Tuosto. Composition of synchronous communicating systems. *Journal of Logical and Algebraic Methods in Programming*, 2023.

[6] A. Boudet, E. Contejean, and H. Devie. A new AC unification algorithm with an algorithm for solving systems of diophantine equations. In *Symposium on Logic in Computer Science*, 1990.

[7] S. Broda, A. Machiavelo, N. Moreira, and R. Reis. Automata for regular expressions with shuffle. *Information and Computation*, 2018.

[8] D. Cerna and T. Kutsia. Idempotent Anti-unification. *Transactions on Computational Logic*, 2019.

[9] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, José Meseguer, and Carolyn Talcott. Maude System. Available at http://maude.cs.illinois.edu, 2023. Version 3.3.1.

[10] S. Escobar, J. Meseguer, and R. Sasse. Variant Narrowing and Equational Unification. *Electronic Notes in Theoretical Computer Science*, 2009.

[11] C. A. R. Hoare. Communicating sequential processes. ACM / Morgan & Claypool, 2021.

[12] J. Lange and E. Tuosto. Synthesising Choreographies from Local Session Types. In *CONCUR 2012 – Concurrency Theory*, 2012.

[13] E. Mahe, B. Bannour, C. Gaston, and P. Le Gall. Efficient interaction-based offline runtime verification of distributed systems with lifeline removal. *Science of Computer Programming*, 2025.

[14] E. Mahe, C. Gaston, and P. Le Gall. Denotational and operational semantics for interaction languages: Application to trace analysis. *Science of Computer Programming*, 2024.

[15] R. Milner. *A Calculus of Communicating Systems*. Springer, 1980.

[16] G. D. Plotkin. A Note on Inductive Generalization. In *Machine Intelligence 5*. Edinburgh, 1970.