for maps that are used as substitution). Statements like $\exists c_j^{j \in J}$ defines both $J$ and the mapping $j \mapsto c_j$. The disjoint union on sets is noted $\oplus$. Disjoint union is also used on maps. There are several ways of ensuring a union is disjoint, we will indifferently either suppose sets are disjoint or rename conflicting objects (useful for variables). In a formula, a quantifier followed by a finite set will be used as a shorthand for the quantification on every variable in the set: $\forall \{a_1, \dots, a_n\}, \exists \{b_1, \dots, b_m\}, P$ means $\forall a_1, \dots, \forall a_n, \exists b_1, \dots, \exists b_m, P$.

Our expression algebra $E$ is the disjoint union of terms, actions, and formulas $E = \mathcal{T} \oplus \mathcal{A} \oplus \mathcal{F}$. $\mathcal{T}$ and $\mathcal{A}$ are term algebras. The set of formulas $\mathcal{F}$ contain at least first order formulas and equality<fnref n="4" /> over $\mathcal{T}$ and $\mathcal{A}$. For $e \in E$, $\text{vars}(e)$ is the set of variables in $e$ that are not bound by a binder. An expression is closed if $\text{vars}(e) = \emptyset$. The set $\mathcal{P}$ denotes values which is a subset of closed terms. $\mathcal{F}_V$ is the set of formulas $f$ that only uses variables in $V$, i.e., the formulas such that $\text{vars}(f) \subseteq V$. The parallel substitution of variables in $e$ by a map $\psi: V \to \mathcal{T}$ is denoted $e\{\psi\}$.

We suppose given a satisfiability relation on closed formulas, denoted $|=$. We will use two variants of the satisfiability relation:

- The satisfiability of a formula $f \in \mathcal{F}$ under some valuation $\sigma: V \to \mathcal{P}$ is defined as follows: $\sigma|=$ $f \iff \exists \text{vars}(f\{\sigma\})$, $f\{\sigma\}$

- The satisfiability of a formula $f \in \mathcal{F}$ with some variable set $V$ as context is defined as follows: $V \vdash f \iff \forall V, \exists (\text{vars}(f) \setminus V), f$

## 2.2 Open Automata (OA)

OA are labelled transition systems with variables that can be used to compose other automata: they are made of transitions that are dependent on the actions of “holes”, a composition operation consists in filling a hole with another automaton to obtain a more complex automaton. The variables make the OA symbolic, and the holes allow for a partial definition of the behaviour.

**Definition 1 (Open transition, Open automaton).** An open automaton is a tuple $(S, s_0, V, \sigma_0, J, T)$ with $S$ a set of states, $s_0 \in S$ the initial state, $V$ the finite set of variable names, $\sigma_0: V \to \mathcal{P}$ the initial valuation of variables, $J$ the set of hole names and $T$ the set of open transitions.

An open transition is a structure $\mathop{\beta_{j}^{j \in J'}}_{s \stackrel{\alpha}{\rightarrow} s'}$, $g, \psi$ made of several composing entities, equivalent to a tuple. In an open transition $s, s' \in S$ are the source and target states, $\alpha \in \mathcal{A}$ is the resulting action that can be observed from the outside, $J' \subseteq J$ are the holes involved in the transition, $g \in \mathcal{F}$ is the guard that may constraint the transition, and $\psi: V \to \mathcal{T}$ are the variable assignments that have an effect on the state of the automaton. Each $\beta_j \in \mathcal{A}$ is an action of the holes $j$, To be well-formed, an open transition should use only variables of the automaton

<footnote n="4">⁴ Equality does not need to be only syntactic.</footnote>
and variables appearing in the involved actions, formally:

$$ vars(g) \subseteq vars(\alpha) \cup \bigcup_{j \in J'} vars(\beta_j) \cup V \\ \forall v \in V. vars(\psi(v)) \subseteq vars(\alpha) \cup \bigcup_{j \in J'} vars(\beta_j) \cup V $$

A pair consisting of a state and a valuation is called a configuration (of the automaton). We use two operators to access pieces of information of the OA.

**Definition 2 (Out-transition, Transition variables).** Let $\langle S, s_0, V, \sigma_0, J, T \rangle$ be an automaton and let $r$ be a state in $S$. $OT_T(r) \subset T$ are the transition outgoing from state $r^5$. The local variables of a transition $vars(t)$ are all variables appearing in transition $t$ except the variables of the automaton. Outgoing transitions and variables are formally defined as follows.

$$ OT_T(r) = \left\{ \begin{array}{l} \beta_j^{j \in J'} , g, \psi \\ \vdots \\ s \xrightarrow{\alpha} s' \end{array} \in T \mid s = r \right\} \\ vars\left( \begin{array}{l} \beta_j^{j \in J'} , g, \psi \\ \vdots \\ s \xrightarrow{\alpha} s' \end{array} \right) = \left( vars(\alpha) \cup \bigcup_{j \in J'} vars(\beta_j) \right) \setminus V $$

*Example 1 (prod-cons)*. As a running example, we consider a classical producer-consumer pair interacting through FIFO buffer, named prod-cons. Fig. 1 reflects the overall structure of the system involving a producer process, a consumer process and an orchestrator that coordinates their activities.

<figure><img src="image_30.png" /><figcaption>**Fig. 1.** Structure of the example. Each box corresponds to a process whose ports are the actions it can perform. The actions observable by the environment are **push**, which indicates the enqueuing of an element, **pop** which indicates the dequeuing, and **print** which indicates the production of results.</figcaption></figure>

The OA modelling the behaviour of such a system using an unbounded circular/ring buffer is depicted in Fig. 2. The automaton has a single state with

<footnote n="5">⁵ When the set $T$ is clear from the context, it will be omitted and we will use $OT(r)$</footnote>
<figure><img src="image_31.png" /><figcaption>Fig. 2. OA for the prod-cons system using FIFO circular buffer.</figcaption></figure>

two holes: P and Q that are the two interacting processes. l (as last) indicates the next available position for enqueuing an element and f (as first) is the position that contains the next element to be deunteed. The buffer reacts to a push from P and enqueues it. Similarly, whenever Q pops an element, it dequeues it. Additionally, whenever Q produces an item, it is exposed as an external observable print action. When any process do its internal computation, it is exposed externally as unobservable action τ.

The example uses several kinds of data. Variable m holds a message (we can leave the message type abstract here). We additionally use arrays of messages with a syntax of the form M[l] for array accesses; M is an array of N elements, from 0 to N − 1. Finally we use addition and modulo operation (%) on integers.

□

*Open automata composition.* OA are partially specified automata, the partiality arises from the holes. A hole can be seen as a port in which we can plug an OA. The plugging operation is called composition. The composition of OA was already implicitly defined by the means of composition on pNets in previous work [16]. We provide here a (new) direct definition of composition for OA.

**Definition 3 (Composition of OA).** Let $A_c = \langle S_c, s_{0c}, V_c, \sigma_{0c}, J_c, T_c \rangle$ be an OA and $k$ one of its holes, $k \in J_c$. Let $A_p = \langle S_p, s_{0p}, V_p, \sigma_{0p}, J_p, T_p \rangle$ be another OA, the composition $A_c[A_p/k]$ that fills the hole $k$ of the context OA $A_c$ with the parameter OA $A_p$ is defined as follows:

$$A_c[A_p/k] ::= \langle S_c \times S_p, (s_{0c}, s_{0p}), V_c \uplus V_p, \sigma_{0c} \uplus \sigma_{0p}, J_p \uplus J_c \setminus \{k\}, T \rangle$$

with

$$T = \left\{ \begin{array}{l} \left. \begin{array}{l} \beta_j^{j \in J'_p \uplus J'_c}, g_c \wedge g_p \wedge \alpha_p = \beta_k, \psi_c \uplus \psi_p \\ (s_c, s_p) \xrightarrow{\alpha_c} (s'_c, s'_p) \end{array} \right| \left. \begin{array}{l} \beta_j^{j \in J'_c \uplus \{k\}}, g_c, \psi_c \\ s_c \xrightarrow{\alpha_c} s'_c \end{array} \right\} \in T_c, \quad \left. \begin{array}{l} \beta_j^{j \in J'_p}, g_p, \psi_p \\ s_p \xrightarrow{\alpha_p} s'_p \end{array} \right\} \in T_p \\ \\ \cup \left\{ \begin{array}{l} \left. \begin{array}{l} \beta_j^{j \in J'_c}, g_c, \psi_c \\ (s_c, s_p) \xrightarrow{\alpha_c} (s'_c, s'_p) \end{array} \right| \left. \begin{array}{l} \beta_j^{j \in J'_c}, g_c, \psi_c \\ s_c \xrightarrow{\alpha_c} s'_c \end{array} \right\} \in T_c, k \notin J'_c, s_p \in S_p \end{array} \right\}$$

The first OA decides when the second can evolve by involving its hole in a transition: the action emitted when $A_p$ makes a transition is synchronised with
<figure><img src="image_32.png" /><figcaption>**Fig. 3.** (Left) A producer. It produces one item at a time and pushes it. (Right) A consumer. It pops an item, does some work and pushes the result.</figcaption></figure>

<figure><img src="image_33.png" /><figcaption>**Fig. 4.** OA for filling the hole P in prod-cons: prod-cons[P/producer].</figcaption></figure>

the action of the hole $k$ in transitions of $A_c$. The condition $\alpha_p = \beta_k$ ensures that the action emitted by the automaton $A_p$ filling the hole is the one expected in the hole $k$ of the open automaton $A_c$.

*Example 2.* Fig. 3 shows a producer automaton and a consumer automaton that can be used to fill the holes P and Q of prod-cons defined in Example 1.

The OA on Fig. 4 is the composition of the system in Fig. 2 and the producer in Fig. 3 (left). The composition consists of two states (the product of the states of both automata). The transitions from one state to another come from the synchronisation of the transitions of the encompassing automaton with those of the producer filling the hole P, this is why there is no more action from hole P in the composed automaton. Only elements related to the hole P are changed and in particular, transitions involving Q remain unchanged. $\square$

## 2.3 Relations between Open Automata

Establishing semantic equivalences and simulation relations between different OA requires to compare their states. For this purpose, we suppose that the variables of the two OA are disjoint (a renaming of variables may have to be applied before comparing OA states).

**Definition 4 (Relation on open automata configurations).** Suppose $V_1$ and $V_2$ are disjoint. A relation on configurations of two OA $\langle S_1, s_{01}, V_1, \sigma_{01}, J_1, T_1 \rangle$ and $\langle S_2, s_{02}, V_2, \sigma_{02}, J_2, T_2 \rangle$ is a function $\mathcal{R}: S_1 \times S_2 \to \mathcal{R}_{V_1 \otimes V_2}$.
The idea is that two states are related depending on the satisfiability of the expression relying their variables, i.e., if the variables of the OA verify a certain formula. In other words, to each pair of states is attached a boolean formula that may refer to the variables of each of the two OA, stating whether the two states are related or not. Additionally, we say that the relation $\mathcal{R}$ relates the initial states of the automata if: $\sigma_{01} \preceq \sigma_{02} \vdash \mathcal{R}(s_{01}, s_{02})$. We illustrate such a relation over automata with bisimulation relation below.

## 2.4 A Bisimulation for Open Automata

Bisimulation between OA was defined in [6]. We show below the principles of this bisimulation. We first recall the usual definition of bisimulation. Bisimulation can be defined as follows for standard transition systems:

**Definition 5 (Classical Bisimulation).** A bisimulation is a relation $\mathcal{R}$ such that if $s \mathcal{R} t$ then:

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l}
\forall l \ s', \ s \stackrel{l}{\rightarrow} s' \implies & \exists t'. \ s' \ \mathcal{R} \ t' \wedge t \stackrel{l}{\rightarrow} t' & s \ \mathcal{R} \ t \\
\text{and conversely} & \text{i.e.} \quad l \downarrow & t \downarrow \\
\forall l \ t', \ t \stackrel{l}{\rightarrow} t' \implies & \exists s'. \ s' \ \mathcal{R} \ t' \wedge s \stackrel{l}{\rightarrow} s' & s' \ \mathcal{R} \ t'
\end{array}
$$

$s$ and $t$ are bisimilar, written $s \sim t$ iff there is a bisimulation relation $\mathcal{R}$ such that $s \mathcal{R} t$. If only the first one of the two implications above is verified, we say that $s$ simulates $t$ and denote it $s \le t$.

A bisimulation relation relates pair of states and ensures that any behaviour of one automaton can be performed by the other one while staying in relation. We informally explain here the symbolic nature of the bisimulation for OA and the related complexity of its definition. The notion of symbolic bisimulation, as it was introduced in [15], is aimed at computing bisimulation of value-passing systems, i.e. systems made of processes exchanging data with their environment and between processes, where data are values from a possibly infinite domain. The presence of holes in fact raises no strong difficulty but the variables must be handled carefully. Consider the two following simple OA:

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

We should be able to consider these two OA as bisimilar. Both can input any $\beta(x)$ input on their hole and stores the value of $x$, emitting $\alpha(x)$ along the transition. The difference is the way $x$ is stored. We can then define a configuration relation $\mathcal{R}$ such that $\mathcal{R}(s, s_2)$ is true and $\mathcal{R}(t, t_2)$ holds when $z \ge 0$ and
$y = z$, while $\mathcal{R}(t', t_2)$ holds when $z < 0$ and $y = -z$. This illustrates relation on configurations, but also shows that bisimulation on OA is more complex than in the classical case. Indeed, we need two transitions on the left OA to simulate a single one on the right OA. We should check that these two transitions cover all the cases accepted by the right hand side OA, and of course that destination states are in relation. Formally, FH-bisimulation is defined as follows [6]:

**Definition 6 (Strong FH-bisimulation).**

Suppose $\langle S_1, s_{01}, V_1, \sigma_{01}, J_1, T_1 \rangle$ and $\langle S_2, s_{02}, V_2, \sigma_{02}, J_2, T_2 \rangle$ are OA with identical holes of the same sort, with disjoint sets of variables ($V_1 \cap V_2 = \emptyset$).

Then $\mathcal{R}$, a relation on configurations of OA, is an FH-bisimulation if and only if for any states $s \in S_1$ and $t \in S_2$, we have the following:

- For any open transition $\mathcal{O}T$ in $T_1$: $\frac{\beta_{j \in J'}^{j \in J'}, g_{\mathcal{O}T}, \psi_{\mathcal{O}T}}{s \xrightarrow{\alpha} s'}$ there exists an indexed

set of open transitions $\mathcal{O}T_x^{x \in X} \subseteq T_2$: $\frac{\beta_{j_x \in J_x}^{j \in J_x}, g_{\mathcal{O}T_x}, \psi_{\mathcal{O}T_x}}{t \xrightarrow{\alpha_x} t_x}$ such that the following holds

$$ \mathcal{R}(s,t) \wedge g_{\mathcal{O}T} \implies \bigvee_{x \in X} (\forall j. \beta_j = \beta_{jx} \wedge g_{\mathcal{O}T_x} \wedge \alpha = \alpha_x \wedge \mathcal{R}(s', t_x) \{\psi_{\mathcal{O}T} \uplus \psi_{\mathcal{O}T_x}\}) $$

- and symmetrically any open transition from $t$ in $T_2$ can be covered by a set of transitions from $s$ in $T_1$.

Two automata are bisimilar if there exists a strong FH-bisimulation $\mathcal{R}$ that relates their initial states.

Note that this definition matches an open transition $t_1$ to a family of covering open transitions $t_{2x}^{x \in X}$. Intuitively, this means that for every pair of related states ($s_1, s_2$) of the two automata, and for every transition of the first automaton from $s_1$, there is a set of matching transitions of the second automaton from $s_2$ such that the produced action match, the actions of the same holes and the successors are related after variable update. Technically, the following sections do not rely on the definition of strong bisimulation on OA, but they follow the same principles and in particular the same way to faithfully simulate an open transition by a set of other open transitions.

## 2.5 Reachability

We finally define a new predicate abstracting state reachability for OA, it allows us to reason on reachable states in an automaton. It can be seen as an abstraction of the reachable states under the form of a predicate that must stay verified along the execution of the OA.
**Definition 7 (Reachability).** For any OA $A = (S, s_0, V, \sigma_0, J, T)$, a reachability predicate $\check{\forall}_A : S \to \mathcal{F}$ is any predicate on states that is valid on initial state, and preserved across transitions:

$$ \sigma_0 \vdash \check{\forall}_A(s_0) \quad \wedge \quad \forall t = \mathop{\beta_j^{j \in J'}}_{s \xrightarrow{\alpha} s'} , g, \psi \in T, vars(t) \vdash (\check{\forall}_A(s) \wedge g \implies \check{\forall}_A(s') \{\psi\}) $$

Reachability takes into account all paths, and can over-approximate the reachable configurations. From an automation point of view, finding the most precise reachability predicate for a given automaton is not decidable because of the symbolic nature of OA, but only an over-approximation is necessary.

## 3 Simulation for Automata with the Same Holes

Similarly to FH-bisimulation [6] we are interested in finding simulation relations between configurations of two OA that contain variables and holes. When dealing with open systems it is common to define simulation in terms of a simulation relation. We rely on a classical notion of simulation and perform the same extension as in [6], i.e., we start from a simulation relation and add holes and symbolic. The idea is to consider two configurations related by a relation; if one state can do a transition, then the other can also make this transition. Like for bisimulation, a simulation relation characterises when two states are related, and this characterisation is expressed as a predicate on the variables of the two automata. Simulation defines conditions on a relation $\mathcal{R}$ such that $\mathcal{R}(s_1, s_2)$ is a predicate (possibly involving variables of the automata) that is true when the state $s_1$ of $A_1$ simulates the state $s_2$ of $A_2$.

However here we want to build a simulation relation that also guarantees that no deadlock is introduced when refining the automaton. This property is quite frequent in simulation relation, and referred to as *lack of new deadlocks* [19] or *complete simulation* [22]. The notion of deadlock should however be specialised to our OA. Indeed, it is not very useful to check the existence of a transition, instead it makes more sense to use the guards to check if a transition can be taken. We thus define a deadlock reduction criterion based on how the outgoing transitions are guarded. As such, a simulation does not introduce deadlocks if in the conditions where no transition is possible in the refined automaton, no transition were already possible in the more general one. More formally, for any pair of states $s_1$ and $s_2$ we introduce a criterion of the form:

$$ \forall (s_1, s_2) \in S_1 \times S_2, $$

$$ V_1 \oplus V_2 \vdash \left( \mathcal{R}(s_1, s_2) \wedge \neg \left( \bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1) \right) \implies \neg \left( \bigvee_{t_2 \in \text{OT}(s_2)} \text{guard}(t_2) \right) \right) $$

Which can be rewritten as:

$$ \forall (s_1, s_2) \in S_1 \times S_2, V_1 \oplus V_2 \vdash \left( \mathcal{R}(s_1, s_2) \implies \left( \bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1) \right) \vee \neg \left( \bigvee_{t_2 \in \text{OT}(s_2)} \text{guard}(t_2) \right) \right) $$
Both statements being equivalent, as each of them may reveal more intuitive
than the other in different situations, we use them interchangeably. We can now
state the definition of simulation between OA that have the same set of holes.

**Definition 8 (Hole-equal simulation).** Consider two OA with identical set of holes: $A_1 = \langle S_1, s_{01}, V_1, \sigma_{01}, J, T_1 \rangle$ and $A_2 = \langle S_2, s_{02}, V_2, \sigma_{02}, J, T_2 \rangle$, the relation on configurations $\mathcal{R}: S_1 \times S_2 \to \mathcal{R}_{V_1 \prec V_2}$ is a hole-equal simulation from $A_1$ to $A_2$ if the following conditions hold :

$$
(1) \sigma_{01} \uplus \sigma_{02} \vdash \mathcal{R}(s_{01}, s_{02})
$$

$$
(2) \forall (s_1, s_2) \in S_1 \times S_2,
$$

$$
\forall t_1 = \mathop{\beta_{1j}^{j \in J'_1} \ldots g_1, \psi_1}_{s_1 \xrightarrow{\alpha_1} s'_1} \in \mathrm{OT}(s_1). \quad \exists \left( t_{2x} = \mathop{\beta_{2xj}^{j \in J'_2} \ldots g_{2x}, \psi_{2x}}_{s_2 \xrightarrow{\alpha_{2x}} s'_{2x}} \right)^{x \in X} \in \mathrm{OT}(s_2).
$$

$$
(\forall x \in X, J'_{2x} = J'_{1}) \wedge
$$

$$
V_1 \oplus V_2 \oplus \mathrm{vars}(t_1) \vdash \mathcal{R}(s_1, s_2) \wedge g_1 \implies \bigvee_{x \in X} \left( \begin{array}{@{}l@{}} \alpha_{2x} = \alpha_1 \wedge \bigwedge_{j \in J'_1} \beta_{2xj} = \beta_{1j} \wedge \\ g_{2x} \wedge \mathcal{R}(s'_1, s'_{2x}) \{\{\psi_{2x} \oplus \psi_1\}\} \end{array} \right)
$$

(3) Deadlock reduction:

$$
\forall (s_1, s_2) \in S_1 \times S_2, V_1 \oplus V_2 \vdash \left( \mathcal{R}(s_1, s_2) \implies \left( \bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1) \right) \lor \neg \left( \bigvee_{t_2 \in \text{OT}(s_2)} \text{guard}(t_2) \right) \right)
$$

If there is a hole-equal simulation from $A_1$ to $A_2$, then we say that $A_2$ simulates $A_1$; we denote it $A_2 \le A_1$.

The first and second conditions coincide with the natural way to prove induc-
tively that an automaton simulates another by starting with the initial state. The
third condition ensures that simulation prevents the introduction of deadlocks.
Similarly to bisimulation, the second condition states that, for any transition
of the simulating automaton $A_1$, it corresponds to a transition of the automa-
ton $A_2$ that does the same thing and ends up in a similar state. However a
family is needed in $A_2$ because of the symbolic nature of transitions, and be-
cause depending on the values of the variables, $t_1$ may correspond to different
transitions in $A_2$. Our definition captures a simple simulation for OA with the
same holes that is more expressive than a strict simulation since it matches a
transition with a family of transitions. For example, with such a relation we are
able to check the simulation between two OA that differ by duplicated states,
removed duplicated transitions, reinforced guards, different variables, etc. We
will show in Section 5 that this simulation relation has good properties in terms
of transitivity, compositionality, and reflexivity.

**Example 3.** To illustrate the simulation of OA, we consider a variation on the
**prod-cons** example. Namely, we suppose that the two processes *P* and *Q* com-
municate through a one-place buffer. Fig. 5 shows the OA modelling this sim-
pler version of the system, that we refer to as **simprod-cons**. We can easily
check that this automaton simulates the one of Fig. 2. Indeed, one can see that
$\mathcal{R} = \{(r_0, s_0) \to l = f, (r_0, s_1) \to f = l + 1\%N\}$ is a simulation relation. It follows
that $\mathbf{simprod-cons} \le \mathbf{prod-cons}$. $\square$

The simulation relation defined above is insufficient in the setting of compo-
sition which is the main advantage of the OA-based approach. Indeed, it should
be possible to refine an automaton by filling its hole, providing a concrete view
of a part of the application that was not specified originally. More generally, it
should be possible to relate automata that do not have the same holes because
composition is a crucial part of system specification. However, filling holes can
result in a system with more or less holes than the original system because the
plugged subsystem can contain itself many holes. Next section defines a more
powerful simulation relation able to reason on automata with different sets of
holes.

4 A Simulation Relation that Takes Holes into Account

This section extends the preceding relation to automata where the set of holes
is not the same. This is particularly useful to state whether the automaton
after composition is a simulation of the original automaton or not. Indeed, when
composing the set of holes changes. Being able to compare automata with only
some of their holes in common seems useful in general.

One major challenge in the extension of simulation to different sets of holes
is to maintain a form of transitivity while being able to take into account the
actions of some of the holes. A naive definition of simulation would ensure that
only the holes that are identical in the two OA are taken into account in the
simulation. Unfortunately, considering all the common holes does not ensure
transitivity of the simulation for the following reason. If $A_1$ simulates $A_2$ and $A_2$
simulates $A_3$, and one hole $j$ appears in $A_3$ and in $A_1$ but not in $A_2$ then we have
no guarantee on the way $A_1$ and $A_3$ take the actions of this hole into account,
thus a simulation between and $A_1$ and $A_3$ would require conditions involving
actions of the hole $j$ which cannot be ensured. The way we solve this issue is
to remember in the simulation relation which holes have been compared. This
makes the relation parameterised by a subset of the set of holes that belong to
the two automata that we want to take into account. This way, in the example

<figure><img src="image_35.png" /><figcaption>Fig. 5. The simprod-cons OA: the system using one-place buffer.</figcaption></figure>
above, we would have no guarantee on actions the hole j by transitivity but can state a simulation relation with guarantees on the actions of the other holes.

In the following definition we add a parameter $H$ which is the set of holes tracked by the simulation relation and adapt the definition by ignoring actions of the holes that are not in $H$.

Consequently, there is no guarantee related to the actions of the holes outside $H$. We provide compositionality properties when plugging an automaton inside a hole in $H$ but cannot state anything when plugging an automaton outside $H$. The principle is that any property concerning holes that are not in $H$ should be proven specifically for the considered automaton or the considered composition of automata.

**Definition 9 (Hole-tracking simulation).** For two OA

$A_1 = \langle S_1, s_{01}, V_1, \sigma_{01}, J_1, T_1 \rangle$ and $A_2 = \langle S_2, s_{02}, V_2, \sigma_{02}, J_2, T_2 \rangle$, $A_1$ is a simulation of $A_2$ tracking holes $H$, noted $A_1 \leq H A_2$, with $H \subseteq J_1 \cap J_2$, if there is a relation on configurations $\mathcal{R}: (S_1 \times S_2) \to \bar{\mathcal{R}}_{V_1 \leftrightarrow V_2}$ such that<fnref n="6" />:

$$ (1) \quad \sigma_{01} \uplus \sigma_{02} \vdash \mathcal{R}(s_{01}, s_{02}) $$

$$ (2) \quad \forall (s_1, s_2) \in S_1 \times S_2, $$

$$ \begin{gathered} \forall \substack{\beta^{j \in J'_1}, g_1, \psi_1 \\ s_1 \xrightarrow{\alpha_1} s'_1} \in \mathrm{OT}(s_1), \exists \left( \substack{\beta^{j \in J'_{2x}}, g_{2x}, \psi_{2x} \\ s_2 \xrightarrow{\alpha_{2x}} s'_{2x}} \in \mathrm{OT}(s_2) \right)^{x \in X}, \\ (\forall x \in X, J'_{2x} \cap H = J'_1 \cap H) \wedge \\ V_1 \leftrightarrow V_2 \leftrightarrow \mathrm{vars}(t_1) \vdash \\ \left( \mathcal{R}(s_1, s_2) \wedge g_1 \implies \bigvee_{x \in X} \left( \substack{\alpha_1 = \alpha_{2x} \wedge \bigwedge_{j \in J'_1 \cap H} \beta_{1j} = \beta_{2xj} \\ g_{2x} \wedge \mathcal{R}(s'_1, s'_{2x}) \{\psi_1 \uplus \psi_{2x}\} \\ \phantom{g_{2x} \wedge \mathcal{R}(s'_1, s'_{2x}) \{\psi_1 \uplus \psi_{2x}\}} \end{array} \right) \end{gathered} $$

(3) Deadlock reduction:

$$ \forall (s_1, s_2) \in S_1 \times S_2, V_1 \leftrightarrow V_2 \vdash \left( \mathcal{R}(s_1, s_2) \implies \left( \bigvee_{t_1 \in \mathrm{OT}(s_1)} \mathrm{guard}(t_1) \right) \vee \left( \bigvee_{t_2 \in \mathrm{OT}(s_2)} \mathrm{guard}(t_2) \right) \right) $$

Note that every action of the holes outside $H$ is unconstrained according to the simulation relation.

**Property 1 (Relating simulations).** Hole-equal simulation is a particular case of hole-tracking simulation when $J_1 = J_2 = H$.

In particular, if an OA has no hole, the two definitions are equivalent and result in a “symbolic simulation”, if additionally there is no variable in the OA, this corresponds to classical simulation.

**Example 4.** Consider the automata of Examples 1 and 3. As we saw above, $\mathbf{simprod-cons} \leq \mathbf{prod-cons}$, therefore $\mathbf{prod-cons} \leq_{\{P,Q\}} \mathbf{simprod-cons}$.

<footnote n="6">⁶ Note that the definition below is identical to the hole equal simulation except $\cap H$ is added in a few places.</footnote>
*Property 2 (Tracked holes).* By construction, if an automaton is the simulation of another one, it is also a simulation by tracking less holes.

$$A_1 \leq_H A_2 \wedge H' \subseteq H \implies A_1 \leq_{H'} A_2$$

Now that we have a simulation relation that takes both variable parameters and process parameters into account, we would like to ensure that it has properties one would expect for a simulation relation.

# 5 Properties of our Simulation Relations

Before reasoning on the properties of simulation, we need to introduce one additional notion that characterises when the composition of two automata does not introduce new blocked transitions.

## 5.1 Non-blocking Composition

Unfortunately, the deadlock reduction property in the definition of simulation is not compositional: the composition operator can itself introduce a deadlock. In other words, when filling the hole of two related automata with a third one, even if there is a deadlock reduction between the two original automata, there might not be a deadlock reduction in the composed ones. The same problem may arise when two related automata are composed in the same hole of a third one.

This creates a conflict between deadlock reduction and the properties involving composition. We call non-blocking composition a composition that can safely be used to compose OA that are involved in a deadlock reducing relation.

**Definition 10 (Non-blocking composition).** Consider two OA:

$A_1 = \langle S_1, s_{01}, V_1, \sigma_{01}, J_1, T_1 \rangle$ and $A_2 = \langle S_2, s_{02}, V_2, \sigma_{02}, J_2, T_2 \rangle$. Let A be the OA resulting from the composition $A = A_1[A_2/k] = \langle S, s_0, V, \sigma_0, J, T \rangle$. The composition $A_1[A_2/k]$ is non-blocking if A has a reachability predicate such that, for each reachable configuration, if there is a possible transition in $A_1$ then there is a possible transition in A:

$$\forall s = (s_1, s_2) \in S, V \uplus \bigcup_{t \in \text{OT}(s_1)} vars(t) \vdash \left( \forall A(s) \wedge \bigvee_{t \in \text{OT}(s_1)} guard(t) \implies \bigvee_{t \in \text{OT}(s)} guard(t) \right)$$

Like in the definition of simulation (Definition 8) we use guards to ensure that the transition can occur. In general, one would not want to only consider non-blocking composition as it may reveal a bit restrictive, but it is the best necessary condition that we could identify for compositionality of simulation. It will be used to prove composition theorems given below. In absence of non-blocking composition, simulation may also be checked specifically for a given composed automaton.
## 5.2 Properties

We now state the properties of our simulation, their formal proofs can be found in the appendices. We express these properties in terms of hole-tracking simulation because, thanks to Property 1 all the properties of hole-tracking simulation are also valid for hole-equal simulation. The first crucial theorem of simulation is that it is a preorder on the set of OA. This latter enables stepwise refinement.

**Theorem 1 (Simulation is a preorder).** *Hole-tracking simulation is reflexive and transitive: it is a preorder on the set of OA.*

*Proof sketch.* The relation $\leq_H$ is reflexive, $A \leq_H A$. This is shown by considering the relation $\mathcal{R}$ such that $\mathcal{R}(s_1, s_2) \triangleq s_1 = s_2 \wedge \bigwedge_{v \in \mathrm{vars}(s_1)} v = v$ we can prove the conditions for Definition 9. Appendix A gives the proof of transitivity. It is done classically by identifying the relation between $A_1$ and $A_3$ that is a simulation. What is less classical is the definition of this relation because it is a boolean formula. For each couple of states $s_1$ and $s_3$ of $A_1$ and $A_3$ we build a formula that defines the simulation. To do this, we take the disjunction of formulas relating $s_1$ and $s_3$, and passing by all states $s_2$ of $A_2$. More precisely, we define a relation of the following form:

$$ \mathcal{R}_{13}(s_1, s_3) = \bigvee_{s_2 \in S_2} (\mathcal{R}_{12}(s_1, s_2) \wedge \mathcal{R}_{23}(s_2, s_3)) $$

We then prove that this relation is a simulation, according to Definition 9. □

The next theorem states that if two automata are in simulation relation and the same automaton is placed in the same hole of the two automata, then the simulation is preserved. This is the first step toward proving that simulation is compositional in the sense that it is sufficient to prove simulation for the composed automata separately to obtain a simulation relation.

**Theorem 2 (Context refinement).** Let $A_1, A_2$ and $A_3$ be three OA with $A_1 \leq_H A_2$. Let $J_3$ be the set of holes of $A_3$ and suppose that $k \in H$. Suppose additionally that $A_1[A_3/k]$ is non-blocking. We have:

$$ A_1[A_3/k] \leq_{J_3 \omega H \setminus \{k\}} A_2[A_3/k] $$

*Proof sketch.* The proof relies on a simulation relation that we consider is the one that makes $A_1$ and $A_2$ similar, complemented with identity of configurations for $A_3$. Then, by construction, all transitions of the composed automaton $A_1[A_3/k]$ are specified by open transitions of $A_1$. For the transitions that do not involve hole $k$, the transition of $A_1[A_3/k]$ is the same and simulation between $A_1$ and $A_2$ allows us to conclude directly. If the hole $k$ is involved the considered relation implies that valuations in $A_3$ are equal (i.e., the value for each variable are the same in both valuations), after a transition we should obtain “equal” valuations because post-conditions are deterministic. The requirement “$A_1[A_3/k]$ is non-blocking” ensures the deadlock reduction property holds. More precisely, if $A_1[A_3/k]$ is stuck, then $A_1$ is stuck, and thus $A_1[A_2/k]$ is also stuck. □
**Example 5.** Consider again the prod-cons and simprod-cons automata given in the examples above. Since prod-cons $\leq_{\{P,Q\}}$ simprod-cons, then according to Theorem 2, prod-cons[producer/P] $\leq_{\{Q\}}$ simprod-cons[producer/P]. The automaton of prod-cons[producer/P] is shown in Fig. 4. The automaton resulting from the composition of simprod-cons and producer is bigger and not shown here. □

**Theorem 3 (Congruence).** Let $A_1, A_2$ and $A_3$ be three OA with $A_2 \leq_H A_3$. Let $J_1$ be the set of holes of $A_1$ and suppose that $k \in J_1$. Suppose additionally that the composition $A_1[A_2/k]$ is non-blocking. We have:

$$A_1[A_2/k] \leq_{J_1 \circled{H} \setminus \{k\}} A_1[A_3/k]$$

Consequently, as the simulation is transitive we can compose the previous theorems and state the following:

**Theorem 4 (Composability).** Let $A_1, A_2, A_3$ and $A_4$ be four OA with $A_1 \leq_H A_2$ and $A_3 \leq_{H'} A_4$. Suppose that $k \in H$. We have:

$$A_1[A_3/k] \leq_{H \circled{H'} \setminus \{k\}} A_2[A_4/k]$$

**Example 6.** As an example of the use of this theorem, if we design a refined version of the producer process of Example 2 called Refproducer. According to Theorem 4, we have prod-cons[producer/P] $\leq_{\{Q\}}$ simprod-cons[Refproducer/P].

Note that the substitution operation can be extended to a multiple substitution that fills several holes at the same time, and the theorems can be adapted accordingly.

# 6 Related Work

The origins of refinement are in the approach of programming that aims to provide solid foundations for building correct programs [12]. Many work contributed to the development of elaborated notions of refinement in various area (e.g. [7,1,10,8]). In the context of process algebra, refinement between processes can be defined in terms of simulations relation (e.g. ([18,21]). However, the concept of simulations presented so far has focused on the refinement of systems that are inherently closed, i.e., systems which are bounded and without environment,

The simulation ensures the preservation of safety properties as deadlock-freeness and, more generally, all linear temporal logic properties [1,19]. The difference between the existing refinement principles have been studied in [13], for example the authors explain in what sense failure semantics is different from (bi)simulation in the compared systems and properties ensured. In this paper we particularly focus on the compositionality of simulation-based refinement.

There are not a lot of works that study refinement for open systems. Defining refinement of open systems as trace inclusion is addressed as a notion of subtyping in type theory (e.g. [14,9]). The definition of refinement is based on a
connection between session types and communicating automata theories – a no-
tion of session automata based on Communicating Finite-State Machines, that
are used for modelling processes communicating through FIFO channels. The
refinement of open systems is also defined in terms of alternating simulation
[4,3]. Alternating simulation is originating from the game theory [2], it allows
the study of relation between individual components by viewing them as alter-
nating transition systems. In particular, a refinement of game-based automata
expresses that the refined component can offer more services (input actions) and
fewer service demands (output actions). However, the composition of such au-
tomata may lead to illegal states, where one automaton issues an output that is
not acceptable as input in the other one. The theory of alternating simulation
provides an optimistic approach to compute compatibility between automata
based on the fact that each automaton expects the other to provide legal inputs,
i.e., two components can be composed if there is an environment where they can
work together. Our approach has some commonalities with the above mentioned
simulation [3]: both are process-oriented approaches even if they are not based
on the same notion of simulation, and both include in the model how to com-
pose and interact with processes that are accepted as parameters. Nevertheless,
they differ in that our approach focuses on the compositional properties of the
simulation, and not on the fact that entities can be composed.

Previous works on OA focused on equivalence relations compatible with com-
position. In [17], a computable bisimulation is introduced, while in [6] a weak
version of the bisimulation is introduced. In this paper we tackle the refinement
relation in the form of simulation, as is the case for the corresponding relations
on labelled transition systems [8]. Unlike the standard simulation we deal with
symbolic and open models. In [24], the authors exploit transition systems to
reason about the systems that are partially specified by using variables, making
the state space potentially infinite.

Some work target component-based refinement with the concern of preserving
deadlock freedom (e.g. [11,19]). These works are not concerned with the theory
of open symbolic systems, and therefore do not focus on the same modularity as
we do, in particular we provide preservation of refinement by composition.

7 Conclusion

In this article we investigated the notion of refinement for a symbolic and open
model: open automata. OA are convenient for compositional software verifica-
tion. Indeed, OA model parallel systems that are parameterised both by the use
of variables and by the possibility to compose automata. The formalism supports
compositional specification through the simulation paradigm. In this paper, we
introduce a refinement relation between open automata. It relies on a simulation
relation between the two automata; it specifies that the refined process must fol-
low the behaviour of the simulated one. We finally showed that simulation is a
preorder that is preserved by composition, both when filling a hole and when
placing automata in comparable contexts.
## References

1. Abrial, J.R.: The B-book - Assigning programs to meanings. Cambridge University Press (1996)

2. de Alfaro, L.: Game models for open systems. In: Dershowitz, N. (ed.) Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. Lecture Notes in Computer Science, vol. 2772, pp. 269–289. Springer (2003). https://doi.org/10.1007/978-3-540-39910-0_12

3. de Alfaro, L., Henzinger, T.A.: Interface automata. In: Tjoa, A.M., Gruhn, V. (eds.) Proceedings of the 8th European Software Engineering Conference held jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering 2001, Vienna, Austria, September 10-14, 2001. pp. 109–120. ACM (2001). https://doi.org/10.1145/503209.503226

4. Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR’98 Concurrency Theory. pp. 163–178. Springer Berlin Heidelberg, Berlin, Heidelberg (1998)

5. Ameur-Boulifa, R., Henrio, L., Kulankhina, O., Madelaine, E., Savu, A.: Behavioural semantics for asynchronous components. Journal of Logical and Algebraic Methods in Programming **89**, 1–40 (2017). https://doi.org/https://doi.org/10.1016/j.jlamp.2017.02.003, https://www.sciencedirect.com/science/article/pii/S2352220817300287

6. Ameur-Boulifa, R., Henrio, L., Madelaine, E.: Compositional equivalences based on Open pNets. Journal of Logical and Algebraic Methods in Programming **131**, 100842 (2023). https://doi.org/https://doi.org/10.1016/j.jlamp.2022.100842, https://www.sciencedirect.com/science/article/pii/S2352220822000955

7. Back, R., Sere, K.: Stepwise refinement of parallel algorithms. Science of Computer Programming **13**(2), 133–180 (1990). https://doi.org/https://doi.org/10.1016/0167-6423(90)90069-P, https://www.sciencedirect.com/science/article/pii/016764239090069P

8. Bellegarde, F., Julliand, J., Kouchnarenko, O.: Ready-simulation is not ready to express a modular refinement relation. In: Maibaum, T. (ed.) Fundamental Approaches to Software Engineering. pp. 266–283. Springer Berlin Heidelberg, Berlin, Heidelberg (2000)

9. Bravetti, M., Zavattaro, G.: Asynchronous session subtyping as communicating automata refinement. Softw. Syst. Model. **20**(2), 311–333 (2021). https://doi.org/10.1007/s10270-020-00838-x

10. Butler, M.J., Grundy, J., Långbacka, T., Ruksenas, R., von Wright, J.: The refinement calculator: Proof support for program refinement. In: Groves, L., Reeves, S. (eds.) Proc. Conf. Formal Methods Pacific’97, Springer Series in Discrete Mathematics and Theoretical Computer Science (01/01/97). pp. 40–61 (1997), https://eprints.soton.ac.uk/250550/

11. Dihego, J., Sampaio, A., Oliveira, M.: A refinement checking based strategy for component-based systems evolution. Journal of Systems and Software **167**, 110598 (2020). https://doi.org/https://doi.org/10.1016/j.jss.2020.110598

12. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976)

13. Eshuis, R., Fokkinga, M.M.: Comparing refinements for failure and bisimulation semantics. Fundam. Inf. **52**(4), 297–321 (Apr 2002)

14. Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Informatica **42**(2-3), 191–225 (2005). https://doi.org/10.1007/s00236-005-0177-z
15. Hennessy, M., Lin, H.: Symbolic bisimulations. Theoretical Computer Science 138(2), 353-389 (1995). https://doi.org/10.1016/0304-3975(94)00172-F, https://www.sciencedirect.com/science/article/pii/030439759400172F, meeting on the mathematical foundation of programing semantics

16. Henrio, L., Madelaine, E., Zhang, M.: A theory for the composition of concurrent processes. In: Albert, E., Lanese, I. (eds.) Formal Techniques for Distributed Objects, Components, and Systems. pp. 175-194. Springer International Publishing, Cham (2016)

17. Hou, Z., Madelaine, E.: Symbolic bisimulation for open and parameterized systems. In: Proceedings of the 2020 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. pp. 14-26. PEPM 2020, Association for Computing Machinery, New York, NY, USA (2020). https://doi.org/10.1145/3372884.3373161

18. Jifeng, H.: Process simulation and refinement. Form. Asp. Comput. 1(1), 229-241 (mar 1989). https://doi.org/10.1007/BF01887207, https://doi.org/10.1007/BF01887207

19. Kouchnarenko, O., Lanoix, A.: How to verify and exploit a refinement of component-based systems. In: Virbitskaite, I., Voronkov, A. (eds.) Perspectives of Systems Informatics. pp. 297-309. Springer Berlin Heidelberg, Berlin, Heidelberg (2007)

20. Milner, R.: Communication and Concurrency. Prentice-Hall, Inc., USA (1989)

21. Milner, R.: A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol. 92. Springer (1980). https://doi.org/10.1007/3-540-10235-3

22. Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2012), https://hal.inria.fr/hal-00907026

23. Wang, B., Madelaine, E., Zhang, M.: Symbolic Weak Equivalences: Extension, Algorithms, and Minimization - Extended version. Research Report RR-9389, Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France ; East China Normal University (Shanghai) (Jan 2021), https://hal.inria.fr/hal-03126313

24. Zhang, L., Meng, Q., Lo, K.: Compositional abstraction refinement for component-based systems. Journal of Applied Mathematics 2014, 1-12 (2014). https://doi.org/10.1155/2014/703098
A Proof of Transitivity for Refinement (Theorem 1)

If $A_1 \leq_H A_2$ and $A_2 \leq_{H'} A_3$, then $A_1 \leq_{H \cap H'} A_3$.

*Proof.* If $A_1 \leq_H A_2$ then there is $\mathcal{R}_{12}$ a relation between states of $A_1$ and of $A_2$; If $A_2 \leq_{H'} A_3$ then there is $\mathcal{R}_{23}$ a relation between states of $A_2$ and of $A_3$. We build a relation between states of $A_1$ and of $A_3$ as follows: for each pair of states $s_1, s_3$, for each state $s_2$ such that $\mathcal{R}_{12}$ relates $s_1$ and $s_2$, and $\mathcal{R}_{23}$ relates $s_2$ and $s_3$. Let $\mathcal{R}_{13}$ be the relation:

$$ \mathcal{R}_{13}(s_1, s_3) = \bigvee_{s_2 \in S_2} (\mathcal{R}_{12}(s_1, s_2) \wedge \mathcal{R}_{23}(s_2, s_3)) $$

We will show that $A_1 \leq_{H \cap H'} A_3$ by exhibiting $\mathcal{R}_{13}$ as a hole-tracking simulation of $A_1$ by $A_3$.

We have to prove that the relation $\mathcal{R}_{13}$ satisfies the three conditions of the definition of a refinement of OA.

1. Firstly, we have to $\mathcal{R}_{13}$ satisfies initial configurations:

$$ \sigma_{01} \oplus \sigma_{03} \vdash \mathcal{R}_{13}(s_{01}, s_{03}) $$

By knowing that substitutions only have an effect on the variables of the OA they belong to, they also produce terms containing only variables of the OA they belong to. We have:

$$ (\sigma_{01} \oplus \sigma_{02} \vdash \mathcal{R}_{12}(s_{01}, s_{02})) \wedge (\sigma_{02} \oplus \sigma_{03} \vdash \mathcal{R}_{23}(s_{02}, s_{03})) \implies $$

$$ \mathcal{R}_{12}(s_{01}, s_{02}) \{\sigma_{01} \oplus \sigma_{02}\} \wedge \mathcal{R}_{23}(s_{02}, s_{03}) \{\sigma_{02} \oplus \sigma_{03}\} \implies $$

$$ \mathcal{R}_{12}(s_{01}, s_{02}) \{\sigma_{01} \oplus \sigma_{02} \oplus \sigma_{03}\} \wedge \mathcal{R}_{23}(s_{02}, s_{03}) \{\sigma_{01} \oplus \sigma_{02} \oplus \sigma_{03}\} \implies $$

$$ \underbrace{\mathcal{R}_{12}(s_{01}, s_{02}) \wedge \mathcal{R}_{23}(s_{02}, s_{03}) \{\sigma_{01} \oplus \sigma_{02} \oplus \sigma_{03}\}}_{= \mathcal{R}_{13}(s_{01}, s_{03})} $$

Since $\sigma_{02}$ has no effect on variables of $s_{01}$ and $s_{03}$ thus we get the expected result.

2. Secondly, we need to prove that for any open transition $t_1$ in $T_1$ originating from $s_1$:

$$ \beta_{1j}^{j \in J_1}, g_1, \psi_1 \underset{s_1}{\overset{\alpha_1}{\rightleftharpoons}} s_1' \in \text{OT}(s_1) $$

there exists an indexed family of OTs originating from $s_3$:

$$ V_1 \oplus V_3 \oplus vars(t_1) \vdash $$

$$ \left( R_{13}(s_1, s_3) \wedge g_1 \implies \bigvee_{z \in Z} \left( \begin{array}{l} \alpha_1 = \alpha_{3z} \wedge \bigwedge_{j \in J'_{3z} \cap (H \cap H')} \beta_{1j} = \beta_{3jz} \wedge \\ g_{3z} \wedge R_{12}(s'_1, s'_3) \{\psi_1 \oplus \psi_{3z}\} \end{array} \right) \right) $$

The proof of this simulation step follows the same principles as the one given in [6] for the proof of transitivity of bisimulation<fnref n="7" />. It relies on the fact that

<footnote n="7">⁷ In particular, the bisimulation relation exhibited for proving transitivity is the same.</footnote>
one open transition of $A_1$ is simulated by a family of open transitions of $A_2$, and one open transition of $A_2$ is simulated by a family of open transitions of $A_3$. Transitivity leads to a doubly indexed family of simulating open transition.

3. Lastly, we have to prove the satisfaction of the deadlock reduction condition. To build $\mathcal{R}_{13}$ we need to rely on the disjunction of all possible paths to relate $s_1$ and $s_3$, which leads to

$$ \mathcal{R}_{13}(s_1, s_3) = \bigvee_{p \in P} (\mathcal{R}_{12}(s_1, s_{2p}) \wedge \mathcal{R}_{23}(s_{2p}, s_3)) $$

Consider any $(s_1, s_3) \in \mathcal{R}_{13}$ there is a set of states $(s_{2p})^{p \in P}$ of $A_2$ relating $s_1$ and $s_3$.

First, according to the relation between $A_1$ and $A_2$ OA, for all $(s_1, s_{2p}) \in S_1 \times S_2$ we have:

$$ V_1 \oplus V_2 \vdash \mathcal{R}_{12}(s_1, s_{2p}) \implies \bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1) \vee \neg(\bigvee_{t_{2p} \in \text{OT}(s_{2p})} \text{guard}(t_{2p})) $$

Second, according to the relation between $A_2$ and $A_3$ OA, for all $(s_{2p}, s_3) \in S_2 \times S_3$ we have:

$$ V_2 \oplus V_3 \vdash \mathcal{R}_{23}(s_{2p}, s_3) \implies \bigvee_{t_1 \in \text{OT}(s_{2p})} \text{guard}(t_{2p}) \vee \neg(\bigvee_{t_3 \in \text{OT}(s_3)} \text{guard}(t_3)) $$

With the conjunction of both, we get:

$$ V_1 \oplus V_2 \oplus V_3 \vdash \mathcal{R}_{12}(s_1, s_{2p}) \wedge \mathcal{R}_{23}(s_{2p}, s_3) \implies \bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1) \vee \neg(\bigvee_{t_3 \in \text{OT}(s_3)} \text{guard}(t_3)) $$

This is valid for all $s_{2p} \in (s_{2p})^{p \in P}$, then we have:

$$ V_1 \oplus V_2 \oplus V_3 \vdash \underbrace{\bigvee_{p \in P} (R_{12}(s_1, s_{2p}) \wedge R_{23}(s_{2p}, s_3))}_{R_{13}(s_1, s_3)} \implies (\bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1)) \vee \neg(\bigvee_{t_3 \in \text{OT}(s_3)} \text{guard}(t_3)) $$

By removing the $A_2$ variables that have not effect on $A_2$ et $A_3$, we get the desired result:

$$ V_1 \oplus V_3 \vdash \mathcal{R}_{13}(s_1, s_3) \implies (\bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1)) \vee \neg(\bigvee_{t_3 \in \text{OT}(s_3)} \text{guard}(t_3)) $$

□
## B Proof of Context Refinement (Theorem 2)

Suppose that $A_1 \leqslant_H A_2$, $k \in H$ and that $A_1[A_3/k]$ is non-blocking. We have:

$$A_1[A_3/k] \leq_{J_3 \uparrow H \setminus \{k\}} A_2[A_3/k]$$

Pictorially, the theorem states the following result:

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

*Proof.* Let us denote by $A_{13}$ (resp. $A_{23}$) the OA resulting from $A_1[A_3/k]$ (resp. $A_2[A_3/k]$), to prove the theorem it is sufficient to prove that there exists a relation between states of the two OA that satisfies the conditions of Definition 9. We denote $A_1 = \langle S_1, s_{01}, J_1, V_1, \sigma_{01}, T_1 \rangle$, $A_2 = \langle S_2, s_{02}, J_2, V_2, \sigma_{02}, T_2 \rangle$ and $A_3 = \langle S_3, s_{03}, J_3, V_3, \sigma_{03}, T_3 \rangle$. The proof requires to rename the variables of one instance of the two $A_3$ automata to avoid clashes in variable names (this is required by the definition of refinement). In practice we will use superscripts 1 and 2 to distinguish elements of the two instances of $A_3$.

Let $\mathcal{R}$ be the refinement relation relating states of $A_1$ and $A_2$. Let us denote with $t^1$ and $t^2$ the elements of $A_1$ and $A_2$ respectively. Consider any two states $s_{13} = (s_1, s_3^1)$ and $s_{23} = (s_2, s_3^2)$ ($s_3^1$ and $s_3^2$ are the same with renaming). We define a relation $\mathcal{R}'$ relating states of $s_{13}$ and $s_{23}$ as follows:

$$\mathcal{R}'(s_{13}, s_{23}) = \mathcal{R}(s_1, s_2) \wedge \check{\mathcal{A}}_{A_{13}}(s_{13}) \wedge \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2$$

We want to prove that $(\mathcal{R}', H \uplus J_3 \setminus \{k\})$ is a hole-tracking simulation of $A_{13}$ and $A_{23}$. In the following we denote $H' = H \cup J_3 \setminus \{k\}$.

1. First, we have to prove the relation for initial states:

$$\sigma_{013} \uplus \sigma_{023} \vdash \mathcal{R}'(s_{013}, s_{023})$$

with $\sigma_{013} = \sigma_{01} \uplus \sigma_{03}^1$, $\sigma_{023} = \sigma_{02} \uplus \sigma_{03}^2$, $s_{013} = (s_{01}, s_{03}^1)$, and $s_{023} = (s_{02}, s_{02}^2)$.

By using the fact that $\mathcal{R}$ relates initial configurations of $A_1$ and $A_2$, we have:

$$(\sigma_{01} \uplus \sigma_{02} \vdash \mathcal{R}(s_{01}, s_{02}))$$

Considering that initial valuations $\sigma_{03}^1$ and $\sigma_{03}^2$ associate the same values to the “same” variables modulo renaming, so the following holds:

$$\left( \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 \right) \{\{\sigma_{03}^1 \uplus \sigma_{03}^2\}\}.$$
Additionally, because the domains of the substitution function are disjoint, the substitution function has an effect only on the related elements, we get:

$$ (\sigma_{01} \oplus \sigma_{02} \vdash \mathcal{R}(s_{01}, s_{02})) \\ \implies \mathcal{R}(s_{01}, s_{02})\{\sigma_{01} \oplus \sigma_{02}\} \wedge \left( \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 \right) \{\{\sigma_{03}^1 \oplus \sigma_{03}^2\}\} \\ \implies \left( \mathcal{R}(s_{01}, s_{02}) \wedge \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 \right) \{\{\sigma_{01} \oplus \sigma_{02} \oplus \sigma_{03}^1 \oplus \sigma_{03}^2 \oplus \sigma_{013}\}\} \\ \implies \sigma_{013} \oplus \sigma_{023} \vdash \mathcal{R}'(s_{013}, s_{023}) $$

The last step comes from the additional fact that $\check{\mathcal{A}}_{13}(s_{013})$.

2. Second, we need to prove for any open transition $t_{13}$ in $T_{13}$ originating from $s_{13}$:

$$ \frac{\beta_{13j}^{j \in J'_{13}}, g_{13}, \psi_{13}}{s_{13} \xrightarrow{\alpha_{13}} s'_{13}} \in \text{OT}(s_{13}) $$

there exists an indexed family $t_{23x}$ of OTs originating from $s_{23}$ that simulate it:

$$ \left( \frac{\beta_{23xj}^{j \in J'_{23x}}, g_{23x}, \psi_{23x}}{s_{23} \xrightarrow{\alpha_{23x}} s'_{23x}} \in \text{OT}(s_{23}) \right)_{x \in X} $$

such that $(\forall x \in X, J'_{23x} \cap H' = J'_{13} \cap H')$ and

$$ V_{13} \oplus V_{23} \oplus \text{vars}(t_{13}) \vdash $$

$$ \mathcal{R}'(s_{13}, s_{23}) \wedge g_{13} \implies \bigvee_{x \in X} \left( \begin{array}{l} \alpha_{13} = \alpha_{23x} \wedge \bigwedge_{j \in J'_{23x} \cap H'} \beta_{13j} = \beta_{23xj} \wedge \\ g_{23x} \wedge \mathcal{R}'(s'_{13}, s'_{23x})\{\psi_{13} \oplus \psi_{23x}\} \end{array} \right) $$

Recall that by definition of composition and OA refinement we have:

$$ \begin{gathered} V_{13} = V_1 \oplus V_3^1 \text{ and } V_{23} = V_2 \oplus V_3^2 \\ H' \subseteq J_3 \oplus (J_1 \cap J_2) \setminus \{k\} = (J_3 \oplus J_1 \setminus \{k\}) \cap (J_3 \oplus J_2 \setminus \{k\}) \end{gathered} $$

First of all, we have by hypothesis $A_1 \le_H A_2$, then for any open transition $t_1$ in $T_1$ originating from $s_1$:

$$ \frac{\beta_{1j}^{j \in J'_{1}}, g_{1}, \psi_{1}}{s_{1} \xrightarrow{\alpha_{1}} s'_{1}} \in \text{OT}(s_{1}) $$
there exists an indexed family of OTs originating from $s_2$:

$$ \left( \begin{array}{c} \beta_{2x_j}^{j \in J'_{2x}}, g_{2x}, \psi_{2x} \\ \vdots \\ s_2 \xrightarrow{\alpha_{2x}} s'_{2x} \end{array} \right) \in \mathrm{OT}(s_2) \qquad x \in X $$

such that $\forall x \in X, J'_{2x} \cap H = J'_1 \cap H$ and

$$ V_1 \oplus V_2 \oplus \mathrm{vars}(t_1) \vdash \\ \mathcal{R}(s_1, s_2) \wedge g_1 \implies \bigvee_{x \in X} \left( \begin{array}{l} \alpha_1 = \alpha_{2x} \wedge \bigwedge_{j \in J'_{2x} \cap H} \beta_{1j} = \beta_{2xj} \wedge \\ g_{2x} \wedge \mathcal{R}(s'_1, s'_{2x}) \{ \psi_1 \oplus \psi_{2x} \} \end{array} \right) \quad (*) $$

Consider any transition $t_{13}$ in $A_{13}$. Based on the definition of composition $t_{13}$ can be obtained from two different cases, we will consider the two cases separately.

**First case: Both automata perform a transition.** The transition $t_{13}$ is obtained by the composition of transitions $t_1 = \frac{\beta_{1j}^{j \in J'_1}, g_1, \psi_1}{s_1 \xrightarrow{\alpha_1} s'_1} \in \mathrm{OT}(s_1)$ and

$$ t_3^1 = \frac{(\beta_{3j}^1)^{j \in J_3^1}, g_3^1, \psi_3^1}{s_3^1 \xrightarrow{\alpha_3} s_3^1} \in \mathrm{OT}(s_3) \quad \text{when } k \in J'_1 $$

The result is:

$$ t_{13} = \frac{\beta_{1j}^{j \in J'_1 \setminus \{k\}} \oplus (\beta_{3j}^1)^{j \in J_3^1}, g_1 \wedge g_3^1 \wedge \alpha_3^1 = \beta_{1k}, \psi_1 \oplus \psi_3^1}{(s_1, s_3^1) \xrightarrow{\alpha_1} (s'_1, s'_{3})} \quad \text{where } k \in J'_1 $$

We then obtain a family of OTs by the simulation of $A_1$ by $A_2$ (as stated above). By hypothesis we have $k \in H$, so in the case where $k \in J'_1$, we deduce that $k \in J'_{2x}$ we can then build a family of OTs $t_{23x}^{x \in X}$ with the same transitions of $A_3$ (up to renaming) as those used to build $t_{13}$.

$$ t_{23x} = \left( \frac{\beta_{2x_j}^{j \in J'_{2x} \setminus \{k\}} \oplus (\beta_{3j}^2)^{j \in J_3^2}, g_{2x} \wedge g_3^2 \wedge \alpha_3^2 = \beta_{2xk}, \psi_{2x} \oplus \psi_3^2}{(s_2, s_3^2) \xrightarrow{\alpha_{2x}} (s'_{2x}, s'_{3})} \right) \qquad x \in X $$
Recall that in this case $k \in J'_1$, so $\forall x \in X$ we have

$$
\begin{align*}
J'_{23x} \cap H' &= ((J'_{2x} \setminus \{k\}) \uplus J_3^{2'}) \cap (H \uplus J_3 \setminus \{k\}) \\
&= ((J'_{2x} \cap (H \uplus J_3)) \uplus (J_3^{2'} \cap (H \uplus J_3))) \setminus \{k\} \\
&= ((J'_{2x} \cap H) \uplus (J_3^{2'} \cap J_3)) \setminus \{k\} \\
&\qquad \text{since } J_3 \cap J'_{2x} = \emptyset \text{ and } H \cap J_3^{2'} = \emptyset \\
&= ((J'_{2x} \cap H) \uplus J_3^{2'}) \setminus \{k\} \text{ since } J_3^{2'} \subseteq J_3 \\
&= ((J'_1 \cap H) \uplus J_3^{1'}) \setminus \{k\} \quad \text{since } J_3^{1'} = J_3^{2'} \text{ and } J'_1 \cap H = J'_{2x} \cap H \\
&= ((J'_1 \cap H) \uplus (J_3^{1'} \cap J_3)) \setminus \{k\} \text{ since } J_3^{1'} \subseteq J_3 \\
&= (J'_1 \cap (J_3 \uplus H)) \uplus ((J_3^{1'} \cap (J_3 \uplus H)) \setminus \{k\}) \\
&\qquad \text{since } J_3 \cap J'_1 = \emptyset \text{ and } H \cap J_3^{1'} = \emptyset \\
&= ((J'_1 \uplus J_3^{1'}) \setminus \{k\}) \cap ((J_3 \uplus H) \setminus \{k\}) \\
&= J'_{13} \cap H'
\end{align*}
$$

In this case the composition gives:

$$g_{13} \Leftrightarrow g_1 \wedge g_3^1 \wedge \alpha_3^1 = \beta_{1k} \text{ and } g_{23x} \Leftrightarrow g_{2x} \wedge g_3^2 \wedge \alpha_3^2 = \beta_{2xk}$$

As $k \in H$ we have $\beta_{1k} = \beta_{2xk}$ then we deduce:

$$g_3^1 \wedge \alpha_3^1 = \beta_{1k} \Leftrightarrow g_3^2 \wedge \alpha_3^2 = \beta_{2xk}$$

The proof of the rest is based on the following facts:

(a) By construction of $t_{13}$ and $t_{23x}$ we have $\alpha_{13} = \alpha_1$ and $\alpha_{23x} = \alpha_{2x}$. So we deduce: $\alpha_1 = \alpha_{2x} \Rightarrow \alpha_{13} = \alpha_{23x}$.

(b) By composition we have also:

$$\beta_{13j}^{j \in J'_{13}} = \beta_{1j}^{j \in J'_1 \setminus \{k\}} \uplus (\beta_{3j}^{1'} )^{j \in J'_3} \text{ and } \beta_{23x_j}^{j \in J'_{23}} = \beta_{2x_j}^{j \in J'_2 \setminus \{k\}} \uplus (\beta_{3j}^{2'})^{j \in J'_3}$$

Therefore, we have for all $j \in J'_{13}$ (recall that $J'_{13} = J'_{23}$):

$$\beta_{13j} = \beta_{23x_j} \Rightarrow (j \in J'_1 \wedge \beta_{1j} = \beta_{2x_j}) \vee (j \in J_3^{1'} \wedge \beta_{3j}^{1} = \beta_{3j}^{2})$$

(c) Considering $\beta_{3j}^1$ and $\beta_{3j}^2$ are the same (up to renaming) we have:

$$V_3^1 \uplus V_3^2 \uplus vars(t_{13}) \vdash \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \implies \bigwedge_{j \in J_3^{2'}} \beta_{3j}^1 = \beta_{3j}^2$$

Then we compose by disjunction with the following hypothesis (part of formula (*)).
$$V_1 \oplus V_2 \oplus vars(t_1) \vdash \bigwedge_{j \in J_{2x}'} \beta_{1j} = \beta_{2xj}$$

$$V_1 \oplus V_2 \oplus V_3^1 \oplus V_3^2 \oplus vars(t_{13}) \vdash \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \implies \bigwedge_{j \in J_{2x}'} \beta_{1j} = \beta_{2xj} \lor \bigwedge_{j \in J_{3}^{2'}} \beta_{3j}^1 = \beta_{3j}^2$$

$$\Rightarrow V_{13} \oplus V_{23} \oplus vars(t_{13}) \vdash \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \implies \bigwedge_{j \in (J_{2x}^' \cap H) \lor J_3^{2'}} \beta_{13j} = \beta_{23xj}$$

$$\Rightarrow V_{13} \oplus V_{23} \oplus vars(t_{13}) \vdash \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \implies \bigwedge_{j \in ((J_{2x}^' \cap H) \lor J_3^{2'}) \setminus \{k\}} \beta_{13j} = \beta_{23xj}$$

$$\Rightarrow V_{13} \oplus V_{23} \oplus vars(t_{13}) \vdash \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \implies \bigwedge_{j \in (J_{23x}^' \cap H')} \beta_{13j} = \beta_{23xj}$$

We can extend the valuation context of the variables to cover the variables of the transitions $t_3$ and the variables in $V_3^1$ and $V_3^2$ in the formula (*). By using the statements resulting from the cases (a), (b) and (c), we get:

$$V_{13} \oplus V_{23} \oplus vars(t_{13}) \vdash$$

$$\mathcal{R}(s_1, s_2) \land (g_1 \land g_3^1 \land \alpha_3^1 = \beta_{1k}) \land \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \implies$$

$$\bigvee_{x \in X} \left( \begin{array}{l} \alpha_{13} = \alpha_{23x} \land \bigwedge_{j \in (J_{23x}^' \cap H')} \beta_{13j} = \beta_{23xj} \land \\ g_{2x} \land \mathcal{R}(s_1', s_{2x}') \{\psi_1 \oplus \psi_{2x}\} \end{array} \right) \land g_3^2 \land \alpha_3^2 = \beta_{2xk}$$

That can be re-written as follows:

$$V_{13} \oplus V_{23} \oplus vars(t_{13}) \vdash$$

$$\mathcal{R}(s_1, s_2) \land g_{13} \land \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \implies \bigvee_{x \in X} \left( \begin{array}{l} \alpha_{13} = \alpha_{23x} \land \bigwedge_{j \in J_{23x}^' \cap H'} \beta_{13j} = \beta_{23xj} \land \\ g_{23x} \land \mathcal{R}(s_1', s_{2x}') \{\psi_1 \oplus \psi_{2x}\} \end{array} \right)$$

Moreover, we have for any transition $t_3$ in $A_3$ relating $s_3$ and $s_3'$ the following:

$$V_{13} \oplus V_{23} \oplus vars(t_{13}) \vdash$$

$$\bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \land s_3^1 = s_3^2 \implies \bigwedge_{v_3 \in V_3} \psi_{13}(v_3^1) = \psi_{13}(v_3^2) \land s_3^{1'} = s_3^{2'}$$

Furthermore, according to the Definition 7 (reachability applied to the composed automaton $A_1[A_3/k]$) we have, for all $t_{13} \in T_{13}$:

$$vars(t_{13}) \vdash (\check{\alpha}_{13}(s_{13}) \land g_{13} \implies \check{\alpha}_{13}(s_{13}') \{\psi_{13}\})$$
Thus, we get:

$$
\begin{align*}
& V_{13} \uplus V_{23} \uplus \mathrm{vars}(t_1) \cap \mathrm{vars}(t_{13}) \vdash \\
& \phantom{V_{13} \uplus V_{23} \uplus \mathrm{vars}(t_1) \cap \mathrm{vars}(t_{13}) \vdash} \mathcal{R}(s_1, s_2) \wedge g_{13} \wedge \mathbf{\check{\mathrm{A}}}_{A_{13}}(s_{13}) \wedge \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 \\
& \Rightarrow \\
& \quad \bigvee_{x \in X} \left( \begin{array}{@{}l@{}}
\alpha_{13} = \alpha_{23x} \wedge \bigwedge_{j \in J'_{23x} \cap H'} \beta_{13j} = \beta_{23xj} \wedge g_{23x} \wedge \mathcal{R}(s'_1, s'_{2x}) \{\psi_1 \uplus \psi_{2x}\} \\
\wedge \mathbf{\check{\mathrm{A}}}_{A_{13}}(s'_{13}) \{\psi_{13}\} \wedge \bigwedge_{v_3 \in V_3} \psi_{13}(v_3^1) = \psi_{13}(v_3^2) \wedge s_3^{1'} = s_3^{2'}
\end{array} \right)
\end{align*}
$$

From the two previous formulas, we get:

$$
\begin{align*}
& V_{13} \uplus V_{23} \uplus \mathrm{vars}(t_{13}) \vdash \\
& \quad \mathcal{R}(s_1, s_2) \wedge g_{13} \wedge \mathbf{\check{\mathrm{A}}}_{A_{13}}(s_{13}) \wedge \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 \\
& \implies \\
& \quad \bigvee_{x \in X} \left( \begin{array}{@{}l@{}}
\alpha_{13} = \alpha_{23x} \wedge \bigwedge_{j \in J'_{23x} \cap H'} \beta_{13j} = \beta_{23xj} \wedge g_{23x} \wedge \mathbf{\check{\mathrm{A}}}_{A_{13}}(s'_{13}) \{\psi_{13}\} \wedge \\
\mathcal{R}(s'_1, s'_{2x}) \{\psi_1 \uplus \psi_{2x}\} \wedge \bigwedge_{v_3 \in V_3} \psi_{13}(v_3^1) = \psi_{13}(v_3^2) \wedge s_3^{1'} = s_3^{2'}
\end{array} \right)
\end{align*}
$$

Because of the independence of the substitution domains, we simplify and
get the expected formula:

$$
V_{13} \uplus V_{23} \uplus \mathrm{vars}(t_{13}) \vdash \\
\mathcal{R}'(s_{13}, s_{23}) \wedge g_{13} \implies \bigvee_{x \in X} \left( \begin{array}{@{}l@{}}
\alpha_{13} = \alpha_{23x} \wedge \bigwedge_{j \in J'_{23x} \cap H'} \beta_{13j} = \beta_{23xj} \wedge \\
g_{23x} \wedge \mathcal{R}'(s'_{13}, s'_{23x}) \{\psi_{13} \uplus \psi_{23x}\}
\end{array} \right)
$$

Second case: Only the encompassing automaton performs a transition. $t_{13}$ is obtained by the transition $t_1 = \frac{\beta_{1j}^{j \in J'_1}, g_1, \psi_1}{s_1 \xrightarrow{\alpha_1} s'_1}$ alone with the state $s_3^1$ unchanged, if $k \notin J'_1$

$$
t_{13} = \frac{\beta_{1j}^{j \in J'_1}, g_1, \psi_1}{(s_1, s_3^1) \xrightarrow{\alpha_1} (s'_1, s_3^1)}
$$

As stated above, from the simulation of $A_1$ by $A_2$ we get a family of OTs $t_{2x}^{x \in X}$. The composition of this family of OTs with the same transitions of $A_3$ (up to renaming) as those used to build $t_{13}$ produces a family of OTs $t_{23x}^{x \in X}$ in the form:

$$
t_{23x} = \left( \frac{\beta_{2xj}^{j \in J'_{2x}}, g_{2x}, \psi_{2x}}{(s_2, s_3^2) \xrightarrow{\alpha_{2x}} (s'_{2x}, s_3^2)} \right)^{x \in X}
$$
By hypothesis we have $k \in H$, since $k \notin J'_1$, we deduce $k \notin J'_{2x}$.
$\forall x \in X$ we have:

$$
\begin{align*}
J'_{23x} \cap H' &= J'_{2x} \cap (J_3 \uplus H \setminus \{k\}) \\
&= (J'_{2x} \cap H) \text{ since } J'_{2x} \cap J_3 = \emptyset \wedge k \notin J'_{2x} \\
&= (J'_1 \cap H) \text{ since } J'_1 \cap H = J'_{2x} \cap H \\
&= (J'_{13} \cap H') \text{ since } J_3 \cap J'_1 = \emptyset \wedge k \notin J'_1
\end{align*}
$$

The proof of the rest of the formula follows the same steps as the previous case the only argument that change is that by composition we obtain: $g_{13}$ is the same as $g_1$ and $g_{23x}$ is the same as $g_{2x}$ and the actions of $\alpha_{13}$, resp. $\alpha_{23x}$, is the same as $\alpha_1$, resp. $\alpha_{2x}$. Similarly $\beta_{13j}$ and $\beta_{23xj}$ that are the same as $\beta_{1j}$ and $\beta_{2xj}$ respectively. We also apply the reachability definition but only on the automaton $A_1$

3. Lastly, we have to prove the satisfaction of the deadlock reduction condition, i.e., for all $(s_{13}, s_{23}) \in S_{13} \times S_{23}$

$$
V_{13} \uplus V_{23} \vdash \mathcal{R}(s_{13}, s_{23}) \wedge \neg(\bigvee_{t_{13} \in \mathrm{OT}(s_{13})} \mathrm{guard}(t_{13})) \implies \neg(\bigvee_{t_{23} \in \mathrm{OT}(s_{23})} \mathrm{guard}(t_{23}))
$$

By hypothesis the composition $A_1[A_3/k]$ is non-blocking, then according to
the Definition 10 we have for all state $s_{13}$:

$$
V_{13} \uplus \bigcup_{t_1 \in \text{OT}(s_1)} \text{vars}(t_1) \vdash \left( \bigvee_{A_{13}(s_{13})} \wedge \bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1) \right) \implies \bigvee_{t_{13} \in \text{OT}(s_{13})} \text{guard}(t_{13})
$$

From this we can infer:

$$
V_{13} \uplus \bigcup_{t_1 \in \mathrm{OT}(s_1)} vars(t_1) \vdash \neg(\bigvee_{t_{13} \in \mathrm{OT}(s_{13})} guard(t_{13})) \implies \neg(\bigvee_{t_1 \in \mathrm{OT}(s_1)} guard(t_1)) \vee \neg_A_{13}(s_{13})
$$

Furthermore, from the second hypothesis stating that $A_1 \leq_H A_2$, we have
for all $(s_1, s_2) \in S_1 \times S_2$

$$
V_1 \uplus V_2 \vdash \mathcal{R}(s_1, s_2) \wedge \neg(\bigvee_{t_1 \in \mathrm{OT}(s_1)} \mathrm{guard}(t_1)) \implies \neg(\bigvee_{t_2 \in \mathrm{OT}(s_2)} \mathrm{guard}(t_2))
$$

From the two previous formula can deduce:

$$
\begin{align*}
V_{13} \uplus V_2 \uplus \bigcup_{t_1 \in \mathrm{OT}(s_1)} vars(t_1) \vdash \\
R(s_1, s_2) \wedge \neg(\bigvee_{t_{13} \in \mathrm{OT}(s_{13})} guard(t_{13})) &\implies \neg(\bigvee_{t_2 \in \mathrm{OT}(s_2)} guard(t_2)) \vee \neg_A \sqrt{\mathrm{A}_{13}}(s_{13})
\end{align*}
$$
By definition of the composition of open automata, each guard of automaton $A_{23}$ is of the form $guard(t_{23}) = guard(t_2) \wedge t$, thus we have:

$$V_{23} \vdash \neg(\bigvee_{t_1 \in \text{OT}(s_2)} \text{guard}(t_2)) \implies \neg(\bigvee_{t_{23} \in \text{OT}(s_{23})} \text{guard}(t_{23}))$$

From the two previous formula and by introducing the following tautology

$$\left( \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 \right), \text{ we get:}$$

$$V_{13} \bowtie V_{23} \vdash \mathcal{R}(s_1, s_2) \wedge \check{\wedge}_{A_{13}}(s_{13}) \wedge \left( \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 \right) \wedge \neg \bigvee_{t_{13} \in \text{OT}(s_{13})} \text{guard}(t_{13})$$

$$\implies \left( \neg \bigvee_{t_{23} \in \text{OT}(s_{23})} \text{guard}(t_{23}) \vee \neg \check{\wedge}_{A_{13}}(s_{13}) \right) \wedge \check{\wedge}_{A_{13}}(s_{13}) \implies \neg \bigvee_{t_{23} \in \text{OT}(s_{23})} \text{guard}(t_{23})$$

which gives the expected result. □

### C Proof of Congruence (Theorem 3)

Suppose $A_2 \leq_H A_3$ and $k \in H$. and the composition $A_1[A_2/k]$ is non-blocking. We have:

$$A_1[A_2/k] \leq_{J_1 \bowtie H \setminus \{k\}} A_1[A_3/k]$$

Pictorially, the theorem states the following result:

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

*Proof.* Let us denote by $A_{12}$ (resp. $A_{13}$) the OA resulting from $A_1[A_2/k]$ (resp. $A_1[A_3/k]$), to prove the theorem it is sufficient to prove that there exists a relation between states of the two OA that satisfies the conditions of the Definition 9.

We denote $A_1 = \langle S_1, s_{01}, J_1, V_1, \sigma_{01}, T_1 \rangle$ and

$A_2 = \langle S_2, s_{02}, J_2, V_2, \sigma_{02}, T_2 \rangle$ and $A_3 = \langle S_3, s_{03}, J_3, V_3, \sigma_{03}, T_3 \rangle$.

Let $\mathcal{R}$ be the refinement relation relating states of $A_2$ and $A_3$. Let us denote with $t^2$ and $t^3$ the elements of $A_2$ and $A_3$ respectively. Consider any two states $s_{12} = (s_1^1, s_2)$ and $s_{13} = (s_1^2, s_3)$ ($s_1^1$ and $s_1^2$ are the same with renaming). We define a relation $\mathcal{R}'$ relating states of $s_{12}$ and $s_{13}$ as follows:

$$\mathcal{R}'(s_{12}, s_{13}) = \mathcal{R}(s_2, s_3) \wedge \check{\wedge}_{A_{12}}(s_{12}) \wedge \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \wedge s_1^1 = s_1^2$$
Let us denote $H' = H \cup J_1 \setminus \{k\}$. We want to prove that $(\mathcal{R}', H')$ is a hole-tracking simulation of $A_{12}$ and $A_{13}$. As for the previous proof we deal with cases:

1. First, we have to prove the relation for initial states:

$$ \sigma_{012} \oplus \sigma_{013} \vdash \mathcal{R}'(s_{012}, s_{013}) $$

with $\sigma_{012} = \sigma_{01}^1 \oplus \sigma_{03}$, $\sigma_{013} = \sigma_{01}^2 \oplus \sigma_{03}$, $s_{012} = (s_{01}^1, s_{02})$, and $s_{013} = (s_{01}^2, s_{03})$.

The proof of this point is similar to that of Theorem 2.

2. Second, we need to prove for any $\mathcal{O}T t_{12}$ in $T_{12}$ originating from $s_{12}$

$$ \frac{\beta_{12j}^{j \in J'_{12}}, g_{12}, \psi_{12}}{s_{12} \xrightarrow{\alpha_{12}} s'_{12}} \in \mathcal{O}T(s_{12}) $$

there exists an indexed family $t_{13x}$ of OTs originating from $s_{13}$ that simulates it:

$$ \left( \frac{\beta_{13x_j}^{j \in J'_{13x}}, g_{13x}, \psi_{13x}}{s_{13} \xrightarrow{\alpha_{13x}} s'_{13x}} \in \mathcal{O}T(s_{13}) \right)^{x \in X} $$

such that $(\forall x \in X, J'_{13x} \cap H' = J'_{12} \cap H')$ and

$$ V_{12} \oplus V_{13} \oplus \mathit{vars}(t_{12}) \vdash $$

$$ \mathcal{R}'(s_{12}, s_{13}) \wedge g_{12} \implies \bigvee_{x \in X} \left( \begin{array}{l} \alpha_{12} = \alpha_{13x} \wedge \bigwedge_{j \in J'_{13x} \cap H'} \beta_{12j} = \beta_{13x_j} \wedge \\ g_{13x} \wedge \mathcal{R}'(s'_{12}, s'_{13x}) \{\psi_{12} \oplus \psi_{13x}\} \end{array} \right) $$

By definition of composition and OA refinement we have:

$$ V_{12} = V_1^1 \oplus V_3 \text{ and } V_{13} = V_1^2 \oplus V_3 $$

$$ \begin{aligned} H' &= H \oplus J_1 \setminus \{k\} \subseteq J_1 \oplus (J_2 \cap J_3) \setminus \{k\} = (J_1^1 \oplus J_2 \setminus \{k\}) \cap (J_1^2 \oplus J_3 \setminus \{k\}) \\ &= J_{12} \cap J_{13} \end{aligned} $$

We have by hypothesis $A_2 \leq H A_3$, then for any open transition $t_2$ in $T_2$ originating from $s_2$:

$$ \frac{\beta_{2j}^{j \in J'_{2}}, g_{2}, \psi_{2}}{s_{2} \xrightarrow{\alpha_{2}} s'_{2}} \in \mathcal{O}T(s_{2}) $$

there exists an indexed family of OTs originating from $s_3$:

$$ \left( \frac{\beta_{3x_j}^{j \in J'_{3x}}, g_{3x}, \psi_{3x}}{s_3 \xrightarrow{\alpha_{3x}} s'_{3x}} \in \mathcal{O}T(s_3) \right)^{x \in X} $$
such that $\forall x \in X, J'_{3x} \cap H = J'_{2} \cap H$ and

$$V_2 \oplus V_3 \oplus vars(t_2) \vdash \\ \mathcal{R}(s_2, s_3) \wedge g_2 \implies \bigvee_{x \in X} \left( \begin{array}{l} \alpha_2 = \alpha_{3x} \wedge \bigwedge_{j \in J'_{3x} \cap H} \beta_{2j} = \beta_{3xj} \wedge \\ g_{3x} \wedge \mathcal{R}(s'_2, s'_{3x}) \{ \psi_2 \oplus \psi_{3x} \} \end{array} \right) (*)$$

Consider any transition $t_{12}$ in $A_{12}$. Based on the definition of the composition $t_{12}$ can be obtained from two different cases, we will consider the two cases separately.

**First case: Both automata perform a transition.** The transition $t_{12}$ is obtained by the composition of transition $t_2 = \frac{\beta_{2j}^{j \in J'_2}, g_2, \psi_2}{s_2 \xrightarrow{\alpha_2} s'_2}$ and a transition

$$t_1^1 = \frac{(\beta_{1j}^1)^{j \in J'_1}, g_1^1, \psi_1^1}{s_1^1 \xrightarrow{\alpha_1} s_1^{1'}} \quad \text{when } k \in J'_1$$

The result:

$$t_{12} = \frac{\beta_{1j}^1, \beta_{2j}^1, \dots, \beta_{2j}^{j \in J'_2}, g_1^1, g_2^1, \dots, g_2^{j \in J'_2}, \alpha_1^1 = \beta_{2k}, \psi_1^1, \psi_2^1}{(s_1^1, s_2) \xrightarrow{\alpha_1} (s_1^{1'}, s_2^{1'})} \quad \text{where } k \in J'_1$$

We then obtain a family of OTs by the simulation of $A_2$ by $A_3$ (as stated above). By hypothesis we have $k \in H$, so in the case where $k \in J'_1$, we deduce that $k \in J'_{3x}$ we can then build a family of OTs $t_{13x}^{x \in X}$ with the same transition, up to renaming, as the one used to build $t_{12}$ (i.e., $t_1^1$), where $s_1^{2'}$ is the same as $s_1^{1'}$ up to renaming.

$$t_{13x} = \left( \frac{(\beta_{1j}^2)^{j \in J'_1} \oplus \beta_{3xj}^{j \in J'_3 \setminus \{k\}}, g_{3x} \wedge g_1^2 \wedge \alpha_1^2 = \beta_{3xk}, \psi_{3x} \oplus \psi_1^2}{(s_1^2, s_3) \xrightarrow{\alpha_1^2} (s_1^{2'}, s_{3x}^{2'})} \right)^{x \in X}$$
Recall that in this case $k \in J_1^{1'}$, so $\forall x \in X$ we have:

$$
\begin{align*}
J'_{13x} \cap H' &= ((J'_{3x} \setminus \{k\}) \uplus J_1^{2'}) \cap (H \uplus J_1 \setminus \{k\}) \\
&= ((J'_{3x} \cap (H \uplus J_1)) \uplus (J_1^{2'} \cap (H \uplus J_1))) \setminus \{k\} \\
&= ((J'_{3x} \cap H) \uplus (J_1^{2'} \cap J_1)) \setminus \{k\} \\
&\qquad \text{since } J_1 \cap J'_{3x} = \emptyset \text{ and } H \cap J_1^{2'} = \emptyset \\
&= ((J'_{3x} \cap H) \uplus J_1^{2'}) \setminus \{k\} \text{ since } J_1^{2'} \subseteq J_1 \\
&= ((J'_2 \cap H) \uplus J_1^{1'}) \setminus \{k\} \\
&\qquad \text{since } J_1^{1'} = J_1^{2'} \text{ and } J'_2 \cap H = J'_{3x} \cap H \\
&= ((J'_2 \cap H) \uplus (J_1^{1'} \cap J_1)) \setminus \{k\} \text{ since } J_1^{1'} \subseteq J_1 \\
&= (J'_2 \cap (J_1 \uplus H)) \uplus ((J_1^{1'} \cap (J_1 \uplus H)) \setminus \{k\}) \\
&\qquad \text{since } J_1 \cap J'_2 = \emptyset \text{ and } H \cap J_1^{1'} = \emptyset \\
&= ((J'_2 \uplus J_1^{1'}) \setminus \{k\}) \cap ((J_1 \uplus H) \setminus \{k\}) \\
&= J'_{12} \cap H'
\end{align*}
$$

In this case the composition gives:

$$g_{12} \Leftrightarrow g_1^1 \wedge g_2 \wedge \alpha_1^1 = \beta_{2k} \text{ and } g_{13x} \Leftrightarrow g_1^2 \wedge g_{3x} \wedge \alpha_1^2 = \beta_{3xk}$$

As $k \in H$ we have $\alpha_1^1 = \alpha_1^2$ then we deduce:

$$g_1^1 \wedge \alpha_1^1 = \beta_{2k} \Leftrightarrow g_1^2 \wedge \alpha_1^2 = \beta_{3xk}$$

The proof of the rest is based on the following facts:

(a) By construction of $t_{12}$ and $t_{13x}$ we have $\alpha_{12} = \alpha_1^1$ and $\alpha_{13x} = \alpha_1^2$. Since $\alpha_1^1$ and $\alpha_1^2$ are the same (up to renaming) we deduce: $\alpha_{12} = \alpha_{13x}$.

(b) By composition we have also:

$$\beta_{12j}^{j \in J'_{12}} = (\beta_{1j}^1)_{j \in J'_1 \setminus \{k\}} \uplus (\beta_{2j})_{j \in J'_2} \text{ and } \beta_{13xj}^{j \in J'_{13}} = (\beta_{1j}^2)_{j \in J_1^{2'} \setminus \{k\}} \uplus \beta_{3xj}^{j \in J'_{3x} \setminus \{k\}}$$

Therefore, we have for all $j \in J'_{12}$ (recall that $J'_{12} = J'_{13}$):

$$\beta_{12j} = \beta_{13xj} \Rightarrow (j \in J_1^{1'} \wedge \beta_{1j}^1 = \beta_{1j}^2) \vee (j \in J_2^{1'} \wedge \beta_{2j} = \beta_{3xj})$$

(c) Considering $\beta_{1j}^1$ and $\beta_{1j}^2$ are the same (up to renaming) we have:

$$V_1^1 \uplus V_1^2 \uplus vars(t_{12}) \vdash \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \implies \bigwedge_{j \in J_1^{2'}} \beta_{1j}^1 = \beta_{1j}^2$$

We compose by disjunction with the following hypothesis (part of formula (*)).
$$V_2 \oplus V_3 \oplus vars(t_2) \vdash \bigwedge_{j \in J'_{3x} \cap H} \beta_{2j} = \beta_{3xj}$$

$$ \begin{align*} V_2 \oplus V_3 \oplus V_1^1 \oplus V_1^2 \oplus vars(t_{12}) \vdash & \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \implies \bigwedge_{j \in J'_{3x} \cap H} \beta_{2j} = \beta_{3xj} \lor \bigwedge_{j \in J'_{1}^2} \beta_{1j}^1 = \beta_{1j}^2 \\ & \Rightarrow V_{12} \oplus V_{13} \oplus vars(t_{12}) \vdash \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \implies \bigwedge_{j \in (J'_{3x} \cap H) \lor J'_{1}^2} \beta_{12j} = \beta_{13xj} \\ & \Rightarrow V_{12} \oplus V_{13} \oplus vars(t_{12}) \vdash \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \implies \bigwedge_{j \in ((J'_{3x} \cap H) \lor J'_{1}^2) \setminus \{k\}} \beta_{12j} = \beta_{13xj} \\ & \Rightarrow V_{12} \oplus V_{12} \oplus vars(t_{12}) \vdash \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \implies \bigwedge_{j \in (J'_{13x} \cap H')} \beta_{12j} = \beta_{13xj} \end{align*} $$

We can extend the valuation context of the variables to cover the variables of the transitions $t_1$ and variables $V_1^1$ and $V_1^2$ in the formula $(*)$. By using the statements resulting from the cases (a), (b) and (c), we get:

$$ \begin{align*} V_{13} \oplus V_{13} \oplus vars(t_{12}) \vdash \\ \mathcal{R}(s_2, s_3) \land (g_2 \land g_1^1 \land \alpha_1^1 = \beta_{2k}) \land \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 &\implies \\ \bigvee_{x \in X} \left( \begin{array}{@{}l@{}} \alpha_{12} = \alpha_{13x} \land \bigwedge_{j \in (J'_{13x} \cap H')} \beta_{12j} = \beta_{13xj} \land \\ \phantom{\alpha_{12} = \alpha_{13x} \land \bigwedge_{j \in (J'_{13x} \cap H')} \beta_{12j} = \beta_{13xj} \land} g_{3x} \land \mathcal{R}(s'_2, s'_{3x}) \{\psi_2 \oplus \psi_{3x}\} \end{array} \right) \land g_1^2 \land \alpha_1^2 = \beta_{3xk} \end{align*} $$

That can be re-written as follows:

$$ V_{12} \oplus V_{13} \oplus vars(t_{12}) \vdash \\ \mathcal{R}(s_2, s_3) \land g_{12} \land \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \implies \bigvee_{x \in X} \left( \begin{array}{@{}l@{}} \alpha_{12} = \alpha_{13x} \land \bigwedge_{j \in J'_{13x} \cap H'} \beta_{12j} = \beta_{13xj} \land \\ \phantom{\alpha_{12} = \alpha_{13x} \land \bigwedge_{j \in J'_{13x} \cap H'} \beta_{12j} = \beta_{13xj} \land} g_{13x} \land \mathcal{R}(s'_2, s'_{3x}) \{\psi_2 \oplus \psi_{3x}\} \end{array} \right) $$

Moreover, we have for any transition $t_1$ in $A_1$ relating $s_1^1$ and $s_1^{1'}$ the following:

$$ V_{12} \oplus V_{13} \oplus vars(t_{12}) \vdash \\ \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \land s_1^1 = s_1^2 \implies \bigwedge_{v_1 \in V_1} \psi_{12}(v_1^1) = \psi_{13x}(v_1^2) \land s_1^{1'} = s_1^{2'} $$
From the two previous formula, we get:

$$
\begin{align*}
& V_{12} \uplus V_{13} \uplus \mathrm{vars}(t_{12}) \vdash \\
& R(s_2, s_3) \wedge g_{12} \wedge \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \wedge s_1^1 = s_1^2 \implies \\
& \qquad \bigvee_{x \in X} \left( \begin{array}{@{}l@{}}
\alpha_{12} = \alpha_{13x} \wedge \bigwedge_{j \in J'_{13x} \wedge H'} \beta_{12j} = \beta_{13xj} \wedge g_{13x} \wedge \\
\phantom{\alpha_{12} = \alpha_{13x} \wedge \bigwedge_{j \in J'_{13x} \wedge H'} \beta_{12j} = \beta_{13xj} \wedge} \\
R(s'_2, s'_{3x}) \{\psi_2 \uplus \psi_{3x}\} \wedge \bigwedge_{v_1 \in V_1} \psi_{12}(v_1^1) = \psi_{13x}(v_1^2) \wedge s_1^{1'} = s_1^{2'}
\end{array} \right)
\end{align*}
$$

Furthermore, according to the Definition 7 (reachability, applied to the com-
posed automaton $A_1[A_2/k]$) we have, for all $t_{12} \in T_{12}$:

$$
\mathrm{vars}(t_{12}) \vdash (\check{\mathrm{A}}_{12}(s_{12}) \wedge g_{12} \implies \check{\mathrm{A}}_{12}(s'_{12}) \{\psi_{12}\})
$$

Thus, we get:

$$
\begin{align*}
& V_{12} \uplus V_{13} \uplus vars(t_{12}) \vdash \\
& \quad \mathcal{R}(s_2, s_3) \wedge g_{12} \wedge \check{\mathcal{A}}_{A_{12}}(s_{12}) \wedge \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \wedge s_1^1 = s_1^2 \implies \\
& \qquad \bigvee_{x \in X} \left( \begin{array}{@{}l@{}}
\alpha_{12} = \alpha_{13x} \wedge \bigwedge_{j \in J'_{13x} \wedge H'} \beta_{12j} = \beta_{13xj} \wedge g_{13x} \wedge \\
\phantom{\alpha_{12} = \alpha_{13x} \wedge \bigwedge_{j \in J'_{13x} \wedge H'} \beta_{12j} = \beta_{13xj} \wedge} \\
\mathcal{R}(s'_2, s'_{3x}) \{\psi_2 \uplus \psi_{3x}\} \wedge \check{\mathcal{A}}_{A_{12}}(s'_{12}) \{\psi_{12}\} \\
\phantom{\alpha_{12} = \alpha_{13x} \wedge \bigwedge_{j \in J'_{13x} \wedge H'} \beta_{12j} = \beta_{13xj} \wedge g_{13x} \wedge} \\
\wedge \bigwedge_{v_1 \in V_1} \psi_{12}(v_1^1) = \psi_{13x}(v_1^2) \wedge s_1^{1'} = s_1^{2'}
\end{array} \right)
\end{align*}
$$

Because of the independence of the substitution domains, we simplify and
get the expected formula:

$$
\begin{align*}
& V_{12} \uplus V_{13} \uplus vars(t_{12}) \vdash \mathcal{R}'(s_{12}, s_{13}) \wedge g_{12} \implies \\
& \quad \bigvee_{x \in X} \left( \alpha_{12} = \alpha_{13x} \wedge \bigwedge_{j \in J'_{13x} \wedge H'} \beta_{12j} = \beta_{13xj} \wedge g_{13x} \wedge \mathcal{R}'(s'_{12}, s'_{13x}) \{\psi_{12} \uplus \psi_{13x}\} \right)
\end{align*}
$$

Second case: Only the encompassing automaton performs a transition. $t_{12}$ is obtained by the transition $t_1^1 = \frac{(\beta_{1j}^1)^{j \in J_1^1}, g_1^1, \psi_1^1}{s_1^1 \xrightarrow{\alpha_1^1} s_1^{1'}}$ alone with the state $s_2$ unchanged, if $k \notin J_1^{1'}$

$$
t_{12} = \frac{(\beta_{1j}^1)^{j \in J_1^1}, g_1^1, \psi_1^1}{(s_1^1, s_2) \xrightarrow{\alpha_1^1} (s_1^{1'}, s_2)}
$$
The hole is not involved we can define $t_{13}$ with the same transition $t_1$ of $A_1$ (where elements of $t_1$ are the same as above modulo renaming of variables):

$$t_{13} = \frac{(\beta_{1j}^2)^{j \in J_1^{2'}} \cdot g_1^2 \cdot \psi_1^2}{(s_1^1, s_3) \xrightarrow{\alpha_1^2} (s_1^{2'}, s_3)}$$

We thus take $(t_{13x})^{x \in X} = \{t_{13}\}$. $\forall x \in X$ we have $J'_{13x} = J_1^{2'}$ and trivially:

$$\begin{align*}
J'_{13x} \cap H' &= J_1^{2'} \cap (J_1 \uplus H \setminus \{k\}) \\
&= J_1^{1'} \cap (J_1 \uplus H \setminus \{k\}) \text{ since } J_1^{2'} = J_1^{1'} \\
&= (J'_{12} \cap H')
\end{align*}$$

Moreover, we have by definition

$$\mathcal{R}'(s_{12}, s_{13}) = \mathcal{R}(s_2, s_3) \wedge \check{\mathcal{A}}_{A_{12}}(s_{12}) \wedge \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \wedge s_1^1 = s_1^2$$

Thus, because transitions $t_1^1$ and $t_1^2$ are the same:

$$\mathcal{R}'(s_{12}, s_{13}) \implies \underbrace{\mathcal{R}(s_2, s_3) \wedge \check{\mathcal{A}}_{A_{12}}(s_{12}) \wedge \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \wedge s_1^{1'} = s_1^{2'}}_{\mathcal{R}'(s_{12}^{1'}, s_{13}^{1'})}$$

Moreover, we have the following:

$$V_{12} \uplus V_{13} \uplus vars(t_{12}) \vdash \\ \quad \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \wedge s_1^1 = s_1^2 \implies \bigwedge_{v_1 \in V_1} \psi_{12}(v_1^1) = \psi_{13}(v_1^2) \wedge s_1^{1'} = s_1^{2'}$$

Furthermore, according to the Definition 7 (reachability, applied to the composed automaton $A_1$) we have, for all $t_{12} \in T_{12}$:

$$vars(t_{12}) \vdash (\check{\mathcal{A}}_{A_{12}}(s_{12}) \wedge g_{12} \implies \check{\mathcal{A}}_{A_{12}}(s_{12}^{1'}) \{\psi_{12}\})$$

Because $\alpha_{12}$ and $\alpha_{13}$ are the same, and also $\beta_{12}$ and $\beta_{13}$ are the same (modulo renaming of variables), we deduce from the above the expected formula (instantiated with X a singleton):

$$V_{12} \uplus V_{13} \uplus vars(t_{12}) \vdash \mathcal{R}'(s_{12}, s_{13}) \wedge g_{12} \implies \left( \bigwedge_{j \in J'_{13} \cap H'} \alpha_{12} = \alpha_{13} \wedge \bigwedge_{j \in J'_{13} \cap H'} \beta_{12j} = \beta_{13j} \wedge g_{13} \wedge \mathcal{R}'(s'_{12}, s'_{13}) \{\psi_{12} \uplus \psi_{13}\} \right)$$

3. Lastly, we have to prove the satisfaction of the deadlock reduction condition, i.e., for all $(s_{12}, s_{13}) \in S_{12} \times S_{13}$

$$V_{12} \uplus V_{13} \vdash \mathcal{R}'(s_{12}, s_{13}) \wedge \neg(\bigvee_{t_{12} \in \text{OT}(s_{12})} \text{guard}(t_{12})) \implies \neg(\bigvee_{t_{13} \in \text{OT}(s_{13})} \text{guard}(t_{13}))$$
Let's start with the hypothesis of the theorem stating that $A_2 \leq H A_3$, thus we have for all $(s_2, s_3) \in S_2 \times S_3$

$$V_2 \oplus V_3 \vdash \mathcal{R}(s_2, s_3) \wedge \neg(\bigvee_{t_2 \in \mathrm{OT}(s_2)} \mathrm{guard}(t_2)) \implies \neg(\bigvee_{t_3 \in \mathrm{OT}(s_3)} \mathrm{guard}(t_3))$$

By hypothesis the composition $A_1[A_2/k]$ is non-blocking, then according to the Definition 10 we have for all state $s_{12}$:

$$V_{12} \oplus \bigcup_{t_1 \in \mathrm{OT}(s_1)} vars(t_1) \vdash \left( \check{A}_{12}(s_{12}) \wedge \bigvee_{t_1 \in \mathrm{OT}(s_1)} guard(t_1) \right) \implies \bigvee_{t_{12} \in \mathrm{OT}(s_{12})} guard(t_{12})$$

Which implies

$$V_{12} \oplus \bigcup_{t_1 \in \mathrm{OT}(s_1)} vars(t_1) \vdash \neg \bigvee_{t_{12} \in \mathrm{OT}(s_{12})} guard(t_{12}) \implies \left( \neg \check{A}_{12}(s_{12}) \vee \neg \bigvee_{t_1 \in \mathrm{OT}(s_1)} guard(t_1) \right)$$

Additionally, each transition $t_{13}$ of $\mathrm{OT}(s_{13})$ is of the form $g_1 \wedge g_3 \wedge g$ with $g_1$ a guard of a transition $t_1$ of $\mathrm{OT}(s_1)$. Thus we have

$$\neg \bigvee_{t_1 \in \mathrm{OT}(s_1)} guard(t_1) \implies \neg(\bigvee_{t_{13} \in \mathrm{OT}(s_{13})} guard(t_{13}))$$

Thus we have, as $\mathcal{R}$ contains the reachability of state $s_{12}$:

$$V_{12} \oplus V_{13} \vdash \mathcal{R}'(s_{12}, s_{13}) \wedge \neg(\bigvee_{t_{12} \in \mathrm{OT}(s_{12})} \mathrm{guard}(t_{12})) \implies \\ \left( \check{A}_{12}(s_{12}) \wedge \left( \neg \check{A}_{12}(s_{12}) \vee \neg(\bigvee_{t_{13} \in \mathrm{OT}(s_{13})} \mathrm{guard}(t_{13})) \right) \right) \implies \neg(\bigvee_{t_{13} \in \mathrm{OT}(s_{13})} \mathrm{guard}(t_{13}))$$

□
# Conclusion

The work reported in this manuscript mirrors some of my research activities over the last few years. It follows a work that I have started since my PhD thesis, which continues to raise further exploration. Our long term goal is to provide a theoretical and practical framework for the design and development of reliable distributed and embedded systems.

While many approaches and techniques have been proposed to ease the reasoning about large scale distributed systems, and solutions have been effectively implemented to overcome the current limitations of verification techniques, it remains a real challenge to combine the results of such specialized techniques and to foresee their impact on open systems. Each technique exploits the characteristics of the formalism on which it is based. Some of them, use symbolic models for explicit data manipulation, to overcome the finiteness limit constraints, others allow the compositional description of systems to enable compositional verification methods. To the best of our knowledge, there is no work that combines all these techniques together. It could be because most of the languages on which they are based are not rich enough to cover all aspects, which is especially the key strength of the open pNets (and open automata) formalism.

A further important dimension of the open pNets (and open automata) model, it provides a rigorous methodology for the design of concurrent and distributed systems; it supports the vertical and the horizontal dimension of systems development through refinement and composition. However, there are very few approaches that combine both (e.g. [69]).

The work discussed in this document provides theoretical foundations for a fully tool-equipped approach and relies on the proposed bisimulation engines [111]

and SMT Solving algorithms [53]. Practically, the advocated framework is based on an approach combining symbolic operational semantic and bisimulation equivalences with deductive reasoning on the data part, and in practice combining bisimulation algorithms with SMT solvers to get automatic procedures proving behavioural properties of these open systems.

Work still needs to be done in that field, we envisage several directions for extending our proposal, both theoretically and practically. Some future research that can be considered in the short term:

* Despite the rich language of pNets, simply expressing parametrized topologies (vectors, rows, rings, matrices,...) that are very useful in real applications is still very difficult. Expressing them requires to concretely extend the pNets model, by introducing a notion of topological parameters and spatial structures. Doing so requires enriching the automata description formalism, but also the synchronization mechanism.

* The composition operation of open automata is a kind of refinement that allows for an extension of the functionality. However, this refinement is not safe with respect to trace safety, because it is possible to introduce new traces in the implementation (necessarily because the intended use is that the specification model is a partial specification that is completed). However, the ability to complete the specification and preserve behaviours is a property that is sometimes required in some applications (e.g. [96]). There is a need to investigate under what conditions (structural or syntactic restrictions) the preservation can be guaranteed.

* The development of practical tools that supports equivalence checking of open pNets (open automata)
models for verifying real-life concurrent systems.
In fact, bisimulation algorithms have already been
implemented but they require further improvement.
The challenges for the implementation, in the con-
text of our symbolic systems, are not so much algo-
rithmic complexity, as was the case with classical
weak bisimulation on finite models, but decidabil-
ity and termination. The naive approach, using an
explicit construction of the weak transition, may
in itself introduce non-termination, so the adopted
solution was a direct implementation of the weak
bisimulation definition [111], without construct-
ing the weak automata beforehand, but searching
on demand to construct the required weak tran-
sitions. It may be more effective to explore other
more pragmatic approaches of weak bisimulation
over weak automata.
Bibliography

[1] Martín Abadi and Leslie Lamport. The existence of refinement mappings. *Theoretical Computer Science*, 82(2):253-284, 1991.

[2] Martín Abadi and Leslie Lamport. Conjoining specifications. *ACM Transactions on Programming Languages and Systems*, 17(3):507-535, 1995.

[3] Jean-Raymond Abrial. *The B-book - assigning programs to meanings*. Cambridge University Press, 1996.

[4] Marco Aldinucci, Carlo Bertolli, Sonia Campa, Massimo Coppola, Marco Vanneschi, and Corrado Zoccolo. Autonomic Grid Components: the GCM Proposal and Self-optimising ASSIST Components. In *Joint Workshop on HPC Grid programming Environments and COmponents and Component and Framework Technology in High-Performance and Scientific Computing at HPDC'15*, June 2006.

[5] Rajeev Alur and Thomas A. Henzinger. Reactive modules. *Formal Methods in System Design*, 15(1):7-48, 1999.

[6] Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, and Moshe Y. Vardi. Alternating refinement relations. In Davide Sangiorgi and Robert de Simone, editors, *CONCUR: Concurrency Theory*, pages 163-178. Springer Berlin Heidelberg, 1998.

[7] Rabéa Ameur-Boulifa, Ana R. Cavalli, and Stephane Maag. Verifying complex software control systems from test objectives: Application to the ETCS system. In Marten van Sinderen and Leszek A. Maciaszek, editors, *Proceedings of the 14th International Conference on Software Technologies, ICSOFT*, pages 397-406. SciTePress, 2019.

[8] Rabéa Ameur-Boulifa, Raluca Halalai, Ludovic Henrio, and Eric Madelaine. Verifying safety of fault-tolerant distributed components. In *International Symposium on Formal Aspects of Component Software*, Lecture Notes in Computer Science. Springer, September 2011.

[9] Rabéa Ameur-Boulifa, Raluca Halalai, Ludovic Henrio, and Eric Madelaine. Verifying safety of fault-tolerant distributed components. In Farhad Arbab and Peter Csaba Ölveczky, editors, *Formal Aspects of Component Software*, pages 278-295. Springer Berlin Heidelberg, 2012.

[10] Rabéa Ameur-Boulifa, Ludovic Henrio, Oleksandra Kulankhina, Eric Madelaine, and Alexandra Savu. Behavioural semantics for asynchronous components. *Journal of Logical and Algebraic Methods in Programming*, 89:1-40, 2017.

[11] Rabéa Ameur-Boulifa, Ludovic Henrio, and Eric Madelaine. Compositional equivalences based on open pNets. *Journal of Logical and Algebraic Methods in Programming*, 131:100842, 2023.

[12] Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, and Richard J. Trefler. Assume-guarantee based compositional reasoning for synchronous timing diagrams. TACAS 2001, pages 465-479, Berlin, Heidelberg, 2001. Springer-Verlag.

[13] Henrik Reif Andersen. Partial model checking. *Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science*, pages 398-407, 1995.
[14] André Arnold. Synchronised behaviours of processes and rational relations. *Acta Informatica*, 17:21–29, 1982.

[15] Isabelle Attali, Tomás Barros, and Eric Madelaine. Parameterized specification and verification of the chilean electronic invoices system. In *XXIV International Conference of the Chilean Computer Science Society*, pages 14–25. IEEE Computer Society, 2004.

[16] Didier Austry and Gérard Boudol. Algebre de processus et synchronisation. Research Report RR-0187, INRIA, 1983.

[17] Ralph-Johan Back and Joakim von Wright. *Refinement Calculus - A Systematic Introduction*. Graduate Texts in Computer Science. Springer, 1998.

[18] J.C.M. Baeten. A brief history of process algebra. *Theoretical Computer Science*, 335(2):131–146, 2005. Process Algebra.

[19] T. Barros, A. Cansado, E. Madelaine, and M. Rivera. Model checking distributed components : The Vercors platform. In *3rd workshop on Formal Aspects of Component Systems (FACS’06)*, volume 182, pages 3–16, Prague, Czech Republic, Sep 2007. ENTCS.

[20] Tomás Barros. *Spécification et vérification formelles des systèmes de composants répartis. (Formal specification and verification of distributed component systems)*. PhD thesis, University of Nice Sophia Antipolis, France, 2005.

[21] Tomás Barros, Rabéa Ameur-Boulifa, Antonio Cansado, Ludovic Henrio, and Eric Madelaine. Behavioural models for distributed Fractal components. *Annales des Télécommunications*, 64(1-2):25–43, 2009.

[22] Tomás Barros, Rabéa Boulifa, Antonio Cansado, Ludovic Henrio, and Eric Madelaine. Behavioural models for distributed fractal components (extended version). Research Report RR-6491, INRIA, 04 2008.

[23] Tomás Barros, Rabéa Boulifa, and Eric Madelaine. Parameterized models for distributed Java objects. In *Formal Techniques for Networked and Distributed Systems FORTE 2004*, volume LNCS 3235, pages 43–60, Madrid, September 2004. Spinger Verlag.

[24] F. Baude, D. Caromel, N. Maillard, and E.N. Mathias. Hierarchical mpi-like programming using gcm components as implementation support. Selected and presented at the CoreGRID workshop: Grid Systems, Tools and Environments, Grids@work II conference, Dec. 2006.

[25] Françoise Baude, Denis Caromel, Cédric Dalmasso, Marco Danelutto, Vladimir Getov, Ludovic Henrio, and Christian Pérez. GCM: A Grid Extension to Fractal for Autonomous Distributed Components. *Annals of Telecommunications*, 64(1):5–24, 2009.

[26] Sebastian S. Bauer, Philip Mayer, Andreas Schroeder, and Rolf Hennicker. On Weak Modal Compatibility, Refinement, and the MIO Workbench. In Javier Esparza and Rupak Majumdar, editors, *Tools and Algorithms for the Construction and Analysis of Systems*, pages 175–189. Springer Berlin Heidelberg, 2010.

[27] Françoise Bellegarde, Célina Charlet, and Olga Kouchnarenko. *How to Compute the Refinement Relation for Parameterized Systems*, pages 181–209. Kluwer Academic Publishers, USA, 2004.

[28] Françoise Bellegarde, Jacques Julliand, and Olga Kouchnarenko. Ready-simulation is not ready to express a modular refinement relation. In Tom Maibaum, editor, *Fundamental Approaches to Software Engineering*, pages 266–283, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg.

[29] Bernard Berthomieu, Jean-Paul Bodeveix, Patrick Farail, M Filali, Hubert Garavel, Pierre Gaufillet, Frederic Lang, and François Vernadat. Fiacre: an Intermediate Language for Model Verification in the Topcased Environment. In *4th European Congress ERTS Embedded Real Time Software*, January 2008.
[30] Tommaso Bolognesi and Ed Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14(1):25-59, 1987.

[31] Johannes Borgström, Sébastien Briais, and Uwe Nestmann. Symbolic Bisimulation in the Spi Calculus. In CONCUR - Concurrency Theory, 15th International Conference, volume 3170 of LNCS, pages 161-176. Springer, 2004.

[32] R. Boulifa and E. Madelaine. Model generation for distributed Java programs. In E. Astesiano N. Guelfi and G. Reggio, editors, Workshop on scientiFic engineering of Distributed Java applications, Luxembourg, nov 2003. Springer-Verlag, LNCS 2952.

[33] Rabéa Boulifa. Génération de modèles comportementaux des applications réparties. PhD thesis, University of Nice - Sophia Antipolis - UFR Sciences, December 2004.

[34] Rabéa Boulifa, Ludovic Henrio, and Eric Madelaine. Behavioural models for group communications. In WCSI-10: International Workshop on Component and Service Interoperability, number 37 in EPTCS, pages 42-56, 2010.

[35] Mario Bravetti and Gianluigi Zavattaro. Asynchronous session subtyping as communicating automata refinement. Software and Systems Modeling, 20(2):311-333, 2021.

[36] Ed Brinksma, Giuseppe Scollo, and Chris Steenbergen. Lotos Specifications, Their Implementations and Their Tests, pages 468-479. IEEE Computer Society Press, Washington, DC, USA, 1995.

[37] S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A Theory of Communicating Sequential Processes. J. ACM, 31(3):560 - 599, Jun 1984.

[38] Eric Bruneton, Thierry Coupaye, Matthieu Leclercq, Vivien Quéma, and Jean-Bernard Stefani. The FRACTAL component model and its support in Java. Software Practice and Experience, 36(11-12):1257-1284, 2006.

[39] Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, 1986.

[40] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 10²⁰ states and beyond. Information and Computation, 98(2):142-170, 1992.

[41] Maria Grazia Buscemi and Ugo Montanari. Open Bisimulation for the Concurrent Constraint Pi-Calculus. In ESOP 2008 - Programming Languages and Systems, 17th European Symposium on Programming, volume 4960 of Lecture Notes in Computer Science, pages 254-268. Springer, 2008.

[42] Muffy Calder and Carron Shankland. A symbolic semantics and bisimulation for full lotos. In International Conference on Formal Techniques for Networked and Distributed Systems, pages 185-200. Springer, 2001.

[43] Antonio Cansado, Denis Caromel, Ludovic Henrio, Eric Madelaine, Marcela Rivera, and Emil Salageanu. A Specification Language for Distributed Components Implemented in GCM/ProActive, pages 418-448. Springer Berlin Heidelberg, Berlin, Heidelberg, 2008.

[44] Antonio Cansado and Eric Madelaine. Specification and verification for grid component-based applications: from models to tools. In Frank S. de Boer, Marcello M. Bonsangue, and Eric Madelaine, editors, FMCO 2008, number 5751 in LNCS. Springer-Verlag, 2009.

[45] Sarah Chabane, Rabéa Ameur-Boulifa, and Mohamed Mezghiche. Rethinking of I/O-Automata Composition. In Forum on specification & Design Languages (FDL), Verona, Italy, September 2017.

[46] Shing-Chi. Cheung and Jeff Kramer. compositional reachability analysis of finite-state distributed systems with user-specified constraints. In Proceedings of the 3rd ACM SIGSOFT Symposium on Foundations of Software Engineering, SIGSOFT '95, pages 140-150, New York, NY,
USA, 1995. Association for Computing Machinery.

[47] Shing Chi Cheung and Jeff Kramer. Context constraints for compositional reachability analysis. *ACM Transactions on Software Engineering and Methodology*, 5(4):334–377, 1996.

[48] Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In E. Allen Emerson and Aravinda Prasad Sistla, editors, *Computer Aided Verification*, pages 154–169, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg.

[49] Rance Cleaveland and Oleg Sokolsky. CHAP-TER 6 - Equivalence and Preorder Checking for Finite-State Systems. In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, *Handbook of Process Algebra*, pages 391–424. Elsevier Science, Amsterdam, 2001.

[50] CoreGRID Programming Model Virtual Institute. Programming models for the single gcm component: a survey, Sep. 2006. Deliverable D.PM.06.

[51] Luca de Alfaro. Game Models for Open Systems. In Nachum Dershowitz, editor, *Verification: Theory and Practice*, volume 2772 of Lecture Notes in Computer Science, pages 269–289. Springer, 2003.

[52] Luca de Alfaro and Thomas A. Henzinger. Interface automata. In A Min Tjoa and Volker Gruhn, editors, *Proceedings of the 8th European Software Engineering Conference held jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering 2001*, Vienna, Austria, September 10-14, 2001, pages 109–120. ACM, 2001.

[53] Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Z3: an efficient SMT solver. In *TACAS*, volume 4963 of *Lecture Notes in Computer Science*, pages 337–340. Springer, 2008.

[54] Stéphanie Delaune, Steve Kremer, and Mark Ryan. Symbolic Bisimulation for the Applied Pi Calculus.

In *FSTTCS 2007 - Foundations of Software Technology and Theoretical Computer Science, 27th International Conference*, volume 4855 of LNCS, pages 133–145. Springer, 2007.

[55] José Dihego, Augusto Sampaio, and Marcel Oliveira. A refinement checking based strategy for component-based systems evolution. *Journal of Systems and Software*, 167:110598, 2020.

[56] Edsger W. Dijkstra. *A discipline of programming*. Series in automatic computation. Prentice-Hall, 1976.

[57] E. Allen Emerson and Edmund M. Clarke. Characterizing correctness properties of parallel programs using fixpoints. In Jaco De Bakker and Jan Van Leeuwen, editors, *Automata, Languages and Programming*, pages 169–181. Springer Berlin Heidelberg, 1980.

[58] Rik Eshuis and Maarten M. Fokkinga. Comparing Refinements for Failure and Bisimulation Semantics. *Fundamenta Informaticae*, 52(4):297–321, 2002.

[59] Yuan Feng, Yuxin Deng, and Mingsheng Ying. Symbolic bisimulation for quantum processes. *ACM Transactions on Computational Logic (TOCL)*, 15(2):14, 2014.

[60] Hubert Garavel. Revisiting sequential composition in process calculi. *Journal of Logical and Algebraic Methods in Programming*, 84(6):742–762, 2015. "Special Issue on Open Problems in Concurrency Theory".

[61] Hubert Garavel, Frédéric Lang, and Radu Mațeescu. An overview of CADP 2001. *European Association for Software Science and Technology Newsletter*, 4:13–24, aug 2002.

[62] Hubert Garavel, Frédéric Lang, and Radu Mațeescu. Compositional verification of asynchronous concurrent systems using cadp. *Acta Informatica*, 52(4–5):337–392, jun 2015.

[63] Hubert Garavel, Frédéric Lang, and Laurent Mounier. Compositional Verification in Action.
In Falk Howar and Jiří Barnat, editors, *Formal Methods for Industrial Critical Systems*, pages 189–210, Cham, 2018. Springer International Publishing.

[64] Nuno Gaspar, Ludovic Henrio, and Eric Madelaine. Formally reasoning on a reconfigurable component-based system - A case study for the industrial world. In José Luiz Fiadeiro, Zhiming Liu, and Jinyun Xue, editors, *Formal Aspects of Component Software - 10th International Symposium, FACS 2013*, volume 8348 of LNCS, pages 137–156. Springer, 2013.

[65] Simon J. Gay and Malcolm Hole. Subtyping for session types in the pi calculus. *Acta Informatica*, 42(2-3):191–225, 2005.

[66] Dimitra Giannakopoulou, Kedar S. Namjoshi, and Corina S. Păsăreanu. *Compositional Reasoning*, pages 345–383. Springer International Publishing, Cham, 2018.

[67] Susanne Graf, Bernhard Steffen, and Gerald Lüttgen. Compositional minimisation of finite state systems using interface specifications. *Formal Aspects of Computing*, 8(5):607–616, sep 1996.

[68] Jan Friso Groote, Jeroen J. A. Keiren, Bas Luttik, Erik P. de Vink, and Tim A. C. Willemse. Modelling and Analysing Software in mCRL2. In Farhad Arbab and Sung-Shik Jongmans, editors, *Formal Aspects of Component Software*, pages 25–48, Cham, 2020. Springer International Publishing.

[69] Serge Haddad, Rolf Hennicker, and Mikael H. Møller. Specification of Asynchronous Component Systems with Modal I/O-Petri Nets. In *8th Symposium on Trustworthy Global Computing (TGC)*, volume LNCS 8358, pages 219–234, Buenos Aires, Argentina, 2014. Springer.

[70] D. Harel and A. Pnueli. On the development of reactive systems. In Krzysztof R. Apt, editor, *Logics and Models of Concurrent Systems*, pages 477–498, Berlin, Heidelberg, 1985. Springer Berlin Heidelberg.

[71] David Harel. Statecharts: a visual formalism for complex systems. *Science of Computer Programming*, 8(3):231–274, 1987.

[72] Matthew Hennessy and Huimin Lin. Symbolic bisimulations. *Theoretical Computer Science*, 138(2):353–389, 1995.

[73] Ludovic Henrio, Oleksandra Kulankhina, Siqi Li, and Eric Madelaine. *Integrated Environment for Verifying and Running Distributed Components*, volume 9633 of *Fundamental Approaches to Software Engineering*, pages 66–83. Eindhoven, Netherlands, Apr 2016.

[74] Ludovic Henrio, Eric Madelaine, and Min Madelaine. *pnets: An expressive model for parameterised networks of processes*. In Masoud Daneshtalab, Marco Aldinucci, Ville Leppänen, Johan Lilius, and Mats Brorsson, editors, *23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP*, pages 492–496. IEEE Computer Society, 2015.

[75] Ludovic Henrio, Eric Madelaine, and Min Zhang. A Theory for the Composition of Concurrent Processes. In Elvira Albert and Ivan Lanese, editors, *36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)*, volume LNCS-9688, pages 175–194, Heraklion, Greece, June 2016.

[76] C. A. R. Hoare. Communicating sequential processes. *Commun. ACM*, 21(8):666–677, 1978.

[77] C.A.R. Hoare. *Communicating Sequential Processes*. Prentice-Hall International Series in Computer Science. Prentice Hall, 1985.

[78] Hans Hüttel and Kim Guldstrand Larsen. The use of static constructs in A modal process logic. In *Logic at Botik '89, Symposium on Logical Foundations of Computer Science*, volume 363 of *Lecture Notes in Computer Science*, pages 163–180. Springer, 1989.
[79] Anna Ingólfsdóttir and Huimin Lin. A symbolic approach to value-passing processes. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, *Handbook of Process Algebra*, pages 427–478. North-Holland/Elsevier, 2001.

[80] Olga Kouchnarenko and Arnaud Lanoix. How to verify and exploit a refinement of component-based systems. In Irina Virbitskaite and Andrei Voronkov, editors, *Perspectives of Systems Informatics*, pages 297–309. Springer Berlin Heidelberg, 2007.

[81] Jean-Pierre Krimm and Laurent Mounier. Compositional state space generation from lotos programs. In Ed Brinksma, editor, *Tools and Algorithms for the Construction and Analysis of Systems*, pages 239–258, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg.

[82] Kåre J. Kristoffersen, François Laroussinie, Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. A compositional proof of a real-time mutual exclusion protocol. In Michel Bidoit and Max Dauchet, editors, *TAPSOFT: Theory and Practice of Software Development, 7th International*, volume 1214 of LNCS, pages 565–579. Springer, 1997.

[83] Kim Guldstrand Larsen and Bent Thomsen. A modal process logic. [1988] *Proceedings. Third Annual Information Symposium on Logic in Computer Science*, pages 203–210, 1988.

[84] Kim Guldstrand Larsen and Liu Xinxin. Compositionality through an operational semantics of contexts. *Journal of Logic and Computation*, 1(6):761–795, 1991.

[85] Huimin Lin. Symbolic transition graph with assignment. In Ugo Montanari and Vladimiro Sassetto, editors, *CONCUR: Concurrency Theory*, pages 50–65. Springer Berlin Heidelberg, 1996.

[86] Jørn Lind-Nielsen, Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kåre J. Kristoffersen, and Kim Guldstrand Larsen. Verification of large state/event systems using compositionality and dependency analysis. In Bernhard Steffen, editor, *Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS*, volume 1384 of Lecture Notes in Computer Science, pages 201–216. Springer, 1998.

[87] Jia Liu and Huimin Lin. A Complete Symbolic Bisimulation for Full Applied Pi Calculus. In *SOFSEM - 36th Conference on Current Trends in Theory and Practice of Computer Science*, volume 5901, pages 552–563. Springer, 2010.

[88] Hong-Viet Luong, Thomas Lambolais, and Anne-Lise Courbis. Implementation of the Conformance Relation for Incremental Development of Behavioural Models. In Krzysztof Czarnecki, Ileana Ober, Jean-Michel Bruel, Axel Uhl, and Markus Völter, editors, *Model Driven Engineering Languages and Systems, 11th International Conference, MODELS*, volume 5301 of LNCS, pages 356–370. Springer, 2008.

[89] Radu Mateescu, Pascal Poizat, and Gwen Salaün. Behavioral Adaptation of Component Compositions based on Process Algebra Encodings. In *Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE)*, pages 385–388, Atlanta, United States, 2007.

[90] K. L. McMillan. A compositional rule for hardware design refinement. In Orna Grumberg, editor, *Computer Aided Verification*, pages 24–35. Springer Berlin Heidelberg, 1997.

[91] R. Milner. *Communication and Concurrency*. Int. Series in Computer Science. Prentice-Hall, Englewood Cliffs, New Jersey, 1989. SU Fisher Research 511/24.

[92] Robin Milner. *A Calculus of Communicating Systems*, volume 92 of Lecture Notes in Computer Science. Springer, 1980.

[93] Robin Milner. *A Calculus of Communicating Systems*. Springer-Verlag, Berlin, Heidelberg, 1982.
[94] Robin Milner. Calculi for synchrony and asynchrony. *Theoretical Computer Science*, 25(3):267–310, 1983.

[95] Robin Milner. *Communication and Concurrency*. Int. Series in Computer Science. Prentice-Hall, Englewood Cliffs, New Jersey, 1989. SU Fisher Research 511/24.

[96] Hocine Mokrani, Rabéa Ameur-Boulifa, and Emmanuelle Encrenaz-Tiphène. Assisting refinement in system-on-chip design. In *FDL*, pages 1–6. IEEE, 2013.

[97] Matthieu Morel. *Composants pour la grille. (Components for grid computing)*. PhD thesis, University of Nice Sophia Antipolis, France, 2006.

[98] OMG. Unified Modeling Language (UML), 2011.

[99] David Park. Concurrency and automata on infinite sequences. In Peter Deussen, editor, *Theoretical Computer Science*, pages 167–183, Berlin, Heidelberg, 1981. Springer Berlin Heidelberg.

[100] A. Pnueli. *Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends*, pages 510–584. pringer Berlin Heidelberg, Berlin, Heidelberg, 1986.

[101] Pascal Poizat and Gwen Salaün. Adaptation of open component-based systems. In Marcello M. Bonsangue and Einar Broch Johnsen, editors, *Formal Methods for Open Object-Based Distributed Systems*, pages 141–156. Springer Berlin Heidelberg, 2007.

[102] Christian Prehofer. Behavioral refinement and compatibility of statechart extensions. *Electronic Notes in Theoretical Computer Science*, 295:65–78, 2013.

[103] Xudong Qin, Simon Bliudze, Eric Madelaine, Zechen Hou, Yuxin Deng, and Min Zhang. SMT-based generation of symbolic automata. *Acta Informatica*, 57:627–656, May 2020.

[104] Xudong Qin, Simon Bliudze, Eric Madelaine, and Min Zhang. Using SMT engine to generate symbolic automata. In *18th International Workshop on Automated Verification of Critical Systems (AVOCS)*. Electronic Communications of the EASST, 2018.

[105] Davide Sangiorgi. On the origins of bisimulation and coinduction. *ACM Transactions on Programming Languages and Systems*, 31(4), May 2009.

[106] Joseph Sifakis. A unified approach for studying the properties of transition systems. *Theoretical Computer Science*, 18(3):227–258, 1982.

[107] Rishabh Singh, Dimitra Giannakopoulou, and Corina Păsăreanu. Learning component interfaces with may and must abstractions. In Tayssir Touili, Byron Cook, and Paul Jackson, editors, *Computer Aided Verification*, pages 527–542. Springer Berlin Heidelberg, 2010.

[108] Kuo-Chung Tai and P.V. Koppol. An incremental approach to reachability analysis of distributed programs. In *Proceedings of 1993 IEEE 7th International Workshop on Software Specification and Design*, pages 141–150, 1993.

[109] Rob J. van Glabbeek. The Linear Time - Branching Time Spectrum I. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, *Handbook of Process Algebra*, pages 3–99. North-Holland/Elsevier, 2001.

[110] Moshe Y. Vardi. Verification of open systems. In S. Ramesh and G. Sivakumar, editors, *Foundations of Software Technology and Theoretical Computer Science*, pages 250–266. Springer Berlin Heidelberg, 1997.

[111] Biyang Wang, Eric Madelaine, and Min Zhang. Symbolic Weak Equivalences: Extension, Algorithms, and Minimization - Extended version. Research Report RR-9389, Inria, Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France ; East China Normal University (Shanghai), January 2021.
[112] Glynn Winskel. On the Compositional Checking of Validity (Extended Abstract). In *Proceedings on Theories of Concurrency: Unification and Extension*, CONCUR, pages 481–501. Springer-Verlag, 1990.

[113] Fei Xie, Guowu Yang, and Xiaoyu Song. Compositional reasoning for hardware/software co-verification. In Susanne Graf and Wenhui Zhang, editors, *Automated Technology for Verification and Analysis*, pages 154–169. Springer Berlin Heidelberg, 2006.

[114] Lianyi Zhang, Qingdi Meng, and Kueiming Lo. Compositional abstraction refinement for component-based systems. *Journal of Applied Mathematics*, 2014:1–12, 2014.