# Compositional Equivalences Based on Open pNets

Rabéa Ameur-Boulifa, Ludovic Henrio, Eric Madelaine

► To cite this version:

Rabéa Ameur-Boulifa, Ludovic Henrio, Eric Madelaine. Compositional Equivalences Based on Open pNets. Journal of Logical and Algebraic Methods in Programming, 2022, 131, pp.100842. 10.1016/j.jlamp.2022.100842. hal-03894031v2

HAL Id: hal-03894031

https://hal.science/hal-03894031v2

Submitted on 12 Dec 2022

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

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

<figure><img src="image_1.png" /></figure>
# Compositional Equivalences Based on Open pNets

Rabéa Ameur-Boulifa

LTCI, Télécom Paris, Institut Polytechnique de Paris, France

Ludovic Henrio*

Univ Lyon, EnsL, UCBL, CNRS, Inria, LIP, F-69342, LYON Cedex 07, France.

Eric Madelaine

INRIA Sophia Antipolis Méditérannée, UCA, BP 93, 06902 Sophia Antipolis, France

## Abstract

Establishing equivalences between programs is crucial both for verifying correctness of programs and for justifying optimisations and program transformations. There exist several equivalence relations for programs, and bisimulations are among the most versatile of these equivalences. Among bisimulations one distinguishes strong bisimulation that requires that each action of a program is simulated by a single action of the equivalent program, and weak bisimulation that allows some of the actions to be invisible, and thus not simulated.

pNet is a generalisation of automata that model open systems. They feature variables and hierarchical composition. Open pNets are pNets with holes, i.e. placeholders that can be filled later by sub-systems. However, there is no standard tool for defining the semantics of an open system in this context. This article first defines *open automata* that are labelled transition systems with parameters and holes. Relying on open automata, it then defines bisimilarity relations for the comparison of systems specified as pNets. We first present a strong bisimilarity for open pNets called FH-bisimilarity. Next we offer an equivalence relation similar to the classical *weak bisimulation* equivalence, and study its properties. Among these properties we are interested in compositionality: if two systems are proven equivalent they will be indistinguishable by their context, and they will also be indistinguishable when their holes are filled with equivalent systems. We identify sufficient conditions to ensure compositionality of strong and weak bisimulation. The contributions of this article are illustrated using a transport protocol as running example.

**Keywords:** Bisimulation, compositionality, automata, semantics.

<footnote>*Corresponding author</footnote>

<footnote>Email addresses: rabea.ameur-boulifa@telecom-paris.fr (Rabéa Ameur-Boulifa), ludovic.henrio@cnrs.fr (Ludovic Henrio), eric.madelaine@inria.fr (Eric Madelaine)</footnote>
# 1. Introduction

In the nineties, several works extended the basic behavioural models based on labelled transition systems to address value-passing or parameterised systems, using various symbolic encodings of the transitions [15, 35]. These works use the term *parameter* to designate variables whose value have a strong influence on the system structure and behaviour. In parameterised systems, parameters can typically be the number of processes in the system or the way they interact. In [32, 25], Lin, Ingolfsdottir and Hennessy developed a full hierarchy of bisimulation equivalences, together with a proof system, for value passing CCS, including notions of symbolic behavioural semantics and various symbolic bisimulations (early and late, strong and weak, and their congruent versions). They also extended this work to models with explicit assignments [38]. Separately Rathke [26] defined another symbolic semantics for a parameterised broadcast calculus, together with strong and weak bisimulation equivalences, and developed a symbolic model-checker based on a tableau method for these processes. Thirty years later, no verification platform uses this kind of approaches to provide proof methods for value-passing processes or open process expressions, perhaps because of the difficulty to apply these methods on industrial systems.

This article provides a theoretical background that allows us to implement such a verification platform. We build upon the concept of pNets that we have employed to give a behavioural semantics of distributed components and verify the correctness of distributed applications in the past 15 years. pNets is a low level semantic framework for expressing the behaviour of various classes of distributed languages, and as a common internal format for our tools. pNets support the specification of parameterised hierarchical labelled transition systems: labelled transition systems with parameters can be combined hierarchically.

We develop here a semantics for a model of interacting processes with parameters and holes. Our approach is originally inspired from Structured Operational Semantics with conditional premises as in [20, 45]. But we aim at a more constructive and implementable approach to compute the semantics (intuitively transitions including first order predicates) and to check equivalences for these open systems. The main interest of our symbolic approach is to define a method to prove properties directly on open structures; these properties will then be preserved by any correct instantiation of the holes. As a consequence, our model allows us to reason about composition operators as well as about realistic distributed systems. The parametric nature of the model and the properties of compositionality of the equivalence relations are thus the main strengths of our approach.

*pNets*. pNet is a convenient model to model concurrent systems in a hierarchical and parameterised way. The coordination between processes is expressed as synchronisation vectors that allow for the definition of complex and expressive synchronisation patterns. Open pNets are pNets for which some elements in the
hierarchy are still undefined, such undefined elements are called *holes*. A hole
can be *filled* later by providing another pNet. This article first defines pNets
and illustrates with an example how they can be used to provide the model of
a communicating system.

*A semantics for open pNets based on open automata.* The semantics of pNets
can be expressed as a translation to a labelled transition system (LTS), but only
if the pNet has no parameter and no hole. Adding parameters to a LTS is quite
standard [38] but enabling holes inside LTSs is not a standard notion.

To define a semantics for open pNets we thus need LTSs that have both
standard variable parameters, and process parameters, i.e. holes that can be
filled by processes. We call such LTSs with parameters and holes *open automata*.
The main goal of this article is to define the theory behind open automata and
to use them to provide a semantics and prove compositionality properties for
open pNets. The transitions of open automata are much more complex than
transitions of an LTS as the firing of a transition depends on parameters and
actions that are symbolic. This article defines the notion of *open transition*,
namely a transition that is symbolic in terms of parameters and coordinated
actions.

Note that even if open transitions look similar to the notion of Transition
System Specification [23, 22] and other forms of SOS rules, they are *not* struc-
tural rules, but rules defining the behaviour of the global states of the system.

Unlike pNets, open automata are not hierarchical structures, we consider
them here as a mathematical structure that is convenient for formal reasoning
but not adapted to the definition of a complex and structured system. Open
transitions are expressed in terms of logics while the communication in pNets
is specified as synchronisation vectors that specify synchronised actions. Open
automata could alternatively be seen as an algebra that can be studied inde-
pendently from its application to pNets but their compositionality properties
make more sense in a hierarchical model like pNets.

Previous works and contribution

While most of our previous works relied on closed, fully-instantiated se-
mantics [6, 2, 27], it is only recently that we could design a first version of a
parameterised semantics for pNets with a strong bisimulation equivalence [28].
This article builds upon this previous parameterised semantics and provides a
clean and complete version of the semantics with a slightly simplified formalism
that makes proofs easier. It also adds a notion of global state to automata.
Moreover, in [28] the study of compositionality was only partial, and in partic-
ular the proof that bisimilarity is an equivalence is one new contribution of this
article and provides a particularly interesting insight on the semantic model
we use. The new formalism allowed us to extend the work and define weak
bisimulation for open automata, which is entirely new. This allows us to define
a weak bisimulation equivalence for open pNets with valuable compositionality
properties. To summarise, the contribution of this paper are the following:
* The definition of open automata: an algebra of parameterised automata with holes, and a strong bisimulation relation. This is an adaptation of [28] with an additional result stating that strong FH-bisimilarity is indeed an equivalence relation.

* A semantics for open pNets expressed as translation to open automata. This is an adaptation of [28] with a complete proof that strong FH-bisimilarity is compositional.

* A theory of weak bisimulation for open automata, and a study of its properties. It relies on the definition of weak open transitions that are derived from transitions of the open automaton by concatenating invisible action transitions with one (visible or not) action transition. The precise and sound definition of the concatenation is also a major contribution of this article.

* A resulting weak FH-bisimilarity equivalence for open pNets and a simple static condition on synchronisation vectors inside pNets that is sufficient to ensure that weak FH-bisimilarity is compositional.

* An illustrative example based on a transport protocol, showing the construction of the weak open transitions, and the proof of weak FH-bisimulation.

## What is new about open automata bisimulation?

Bisimulation over a symbolic and open model like open pNets or open automata is different from the classical notion of bisimulation because it cannot rely on the equality over a finite set of action labels. Classical bisimulations require to exhibit, for each transition of one system, a transition of the other system that simulates it. Instead, bisimulation for open automata relies on the simulation of each open transition of one automaton by a set of open transitions of the other one, that should cover all the cases where the original transition can be triggered. This is similar to the early and late symbolic bisimulation equivalences for value-passing CCS [25], though we use more general definitions in our setting.

Compositionality of bisimilarity in our model comes from the specification of the interactions, including actions of the holes. This is quite different from the works on contextual equivalences, e.g. [35, 36]; we will provide a detailed comparison in Section 6. In pNets, synchronisation vectors define the possible interactions between the pNet that fills the hole and the surrounding pNets. In open automata, this is reflected by symbolic hypotheses that depend on the actions of the holes. This additional specification is the price to pay to obtain the compositionality of bisimilarity that cannot be guaranteed in traditional process algebras.

This approach also allows us to specify a sufficient condition on transitions to make weak bisimilarity compositional; namely it is not possible to synchronise on invisible actions from the holes or prevent them to occur. This is loosely related to works on the syntactic conditions on SOS rules to check whether
weak bisimulation is a congruence for some process algebra operators [23]. Our approach is semantical and more global: our sufficient condition applies to all the synchronisations at a given composition level of an (open) system and not on individual rules. It is expressed on the open automaton (see Definition 15).

### Structure

This article is organised as follows. Section 2 provides the definition of pNets and introduces the notations used in this paper, including the definition of open pNets. Section 3 defines open automata, i.e. automata with parameters and transitions conditioned by the behaviour of “holes”; a strong bisimulation equivalence for open automata is also presented in this section. Section 4 gives the semantics of open pNets expressed as open automata, and states compositionality properties of strong bisimilarity for open pNets. Section 5 defines a weak bisimulation equivalence on open automata and derives weak bisimilarity for pNets, together with compositionality properties of weak bisimilarity. Finally, Section 6 discusses related works and Section 7 concludes the paper.

## 2. Background and Notations

This section introduces the notations we will use in this article, and recalls the definition of pNets [28] with an informal semantics of the pNet constructs. The only significant difference compared to our previous definitions (from [28]) is that we remove here the restriction that was stating that variables should be local to a state of a labelled transition system.

### 2.1. Notations

*Term algebra.* Our models rely on a notion of parameterised actions, which are symbolic expressions using data types and variables. As our model aims at encoding the low-level behaviour of possibly very different programming languages, we do not want to impose one specific algebra for denoting actions, nor any specific communication mechanism. So we leave the constructors of the algebra that will be used to build expressions and actions unspecified. Moreover, we use a generic *action interaction* mechanism, based on (some sort of) unification between two or more action expressions, to express various kinds of communication or synchronisation mechanisms.

Formally, we assume the existence of a term algebra $\mathbb{T}$, and denote as $\Sigma$ the signature of the data and action constructors. Within $\mathbb{T}$, we distinguish a set of data expressions $\mathbb{E}$, including a set of boolean expressions $\mathbb{B}$ ($\mathbb{B} \subseteq \mathbb{E}$), and a set of action expressions called the action algebra $\mathbb{A}$, with $\mathbb{A} \subseteq \mathbb{T}, \mathbb{E} \cap \mathbb{A} = \emptyset$; naturally action terms will use data expressions as sub-terms<fnref n="1" />. The function $vars(t)$ identifies the set of variables in a term $t \in \mathbb{T}$.

<footnote n="1">¹In our tools, we use datatypes for the different kinds of terms. In this article, we use different sets of variables for terms of different kinds.</footnote>
We let $e_i$ range over expressions ($e_i \in \mathbb{E}$), op be operators, and $x_i$ and $y_i$ range over variable names. We additionally rely on a set of action names, ranged over by a, b, .... We define two kinds of parameterised actions. The first kind supports two kinds of parameters: input parameters that are variables and output parameters that can be any expression. The second kind makes no distinction between input and output parameters. The actions that distinguish input variables will be used in the definition of pLTS and are defined as follows:

$$
\begin{align*}
\alpha \in \mathbb{A} &::= a(p_1, \dots, p_n) & \text{action terms} \\
p_i &::= ?x \mid e_i & \text{parameters (input var or expression)} \\
e_i &::= \mathit{Value} \mid x \mid \mathit{op}(e_1, \dots, e_n) & \text{Expressions}
\end{align*}
$$

The input variables in an action term are those marked with a ? . We addi-
tionally impose that each input variable does not appear anywhere else in the
same action term: p$_{i}$ =?x ⇒ ∀j ̸ = i.x / ∈ vars( p$_{j}$ ). We define iv ( t ) as the set of
input variables of a term t (without the ’?’ marker). Input variables are used
in guards and to update the local state, they can only appear in well-identified
expressions. Action algebras can encode naturally usual point-to-point message
passing calculi (using a(?x$_{1}$, ..., ?x$_{n}$ ) for inputs, a( v$_{1}$, .., v$_{n}$ ) for outputs), but
they also allow for more general synchronisation mechanisms, like gate negoti-
ation in Lotos, or broadcast communications.

The set of actions that do not distinguish input variables is denoted $\mathbb{A}_S$, it
will be used in synchronisation vectors of pNets:

$$
\alpha \in \mathbb{A}_S ::= a(e_1, \dots, e_n)
$$

Indexed sets. This article extensively uses indexed structures (maps) over some countable indexed sets. The indices can typically be integers, bounded or not. We use indexed sets in pNets because we want to consider a set of processes, and specify separately how to synchronise them. Roughly this could also be realised using tuples, however indexed sets are more general, can be infinite, and give a more compact representation than using the position in a possibly long tuple.

An indexed family is denoted as follows: $t_i^{i \in I}$ is a family of elements $t_i$
indexed over the set $I$. Such a family is equivalent to the mapping $(i \mapsto t_i)^{i \in I}$, and
we will also use mapping notations to manipulate indexed sets. To specify the
set over which the structure is indexed, indexed structures are always denoted
with an exponent of the form $i \in I$. Consequently, $t_i^{i \in I}$ defines first $I$ the set
over which the family is indexed, and then $t_i$ the elements of the family. For
example $t_i^{i \in \{3\}}$ is the mapping with a single entry $t_3$ at index 3; exceptionally,
for mappings with only a few entries we use the notation $(3 \mapsto t_3)$ instead. In
this article, sentences of the form “there exists $t_i^{i \in I}$” means there exist $I$ and a
function that maps each element of $I$ to a term $t_i$.

When this is not ambiguous, we shall abuse notations for sets, and typically
write “indexed set over I” when formally we should speak of multisets, and
“$x \in A_i^{i \in I}$” to mean $\exists i \in I. x = A_i$. To simplify equations, an indexed set can
be denoted $\bar{t}$ instead of $t_i^{i \in I}$ when $I$ is irrelevant or clear from the context.
The disjoint union on sets is $\cup$ and we only use $A \uplus B$ when A and B are disjoint. We extend it to union of indexed sets provided they are indexed over disjoint families; $\cup$ is then defined by the merge of the two sets. The elements of the union of two indexed sets are then accessed by using an index of one of the two joined families. The subtraction operation on indexed sets is $\setminus$, it reduces the set of indices such that $\text{dom}(A \setminus B) = \text{dom}(A) \setminus B$.

**Substitutions.** This article also uses substitutions. Applying a substitution inside a term $t$ is denoted $t\{\{y_i \leftarrow e_i\}\}_{i \in I}$ and consists in replacing in parallel all the occurrences of variables $y_i$ in the term $t$ by the terms $e_i$. Note that a substitution is defined by a partial function that is applied on the variables inside a term. We let *Post* range over partial functions that are used as substitution and use the notation $\{y_i \leftarrow e_i\}_{i \in I}$ to define such a partial function<fnref n="2" />. These partial functions are sometimes called *substitution functions* in the following. Thus, $\{\{Post\}\}$ is the operation that applies, in a parallel manner, the substitution defined by the partial function *Post*. $\odot$ is a composition operator on these partial functions, such that for any term $t$ we have: $t\{\{Post \odot Post'\}\} = (t\{\{Post'\}\})\{\{Post\}\}$. This property must also be valid when the substitution does not operate on all variables. We thus define a composition operation as follows:

$$ (x_k \leftarrow e_k)_{k \in K} \odot (x'_{k'} \leftarrow e'_{k'})_{k' \in K'} = (x_k \leftarrow e_k)_{\{\{x'_{k'} \leftarrow e'_{k'}\}_{k' \in K'}\}}_{k \in K} \cup (x'_{k'} \leftarrow e'_{k'})_{k' \in K''} $$

where $K'' = \{k' \in K' | x'_{k'} \notin \{x_k\}_{k \in K}\}$

## 2.2. The principles of Parameterised Networks (pNets)

pNets are tree-like structures, where the leaves are either *parameterised labelled transition systems (pLTSs)*, expressing the behaviour of basic processes, or *holes*, used as placeholders for unknown processes. Every node of the tree is a pNet, it acts as a synchronising artefacts, using a set of *synchronisation vectors* that express the possible synchronisation between the actions of a subset of the sub-trees. The pNets model is hierarchical in the structure of the processes, this contrasts with *Statecharts* [24] that model high-level behaviour by organising the states (but not processes) in a hierarchy. We introduce pNets through a simple example below, and define formally pLTSs and pNets afterwards:

**Example 1 (CCS choice).** Here is the encoding of a choice operator.

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

It consists of one pNet (Definition 2 below) with two holes and a sub-net. The pNet is represented by the top box with three circles and two synchronisation vectors on the right. The sub-net is a pLTS that is represented by the bottom box.

<footnote n="2">²When using this notation, we suppose, without loss of generality that each $y_i$ is different.</footnote>
Each hole is represented by an empty disc, when the hole is filled it becomes a black disc. The left hole is indexed by $L$ and the right hole by $R$. The sub-net is a LTS with three states and emitting actions $l$ and $r$. In the synchronisation vector $a$ and $b$ range over arbitrary action terms, e.g. including action parameters; $l$ and $r$ on the contrary are specific actions. The set of synchronisation vectors is infinite but admits a simple finite representation.

The behaviour of the pNet is defined with synchronisation vectors also shown on the figure. In the examples, we write them on the form $<a, -, l> \to a$. This states that if the first hole $L$ performs the action $a$ and the third sub-net, i.e. the LTS, performs the action $l$, both of them progress synchronously, and an action $a$ is emitted by the pNet. The symbol $-$ at the second position denotes that the second hole does nothing. On the formal side, numbering and ordering the vectors is cumbersome, this is why we adopt indexed families of actions. The LTS is sometimes called the “control part”, it controls the evolution of the rest of the pNet. The first action of one of the holes decides which branch of the LTS is activated; all subsequent actions will be performed by the same side.

### 2.3. Parameterised Labelled Transition systems (pLTS)

A pLTS is a labelled transition system with variables; variables can be used inside states, actions, guards, and assignments. Note that we make no assumption on finiteness of the set of states nor on finite branching of the transition relation. Compared to our previous works [28, 2] we only global variables, which makes the model easier to use.

**Definition 1 (pLTS).** A pLTS is a tuple $pLTS \triangleq \langle S, s_0, V, \to \rangle$ where:

* $S$ is a set of states.

* $s_0 \in S$ is the initial state.

* $V$ is a set of global variables for the pLTS.

* $\to \subseteq S \times L \times S$ is the transition relation and $L$ is the set of labels. Labels have the form:

$\langle \alpha, e_b, (x_j := e_j)_{j \in J} \rangle$, where $\alpha \in \mathcal{A}$ is a parameterised action, $e_b \in \mathbb{B}$ is a guard, and the variables $x_j$ (that are pairwise distinct) are assigned the expressions $e_j \in \mathbb{E}$. If $s \xrightarrow{\langle \alpha, e_b, (x_j := e_j)_{j \in J} \rangle} s' \in \to$ then $\mathit{vars}(\alpha) \setminus \mathit{iv}(\alpha) \subseteq V$, $\mathit{vars}(e_b) \subseteq V \cup \mathit{vars}(\alpha)$, and $\forall j \in J$. $(\mathit{vars}(e_j) \subseteq V \cup \mathit{iv}(\alpha) \land x_j \in V)$.

A set of assignments between two states is performed in parallel so that their order do not matter and they all use the values of variables before the transition or the values received as action parameters.

### 2.4. Parameterised Networks (pNets)

Now we define pNet nodes as constructors for hierarchical behavioural structures. A pNet has a set of sub-pNets that can be either pNets or pLTSs, and
a set of holes, playing the role of process parameters. A pNet is thus a composition operator that can receive processes as parameters; it expresses how the actions of the sub-processes synchronise.

Each sub-pNet exposes a set of actions, called *internal actions*. *Synchronisation vectors* define the synchronisation between global actions exposed by the pNet and internal actions of its sub-pNets: it synchronises one or several internal actions, and exposes a single resulting global action.

We now define the structure of pNets, the following definition relies on the definition of holes, leaves and sorts formalised below in Definition 3. Informally, holes are process parameters, leaves provide the set of pLTSs at the leaves of the hierarchical structure of a pNet, and sorts give the signature of a pNet, i.e. the actions it exposes.

**Definition 2 (pNets).** A pNet $P$ is a hierarchical structure where leaves are pLTSs and holes

$$P \triangleq pLTS \mid \langle\langle P_i^{i \in I}, \text{Sort}_j^{j \in J}, SV_k^{k \in K} \rangle\rangle$$

We denote $vars(P)$ the set of variables used by the pLTSs inside $P$ and $Sort(P)$ the signature of the actions emitted by $P$; both are defined below, in Definition 3. A pNet is composed of the following:

* $I$ is a set of indices and $P_i^{i \in I}$ is the family of sub-pNets indexed over $I$. $vars(P_i)$ and $vars(P_j)$ must be disjoint for $i \neq j$.

* $J$ is a set of indices, called *holes*. $I$ and $J$ are disjoint: $I \cap J = \emptyset$, $I \cup J \neq \emptyset$.

* $Sort_j \subseteq A_S$ is a set of action terms, denoting the *sort* of hole $j$.

* $SV_k^{k \in K}$ is a set of synchronisation vectors. $\forall k \in K$. $SV_k = \alpha_l^{l \in I_k \cup J_k} \rightarrow \alpha'_k[e_k]$ where $\alpha'_k \in A_S$, $I_k \subseteq I$, $J_k \subseteq J$, $\forall i \in I_k$. $\alpha_i \in Sort(P_i)$, $\forall j \in J_k$. $\alpha_j \in Sort_j$, and $vars(\alpha'_k) \subseteq \bigcup_{l \in I_k \cup J_k} vars(\alpha_l)$. The global action of a vector $SV_k$ is $\alpha'_k$. $e_k \in \mathbb{B}$ is a guard associated to the vector such that $vars(e_k) \subseteq \bigcup_{l \in I_k \cup J_k} vars(\alpha_l)$.

Synchronisation vectors are identified modulo renaming of variables that appear in their action terms, e.g. the vectors $<a(x), b(x)> \rightarrow \tau$ and $<a(y), b(y)> \rightarrow \tau$ are equivalent.

The preceding definition relies on the auxiliary functions defined below:

**Definition 3 (Sorts, holes, leaves, variables of pNets).**

* The *sort* of a pNet is its signature, i.e. the set of actions in $A_S$ it can perform, where each action signature is an action label plus the arity of the action.

$$ \begin{align*} \text{Sort}(\langle\langle S, s_0, V, \rightarrow \rangle\rangle) &= \{\text{Sort}(\alpha)|s \xrightarrow{(\alpha, e_b, (x_j:=e_j)^{j \in J})} s' \in \rightarrow\} \\ \text{Sort}(\langle\langle \overline{P}, \text{Sort}, \overline{SV} \rangle\rangle) &= \{\text{Sort}(\alpha')|\overline{\alpha} \rightarrow \alpha'[e_b] \in \overline{SV}\} \\ \text{Sort}(\alpha(p_1, \dots, p_n)) &= (\alpha, n) \end{align*} $$
• The set of variables of a pNet P, denoted vars(P) is disjoint union the set of variables of all pLTSs that compose P.

• The set of holes Holes(P) of a pNet is the set of indices of the holes of the pNet itself plus the indices of all the holes of its sub-pNets. It is defined inductively (we suppose that those index sets are disjoint):

$$
\begin{align*}
\text{Holes}(\langle\langle S, s_0, V, \rightarrow \rangle\rangle) &= \emptyset \\
\text{Holes}(\langle\langle P_i^{i \in I}, \text{Sort}_j^{j \in J}, \overline{SV} \rangle\rangle) &= J \uplus \bigcup_{i \in I} \text{Holes}(P_i) \\
\forall i \in I. \text{ Holes}(P_i) \cap J &= \emptyset \\
\forall i_1, i_2 \in I. i_1 \neq i_2 \Rightarrow \text{Holes}(P_{i_1}) \cap \text{Holes}(P_{i_2}) &= \emptyset
\end{align*}
$$

• The set of leaves of a pNet is the set of all pLTSs occurring in the structure, as an indexed family of the form $\text{Leaves}(P) = \langle\langle P_i \rangle\rangle_{i \in L}$.

$$
\begin{align*}
\text{Leaves}(\langle\langle S, s_0, V, \rightarrow \rangle\rangle) &= \emptyset \\
\text{Leaves}(\langle\langle P_i^{i \in I}, \text{Sort}, \overline{SV} \rangle\rangle) &= \bigcup_{i \in I} \text{Leaves}(P_i) \uplus \{i \mapsto P_i \mid P_i \text{ is a pLTS}\}
\end{align*}
$$

For example, the controller of Example 1 has the sort ${l, r}$ and holes ${L, R}$.
Note that $\text{Holes}(P)$ is a set of indices because holes are characterized only by
their indices, while entities at the leaves are pLTSs and thus $\text{Leaves}(P)$ is a set
of pLTSs. A pNet $Q$ is closed if it has no hole: $\text{Holes}(Q) = \emptyset$; else it is said to
be open. Sort comes naturally with a compatibility relation that is similar to a
type-compatibility check. We simply say that two sorts are compatible if they
consist of the same actions with the same arity. In practice, it is sufficient to
check the equality of the two sets of action signatures of the two sorts<fnref n="3" />.

The informal semantics of pNets is as follows. pLTSs behave more or less
like classical automata with conditional branching and variables. The actions
on the pLTSs can send or receive values, potentially modifying the value of
variables. pNets are synchronisation entities: a pNet node composes several
sub-pNets and defines how the sub-pNets interact, where a sub-pNet is either
a pNet or a pLTS. The synchronisation between sub-pNets is defined by syn-
chronisation vectors (originally introduced in [3]) that express how an action of
a sub-pNet can be synchronised with actions of other sub-pNet, and how the
resulting synchronised action is visible from outside of the pNet. The synchro-
nisation mechanism is very expressive, including pattern-matching/unification
between the parameterized actions within the vector, and an additional predi-
cate over their variables. Consider a pNet node that assembles several pLTSs,
the synchronisation vectors specify the way that transitions of the composed
pNet are built from the transitions of the sub-nets. This can be seen as “condi-
tional transitions” of the pNet, or alternatively, as a syntax to encode structural

<footnote n="3">³A more complex compatibility relation could be defined, but this is out of the scope of this article.</footnote>
operational semantics (SOS rules) [42] of the system: each vector expresses not only the actions emitted by the pNet but also what transitions of the composed pLTSs must occur to trigger this global transition. Synchronisation vectors can also express the exportation of an action of a sub-pNet to the next level, or to hide an interaction and make it non-observable. Finally, a pNet can leave sub-pNets undefined and instead declare holes with a well-defined signature. Holes can then be filled with a sub-pNet. This is defined as follows.

**Definition 4 (pNet composition).** An open pNet: $P = \langle \langle P_i^{i \in I}, \text{Sort}_j^{j \in J}, \overline{SV} \rangle \rangle$ can be (partially) filled by providing a pNet $Q$ to fill one of its holes. Suppose $j_0 \in J$ and $\text{Sort}(Q) \subseteq \text{Sort}_{j_0}$, then:

$$P[Q]_{j_0} = \langle \langle P_i^{i \in I} \uplus \{j_0 \to Q\}, \text{Sort}_j^{j \in J \setminus \{j_0\}}, \overline{SV} \rangle \rangle$$

pNets are composition entities equipped with a rich synchronisation mechanism: synchronisation vectors allow the expression of synchronisation between any number of entities and at the same time the passing of data between processes. Their strongest feature is that the data emitted by processes can be used inside the synchronisation vector to do addressing: it is easy to synchronise a process indexed by $n$ with the action $a(v, n)$ of another process. This is very convenient to model systems and encode futures or message routing.

pNets have been used to model distributed components using the Grid Component Model, illustrating the expressiveness of the model [2]. These works show that pNets are convenient to express the behaviour of a system in a compositional way. Unfortunately, the semantics of pNets and the existing tools at that point were only able to deal with a closed and completely instantiated system: pNets could be used as composition operators in the definition of the semantics, which was sufficient to perform finite-state model checking on a closed system, but there was no theory for the use of pNets as operators and no tool for proving properties on open system. Consequently, much of the formalisation efforts did not use holes and the interplay between holes, sorts, and synchronisation vector was not formalised. In previous works [2], only closed pNets were equipped with a semantics, which was defined as labelled transition systems. The theory of pNets as operators for open systems is given in the following sections. Comparing formally the existing direct operational semantics and the semantics derived from open automata in the current article would be an interesting partial proof of soundness for our semantics. The proof could only be partial as the formal semantics that exists only consider closed and fully instantiated pNets. Proving an equivalence between the semantics presented in this article and the operational one shown in [2] is outside the scope of this article because we focus here on the modelling of holes that were not considered in the previous semantics. It is however easy to see that, in case there is no hole the structure of the open automaton that defines the semantics here is very close to the pLTS that is used to define the semantics, even though the formalisms are slightly different.
### 2.5. Running example

To illustrate this work, we use a simple communication protocol, that provides safe transport of data between two processes, over unsafe media.

Figure 1 (left) shows the example principle, which corresponds to the hierarchical structure of a pNet: two unspecified processes *P* and *Q* (holes) communicate messages, with a data value argument, through the two protocol entities. Process *P* sends a **p-send(m)** message to the *Sender*; this communication is denoted as in(*m*). At the other end, process *Q* receives the message from the *Receiver*. The holes *P* and *Q* can also have other interactions with their environment, represented here by actions **p-a** and **q-b**. The underlying network is modelled by a medium entity transporting messages from the sender to the receiver, and that is able to detect transport errors and signal them to the sender. The return *ack* message from *Receiver* to *Sender* is supposed to be safe. The final transmission of the message to the recipient (the hole *Q*) includes the value of the “error counter” *ec*.

Figure 1 (right) shows a graphical view of the pNet *SimpleProtocolSpec* that specifies the system. The pNet is made of the composition of two pNets: a *SimpleSystem* node, and a *PerfectBuffer* sub-pNet. The full system implementation should be equivalent (e.g. weakly bisimilar) to this *SimpleProtocolSpec*. The pNet has a tree-like structure. The root node of the tree *SimpleSystem* is the top level of the pNet structure. It acts as the parallel operator. It consists of three nodes: two holes *P* and *Q* and one sub-pNet, denoted *PerfectBuffer*. Nodes of the tree are synchronised using four synchronisation vectors, that express the possible synchronisations between the parameterised actions of a subset of the nodes. For instance, in the vector < **p-send(m)**, in(*m*), __________ >→ in(*m*) only *P* and *PerfectBuffer* nodes are involved in the synchronisation. The synchronisation between these processes occurs when process *P* performs **p-send(m)** action sending a message, and the *PerfectBuffer* accepts the message through an in(*m*) action at the same time; the result that will be returned at upper level is the action in(*m*).

Figure 2 shows the pNet model of the protocol implementation, called *SimpleProtocolImpl*. When the *Medium* detects an error (modelled by a local τ action), it sends back a **m-error** message to the *Sender*. The *Sender* increments its local error counter *ec*, and resends the message (including *ec*) to the *Medium*, that will, eventually, transmit *m*, *ec* to the *Receiver*.

## 3. A model of process composition

The semantics of open pNets will be defined as an open automaton. An open automaton is an automaton where each transition composes transitions of several LTSs with action of some holes, the transition occurs if some predicates hold, and can involve a set of state modifications. This section defines open automata and a bisimulation theory for them. This section is an improved version of the formalism described in [28], extending the automata with a notion of global variable, which makes the state of the automaton more explicit. We
<figure><img src="image_3.png" /><figcaption>Figure 1: pNet structure of the example and its specification expressed as a pNet called SimpleProtocolSpec</figcaption></figure>

also adopt a semantics and logical interpretation of the automata that intuitively can be stated as follows: “if a transition belongs to an open automaton, any refinement of this transition also belongs to the automaton”. Our open automata are clearly inspired by the work of De Simone on SOS rule [15] formats. A precise comparison with related works can be found in Section 6.

### 3.1. Open automata

Open automata (OA) are not composition structures but they are made of transitions that are dependent of the actions of the holes, and they can use variables (potentially with only symbolic values).

**Definition 5 (Open transitions).** An open transition (OT) over a set $J$ of holes with sorts $Sort_j^{J \in J}$, a set $V$ of variables, and a set of states $S$ is a structure of the form:

$$ \beta_j^{J \in J'}, \text{Pred}, \text{Post} \\ s \xrightarrow{\alpha} s' $$

where $J' \subseteq J$ is the set of holes involved in the transition; $s, s' \in S$ are states of the automaton; and $\beta_j$ is a transition of the hole $j$, with $Sort(\beta_j) \subseteq Sort_j$. $\alpha$ is the resulting action of this open transition. Pred is a predicate, Post is a set of assignments that are effective after the open transition, and are represented as a substitution function: $(x_k \leftarrow e_k)^{k \in K}$. Predicates and expressions of an open transition can refer to the variables inside $V$ and the different terms $\beta_j$ and $\alpha$.
<figure><img src="image_4.png" /><figcaption>Figure 2: The SimpleProtocolImpl pNet resulting from the composition of the SimpleSystem and the SimpleProtocol pNets.</figcaption></figure>

More precisely:

$$ 
\begin{array}{l}
\text{vars}(\text{Pred}) \subseteq V \cup \text{vars}(\alpha) \cup \bigcup_{j \in J'} \text{vars}(\beta_j) \wedge \\
\quad \forall k. x_k \in V \wedge \forall k. \text{vars}(e_k) \subseteq V \cup \text{vars}(\alpha) \cup \bigcup_{j \in J'} \text{vars}(\beta_j)
\end{array}
$$

The assignments are applied simultaneously because the variables in V can be in both sides ($x_k$s are distinct). Open transitions are identified modulo logical equivalence on their predicate.

It is important to understand the difference between the red dotted rule and a classical inference rule. They correspond to two different logical levels. On one side, classical (black) inference rules act at the mathematical level of the paper proofs (as e.g. the rules in Definition 13). They use an expressive logic (like any other computer science article). On the other side, open transition rules (with dotted lines) are logical implications that belong to the open automata algebra. Their logic has a specific syntax that can be mechanized; this logic includes the boolean expressions $\mathbb{B}$, boolean operators, and term equality.
An open automaton is an automaton where transitions are open transitions.

**Definition 6 (Open automaton).** An open automaton is a structure $A = \langle J, \mathcal{S}, s_0, V, \mathcal{T} \rangle$ where:

* $J$ is a set of indices.

* $\mathcal{S}$ is a set of states and $s_0$ is an initial state belonging to $\mathcal{S}$.

* $V$ is a set of variables of the automaton and each $v \in V$ may have an initial value $init(v)$.

* $\mathcal{T}$ is a set of open transitions and for each $t \in \mathcal{T}$ there exists $J'$ with $J' \subseteq J$, such that $t$ is an open transition over $J'$ and $\mathcal{S}$.

While the definition and usage of the open transition can be considered purely syntactically, we take in this article a semantic and logical understanding of open automata. We see open transitions as logical formulas with a constrained syntax and logics rather than purely syntactical terms. Consequently, the open transition sets in open automata are closed by a simple form of refinement that allows us to refine the predicate, or substitute any free variable by an expression. Formally, for each predicate *Pred* for each partial function *Post*, if $V \cap \text{dom}(*Post*) = \emptyset$, we have:

$$ \bar{\beta}, \text{Pred}', \text{Post}' \underset{s \xrightarrow{\alpha} s'}{\hspace{2cm}} \in \mathcal{T} \Rightarrow \bar{\beta}\{\text{Post}\}, \text{Pred}'\{\text{Post}\} \wedge \text{Pred}, \text{Post} \odot \text{Post}' \underset{s \xrightarrow{\alpha\{\text{Post}\}} s'}{\hspace{2cm}} \in \mathcal{T} $$

Because of the semantic interpretation of open automata, the set of open transition of an open automaton is infinite (for example because every free variable can be substituted by any term). This raises an issue when a finite representation is needed, which is the case both in our tools, and when writing examples. When needed, we can rely on a *canonical representation* of the open automaton, provided that a finite subset of the open transitions is sufficient to generate, by substitution, the other ones. Thus, we use this canonical representation in our examples. In the following, we will abusively write that we define an “open automaton” when we provide its canonical representation.

Another aspect of the semantic interpretation is that we consider terms up to semantic equivalence, i.e. equivalence of two predicates *Pred* and *Pred'* can be denoted *Pred* = *Pred'*, where the = symbol is interpreted semantically.

Though the definition is simple, the fact that transitions are complex structures relating events must not be underestimated. The first element of theory for open automata, i.e. the definition of a strong bisimulation, is given below.

## 3.2. Bisimulation for open Automata

We define now a bisimulation relation tailored to open automata and their parametric nature. This relation relates states of the open automata and guarantees that the related states are observationally equivalent, i.e. equivalent
states can trigger transitions with identical action labels. Its key characteristics
are 1) the introduction of predicates in the bisimulation relation: the relation
between states may depend on the value of the variables; 2) bisimulation relates
elements of the open transitions and takes into account predicates over variables,
actions of the holes, and state modifications. We name it FH-bisimulation, as
a short cut for the “Formal Hypotheses” over the holes behaviour manipulated
in the transitions, but also as a reference to the work of De Simone [15], that
pioneered this idea. Indeed, our definition uses both hypotheses on the be-
haviour of holes, as in [15], and symbolic manipulation of action expressions, as
in symbolic bisimulations of [25].

One of the original aspects of FH-bisimulation is due to the symbolic na-
ture of open automata. Indeed, a single state of the automaton represents a
potentially infinite number of concrete states, depending on the value of the
automaton variables, and a single open transition of the automaton may also
be instantiated with an unbounded number of values for the transition param-
eters. Consequently it would be too restrictive to impose that each transition
of one automaton is matched by exactly one transition of the bisimilar automa-
ton. Thus the definition of bisimulation requires that, for each open transition
of one automaton, there exists a matching set of open transitions covering the
original one. Indeed depending on the value of action parameters or automaton
variables, different open transitions might simulate the same one.

The parametric nature of the automata entails a second original aspect of
FH-bisimulation: the nature of the bisimulation relation itself. A classical re-
lation between states can be seen as a function mapping pairs of states to a
boolean value (true if the states are related, false if they are not). An FH-
bisimulation relation maps pairs of states to boolean expressions that use vari-
ables of the two systems. Formally, a relation over the states of two open au-
tomata $\langle J, S_1, s_0, V_1, \mathcal{T}_1 \rangle$ and $\langle J, S_2, t_0, V_2, \mathcal{T}_2 \rangle$ has the signature $S_1 \times S_2 \to \mathbb{B}$.
We suppose without loss of generality that the variables of the two open au-
tomata are disjoint. We adopt a notation similar to standard relations and
denote it $\mathcal{R} = \{(s, t|Pred_{s,t})\}$, where: 1) For any pair $(s,t) \in S_1 \times S_2$, there
is a single $(s,t|Pred_{s,t}) \in \mathcal{R}$ stating that $s$ and $t$ are related if $Pred_{s,t}$ is True,
i.e. the states are related when the value of the automata variables satisfy the
predicate $Pred_{s,t}$. 2) The free variables of $Pred_{s,t}$ belong to $V_1$ and $V_2$, i.e.
$vars(Pred_{s,t}) \subseteq V_1 \cup V_2$. FH-bisimulation is defined formally$^4$:

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

Suppose $A_1 = \langle J, S_1, s_0, V_1, \mathcal{T}_1 \rangle$ and $A_2 = \langle J, S_2, t_0, V_2, \mathcal{T}_2 \rangle$ are open automata with identical holes of the same sort, with disjoint sets of variables ($V_1 \cap V_2 = \emptyset$).

Then $\mathcal{R}$ is an FH-bisimulation if and only if for all states $s \in S_1$ and $t \in S_2$, $(s, t|Pred_{s,t}) \in \mathcal{R}$, we have the following:

• For any open transition *OT* in *T*₁:

<footnote n="4">⁴In this article, we denote $\beta_{jx}$ a double indexed set, instead of the classical $\beta_{j,x}$. Indeed the standard notation would be too heavy in our case.</footnote>
<figure><img src="image_5.png" /></figure>

there exists an indexed set of open transitions
$OT_x^{x \in X} \subseteq \mathcal{T}_2$:

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

such that $\forall x. J' = J_x$ and there exists some $Pred_{s',t_x}$ such that $(s', t_x | Pred_{s',t_x}) \in \mathcal{R}$ and

$$ Pred_{s,t} \wedge Pred_{OT} \implies \bigvee_{x \in X} (\forall j. \beta_j = \beta_{jx} \wedge Pred_{OT_x} \wedge \alpha = \alpha_x \wedge Pred_{s',t_x} \{\{Post_{OT} \uplus Post_{OT_x}\}\}) $$

* and symmetrically any open transition from $t$ in $\mathcal{T}_2$ can be covered by a set of transitions from $s$ in $\mathcal{T}_1$.

Two open automata are FH-bisimilar if there exists an FH-bisimulation that relates their initial states<fnref n="5" />. We call this relation *FH-bisimilarity*.

Classically, $Pred_{s',t_x} \{\{Post_{OT} \uplus Post_{OT_x}\}\}$ applies in parallel the substitution defined by the partial functions $Post_{OT}$ and $Post_{OT_x}$ (parallelism is crucial inside each $Post$ set but not between $Post_{OT}$ and $Post_{OT_x}$ that are independent), applying the assignments of the involved rules. We can prove that bisimilarity is an equivalence relation.

Note that, if there is a FH-bisimulation $\mathcal{R}$ such that $(s, t | Pred) \in \mathcal{R}$, and additionally $Pred' \Rightarrow Pred$ and it does not mean that there is a FH-bisimulation $\mathcal{R}'$ such that $(s, t | Pred')$, indeed pair of states such that $Pred$ is true and $Pred'$ is false might be necessary to prove the FH-bisimulation.

**Example 2.** The simulation of one transition by many others is one non-standard aspect of this definition. This is made necessary by the parameterised nature of our model. Consider the following open transition.

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

Bisimulation should allow it to be matched by the two following ones (depending on the value of $x$), to prove that the relation $\mathcal{R} = \{(s_1, s_2, True), (s'_1, s'_2, True)\}$ is a bisimulation.

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

<footnote n="5">⁵In other words, the predicate relation associated to the initial states is True.</footnote>
This example illustrates the necessity of multiple transitions in the definition of bisimulation in a naive and minimalistic way. It can easily be extended into a non-trivial example with more states and different usage of the variables.

**Theorem 1 (FH-bisimilarity is an equivalence).** *FH-bisimilarity is re-flexive, symmetric and transitive.*

The proof of this theorem can be found in Appendix A.1. The only non-trivial part of the proof is about transitivity. It relies on the following elements. First, the transitive composition of two relations with predicate is defined; this is not exactly standard as it requires to define the right predicate for the transitive composition and producing a single predicate to relate any two states. Then the fact that one open transition is simulated by a family of open transitions leads to a doubly indexed family of simulating open transition; this needs particular care, also because of the use of renaming (*Post*) when proving that the predicates satisfy the definition (property on $Pred_{s,t} \wedge Pred_{OT}$ in the definition).

*Finite versus infinite open automata, and decidability*

As mentioned in page 6, we adopt here a semantic view on open automata. More precisely, in [29], we define *semantic open automata* (infinite as in Definition 6), and *structural open automata* (finite) that can be generated as the semantics of pNets (see Definition 9), and used in their implementation. Then we define an alternative version of our bisimulation, called structural FH-bisimulation, based on structural open automata, and prove that the *semantic* and *structural* FH-bisimulations coincide. In the sequel, all mentions of finite automata, and algorithms for bisimulations, implicitly refer to their *structural* versions.

If we assume that everything is finite (states and transitions in the open automata), then it is easy to prove that it is decidable whether a relation is a FH-bisimulation, provided the logic of the predicates is decidable (a proof of this claim can be found in [28]). Formally:

**Theorem 2 (Decidability of FH-bisimulation).** Let $A_1$ and $A_2$ be finite open automata and $\mathcal{R}$ a relation over their states $S_1$ and $S_2$ constrained by a set of predicates. Assume that the predicate inclusion is decidable over the action algebra $\mathcal{A}$. Then it is decidable whether the relation $\mathcal{R}$ is an FH-bisimulation.

# 4. Semantics of Open pNets

This section defines the semantics of an open pNet as a translation into an open automaton. In this translation, the states of the open automaton are obtained as products of the states of the pLTSs at the leaves of the composition. The predicates on the transitions result both from the predicates on the transitions of the pLTSs, and from the synchronisation vectors involved in the transition.
The definition of bisimulation for open automata allows us to derive a bisimilarity relation for open pNets. As pNets are composition structures, it then makes sense to prove compositionality lemmas: we prove that the composition of strongly bisimilar pNets are themselves bisimilar.

### 4.1. Deriving an open automaton from an open pNet

To derive an open automaton from a pNet, we first describe the set of states of the automaton. Then we show the construction rule for transitions of the automaton, which relies on the derivation of predicates unifying synchronisation vectors and the actions of the pNets involved in a given synchronisation.

States of open pNets are tuples of states. We denote them as $\langle \dots \rangle$ for distinguishing tuple states from other tuples.

**Definition 8 (States of open pNets).** A state of an open pNet is a (not necessarily finite) tuple of the states of its leaves.

For any pNet P, let Leaves($P$) = $\langle\langle S_i, s_{i0}, V, \to_i \rangle\rangle$ be the set of pLTS at its leaves, then States($P$) = $\{\langle s_i \rangle_{i \in L} \mid \forall i \in L, s_i \in S_i\}$. A pLTS being its own single leave: States($\langle\langle S, s_0, V, \to \rangle\rangle$) = $\{\langle s \rangle \mid s \in S\}$.

The initial state is defined as: InitState($P$) = $\langle s_{i0} \rangle_{i \in L}$.

To be precise, the state of each pLTS is entirely characterized by both the state of the automaton, and the values of its variables $V$.

**Predicates.** We define a predicate Pred$_{sv}$ relating a synchronisation vector (of the form $(\alpha'_i)_{i \in I}$, $(\beta'_j)_{j \in J} \to \alpha'[e_b]$), the actions of the involved sub-pNets and the resulting actions. This predicate verifies:

$$ \text{Pred}_{sv}((\alpha'_i)_{i \in I}, (\beta'_j)_{j \in J} \to \alpha'[e_b]), \alpha_i^{i \in I}, \beta_j^{j \in J}, \alpha) \iff \\ \forall i \in I. \alpha_i = \alpha'_i \land \forall j \in J. \beta_j = \beta'_j \land \alpha = \alpha' \land e_b $$

Somehow, this predicate entails a verification of satisfiability in the sense that if the predicate Pred$_{sv}$ is not satisfiable, then the transition associated with the synchronisation will not occur in the considered state, or equivalently will occur with a False precondition. If the action families do not match or if there is no valuation of variables such that the above formula can be ensured then the predicate is undefined.

The definition of this predicate is not constructive. In our tool [44], we construct a logical formula encoding the matching and unification condition involved, and we let an SMT engine (in the current implementation Z3 [33]) decide its satisfiability.

**Example 3 (An open-transition).** At the upper level, the SimpleSystem pNet of Figure 2 has 2 holes and SimpleProtocol as a sub-pNet, itself containing 3 pLTSs. One of its possible open transitions (synchronizing the hole P with the Sender within the SimpleProtocol) is:
$$ \frac{s \xrightarrow{\langle \alpha, e_b, (x_j:=e_j)^{j \in J} \rangle} s' \in \rightarrow}{\langle\langle S, s_0, \rightarrow \rangle\rangle \models \underbrace{\emptyset, e_b, \{x_j \leftarrow e_j\}}^{\triangleleft s \triangleright \xrightarrow{\alpha} \triangleleft s' \triangleright} \mathop{\mathbf{Tr}}\nolimits^j} $$

and

$$ \begin{array}{l} \text{Leaves}(\langle\langle P_m^{m \in I}, \overline{Sort}, SV_k^{k \in K} \rangle\rangle) = pLTS_l^{l \in L} \quad k \in K \\ SV_k = (\alpha'_m)^{m \in I_1 \uplus I_2 \uplus J} \rightarrow \alpha'[e_b] \\ \qquad \beta_j^{j \in J_m}, Pred_m, Post_m \\ \forall m \in I_1. P_m \models \underbrace{\beta_j^{j \in J_m}, Pred_m, Post_m}_{\triangleleft s'_i^{i \in L_m} \triangleright \xrightarrow{\alpha_m} \triangleleft (s'_i)^{i \in L_m} \triangleright} \\ \forall m \in I_2. P_m \models \underbrace{\emptyset, Pred_m, Post_m}_{\triangleleft s_m \triangleright \xrightarrow{\alpha_m} \triangleleft s'_m \triangleright} \quad J' = \bigcup_{m \in I_1} J_m \uplus J \\ Pred = \bigwedge_{m \in I_1 \uplus I_2} Pred_m \wedge Pred_{sv}(SV_k, \alpha_m^{m \in I_1 \uplus I_2}, \beta_j^{j \in J}, \alpha) \\ \forall i \in L \setminus \left( \bigcup_{m \in I_1} L_m \uplus I_2 \right) . s'_i = s_i \quad \text{fresh}(\alpha'_m, \alpha', \beta_j^{j \in J}, \alpha) \\ \hline \frac{\beta_j^{j \in J'}, Pred, \bigcup_{m \in I_1 \uplus I_2} Post_m}{\langle\langle P_m^{m \in I}, \overline{Sort}, SV_k^{k \in K} \rangle\rangle \models \underbrace{\emptyset, Pred, \bigcup_{m \in I_1 \uplus I_2} Post_m}_{\triangleleft s'_i^{i \in L} \triangleright \xrightarrow{\alpha} \triangleleft (s'_i)^{i \in L} \triangleright}} \end{array} $$

<caption>Figure 3: Rules Tr1 and Tr2 defining the semantics of open pNets</caption>

$$ OT_1 = \frac{\{P \to p\text{-send}(m)\}, [m=m'], (s\_msg \leftarrow m)}{\triangleleft s_0, m_0, r_0 \triangleright \xrightarrow{\text{in}(m')} \triangleleft s_1, m_0, r_0 \triangleright} $$

The global states here are triples, the product of states of the 3 pLTSs (holes have no state). The assignment performed by the open transition uses the variable m from the action of hole P to set the value of the sender variable named s\_msg.

We build the semantics of open pNets as an open automaton over the states given by Definition 8. The open transitions first project the global state into states of the leaves, then apply pLTS transitions on these states, and compose them with the sort of the holes. The semantics instantiates fresh variables using the predicate fresh(x), additionally, for an action α, fresh(α) means all variables in α are fresh.

**Definition 9 (Semantics of open pNets).** The semantics of a pNet P is an open automaton $A = \langle Holes(P), States(P), InitState(P), vars(P), T \rangle$ where T is the smallest set of open transitions such that $T = \{OT | P \models OT\}$ and $P \models OT$ is defined by the rules in Figure 3.
* The rule **Tr1** for a pLTS checks that the guard is verified and transforms assignments into post-conditions.

* The rule **Tr2** deals with pNet nodes: for each possible synchronisation vector (of index *k*) applicable to the rule subject, the premises include one *open transition* for each sub-pNet involved, one possible *action* for each hole involved, and the predicate relating these with the resulting action of the vector. The sub-pNets involved are split between two sets, $I_2$ for sub-pNets that are pLTSs (with open transitions obtained by rule **Tr1**), and $I_1$ for the sub-pNets that are not pLTSs (with open transitions obtained by rule **Tr2**), *J* is the set of holes involved in the transition<fnref n="6" />.

A key to understand **Tr2** is that the open transitions are expressed in terms of the leaves and holes of the whole pNet structure, i.e. a flattened view of the pNet. For example, *L* is the index set of the Leaves, $L_m$ the index set of the leaves of one sub-pNet indexed *m*, so all $L_m$ are disjoint subsets of *L*. Thus the states in the open transitions, at each level, are tuples including states of all the leaves of the pNet, not only those involved in the chosen synchronisation vector.

Note that the construction is symbolic, and each open transition deduced expresses a whole family of behaviours, for any possible value of the variables.

In [28], we have shown a detailed example of the construction of a complex open transition, building a deduction tree using rules **Tr1** and **Tr2**. We have also shown in [28] that an open pNet with finite synchronisation sets, finitely many leaves and holes, and each pLTS at leaves having a finite number of states and (symbolic) transitions, induces a finite automaton. The algorithm for building such an automaton can be found in [43].

<figure><img src="image_9.png" /><figcaption>Figure 4: Open automaton for *SimpleProtocolSpec*</figcaption></figure>

<footnote n="6">⁶Formally, if $SV_k = (\alpha')_m^{m \in M} \rightarrow \alpha'[e_b]$ is a synchronisation vector of P then $J = M \cap \text{Holes}(P)$, $I_2 = M \cap \text{Leaves}(P)$, $I_1 = M \setminus J \setminus I_2$. We could replace $I_1$ and $I_2$ by their formal definition in **Tr2** but the rule would be more difficult to read.</footnote>
### Example

Figure 4 shows the open automaton computed from the *SimpleProtocolSpec* pNet given in Figure 1. For later references, we name $SS_i$ the transitions of this (strong) specification automaton while transitions of the *SimpleProtocolImpl* pNet are labelled $SI_i$. In the figures we annotate each open automaton with the set of its variables.

<figure><img src="image_10.png" /><figcaption>Figure 5: Open automaton for *SimpleProtocolImpl*</figcaption></figure>

Figure 5 shows the open automaton of *SimpleProtocolImpl* from Figure 2. In this drawing, we have short labels for states, representing $\langle s_0, m_0, r_0 \rangle$ by 000. Note that open transitions are denoted $SI_i$ and tau open transition by $SI_τ$. The resulting behaviour is quite simple: we have a main loop including receiving a message from *P* and transmitting the same message to *Q*, with some intermediate $τ$ actions from the internal communications between the protocol processes. In most of the transitions, you can observe that data is propagated between the successive pLTS variables (holding the message, and the error counter value). On the right of the figure, there is a loop of $τ$ actions ($SI_4$, $SI_5$ and $SI_6$) showing the handling of errors and the incrementation of the error counter.

## 4.2. pNet Composition Properties: composition of open transitions

The semantics of open pNets allows us to prove two crucial properties relating pNet composition with pNet semantics: open transition of a composed pNet can be decomposed into open transitions of its composing sub-pNets, and conversely, from the open transitions of sub-pNets, an open transition of the composed pNet can be built.

We start with a decomposition property: from one open transition of $P[Q]_{j_0}$, we exhibit corresponding behaviours of *P* and *Q*, and determine the relation between their predicates.
**Lemma 1 (Open transition decomposition).** Consider two pNets P and Q that are not pLTSs<fnref n="7" />. Let Leaves(Q) = $p_l^{i \in L_Q}$ and suppose:

$$P[Q]_{j_0} \models \frac{\beta_j^{j \in J}, \text{Pred}, \text{Post}}{\triangleleft s_i^{i \in L} \triangleright \xrightarrow{\alpha} \triangleleft s_i^{i' \in L} \triangleright}$$

with $J \cap \text{Holes}(Q) \neq \emptyset$ or $\exists i \in L_Q. s_i \neq s_i'$, i.e. Q takes part in the reduction. Then there exist $\alpha_Q, \text{Pred}', \text{Pred}'', \text{Post}', \text{Post}''$ s.t.:

$$P \models \frac{\beta_j^{j \in (J \setminus \text{Holes}(Q)) \cup \{j_0\}}, \text{Pred}', \text{Post}'}{\triangleleft s_i^{i \in L \setminus L_Q} \triangleright \xrightarrow{\alpha} \triangleleft s_i^{i' \in L \setminus L_Q} \triangleright} \\ \text{and} \\ Q \models \frac{\beta_j^{j \in J \cap \text{Holes}(Q)}, \text{Pred}'', \text{Post}''}{\triangleleft s_i^{i \in L_Q} \triangleright \xrightarrow{\alpha_Q} \triangleleft s_i^{i' \in L_Q} \triangleright}$$

and $\text{Pred} \iff \text{Pred}' \wedge \text{Pred}'' \wedge \alpha_Q = \beta_{j_0}, \text{Post} = \text{Post}' \lor \text{Post}''$ where $\text{Post}''$ is the restriction of $\text{Post}$ over variables of Q.

Lemma 2 is combining an open transition of P with an open transition of Q, and building a corresponding transition of $P[Q]_{j_0}$ by assembling their elements.

**Lemma 2 (Open transition composition).** Suppose $j_0 \in J$ and:

$$P \models \frac{\beta_j^{j \in J}, \text{Pred}, \text{Post}}{\triangleleft s_i^{i \in L} \triangleright \xrightarrow{\alpha} \triangleleft s_i^{i' \in L} \triangleright} \quad \text{and} \quad Q \models \frac{\beta_j^{j \in J_Q}, \text{Pred}', \text{Post}'}{\triangleleft s_i^{i \in L_Q} \triangleright \xrightarrow{\alpha_Q} \triangleleft s_i^{i' \in L_Q} \triangleright}$$

Then, we have:

$$P[Q]_{j_0} \models \frac{\beta_j^{(j \in J \setminus \{j_0\}) \lor J_Q}, \text{Pred} \wedge \text{Pred}' \wedge \alpha_Q = \beta_{j_0}, \text{Post} \lor \text{Post}'}{\triangleleft s_i^{i \in L \lor L_Q} \triangleright \xrightarrow{\alpha} \triangleleft s_i^{i' \in L \lor L_Q} \triangleright}$$

Note that this does not mean that any two pNets can be composed and produce an open transition. Indeed, the predicate $\text{Pred} \wedge \text{Pred}' \wedge \alpha_Q = \beta_{j_0}$ is often not satisfiable, in particular if the action $\alpha_Q$ cannot be matched with $\beta_{j_0}$. Note also that $\beta_{j_0}$ is only used as an intermediate term inside formulas in the composed open transition: it does not appear as global action, and will not appear as an action of a hole.

### 4.3. Bisimulation for open pNets – a composable bisimulation theory

As our symbolic operational semantics provides an open automaton, we can apply the notion of strong (symbolic) bisimulation on automata to open pNets.

**Definition 10 (FH-bisimulation for open pNets).** Two pNets are FH-bisimilar if their associated open automata are bisimilar.

<footnote n="7">⁷A similar lemma can be proven for a pLTS Q.</footnote>
We can now prove that pNet composition preserves FH-bisimilarity. More precisely, one can define two preservation properties, namely 1) when one hole of a pNet is filled by two bisimilar other (open) pNets; and 2) when the same hole in two bisimilar pNets are filled by the same pNet, in other words, composing a pNet with two bisimilar contexts. The general case will be obtained by transitivity of the bisimilarity relation (Theorem 1).

**Theorem 3 (Congruence).** Consider an open pNet

$P = \langle\langle P_i^{i \in I}, \text{Sort}_j^{j \in J}, \overline{SV} \rangle\rangle$. Let $j_0 \in J$ be a hole. Let $Q$ and $Q'$ be two FH-bisimilar pNets such that$^8$ $\text{Sort}(Q) = \text{Sort}(Q') = \text{Sort}_{j_0}$. Then $P[Q]_{j_0}$ and $P[Q']_{j_0}$ are FH-bisimilar.

**Theorem 4 (Context equivalence).** Consider two open pNets

$P = \langle\langle P_i^{i \in I}, \text{Sort}_j^{j \in J}, \overline{SV} \rangle\rangle$ and $P' = \langle\langle P'_i^{i \in I}, \text{Sort}_j^{j \in J}, \overline{SV} \rangle\rangle$ that are FH-bisimilar (they thus have the same holes). Let $j_0 \in J$ be a hole, and $Q$ be a pNet such that $\text{Sort}(Q) = \text{Sort}_{j_0}$. Then $P[Q]_{j_0}$ and $P'[Q]_{j_0}$ are FH-bisimilar.

Finally, the previous theorems can be composed to state a general theorem about composability and FH-bisimilarity.

**Theorem 5 (Composability).** Consider two FH-bisimilar pNets with an arbitrary number of holes, when replacing, inside those two original pNets, a subset of the holes by FH-bisimilar pNets, we obtain two FH-bisimilar pNets.

This theorem is quite powerful, as it somehow implies that the theory of open pNets can be used to study properties of process composition. Open pNets can indeed be applied to study process operators and process algebras, as shown in [28] where compositional properties are extremely useful. In the case of interaction protocols [12], compositionality of bisimulation can justify abstractions used in some parts of the application.

## 5. Weak bisimulation

Weak symbolic bisimulation [25] was introduced to relate transition systems that have indistinguishable behaviour, with respect to some definition of *internal actions* that are considered local to some subsystem, and consequently cannot be observed, nor used for synchronisation with their context. The notion of non-observable actions varies in different contexts, e.g. *tau* in CCS [40, 41], and *i* in Lotos [10]. We could define classically a set of *internal/non-observable actions* depending on a specific action algebra. However in this paper, to simplify the notations, we will simply use $\tau$ as the single non-observable action; the generalisation of our results to a set of non-observable actions is trivial. Naturally, a non-observable action cannot be synchronised with actions of other

<footnote>$^8$Note that $\text{Sort}(Q) = \text{Sort}(Q')$ is ensured by strong bisimilarity.</footnote>
systems in its environment. We show here that under such assumption of non-observability of $\tau$ actions, see Definition 11, we can define a weak bisimulation relation that is compositional, in the sense of open pNet composition. In this section we will first define a notion of weak open transition similar to open transition. In fact a weak open transition is made of several open transitions labelled as non-observable transitions, plus potentially one observable open transition. This allows us to define weak open automata, and a weak bisimulation relation based on these weak open automata. Finally, we apply this weak bisimulation to open pNets, obtain a weak bisimilarity relation for open pNets, and prove that this relation has compositional properties.

### 5.1. Preliminary definitions and notations

We first specify in terms of open transition, what it means for an action to be non-observable. We first define (in Definition 11) systems that cannot observe $\tau$ actions of sub-systems; namely pNets that cannot change their state, or emit an observable action when one of its holes emits a $\tau$ action.

More precisely, we state that $\tau$ is not observable if the automaton always allows any $\tau$ transition from holes, and additionally the global transition resulting from a $\tau$ action of a hole is a $\tau$ transition not changing the pNet's state. We define $\mathrm{Id}(V)$ as the identity function on the set of variables $V$.

**Definition 11 (Non-observability of $\tau$ actions for open automata).**

An open automaton $A = \langle J, S, s_0, V, \mathcal{T} \rangle$ cannot observe $\tau$ actions if and only if for all $j$ in $J$ and $s$ in $S$ we have:

$$ (j \to \tau), \mathrm{True}, \mathrm{Id}(V) \underset{s \to s'}{\overset{\tau}{\vdots}} \in \mathcal{T} \qquad 1. $$

and

2. for all $\beta_j, J, \alpha, s, s', \mathrm{Pred}, \mathrm{Post}$ such that

$$ \beta_j^{j \in J}, \mathrm{Pred}, \mathrm{Post} \underset{s \to s'}{\overset{\alpha}{\vdots}} \in \mathcal{T} \qquad 2. $$

If there exists $j$ such that $\beta_j = \tau$ then we have:

$$ \alpha = \tau \wedge s = s' \wedge \mathrm{Pred} = \mathrm{True} \wedge \mathrm{Post} = \mathrm{Id}(V) \wedge J = \{j\} \qquad 3. $$

The first statement of the definition states that the open automaton must allow a hole to do a silent action at any time, and must not observe it, i.e. it cannot change its internal state because a hole did a $\tau$ transition. The second statement ensures that there cannot be in the open automaton other transitions that would be able to observe a $\tau$ action from a hole: statement (2) states that all the open transitions where a hole does a $\tau$ action must be of the shape given in statement (1). In this second statement, the condition $J = \{j\}$ is a bit restrictive, it could
safely be replaced by $\forall j \in J. \beta_j = \tau$, allowing the other holes to perform $\tau$ transitions too (because these $\tau$ actions cannot be observed). This possible synchronisation of $\tau$ actions would not be a problem as condition 1 still ensures that each process can do a $\tau$ separately.

By definition, one weak open transition contains several open transitions, where each open transition can require an observable action from a given hole, the same hole might have to emit several observable actions for a single weak open transition to occur. Consequently, for a weak open transition to trigger, a sequence of actions from a given hole may be required.

Thus, we let $\gamma$ range over sequences of action terms and use $\oplus$ as the concatenation operator that appends sequences of action terms: given two sequences of action terms $\gamma \oplus \gamma'$ concatenates the two sequences. The operation is lifted to indexed sets of sequences: at each index $i$, $\overline{\gamma_1} \oplus \overline{\gamma_2}$ concatenates the sequences of actions at index $i$ of $\overline{\gamma_1}$ and the one at index $i$ of $\overline{\gamma_2}^9$. [a] denotes a sequence with a single element. These new actions are sequences of observable actions, we thus need an operator to build them from a set of actions that occur in open transitions, i.e. an operator that takes a set of actions performed by one hole and produces a sequence of observable actions. Thus we define $(\bar{\beta})^\nabla$ as the mapping $\bar{\beta}$ with only observable actions of the holes in $I$, but where each element is either empty or a list of length 1:

$$ (\beta_i^{i \in I})^{\nabla} = [\beta_i]^{i \in I'} \text{ where } I' = \{i | i \in I \wedge \beta_i \neq \tau\} $$

As an example the $(\bar{\beta})^\nabla$ built from the transition $OT_1$ in Example 3, page 19 is $P \to [\text{p-send}(m)]$. Remark that in our simple example no $\tau$ transition involves any visible action from a hole, so we have no $\beta$ sequences of length longer than 1 in the weak automaton.

## 5.2. Weak open transition definition

Because of the non-observability property (Definition 11), it is possible to add any number of $\tau$ transitions of the holes before or after any open transition freely. This property justifies the fact that we can abstract away from $\tau$ transitions from holes in the definition of a weak open transition. We define weak open transitions similarly to open transitions except that holes can perform sequences of observable actions instead of single actions (observable or not). Compared to the definition of open transition, this small change has a significant impact as a single weak transition is the composition of several transitions of the holes.

**Definition 12 (Weak open transition (WOT)).** A weak open transition over a set $J$ of holes with sorts $\text{Sort}_j^{j \in J}$ and a set of states $S$ is a structure of the form:

$$ \gamma_j^{j \in J'}, \text{Pred}, \text{Post} \\ s \stackrel{\alpha}{\Rightarrow} s' $$

<footnote n="9">⁹One of the two sequences is empty when $i \notin \text{dom}(\overline{\gamma_1})$ or $i \notin \text{dom}(\overline{\gamma_2})$.</footnote>
$$ \begin{array}{ccc} \begin{array}{c} \emptyset, \text{True}, \text{Id}(V) \\ \vdots \\ s \stackrel{\tau}{\Rightarrow} s \end{array} & \in \mathcal{W}\mathcal{T} & \mathbf{WT1} \quad \text{and} \quad \begin{array}{c} \overline{\beta, \text{Pred}, \text{Post}} \\ \vdots \\ s \stackrel{\alpha}{\Rightarrow} s' \end{array} \in \mathcal{T} \\ & & \begin{array}{c} \overline{(\beta)^{\nabla}, \text{Pred}, \text{Post}} \\ \vdots \\ s \stackrel{\alpha}{\Rightarrow} s' \end{array} \in \mathcal{W}\mathcal{T} \quad \mathbf{WT2} \end{array} $$

and

$$ \begin{array}{c} \overline{\gamma_1, \text{Pred}_1, \text{Post}_1} \\ \vdots \\ s \stackrel{\tau}{\Rightarrow} s_1 \end{array} \in \mathcal{W}\mathcal{T} \qquad \begin{array}{c} \overline{\gamma_2, \text{Pred}_2, \text{Post}_2} \\ \vdots \\ s_1 \stackrel{\alpha}{\Rightarrow} s_2 \end{array} \in \mathcal{W}\mathcal{T} \\ \begin{array}{c} \overline{\gamma_3, \text{Pred}_3, \text{Post}_3} \\ \vdots \\ s_2 \stackrel{\tau}{\Rightarrow} s' \end{array} \in \mathcal{W}\mathcal{T} \qquad \bar{\gamma} = \bar{\gamma}_1 \oplus \bar{\gamma}_2 \{\text{Post}_1\} \oplus \bar{\gamma}_3 \{\text{Post}_2 \odot \text{Post}_1\} \\ \begin{array}{c} \alpha' = \alpha \{\text{Post}_1\} \\ \vdots \\ \alpha' \end{array} \qquad \begin{array}{c} \text{Pred} = \text{Pred}_1 \wedge \text{Pred}_2 \{\text{Post}_1\} \wedge \text{Pred}_3 \{\text{Post}_2 \odot \text{Post}_1\} \\ \vdots \\ \text{Pred}_3 \{\text{Post}_2 \odot \text{Post}_1\} \end{array} \in \mathcal{W}\mathcal{T} \\ \begin{array}{c} \overline{\gamma, \text{Pred}, \text{Post}_3 \odot \text{Post}_2 \odot \text{Post}_1} \\ \vdots \\ s \stackrel{\alpha'}{\Rightarrow} s' \end{array} \in \mathcal{W}\mathcal{T} \end{array} $$

<caption>Figure 6: Weak transition definition</caption>

Where $J' \subseteq J$, $s, s' \in S$ and $\gamma_j$ is a list of transitions of the hole $j$, with each element of the list in $\text{Sort}_j$. $\alpha$ is an action label denoting the resulting action of this open transition. $\text{Pred}$ and $\text{Post}$ are defined similarly to Definition 5. We use $\mathcal{W}\mathcal{T}$ to range over sets of weak open transitions.

A weak open automaton $\langle J, S, s_0, V, \mathcal{W}\mathcal{T} \rangle$ is similar to an open automaton except that $\mathcal{W}\mathcal{T}$ is a set of weak open transitions over $J$ and $S$.

A weak open transition labelled $\alpha$ can be seen as a sequence of open transitions that are all labelled $\tau$ except one that is labelled $\alpha$; however conditions on predicates, effects, and states must be verified for this sequence to be fired.

We are now able to build a weak open automaton from an open automaton. This is done in a way that resembles the process of $\tau$ saturation: we add $\tau$ open transitions before or after another open transition, regardless of whether it is observable or not.

**Definition 13 (Building a weak open automaton).**

Let $A = \langle J, S, s_0, V, \mathcal{T} \rangle$ be an open automaton. The weak open automaton derived from $A$ is an open automaton $\langle J, S, s_0, V, \mathcal{W}\mathcal{T} \rangle$ where $\mathcal{W}\mathcal{T}$ is derived from $\mathcal{T}$ by saturation, applying the rules of Figure 6.

Rule **WT1** states that it is always possible to perform a non-observable transition, where the state is unchanged and the holes perform no action. Rule **WT2** states that each open transition is a weak open transition. Finally, Rule **WT3** allows any number of $\tau$ transitions before or after any weak open transition. This rule carefully composes predicates, effects, and actions of the holes. Indeed, predicate $\text{Pred}_2$ manipulates variables of $s_1$ that result from the first weak
open transition. Their values thus depend on the initial state but also on the effect (as a substitution function $Post_1$) of the first weak open transition. In the same manner, $Pred_3$ must be applied the substitution defined by the composition $Post_2 \odot Post_1$. Similarly, effects on variables must be applied to obtain the global effect of the composed weak open transition, to observable actions of the holes, and to the global action of the weak open transition.

<figure><img src="image_11.png" /><figcaption>Figure 7: Construction of an example of weak open transition</figcaption></figure>

**Example 4 (A weak open-transition).** Figure 7 shows the construction of one of the weak transitions of the open automaton of *SimpleProtocolSpec*. On the top we show the subset of the original open automaton (from Figure 4) considered here, and at the bottom the generated weak transition. For readability, we abbreviate the weak open transitions encoded by $\frac{}{s \stackrel{\tau}{\Rightarrow} s'}$ as $W_\tau$.

The weak open transition shown here is the transition delivering the result of the algorithm to hole $Q$ by applying rules: **WT1**, **WT2**, and **WT3**. First rule **WT1** adds a $WT_\tau$ loop on each state. Rule **WT2** transforms each 2 OTs into WOTs. Then consider application of Rule **WT3** on a sequence of 3 WOTs. $\frac{}{b1 \stackrel{\tau}{\Rightarrow} b1}$; $\frac{}{b1 \stackrel{\tau}{\Rightarrow} b1}$; $\frac{}{b1 \stackrel{\tau}{\Rightarrow} b1}$. The

result will be: $\frac{}{b1 \stackrel{\tau}{\Rightarrow} b1}$. We can iterate this construction an arbitrary number of times, getting for any natural number $n$ a weak open transition: $\frac{}{\emptyset, True, (ec \leftarrow ec + n)}$; $\frac{}{b1 \stackrel{\tau}{\Rightarrow} b1}$; $\frac{}{b1 \stackrel{\tau}{\Rightarrow} b1}$; $\frac{}{b1 \stackrel{\tau}{\Rightarrow} b1}$. Finally, applying again **WT3**, and using

the central open transition having $out(b\_msg, b\_ec)$ as $\alpha$, we get the resulting weak open transition between $b1$ and $b0$ (as shown in Figure 7). Applying the substitutions finally yields the weak transitions family $WS_7$ in Figure 8.

**Example 5 (Weak open automata).** Figures 8 and 9 respectively show the
weak automata of *SimpleProtocolSpec* and *SimpleProtocolImpl*. We encode weak open transitions by *WS* on the specification model and by *WI* on the implementation model.

<figure><img src="image_12.png" /><figcaption>Figure 8: Weak Open Automaton of *SimpleProtocolSpec*</figcaption></figure>

For readability, we only give names to the weak open transitions of *SimpleProtocolImpl* in Figure 9; we detail some of these transitions below and the full list is included in Appendix C. Let us point out that the weak OT loops (*WI*₁, *WI*₂ and *W*τ) on state 000 are also present in all other states, we did not repeat them. Additionally, many WOTs are similar, and numbered accordingly as 3, 3a, 3b, 3c and 8, 8a, 8b, 8c respectively: they only differ by their respective source or target states; the "variant" WOTs appear in blue in Figure 9, note that composed WOTs also appear in blue.

<figure><img src="image_13.png" /><figcaption>Figure 9: Weak Open Automaton of *SimpleProtocolImpl*</figcaption></figure>
Now let us give some details about the construction of the weak automaton of the SimpleProtocolImpl pNet, obtained by application of the weak rules as explained above. We concentrate on weak open transitions $WI_3$ and $WI_4$. Let us denote as $post_n$ the effect (as a substitution function) of the strong open transitions $SI_n$ from Figure 5:

$$post_3 = (s\_msg \leftarrow m, s\_ec \leftarrow 0)$$

$$post_4 = (m\_msg \leftarrow s\_msg, m\_ec \leftarrow s\_ec)$$

$$post_5 = ()$$

$$post_6 = (s\_ec \leftarrow s\_ec+1)$$

Then the effect of one single $100 \xrightarrow{OT_4} 210 \xrightarrow{OT_5} 220 \xrightarrow{OT_6} 100$ loop is$^{10}$:

$$post_{456} = post_6 \odot post_5 \odot post_4 = (s\_ec \leftarrow s\_ec + 1)$$

So if we denote $post_{456*}$ any iteration of this loop, we get $post_{456*} = (s\_ec \leftarrow s\_ec + n)$ for any $n \ge 0$, and the Post of the weak OT $WI_3$ is:

$Post_3 = post_{456*} \odot post_3 = (s\_msg \leftarrow m, s\_ec \leftarrow n), \forall n \ge 0$ and Post of $WI_{3a}$ is:

$$post_4 \odot post_{456*} \odot post_3 = (m\_msg \leftarrow m, m\_ec \leftarrow n), \forall n \ge 0.$$

We can now show some of the weak OTs of Figure 9 (the full table is included in Appendix C). As we have seen above, the effect of rule $WT_3$ when a silent action have an effect on the variable $ec$ will generate an infinite family of WOTs, depending on the number of iterations through the loops. We denote these families using a "meta-variable" $n$, ranging over Nat.

$$WI_1 = \frac{\{P \to p-a\}, [\forall x.p-a \neq p-send(x)], ()}{s \xrightarrow{p-a} s} \quad (\text{for any } s \in S)$$

$$\forall n \ge 0. \quad WI_3(n) = \frac{\{P \to p-send(m)\}, True, (s\_msg \leftarrow m, s\_ec \leftarrow n)}{000 \xrightarrow{in(m)} 100}$$

$$\forall n \ge 0. \quad WI_4(n) = \frac{\{\}, True, (m\_msg \leftarrow s\_msg, m\_ec \leftarrow s\_ec + n, s\_ec \leftarrow s\_ec + n)}{100 \xrightarrow{\tau} 210}$$

$$\forall n \ge 0. \quad WI_{456}(n) = \frac{\{\}, True, (s\_ec \leftarrow s\_ec + n)}{100 \xrightarrow{\tau} 100}$$

The Post of the weak OT $WI_{6a}$ is:

$$\begin{align*} Post_{6a} &= post_4 \odot post_{456*} \odot post_6 \\ &= (m\_msg \leftarrow s\_msg, m\_ec \leftarrow s\_ec) \odot (s\_ec \leftarrow s\_ec + n) \odot (s\_ec \leftarrow s\_ec + 1) \\ &= (m\_msg \leftarrow s\_msg, m\_ec \leftarrow s\_ec + 1 + n, s\_ec \leftarrow s\_ec + 1 + n) \end{align*}$$

So we get:

$$\forall n \ge 0. \quad WI_{6a}(n) = \frac{\{\}, True, (m\_ec \leftarrow s\_ec + 1 + n, s\_ec \leftarrow s\_ec + 1 + n)}{220 \xrightarrow{\tau} 210}$$

<footnote>$^{10}$when showing the result of Posts composition, we will omit the identity substitution functions introduced by the $\odot$ definition in page 7.</footnote>
### 5.3. Composition properties: composition of weak open transitions

We now have two different semantics for open pNets: a strong semantics, defined as an open automaton, and as a weak semantics, defined as a weak open automaton. Like the open automaton, the weak open automaton features valuable composition properties. We can exhibit a composition property and a decomposition property that relate open pNet composition with their semantics, defined as weak open automata. These are however technically more complex than the ones for open automata because each hole performs a set of actions, and thus a composed transition is the composition of one transition of the top-level pNet and a sequence of transitions of the sub-pNet that fills its hole. Composition and decomposition properties can be found as Lemma 6, Lemma 7, and Lemma 8 in Appendix B.2.

### 5.4. Weak FH-bisimulation

For defining a bisimulation relation between weak open automata, two options are possible. One option is that we define a simulation similar to the strong simulation but based on weak open automata, this would look like the FH-simulation but would need to be adapted to weak open transitions. Alternatively, we could define directly and classically a weak FH-simulation as a relation between two open automata, relating the open transitions of the first one with the transitions of the weak open automaton derived from the second one.

The definition below specifies how a set of weak open transitions can simulate an open transition, and under which condition; this is used to relate, by weak FH-bisimulation, two open automata by reasoning on the weak open automata that can be derived from the strong ones.

**Definition 14 (Weak FH-bisimulation).**

Let $A_1 = \langle J, S_1, s_0, V_1, T_1 \rangle$ and $A_2 = \langle J, S_2, t_0, V_2, T_2 \rangle$ be open automata with disjoint sets of variables. Let $\langle J, S_1, s_0, V_1, WT_1 \rangle$ and $\langle J, S_2, t_0, V_2, WT_2 \rangle$ be the weak open automata derived from $A_1$ and $A_2$ respectively. Let $\mathcal{R}$ a relation over $S_1$ and $S_2$, as in Definition 7.

Then $\mathcal{R}$ is a weak FH-bisimulation iff for any states $s \in S_1$ and $t \in S_2$ such that $(s, t | Pred_{s,t}) \in \mathcal{R}$, we have the following:

* For any open transition $OT$ in $T_1$:

$$ \beta_j^{j \in J'}, Pred_{OT}, Post_{OT} \\ s \xrightarrow{\alpha} s' $$

there exists an indexed set of weak open transitions $WOT_x^{x \in X} \subseteq WT_2$:

$$ \gamma_{jx}^{j \in J_x}, Pred_{OT_x}, Post_{OT_x} \\ t \xrightarrow{\alpha_x} t_x $$
such that $\forall x. \{j \in J' | \beta_j \neq \tau\} = J_x, (s', t_x | Pred_{s',t_x}) \in \mathcal{R}$; and

$$ Pred_{s,t} \wedge Pred_{OT} \implies \bigvee_{x \in X} (\forall j \in J_x.(\beta_j)^\nabla = \gamma_{jx} \wedge Pred_{OT_x} \wedge \alpha = \alpha_x \wedge Pred_{s',t_x} \{\{Post_{OT} \uplus Post_{OT_x}\}\}) $$

* and symmetrically any open transition from $t$ in $\mathcal{T}_2$ can be covered by a set of weak transitions from $s$ in $\mathcal{W}\mathcal{T}_1$.

Two open automata are weak FH-bisimilar if there exists a weak FH-bisimulation relation that relates their initial states. This relation is called weak FH-bisimilarity. Two pNets are weak FH-bisimilar if their associated open automata are weakly bisimilar.

Compared to strong bisimulation, except the use of weak open transitions to simulate an open transition, the condition on predicate is slightly changed concerning actions of the holes. Indeed, only the visible actions of the holes must be compared and they form a list of actions, but of length at most one.

Our first important result is that weak FH-bisimilarity is an equivalence in the same way as strong FH-bisimilarity.

**Theorem 6 (Weak FH-bisimilarity is an equivalence).**

Weak FH-bisimilarity is reflexive, symmetric and transitive.

The proof is detailed in Appendix B.1, it follows a similar pattern as the proof that strong FH-bisimilarity is an equivalence, but technical details are different, and in practice we rely on a variant of the definition of weak FH-bisimilarity; this equivalent version simulates a weak open transition with a set of weak open transition. The careful use of the best definition of weak FH-bisimilarity makes the proof similar to the strong FH-bisimilarity case.

*Proving bisimulation in practice*

In practice, we are dealing with finite representations of the (infinite) open automata. In [29], we defined a slightly modified definition of the “coverage” proof obligation, in the case of strong FH-bisimulation. This modification is required to manage in a finite way all possible instantiations of an OT. In the case of weak FH-bisimulation, the proof obligation from Definition 14 becomes:

$$ \forall f_{v_{OT}}. \left\{ Pred_{s,t} \wedge Pred_{OT} \implies \bigvee_{x \in X} \left[ \exists f_{v_{OT_x}}. \left( \forall j \in J_x.(\beta_j)^\nabla = \gamma_{jx} \wedge Pred_{OT_x} \wedge \alpha = \alpha_x \wedge Pred_{s',t_x} \{\{Post_{OT} \uplus Post_{OT_x}\}\} \right) \right] \right\} $$

where $f_{v_{OT}}$ denotes the set of free variables of all expressions in $OT$.
### 5.5. Weak FH-bisimulation for open pNets

Before defining a weak open automaton for the semantics of open pNets, it is necessary to state under which condition a pNet is unable to observe silent actions of its holes. In the setting of pNets this can simply be expressed as a condition on the synchronisation vectors. Precisely, the set of synchronisation vectors must contain vectors that let silent actions go through the pNet, i.e. synchronisation vectors where one hole does a $\tau$ transition, and the global visible action is a $\tau$. Additionally, no other synchronisation vector must be able to react on a silent action from a hole, i.e. if a synchronisation vector observes a $\tau$ from a hole it cannot synchronise it with another action nor emit an action that is not $\tau$. This is formalised as follows:

**Definition 15 (Non-observability of silent actions for pNets).**

A pNet $\langle P_i^{i \in I}, \text{Sort}_j^{j \in J}, \overline{SV} \rangle$ cannot observe silent actions if it verifies: $\forall i \in I \uplus J. (i \to \tau) \to \tau[\text{True}] \in \overline{SV}$ and

$$ \forall \left( (\alpha_i)^{i \in I'} \to \alpha'[e_b] \in \overline{SV} \right), \forall i \in I' \cap J. \alpha_i = \tau \implies \alpha' = \tau \land I' = \{i\} $$

With this definition, it is easy to check that the open automaton that gives the semantics of such an open pNet cannot observe silent actions in the sense of Definition 11.

**Property 1 (Non-observability of silent actions).** The semantics of a pNet, as provided in Definition 9, that cannot observe silent actions is an open automaton that cannot observe silent actions.

Under this condition, it is safe to define the weak open automaton that provides a weak semantics to a given pNet. This is simply obtained by applying Definition 13 to generate a weak open automaton from the open automaton that is the strong semantics of the open pNet, as provided by Definition 9.

**Definition 16 (Semantics of pNets as a weak open automaton).** Let A be the open automaton expressing the semantics of an open pNet P; let $\langle J, S, s_0, V, WT \rangle$ be the weak open automaton derived from A; we call this weak open automaton the weak semantics of the pNet P. Then, we denote $P \models WOT$ whenever $WOT \in WT$.

From the definition of the weak open automata of pNets, we can now study the properties of weak bisimulation concerning open pNets.

### 5.6. Properties of weak bisimulation for open pNets

When silent actions cannot be observed, weak FH-bisimilarity is a congruence for open pNets: if P and Q are weakly bisimilar to P' and Q' then the composition of P and Q is weakly bisimilar to the composition of P' and Q', where composition is the hole replacement operator: $P[Q]_j$ and $P'[Q']_j$ are weak FH-bisimilar. This can be shown by proving the two following theorems.
The detailed proof of these theorem can be found in Appendix B.2. The proof strongly relies on the fact that weak FH-bisimulation is an equivalence, but also on the composition properties for open automata.

**Theorem 7 (Congruence for weak FH-bisimilarity).** Consider an open pNet $P$ that cannot observe silent actions, of the form $P = \langle\langle P_i^{i \in I}, \text{Sort}_j^{j \in J}, \overline{SV} \rangle\rangle$. Let $j_0 \in J$ be a hole. Let $Q$ and $Q'$ be two weak FH-bisimilar pNets such that$^{11}$ $\text{Sort}(Q) = \text{Sort}(Q') \subseteq \text{Sort}_{j_0}$. Then $P[Q]_{j_0}$ and $P[Q']_{j_0}$ are weak FH-bisimilar.

**Theorem 8 (Context equivalence for weak FH-bisimilarity).** Consider two open pNets $P = \langle\langle P_i^{i \in I}, \text{Sort}_j^{j \in J}, \overline{SV} \rangle\rangle$ and $P' = \langle\langle P_i'^{i \in I}, \text{Sort}_j'^{j \in J}, \overline{SV}' \rangle\rangle$ that are weak FH-bisimilar (recall they must have the same holes to be FH-bisimilar) and that cannot observe silent actions. Let $j_0 \in J$ be a hole, and $Q$ be a pNet such that $\text{Sort}(Q) \subseteq \text{Sort}_{j_0}$. Then $P[Q]_{j_0}$ and $P'[Q]_{j_0}$ are weak FH-bisimilar.

Finally, the previous theorems can be composed to state a general theorem about composability and weak FH-bisimilarity.

**Theorem 9 (Composability of weak FH-bisimilarity).** Consider two weak FH-bisimilar pNets with an arbitrary number of holes, such that the two pNets cannot observe silent actions. When replacing, inside those two original pNets, a subset of the holes by weak FH-bisimilar pNets, we obtain two weak FH-bisimilar pNets.

**Example 6 (CCS Choice).** Consider the $+$ operator of CCS, shown in Example 1. The pNet does not satisfy Definition 15. Indeed, if $a$ or $b$ is $\tau$ then the $+$ operator can observe the $\tau$ transition. It is well-known that weak bisimilarity is not a congruence in CCS, this corresponds to the fact that the $+$ operator can observe the $\tau$ transitions. Thus, even if we can define a weak FH-bisimilarity for CCS with $+$ it does not verify the necessary requirements for being a congruence. On the other side, the parallel operator defined similarly *satisfies* Definition 15, and indeed bisimilarity is a congruence for the parallel operator in CCS.

### Running example

In Section 5 we have shown the full saturated weak automaton for both *SimpleProtocolSpec* and *SimpleProtocolImpl*. We will show here how we can check if some given relation between these two automata is a weak FH-bisimulation.

Preliminary remarks:

* Both pNets trivially verify the “non-observability” condition: the vectors having $\tau$ as an action of a sub-net are of the form “$< -, \tau, - > \to \tau$”.

<footnote>11Note that $\text{Sort}(Q) = \text{Sort}(Q')$ is ensured by weak FH-bisimilarity.</footnote>
<table><caption>Table 1: Bisimulation for the running example.</caption><thead><tr><th>SimpleProtocolSpec<br>states</th><th>SimpleProtocolImpl<br>states</th><th>Predicate</th></tr></thead><tbody><tr><td>b0</td><td>000</td><td>True</td></tr><tr><td>b0</td><td>202</td><td>True</td></tr><tr><td>b1</td><td>100</td><td>b_msg = s_msg &amp; b_ec = s_ec</td></tr><tr><td>b1</td><td>210</td><td>b_msg = m_msg &amp; b_ec = m_ec</td></tr><tr><td>b1</td><td>220</td><td>b_msg = s_msg &amp; b_ec = s_ec</td></tr><tr><td>b1</td><td>201</td><td>b_message = r_message &amp; b_ec = r_ec</td></tr></tbody></table>

* We must take care of variable name conflicts: in our example, the variables of the 2 systems already have different names, but the action parameters occurring in the transitions (`m`, `msg`, `ec`) are the same, that is not correct. In the tools, this is managed by the static semantic layer; in the example, we rename the only conflicting variables `m` into `m1` for `SimpleProtocolSpec`, and `m2` for `SimpleProtocolImpl`.

Now consider the relation $\mathcal{R}$ defined by the triples in Table 1.

Checking that $\mathcal{R}$ is a weak FH-bisimulation means checking, for each of these triples, that each (strong) OT of one of the states corresponds to a set of WOTs of the other, using the conditions from Definition 14. We give here one example: consider the second triple from the table, and transition $SS_3$ from state `b0`. Its easy to guess that it will correspond to $WI_3(0)$ of state `202` (and equivalently state `000`, see Figure 9):

$$ 
\begin{aligned}
SS_3 &= \frac{\{P \mapsto \text{p-send}(m1)\}, \text{True}, (\text{b\_msg} \leftarrow \text{m1}, \text{b\_ec} \leftarrow 0) \qquad \text{in}(m1) \to b1}{b0} \\
WI_3(0) &= \frac{\{P \mapsto \text{p-send}(m2)\}, \text{True}, (\text{s\_msg} \leftarrow \text{m2}, \text{s\_ec} \leftarrow 0)}{000 \qquad \text{in}(m2) \to 100}
\end{aligned}
$$

Let us check formally the conditions:

* Their sets of active (non-silent) holes is the same: $J' = J_x = \{P\}$.

* Triple (`b1`, `100`, `b_message` = `s_message` &amp; `b_ec` = `s_ec`) is in $\mathcal{R}$.

* The verification condition

$$ \forall fv_{OT}. \{Pred \land Pred_{OT} \implies \bigvee_{x \in X} [\exists fv_{OT_x}. (\forall j \in J_x.(\beta_j)^\nabla = \gamma_{jx} \land Pred_{OT_x} \land \alpha = \alpha_x \land Pred_{s',t_x} \{\text{Post}_{OT} \uplus \text{Post}_{OT_x}\})] \} $$

gives us:

$$ \begin{aligned} \forall \mathbf{m1}. \{\text{True} \land \text{True} &\implies \exists \mathbf{m2}. \\ ([\text{p-send}(\mathbf{m1}')] = [\text{p-send}(\mathbf{m2}')] \land \text{True} \land \text{in}(\mathbf{m1}) = \text{in}(\mathbf{m2})] \land \end{aligned} $$
$$ (b\_msg=s\_msg \land b\_ec=s\_ec) \{((b\_msg \leftarrow m1, b\_ec \leftarrow 0) \lor (s\_msg \leftarrow m2, s\_ec \leftarrow 0)) \} $$

That is reduced to:

$$ \forall m1. \exists m2. (p\_send(m1) = p\_send(m2) \land in(m1) = in(m2) \land m1 = m2 \land 0 = 0) $$

That is a tautology.

# 6. Related Works

To the best of our knowledge, there are not many research works on Weak Bisimulation Equivalences between such complicate system models (open, symbolic, data-aware, with loops and assignments). We give a brief overview of other related publications, focussing first on Open and Compositional approaches, then on Symbolic Bisimulation for data-sensitive systems.

## Open and compositional systems

In [34, 33], the authors investigate several methodologies for the compositional verification of software systems, with the aim to verify reconfigurable component systems. To improve scalability and compositionality, the authors decompose the verification problem that is to be resolved by a SMT (satisfiability modulo theory) solver into independent sub-problems on independent sets of variables. These works clearly highlight the interest of incremental and compositional verification in a very general setting. In our own work on open pNets, adding more structure to the composition model, we show how to enforce a compositional proof system that is more versatile than independent sets of variables as the composition is structured and allows arbitrary synchronisations between sub-entities. Our theory has also been encoded into an SMT solver and it would be interesting to investigate how the examples of evolving systems studied by Johnson et al. could be encoded into pNet and verified by our framework. However, the models of Johnson et al. are quite different from ours, in particular they are much less structured, and translating them is clearly outside the scope of this article.

In previous work [19], we also have shown how (closed) pNet models could be used to encode and verify finite instances of reconfigurable component systems.

Methodologies for reasoning about abstract semantics of open systems can be found in [4, 5, 17], authors introduce behavioural equivalences for open systems from various symbolic approaches. Working in the setting of process calculi, some close relations exist with the work of the authors of [4, 5], where both approaches are based on some kinds of labelled transition systems. The distinguishing feature of their approach is that the transitions systems are labelled with logical formulae that provides an abstract characterization of the structure that a hole must possess and of the actions it can perform in order to allow a transition to fire. Logical formulae are suitable formalisms that capture the general class of components that can act as the placeholders of the
system during its evolution. In our approach we purposely leave the algebra of action terms undefined but the only operation we allow on action of holes is the comparison with other actions. Defining properly the interaction between a logical formulae in the action and the logics of the pNet composition seems very difficult. mCRL2 [21] is another effective model for specifying and proving properties of concurrent systems. mCRL2 has an established tool-suite and share similarities with pNets. However, pNets feature hierarchical composition with more structure than mCRL2 that composes processes with a parallel operator. Synchronisation of processes is expressed very differently; it is difficult to precisely compare multi-actions of mCRL2 with synchronisation vectors of pNets but synchronisation vector of pNets enforce a synchronisation based on the structure while in mCRL2 synchronisation is specified in a versatile, flexible, but less structured way.

In the same vein as context systems [36], pNets is a formalism for modular and possibly incomplete description of concurrent systems. The two formalisms are however different as the theory of contexts relies on a form of rewrite rules, while pNets rely on parametric automata to express the system behaviour. pNets have similar features as context systems [36] and static constructs [31]. Indeed all these approaches allow for modular and possibly incomplete description and structural composition of systems. The main originality of pNets compared to these other compositional approaches is the parameterised nature of the specification, which enables reasoning on value-passing systems but also on rich synchronisations that depend on the value of parameters.

## Decomposition techniques

Quotienting of process algebras [36] and decomposition techniques for mCRL2 [37] share similarities with our approach; they propose to overcome the state-space-explosion problem by decomposing formulas to be verified according to the process composition. The decomposed problem must be equivalent to the original one. However these techniques are expressed in a very different setting from ours and it is difficult to precisely relate them to the more structural and parameterised point of view we adopt here. We could try to apply such automatic decomposition techniques to open pNets, but deriving a decomposition for systems synchronised in a very parameterised way like we do requires further investigations. Both parallel composition [36] and mCRL2 [37] feature a concrete verification setting where decomposition is useful, while open automata provide a more general setting that could be used to represent both frameworks and hopefully generalise process decomposition results of [36, 37].

## Logical and semantics approaches

Among the approaches for modelling open systems, one can cite [7] that uses transition conditions depending on an external environment, and introduce bisimulation relations based on this approach. The approach of [7] is highly based on logics and their bisimulation theory is richer than ours in this aspect, while our theory is highly structural and focuses on relation between structure and equivalence. Also, we see composition as a structural operation putting
systems together, and do not focus on the modelling of an unknown outside
world. Overall we believe that the two approaches are complementary but
comparing precisely the two different bisimulation theories is not trivial.

There is also a clear relation with the seminal works on rule formats for Structured Operational Semantics, e.g. De Simone format, GSOS, and conditional rules with or without negative premises [15, 9, 23, 45]. The Open pNets model provides a way to define operators similar to these rules formats, but with quite different aim and approach. A formal comparison would be interesting, though not trivial. What we can say easily is that: the pNet format syntactically encompasses De Simone, GSOS, and conditional premises rules. Then our compositionality result is more powerful than their classical results, but this is not a surprise, as we rely on a (sufficient) syntactic hypothesis on a particular system, rather than the general rules defining an operator. Last, we intentionally do not accept negative premises, that would be more to put into practice in our implementation. This extension could be studied in future work.

## Symbolic and data-sensitive systems

As mentioned in the *Introduction*, we were substantially inspired by the works of Lin et al. [32, 25, 38]. They developed the theory of symbolic transition graphs (STG), and the associated symbolic (early and late, strong and weak) bisimulations. Moreover, they studied STGs with assignments as a model for message-passing processes. Our work extends those contributions in several ways: first our models are compositional, and our bisimulations come with effective conditions for being preserved by pNet composition (i.e. congruent), even for the weak version. This result is more general than the bisimulation congruences for value-passing CCS in [32]. Then our settings for management of data types are much less restrictive, thanks to our use of satisfiability engines, while Lin’s algorithms were limited to data-independent systems.

In a similar way, [1] presents a notion of "data-aware" bisimulations on data graphs, in which computation of such bisimulations is studied based on XPath logical language extended with tests for data equality.

Research related to the keyword "Symbolic Bisimulation" refer to two very different domains, namely BDD-like techniques for modelling and computing finite-state bisimulations, that are not related to our topic; and symbolic semantics for data-dependant or high-order systems, that are very close in spirit to our approach. In this last area, we can mention Calder's work [14], that defines a symbolic semantic for full Lotos, with a symbolic bisimulation over it; Borgstrom et al., Liu et al, Delaune et al. and Buscemi et al. providing symbolic semantics and equivalence for different variants of pi calculus respectively [11, 16, 39, 13]; and more recently Feng et al. provide a symbolic bisimulation for quantum processes [18]. All the above works are based on models definitely different from ours, and none of them allows system to be as much parameterised as open pNets; this additional expressiveness is due to the open and symbolic nature of our constructs.
## 7. Conclusion and discussion

pNets (Parameterised Networks of Automata) is a formalism adapted to the representation of the behaviour of parallel or distributed systems. One strength of pNets is their parameterised nature, making them suitable for to the representation of systems of arbitrary size, and making the modelling of parameterised systems possible. Parameters are also crucial to reason about interaction protocols that can address one entity inside an indexed set of processes. pNets have been successfully used to represent behavioural specification of parallel and distributed components and verify their correctness [2, 27]. VCE is the specification and verification platform that uses pNets as an intermediate representation. In this platform we have developed tool support for computing the symbolic semantics in term of open automata; this is presented in [43, 44], together with a case-study based on the on-board control software of satellites. In [8] we present how to encode reactive systems from the BIP specification language and check their temporal properties using VCE. In [29, 30] we describe our strong bisimulation algorithms, with illustration on the equivalence of different encodings of operators.

Open pNets are pNets with holes; they are adapted to represent processes parameterised by the behaviour of other processes, like composition operators or interaction protocols that synchronise the actions of processes that can be provided afterwards. Open pNets are hierarchical composition of automata with holes and parameters. We defined here a semantics for open pNets and a complete bisimulation theory for them. The semantics of open pNets relies on the definition of open automata that are automata with holes and parameters, but no hierarchy. Open automata are a flattened view of the pNet; their behaviour is expressed as open transitions that allow for a more semantic interpretation of process parameters (holes) than pNets. In the end, open automata are labelled transition systems with parameters and holes, a notion that is useful to define semantics, but makes less sense for the high level modelling of a system, compared to pNets. Open automata is the formalism that makes it possible to define FH-bisimilarity.

This article defines a strong and a weak bisimulation relation that are adapted to parameterised systems and hierarchical composition. FH-bisimulation handles pNet parameters in the sense that two states might be or not in relation depending on the value of parameters. Strong FH-bisimilarity is compositional in the sense that it is maintained when composing processes. We also identified a simple and realistic condition on the semantics of non-observable actions that allows weak FH-bisimilarity to be also compositional. Overall we believe that this article paved the way for a solid theoretical foundation for compositional verification of parallel and distributed systems.

The pNets formalism supports the refinement checking at the automaton level through a simulation, with symbolic evaluation of guards and transitions. The definition of simulation on open automata should be stronger than a classical simulation since it matches a transition with a family of transitions. Such a relation should be able to check the refinement by taking into account state
duplication, transition removal, guard strengthening, variable modification. Additionally, composition of pNets gives the possibility to either add new holes to a system or fill holes. A useful simulation relation should thus support the comparison of automata that do not have the same number of holes. Designing such a simulation relation is a non-trivial extension that we leave for future work.

We are currently looking at further properties of FH-bisimulation, but also the relations with existing equivalences on both closed and open systems. In particular, our model being significantly different from those considered in [32], it would be interesting to compare our “FH” family of bisimulations with the hierarchy of symbolic bisimulations from those authors. We also plan to apply open pNets to the study of complex composition operators in a symbolic way, for example in the area of parallel skeletons, or distributed algorithms.

Recently we published preliminary work on methods for checking weak FH-bisimulation [46]. The challenges here, in the context of our symbolic systems, are not so much algorithmic complexity, as was the case with classical weak bisimulation on finite models, but decidability and termination. The naive approach, using an explicit construction of the weak transition, may in itself introduce non-termination, so we prefer a direct implementation of the weak bisimulation definition, without constructing the weak automata beforehand, but searching on demand to construct the required weak transitions. We illustrate this approach on a simple error-correcting transport protocol case-study. Beside, we explore in [47] more pragmatic approaches using weak bisimulation preserving (pattern-based) reduction rules.

## References

[1] Sergio Abriola, Pablo Barceló, Diego Figueira, and Santiago Figueira. Bisimulations on data graphs. *Journal of Artificial Intelligence Research*, 61:171–213, 2018.

[2] 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.

[3] André Arnold. Synchronised behaviours of processes and rational relations. *Acta Informatica*, 17:21–29, 1982.

[4] Paolo Baldan, Andrea Bracciali, and Roberto Bruni. Bisimulation by unification. In *AMAST 2002 - Algebraic Methodology and Software Technology, 9th International Conference*, volume 2422 of *Lecture Notes in Computer Science*, pages 254–270. Springer, 2002.

[5] Paolo Baldan, Andrea Bracciali, and Roberto Bruni. A semantic framework for open processes. *Theoretical Computer Science*, 389(3):446–483, 2007.
[6] 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.

[7] Harsh Beohar, Barbara König, Sebastian Küpper, and Alexandra Silva. Conditional transition systems with upgrades. *Science of Computer Programming*, 186:102320, 2020.

[8] Simon Bliudze, Ludovic Henrio, and Eric Madelaine. Verification of concurrent design patterns with data. In Hanne Riis Nielson and Emilio T Costo, editors, *COORDINATION 2019 - 21st International Conference on Coordination Models and Languages*, volume LNCS-11533 of *Coordination Models and Languages*, pages 161-181. Springer International Publishing, 2019.

[9] Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced. *Journal of the ACM*, 42(1):232-268, 1995.

[10] Tommaso Bolognesi and Ed Brinksma. Introduction to the ISO specification language LOTOS. *Computer Networks*, 14(1):25-59, 1987.

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

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

[13] 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.

[14] Muffy Calder and Carron Shankland. A symbolic semantics and bisimulation for full LOTOS. In *FORTE 2001 - 21st International Conference on Formal Techniques for Networked and Distributed Systems*, pages 185-200. Springer, 2001.

[15] Robert De Simone. Higher-level synchronising devices in MEIJE-SCCS. *Theoretical Computer Science*, 37:245-267, 1985.

[16] 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 *Lecture Notes in Computer Science*, pages 133-145. Springer, 2007.
[17] Jérémy Dubut. Bisimilarity of Diagrams. In *RAMiCS 2020 - Relational and Algebraic Methods in Computer Science, 18th International Conference*, volume 12062 of *Lecture Notes in Computer Science*, pages 65–81. Springer, 2020.

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

[19] Nuno Gaspar, Ludovic Henrio, and Eric Madelaine. Formally reasoning on a reconfigurable component-based system - A case study for the industrial world. In *FACS 2013 - Formal Aspects of Component Software, 10th International Symposium.*, volume 8348 of *Lecture Notes in Computer Science*, pages 137–156. Springer, 2013.

[20] Jan Friso Groote. Transition system specifications with negative premises. *Theoretical Computer Science*, 118(2):263–299, 1993.

[21] 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.

[22] Jan Friso Groote, Mohammad Reza Mousavi, and Michel A. Reniers. A hierarchy of SOS rule formats. *Electronic Notes in Theoretical Computer Science*, 156(1):3–25, 2006. Proceedings of the Second Workshop on Structural Operational Semantics.

[23] Jan Friso Groote and Frits Vaandrager. Structured operational semantics and bisimulation as a congruence. *Information and Computation*, 100(2):202–260, 1992.

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

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

[26] Matthew Hennessy and Julian Rathke. Bisimulations for a calculus of broadcasting systems. *Theoretical Computer Science*, 200(1-2):225–260, 1998.

[27] Ludovic Henrio, Oleksandra Kulankhina, Siqi Li, and Eric Madelaine. Integrated environment for verifying and running distributed components. In *FASE 2016 - 19th International Conference on Fundamental Approaches to Software Engineering*, pages 66–83. Springer Berlin Heidelberg, 2016.

[28] Ludovic Henrio, Eric Madelaine, and Min Zhang. A Theory for the Composition of Concurrent Processes. In *FORTE 2016 - 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems*, volume 9688, pages 175–194. Springer, 2016.
[29] Zechen Hou and Eric Madelaine. Symbolic Bisimulation for Open and Parameterized Systems. In *PEPM 2020 - Workshop on Partial Evaluation and Program Manipulation*. ACM SIGPLAN, 2020.

[30] Zechen Hou, Eric Madelaine, Jing Liu, and Yuxin Deng. Symbolic Bisimulation for Open and Parameterized Systems - Extended version. Research Report RR-9304, Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France ; East China Normal University (Shanghai), November 2019.

[31] 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.

[32] Anna Ingólfsdóttir and Huimin Lin. A symbolic approach to value-passing processes. In *Handbook of Process Algebra*, pages 427–478. North-Holland/Elsevier, 2001.

[33] Kenneth Johnson and Radu Calinescu. Efficient Re-resolution of SMT Specifications for Evolving Software Architectures. In *QoSA 2014 - 10th International ACM Sigsoft Conference on Quality of Software Architectures*, pages 93–102. ACM, 2014.

[34] Kenneth Johnson, Radu Calinescu, and Shinji Kikuchi. An incremental verification framework for component-based software systems. In *CBSE 2013 - 16th International ACM Sigsoft Symposium on Component-based Software Engineering*, pages 33–42. ACM, 2013.

[35] Kim G. Larsen. A context dependent equivalence between processes. *Theoretical Computer Science*, 49:184–215, 1987.

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

[37] Maurice Laveaux and Tim A. C. Willemse. Decomposing monolithic processes in a process algebra with multi-actions. In *ICE*, volume 347 of *EPTCS*, pages 57–76, 2021.

[38] Huimin Lin. Symbolic transition graph with assignment. In *CONCUR '96 - Concurrency Theory, 7th International Conference*, volume 1119, pages 50–65. Springer Berlin Heidelberg, 1996.

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

[40] Robin Milner. *A Calculus of Communicating Systems*. Springer-Verlag, Berlin, Heidelberg, 1982.
[41] Robin Milner. *Communication and Concurrency*. Int. Series in Computer Science. Prentice-Hall, Englewood Cliffs, New Jersey, 1989. SU Fisher Research 511/24.

[42] Gordon D. Plotkin. A structural approach to operational semantics. *Journal of Logic and Algebraic Programming*, 60-61:17-139, 2004.

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

[44] Xudong Qin, Simon Bliudze, Eric Madelaine, and Min Zhang. Using SMT engine to generate Symbolic Automata - Extended version. Research Report RR-9177, Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France; inria, June 2018.

[45] Robert Jan Van Glabbeek. The meaning of negative premises in transition system specifications II. *The Journal of Logic and Algebraic Programming*, 60-61:229-258, 2004.

[46] Biyang Wang, Eric Madelaine, and Min Zhang. New symbolic model and equivalences checking for open automata. In *SMC 2021 - IEEE International Conference on Systems, Man, and Cybernetics*, pages 2360-2367. IEEE, 2021.

[47] 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), 2021.
# Appendix A. Proof on FH-bisimulation

## Appendix A.1. Bisimilarity is an equivalence: Proof of Theorem 1

Suppose $\mathcal{R}$ is an FH-bisimilarity. Then $\mathcal{R}$ is an equivalence, that is, $\mathcal{R}$ is reflexive, symmetric and transitive.

**PROOF.** It is trivial to check reflexivity and symmetry. Here we focus on the transitivity. To prove transitivity of strong FH-bisimilarity on pNets it is sufficient to prove transitivity of the strong FH-bisimilarity on states. Consider 3 open automata $\mathcal{T}_1, \mathcal{T}_2, \mathcal{T}_3$ and states $s, t, u$ in those automata<fnref n="12" />. Suppose we have $\mathcal{R}$ an FH-bisimulation relation between states of $\mathcal{T}_1$ and of $\mathcal{T}_2$; members of $\mathcal{R}$ are of the form $(s, t|\text{Pred}_{s,t})$. Suppose we also have $\mathcal{R}'$ an FH-bisimulation relation between states of $\mathcal{T}_2$ and of $\mathcal{T}_3$; members of $\mathcal{R}'$ are of the form $(t, u|\text{Pred}_{t,u})$.

Let $\mathcal{R}''$ be the relation:

$$ \mathcal{R}'' = \{(s, u|\text{Pred}_{s,u}) \mid \begin{array}{l} \text{Pred}_{s,u} = \bigvee \text{Pred}_{s,t} \wedge \text{Pred}_{t,u} \\ (s, t|\text{Pred}_{s,t}) \in \mathcal{R} \\ (t, u|\text{Pred}_{t,u}) \in \mathcal{R}' \end{array} \} $$

This relation is the adaptation of the transitivity to the conditional relationship that defines a bisimulation. Indeed the global disjunction together with the conjunction of predicates plays exactly the role of the intermediate element in a transitivity rule: “there exists an intermediate state” corresponds to the global disjunction, and the conjunction of states expresses the intermediate predicate is used to ensure satisfiability of the predicate relating the first state to the last one.

The relation is built as follows: for each pair of states $s, u$, for each state $t$ such that $\mathcal{R}$ relates $s$ and $t$, and $\mathcal{R}'$ relates $t$ and $u$, we take the conjunction of the two predicates. The predicates for different values of $t$ are collected by a disjunction.

We will show that $\mathcal{R}''$ is an FH-bisimulation. Consider $(s, u|\text{Pred}_{s,u}) \in \mathcal{R}''$. Then there is a set of states of $\mathcal{T}_2$ relating $s$ and $u$, let $(t_p)_{p \in P}$ be this family. We have $\text{Pred}_{s,u} = \bigvee_{p \in P} \text{Pred}_{s,p} \wedge \text{Pred}_{p,u}$.

For any $p \in P$ by definition of $\mathcal{R}'', (s, t_p|\text{Pred}_{s,p}) \in \mathcal{R}$, and $(t_p, u|\text{Pred}'_{p,u}) \in \mathcal{R}'$. We have the following by definition of bisimulation: For any open transition $\mathcal{OT}$ in $\mathcal{T}_1$ originating from $s$.

$$ \beta_{j \in J_1}^{s \to s'} \text{, } \text{Pred}_{\mathcal{OT}}, \text{Post}_{\mathcal{OT}} $$

<footnote n="12">¹²We omit the constraints stating that each $s_x, t_x, u_x$ is in the states of $\mathcal{T}_1, \mathcal{T}_2, \mathcal{T}_3$ for the sake of readability.</footnote>
There exists an indexed set of open transitions $OT_{px}^{x \in X} \subseteq \mathcal{T}_2$:

$$ \frac{\beta_{jpx}^{j \in J_{px}}, Pred_{OT_{px}}, Post_{OT_{px}}}{t_p \xrightarrow{\alpha_{px}} t_{px}} (*) $$

such that $\forall x, J_1 = J_{px}, (s', t_{px} | Pred_{px}) \in \mathcal{R}$; and

$$ Pred_{s,p} \wedge Pred_{OT} \implies \bigvee_{x \in X} \left( \forall j. \beta_j = \beta_{jpx} \wedge Pred_{OT_{px}} \wedge \alpha = \alpha_{px} \wedge Pred_{px} \{ \text{Post}_{OT} \uplus \text{Post}_{OT_{px}} \} \right) $$

For any open transition $OT_{px}$, since $(t_p, u | Pred'_{p,u}) \in \mathcal{R}'$ there exists an indexed set of open transitions $OT_{pxy}^{y \in Y} \subseteq \mathcal{T}_3$:

$$ \frac{\beta_{jpxy}^{j \in J_{pxy}}, Pred_{OT_{pxy}}, Post_{OT_{pxy}}}{u \xrightarrow{\alpha_{pxy}} u_{pxy}} (***) $$

such that $\forall y, J_{px} = J_{pxy}, (t_{px}, u_{pxy} | Pred_{pxy}) \in \mathcal{R}'$; and

$$ Pred'_{p,u} \wedge Pred_{OT_{px}} \implies \bigvee_{y \in Y} \left( \forall j. \beta_{jpx} = \beta_{jpxy} \wedge Pred_{OT_{pxy}} \wedge \alpha_{px} = \alpha_{pxy} \wedge Pred_{pxy} \{ \text{Post}_{OT_{px}} \uplus \text{Post}_{OT_{pxy}} \} \right) $$

This is verified for each $p \in P$.

Overall, we have a family of open transitions $OT_{pxy}^{p \in P, x \in X, y \in Y} \subseteq \mathcal{T}_3$ that should simulate $OT$.

First, we have $\forall y, \forall x, \forall p, J_1 = J_{px} = J_{pxy}, (s', u_{pxy} | Pred'_{pxy}) \in \mathcal{R}''$ for some $Pred'_{pxy}$. Indeed for any $p, x$, and $y$, $t_{px}$ relates $s'$ and $u_{pxy}$, we have $(s', t_{px} | Pred_{px}) \in \mathcal{R}$ and $(t_{px}, u_{pxy} | Pred_{pxy}) \in \mathcal{R}'$. More precisely, $t_{px} \in (t'_p)^{p \in P'}$ where $(t'_p)^{p \in P'}$ and $P' \subseteq P$ is the set of states relating $s'$ and $u_{pxy}$ (the states used in the open transition must belong to the set of states ensuring the transitive relation). Additionally, for all $p, x, y, Pred_{px} \wedge Pred_{pxy} \implies Pred'_{pxy}$ (this is one element of the disjunction defining the predicate $Pred'_{pxy}$ relating $s'$ and $u_{pxy}$ in the definition of $\mathcal{R}''$).

One can notice that, as bisimulation predicates are used to relate states that belong to two different open automata, the free variables of these predicates that do not belong to the two related automata can safely be renamed to avoid any name clash. In practice, we can suppose that $Pred'_{pxy}$ does not contain the variables of $\mathcal{T}_2$ because it is used to relate states of $\mathcal{T}_1$ and $\mathcal{T}_3$. Indeed if $Pred'_{pxy}$ uses variables of $\mathcal{T}_2$, we can consider instead another predicate that is equivalent to $Pred'_{pxy}$ and does not contain the variables of $\mathcal{T}_2$ (this is safe according to the semantic interpretation of open automata and relations). Similarly, we can
suppose that $Pred_{px}$ contains no variable in $T_3$, and $Pred_{pxy}$ contains no variable in $T_1$.

Second, by definition of bisimulation we need (recall that $Pred_{s,u}$ is the original predicate relating $s$ and $u$ by definition of the transitive closure):

$$Pred_{s,u} \wedge Pred_{OT} \implies \bigvee_{x \in X} \bigvee_{y \in Y} \bigvee_{p \in P} \left( \forall j. \beta_j = \beta_{jpxy} \wedge Pred_{OT_{pxy}} \wedge \alpha = \alpha_{pxy} \wedge Pred'_{pxy} \{ \{Post_{OT} \uplus Post_{OT_{pxy}}\} \} \right).$$

From (*) and (**) we have:

for all $p$, $Pred_{s,p} \wedge Pred_{OT} \wedge Pred_{p,u}$

$$\implies \bigvee_{x \in X} \left( \forall j. \beta_j = \beta_{jp_x} \wedge Pred_{OT_{p_x}} \wedge \alpha = \alpha_{p_x} \wedge Pred_{px} \{ \{Post_{OT} \uplus Post_{OT_{px}}\} \} \right) \wedge Pred_{p,u}$$

$$\implies \bigvee_{x \in X} \left( \forall j. \beta_j = \beta_{jp_x} \wedge (Pred_{OT_{px}} \wedge Pred_{p,u}) \wedge \alpha = \alpha_{px} \wedge Pred_{px} \{ \{Post_{OT} \uplus Post_{OT_{px}}\} \} \right)$$

$$\implies \bigvee_{x \in X} \left( \forall j. \beta_j = \beta_{jp_x} \wedge \bigvee_{y \in Y} \left( \forall j'. \beta_{j'px} = \beta_{j'pxy} \wedge Pred_{OT_{pxy}} \wedge \alpha_{px} = \alpha_{pxy} \wedge Pred_{pxy} \{ \{Post_{OT_{px}} \uplus Post_{OT_{pxy}}\} \} \right) \wedge \alpha = \alpha_{px} \wedge Pred_{px} \{ \{Post_{OT} \uplus Post_{OT_{px}}\} \} \right)$$

$$\implies \bigvee_{x \in X} \bigvee_{y \in Y} \left( \forall j, j'. \beta_j = \beta_{jp_x} \wedge \beta_{j'px} = \beta_{j'pxy} \wedge \left( Pred_{OT_{pxy}} \wedge \alpha = \alpha_{px} = \alpha_{pxy} \wedge Pred_{pxy} \{ \{Post_{OT_{px}} \uplus Post_{OT_{pxy}}\} \} \wedge Pred_{px} \{ \{Post_{OT} \uplus Post_{OT_{px}}\} \} \right) \right)$$

By construction, four substitution functions $\{ \} \{ \}$ only have an effect on the variables of the open automaton they belong to, they also produce terms containing only variables of the open automaton they belong to. Finally, because of the domain of the substitution functions of the predicates, we have:

$$Pred_{px} \{ \{Post_{OT} \uplus Post_{OT_{px}}\} \} \wedge Pred_{pxy} \{ \{Post_{OT_{px}} \uplus Post_{OT_{pxy}}\} \} \Leftrightarrow$$

$$Pred_{px} \{ \{Post_{OT} \uplus Post_{OT_{px}} \uplus Post_{OT_{pxy}}\} \} \wedge Pred_{pxy} \{ \{Post_{OT} \uplus Post_{OT_{px}} \uplus Post_{OT_{pxy}}\} \}$$

$$\implies Pred'_{pxy} \{ \{Post_{OT} \uplus Post_{OT_{px}} \uplus Post_{OT_{pxy}}\} \} \Leftrightarrow$$

$$Pred'_{pxy} \{ \{Post_{OT} \uplus Post_{OT_{px}}\} \}$$

This allows us to conclude, with $Pred_{s,u} = \bigvee_{p \in P} Pred_{s,p} \wedge Pred_{p,u}$:

$$\implies \bigvee_{p \in P} (Pred_{s,p} \wedge Pred_{p,u} \wedge Pred_{OT})$$

$$\implies \bigvee_{p \in P} \bigvee_{x \in X} \bigvee_{y \in Y} \left( \forall j, j'. \beta_j = \beta_{jp_x} \wedge \beta_{j'px} = \beta_{j'pxy} \wedge Pred_{OT_{pxy}} \wedge \alpha = \alpha_{px} = \alpha_{pxy} \wedge Pred'_{pxy} \{ \{Post_{OT} \uplus Post_{OT_{pxy}}\} \} \right)$$

$$\implies \bigvee_{x \in X} \bigvee_{y \in Y} \bigvee_{p \in P} \left( \forall j. \beta_j = \beta_{jpxy} \wedge Pred_{OT_{pxy}} \wedge \alpha = \alpha_{pxy} \wedge Pred'_{pxy} \{ \{Post_{OT} \uplus Post_{OT_{pxy}}\} \} \right)$$

Concerning the other direction of bisimulation, it is sufficient to notice that the role of $s$ and $u$ in the definition of $\mathcal{R}''$ is symmetrical, and thus the proof is similar. $\square$
Appendix A.2. Composition Lemmas

The proofs of the composition theorems for FH-bisimilarity rely on two main lemmas, dealing respectively with the decomposition of a composed behaviour between the context and the internal pNet, and with their recomposition.

**Lemma 1: Open transition decomposition**

Consider two pNets P and Q that are not pLTSs<fnref n="13" />. Let Leaves(Q) = $p_l^{l \in L_Q}$; suppose:

$$P[Q]_{j_0} \models \frac{\beta_j^{j \in J}, \text{Pred}, \text{Post}}{\triangleleft s_i^{i \in L} \triangleright \xrightarrow{\alpha} \triangleleft s_i^{i' \in L} \triangleright}$$

with $J \cap \text{Holes}(Q) \neq \emptyset$ or $\exists i \in L_Q, s_i \neq s_i'$, i.e. Q takes part in the reduction. Then, there exist $\alpha_Q, \text{Pred}', \text{Pred}'', \text{Post}', \text{Post}''$ s.t.:

$$P \models \frac{\beta_j^{j \in (J \setminus \text{Holes}(Q)) \cup \{j_0\}}, \text{Pred}', \text{Post}'}{\triangleleft s_i^{i \in L \setminus L_Q} \triangleright \xrightarrow{\alpha} \triangleleft s_i^{i' \in L \setminus L_Q} \triangleright}$$

$$\text{and } Q \models \frac{\beta_j^{j \in J \cap \text{Holes}(Q)}, \text{Pred}'', \text{Post}''}{\triangleleft s_i^{i \in L_Q} \triangleright \xrightarrow{\alpha_Q} \triangleleft s_i^{i' \in L_Q} \triangleright}$$

and $\text{Pred} \iff \text{Pred}' \wedge \text{Pred}'' \wedge \alpha_Q = \beta_{j_0}, \text{Post} = \text{Post}' \uplus \text{Post}''$ where $\text{Post}''$ is the restriction of $\text{Post}$ over variables $\text{vars}(Q)$.

**Preliminary note:** The introduction of fresh variables introduce alpha-conversion at many points of the proof; we only give major arguments concerning alpha-conversion to make the proof readable; in general, fresh variables appear in each transition inside terms $\beta_j, v$, and $\text{Pred}$.

**PROOF.** Consider rule **Tr2** in Definition 9, applied to the pNet $P[Q]_{j_0}$.

$$\text{Leaves}(\langle\langle P_m^{m \in I}, \overline{\text{Sort}}, SV_k^{k \in K} \rangle\rangle) = pLTS_l^{d \in L} \quad k \in K \quad SV_k = (\alpha'_m)^{m \in I_1 \uplus I_2 \uplus J} \to \alpha'[e_b] \\ \forall m \in I_1. P_m \models \frac{\beta_j^{j \in J_m}, \text{Pred}_m, \text{Post}_m}{\triangleleft s_i^{i \in L_m} \triangleright \xrightarrow{\alpha_m} \triangleleft (s_i^{i'} \in L_m) \triangleright} \quad \emptyset, \text{Pred}_m, \text{Post}_m \\ J' = \bigcup_{m \in I_1} J_m \uplus J \quad \text{Pred} = \bigwedge_{m \in I_1 \uplus I_2} \text{Pred}_m \wedge \text{Pred}_v(SV_k, \alpha_m^{m \in I_1 \uplus I_2}, \beta_j^{j \in J}, \alpha) \\ \forall i \in L \setminus \left( \bigcup_{m \in I_1} L_m \uplus I_2 \right) . s_i' = s_i \quad \text{fresh}(\alpha'_m, \alpha', \beta_j, \alpha)$$

Tr2

$$\frac{\beta_j^{j \in J'}, \text{Pred}, \bigcup_{m \in I_1 \uplus I_2} \text{Post}_m}{\triangleleft s_i^{i \in L} \triangleright \xrightarrow{\alpha} \triangleleft (s_i^{i'} \in L) \triangleright} \langle\langle P_m^{m \in I}, \overline{\text{Sort}}, SV_k^{k \in K} \rangle\rangle \models$$

<footnote n="13">¹³A similar lemma can be proven for a pLTS Q.</footnote>
We know each premise is True for $P[Q]_{j_0}$. $j_0 \in I_1$ because $Q$ is not a pLTS. We try to prove the equivalent premise for $P$.

First, $K$ and the synchronisation vector $SV_k$ are unchanged (however $j_0$ passes from the set of sub-pNets to the set of holes). We have Leaves($P[Q]_{j_0}$) = Leaves($P$) $\cup$ Leaves($Q$).

Now focus on the OTs of the sub-pNets. For each $m \in I_1 \cup I_2$ we have one of the two following OT:

either $m$ in $I_1$

$$ P_m \models \frac{\beta_j^{j \in J_m}, Pred_m, Post_m}{\triangleleft s_i^{i \in L_m} \triangleright \xrightarrow{\alpha_m} \triangleleft (s_i')^{i \in L_m} \triangleright} $$

or, $m$ in $I_2$

$$ P_m \models \frac{\emptyset, Pred_m, Post_m}{\triangleleft s_m \triangleright \xrightarrow{\alpha_m} \triangleleft s'_m \triangleright} $$

Only elements of $(I_1 \cup I_2) \setminus \{j_0\}$ are useful to assert the premise for reduction of $P$; the last one ensures the open transition for the pNet $Q$ (note that $Q$ is at place $j_0$, and by definition of the open transition for $P[Q]_{j_0}$, $L_{j_0} = L_Q$, and $J_{j_0} = J \cap \text{Holes}(Q)$):

$$ Q \models \frac{\beta_j^{j \in J \cap \text{Holes}(Q)}, Pred_{j_0}, Post''}{\triangleleft s_i^{i \in L_Q} \triangleright \xrightarrow{\alpha_{j_0}} \triangleleft (s_i')^{i \in L_Q} \triangleright} $$

This already ensures the second part of the conclusion of the lemma, i.e. the OT for $Q$ if we choose $\alpha_Q = \alpha_{j_0}$ and $Pred'' = Pred_{j_0}$. Considering the OT of $P$ we have another $J'$ that is $J'_p = J' \setminus \text{Holes}(Q) \cup \{j_0\}$; we denote $I'_1 = I_1 \setminus \{j_0\}$ the predicate is $Pred' = \bigwedge_{m \in I'_1 \cup I_2} Pred_m \wedge Pred_{sv}(SV_k, \alpha_m^{m \in I'_1 \cup I_2}, \beta_j^{j \in J \cup \{j_0\}}, \alpha)$

where

$$ Pred_{sv}(SV_k, \alpha_m^{m \in I'_1 \cup I_2}, \beta_j^{j \in J \cup \{j_0\}}, \alpha) \Leftrightarrow $$

$$ \forall i \in I'_1 \cup I_2. \alpha_i = \alpha'_i \wedge \forall j \in J \cup \{j_0\}. \beta_j = \alpha'_j \wedge \alpha = \alpha' \wedge e_b $$

Modulo renaming of fresh variables, this is identical to the predicate that occurs in the source open transition except $\alpha_{j_0} = \alpha'_{j_0}$ has been replaced by $\beta_{j_0} = \alpha'_{j_0}$. As $\alpha_{j_0} = \alpha_Q$ and $\beta_{j_0}$ is free, we have $\beta_{j_0} = \alpha'_{j_0} \wedge \beta_{j_0} = \alpha_Q \iff \alpha_{j_0} = \alpha'_{j_0}$. Thus, $Pred \iff (Pred' \wedge Pred'') \wedge \alpha_Q = \beta_{j_0}$. Finally, Post into conditions of the context $P$ and the pNet $Q$ (they are built similarly as they only deal with leaves): $Post = Post' \cup Post''$. This concludes the proof as we checked all the premises of the open transition for both $P$ and $Q$. We obtain the following reduction by the rule Tr2:
$$
\text{Leaves}(\langle\langle P_m^{m \in I \setminus \{j_0\}}, \overline{\text{Sort}}, SV_k^{k \in K} \rangle\rangle) = pLTS_l^{I \in L} \quad k \in K \quad SV_k = (\alpha'_m)^{m \in I_1 \uplus I_2 \uplus J} \to \alpha'[e_b]
$$
$$
\beta_j^{j \in J_m}, \text{Pred}_m, \text{Post}_m \qquad \emptyset, \text{Pred}_m, \text{Post}_m
$$
$$
\forall m \in I_1 \setminus \{j_0\}. P_m \models \bigcirc_{\prec s'_i \in L_m \succ \alpha_m} \bigcirc_{\prec (s'_i)^{i \in L_m} \succ} \forall m \in I_2. P_m \models \bigcirc_{\prec s'_m \succ \alpha_m} \bigcirc_{\prec (s'_m)^{i \in L_m} \succ}
$$
$$
J' = \bigcup_{m \in I_1 \setminus \{j_0\}} J_m \uplus J
$$
$$
\text{Pred}' = \bigwedge_{m \in I_1 \uplus I_2 \setminus \{j_0\}} \text{Pred}_m \wedge \text{Pred}_{sv}(SV_k, \alpha_m^{m \in I_1 \uplus I_2 \setminus \{j_0\}}, \beta_j^{j \in J \cup \{j_0\}}, \alpha)
$$
$$
\forall i \in L \setminus \left( \bigcup_{m \in I_1 \setminus \{j_0\}} L_m \uplus I_2 \right) . s'_i = s_i \quad \text{fresh}(\alpha'_m, \alpha', \beta_j, \alpha)
$$

$$
\beta_j^{j \in J \setminus \text{Holes}(Q) \cup \{j_0\}}, \text{Pred}', \bigcup_{m \in I_1 \setminus \{j_0\} \cup I_2} \text{Post}_m
$$
$$
\langle\langle P_m^{m \in I \setminus \{j_0\}}, \overline{\text{Sort}}, SV_k^{k \in K} \rangle\rangle \models \bigcirc_{\prec s'_i \in L \setminus L_Q \succ \alpha} \bigcirc_{\prec (s'_i)^{i \in L \setminus L_Q} \succ}
$$
$$
\square
$$

In general, the actions that can be emitted by $Q$ is a subset of the possible
actions of the holes, and the predicate involving $v_Q$ and the synchronisation
vector is more restrictive than the one involving only the variable $\beta_{j_0}$. This has
no impact on the previous proof and this restriction results from the composition
of predicates.

**Lemma 2: Open transition composition**

Consider two pNets $P$ and $Q$ where $P$ is not a pLTS. Suppose $j_0 \in J$ and:

$$
P \models \beta_j^{j \in J}, \text{Pred}, \text{Post} \\
\qquad \bigcirc_{\prec s'_i \in L} \alpha \to \prec s'_i \in L \succ \\
\text{and} \\
Q \models \beta_j^{j \in J_Q}, \text{Pred}', \text{Post}' \\
\qquad \bigcirc_{\prec s'_i \in L_Q} \alpha_Q \to \prec s'_i \in L_Q \succ
$$

Then, we have:

$$
P[Q]_{j_0} \models \beta_j^{(j \in J \setminus \{j_0\}) \uplus J_Q}, \text{Pred} \wedge \text{Pred}' \wedge \alpha_Q = \beta_{j_0}, \text{Post} \uplus \text{Post}' \\
\qquad \bigcirc_{\prec s'_i \in L \uplus L_Q} \alpha \to \prec s'_i \in L \uplus L_Q \succ
$$

Note that this does not mean that any two pNets can be composed and
produce an open transition. Indeed, the predicate *Pred* ∧ *Pred'* ∧ *α*<sub>*Q*</sub> = *β*<sub>*j*<sub>0</sub></sub> will
not be satisfiable if the action of *α*<sub>*Q*</sub> cannot be matched with *β*<sub>*j*<sub>0</sub></sub>. Note also
that *β*<sub>*j*<sub>0</sub></sub> is now only used as an intermediate term inside formulas: it does not
appear neither as global action nor as an action of a hole.
PROOF. Let $P = \langle\langle P_m^{m \in I}, \overline{Sort}, SV_k^{k \in K} \rangle\rangle$. Consider first the open transition derived from $P$. Consider each premise of the open transition (constructed by **Tr2** rule in Definition 9).

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\text{Leaves}(\langle\langle P_m^{m \in I}, \overline{Sort}, SV_k^{k \in K} \rangle\rangle) = pLTS_l^{d \in L} & k \in K & SV_k = (\alpha'_m)^{m \in I_1 \uplus I_2 \uplus J} \to \alpha'[e_b] \\
\beta_j^{j \in J_m}, Pred_m, Post_m & \emptyset, Pred_m, Post_m & \\
\forall m \in I_1. P_m \models \quad \begin{array}[t]{@{}c@{\quad}l@{}}
  \multicolumn{2}{@{}c@{}}{\text{\textbf{...................}} \\
  \llcorner s_i^{i \in L_m} \triangleright \xrightarrow{\alpha_m} \llcorner (s'_i)^{i \in L_m} \triangleright \\
  \multicolumn{2}{@{}c@{}}{\text{...................}}}
\end{array} & \forall m \in I_2. P_m \models \quad \begin{array}[t]{@{}c@{\quad}l@{}}
  \multicolumn{2}{@{}c@{}}{\text{\textbf{...................}} \\
  \llcorner s_m \triangleright \xrightarrow{\alpha_m} \llcorner s'_m \triangleright \\
  \multicolumn{2}{@{}c@{}}{\text{...................}}}
\end{array} \\
J' = \biguplus_{m \in I_1} J_m \uplus J & \text{Pred} = \bigwedge_{m \in I_1 \uplus I_2} \text{Pred}_m \wedge \text{Pred}_{sv}(SV_k, \alpha_m^{m \in I_1 \uplus I_2}, \beta_j^{j \in J}, \alpha) & \\
\forall i \in L \setminus \left( \biguplus_{m \in I_1} L_m \uplus I_2 \right) . & s'_i = s_i & \text{fresh}(\alpha'_m, \alpha', \beta_j, \alpha)
\end{array}
$$

Tr2

$$
\beta_j^{j \in J'}, Pred, \biguplus_{m \in I_1 \uplus I_2} Post_m
$$

We know each premise is True for *P* and try to prove the equivalent premise for *P*[*Q*]>*j*₀ (using the open transition of *Q*). *P*[*Q*]>*j*₀ exhibits a similar **Tr2** rule where *K* and the synchronisation vector are unchanged (*j*₀ is now in the set of sub-*pNets*); *SV*<sub>*k*</sub> = (*α*'<sub>*j*</sub>)<sup>*j* ∈ *I*<sub>1</sub>∪*j*∈*Q*</sup> ⊎ *J* → *α*'[*e*<sub>*b*</sub>]. Leaves(*P*[*Q*]>*j*₀) = Leaves(*P*) ⊎ Leaves(*Q*). *I* and *J* are the set of leaves and holes of *P*, *I*₁ ⊎ *I*₂ and *J*′ are the sets of moving leaves and holes in the reduction of *P*. All sub-*pNets* of must be reduced, we need:

$$
\forall m \in I_1 \uplus \{j_0\}. P_m \models \quad \begin{array}[t]{@{}c@{}} \beta_j^{j \in J_m}, \text{Pred}_m, \text{Post}_m \\ \llcorner s_i^{i \in L_m} \triangleright \xrightarrow{\alpha_m} \llcorner (s'_i)^{i \in L_m} \triangleright \end{array}
$$

$$
\forall m \in I_2. P_m \models \quad \begin{array}{@{}c@{}} \emptyset, \text{Pred}_m, \text{Post}_m \\ \llcorner s_m \triangleright \xrightarrow{\alpha_m} \llcorner s'_m \triangleright \end{array}
$$

the sub-pNet at position $j_0$ is the one filled by $Q$ (we define $P_{j_0} = Q$ and similarly $J_m = J_Q$, $Pred_m = Pred'$, $Post_m = Post'$, ... are the elements of the OT of $Q$) which offers an open transition by hypothesis, the other open transitions are immediate consequence of the open transition that can be performed by $P$ (premises of **Tr2**). The set of moving leaves is the union of the moving leaves in the open transition for $P$ and the ones for $Q$; similarly the moving holes are the union of the moving holes, minus $j_0$: $J'_{PQ} = J \setminus \{j_0\} \uplus J_Q$. The predicate for the open transition is:

$$
Pred'' = \bigwedge_{m \in I_1 \uplus I_2} Pred_m \wedge Pred' \wedge Pred(SV_k, v_i^{i \in I_1 \uplus I_2} \uplus (j_0 \mapsto v_Q), \beta_j^{j \in J}, \alpha).
$$

By definition we have:

$Pred(SV_k, \alpha_i^{i \in I} \uplus (j_0 \to \alpha_Q), \beta_j^{j \in J}, v) \iff \forall i \in I. \alpha_i = \alpha'_i \wedge \forall j \in J. \beta_j = \alpha'_j \wedge \alpha = \alpha' \wedge \alpha_Q = \alpha_{j_0} \wedge e_b$, this is equivalent to $\forall i \in I. \alpha_i = \alpha'_i \wedge \forall j \in J. \beta_j = \alpha'_j \wedge \alpha = \alpha' \wedge \alpha_Q = \beta_{j_0} \wedge \beta_{j_0} = \alpha_{j_0} \wedge e_b$ and by definition of $Pred$ (as obtained by applying **Tr2** rule), $Pred'' \iff Pred \wedge Pred' \wedge \alpha_Q = \beta_{j_0}$. The post-condition gathers
the post-conditions related to all the leaves: $\biguplus$ Post$_m = Post \uplus Post'$.

$m \in I_1 \cup \{j_0\} \uplus I_2$

Finally, the composed open transition can be built by **Tr2** rule as follows:

$$ \text{Leaves}(\langle\langle P_m^{m \in I \cup \{j_0\}}, \overline{Sort}, SV_k^{k \in K} \rangle\rangle) = pLTS_l^{d \in L} \quad k \in K \quad SV_k = (\alpha'_m)^{m \in I_1 \uplus I_2 \uplus J} \to \alpha'[e_b] $$

$$ \beta_j^{j \in J_m}, Pred_m, Post_m \qquad \emptyset, Pred_m, Post_m $$

$$ \forall m \in I_1 \cup \{j_0\}. P_m \models \underset{\Delta s_i^{i \in L_m} \triangleright \xrightarrow{\alpha_m} \Delta (s'_i)^{i \in L_m \Delta}}{\cdots\cdots\cdots\cdots\cdots\cdots\cdots\cdots\cdots\cdots} \quad \forall m \in I_2. P_m \models \underset{\Delta s_m \triangleright \xrightarrow{\alpha_m} \Delta s'_m \Delta}{\cdots\cdots\cdots\cdots\cdots\cdots\cdots\cdots\cdots} $$

$$ J'_{PQ} = J \setminus \{j_0\} \uplus J_Q $$

$$ Pred'' = \bigwedge_{m \in I_1 \uplus I_2} Pred_m \wedge Pred' \wedge Pred(SV_k, v_i^{i \in I_1 \uplus I_2} \uplus (j_0 \to v_Q), \beta_j^{j \in J}, \alpha) $$

$$ \forall i \in L \setminus \left( \biguplus_{m \in I_1 \cup \{j_0\}} L_m \uplus I_2 \right) . s'_i = s_i \quad \text{fresh}(\alpha'_m, \alpha', \beta_j, \alpha) $$

$$ \langle\langle P_m^{m \in I}, \overline{Sort}, SV_k^{k \in K} \rangle\rangle \models \underset{\Delta s_i^{i \in L \uplus L_Q} \triangleright \xrightarrow{\alpha} \Delta (s'_i)^{i \in L \uplus L_Q \Delta}}{\beta_j^{j \in J'_{PQ}}, Pred'', Post \uplus Post'} $$

This provides the desired conclusion. □

Note that we also have the following lemma (trivial):

**Lemma 3 (Open transition composition – inactive).**

This lemma is the simple case where the pNet filling the hole is not involved in the transition. Suppose $j_0 \notin J$ and $L_Q = \text{Leaves}(Q)$:

$$ P \models \underset{\Delta s_i^{i \in L} \triangleright \xrightarrow{\alpha} \Delta s'_i^{i \in L \Delta}}{\beta_j^{j \in J}, Pred, Post} $$

Then, for any state $\Delta s_i^{i \in L_Q \Delta}$ of $Q$, we have:

$$ P[Q]_{j_0} \models \underset{\Delta s_i^{i \in L} \uplus s_i^{i \in L_Q} \triangleright \xrightarrow{\alpha} \Delta s'_i^{i \in L} \uplus s_i^{i \in L_Q \Delta}}{\beta_j^{j \in J}, Pred, Post} $$

The proof is trivial.

**Appendix A.3. Proof of Theorem 3**

**Congruence:** Consider an open pNet: $P = \langle\langle P_i^{i \in I}, Sort_j^{j \in J}, SV \rangle\rangle$. Let $j_0 \in J$ be a hole. Let $Q$ and $Q'$ be two FH-bisimilar pNets such that $Sort(Q) = Sort(Q') \subseteq Sort_{j_0}^{14}$. Then $P[Q]_{j_0}$ and $P[Q']_{j_0}$ are FH-bisimilar.

<footnote n="14">¹⁴Note that $Sort(Q) = Sort(Q')$ is ensured by strong bisimilarity.</footnote>
PROOF. The proof of Theorem 3 exhibits classically a bisimulation relation for a composed system. It considers then an open transition of $P[Q]_{j_0}$ that should be simulated. It then uses Lemma 1 to decompose the open transition of $P[Q]_{j_0}$ and obtain an open transition of $P$ and $Q$; the FH-bisimulation property can be applied to $Q$ to obtain an equivalent family of open transitions of $Q'$; this family is then recomposed by Lemma 2 to build a set of open transitions of $P[Q']_{j_0}$ that will simulate the original one.

Let Leaves($Q$) = $p_l^i \in L$, Leaves($Q'$) = $p_l'^i \in L'$, Leaves($P$) = $p_l^i \in L_P$. Consider $Q$ FH-bisimilar to $Q'$. It means that there is a relation $\mathcal{R}$ that is an FH-bisimulation between the open automata of the two pNets. We will consider the relation $\mathcal{R}' = \{(s, t | Pred_{s,t}) | s = s' \lor s'' \land t = t' \lor s'' \land s'' \in S_P \land (s', t' | Pred_{s,t}) \in \mathcal{R}\}$ where $S_P$ is the set of states of the open automaton of $P$. We will prove that $\mathcal{R}'$ is an open FH-bisimulation. Consider a pair of FH-bisimilar states: $(\Delta s_i^i \in L_P \lor L \triangleright, \Delta t_i^i \in L' \lor s_i^i \in L_P \triangleright | Pred_{s,t}) \in \mathcal{R}'$. Consider an open transition $OT$ of $P[Q]_{j_0}$.

$$ P[Q]_{j_0} \models \frac{\beta_j^{j \in J}, Pred_{OT}, Post_{OT}}{\Delta s_i^{i \in L_P \lor L} \triangleright \xrightarrow{\alpha} \Delta s_i'^{i \in L_P \lor L} \triangleright} $$

Let $J' = J \setminus \text{Holes}(Q) \cup \{j_0\}$. By Lemma 1 we have:

$$ P \models \frac{\beta_j^{j \in J'}, Pred', Post'}{\Delta s_i^{i \in L_P} \triangleright \xrightarrow{\alpha} \Delta s_i'^{i \in L_P} \triangleright} $$

$$ Q \models \frac{\beta_j^{j \in J \cap \text{Holes}(Q)}, Pred'', Post''}{\Delta s_i^{i \in L} \triangleright \xrightarrow{\alpha_Q} \Delta s_i'^{i \in L} \triangleright} $$

and $Pred_{OT} \iff Pred' \land Pred'' \land \alpha_Q = \beta_{j_0}$, $Post_{OT} = Pred' \lor Post''$ ($Post''$ is the restriction of $Post$ over $\text{vars}(Q)$). As $Q$ is FH-bisimilar to $Q'$ and $(\Delta s_i^i \in L \triangleright, \Delta t_i^i \in L' \triangleright | Pred_{s,t}) \in \mathcal{R}$ there is a family $OT_x'$ of open transitions of the automaton of $Q'$ such that

$$ Q' \models \frac{\beta_{jx}^{j \in J \cap \text{Holes}(Q)}, Pred_{OT_x}, Post_{OT_x}}{\Delta t_i^{i \in L'} \triangleright \xrightarrow{\alpha_x} \Delta t_{ix}^{i \in L'} \triangleright} $$

and $\forall x, (\Delta s_i^i \in L \triangleright, \Delta t_{ix}^i \in L' \triangleright | Pred_{sx}) \in \mathcal{R}$; and $Pred_{s,t} \land Pred'' \Rightarrow$

$$ \bigvee_{x \in X} \left( \forall j \in J \cap \text{Holes}(Q) . \beta_j = \beta_{jx} \land Pred_{OT_x} \land \alpha_Q = \alpha_x \land Pred_{s,x} \{ \text{Post}'' \lor \text{Post}_{OT_x} \} \right) $$

We can now apply Lemma 2 on each of the $OT_x'$ together with the transition of $P$ and obtain a new family $OT_x$ of open transitions (where for $i \in L_P$, $t_i = s_i$ and $t_{ix} = s_i'$, and for $j \in \text{Holes}(P)$, $\beta_{jx} = \beta_j$):

$$ P[Q']_{j_0} \models \frac{\beta_{jx}^{j \in J}, Pred' \land Pred_{OT_x} \land \alpha_x = \beta_{j_0 x}, Post' \lor Post_{OT_x}}{\Delta t_i^{i \in L' \lor L_Q} \triangleright \xrightarrow{\alpha_x} \Delta t_{ix}^{i \in L' \lor L_Q} \triangleright} $$

Observe that we used the fact that $J = (J \setminus \text{Holes}(Q) \cup \{j_0\}) \setminus \{j_0\} \cup (J \cap \text{Holes}(Q))$. Now we have to verify the conditions for the FH-bisimulation
between OT and $OT_x$. $\forall x, (\langle s' \rangle_i^{i \in L_P \uplus L_\triangleright}, \langle t \rangle_{ix}^{i \in L_P \uplus L'_\triangleright} | Pred_{s,x}) \in \mathcal{R}'$ (by definition of $\mathcal{R}'$) and in three steps we get:

$$Pred_{s,t} \wedge Pred_{\mathcal{O}T} \implies Pred_{s,t} \wedge Pred' \wedge Pred'' \wedge \alpha_Q = \beta_{j_0}$$

$$\implies \bigvee_{x \in X} \left( \forall j \in J \cap \text{Holes}(Q), \beta_j = \beta_{jx} \wedge Pred_{\mathcal{O}T_x} \wedge \alpha_Q = \alpha_x \wedge Pred_{s,x} \{ \langle \text{Post}'' \uplus \text{Post}_{\mathcal{O}T_x} \rangle \} \right) \wedge$$

$$Pred' \wedge \alpha_Q = \beta_{j_0}$$

$$\implies \bigvee_{x \in X} \left( \forall j \in J \cap \text{Holes}(Q), \beta_j = \beta_{jx} \wedge Pred' \wedge Pred_{\mathcal{O}T_x} \wedge \alpha_Q = \alpha_x \wedge \alpha_Q = \beta_{j_0x} \wedge \right.$$

$$Pred_{s,x} \{ \langle \text{Post}'' \uplus \text{Post}_{\mathcal{O}T_x} \rangle \}$$

Note that, $\beta_{j_0}$ can be transformed into $\beta_{j_0x}$ because of the implication hypothesis. The obtained formula reaches the goal except for two points:

* We need $\forall j \in J$ instead of $\forall j \in J \cap \text{Holes}(Q)$ but adding prerequisite on more variables does not change the validity of the formula (those variables are not used).

* Concerning the last term, we need $Pred_{s,x} \{ \langle \text{Post}_{\mathcal{O}T} \uplus (\text{Post}' \uplus \text{Post}_{\mathcal{O}T_x}) \rangle \}$, i.e. $Pred_{s,x} \{ \langle (\text{Post}' \uplus \text{Post}'') \uplus (\text{Post}' \uplus \text{Post}_{\mathcal{O}T_x}) \rangle \}$. We can conclude by observing that $Pred_{s,x}$ does not use any variable of $P$ and thus the substitution $\{ \langle \text{Post}' \rangle \}$ has no effect on it.

Finally:

$$Pred_{s,t} \wedge Pred_{\mathcal{O}T} \implies$$

$$\bigvee_{x \in X} \left( \forall j \in J. \beta_j = \beta_{jx} \wedge (Pred' \wedge Pred_{\mathcal{O}T_x} \wedge \alpha_Q = \beta_{j_0x}) \wedge \alpha_Q = \alpha_x \wedge Pred_{s,x} \{ \langle \text{Post}'' \uplus \text{Post}_{\mathcal{O}T_x} \rangle \} \right)$$

This proves the condition of the FH-simulation, the other direction is similar.

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

## Appendix A.4. Proof of Theorem 4: Context equivalence

Consider two FH-bisimilar open pNets: $P = \langle P_i^{i \in I}, Sort_j^{j \in J}, \overline{SV} \rangle$ and $P' = \langle P_i^{i \in I}, Sort_j^{j \in J}, \overline{SV} \rangle$ (recall they must have the same holes to be bisimilar). Let $j_0 \in J$ be a hole, and $Q$ be a pNet such that $Sort(Q) \subseteq Sort_{j_0}$. Then $P[Q]_{j_0}$ and $P'[Q]_{j_0}$ are FH-bisimilar.

PROOF. The proof of Theorem 4 exhibits a bisimulation relation for a composed system. It then uses Lemma 1 to decompose the open transition of $P[Q]_{j_0}$ and obtain an open transition of $P$ on which the FH-bisimulation property can be applied to obtain an equivalent family of open transitions of $P'$; this family is then recomposed by Lemma 2 to build a set of open transitions of $P'[Q]_{j_0}$ that will simulate the original one.

Let Leaves($Q$) = $p_l^{l \in L_Q}$, Leaves($P$) = $p_l^{l \in L}$, Leaves($P'$) = $p_l'^{l \in L'}$. Consider $P$ FH-bisimilar to $P'$. It means that there is a relation $\mathcal{R}$ that is an FH-bisimulation between the open automata of the two pNets. We will consider the relation $\mathcal{R}' = \{(s, t | Pred_{s,t}) | s = s' \uplus s'' \wedge t = t' \uplus s'' \wedge s \in S_Q \wedge (s', t' | Pred_{s,t}) \in \mathcal{R}\}$ where $S_Q$ is the set of states of the open automaton of $Q$. We will prove
that $\mathcal{R}'$ is an open FH-bisimulation. Consider a pair of FH-bisimilar states: $(\langle s_{1i}^{i \in L \uplus L_Q} \rangle_{\Delta}, \langle s_{2i}^{i \in L'} \uplus s_{1i}^{i \in L_Q} \rangle_{\Delta} | \mathrm{Pred}) \in \mathcal{R}'$. Consider an open transition $\mathrm{OT}$ of $P[\mathcal{Q}]_{j_0}$.

$$ P[\mathcal{Q}]_{j_0} \models \frac{\beta_j^{j \in J}, \mathrm{Pred}_{\mathrm{OT}}, \mathrm{Post}_{\mathrm{OT}}}{\langle s_i^{i \in L \uplus L_Q} \rangle_{\Delta} \xrightarrow{\alpha} \langle s_i^{i \in L \uplus L_Q} \rangle_{\Delta}} $$

Let $J' = J \setminus \mathrm{Holes}(Q) \cup \{j_0\}$. By Lemma 1 we have:

$$ P \models \frac{\beta_j^{j \in J'}, \mathrm{Pred}', \mathrm{Post}'}{\langle s_1^{i \in L} \rangle_{\Delta} \xrightarrow{\alpha} \langle s_1^{i \in L} \rangle_{\Delta}} $$

$$ Q \models \frac{\beta_j^{j \in J \cap \mathrm{Holes}(Q)}, \mathrm{Pred}'', \mathrm{Post}''}{\langle s_i^{i \in L_Q} \rangle_{\Delta} \xrightarrow{\alpha_Q} \langle s_i^{i \in L_Q} \rangle_{\Delta}} $$

and $\mathrm{Pred}_{\mathrm{OT}} \iff \mathrm{Pred}' \wedge \mathrm{Pred}'' \wedge \alpha_Q = \beta_{j_0}$, $\mathrm{Post}_{\mathrm{OT}} = \mathrm{Post}' \uplus \mathrm{Post}''$ ($\mathrm{Post}''$ is the restriction of $\mathrm{Post}$ over $\mathrm{vars}(Q)$). As $P$ is FH-bisimilar to $P'$ and $(\langle s_i^{i \in L' \uplus L_Q} \rangle_{\Delta}, \langle s_i^{i \in L' \uplus L_Q} \rangle_{\Delta} | \mathrm{Pred}_{s,t}) \in \mathcal{R}$ there is a family $\mathrm{OT}'_x$ of open transitions of the automaton of $P'$ such that

$$ P' \models \frac{\beta_{jx}^{j \in J'}, \mathrm{Pred}_{\mathrm{OT}_x}, \mathrm{Post}_{\mathrm{OT}_x}}{\langle t_i^{i \in L'} \rangle_{\Delta} \xrightarrow{\alpha_x} \langle t_{ix}^{i \in L'} \rangle_{\Delta}} $$

and $\forall x, (\langle s_i^{i \in L' \uplus L_Q} \rangle_{\Delta}, \langle s_{ix}^{i \in L'} \rangle_{\Delta} | \mathrm{Pred}_{s_x}) \in \mathcal{R}$; and

$$ \mathrm{Pred}_{s,t} \wedge \mathrm{Pred}' \implies \bigvee_{x \in X} \left( \forall j \in J'. \beta_j = \beta_{jx} \wedge \mathrm{Pred}_{\mathrm{OT}_x} \wedge \alpha = \alpha_x \wedge \mathrm{Pred}_{s,x} \{ \mathrm{Post}' \uplus \mathrm{Post}_{\mathrm{OT}_x} \} \right) $$

We can now apply Lemma 2 on each of the $\mathrm{OT}'_x$ together with the transition of $Q$ and obtain a new family $\mathrm{OT}_x$ of open transitions (where for $i \in L_Q$, $t_i = s_i$ and $t_{ix} = s'_i$, and for $j \in \mathrm{Holes}(Q)$, $b_{jx} = b_j$):

$$ P'[Q]_{j_0} \models \frac{\beta_{jx}^{j \in J}, \mathrm{Pred}_{\mathrm{OT}_x} \wedge \mathrm{Pred}'' \wedge \alpha_Q = \beta_{j_0 x}, \mathrm{Post}_{\mathrm{OT}_x} \uplus \mathrm{Post}''}{\langle t_i^{i \in L' \uplus L_Q} \rangle_{\Delta} \xrightarrow{\alpha_x} \langle t_{ix}^{i \in L' \uplus L_Q} \rangle_{\Delta}} $$

Observe that $J = (J \setminus \mathrm{Holes}(Q) \cup \{j_0\}) \setminus \{j_0\} \cup (J \cap \mathrm{Holes}(Q))$. Now we have to verify the conditions for the FH-bisimulation between $\mathrm{OT}$ and $\mathrm{OT}_x$. $\forall x, (\langle s_i^{i \in L \uplus L_Q} \rangle_{\Delta}, \langle s_{ix}^{i \in L' \uplus L_Q} \rangle_{\Delta} | \mathrm{Pred}_{s,x}) \in \mathcal{R}'$ (by definition of $\mathcal{R}'$) and in four steps we get:

$$ \begin{align*} \mathrm{Pred}_{s,t} \wedge \mathrm{Pred}_{\mathrm{OT}} &\implies \mathrm{Pred}_{s,t} \wedge \mathrm{Pred}' \wedge \mathrm{Pred}'' \wedge \alpha_Q = \beta_{j_0} \\ &\implies \bigvee_{x \in X} \left( \forall j \in J'. \beta_j = \beta_{jx} \wedge \mathrm{Pred}_{\mathrm{OT}_x} \wedge \alpha_Q = \beta_{j_0} \wedge \alpha = \alpha_x \wedge \mathrm{Pred}_{s,x} \{ \mathrm{Post}' \uplus \mathrm{Post}_{\mathrm{OT}_x} \} \right) \wedge \mathrm{Pred}'' \end{align*} $$
$$ \implies \bigvee_{x \in X} \left( \forall j \in J'. \beta_j = \beta_{jx} \wedge (\mathrm{Pred}_{\mathrm{OT}_x} \wedge \mathrm{Pred}'' \wedge \alpha_Q = \beta_{j_0 x}) \wedge \alpha = \alpha_x \wedge \mathrm{Pred}_{s,x} \{ \mathrm{Post}' \uplus \mathrm{Post}_{\mathrm{OT}_x} \} \right) $$

The obtained formula reaches the goal except for two points:

* We need $\forall j \in J$ instead of $\forall j \in J'$ with $J' = J \setminus \mathrm{Holes}(Q) \cup \{j_0\}$ but the formula under the quantifier does not depend on $b_{j_0}$ now (thanks to the
substitution). Concerning Holes($Q$), adding prerequisite on more variables does not change the validity of the formula (those variables are not used).

* We need $Pred_{s,x}\{(Post_{OT} \uplus (Post_{OT_x} \uplus Post'')\})$, i.e., $Pred_{s,x}\{(Post' \uplus Post'') \uplus (Post_{OT_x} \uplus Post'')\})$. We can conclude by observing that $Pred_{s,x}$ does not use any variable of $Q$ and thus the substitution involving $Post''$ has no effect.

This proves the condition of the FH-simulation, the other direction is similar.

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

## Appendix B. Weak FH-bisimilarity lemmas and proofs

We define a quantified composition operator for effects, i.e. *Post* elements of the open transitions. We use $\bigcirc_{i=n}^{1} Post_i$ to denote $Post_n \odot \dots \odot Post_0$. By

convention $\bigcirc_{i=0}^{1} Post_i$ is the identity.

### Appendix B.1. Weak FH-bisimilarity is an equivalence

In this section, we first define two alternative definitions, one for weak open transition, one for weak bisimulation. We use these two alternative definitions to show that weak bisimulation is an equivalence, we will also re-use these alternative definitions in the proofs of the theorems in next sections.

**Lemma 4 (Alternative definition of weak open transitions).** Let $A = \langle J, S, s_0, V_1, T \rangle$ be an open automaton and $\langle J, S, s_0, V_2, WT \rangle$ be the weak open automaton derived from $A$. The two following statements are equivalent

1. Either $\alpha = \tau \wedge \bar{\gamma} = \emptyset \wedge Pred = True \wedge Post = Id(s) \wedge s = s'$; or there exist $\bar{\beta}_{1i}, \beta_{2i}$, and $\bar{\beta}_{3i}, Pred_{1i}, Pred_{3i}, Post_{1i},$ and $Pred_2, Post_2$, $n \ge 0, m \ge 0$ s.t.<fnref n="15" />:

$$ \forall i \in [1..n]. \frac{\bar{\beta}_{1i}, Pred_{1i}, Post_{1i}}{s_{1i} \xrightarrow{\tau} s_{1(i+1)}} \in T \wedge \frac{\bar{\beta}_{2}, Pred_{2}, Post_{2}}{s_{2} \xrightarrow{\alpha} s'_{2}} \in T \wedge $$

$$ \forall i \in [1..m]. \frac{\bar{\beta}_{3i}, Pred_{3i}, Post_{3i}}{s_{3i} \xrightarrow{\tau} s_{3(i+1)}} \in T $$

<footnote n="15">¹⁵$n=0$ (resp. $m=0$) corresponds to the case where there is no $\tau$ transition before (resp. after) the transition $\alpha$.</footnote>
In other words, we consider the sequence of $(n + m + 2)$ open transitions:

$$ (\forall i \in [1..n+1]. \begin{array}{c} \xrightarrow{\beta_{1i}, Pred_{1i}, Post_{1i}} \\ s_{1i} \xrightarrow{\tau} s_{1(i+1)} \end{array} \in \mathcal{T} \wedge \begin{array}{c} \xrightarrow{\beta_2, Pred_2, Post_2} \\ s_2 \xrightarrow{\alpha} s'_2 \end{array} \in \mathcal{T} \wedge \\ \forall i \in [1..m]. \begin{array}{c} \xrightarrow{\beta_{3i}, Pred_{3i}, Post_{3i}} \\ s_{3i} \xrightarrow{\tau} s_{3(i+1)} \end{array} \in \mathcal{T}) $$

By recurrence hypothesis we suppose that (1) ⇒ (2) holds for $n$ and $m$ (compared to the line above, we remove the first $\tau$ transition). We have:

$$ (\forall i \in [2..n+1]. \begin{array}{c} \xrightarrow{\beta_{1i}, Pred_{1i}, Post_{1i}} \\ s_{1i} \xrightarrow{\tau} s_{1(i+1)} \end{array} \in \mathcal{T} \wedge \begin{array}{c} \xrightarrow{\beta_2, Pred_2, Post_2} \\ s_2 \xrightarrow{\alpha} s'_2 \end{array} \in \mathcal{T} \wedge \\ \forall i \in [1..m]. \begin{array}{c} \xrightarrow{\beta_{3i}, Pred_{3i}, Post_{3i}} \\ s_{3i} \xrightarrow{\tau} s_{3(i+1)} \end{array} \in \mathcal{T}) \Rightarrow \begin{array}{c} \xrightarrow{\bar{\gamma}, Pred, Post} \\ s'' \xrightarrow{\alpha'} s' \end{array} \in WT $$

where

$$ s'' = s_{12} \wedge s_{1(n+2)} = s_2 \wedge s'_2 = s_{31} \wedge s_{3(m+1)} = s' $$

$$ \alpha' = \alpha \{ \bigcirc_{j=n+1}^{2} Post_{1j} \} $$

$$ \bar{\gamma} = \bigoplus_{i=2}^{n+1} (\beta_{1i} \{ \bigcirc_{j=i-1}^{2} Post_{1j} \})^{\nabla} \oplus (\beta_2 \{ \bigcirc_{j=n+1}^{2} Post_{1j} \})^{\nabla} \oplus $$

$$ \bigoplus_{i=1}^{m} (\beta_{3i} \{ \bigcirc_{j=i-1}^{1} Post_{3j} \odot Post_{2} \odot \bigcirc_{j=n}^{1} Post_{1j} \})^{\nabla} $$

$$ Pred = \bigwedge_{i=2}^{n+1} Pred_{1i} \{ \bigcirc_{j=i-1}^{2} Post_{1j} \} \wedge Pred_2 \{ \bigcirc_{j=n+1}^{2} Post_{1j} \} \wedge \\ \left( \bigwedge_{i=1}^{m} Pred_{3i} \{ \bigcirc_{j=i-1}^{1} Post_{3j} \odot Post_{2} \odot \bigcirc_{j=n+1}^{1} Post_{1j} \} \right) $$

$$ Post = \bigcirc_{j=m}^{1} Post_{3j} \odot Post_{2} \odot \bigcirc_{j=n+1}^{2} Post_{1j} $$

We need to prove that by adding the following open transition the implication remains true:

$$ \overline{\beta_{11}, Pred_{11}, Post_{11}} \xrightarrow{\tau} s_{12} $$
The right part of the disjunction, i.e.

$$ (\alpha = \tau \wedge \bar{\gamma} = \emptyset \wedge \mathrm{Pred} = \mathrm{True} \wedge \mathrm{Post} = \mathrm{Id}(s) \wedge s = s') $$

is handled trivially by rule **WT1**.

(=$\Leftarrow$) We proceed by structural induction on the rules building the weak transition (as described in the original definition). The recurrence hypothesis being that the original definition implies the characterization (1), with the conditions stated at the bottom of the theorem. We consider the different rules:

* Case rule **WT1**. We have:

$$ \frac{\emptyset, \mathrm{True}, \mathrm{Id}(s)}{s \stackrel{\tau}{\Rightarrow} s} \in \mathcal{WT} $$

We can directly conclude by the right part of the disjunction the following:

$$ \frac{\emptyset, \mathrm{True}, \mathrm{Id}(s)}{s \stackrel{\tau}{\Rightarrow} s} \in \mathcal{WT} \Rightarrow (\alpha = \tau \wedge \bar{\gamma} = \emptyset \wedge \mathrm{Pred} = \mathrm{True} \wedge \mathrm{Post} = \mathrm{Id}(s) \wedge s = s') $$

* Case rule **WT2**. We have:

$$ \frac{\bar{\gamma}, \mathrm{Pred}, \mathrm{Post}}{s \stackrel{\alpha}{\Rightarrow} s'} \in \mathcal{WT} \Rightarrow \frac{\bar{\beta}, \mathrm{Pred}, \mathrm{Post}}{s \stackrel{\alpha}{\Rightarrow} s'} \in \mathcal{T} $$

where $\bar{\gamma} = (\bar{\beta})^{\nabla}$.

These two cases above prove the implication with $n = 0$ and $m = 0$.

* Case rule **WT3**. We have:

$$ \frac{\begin{array}{c} \bar{\gamma}_1, \mathrm{Pred}_1, \mathrm{Post}_1 \\ \frac{\dots}{s \stackrel{\tau}{\Rightarrow} s'} \end{array}}{\begin{array}{c} \bar{\gamma}_2, \mathrm{Pred}_2, \mathrm{Post}_2 \\ \frac{s' \stackrel{\alpha}{\Rightarrow} s''}{s'' \stackrel{\tau}{\Rightarrow} s'''} \end{array}} \in \mathcal{WT} \quad \frac{\begin{array}{c} \bar{\gamma}_3, \mathrm{Pred}_3, \mathrm{Post}_3 \\ \frac{\dots}{s'' \stackrel{\tau}{\Rightarrow} s'''} \end{array}}{\begin{array}{c} \bar{\gamma}_1 \oplus \bar{\gamma}_2 \{\mathrm{Post}_1\} \oplus \bar{\gamma}_3 \{\mathrm{Post}_2 \odot \mathrm{Post}_1\} \\ \alpha' = \alpha \{\mathrm{Post}_1\} \end{array}} \in \mathcal{WT} \\ \frac{\bar{\gamma}, \mathrm{Pred}, \mathrm{Post}_3 \odot \mathrm{Post}_2 \odot \mathrm{Post}_1}{s \stackrel{\alpha'}{\Rightarrow} s'''} \in \mathcal{WT} $$

1. By induction hypothesis this means each tau weak open transition can be written as a series of $n_1$ tau open transitions such $n_1 = n+m+1$, hence by simplification we have (strictly speaking, by induction we
might also have the case $\alpha = \tau \wedge \bar{\gamma} = \emptyset \wedge \dots$ but in this case, rule **WT1** allows us to obtain a similar reduction with $n_1 = 1$):

$$ \frac{\bar{\gamma}_1, Pred_1, Post_1}{s \stackrel{\tau}{\Rightarrow} s'} \in \mathcal{W}\mathcal{T} \Rightarrow \forall i \in [1..n_1]. \frac{\bar{\beta}_{1i}, Pred_{1i}, Post_{1i}}{s_{1i} \stackrel{\tau}{\rightarrow} s_{1(i+1)}} \in \mathcal{T} $$

where

$$ \begin{gathered} s = s_{11} \wedge s_{1(n_1+1)} = s', \quad \bar{\gamma}_1 = \bigoplus_{i=1}^{n_1} (\bar{\beta}_{1i} \{ \bigcirc_{j=i-1}^{1} Post_{1j} \})^{\nabla} \\ Pred_1 = \bigwedge_{i=1}^{n_1} (Pred_{1i} \{ \bigcirc_{j=i-1}^{1} Post_{1j} \}), \quad Post_1 = \bigcirc_{i=n_1}^{1} \{ Post_{1i} \} \end{gathered} $$

2. Similarly, a series of $m_1$ open transitions such that $m_1 = n + m + 1$ can be simplified as follows:

$$ \frac{\bar{\gamma}_3, Pred_3, Post_3}{s'' \stackrel{\tau}{\Rightarrow} s'''} \in \mathcal{W}\mathcal{T} \Rightarrow \forall i \in [1..m_1]. \frac{\bar{\beta}_{3i}, Pred_{3i}, Post_{3i}}{s_{3i} \stackrel{\tau}{\rightarrow} s_{3(i+1)}} \in \mathcal{T} $$

where

$$ \begin{gathered} s'' = s_{31} \wedge s_{3(m_1+1)} = s''' \wedge \\ \bar{\gamma}_3 = \bigoplus_{i=1}^{m_1} (\bar{\beta}_{3i} \{ \bigcirc_{j=i-1}^{1} Post_{3j} \})^{\nabla} \wedge \\ Pred_3 = \bigwedge_{i=1}^{m_1} (Pred_{3i} \{ \bigcirc_{j=i-1}^{1} Post_{3j} \}) \wedge Post_3 = \bigcirc_{i=m_1}^{1} \{ Post_{3i} \} \end{gathered} $$

3. Concerning the middle reduction, by induction hypothesis there exists a set of open transitions in $\mathcal{T}$ such that:

$$ \begin{gathered} \frac{\bar{\gamma}_2, Pred_2, Post_2}{s' \stackrel{\alpha'}{\Rightarrow} s''} \in \mathcal{W}\mathcal{T} \Rightarrow \left( \forall i \in [1..n_2]. \frac{\bar{\beta}_{2i}, Pred_{2i}, Post_{2i}}{s_{2i} \stackrel{\tau}{\rightarrow} s_{2(i+1)}} \in \mathcal{T} \wedge \right. \\ \left. \frac{\bar{\beta}', Pred', Post'}{s_2 \stackrel{\alpha''}{\Rightarrow} s'_2} \in \mathcal{T} \wedge \forall i \in [1..m_2]. \frac{\bar{\beta}'_{2i}, Pred'_{2i}, Post'_{2i}}{s'_{2i} \stackrel{\tau}{\rightarrow} s'_{2(i+1)}} \in \mathcal{T} \right) \end{gathered} $$
where

$$s' = s_{21} \wedge s_{2(n_2+1)} = s_2 \wedge s'_2 = s'_{21} \wedge s'_{2(m_2+1)} = s''$$

$$\alpha'' = \alpha' \{ \bigcirc_{j=n_2}^{1} \mathrm{Post}_{2j} \}$$

$$\overline{\gamma_2} = \bigoplus_{i=1}^{n_2} (\overline{\beta_{2i}} \{ \bigcirc_{j=i-1}^{1} \mathrm{Post}_{2j} \})^{\nabla} \oplus (\overline{\beta'_{2i}} \{ \bigcirc_{j=n_2}^{1} \mathrm{Post}_{2j} \})^{\nabla} \oplus$$

$$\bigoplus_{i=1}^{m_2} (\overline{\beta'_{2i}} \{ \bigcirc_{j=i-1}^{1} \mathrm{Post}'_{2j} \odot \mathrm{Post}' \odot \bigcirc_{j=n_2}^{1} \mathrm{Post}_{2j} \})^{\nabla}$$

$$\mathrm{Pred}_2 = \bigwedge_{i=1}^{n_2} \mathrm{Pred}_{2i} \{ \bigcirc_{j=i-1}^{1} \mathrm{Post}_{2j} \} \wedge \mathrm{Pred}' \{ \bigcirc_{j=n_2}^{1} \mathrm{Post}_{2j} \} \wedge$$

$$( \bigwedge_{i=1}^{m_2} \mathrm{Pred}'_{2i} \{ \bigcirc_{j=i-1}^{1} \mathrm{Post}'_{2j} \odot \mathrm{Post}' \odot \bigcirc_{j=n_2}^{1} \mathrm{Post}_{2j} \} )$$

$$\mathrm{Post}_2 = \bigcirc_{j=m_2}^{1} \mathrm{Post}'_{2j} \odot \mathrm{Post}' \odot \bigcirc_{j=n_2}^{1} \mathrm{Post}_{2j}$$

Therefore, we can deduce that we have:

$$\overline{\gamma}, \mathrm{Pred}, \mathrm{Post} \underset{s \stackrel{\alpha}{\Rightarrow} s'}{\in} \mathcal{W}\mathcal{T} \Rightarrow \left( \forall i \in [1..(n_1+n_2)]. \overline{\beta_{4i}, \mathrm{Pred}_{4i}, \mathrm{Post}_{4i}} \underset{s_{4i} \stackrel{\tau}{\rightarrow} s_{4(i+1)}}{\in} \mathcal{T} \wedge \right.$$

$$\overline{\beta'}, \mathrm{Pred}', \mathrm{Post}' \underset{s_2 \stackrel{\alpha''}{\rightarrow} s'_2}{\in} \mathcal{T} \wedge \forall i \in [1..(m_1+m_2)]. \overline{\beta_{5i}, \mathrm{Pred}_{5i}, \mathrm{Post}_{5i}} \underset{s_{5i} \stackrel{\tau}{\rightarrow} s_{5(i+1)}}{\in} \mathcal{T})$$

such that

$$s_{4i} = \begin{cases} s_{1i} & \text{if } i \le n_1 \\ s_{2i-n_1} & \text{if } i > n_1 \end{cases}$$

$$s_{5i} = \begin{cases} s_{3i} & \text{if } i \le m_1 \\ s'_{2i-m_1} & \text{if } i > m_1 \end{cases}$$

and similarly for $\mathrm{Pred}_{4i}$, $\mathrm{Pred}_{5i}$, $\mathrm{Post}_{4i}$, and $\mathrm{Post}_{5i}$.
Also, we have the following assertions:

$$
\begin{align*}
s = s_{41} \wedge s_{4(n_1+n_2+1)} &= s_2 \wedge s'_2 = s_{51} \wedge s_{5(m_1+m_2+1)} = s' \\
\alpha'' &= \alpha \{ \bigcirc_{j=n_1+n_2}^{1} \mathrm{Post}_{4j} \} \\
\bar{\gamma} &= \bigoplus_{i=1}^{n_1+n_2} (\bar{\beta}_{4i} \{ \bigcirc_{j=i-1}^{1} \mathrm{Post}_{4j} \})^{\nabla} \oplus (\bar{\beta}' \{ \bigcirc_{j=n_1+n_2}^{1} \mathrm{Post}_{4j} \})^{\nabla} \oplus \\
&\qquad \bigoplus_{i=1}^{m_1+m_2} (\bar{\beta}_{5i} \{ \bigcirc_{j=i-1}^{1} \mathrm{Post}'_{5i} \odot \mathrm{Post}' \odot \bigcirc_{j=n_1+n_2}^{1} \mathrm{Post}_{4i} \})^{\nabla} \\
\mathrm{Pred} &= \bigwedge_{i=1}^{n_1+n_2} \mathrm{Pred}_{4i} \{ \bigcirc_{j=i-1}^{1} \mathrm{Post}_{4j} \} \wedge \mathrm{Pred}' \{ \bigcirc_{j=n_1+n_2}^{1} \mathrm{Post}_{4j} \} \wedge \\
&\qquad \bigwedge_{i=1}^{m_1+m_2} \mathrm{Pred}_{5i} \{ \bigcirc_{j=i-1}^{1} \mathrm{Post}_{5j} \odot \mathrm{Post}' \odot \bigcirc_{j=n_1+n_2}^{1} \mathrm{Post}_{4j} \} \\
\mathrm{Post} &= \bigcirc_{j=m_1+m_2}^{1} \mathrm{Post}_{5j} \odot \mathrm{Post}' \odot \bigcirc_{j=n_1+n_2}^{1} \mathrm{Post}_{4j}
\end{align*}
$$

This concludes the inductive step, showing that the decomposition expressed by the $\Leftarrow$ direction of the lemma is always possible with the right side conditions. $\square$

**Lemma 5 (Alternative definition of weak bisimulation).** The definition of weak bisimulation given in Definition 14 is equivalent to the following one:

Let $A_1 = \langle J, S_1, s_0, V_1, T_1 \rangle$ and $A_2 = \langle J, S_2, t_0, V_2, T_2 \rangle$ be open automata; $\langle J, S_1, s_0, V_1, WT_1 \rangle$ and $\langle J, S_2, t_0, V_2, WT_2 \rangle$ be the weak open automaton derived from $A_1$ and $A_2$ respectively. For any states $s \in S_1$ and $t \in S_2$ such that $(s, t|\mathrm{Pred}_{s,t}) \in \mathcal{R}$, we have:

* For any open transition WOT in $WT_1$:

$$ \frac{\gamma_j^{j \in J'}, \mathrm{Pred}_{\mathrm{OT}}, \mathrm{Post}_{\mathrm{OT}}}{s \stackrel{\alpha}{\Rightarrow} s'} $$

there exists an indexed set of weak open transitions $WOT_x^{x \in X} \subseteq WT_2$:

$$ \frac{\gamma_{1x}^{j \in J_x}, \mathrm{Pred}_{\mathrm{OT}_x}, \mathrm{Post}_{\mathrm{OT}_x}}{t \stackrel{\alpha_x}{\Rightarrow} t_x} $$

such that $\forall x, J' = J_x, (s', t_x|\mathrm{Pred}_{s',x}) \in \mathcal{R}$; and

$$ \mathrm{Pred}_{s,t} \wedge \mathrm{Pred}_{\mathrm{OT}} \implies \bigvee_{x \in X} (\forall j \in J_x. \gamma_j = \gamma_{jx} \wedge \mathrm{Pred}_{\mathrm{OT}_x} \wedge \alpha = \alpha_x \wedge \mathrm{Pred}_{s',x} \{ \mathrm{Post}_{\mathrm{OT}} \uplus \mathrm{Post}_{\mathrm{OT}_x} \}) $$
• and symmetrically any open transition from WOT in WT₂ can be covered by a set of weak transitions from s in WT₁.

PROOF. Note that Definition 14 is a particular case of the definition above, thus we only need to prove one direction of the equivalence between the two definitions, namely:

(⇒) We prove that Definition 14 implies the definition above. In other words, suppose that $Pred_{s,t} \in \mathcal{R}$ and suppose that the following statement holds:

$$ \frac{\gamma_j^{j \in J'}, Pred_{OT}, Post_{OT}}{s \stackrel{\alpha}{\Rightarrow} s'} \in WT_1 $$

Moreover, by using Lemma 4 we know that:

$$ \frac{\gamma_j^{j \in J'}, Pred_{OT}, Post_{OT}}{s \stackrel{\alpha}{\Rightarrow} s'} \in WT_1 \Rightarrow \left( \begin{array}{l} \forall i \in [1..n] \frac{\beta_{1ij}^{j \in J_1'}, Pred_{1i}, Post_{1i}}{s_{1i} \xrightarrow{\tau} s_{1(i+1)}} \in T_1 \wedge \\ \beta_{2j}^{j \in J_2'}, Pred_2, Post_2 \\ \frac{\alpha'}{s_{20} \xrightarrow{\alpha'} s_{21}} \in T_1 \wedge \\ \forall i \in [1..m] \frac{\beta_{3ij}^{j \in J_3'}, Pred_{3i}, Post_{3i}}{s_{3i} \xrightarrow{\tau} s_{3(i+1)}} \in T_1 \end{array} \right) $$

where

$$ s = s_{11} \wedge s_{1(n+1)} = s_{20} \wedge s_{21} = s_{31} \wedge s_{3(m+1)} = s' $$

$$ \alpha = \alpha' \{ \bigcirc_{j=n}^{1} Post_{1j} \} $$

$$ \gamma_j^{j \in J'} = \bigoplus_{i=1}^{n} \overline{(\beta_{1i} \{ \bigcirc_{j=i-1}^{1} Post_{1j} \})}^{\nabla} \oplus \overline{(\beta_2 \{ \bigcirc_{j=n}^{1} Post_{1j} \})}^{\nabla} \oplus $$

$$ \bigoplus_{i=1}^{m} \overline{(\beta_{3i} \{ \bigcirc_{j=i-1}^{1} Post_{3j} \odot Post_{2} \bigcirc \bigcirc_{j=n}^{1} Post_{1j} \})}^{\nabla} $$

$$ Pred_{OT} = \bigwedge_{i=1}^{n} Pred_{1i} \{ \bigcirc_{j=i-1}^{1} Post_{1j} \} \wedge Pred_{2} \{ \bigcirc_{j=n}^{1} Post_{1j} \} \wedge $$

$$ \left( \bigwedge_{i=1}^{m} Pred_{3i} \{ \bigcirc_{j=i-1}^{1} Post_{3j} \odot Post_{2} \bigcirc \bigcirc_{j=n}^{1} Post_{1j} \} \right) $$

$$ Post_{OT} = \bigcirc_{j=m}^{1} Post_{3j} \odot Post_{2} \bigcirc \bigcirc_{j=n}^{1} Post_{1j} $$
For the sake of simplicity, we prove the rule in the restricted case where $n$ and $m$ are equal to 1, hence a single tau open transition will be considered on each side of the potentially visible one. The proof may be easily generalized to the multiple tau open transitions by using the same reasoning and **WT3** rule. Consider each open transition separately:

1. For the first open transition in $\mathcal{T}_1$:

$$ \frac{\beta_{1j}^{j \in J_1'} \text{, Pred}_1 \text{, Post}_1}{s_{11} \xrightarrow{\tau} s_{12}} $$

by hypothesis we have $(s, t | Pred_{s,t}) \in \mathcal{R}$ and $s = s_{11}$. Thus, by Definition 14 we can deduce there exists an indexed set of weak open transitions $WOT_a^{a \in A} \subseteq W\mathcal{T}_2$:

$$ \frac{\gamma_{ja}^{j \in J_a} \text{, Pred}_{OT_a} \text{, Post}_{OT_a}}{t \xrightarrow{\alpha_{1a}} u_a} $$

such that $\forall a, J_a = \{j \in J_1' | \beta_{1j} \neq \tau\}, (s_{12}, u_a | Pred_{s_{11},a}) \in \mathcal{R}$ and $Pred_{s,t} \wedge Pred_1 \Rightarrow \bigvee_{a \in A} (\forall j \in J_a.(\beta_{1j})^{\nabla} = \gamma_{ja} \wedge Pred_{OT_a} \wedge \alpha_{1a} = \tau \wedge Pred_{s_{11},a}\{Post_1 \uplus Post_{OT_a}\})$

Note that, because $\mathbb{E} \cap \mathbb{A} = \emptyset$ (actions and expressions are disjoint) and $\alpha_{1a} = \tau$ we have directly ($\alpha_{1a}$ cannot be a variable, and cannot contain expressions/variables because $\tau$ has no parameter):

$$ \frac{\gamma_{ja}^{j \in J_a} \text{, Pred}_{OT_a} \text{, Post}_{OT_a}}{t \xrightarrow{\tau} u_a} $$

2. Concerning the middle open transition in $\mathcal{T}_1$:

$$ \frac{\beta_{2j}^{j \in J_2'} \text{, Pred}_2 \text{, Post}_2}{s_{20} \xrightarrow{\alpha'} s_{21}} $$

we have $(s_{11}, u_a | Pred_{s_{11},a}) \in \mathcal{R}$ and $s_{11} = s_{20}$. Again by Definition 14 we can deduce there exists an indexed set of weak open transitions $WOT_b^{b \in B} \subseteq W\mathcal{T}_2$:

$$ \frac{\gamma_{jb}^{j \in J_b} \text{, Pred}_{OT_b} \text{, Post}_{OT_b}}{u_a \underset{v_b}{\overset{\alpha_{2b}}{\rightleftharpoons}}} $$

such that $\forall b, J_b = \{j \in J_2' | \beta_{2j} \neq \tau\}, (s_{21}, v_b | Pred_{s_{21},b}) \in \mathcal{R}$; $Pred_{s_{11},a} \wedge Pred_2 \Rightarrow \bigvee_{b \in B} (\forall j \in J_b.(\beta_{2j})^{\nabla} = \gamma_{jb} \wedge Pred_{OT_b} \wedge \alpha' = \alpha_{2b} \wedge Pred_{s_{21},b}\{Post_2 \uplus Post_{OT_b}\})$
plication, we get:

$$ \begin{array}{l} \mathrm{Pred}_{s,t} \wedge \mathrm{Pred}_1) \wedge \mathrm{Pred}_2\{\{\mathrm{Post}_1\}\} \implies \\ \quad \bigvee_{a \in A} (\forall j \in J_a.(\beta_{1j})^\nabla = \gamma_{ja} \wedge \mathrm{Pred}_{OT_a} \wedge \\ \qquad \mathrm{Pred}_{s_{11},a}\{\{\mathrm{Post}_1 \uplus \mathrm{Post}_{OT_a}\}\} \wedge \mathrm{Pred}_2\{\{\mathrm{Post}_1 \uplus \mathrm{Post}_{OT_a}\}\}) \end{array} $$

Note that on the right side of the implication we added the substitution of $Post_{OT_x}$ without affecting the validity of the statement, because the domain of the substitution function $Post_{OT_x}$ is disjoint from the others. Hence a little rewriting gives:

$$ \begin{array}{l} \mathrm{Pred}_{s,t} \wedge \mathrm{Pred}_1) \wedge \mathrm{Pred}_2\{\{\mathrm{Post}_1\}\} \implies \\ \quad \bigvee_{a \in A} (\forall j \in J_a.(\beta_{1j})^\nabla = \gamma_{ja} \wedge \mathrm{Pred}_{OT_a} \wedge (\mathrm{Pred}_{s_{11},a} \wedge \mathrm{Pred}_2\{\{\mathrm{Post}_1 \uplus \mathrm{Post}_{OT_a}\}\})) \end{array} $$

By replacing the inner predicate ($\mathrm{Pred}_{s_{11},u_a} \wedge \mathrm{Pred}_2$) by the conclusion of the statement given in case 2, the formula becomes:

$$ \begin{array}{l} \mathrm{Pred}_{s,t} \wedge \mathrm{Pred}_1) \wedge \mathrm{Pred}_2\{\{\mathrm{Post}_1\}\} \implies \\ \quad \bigvee_{a \in A} (\forall j \in J_a.(\beta_{1j})^\nabla = \gamma_{ja} \wedge \mathrm{Pred}_{OT_a} \wedge (\bigvee_{b \in B} (\forall j \in J_b.(\beta_{2j})^\nabla = \gamma_{jb} \wedge \mathrm{Pred}_{OT_b} \wedge \alpha' = \alpha_{2b} \wedge \\ \qquad \mathrm{Pred}_{s_{21},b}\{\{\mathrm{Post}_2 \uplus \mathrm{Post}_{OT_b}\}\})\{\{\mathrm{Post}_1 \uplus \mathrm{Post}_{OT_a}\}\})) \end{array} $$

This can be rewritten into:

$$ \begin{array}{l} \mathrm{Pred}_{s,t} \wedge \mathrm{Pred}_1) \wedge \mathrm{Pred}_2\{\{\mathrm{Post}_1\}\} \implies \\ \quad \bigvee_{a \in A} \bigvee_{b \in B} (\forall j \in J_a.(\beta_{1j})^\nabla = \gamma_{ja} \wedge \forall j \in J_b.(\beta_{2j})^\nabla = \gamma_{jb} \wedge \{\{\mathrm{Post}_1 \uplus \mathrm{Post}_{OT_a}\}\} \wedge \mathrm{Pred}_{OT_a} \wedge \\ \qquad \mathrm{Pred}_{OT_b}\{\{\mathrm{Post}_1 \uplus \mathrm{Post}_{OT_a}\}\} \wedge (\alpha' = \alpha_{2b}) \wedge \{\{\mathrm{Post}_1 \uplus \mathrm{Post}_{OT_a}\}\} \wedge \\ \qquad \mathrm{Pred}_{s_{21},b}\{\{\mathrm{Post}_2 \odot \mathrm{Post}_1 \uplus \mathrm{Post}_{OT_b} \odot \mathrm{Post}_{OT_a}\}\}) \end{array} $$

Since $Post_1$ does not act on $\gamma_{jb}$, nor on $\mathrm{Pred}_{OT_b}$ and $\alpha_2$. As well $Post_{OT_a}$ does not act on $\alpha'$, nor on $\beta_{2j}$ the formula can be simplified as follows:

$$ \begin{array}{l} \mathrm{Pred}_{s,t} \wedge \mathrm{Pred}_1) \wedge \mathrm{Pred}_2\{\{\mathrm{Post}_1\}\} \implies \\ \quad \bigvee_{a \in A} \bigvee_{b \in B} (\forall j \in J_a.(\beta_{1j})^\nabla = \gamma_{ja} \wedge \forall j \in J_b.(\beta_{2j})^\nabla \{\{\mathrm{Post}_1\}\} = \gamma_{jb} \{\{\mathrm{Post}_{OT_a}\}\} \wedge \mathrm{Pred}_{OT_a} \wedge \\ \qquad \mathrm{Pred}_{OT_b}\{\{\mathrm{Post}_{OT_a}\}\} \wedge \alpha' \{\{\mathrm{Post}_1\}\} = \alpha_{2b} \{\{\mathrm{Post}_{OT_a}\}\} \wedge \\ \qquad \mathrm{Pred}_{s_{21},b}\{\{\mathrm{Post}_2 \odot \mathrm{Post}_1 \uplus \mathrm{Post}_{OT_b} \odot \mathrm{Post}_{OT_a}\}\}) \end{array} $$
Finally, the conjunction with the term $Pred_3\{\{Post_2 \odot Post_1\}\}$ of the both sides of the implication and rewriting, we get:

$$
\begin{align*}
Pred_{s,t} \wedge Pred_1) \wedge Pred_2\{\{Post_1\}\} \wedge Pred_3\{\{Post_2 \odot Post_1\}\} &\implies \\
\bigvee_{a \in A} \bigvee_{b \in B} (\forall j \in J_a.(\beta_j^1)^\nabla = \gamma_{ja} \wedge \forall j \in J_b.(\beta_{2j})^\nabla \{\{Post_1\}\} = \gamma_{jb}\{\{Post_{OT_a}\}\} \wedge Pred_{OT_a} \wedge \\
& Pred_{OT_b}\{\{Post_{OT_a}\}\} \wedge \alpha'\{\{Post_1\}\} = \alpha_{2b}\{\{Post_{OT_a}\}\} \wedge (Pred_{s_{21},v_b} \wedge Pred_3) \\
& \qquad \{\{Post_2 \odot Post_1 \uplus Post_{OT_b} \odot Post_{OT_a}\}\})
\end{align*}
$$

Again note that because of the domain of the substitution function is indepen-
dent from some predicates and expressions, we removed $Post_1$ and we added the
term $Post_{OT_b} \odot Post_{OT_a}$ in the substitution of the right side of the implication.
Finally, by replacing the predicate ($Pred_{s_{21},b} \wedge Pred_3$) by the conclusion of the
implication given in case 3, we get:

$$
\begin{align*}
Pred_{s,t} \wedge \underbrace{Pred_1 \wedge Pred_2\{\{Post_1\}\} \wedge Pred_3\{\{Post_2 \odot Post_1\}\}}_{Pred_{OT}} &\implies \\
\bigvee_{a \in A} \bigvee_{b \in B} \bigvee_{c \in C} (\forall j \in J_a.(\beta_{1j})^\nabla = \gamma_{ja} \wedge \forall j \in J_b.(\beta_{2j}\{\{Post_{OT_a}\}\})^\nabla = \gamma_{jb}\{\{Post_{OT_a}\}\} \wedge \\
& \qquad \forall j \in J_c.(\beta_{3j}\{\{Post_2 \odot Post_1\}\})^\nabla = \gamma_{jc}\{\{Post_{OT_b} \odot Post_{OT_a}\}\} \wedge \\
& \qquad \underbrace{Pred_{OT_a} \wedge Pred_{OT_b}\{\{Post_{OT_a}\}\} \wedge Pred_{OT_c}\{\{Post_{OT_b} \odot Post_{OT_a}\}\}}_{Pred} \wedge \\
& \qquad \underbrace{\alpha'\{\{Post_1\}\}}_{\alpha} = \underbrace{\alpha_{2b}\{\{Post_{OT_a}\}\}}_{\alpha''} \\
& \wedge Pred_{s_{31},c}\{\underbrace{Post_3 \odot Post_2 \odot Post_1}_{Post_{OT}} \uplus \underbrace{Post_{OT_c} \odot Post_{OT_b} \odot Post_{OT_a}}_{Post}\})
\end{align*}
$$

The three for all statements (on $J_a$, $J_b$ and $J_c$) can be concatenated using $\oplus$, the
list union lifted to indexed sets (if $\gamma = \gamma'$ and $\gamma'' = \gamma'''$ then $\gamma \oplus \gamma'' = \gamma' \oplus \gamma''$).

$$
\forall j \in J_a \uplus J_b \uplus J_c. (\beta_{1j})^{\nabla} \oplus (\beta_{2j} \{\{Post_{OT_a}\}\})^{\nabla} \oplus (\beta_{3j} \{\{Post_2 \odot Post_1\}\})^{\nabla} = \\
\gamma_{ja} \oplus \gamma_{jb} \{\{Post_{OT_a}\}\} \oplus \gamma_{jc} \{\{Post_{OT_b} \odot Post_{OT_a}\}\}
$$

We have $s_{31} = s'$, so can rewrite the formula:

$$
Pred_{s,t} \wedge Pred_{OT} \implies \bigvee_{a \in A} \bigvee_{b \in B} \bigvee_{c \in C} (\forall j \in J. \gamma'_j = \gamma_j \wedge Pred \wedge \alpha = \alpha'' \wedge Pred_{s',c}\{\{Post_{OT} \uplus Post\}\})
$$

All the combinations of elements in A, B, and C provide a set X of weak
open transitions (each combination of one transition in A, one in B, and one in
C provides one weak open transition in the set X, i.e. each x ∈ X corresponds
to a triple $(a, b, c) \in A \times B \times C$); this defines a set of weak open transitions indexed over $X$; each such open transition leads to a $w_c$ that we call $t_x$. This re-indexing allows us to conclude:

$$Pred_{s,t} \wedge Pred_{OT} \implies \bigvee_{x \in X} \left( \forall j \in J. \gamma'_j = \gamma_j \wedge Pred \wedge \alpha = \alpha'' \wedge Pred_{s',x} \{ \{Post_{OT} \uplus Post \} \} \right)$$

**Theorem 6.** *Weak FH-bisimilarity is an equivalence.* Suppose $\mathcal{R}$ is a weak FH-bisimulation. Then $\mathcal{R}$ is an equivalence, that is, $\mathcal{R}$ is reflexive, symmetric and transitive.

With the above lemma, we can use the same technique as for Theorem 1 to prove that a weak FH-bisimilarity is an equivalence. Indeed, we essentially use the same proof-scheme the main difference concerns $\beta$ and $\gamma$. Indeed, while the schema of the proof of transitivity was not directly applicable on the definition of weak bisimulation, Lemma 5 provides a characterization of weak bisimulation similar to the definition of strong bisimulation, and thus the same proof scheme is directly applicable.

## Appendix B.2. Composition properties

This section gives decomposition/composition lemmas and their proofs, these are the equivalent of the composition lemmas for open transitions, but applied to weak open automata.

**Lemma 6 (Weak open transition decomposition).** Let $\text{Leaves}(Q) = p\text{LTS}_l^{l \in L_Q}$; suppose$^{16}$:

$$P[Q]_{j_0} \models \begin{array}{c} \gamma_j^{j \in J}, \text{Pred}, \text{Post} \\ \vdots \\ \llcorner s_i^{i \in L} \triangleright \alpha \Rightarrow \llcorner s'_i^{i \in L} \triangleright \end{array}$$

with $J \cap \text{Holes}(Q) \neq \emptyset$ or $\exists i \in L_Q. s_i \neq s'_i$, i.e. $Q$ takes part in the reduction. Then there exist $n, \text{Pred}', \text{Post}',$ and for all $p \in [1..n]$ there exist $\beta_p, \alpha_p, \text{Pred}_p, \text{Post}_p$ and a family $\gamma_{pj}^{j \in J_p}$ and for all $p \in [1..n+1]$ $s_{pi}^{i \in L_Q}$. s.t.:

<footnote>$^{16}$Note that the hypotheses of the lemma imply that $Q$ is not a pLTS but a similar lemma can be proven for a pLTS $Q$.</footnote>
$$ P \models \frac{\gamma_j^{j \in (J_p \setminus \text{Holes}(Q)) \cup \{j_0\}}, \text{Pred}^{\prime}, \text{Post}^{\prime}}{\triangleleft s_i^{i \in L \setminus L_Q} \triangleright \stackrel{\alpha}{\Rightarrow} \triangleleft s_i^{i' \in L \setminus L_Q} \triangleright} \quad \text{and} \quad \gamma_{j_0} = [\beta_0, \dots, \beta_n] $$

$$ \text{and for all } p \in [1..n] \quad Q \models \frac{\gamma_{pj}^{j \in J_p}, \text{Pred}_p, \text{Post}_p}{\triangleleft s_{pi}^{i \in L_Q} \triangleright \stackrel{\alpha_p}{\Rightarrow} \triangleleft s_{(p+1)i}^{i \in L_Q} \triangleright} $$

$$ \text{such that} \quad \bigcup_{p=1}^{n} J_p = J \cap \text{Holes}(Q), \quad \gamma_j^{j \in J \cap \text{Holes}(Q)} = \bigoplus_{p=1}^{n} (\gamma_{pj}^{j \in J_p}) \{ \bigcirc_{i=p-1}^{1} \text{Post}_i \}, $$

$$ \text{Pred} \iff \text{Pred}' \wedge \bigwedge_{p=1}^{n} (\alpha_p \{ \bigcirc_{i=p-1}^{1} \text{Post}_i \}) = \beta_p \wedge \text{Pred}_p \{ \bigcirc_{i=p-1}^{1} \text{Post}_i \}), $$

$$ \text{Post} = \text{Post}' \circled{\bigcirc}_{p=n}^{1} \text{Post}_p, \text{ and } \forall i \in L_Q. s_{(n+1)i} = s_i' \wedge s_{1i} = s_i $$

where for any $p$, $\text{Post}_p$ only acts upon variables $\text{vars}(Q)$.

PROOF. Suppose that we have:

$$ P[Q]_{j_0} \models \frac{\gamma_j^{j \in J}, \text{Pred}, \text{Post}}{\triangleleft s_l^{l \in L} \triangleright \stackrel{\alpha}{\Rightarrow} \triangleleft s_l^{l' \in L} \triangleright} $$

By Lemma 4 this implies the following:

$$ \forall p \in [1..m_1] P[Q]_{j_0} \models \frac{\overline{\beta_{1p}}, \text{Pred}_{1p}, \text{Post}_{1p}}{\triangleleft s_{pl}^{l \in L} \triangleright \stackrel{\tau}{\rightarrow} \triangleleft s_{(p+1)l}^{l \in L} \triangleright}, \quad P[Q]_{j_0} \models \frac{\overline{\beta_2}, \text{Pred}_2, \text{Post}_2}{\triangleleft t_l^{l \in L} \triangleright \stackrel{\alpha'}{\rightarrow} \triangleleft t_l^{l' \in L} \triangleright} $$

$$ \text{and } \forall p \in [1..m_2] P[Q]_{j_0} \models \frac{\overline{\beta_{3p}}, \text{Pred}_{3p}, \text{Post}_{3p}}{\triangleleft u_{pl}^{l \in L} \triangleright \stackrel{\tau}{\rightarrow} \triangleleft u_{(p+1)l}^{l \in L} \triangleright} $$

where
$$ \forall l \in L. s_l = s_{1l} \wedge s_{(m_1+1)l} = t_l \wedge t'_l = u_{1l} \wedge u_{(m_2+1)l} = s'_l $$

$$ \alpha = \alpha' \{ \bigcirc_{j=m_1}^{1} \text{Post}_{1j} \} $$

$$ \gamma_j^{j \in J} = \bigoplus_{i=1}^{m_1} (\overline{\beta_{1i}} \{ \bigcirc_j^1 \text{Post}_{1j} \})^\nabla \oplus $$

$$ (\overline{\beta_2} \{ \bigcirc_j^1 \text{Post}_{1j} \})^\nabla \oplus \bigoplus_{i=1}^{m_2} (\overline{\beta_{3i}} \{ \bigcirc_j^1 \text{Post}_{3j} \odot \text{Post}_{2j} \bigcirc^1 \text{Post}_{1j} \})^\nabla $$

$$ \text{Pred} = \bigwedge_{i=1}^{m_1} \text{Pred}_{1i} \{ \bigcirc_j^1 \text{Post}_{1j} \} \wedge \text{Pred}_2 \{ \bigcirc_j^1 \text{Post}_{1j} \} \wedge $$

$$ \bigwedge_{i=1}^{m_2} \text{Pred}_{3i} \{ \bigcirc_j^1 \text{Post}_{3j} \odot \text{Post}_{2j} \bigcirc^1 \text{Post}_{1j} \} $$

$$ \text{Post} = \bigcirc_{j=m_2}^{1} \text{Post}_{3j} \odot \text{Post}_{2j} \bigcirc \bigcirc_{j=m_1}^{1} \text{Post}_{1j} $$

We can apply Lemma 1 on each *OT*:

1. For each open transition $OT_p$ in the form $(\overline{\beta}_{1p} = \beta_{1pj}^{j \in J_{1p}})$:

$$ P[Q]_{j_0} \models \begin{array}{@{}c@{\quad}c@{}} \beta_{1pj}^{j \in J_{1p}} & \text{Pred}_{1p}, \text{Post}_{1p} \\ \multicolumn{2}{@{}c@{}}{\Delta s_{pl}^{l \in L} \triangleright \xrightarrow{\tau} \Delta s_{(p+1)l}^{l \in L} \triangleright} \end{array} $$

If $Q$ moves then we obtain by Lemma 1:

$$ P \models \begin{array}{@{}c@{\quad}c@{}} (\beta_{1pj})^{j \in (J_{1p} \setminus \text{Holes}(Q)) \cup \{j_0\}}, & \text{Pred}'_{1p}, \text{Post}'_{1p} \\ \multicolumn{2}{@{}c@{}}{\Delta s_{pl}^{l \in L \setminus L_Q} \triangleright \xrightarrow{\tau} \Delta (s_{(p+1)l})^{l \in L \setminus L_Q} \triangleright} \end{array} \quad \text{and} $$

$$ Q \models \begin{array}{@{}c@{\quad}c@{}} (\beta_{1pj})^{j \in J_{1p} \cap \text{Holes}(Q)}, & \text{Pred}''_{1p}, \text{Post}''_{1p} \\ \multicolumn{2}{@{}c@{}}{\Delta s_{pl}^{l \in L_Q} \triangleright \xrightarrow{\alpha_{1p}} \Delta s_{(p+1)l}^{l \in L_Q} \triangleright} \end{array} $$

such that

$\text{Pred}_{1p} \iff \text{Pred}'_{1p} \wedge \text{Pred}''_{1p} \wedge \alpha_{1p} = \beta_{1pj_0}, \text{Post}_{1p} = \text{Post}'_{1p} \uplus \text{Post}''_{1p}$ where $\text{Post}''_{1p}$ is the restriction of $\text{Post}_{1p}$ over $\text{vars}(Q)$.

Else $Q$ does not move and we have:

$$ P \models \begin{array}{@{}c@{\quad}c@{}} (\beta_{1pj})^{j \in (J_{1p} \setminus \text{Holes}(Q))}, & \text{Pred}'_{1p}, \text{Post}'_{1p} \\ \multicolumn{2}{@{}c@{}}{\Delta (s_{pl})^{l \in L \setminus L_Q} \triangleright \xrightarrow{\tau} \Delta (s_{(p+1)l})^{l \in L \setminus L_Q} \triangleright} \end{array} \quad \text{and} \quad \Delta (s_p)_l^{l \in L_Q} \triangleright = \Delta (s_{(p+1)l})^{l \in L_Q} \triangleright $$

2. Similarly, we have similar open transitions on states $u_{pl}$ (for the final $\tau$ transitions).

3. Finally, for the open transition in the form $(\overline{\beta}_2 = \beta_{2j}^{j \in J_2})$:
$$P[Q]_{j_0} \models \frac{\beta_{2j}^{j \in J_2}, \mathrm{Pred}_2, \mathrm{Post}_2}{\triangleleft t_l^{l \in L_Q} \triangleright \xrightarrow{\alpha'} \triangleleft (t_l')^{l \in L_Q} \triangleright}$$

If $Q$ moves then we obtain by Lemma 1:

$$P \models \frac{(\beta_{2j})^{j \in (J_2 \setminus \mathrm{Holes}(Q)) \cup \{j_0\}}, \mathrm{Pred}_2', \mathrm{Post}_2'}{\triangleleft t_l^{l \in L \setminus L_Q} \triangleright \xrightarrow{\alpha'} \triangleleft t_l'^{l \in L \setminus L_Q} \triangleright} \quad \text{and}$$

$$Q \models \frac{(\beta_{2j})^{j \in J_2 \cap \mathrm{Holes}(Q)}, \mathrm{Pred}_2'', \mathrm{Post}_2''}{\triangleleft t_l^{l \in L_Q} \triangleright \xrightarrow{\alpha_{21}} \triangleleft t_l'^{l \in L_Q} \triangleright}$$

such that $\mathrm{Pred}_2 \iff \mathrm{Pred}_2' \wedge \mathrm{Pred}_2'' \wedge \alpha_{20} = \beta_{2j_0}, \mathrm{Post}_2 = \mathrm{Post}_2' \unlhd \mathrm{Post}_2''$ where $\mathrm{Post}_2''$ is the restriction of $\mathrm{Post}_2$ over variables $\mathrm{vars}(Q)$.

Else $Q$ does not move and we have:

$$P \models \frac{(\beta_{2j})^{j \in (J_2 \setminus \mathrm{Holes}(Q)) \cup \{j_0\}}, \mathrm{Pred}_2', \mathrm{Post}_2'}{\triangleleft t_l^{l \in L \setminus L_Q} \triangleright \xrightarrow{\alpha'} \triangleleft (t_l')^{l \in L \setminus L_Q} \triangleright} \quad \text{and} \quad \triangleleft t_l^{l \in L_Q} \triangleright = \triangleleft (t_l')^{l \in L_Q} \triangleright$$

By using Lemma 4, and denoting $J = \bigcup_{i=1}^{m_1} J_{1i} \cup J_2 \cup \bigcup_{i=1}^{m_2} J_{3i}$, we can conclude from cases (1), (2) and (3) that we have:

$$P \models \frac{(\gamma_j')^{j \in (J \setminus \mathrm{Holes}(Q)) \cup \{j_0\}}, \mathrm{Pred}', \mathrm{Post}'}{\triangleleft s_l^{l \in L \setminus L_Q} \triangleright \xrightarrow{\alpha''} \triangleleft s_l'^{l \in L \setminus L_Q} \triangleright}$$

$$\text{where } \alpha'' = \alpha' \{\bigcirc_{j=m_1}^{1} \mathrm{Post}'_{1j}\}$$

On the other hand, we have:

$$\alpha = \alpha' \{\bigcirc_{j=m_1}^{1} \mathrm{Post}'_{1j}\} \{\bigcirc_{j=m_1}^{1} \mathrm{Post}''_{1j}\} = \alpha'' \{\bigcirc_{j=m_1}^{1} \mathrm{Post}''_{1j}\}.$$

As $\{\bigcirc_{j=m_1}^{1} \mathrm{Post}''_{1j}\}$ has no effect on variables of $P$ and thus on variables of $\alpha''$, so we have $\alpha = \alpha''$.

$$\forall l \in L. s_l = s_{1l} \wedge s_{(m_1+1)l} = t_l \wedge t_l' = u_{1l} \wedge u_{(m_2+1)l} = s_l'$$

$$(\gamma_j')^{j \in (J \setminus \mathrm{Holes}(Q)) \cup \{j_0\}} = \bigoplus_{i=1}^{m_1} (\beta_{1i} \{\bigcirc_{j=i-1}^{1} \mathrm{Post}'_{1j}\})^{\nabla} \oplus (\beta_2 \{\bigcirc_{j=m_1}^{1} \mathrm{Post}'_{1j}\})^{\nabla} \oplus \\ \bigoplus_{i=1}^{m_2} (\beta_{3i} \{\bigcirc_{j=i-1}^{1} \mathrm{Post}'_{3j} \odot \mathrm{Post}'_{2} \odot \bigcirc_{j=m_1}^{1} \mathrm{Post}'_{1j}\})^{\nabla}$$
$$
\begin{align*}
\text{Pred}' &= \bigwedge_{i=1}^{m_1} \text{Pred}'_{1i} \llbracket \bigcirc^{1} \text{Post}'_{1j} \rrbracket \wedge \text{Pred}'_{2} \llbracket \bigcirc^{1} \text{Post}'_{1j} \rrbracket \wedge \\
&\phantom{= \bigwedge_{i=1}^{m_1} \text{Pred}'_{1i} \llbracket \bigcirc^{1} \text{Post}'_{1j} \rrbracket \wedge} \bigwedge_{i=1}^{m_2} \text{Pred}'_{3i} \llbracket \bigcirc^{1} \text{Post}'_{3j} \odot \text{Post}'_{2} \odot \bigcirc^{1} \text{Post}'_{1j} \rrbracket \\
&\phantom{= \bigwedge_{i=1}^{m_1} \text{Pred}'_{1i} \llbracket \bigcirc^{1} \text{Post}'_{1j} \rrbracket \wedge} \text{Post}' = \bigcirc^{1} \text{Post}'_{3j} \odot \text{Post}'_{2} \odot \bigcirc^{1} \text{Post}'_{1j}
\end{align*}
$$

Note that for all $j \in J \setminus \text{Holes}(Q)$, $\gamma'_j = \gamma_j$ because for all $l \text{Post}'_{1l}$ coincides with $\text{Post}_{1l}$ on the variables of $\beta_{1ij}$, and similarly for $\text{Post}'_{2}$ and $\text{Post}'_{3l}$.

We introduce the following predicate (we will need it for reasoning about
the global predicate and will reason about it along the proof):

$$
\begin{align*}
\text{Pred}_{\beta} &= \bigwedge_{\substack{p=1 \\ m_2}}^{m_1} (\beta_{1pj_0} = \alpha_{1p}) \llbracket \bigcirc^{1} \text{Post}_{1j} \rrbracket \wedge (\beta_{2j_0} = \alpha_{21}) \llbracket \bigcirc^{1} \text{Post}_{1j} \rrbracket \wedge \\
&\phantom{=} \bigwedge_{\substack{p=1 \\ m_2}} (\beta_{3pj_0} = \alpha_{3p}) \llbracket \bigcirc^{1} \text{Post}_{3j} \odot \text{Post}_{2} \odot \bigcirc^{1} \text{Post}_{1j} \rrbracket
\end{align*}
$$

Concerning $Q$, we reduce the sequence of OTs to a path for which it moves in
all steps. In other words, if $Q$ does not move at step $q$, then we have $\llbracket s_{q_l}^{l \in L_Q} \rfloor =
\llbracket s_{(q+1)l}^{l \in L_Q} \rfloor$, then we skip the state $\llbracket s_{(p+1)l}^{l \in L_Q} \rfloor$, i.e. we rename all the following
states $\llbracket s_{pl}^{l \in L_Q} \rfloor$ where $p \ge q+1$ into $\llbracket s_{(p-1)l}^{l \in L_Q} \rfloor$. Note that self-loops where $Q$
does an action but stays at the same state are not removed. We proceed in the
same way for states named $u$. To simplify the proof, we suppose that in case 3,
$Q$ moves, else transition 3 of $Q$ should be skipped and the last $s_{pl}$ are equal to
the first $u_{1l}$. So we have:

$$
\begin{align*}
\forall p \in [1..n_1] \ Q &\models \frac{(\beta'_{1pj})^{j \in J \cap \text{Holes}(Q)}, \text{Pred}'_p, \text{Post}''_p}{\llbracket s_{pl}^{l \in L_Q} \rfloor \rightharpoonup \alpha_{1p} \rightharpoonup \llbracket s_{(p+1)l}^{l \in L_Q} \rfloor}, \\
Q &\models \frac{(\beta'_{2j})^{j \in J \cap \text{Holes}(Q)}, \text{Pred}'_2, \text{Post}''_2}{\llbracket t_l^{l \in L_Q} \rfloor \rightharpoonup \alpha_{21} \rightharpoonup \llbracket t_l^{l \in L_Q} \rfloor}
\end{align*}
$$

$$
\forall p \in [1..n_2] \ Q \models \frac{(\beta'_{3pj})^{j \in J \cap \text{Holes}(Q)}, \text{Pred}''_{3p}, \text{Post}''_{3p}}{\llbracket u_{pl}^{l \in L_Q} \rfloor \rightharpoonup \alpha_{3p} \rightharpoonup \llbracket u_{(p+1)l}^{l \in L_Q} \rfloor} \\
\text{such that } n_1 \le m_1 \text{ and } n_2 \le m_2.
$$

By renaming all state names ($s$, $u$ and $t$) with the same state name $v$. We
have:

$$
\forall p \in [1..(n_1+n_2+1)] \ Q \models \frac{\beta_{pj}^{j \in J \cap \text{Holes}(Q)}, \text{Pred''}_p, \text{Post''}_p}{\llbracket v_{pl}^{l \in L_Q} \rfloor \rightharpoonup \alpha_p \rightharpoonup \llbracket v_{(p+1)l}^{l \in L_Q} \rfloor}
$$

In this equation, and using case 1 above for all $k \in [1 \dots n_1]$ there is a $p \in [1 \dots m_1]$ such that $\alpha_{1p} = \alpha'_k$ (following the re-indexing done in the removal of steps where $Q$ does not move), we know that $\text{Pred}_{1p}$ contains the predicate $(\alpha_{1p} = \beta_{1pj_0})$.
<figure><img src="image_16.png" /><figcaption>Figure B.10: Composition of the subsequences</figcaption></figure>

Because $\beta_{1pj_0}$ only contains variables of $P$ and $\alpha'_k$ only variables of $Q$, we have:

$$ (\alpha_{1p} = \beta_{1pj_0}) \{ \bigcirc_{j=p-1}^{1} \text{Post}_{1j} \} \iff \alpha_{1p} \{ \bigcirc_{j=p-1}^{1} \text{Post}''_{1j} \} = \beta_{1pj_0} \{ \bigcirc_{j=p-1}^{1} \text{Post}'_{1j} \} \\ \iff \alpha'_k \{ \bigcirc_{j=k-1}^{1} \text{Post}''_j \} = \beta_{1pj_0} \{ \bigcirc_{j=p-1}^{1} \text{Post}'_{1j} \} $$

We can obtain similar equations for $\alpha'_{n_1+1}$ related with $\beta_{2j_0}$ and the $\alpha'_k$ for $k \ge n_1 + 2$ related with $\beta_{3pj_0}$ for some $p$. Note that the substitutions are however more complex in the other cases. Overall we obtain (we skip here the details about the three cases 1, 2, and 3 above that all fall into the same equation because of the re-indexing we perform):

$$ \mathrm{Pred}_{\beta} \iff \gamma_{j_0} = ([\alpha'_{p} \{ \bigcirc_{j=p-1}^{1} \mathrm{Post}''_{j} \}] | p \in [1..n_1 + n_2 + 1])^{\nabla} \quad (B.1) $$

Let us consider the sequence of $(n_1+n_2+1)$ actions $\alpha'_p$ some of them may be non-observable (they are $\tau$ transitions). By considering the sequence of $\tau$ and non-$\tau$ actions we split the sequence of actions into $n+1$ sub-sequences, such that each sub-sequence is a sequence of actions containing only one observable action that will be named $\alpha_p$, and possibly many non-observable ($\tau$) ones.

We can decompose each of the $n+1$ sub-sequences in the following way (see Figure B.10). For $k \in [0..n]$ the position of the $k^{th}$ visible action is $n_k$. For $l \in [1..n]$, $n'_l$ is any index between $n_{l-1}$ and $n_l$, additionally $n'_1 = 1$ and $n'_{n+1} = n_1 + n_2 + 1$. We obtain $n$ sub-sequences made of the following OTs, for all $k \in [1..n]$:

$$ \forall p \in [n'_k..(n_k-1)] \ Q \models \frac{\beta_{p,l}^{j \in J \cap \text{Holes}(Q)}, \text{Pred}_p'', \text{Post}_p''}{\Delta v_{pl} \triangleright \tau \rightarrow \Delta v_{(p+1)l} \triangleright} $$

$$ Q \models \frac{\beta_{n_k l}^{j \in J \cap \text{Holes}(Q)}, \text{Pred}_{n_k}'', \text{Post}_{n_k}''}{\Delta v_{n_k l}^{l \in L_Q} \triangleright \alpha_{n_k}' \rightarrow \Delta v_{(n_k+1)l}^{l \in L_Q} \triangleright} \text{ and} $$

$$ \forall p \in [(n_k+1)..(n'_{k+1}-1)] \ Q \models \frac{\beta_{p,j}^{j \in J \cap \text{Holes}(Q)}, \text{Pred}_p'', \text{Post}_p''}{\Delta v_{pl}^{l \in L_Q} \triangleright \tau \rightarrow \Delta v_{(p+1)l}^{l \in L_Q} \triangleright} $$

Thereafter, by Lemma 4 we can deduce the following weak open transition:

$$ Q \models \frac{(\gamma_{kj})^{j \in J \cap \text{Holes}(Q)}, \text{Pred}_k, \text{Post}_k}{\Delta v_{kl}^{l \in L_Q} \triangleright \alpha_k \Rightarrow \Delta (v'_{kl})^{l \in L_Q} \triangleright} $$