# Barbed Semantics for Open Reactive Systems

Fabio Gadducci, Giacoma Valentina Monreale

## ► To cite this version:

Fabio Gadducci, Giacoma Valentina Monreale. Barbed Semantics for Open Reactive Systems. 21th International Workshop on Algebraic Development Techniques (WADT), Jun 2012, Salamanca, Spain. pp.161-177, 10.1007/978-3-642-37635-1_10. hal-01485968

HAL Id: hal-01485968

https://inria.hal.science/hal-01485968

Submitted on 9 Mar 2017

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# Barbed Semantics for Open Reactive Systems*

Fabio Gadducci and Giacoma Valentina Monreale

Department of Informatics, University of Pisa, Italy

**Abstract.** Reactive systems (RSs) represent a meta-framework aimed at deriving labelled transition systems from unlabelled ones such that the induced bisimilarity is a congruence. Such a property is desirable, since it allows one to replace a subsystem with an equivalent one without changing the behaviour of the overall system. One of the main drawback of RSs is the restriction to the analysis of ground (i.e., completely specified) systems. Only recently the theory was extended to consider open systems (and rules) and an associated strong bisimulation equivalence. However, the resulting bisimilarity adopted for the formalism turns out to be a congruence only under very restrictive conditions, hindering the applicability of the framework. In this paper we suggest to consider (strong and weak) barbed equivalence as an alternative for open RSs. After proving that it is always a congruence, we instantiate our proposal by addressing the semantics of Asynchronous CCS and of Mobile Ambients.

**Keywords:** Open reactive systems, (saturated) barbed bisimilarities.

## 1 Introduction

The most common technique for specifying the dynamics of a system is based on a reduction semantics: a set representing the states of the system, plus an unlabelled relation among these states, usually built out of a finite set of rules, denoting the evolutions. Despite the advantage of conveying the behaviour with relatively few rules, the main drawback of reduction semantics is that the dynamics of a system is described in a monolithic way, meaning that the evolution is obtained by closing the set of rules under all contexts. Thus, a subsystem can be interpreted only by inserting it inside the contexts where a reduction may take place. To make the analysis simpler, it is often necessary to consider descriptions accounting separately for the behaviour of each single sub-component, thus increasing modularity and enhancing the opportunities for verification.

The theory of reactive systems (RSs) [17] offers a framework that allows to distill labelled transition systems (LTSs), hence to obtain behavioural equivalences, for formalisms based on reduction semantics. The idea is simple: a system $p$ has a labelled transition $p \xrightarrow{c} p'$ if the system obtained by inserting $p$ inside the (unary) minimal context $c$ may reduce to $p'$. The notion of “minimal” context is expressed via the categorical notion of relative pushout (RPO), which ensures

<footnote>* Research partially supported by the EU FP7-ICT IP ASCEns (IP 257414).</footnote>
that bisimilarity is a congruence when enough RPOs exist. A grupoidal extension (GRSs) has been proposed [24], in order to deal with equationally specified systems (e.g. processes in a calculus with structural congruence).

Should all the possible contexts allowing a reduction be admitted as labels, the resulting bisimilarity would in general be coarser. Despite being better suited in some case studies, such an equivalence (called saturated bisimilarity) is usually intractable, since it has to tackle a potentially infinite set of contexts. The problem has been addressed in [6] by introducing an “efficient” characterisation of these semantics, where one avoids considering all contexts by using in a cuning way RPOs, at the price of modifying the standard, symmetric presentation of the (either strong or weak) bisimulation equivalences.

Despite their wide range of applicability, saturated and “minimal contexts” bisimilarities still fail to cover all the interesting possibilities: the former is sometimes too fine-grained, while the latter is too coarse. As for process calculi, the standard way out of the impasse is to consider barbs [20] (that is, predicates on the states of a system) and barbed equivalences (where the check of such predicates is added to the bisimulation game). The flexibility of the definition allows for recasting a variety of observational, bisimulation-based equivalences. Therefore, a suitable notion of barbed saturated semantics for RSs is introduced in [4], and it is further investigated in [3,5], where an efficient characterisation for both the strong and weak case is presented, avoiding to consider all contexts.

Even if these extensions witness the vitality of the formalism, one of the fiercest limits suffered by RSs was the restriction to ground rules for describing the dynamics of a system. We are aware of two different attempts to deal with parametric rules in the (G)RS framework. In [10], the notion of a category of second-order contexts is introduced and the RPO construction is carried out in this setting, to capture the lazy observational equivalence of λ-calculus. In [16], a general theory for open (G)RSs is developed, by considering open terms and rules. So, now the transitions are labelled not only with the minimal context but also with the most general instantiation allowing a reduction. More explicitly, $p \xrightarrow[c]{x} p'$ if $p$ inserted into the context $c$ and instantiated with the (possibly open) term $x$ may evolve into a state $p'$. The notions of minimal context and most general instantiation are captured at once by the notion of (G-)lux. The (strong) bisimilarity induced by the synthesised LTS for open terms is a congruence only under very restrictive conditions, hindering the applicability of the framework. It indeed seems that such conditions are satisfied by simple process calculi with a trivial structural congruence, but that this is not always so for richer calculi.

This paper, along the lines of [4], proposes a suitable notion of barbed saturated bisimilarity for open GRSs: this is by definition guaranteed to be a congruence and, under certain conditions, it can alternatively be described in a more efficient way via the G-lux LTS and the semi-saturated game. We present the study for both the strong and the weak equivalence and, as it is usual for any newly proposed technique, we test their adequacy against suitable case studies. We thus consider the asynchronous CCS [1], whose simplicity allows us to use it as running example, and MAs, whose more complex behaviour highlights the
usefulness of open semantics. In both cases, we show that the closed version of
our semantics exactly captures the standard ones of the calculus.

The paper is organised as follows. §2 recalls the notion of 2-category on which the one of GRS is based, and shows how it can be used to model the syntax of a calculus. §3 introduces open GRSs and the definition of G-lux LTS. The technical core of the paper is presented in §4, where both the strong and weak barbed saturated semantics for open GRSs are studied, and labelled characterisations of them by means of their semi-saturated counterparts are offered. §5 shows an application of the framework to MAs and §6 concludes the paper.

The appendix recalls the categorical notions of GRPO and GRPB (needed
in §3), as well as the proof of our main result.

**2 A categorical representation of process calculi**

This section briefly introduces a categorical representation of a process calculus, previously introduced in [16], and based on the notion of 2-category [8,15].

**Definition 1 (2-category).** A 2-category **C** is a category such that, given any two objects *a* and *b*, the hom-set of *a* and *b* (the collections of arrows between them) is the class of objects of some category **C**(*a*, *b*) and, correspondingly, whose composition functions *∗*: **C**(*a*, *b*) × **C**(*b*, *c*) → **C**(*a*, *c*) are functors.

Arrows of $\mathbf{C}(a, b)$ are called 2-cells and are denoted by $\alpha: f \Rightarrow g: a \to b$, the composition in $\mathbf{C}(a, b)$ is instead denoted by $\bullet$.

**Definition 2 (G-category).** A groupoidal category (*G-category*) is a 2-*category* whose 2-*cells* are *invertible*.

G-categories can be used to model the syntax of process calculi. We will show
an example of this by exploiting a G-category based on the PROP-category [18].

**Definition 3 (PROP-category).** A product and permutation category (PROP-category) **C** has natural numbers 0, 1, 2, ... as objects and it is equipped with two further structures, as follows

- for each $n$, the group of permutations of $n$ elements, $S(n)$, is a subgroup of all the invertible elements of the hom-set $\mathbf{C}(n, n)$. The identity permutation is the identity morphism $1_n : n \to n$;

- there is a functor $\otimes: \mathbf{C} \times \mathbf{C} \to \mathbf{C}$, called product and written between its arguments, which acts as addition on the objects, i.e., $m \otimes n = m + n$, and moreover it is required that

1. it is associative: $(f \otimes f') \otimes f'' = f \otimes (f' \otimes f'')$;

2. given $\sigma \in S(n)$ and $\sigma' \in S(n')$, we have $\sigma \otimes \sigma' = \sigma \times \sigma' : n+n' \to n+n'$, where $\times$ denotes the product of permutations;

3. for any two natural numbers $n, n'$, let $\gamma_{n,n'}$ be that permutation in $S(n+n')$ which interchanges the first block of $n$ and the second block of $n'$, $\gamma_{n,n'} : n+n' \to n+n'$. For any maps $f: m \to n$ and $f': m' \to n'$ we require that $\gamma_{n,n'}(f \otimes f') = (f' \otimes f)\gamma_{m,m'}$.
$$ P ::= \epsilon, a.P, \bar{a}, P \mid P \mid (P|Q)|R \equiv P|(Q|R) \quad P|Q \equiv Q|P \mid a.P \mid \bar{a} \rightsquigarrow P \quad \frac{P \rightsquigarrow Q}{P|R \rightsquigarrow Q|R} $$

<caption>Fig. 1. Syntax, structural congruence and reduction relation of ACCS.</caption>

A G-PROP is a PROP where the underlying category is a G-category.

*Example 1.* We now show how the signature of a calculus (modulo term equations) may induce a G-PROP. Inspired by the characterisation of (a fragment of) CCS in [16], we model here the finite, restriction and summation free fragment of the asynchronous version of the calculus [1]. Later on, we will use the same approach for modelling our main case study, i.e., Mobile Ambients (MAs) [9].

The syntax of ACCS is shown on the left of Fig. 1. We assume a set $\mathcal{N}$ of names ranged over by $a, b, c, \dots$. Also, we let $P, Q, R, \dots$ range over the set of processes. The processes are considered up to the structural congruence $\equiv$ induced by the two axioms in the middle of Fig. 1. To keep the example simple, there is no structural rule guaranteeing that $\epsilon$ is the identity for the parallel composition. The transition relation $\rightsquigarrow$ is defined by the rightmost rules of the same figure: it is going to be used just in the forthcoming sections, even if it is introduced here for the sake of presentation.

The signature for ACCS is $\Sigma = \epsilon : 0, a : 1, \bar{a} : 0, | : 2$. The arrows $p : m \to n$ of G-PROP PA2CP represent $n$-tuples of terms over $\Sigma$ quotiented by associativity (the leftmost axiom in the middle of Fig. 1) that altogether contain $m$ distinct holes. Permutations in $(n, n)$ are tuples built from holes, $\otimes$ acts on arrows as tuple juxtaposition, and arrows composition is the standard term composition.

To define the 2-cells of the category, an explicit representation of the arrows of the category is used. A term can be indeed represented as a finite, ordered tree with nodes of any degree, where an immediate child of a node of degree higher than 1 must have degree at most 1. Leaves of such a tree correspond to occurrences either of outputs or of the constants $\epsilon$, so they are labelled with names belonging to $\mathcal{N}$ or with $\epsilon$; nodes of degree 1 correspond to applications of prefix operators and they are indeed labelled with names belonging to $\mathcal{N}$; and nodes of higher degree correspond to term fragments built solely of the parallel operator. So, arrows can be represented as tuples of these trees.

A 2-cell from $p$ to $q$ intuitively says that they are equivalent with respect to the commutative axiom. So, it is defined as a family, indexed by the nodes of (the explicit representation of) $p$, of permutations on the sets of their immediate children, such that the application of all these permutations to $p$ yields $q$.

# 3 Open G-Reactive Systems

This section presents an extension, previously proposed in [16], of the theory of *G-reactive systems* (GRSs) [24]. In general, the aim of this theory is to derive labelled transition systems (LTSs) and bisimulation congruences for those specification formalisms whose operational semantics is provided by reduction rules.
In [24], the technique of LTS derivation is defined for closed GRSs, that is, by considering closed terms and ground reduction rules, while in [16], open terms and parametric rules are considered. The idea is quite simple: a system specified by an open term *p* has a labelled transition *p* $\xrightarrow{c}^x$ *p'* if *p* instantiated with the (open) term *x* and inserted into the context *c* may evolve into a state *p*'.

A G-category $\mathbf{C}$ models the syntax of a formalism. An (*open*) system is an arrow $p : a_1 \to a_2$: it can be plugged into $q : a_2 \to a_3$ via arrows composition. Given arrows $p, q : a_1 \to a_2$, a 2-cell $\alpha : p \Rightarrow q$ represents an isomorphism (i.e., a proof of equivalence) between systems $p$ and $q$. The semantics is given via *reduction rules*: pairs of systems $\langle l, r \rangle$ with the same interfaces.

**Definition 4 (Open GRS).** An open G-reactive system $\mathbf{C}$ consists of

1. a G-category $\mathbf{C}$;

2. a composition-reflecting, 2-cell closed subcategory $\mathbf{D}$ of reactive contexts;

3. a set $\mathfrak{R} \subseteq \bigcup_{a_1, a_2 \in \mathbf{C}} \mathbf{C}(a_1, a_2) \times \mathbf{C}(a_1, a_2)$ of reduction rules.

Intuitively, reactive contexts are those arrows inside which a reduction can occur. By 2-cell closed we mean that $d \in \mathbf{D}$ and $\alpha : d \Rightarrow d'$ in $\mathbf{C}$ implies $d' \in \mathbf{D}$, while by composition-reflecting we mean that $d'; d \in \mathbf{D}$ implies $d, d' \in \mathbf{D}$.

Given an open GRS $\mathbf{C}$, the reduction relation over the terms of $\mathbf{C}$ is generated by closing the reduction rules under all reactive contexts, instantiations and 2-cells. Formally, the *reduction relation* is defined by taking $p \rightsquigarrow p'$ if there exist $\langle l, r \rangle \in \mathfrak{R}$, $d \in \mathbf{D}$, $x \in \mathbf{C}$, $\alpha : p \Rightarrow x; l; d$ and $\alpha' : p' \Rightarrow x; r; d$.

*Example 2.* Consider the G-PROP PA2CP category shown in §2. An open GRS $\mathbf{C}_{\text{ACCS}}$ over it takes as reduction rules the set $\bigcup_{a \in \mathcal{N}} \{\langle a.1 \mid \bar{a}, 1 \rangle\}$, and as the subcategory of reactive contexts the smallest composition-reflecting, 2-cell closed subcategory including arrows of the shape $1 \mid p : 1 \to 1$. Note that it contains no context with a hole after the input operator.

The behaviour of an open GRS is given by an unlabelled transition system. To obtain a labelled one, we instantiate an open system *p* with a sub-term *x*, plug the result into a context *c* and observe if a reduction occurs. Categorically, it means that *x*; *p*; *c* is isomorphic to *y*; *l*; *d* (there exists $\alpha : x; p; c \Rightarrow y; l; d$) for an instantiation *x*, a rule $\langle l, r \rangle$, and a reactive context *d*, as depicted by diagram (i) of Fig. 2. We shall refer to this kind of diagrams as hexagons.

Clearly, the resulting LTS is often infinite-branching, since all contexts and all instantiations allowing reductions may occur as labels. Moreover, it has re- dundant transitions: the ACCS open process a.1 would have both transitions a.1 $\xrightarrow{1|\bar{a}}$ 1 and a.1 $\xrightarrow{1|\bar{a}|p}$ 1 $|q|p$, yet neither *p* nor *q* “concur” to the reduction. In order to remove this kind of redundancy, we thus consider only “minimal con- texts allowing a reduction” and the “most general instantiations”, both modelled by the categorical notion of G-locally universal hexagons (G-luxes). The explicit definition of G-lux is found in [16], here we use a simpler characterisation of it in terms of the better known notions of groupoidal-idem pushouts (GIPOs) and
<figure><img src="image_2.png" /><figcaption>Fig. 2. Hexagon and G-lux.</figcaption></figure>

groupoidal-idem pullbacks (GIPBs) in G-categories (see [16, Lemma 10]). We refer to [24] for the notion of GIPO, the one of GIPB being symmetric. For the convenience of the reader we report both definitions in Appendix A.

**Definition 5 (G-lux).** The hexagon (i) in Fig. 2 is a G-locally universal hexagon (G-lux) if (ii) is a GIPO and (iii) is a GIPB.

We say that a GRS has G-luxes if in its underlying category every hexagon as diagram (i) in Fig. 2 has an inner G-lux hexagon as diagram (iv) such that
$$ \alpha = \delta * 1_p * \beta * 1_z * \psi * 1_e * \varphi * 1_l * \gamma. $$

**Definition 6 (GLUX Transition System).** Let $\mathbb{C}$ be an open GRS and $\mathbb{C}$ its underlying G-category. The GLUX LTS $(\mathrm{LLTS}(\mathbb{C}))$ is defined as follows

- states: $p : a_1 \to a_2$ in $\mathbb{C}$, for arbitrary $a_1$ and $a_2$;

- transitions: $p \xrightarrow{c} p'$ if there exist $d \in \mathbb{D}$, $y \in \mathbb{C}$, rule $\langle l, r \rangle \in \Re$ and 2-cell $\alpha : x; p \Rightarrow y; l; d$ such that diagram (i) of Fig. 2 is a G-lux and $p' = y; r; d$.

**Example 3.** As for the synchronous version [16], it can be shown that the GRS $\mathbb{C}_{\mathrm{ACCS}}$ has G-luxes. The leftmost diagram of Fig. 3 shows the derived transition $a.\bar{a} \xrightarrow{1|\bar{a}} \bar{a}$ (the instantiation 0 is usually omitted). Here the initial state offers a closed process with an input on the channel $a$ at top level, while the environment provides an output action on the same channel, so the communication on it can occur. Note instead that no instantiation is provided. The rightmost diagram of Fig. 3 shows instead the transition $a.e \mid 1 \xrightarrow{\bar{a}} e$. Also in this case the initial state offers an input on $a$ at top level but here it is in parallel with a hole, which is going to be replaced with the output action on the same channel provided by the instantiation. So, also in this case, the communication on the same channel can occur. Note however that here the environment does not offer anything.

In [16], (strong) bisimilarity on LLTS is referred to as GLUX-bisimilarity $\sim^L$: despite the flexibility of the G-luxes framework, $\sim^L$ is a congruence (i.e., if $p \sim^L q$, then $p; c \sim^L q; c, \forall c \in \mathbb{C}$) under some (restrictive) assumptions on $\mathbb{C}$. In particular, a 2-categorical version of the requirement that all arrows of $\mathbb{C}$ are mono must be satisfied. These conditions hold for simple process calculi with a
<figure><img src="image_3.png" /><figcaption>Fig. 3. G-luxes representing the transitions $a.\bar{a} \xrightarrow{1|\bar{a}} \bar{a}$ and $a.\epsilon | 1 \xrightarrow{\bar{a}} \epsilon$.</figcaption></figure>

trivial structural congruence, such as the choice-free fragment of CCS (as proved in [16]) and thus apparently also by its asynchronous version considered here, even if it is doubtful for richer calculi such as Mobile Ambients.

**Remark 1.** The standard notion of GRS [24] is very similar to the one presented in Definition 4. One difference is that in the G-category **C** the existence of a chosen object 0 is required, which can never be the codomain of any arrow and which is used to denote the lack of holes. So, arrows having 0 as domain are deemed to represent closed terms. Building on this, the main difference is that the rules are ground, that is, they are pairs of closed terms, and also the states of the reduction relation and of the derived (GIPO) LTS are so. The reduction relation is thus defined by taking $p \leadsto p'$ if there exist $\langle l, r \rangle \in \Re$, $d \in \mathbf{D}$, $\alpha : p \Rightarrow l; d$ and $\alpha' : q \Rightarrow r; d$. In the LTS, instead, $p \stackrel{c}{\Rightarrow} p'$ if for $d \in \mathbf{D}$ and $\langle l, r \rangle \in \Re$, the square $p, c, l, d$ is a GIPO and $p' = r; d$.

It is easy to see that if we specialise the theory of open GRSs to consider closed terms and closed rules, it subsumes the standard theory of GRSs. Indeed, being both terms and rules ground, in the definition of the reduction relation the $x$ will trivially be the identity on 0, so the definition coincides with the one for closed GRSs. Let us now look at the derived LTS. If we consider again closed states and rules, the definition of transition coincides: since both the instantiations $x$ and $y$ will be the identity on 0, the requirement that diagram (i) of Fig. 2 is a G-lux, by definition, means that the square $p, c, l, d$ is a GIPO and the square $0, p; c, 0, l; d$ a GIPB. So, it is easy to see that $p \stackrel{c}{\Rightarrow} p'$ is a GLUX transition if and only if it is also a GIPO one.

If instead open rules and closed are considered, then in the definition of the reduction relation the instantiation $x$ of $l$ can be different from 0, and an equivalent, closed GRS is obtained by instantiating all the open rules, i.e., if it contains the ground rule $\langle x; l, x; r \rangle$ for any $x$. Instead, as far as the definition of LTS is concerned, in diagram (i) of Fig. 2 the $x$ has to be the identity on 0 (since $p$ is ground). By definition, the hexagon is a G-lux if and only if $p, c, y; l, d$ is a GIPO and the square $0, p; c, y, l; d$ is a GIPB, therefore, it is easy to check that $p \stackrel{c}{\Rightarrow} p'$ is a GLUX transition if and only if the corresponding closed GRS containing the ground rule $\langle y; l, y; r \rangle$ has the same GIPO transition.
# 4 Barbed Semantics for Open Reactive Systems

Barbed bisimulation represents a general technique for generating bisimulation-based equivalences. Intuitively, a barb is just a predicate on the states of a system, which detects the possibility of performing some observable action. We write $P \downarrow_o$ if $P$ satisfies the predicate $o$. Barbed equivalences add the check of such predicates in the bisimulation game: every time that a system shows a barb, the equivalent system has to show the same barb, and vice-versa. For instance, ACCS barbs express the ability of a process to perform an output over a channel. Formally, for a closed process $P$, $P \downarrow_{\bar{a}}$ if $P \equiv \bar{a} \mid Q$, for some $Q$. In [1] this notion is used to give the definition of barbed equivalence for the calculus.

In general, the advantage of this kind of semantics is that the flexibility of the definition allows for recasting a wide variety of observational, bisimulation-based equivalences. For example, in [1], the authors prove that the standard bisimilarity for ACCS, (weak) asynchronous bisimilarity, coincides with (weak) barbed equivalence. In [4], instead, a suitable notion of (weak) barbed semantics for closed RSs is introduced, showing that it can be characterised via the LTS labelled with minimal contexts and the semi-saturated game, and that the proposal captures the behavioural semantics for MAs.

Along the lines of [4], we introduce suitable notions of strong and weak barbed saturated semantics for open GRSs and characterise them via the GLUX LTS.

## 4.1 Strong Open Barbed Saturated Semantics

As for closed systems, barbs for open ones are state predicates. In the following, we fix a 2-cells respected family $\mathcal{O}$ of barbs on open systems, and we write $p \downarrow_o$ if $p$ satisfies $o \in \mathcal{O}$. By 2-cells respected, we mean that $p \downarrow_o$ and $\alpha : p \Rightarrow q$ implies $q \downarrow_o$. For example, if we consider tuples of open terms, ACCS barbs can observe the presence of an output action at top level of a term.

**Definition 7 (Open Barbed Saturated Bisimulation).** A symmetric relation $\mathcal{R}$ is an open barbed saturated bisimulation if whenever $p \mathcal{R} q$ then $\forall x, c$

- if $x; p; c \downarrow_o$ then $x; q; c \downarrow_o$;

- if $x; p; c \rightsquigarrow p'$ then $x; q; c \rightsquigarrow q'$ and $p' \mathcal{R} q'$.

Open barbed saturated bisimilarity $\sim^{\text{OBS}}$ is the largest such bisimulation.

Note that $\sim^{\text{OBS}}$ is a congruence by definition. It can be efficiently characterised through the GLUX transition system via the semi-saturated game.

**Definition 8 (Open Barbed Semi-Saturated Bisimulation).** A symmetric relation $\mathcal{R}$ is an open barbed semi-saturated bisimulation if whenever $p \mathcal{R} q$ then

- $\forall x, c, \text{ if } x; p; c \downarrow_o \text{ then } x; q; c \downarrow_o$;

- if $p \xrightarrow{c} p'$ then $x; q; c \rightsquigarrow q'$ and $p' \mathcal{R} q'$.

Open barbed semi-saturated bisimilarity $\sim^{\text{OBSS}}$ is the largest such bisimulation.
**Proposition 1.** In an open GRS having G-luxes, $\sim^{\text{OBSS}}=\sim^{\text{OBS}}$.

As an immediate test of the adequacy of our framework, we apply it to ACCS. We know that the standard bisimilarity for ACCS coincides with the barbed equivalence, which in turn is equivalent to the open barbed saturated bisimilarity defined only over closed ACCS processes [11]. Now we can define the open barbed semi-saturated bisimilarity for ACCS by using the GLUX LTS for the calculus, and since the open GRS has G-luxes, thanks to Proposition 1, we can say that it coincides with the open barbed saturated bisimilarity. Therefore, if we consider only closed ACCS processes, we can conclude that barbed semi-saturated bisimilarity is equivalent to asynchronous bisimilarity.

*Proof.* Clearly $\sim^{\text{OBS}}\subseteq\sim^{\text{OBSS}}$: it suffices to note that $p \xrightarrow{x} p'$ implies $x;p;c \rightsquigarrow p'$.

We then focus on $\sim^{\text{OBSS}}\subseteq\sim^{\text{OBS}}$. We prove it by showing that the closure $S$ of the strong open barbed semi-saturated bisimilarity with respect to instantiations, contexts and 2-cells $S = \{\langle u, v\rangle|u \Rightarrow x;p;c, v \Rightarrow x;q;c, p \sim^{\text{OBSS}} q, x \in \mathbf{C}, c \in \mathbf{C}\}$ is a strong open barbed saturated bisimulation.

Suppose that $x';u;c' \downarrow_o$. By hypothesis barbs are respected by 2-cells, thus $x';x;p;c;c' \downarrow_o$. Since $p \sim^{\text{OBSS}} q$ also $x';x;q;c;c' \downarrow_o$ and so $x';v;c' \downarrow_o$.

Suppose that $x';u;c' \rightsquigarrow p'$. Then, also $x';x;p;c;c' \rightsquigarrow p'$. This means that for some $\langle l,r\rangle \in \mathfrak{R}$, $y \in \mathbf{C}$ and $d \in \mathbf{D}$, we have that there exists $\alpha: x';x;p;c;c' \Rightarrow y;l;d$ (diagram (i)) and $p'=y;r;d$.

<figure><img src="image_4.png" /><figcaption>(i)</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>(ii)</figcaption></figure>

Since the GRS has G-luxes, we can construct a G-LUX as the inner hexagon of diagram (i). This means that $p \xrightarrow{x''} y'';r;d''$ and since $p \sim^{\text{OBSS}} q$, then $x'';q;c'' \rightsquigarrow q'$ and $y'';r;d'' \sim^{\text{OBSS}} q'$. Therefore, there exists an hexagon as the inner one of diagram (ii) shown above, with $\langle l', r' \rangle \in \mathfrak{R}$ and $q' = y';r';d'$. Thanks to the fact that $\mathbf{D}$ is 2-cell closed and composition reflecting, we know that $e$ is reactive, hence $z;x'';q;c'';e \rightsquigarrow z;q';e$. Since $x';x;q;c;c' \Rightarrow z;x'';q;c'';e$ and $x';v;c' \Rightarrow x';x;q;c;c'$ also $x';x;q;c;c' \rightsquigarrow z;q';e$ (external hexagon of diagram (ii)) and $x';v;c' \rightsquigarrow z;q';e$. Moreover, since $y'';r;d'' \sim^{\text{OBSS}} q'$ and $p'=y;r;d \Rightarrow z;y'';r;d'';e$, we can conclude that $p' S z;q';e$.

## 4.2 Weak Open Barbed Saturated Semantics

This section introduces the weak case of open barbed (semi-)saturated bisimilarity. We begin by introducing the notion of weak barb on open states.
**Definition 9 (Weak Barb).** Let $o \in O$ be a barb. An open state $p$ satisfies the weak barb $o$ (in symbols $p \downarrow_o$) if there exists $p'$ such that $p \rightsquigarrow^* p'$ and $p' \downarrow_o$.

As usual, $\rightsquigarrow^*$ denotes the transitive and reflexive closure of $\rightsquigarrow$.

**Definition 10 (Weak Open Barbed Saturated Bisimulation).** A symmetric relation $\mathcal{R}$ is a weak open barbed saturated bisimulation if whenever $p \mathcal{R} q$ then $\forall x, c$

- if $x; p; c \downarrow_o$ then $x; q; c \downarrow_o$;

- if $x; p; c \rightsquigarrow^* p'$ then $x; q; c \rightsquigarrow^* q'$ and $p' \mathcal{R} q'$.

Weak open barbed saturated bisimilarity $\sim^{\text{WOBS}}$ is the largest such bisimulation.

As for the strong case, it can be efficiently characterised through the GLUX transition system via the semi-saturated game.

**Definition 11 (Weak Open Barbed Semi-Saturated Bisimulation).** A symmetric relation $\mathcal{R}$ is a weak open barbed semi-saturated bisimulation if whenever $p \mathcal{R} q$ then

- $\forall x, c, \text{ if } x; p; c \downarrow_o \text{ then } x; q; c \downarrow_o$;

- if $p \xrightarrow{c} p' \text{ then } x; q; c \rightsquigarrow^* q'$ and $p' \mathcal{R} q'$.

Weak open barbed semi-saturated bisimilarity $\sim^{\text{WOBSS}}$ is the largest such bisimulation.

The correspondence result is stated below: its proof is shown in Appendix B.

**Proposition 2.** In an open GRS having G-luxes, $\sim^{\text{WOBSS}} = \sim^{\text{WOBS}}$.

As for the strong case, also for the weak one we can immediately test our proposal against ACCS. In particular, by following the reasoning used in the previous section for the strong case, we can analogously conclude that if we consider only closed ACCS processes, weak barbed semi-saturated bisimilarity is equivalent to weak asynchronous bisimilarity.

# 5 An Open G-Reactive System for Mobile Ambients

In this section we apply the framework of open GRSs to a richer calculus, that is, the calculus of Mobile Ambients (MAs) [9], in order to show the adequacy of the results presented in §4. After a quick introduction of the calculus, we present the corresponding open GRSs and we test our framework on it.
<figure><img src="image_6.png" /><figcaption>**Fig. 4.** Syntax, structural congruence and reduction relation of MAs.</figcaption></figure>

## 5.1 Mobile Ambients

We consider the finite, restriction free fragment of MAs. The syntax is shown on the left of the upper row of Fig. 4. We assume a set $\mathcal{N}$ of names ranged over by $m, n, u, \dots$. We let $P, Q, R, \dots$ range over the set $\mathcal{P}$ of closed processes. The semantics of the calculus is given by the combination of an equivalence between processes and a relation among them. The structural congruence $\equiv$ is induced by the two axioms on the right of the first row of Fig. 4. It is used to define the reduction relation $\rightsquigarrow$, which is inductively generated by the set of axioms and inference rules shown in the lower rows of Fig. 4.

As said in the previous section, a *barb o* is a predicate over the states of a system, with $P \downarrow_o$ denoting that $P$ satisfies $o$. In MAs, $P \downarrow_n$ denotes the presence at top-level of an ambient $n$. Formally, for a closed process $P$, $P \downarrow_n$ if $P \equiv n[Q]|R$ for some closed processes $Q$ and $R$. A closed process $P$ satisfies the weak barb $n$ (denoted as $P \downarrow_n$) if there exists a process $P'$ such that $P \rightsquigarrow^* P'$ and $P' \downarrow_n$. The notions of strong and weak barb above are respectively used to define the strong and weak reduction barbed congruences [19].

**Definition 12 (Reduction Barbed Bisimulation).** A symmetric relation $\mathcal{R}$ is a reduction barbed bisimulation if whenever $P\mathcal{R}Q$ then $\forall C[-]$ contexts

- if $C[P] \downarrow_o$ then $C[Q] \downarrow_o$;

- if $C[P] \rightsquigarrow P'$ then $C[Q] \rightsquigarrow Q'$ and $P'\mathcal{R}Q'$.

A symmetric relation $\mathcal{R}$ is a weak reduction barbed bisimulation if whenever $P\mathcal{R}Q$ then $\forall C[-]$ contexts

- if $C[P] \downarrow_o$ then $C[Q] \downarrow_o$;

- if $C[P] \rightsquigarrow^* P'$ then $C[Q] \rightsquigarrow^* Q'$ and $P'\mathcal{R}Q'$.

Reduction barbed congruence $\cong$ and weak reduction barbed congruence $\cong^W$ are the largest such bisimulations.

Labelled characterisations of reduction barbed congruences over MAs processes are presented in [22,4] for the strong case, and in [19,4] for the weak one. In the following, we are going to provide an alternative characterisation of them by using the GLUX LTS and the semi-saturated game.
## 5.2 An open GRS for Mobile Ambients

As for ACCS, in order to define the open GRS for MAs, we exploit the G-PROP PA2CP induced from the signature corresponding to the grammar for the calculus modulo the associativity equation. The signature is $\Sigma = \epsilon : 0, n[\quad]: 1, M. : 1, \mid : 2$, where *M* stands for *in n*, *out n* and *open n*.

For the definition of 2-cells, we consider an analogous representation for the terms and consequently for the arrows of the category. The main difference with respect to the representation used for ACCS is that here leaves only correspond to occurrences of the constants $\epsilon$, while a node of degree 1 corresponds to an application of either an ambient operator or a capability. In the former case it is labelled with a name belonging to $\mathcal{N}$, while in the latter case it is labelled with the capability followed by an ambient name.

Now, we use this G-PROP to define the open GRS $C_{MAs}$ for MAs. We take as reduction rules the set $\bigcup_{n,m \in \mathcal{N}} \{\langle n[in m.1 | 2] | m[3], m[n[1 | 2] | 3]\rangle, \langle m[n[\mathit{out} m.1 | 2] | 3], n[1 | 2] | m[3]\rangle, \langle \mathit{open} n.1 | m[2], 1 | 2\rangle\}$, and as the subcategory of reactive contexts the smallest composition-reflecting, 2-cell closed subcategory including arrows of the shapes $1 \mid p : 1 \to 1$ and $n[1] : 1 \to 1$. Note that it does not contain contexts with a hole after a capability.

Fig. 5 shows two interesting labelled transitions derived by applying the synthesis mechanism based on G-luxes. The leftmost G-lux represents $n[1] \xrightarrow[\mathit{in} m.1|2]{1|m[Q]} m[n[1 | 2] | Q]$. The initial open term offers an ambient $n$ with a hole inside it, the instantiation provides the open term $in m.1 | 2$, which is going to replace the hole inside the ambient $n$, while the environment provides an ambient $m[Q]$ which is going to be in parallel with $n$. The rightmost G-lux instead represents $n[1] \xrightarrow[\mathit{out} m.1|2]{m[1|R]} n[1 | 2] | m[R]$. Also in this case the initial open term offers an ambient $n$ with a hole inside it, the instantiation instead provides the open term $\mathit{out} m.1 | 2$, which is going to replace the hole inside the ambient $n$, while the environment provides an ambient $m$ with a hole inside it (which will be replaced by $n$) in parallel with a closed process $R$.

These transitions show the importance of using instantiation and context at the same time. In both cases, indeed, we can note the interaction of three parts intervening in the reduction: the initial state, the instantiation and the context.

<figure><img src="image_7.png" /><figcaption>**Fig. 5.** The transitions $n[1] \xrightarrow[\mathit{in} m.1|2]{1|m[Q]} m[n[1 | 2] | Q]$ and $n[1] \xrightarrow[\mathit{out} m.1|2]{m[1|R]} n[1 | 2] | m[R]$.</figcaption></figure>
This never happens in ACCS, where we only have the synchronization between
two terms in parallel which thus can be offered by just two of these three parts.

**5.3 Open Barbed Semantics for Mobile Ambients**

Here we show that the labelled characterisations of $\cong$ and $\cong^W$ via the GIPO LTS and the semi-saturated game presented in [4] are an instance of our results stated in Propositions 1 and 2.

We begin by observing that if we consider only closed terms and the stan-
dard notion of strong (respectively weak) barb for them, the notion of strong
(respectively weak) open barbed saturated bisimilarity for MAs coincides with
the one of strong (respectively weak) reduction barbed congruence, where $C[P]$
stands for $P; C[-]$. Therefore, as shown in § 4, since the open GRS has G-luxes,
we can efficiently characterise the strong and weak reduction barbed congruence
by instantiating respectively Definitions 8 and 11 for closed MAs processes, with
the standard notion of strong and weak MAs barb and the GLUX LTS for the
calculus. As shown in [4], the quantification over all contexts can be removed
from the first condition of both definitions.

**Definition 13 (MAs Closed Barbed Semi-Saturated Bisimulation).** *A symmetric relation $\mathcal{R}$ is a MAs closed barbed semi-saturated bisimulation if whenever $P\mathcal{R}Q$ then*

$$
\text{ if } P \downarrow_n \text{ then } Q \downarrow_n;
$$

$$
- \text{ if } P \xrightarrow{C[-]} P' \text{ then } C[Q] \rightsquigarrow Q' \text{ and } P' \mathcal{R} Q'.
$$

A symmetric relation $\mathcal{R}$ is a MAs weak closed barbed semi-saturated bisimula-
tion *if whenever* $P\mathcal{R}Q$ *then*

- if $P \downarrow_n$ then $Q \downarrow_n$;

- if $P \xrightarrow{C[-]} P'$ then $C[Q] \rightsquigarrow^* Q'$ and $P' \mathcal{R} Q'$.

MAs closed barbed semi-saturated bisimilarity $\sim_{\mathcal{M}A\mathcal{s}}^{\mathcal{B}SS}$ and MAs weak closed barbed semi-saturated bisimilarity $\sim_{\mathcal{M}A\mathcal{s}}^{\mathcal{W}BSS}$ are the largest such bisimulations.

**Proposition 3.** *Closed barbed semi-saturated bisimilarity for MAs* $\sim_{\mathcal{M}A\mathcal{s}}^{\mathcal{B}SS}$ *coincides with reduction barbed congruence* $\cong$ *and weak closed barbed semi-saturated bisimilarity* $\sim_{\mathcal{M}A\mathcal{s}}^{\mathcal{W}BSS}$ *coincides with weak reduction barbed congruence* $\cong^S$.

According to Remark 1, the results above subsume the ones presented in [4, Theorem 5], thus providing a labelled characterisation for both congruences $\cong$ and $\cong^W$ via the GIPO LTS.

# 6 Conclusions and Further Works

We introduced the notions of (strong and weak) barbed saturated bisimilarity
for open GRSs, and we showed that it can be efficiently characterized via the
GLUX LTS by employing the semi-saturated game. Moreover, in order to show the adequacy of our proposal, we tested it on ACCS and, most importantly, on MAs. In both cases we proved that the framework captures the standard semantics of these calculi. More precisely, we showed that, for both the strong and the weak variant, the open barbed semi-saturated bisimilarity defined on closed ACCS terms coincides with asynchronous bisimilarity, and that on closed MAs terms it coincides with reduction barbed congruence.

However, albeit we showed that the framework is general enough to capture the abstract semantics of well-known formalisms, it is parametric with respect to the choice of the set of barbs: the choice of the “right” barb is left to the ingenuity of the researcher, and often it is not a trivial task [21,14]. So, it would be interesting to extend our framework by considering an automatically derived notion of barb for (open) GRSs. An alternate route would instead be to abstract away from the use of state predicates by providing an efficient labelled characterization of the barbed semantics, as shown for closed GRSs in [3,5].

Our proposal of a semantics for open GRSs builds on [16]. The authors there study only strong bisimilarity, showing that it is a congruence under rather restrictive conditions, hindering the applicability of the framework. Our work aims at partly solving this problem, in order to relax the conditions for proving a congruence property. However, we did not address the issue of the intrinsic redundancy of the G-lux mechanism: the intertwining of context and instantiation may sometimes end up in the offering of components that are not necessary for the reduction. Consider for example the transition represented by the leftmost G-lux in Fig. 5. It is easy to note that *Q* is not necessary for this reduction, since it appears both in the context on the left and in the instantiation on the right.

Concerning future works, a relatively simpler one should be a comparison with the proposal for parametric rules in GRSs in [10]. A more challenging issue would be to investigate the connections with [2,23]: both works propose a semantic framework for open processes, adopting suitable LTS and alternative behavioural semantics, which is however far removed from the GRSs formalism. In general terms, and stimulated by the latter contributions, we plan to investigate the issue of adequacy for open semantics, and the connection between our proposal and the standard definition of bisimilarity for open terms, considering the standard bisimilarity lifted from closed to open terms by instantiating these ones in all possible ways. It is clear that the latter bisimilarity is included in the former one, and for simpler calculi the two might often coincide. However, the connection between open GRSs and the tile model [12] established in [13] suggests us that the bisimilarity that we obtain is finer, as it is proved already for simple CCS variants and argued for richer calculi in [23,7].

## References

1. Amadio, R., Castellani, I., Sangiorgi, D.: On bisimulations for the asynchronous π-calculus. TCS 195(2), 291–324 (1998)

2. Baldan, P., Bracciali, A., Bruni, R.: A semantic framework for open processes. TCS 389(3), 446–483 (2007)
3. Bonchi, F., Gadducci, F., Monreale, G.V.: On barbs and labels in reactive systems. In: Klin, B., Sobocinski, P. (eds.) SOS 2009. EPTCS, vol. 18, pp. 46–61. EPTCS (2009)

4. Bonchi, F., Gadducci, F., Monreale, G.V.: Reactive systems, barbed semantics, and the mobile ambients. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 272–287. Springer (2009)

5. Bonchi, F., Gadducci, F., Monreale, G.V.: Towards a general theory of barbs, contexts and labels. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 289–304. Springer (2011)

6. Bonchi, F., König, B., Montanari, U.: Saturated semantics for reactive systems. In: LICS 2006. pp. 69–80. IEEE Computer Society (2006)

7. Bruni, R., De Frutos-Escrig, D., Martí-Oliet, N., Montanari, U.: Bisimilarity congruences for open terms and term graphs via tile logic. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 259–274. Springer (2000)

8. Bruni, R., Meseguer, J., Montanari, U.: Symmetric monoidal and cartesian double categories as a semantics framework for tile logic. MSCS 12(1), 53–90 (2002)

9. Cardelli, L., Gordon, A.: Mobile ambients. TCS 240(1), 177–213 (2000)

10. Di Gianantonio, P., Honsell, F., Lenisa, M.: RPO, second-order contexts, and λ-calculus. Logical Methods in Computer Science 5(3) (2009)

11. Fournet, C., Gonthier, G.: A hierarchy of equivalences for asynchronous calculi. JLAP 63(1), 131–173 (2005)

12. Gadducci, F., Montanari, U.: The tile model. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language and Interaction: Essays in Honour of Robin Milner, pp. 133–166. MIT Press (2000)

13. Gadducci, F., Monreale, G.V., Montanari, U.: A modular lts for open reactive systems. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) IFIP TCS. LNCS, vol. 7604, pp. 134–148. Springer (2012)

14. Honda, K., Yoshida, N.: On reduction-based process semantics. TCS 151(2), 437–486 (1995)

15. Kelly, G., Street, R.: Review of the elements of 2-categories. In: Sydney Category Seminar. LNM, vol. 420, pp. 75–103. Springer (1974)

16. Klin, B., Sassone, V., Sobocinski, P.: Labels from reductions: Towards a general theory. In: Fiadeiro, J.L., Harman, N., Roggenbach, M., Rutten, J.J.M.M. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 30–50. Springer (2005)

17. Leifer, J., Milner, R.: Deriving bisimulation congruences for reactive systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 243–258. Springer (2000)

18. MacLane, S.: Categorical algebra. Bull. Amer. Math. Soc. 71, 40–106 (1965)

19. Merro, M., Zappa Nardelli, F.: Behavioral theory for mobile ambients. JACM 52(6), 961–1023 (2005)

20. Milner, R., Sangiorgi, D.: Barbed bisimulation. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 685–695. Springer (1992)

21. Rathke, J., Sassone, V., Sobocinski, P.: Semantic barbs and biorthogonality. In: Seidl, H. (ed.) FoSSaCS 2007. LNCS, vol. 4423, pp. 302–316. Springer (2007)

22. Rathke, J., Sobociński, P.: Deriving structural labelled transitions for mobile ambients. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 462–476. Springer (2008)

23. Rensink, A.: Bisimilarity of open terms. IC 156(1-2), 345–385 (2000)

24. Sassone, V., Sobocinski, P.: Deriving bisimulation congruences using 2-categories. Nordic Journal of Computing 10(2), 163–183 (2003)
# A GIPO and GIPB

The first section of the Appendix recalls the notions of GIPO and GIPB.

**Definition 14 (GRPO, GIPO).** Let the diagrams in Fig. 6 be in a G-category C. A candidate for the diagram (i) is a tuple $\langle a_5, n, o, p, \beta, \gamma, \delta \rangle$ such that $1_h * \gamma \bullet \beta * 1_p \bullet 1_g * \delta = \alpha$. This means that the 2-cells $\gamma, \beta$, and $\delta$, as illustrated in diagram (ii), paste together to give $\alpha$. A groupoidal-relative-pushout (GRPO) is a candidate which satisfies the universal property, i.e., for any other candidate $\langle a_6, n', o', p', \beta', \gamma', \delta' \rangle$ there exists a mediating morphism: a quadruple $\langle q : a_5 \to a_6, \varphi : n' \Rightarrow n; q, \psi : o; q \Rightarrow o', \tau : q; p' \Rightarrow p \rangle$ illustrated in diagrams (iii) and (iv). The equations to be satisfied are $1) \gamma' \bullet \varphi * 1_{p'} \bullet 1_n * \tau = \gamma; 2) 1_o * \tau^{-1} \bullet \psi * 1_{p'} \bullet \delta' = \delta; 3) 1_h * \varphi \bullet \beta * 1_q \bullet 1_g * \psi = \beta'$. Such a mediating morphism must be essentially unique, i.e., for any other mediating morphism $\langle q', \varphi', \psi', \tau' \rangle$ there exists a unique 2-cell $\xi : q \Rightarrow q'$ that makes the two mediating morphisms compatible, i.e., $1) \varphi \bullet 1_n * \xi = \varphi', 2) 1_o * \xi^{-1} \bullet \psi = \psi', \text{ and } 3) \xi * 1_{p'} \bullet \tau' = \tau$.

A square such as diagram (i) of Fig. 6 is called G-idem pushout (GIPO) if $\langle a_4, f, m, id_{a_4}, \alpha, 1_f, 1_m \rangle$ is its GRPO.

<figure><img src="image_8.png" /><figcaption>Fig. 6. GRPO</figcaption></figure>

**Definition 15 (GRPB, GIPB).** Let the diagrams in Fig. 7 be in a G-category C. A candidate for the diagram (i) is a tuple $\langle a_5, n, o, p, \beta, \gamma, \delta \rangle$ such that $\gamma * 1_f \bullet 1_p * \beta * \delta * 1_m = \alpha$. This means that the 2-cells $\gamma, \beta$, and $\delta$, as illustrated in diagram (ii), paste together to give $\alpha$. A groupoidal-relative-pullback (GRPB) is a candidate which satisfies the universal property, i.e., for any other candidate $\langle a_6, n', o', p', \beta', \gamma', \delta' \rangle$ there exists a mediating morphism: a quadruple $\langle q : a_6 \to a_5, \varphi : q; n \Rightarrow n', \psi : q; o \Rightarrow o', \tau : p' ; q \Rightarrow p \rangle$ illustrated in diagrams (iii) and (iv). The equations to be satisfied are $1) \gamma' \bullet 1_{p'} * \varphi^{-1} \bullet \tau * 1_n = \gamma; 2) \tau^{-1} * 1_o \bullet 1_{p'} * \psi \bullet \delta' = \delta; 3) \varphi^{-1} * 1_f \bullet 1_q * \beta \bullet \psi * 1_m = \beta'$. Such a mediating morphism must be essentially unique, i.e., for any other mediating morphism $\langle q', \varphi', \psi', \tau' \rangle$ there exists a unique 2-cell $\xi : q \Rightarrow q'$ that makes the two mediating morphisms compatible, i.e., $1) \varphi \bullet \xi * 1_n = \varphi', 2) \xi^{-1} * 1_o \bullet \psi = \psi', \text{ and } 3) 1_{p'} * \xi \bullet \tau' = \tau$.

A square such as diagram (i) of Fig. 7 is called G-idem pullback (GIPB) if $\langle a_1, h, g, id_{a_1}, \alpha, 1_h, 1_g \rangle$ is its GRPB.
<figure><img src="image_9.png" /><figcaption>Fig. 7. GRPB</figcaption></figure>

B Proof of Proposition 2

We first give an alternate definition of weak open barbed saturated bisimulation.

**Lemma 1 (Revising Barbed Saturation).** A symmetric relation $\mathcal{R}$ is a weak open barbed saturated bisimulation if whenever $p\mathcal{R}q$ then $\forall c, x$

- if $x; p; c \downarrow_o$ then $x; q; c \downarrow_o$;

- if $x; p; c \rightsquigarrow p'$ then $x; q; c \rightsquigarrow q'$ and $p' \mathcal{R} q'$.

Let us now move on to the proof of Proposition 2.

We prove that $\sim^{WOBSS} \subseteq \sim^{W OBS}$ by showing that the closure $\mathcal{S}$ of the weak open barbed semi-saturated bisimilarity with respect to instantiations, contexts and 2-cells $\mathcal{S} = \{\langle u, v \rangle | u \Rightarrow x; p; c, v \Rightarrow x; q; c, p \sim^{WOBSS} q, x \in \mathbf{C}, c \in \mathbf{C}\}$ is a weak open barbed saturated bisimulation according to Lemma 1.

Suppose that $x'; u; c' \downarrow_o$. By hypothesis, bars are respected by 2-cells, therefore $x'; x; p; c; c' \downarrow_o$. Since $p \sim^{WOBSS} q$, then $x'; x; q; c; c' \downarrow_o$ and so $x'; v; c' \downarrow_o$.

Now, assume that $x'; u; c' \rightsquigarrow p'$. Then, $x'; x; p; c; c' \rightsquigarrow p'$. This means that for some $\langle l, r \rangle \in \mathfrak{R}$, $y \in \mathbf{C}$ and $d \in \mathbf{D}$ there exists $\alpha : x'; x; p; c; c' \Rightarrow y; l; d$ (the exterior hexagon of the diagram below) and $p' = y; r; d$.

Since the GRS has G-luxes, we can construct a G-lux as the inner hexagon of the diagram on the right. Thus $p \xrightarrow[c'']{c''} y''; r; d''$ and, since $p \sim^{WOBSS} q$, then $x''; q; c'' \rightsquigarrow q'$ and $y''; r; d'' \sim^{WOBSS} q'$. Since $\mathbf{D}$ is 2-cell closed and composition reflecting, we know that $e$ is reactive, hence $z; x''; q; c''; e \rightsquigarrow z; q'$; $e$. Since $z; x''; q; c''; e \Rightarrow x'; x; q; c$ and $x'; x; q; c' \Rightarrow x'; v; c'$ also $x'; x; q; c' \rightsquigarrow z; q'$; $e$ and $x'; v; c' \rightsquigarrow z; q'$; $e$. Moreover, since $y''; r; d'' \sim^{WOBSS} q'$ and $p' = y; r; d \Rightarrow z; y''; r; d''; e$, we can conclude that $p' \mathcal{S} z; q'; e$.

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

In order to prove that $\sim^{W OBS} \subseteq \sim^{WOBSS}$, it suffices to consider Definition 10 and observe that $x; p; c \downarrow_o$ implies $x; p; c \downarrow_o$ and $p \xrightarrow[x]{c} p'$ implies $x; p; c \rightsquigarrow p'$.