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

HAL
open science

# A behavioural theory for a π-calculus with preorders

Daniel Hirschkoff, Jean-Marie Madiot, Xian Xu

► To cite this version:

Daniel Hirschkoff, Jean-Marie Madiot, Xian Xu. A behavioural theory for a π-calculus with preorders.
2014. hal-00949521

HAL Id: hal-00949521

https://hal.science/hal-00949521

Preprint submitted on 21 Feb 2014

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.

Public Domain
A behavioural theory for a
π-calculus with preorders
(long version)

Daniel Hirschkoff¹, Jean-Marie Madiot¹, and Xian Xu²

¹ ENS Lyon, Université de Lyon, CNRS, INRIA, France,

² East China University of Science and Technology, China

**Abstract.** We study the behavioural theory of πP, a π-calculus featuring restriction as the only binder. In contrast with calculi such as Fusions and Chi, reduction in πP generates a preorder on names rather than an equivalence relation. We present two characterisations of barbed congruence in πP: the first is based on a compositional LTS, and the second is an axiomatisation. The results in this paper bring out basic properties of πP, mostly related to the interplay between the restriction operator and the preorder on names.

# 1 Introduction

The π-calculus expresses mobility via name passing, and has two binders: the input prefix binds the value to be received, and restriction is used to delimit the scope of a private name. The study of Fusions [13], Chi [6], Explicit Fusions [16] and Solos [10] has shown that using restriction as the only binder is enough to express name passing. In such calculi (which, reusing a terminology from [8], we shall refer to as *fusion calculi*), the bound input prefix, $a(x).P$, is dropped in favour of free input, $ab.P$. This yields a pleasing symmetry between input and output prefixes; moreover, one can encode bound input in terms of free input as $(vx)ax.P$.

In [8], the analysis of capability types [14] for fusion calculi has shown that an important modification to existing fusion calculi is necessary in order to be able to define meaningful type systems, beyond the simple discipline of sorting. This has led to the introduction of πP, a π-calculus with preorders. Like existing fusion calculi, πP features restriction as the only binder, and free input and output prefixes. The calculus differs however from existing name-passing calculi. The most important difference is that interaction does not have the effect of equating (or *fusing*) two names, but instead generates an *arc* process, according to the following reduction relation:

$$ \bar{c}a.P \mid cb.Q \rightarrow a/b \mid P \mid Q. $$

The arc $a/b$ expresses the fact that anything that can be done using name $b$ can be done using $a$ as well (but not the opposite): we say that $a$ is *above* $b$. Arcs induce a preorder relation on names, which can evolve along reductions.
Arcs can modify interaction possibilities: in presence of $a/b$, $a$ is above $b$, hence a process emitting on $b$ can also make an output transition along channel $a$. In general, an output on channel $c$ can interact with an input on $d$ provided $c$ and $d$ are joinable, written $c \gamma d$, which means that there is some name that is above both $c$ and $d$ according to the preorder relation To formalise these observations, the operational semantics exploits conditions, which are either of the form $b \le a$ ($a$ is above $b$), or $a \gamma b$ ($a$ and $b$ are joinable).

[8] shows that capabilities make sense in a fusion calculus if preorders replace equivalence relations ('fusions'). Accordingly, [8] presents a type system with input/output types and subtyping for $\pi P$. Name preorders have an impact on how processes express behaviours. It is necessary, beyond types, to understand the consequences of introducing this new construct, whose behaviour does not seem to be reducible to known situations. [8] defines barbed congruence, written $\simeq$, and presents some laws for $\simeq$, suggesting that the behavioural theory of $\pi P$ differs from the one of other fusion calculi. As an illustration, consider the following law, which is valid in $\pi P$ (and in the $\pi$-calculus):

$$ \bar{a}(x).\bar{b}(y).(\bar{x} | y) \simeq \bar{a}(x).\bar{b}(y).(\bar{x}.y + \bar{x}).\bar{x}) $$

$\bar{x}$ (resp. $y$) stands for an output (resp. input) where the value being transmitted is irrelevant. In Fusions, unlike in the $\pi$-calculus, the process that creates successively two fresh names $x$ and $y$ cannot prevent the context from equating ("fusing") $x$ and $y$; hence, in order for the equivalence to hold, it is necessary to add a third summand on the right, $[x = y]\tau$. In $\pi P$ we could program the possibility for the context to equate $x$ and $y$, by changing the continuation process $\bar{x} | y$. This example suggests that $\pi P$ gives a better control on restricted names. (Note that a different approach is adopted in [3,4] to address this question.)

In order to gain a better understanding of such phenomena, the main purpose of the present work is to deepen the study of the behavioural theory of $\pi P$, in an untyped setting. We define a structural Labelled Transition System (LTS) for $\pi P$, and show that the induced notion of bisimilarity, written $\sim$, characterises $\simeq$ (Section 3). It can be noted that [8] presents a characterisation of barbed congruence, using an LTS that is rather ad hoc, because it is based on the definition of the reduction relation. Unlike the latter, the LTS we present here is structural. The LTS reveals interesting aspects of interaction in $\pi P$.

An important observation is related to the interplay between arcs and the restriction operator. It is for instance possible for a process to react to an input offer on some channel, say $c$, without being actually able to perform an output on $c$. This is the case for $P_0 \stackrel{\Delta}{=} (\nu a)(\bar{a}v | a/c)$, as $P_0 | cu$ reduces to $v/u$ ($P_0$ could do an output on $c$ if the arc $a/c$ was replaced with $c/a$). This phenomenon leads to the addition of a new type of labels in the LTS, corresponding to what we call protected actions. As expected, protected actions correspond to observables in the reduction-based semantics supporting the definition of $\simeq$.

Arc processes do not have transitions, but, as mentioned above, they induce conditions involving names, which in turn influence the behaviour of processes. Accordingly, strong bisimilarity, $\sim$, not only tests transitions, but also has a clause to guarantee that related processes entail the same conditions. The LTS
includes a label [$\varphi$]$\tau$, expressing “conditional synchronisation”. [$\varphi$]$\tau$ transitions have a special treatment in the definition of $\sim$.

We provide a second characterisation of barbed congruence, by presenting a set of laws that define an axiomatisation of $\simeq$ (Section 4). Algebraic laws help analysing the behaviour of the constructs of the calculus and their interplay.

We discuss the main ideas in the axiomatisation. In a rather expected way, the prefixes in the calculus correspond to the labels of the LTS. This means in particular that we include prefixes for protected inputs and outputs. One of the salient aspects of the axiomatisation is the existence of a state component in processes, corresponding to the preorder induced by arcs. To manipulate the state component of processes, several laws in the axiomatisation can be used to rewrite prefixes using arcs, which makes it possible to express all transitions induced by a prefixed process. Another set of laws express persistence of the state component in processes (the state can only be extended along computation).

Moreover, the restriction operator prevents the state from being globally shared in general: for instance, in process $P_0$ above, name $a$ can be used instead of $c$, but is only known inside the scope of $(\nu a)$. All in all, the handling of restriction in our axiomatisation requires more care than is usually the case, due to the necessity to express the “view” that subprocesses have on the preorder of names. As we show in Section 4, this has an influence on the overall structure of the presentation of the axiomatisation.

Beyond the LTS and the axiomatisation, which are the main contributions of this paper, we present two results that are related to our study of $\simeq$ in $\pi P$:

- Protected actions can be viewed as cocapabilities, in the sense of capability types. We define an i/o type system with cocapabilities for $\pi P$.

- We show that our approach for the axiomatisation of $\pi P$ can be adapted to provide an axiomatisation of behavioural equivalence for the calculus of Explicit Fusions, which features a fusion construct for processes.

The paper describes our results and sketches the most important proofs. We refer to [9] for a more detailed presentation of the technical details. Related work is discussed along the paper, where it is relevant.

# 2 $\pi P$: Reduction-Based Semantics

## 2.1 The Calculus: Preorders and Processes

We consider a countable set of names $a, b, c, \dots, x, y, \dots$, and define conditions $(\varphi)$, extended names $(\alpha, \beta)$, prefixes $(\pi)$ and processes $(P, Q)$ as follows:

$$ 
\begin{array}{l}
\varphi ::= a \le b \mid a \gamma b \quad \alpha, \beta ::= a \mid \{a\} \quad \pi ::= \alpha(x) \mid \bar{\alpha}(x) \mid [\varphi]\tau \\
P, Q ::= P \mid Q \mid (\nu a)P \mid a/b \mid \sum_{i \in I} \pi_i.P_i
\end{array}
$$

In a sum process, we let $I$ range over a finite set of integers. 0 is the inactive process, defined as the empty sum. We use $S$ to range over sum processes of the form $\sum_i \pi_i.P_i$, and write $\pi.P \in S$ if $\pi.P$ is a summand of $S$. We sometimes
decompose sum processes using the binary sum operator, writing, e.g., $S_1 + S_2$ (in particular, $S + 0 = S$). We abbreviate $\pi.0$ as $\pi$, and write $\alpha(x).P$ simply as $\alpha.P$ when the transmitted name is not relevant, and similarly for $\bar{\alpha}$. $(\nu a)$ binds $a$ in the restricted process, and prefixes $\alpha(x)$ $\bar{\alpha}(x)$ bind $x$ in the continuation process. The set of free names of $P$, $fn(P)$, is defined in the usual way. $P\{b/a\}$ is the process obtained by substituting $a$ with $b$ in $P$, in a capture-avoiding way.

There are two forms of $\varphi$ conditions: $a \leqslant b$ is read “b is above a” and $a \succ b$ is read “a and b are joinable”. In both cases, we have $n(\varphi) = \{a, b\}$. We explain below how we extend relations $\leqslant$ and $\succ$ to extended names. When $n(\varphi) = \{a\}$, we say that $\varphi$ is *reflexive* and we abbreviate $[\varphi]\tau$ as $\tau$. Condition $b \leqslant a$ is ensured by the arc process $a/b$.

In a prefix $\alpha(x)$ or $\bar{\alpha}(x)$, we say that extended name $\alpha$ is in subject position, while $x$ is in object position. As discussed in Section 1, extended names include *protected names*, of the form $\{a\}$, which can be used in subject position only. A prefix of the form $[\varphi]\tau$ is called a *conditional* $\tau$, while other prefixes are called *visible*. Bound and free names for prefixes are given by: $bn([\varphi]\tau) = \emptyset$ and $bn(\alpha(x)) = bn(\bar{\alpha}(x)) = \{x\}$, $fn([\varphi]\tau) = n(\varphi)$, $fn(\alpha(x)) = fn(\bar{\alpha}(x)) = n(\bar{\alpha})$ with $n(a) = n(\{a\}) = \{a\}$.

We use an overloaded notation, and define processes representing conditions:

$$a \succ b \triangleq (\nu u)(u/a \mid u/b) \qquad a \leqslant b \triangleq b/a.$$

$\Gamma$ ranges over sets of at most two conditions. We define $\Gamma \vdash \varphi$, meaning that $\Gamma$ implies $\varphi$, and $P \succ \Gamma$, meaning that $P$ entails $\varphi$ for all $\varphi \in \Gamma$:

$$\frac{\vdash\text{-REFL}}{\Gamma \vdash a \leqslant a} \qquad \frac{\vdash\text{-IN}}{\varphi \in \Gamma} \qquad \frac{\vdash\text{-MIRROR}}{\Gamma \vdash b \succ a} \qquad \frac{\vdash\text{-TRANS}}{\Gamma \vdash a \leqslant b} \qquad \frac{\vdash\text{-JOIN}}{\Gamma \vdash a \leqslant b} \qquad \frac{\vdash\text{-EXTJOIN}}{\Gamma \vdash a \leqslant b}$$

$$\frac{\triangleright\text{-ARC}}{a/b \triangleright b \leqslant a} \qquad \frac{\triangleright\text{-COMBINE}}{P \triangleright \Gamma} \qquad \frac{\triangleright\text{-PAR-L}}{\Gamma \triangleright \varphi} \qquad \frac{\triangleright\text{-PAR-R}}{P \mid Q \triangleright \varphi} \qquad \frac{\triangleright\text{-RES}}{P \mid Q \triangleright \varphi} \qquad \frac{P \triangleright \varphi}{(\nu a) P \triangleright \varphi} \quad a \notin n(\varphi)$$

As an example, the reader might check that $(\nu u)(u/a \mid u/b) \mid b/c \succ a \succ c$.

**Notation 1** We write $\Phi(P) = \{\varphi \mid P \succ \varphi\}$ the set of conditions entailed by $P$.

## 2.2 Reduction Semantics and Barbed Congruence

**Definition 1.** Structural congruence, written $\equiv$, is the smallest congruence satisfying $\alpha$-conversion for restriction, and the following axioms:

$$P \mid 0 \equiv P \qquad (P \mid Q) \mid R \equiv P \mid (Q \mid R) \qquad P \mid Q \equiv Q \mid P$$

$$(\nu a)0 \equiv 0 \qquad (\nu c)(\nu d)P \equiv (\nu d)(\nu c)P \qquad (\nu a)(P \mid Q) \equiv (\nu a)P \mid Q \text{ if } a \notin fn(Q)$$

$$\sum_{i \in I} \pi_i.P_i \equiv \sum_{i \in I} \pi_{\sigma(i)} \cdot P_{\sigma(i)} \quad \sigma \text{ a permutation of } I$$
Relations ≡ and ▷ are used to define the reduction of processes. We rely on ▷ to infer that two processes interact on joinable (extended) names. This allows us to introduce reduction-closed barbed congruence, along the lines of [8].

**Definition 2 (Reduction).** $\mapsto$ is the relation defined by the following rules:
(we write $\equiv \mapsto \equiv$ for relation composition):

$$ \frac{\bar{\alpha}(x).P \in S_1 \quad \beta(y).Q \in S_2 \quad R \triangleright \alpha \gamma \beta \quad x \neq y}{R | S_1 | S_2 \mapsto R | (\nu xy)(x/y | P | Q)} \qquad \begin{array}{l} a \gamma \{b\} = \{b\} \gamma a = a \leq b \\ \{a\} \gamma \{b\} = \text{undefined} \end{array} $$

We choose as in [8] a generic definition of barbs, uniform over usual process calculi, instead of the more syntactic characterisation.

**Definition 3 (Barbs).** The barb $\downarrow \bar{a}$ holds for a process $P$ if $P | a(x).\omega \mapsto P'$, where $P'$ is a process in which $\omega$ is unguarded, and $\omega$ is a special name that does not appear in $P$. We define similarly the barb $\downarrow a$, using the tester $\bar{a}(x).\omega$.

**Definition 4.** Barbed congruence is the largest congruence $\simeq$ satisfying:

- if $P \downarrow_a$ and $P \simeq Q$ then $Q \downarrow_a$, and similarly for $\downarrow \bar{a}$, and

- if $P \mapsto P'$ and $P \simeq Q$ then for some $Q'$, $P' \simeq Q'$ and $Q \mapsto Q'$.

The remainder of the paper is devoted to the presentation of two characterisations of $\simeq$. We first comment on the definition of $\pi P$ given above.

[8] discusses an alternative version of reduction, called “eager”, where arcs can rewrite prefixes, yielding, e.g., $d/c | c(x).P \mapsto d/c | d(x).P$. [8] explains why the present semantics is more compelling (for instance $a(x).a(y)$ would not be equivalent to $a(x) | a(y)$ in the eager version).

Our calculus lacks prefixes for free input and output. These can be encoded using bound prefixes, as follows (name $x$ is chosen fresh):

$$ [ab.P] \stackrel{\Delta}{\equiv} (\nu x)a(x).(P | x/b) \qquad [\bar{a}b.P] \stackrel{\Delta}{\equiv} (\nu x)\bar{a}(x).(P | b/x). $$

In a calculus having both kind of prefixes, we could show that the above encoded processes behave like primitive free prefixes.

Moreover, it is possible to encode protected prefixes, as follows ($u$ is fresh):

$$ [{\bar{a}}(x).P] \stackrel{\Delta}{\equiv} (\nu u)(u/a | \bar{u}(x).P) \qquad [{a}(x).P] \stackrel{\Delta}{\equiv} (\nu u)(u/a | u(x).P). $$

**Remark 5 (Comparison with [8]).** Unlike the version of $\pi P$ presented in [8], our calculus has sum and primitive bound prefixes. Including such constructs is customary when studying axiomatisations (bound prefixes are often present as soon as the calculus has restriction — see e.g. [12,15]). We also have primitive protected prefixes, to make the technical development of Section 4 simpler. As discussed above, these are encodable in $\pi P$. The same holds for free prefixes, which are not included in the syntax. An LTS for $\pi P$ based on free prefixes is definable, at the cost of a more complex technical development [9].
# 3 A Labelled Transition System for $\pi P$

## 3.1 LTS and Bisimilarity

The LTS defines transitions $P \xrightarrow{\mu} P'$, where the grammar for the labels, $\mu$, is the same as the one for prefixes $\pi$. We comment on the rules, given on Figure 1.

The first two rules correspond to the firing of visible prefixes. The transition involves a fresh name $x$, upon which the participants in a communication “agree”. Name $y$ remains local, via the installation of an arc, according to the directionality of the prefix. (Adopting a rule with no arc installation would yield a more complex definition of $\sim$). The rule for the $[\varphi]\tau$ prefix is self explanatory. The rule describing communication follows the lines of the corresponding rule for $\mapsto$; no arc is installed (but arcs are introduced in the prefix rules).

The three rules mentioning $\triangleright$ are called *preorder rules*. The two preorder rules for visible actions exploit $\leqslant$, which is defined for extended names (as we did for $\Upsilon$ above). Note that the condition involving $\triangleright$ is *the same* in these two rules. For instance, if $P \xrightarrow{a(x)} P'$ and $P \triangleright a \leqslant c$, we can derive $P \xrightarrow{c(x)} P'$. In this case, $P \triangleright a \leqslant \{c\}$ is also derivable, hence $P \xrightarrow{[c](x)} P'$. We can also check that $P_0$ from Section 1 satisfies $P_0 \xrightarrow{[c](x)}$, because $\bar{a}v \mid a/c \triangleright c \Upsilon a$ (and hence $a \leqslant \{c\}$).

The other preorder rule can be used to modify conditional $\tau$s involved in a transition. As an example, let $P_1 \triangleq (\bar{a}(x).Q \mid n/u) \mid (u(y).R \mid n/a)$. Process $P_1$ can perform a $\tau$ transition: the two arcs can, intuitively, let the output at $a$ and the input at $u$ interact at name $n$. Technically, this can be derived by inferring a $\xrightarrow{[a\Upsilon u]\tau}$ transition (from the output on the left and the input on the right). The latter can then be turned into a $\tau$ transition, exploiting the fact that *the whole process* entails $a \Upsilon u$. Finally, the congruence rules are as expected.

**Definition 6** ($\sim$). A symmetric relation $\mathcal{R}$ is a bisimulation if $P \mathcal{R} Q$ implies:

- If $P \triangleright \varphi$ then $Q \triangleright \varphi$.

- If $P \xrightarrow{\alpha(x)} P'$, with $x \notin \text{fn}(Q)$, then there is $Q'$ such that $Q \xrightarrow{\alpha(x)} Q'$ and $P' \mathcal{R} Q'$; we impose the same condition with $\bar{\alpha}$ instead of $\alpha$.

- If $P \xrightarrow{[\varphi]\tau} P'$ then there is $Q'$ such that $Q \xrightarrow{[\varphi]\tau} Q'$ and $P' \mid \varphi \mathcal{R} Q' \mid \varphi$.

Bisimilarity, written $\sim$, is the greatest bisimulation.

This definition is reminiscent of the efficient bisimulation from [16]. Note in particular the necessity to add $\varphi$ in parallel in the $\xrightarrow{[\varphi]\tau}$ case.

## 3.2 The Characterisation Theorem

**On the $\vdash^i$ relation** We define below $\vdash^i$, an atomic decomposition of $\vdash$ to be able to easily work proof inductions. The idea is that $\Gamma \vdash \varphi$ is equivalent to $\psi \vdash^i \psi_1 \circ \dots \circ \vdash^i \psi_n \varphi$ for some reflexive $\psi$ and for some $\psi_1, \dots, \psi_n \in \Gamma$, where $\vdash^i \psi$ is the relation $\{ (\varphi, \zeta) \mid \varphi, \psi \vdash \zeta \}$.
<figure><img src="image_2.png" /><figcaption>**Fig. 1.** LTS for $\pi_P$. Symmetric versions of the two rules involving $|$ are omitted.</figcaption></figure>

**Definition 7.** The predicate $\varphi_1, \varphi_2 \vDash \varphi_3$ is defined as follows:

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

Note that the second line is the symmetric variant of the first.

**Lemma 8.** If $\varphi_1, \varphi_2 \vDash \varphi$ and $\varphi_{21}, \varphi_{22} \vDash \varphi_2$ then there exists $\varphi'$ such that either:

- $\varphi_1, \varphi_{21} \vDash \varphi'$ and $\varphi', \varphi_{22} \vDash \varphi$, or

- $\varphi_1, \varphi_{22} \vDash \varphi'$ and $\varphi', \varphi_{21} \vDash \varphi$.

*Equivalent formulation:* if $\varphi_{21}, \varphi_{22} \vDash \varphi_2$ then $\varphi_2 \vDash \varphi_2 \subseteq (\varphi_2 \vDash \varphi_1 \cup \varphi_2 \vDash \varphi_2)$.

*Proof.* Finite and exhaustive case analysis on the premises; the proof has been mechanized.

The relations $\vdash$ and $\vDash$ mean the same:

**Lemma 9.** If $\Gamma \vdash \varphi$ then $\varphi \vDash \varphi_1 \dots \varphi_n \vDash \zeta$ for some $\psi_1, \dots, \psi_n \in \Gamma$ and some reflexive $\zeta$.

*Proof.* By induction on $\Gamma \vdash \varphi$. Lemma 8 provides us with a helpful notion of composability that covers the rules $\vdash$-TRANS, $\vdash$-JOIN, $\vdash$-EXTJOIN. $\square$

**Corollary 10.** If $\varphi_1, \varphi_2 \vDash \varphi_3$ then $\varphi_1, \varphi_2 \vdash \varphi_3$. Conversely, if $\Gamma \vdash \varphi$ then $\varphi \vDash \psi_1 \dots \vDash \psi_n \varphi$ for some reflexive $\psi$ and for some $\psi_1, \dots, \psi_n \in \Gamma$.
*Proof.* The first part is trivial: each rule for $\vdash^i$ is simulated by (three) rules for $\vdash$. The second part follows from Lemma 9.

**Notation 2** We write $\varphi_1 \vdash^i \varphi_2 \varphi_3$ whenever $\varphi_1, \varphi_2 \vdash^i \varphi_3$ and we write $\vdash^i_P$ for the union of all $\vdash^i_\varphi$ for $P \triangleright \varphi$.

Intuitively, $\vdash^i_P$ denotes all the implications between conditions that hold because of the conditions that are entailed by process $P$ in one step.

**Lemma 11.** $\vdash^i_{P|Q} \subseteq (\vdash^i_P \cup \vdash^i_Q)^*$.

*Proof.* We write $\mathcal{R}$ for the relation $\vdash^i_P \cup \vdash^i_Q$. We prove by induction on $P \mid Q \triangleright \varphi_2$ that for all $\varphi_1$ and $\varphi_3$, if $\varphi_1, \varphi_2 \vdash^i \varphi_3$ then $\varphi_1 \mathcal{R}^* \varphi_3$. There are three cases. For $\triangleright$-PAR-L we know that $P \triangleright \varphi_2$ so $\varphi_1 \vdash^i_P \varphi_3$ and for $\triangleright$-PAR-R we get the same way $\varphi_1 \vdash^i_Q \varphi_3$. The case for the rule $\triangleright$-COMBINE is handled using Lemma 9. $\square$

**Lemma 12.** If $\varphi_1(\vdash^i_P)^* \varphi_3$ then $\varphi_1 \vdash^i_P \varphi_2 \vdash^i_P \varphi_3$ for some $\varphi_2$ such that $\mathfrak{n}(\varphi_2) \subseteq \mathfrak{n}(\varphi_1) \cup \mathfrak{n}(\varphi_3)$.

*Proof.* (Sketch). Suppose $\varphi_1 \vdash^i_P \dots \vdash^i_P \varphi_3$. One obtains $\varphi_3$ from $\varphi_1$ by appending $\psi$'s such that $P \triangleright \psi$ at the left or at the right of $\varphi_1$. We can in fact append all left $\psi$s at first (an operation that can be done in one $\vdash_P$ step), and once it is done, appending all right $\psi$s (the other $\vdash_P$ step).

**Lemma 13.** Suppose $\varphi_1 \vdash_P^* \varphi_4$ and $\mathfrak{n}(\varphi_i) = \{a_i, b_i\}$. For some $\varphi_2$ and $\varphi_3$ we have $\varphi_1 \vdash_P \varphi_2 \vdash_P \varphi_4$ and $\varphi_1 \vdash_P \varphi_3 \vdash_P \varphi_4$ such that $\mathfrak{n}(\varphi_2) = \{a_1, b_4\}$ and $\mathfrak{n}(\varphi_3) = \{a_4, b_1\}$.

*Proof.* As in the proof of Lemma 12, but we care about whether we do left-right or right-left.

**Lemma 14.** If $0 \triangleright \varphi$ then $\varphi$ is reflexive, and for all $P, P \triangleright \varphi$.

*Proof.* By induction on the derivation of $0 \triangleright \varphi$: the only possible rule is $\triangleright$-COMBINE, which can apply for $P$ as well as for $0$.

**Lemma 15.** If $P \triangleright \varphi$ and there is $a \in \mathfrak{n}(\varphi) \setminus \text{fn}(P)$, then $\varphi$ is reflexive.

*Proof.* We prove by induction on the derivation of $P \triangleright \varphi$ that $\mathfrak{n}(\varphi) = \{a\}$ for each of those $\varphi$. We have only one interesting case, for the $\triangleright$-COMBINE rule: $P \triangleright \varphi_1, \dots, P \triangleright \varphi_n$ and $\varphi_1, \dots, \varphi_n \vdash \varphi$. We can suppose w.l.o.g. that $\Gamma$ only contains $\varphi$s that have been effectively used by one of the rules for $\vdash$.

By induction hypothesis, each time $a$ appear in a $\varphi_i$, $\mathfrak{n}(\varphi_i) = \{a\}$. Hence, as each rule for $\vdash$ propagates $a$ into each premise, it will be the same for all the premises, leading at the end to the fact all $\varphi_i$ are reflexive for $a$, and hence $\mathfrak{n}(\varphi) = \{a\}$. $\square$

A context $C$ is a process with one occurrence of the hole; replacing the hole with $P$ yields a process written $C[P]$.
**Lemma 16.** If $\Phi(P) \subseteq \Phi(Q)$ then $\Phi(C[P]) \subseteq \Phi(C[Q])$.

*Proof.* By induction on $C[P] \triangleright \varphi'$ we prove $C[Q] \triangleright \varphi'$, the case for $\triangleright$-COMBINE is trivial. In all other cases we make a straightforward case analysis on $C$: it cannot be a sum, and if it is $C' \mid R$ with the rule $\triangleright$-PAR-L (or $R \mid C'$ with $\triangleright$-PAR-R, or $\nu a C'$ with $\triangleright$-RES) then the induction hypothesis is enough. It is immediate if $C = C' \mid R$ with the rule $\triangleright$-PAR-R (or $R \mid C'$ with $\triangleright$-PAR-L), and if $C = []$ then we use $P \triangleright \varphi \Rightarrow Q \triangleright \varphi$.

**Lemma 17.** If $P \triangleright \varphi$ then $\Phi(P \mid \varphi) = \Phi(P)$.

*Proof.* By induction on a derivation of $P \mid \varphi \triangleright \psi$ for any $\psi$, we prove $P \triangleright \psi$. The $\triangleright$-PAR-L case is trivial, the $\triangleright$-PAR-R case uses the fact $P \triangleright \psi$, and the $\triangleright$-COMBINE case is trivial.

**Lemma 18.** If $P \equiv Q$ and $P \triangleright \varphi$ then $Q \triangleright \varphi$.

*Proof.* We prove by induction on the derivation of $P \equiv Q$ that $\Phi(P) = \Phi(Q)$; this generalisation is necessary because symmetry is among the axioms of $\equiv$.

In most cases of this induction – the main exceptions being the first two items below – we prove that $\forall \varphi, P \triangleright \varphi \Rightarrow Q \triangleright \varphi$ and $\forall \varphi, Q \triangleright \varphi \Rightarrow P \triangleright \varphi$ separately, using an induction on the judgement $\dashv \triangleright \varphi$. The case for $\triangleright$-COMBINE is immediate so we focus on when the last rule is another one.

1. The congruence rule is handled using Lemma 16.

2. The equivalence rules follow from the fact that $\Leftrightarrow$ is itself an equivalence.

3. $P \mid 0 \equiv P$: the induction on $P \mid 0 \triangleright \varphi$ goes as follows: each $\triangleright$-PAR-L rule is removed, and each $\triangleright$-PAR-R rule is replaced by a proof of $0 \triangleright \varphi \Rightarrow P \triangleright \varphi$ (Lemma 14).

4. $P \equiv P \mid 0$: no induction needed, only an application of $\triangleright$-PAR-L.

5. $(P \mid Q) \mid R \equiv P \mid (Q \mid R)$: the last rule is $\triangleright$-PAR-R or $\triangleright$-PAR-L. In the former case, we know $R \triangleright \varphi$ so two applications of $\triangleright$-PAR-R are needed to prove $P \mid (Q \mid R) \triangleright \varphi$. In the case of rule $\triangleright$-PAR-R, we have $P \mid Q \triangleright \varphi$; we perform another induction on $P \mid Q \triangleright \varphi$ to establish $P \mid (Q \mid R) \triangleright \varphi$.

6. $P \mid (Q \mid R) \equiv (P \mid Q) \mid R$: similar proof.

7. $P \mid Q \equiv Q \mid P$: the last rule is either $\triangleright$-PAR-L ($P \triangleright \varphi$) or $\triangleright$-PAR-R ($Q \triangleright \varphi$), and we apply respectively $\triangleright$-PAR-R or $\triangleright$-PAR-L.

8. $Q \mid P \equiv P \mid Q$: same proof.

9. $(\nu a)P \equiv (\nu b)P\{b/a\}$ when $b \notin \text{fn}(P)$: the last rule, and the one we apply, is $\triangleright$-RES and we end up proving that if $P \triangleright \varphi$ then $P\{b/a\} \triangleright \varphi$ when $a, b \notin \mathfrak{n}(\varphi)$. More generally we can prove $P \triangleright \varphi \Rightarrow P_\sigma \triangleright \varphi_\sigma$ for all (even non injective) substitution $\sigma$ since $\triangleright$ and $\vdash$ are oblivious to substitutions.

10. $(\nu b)P\{b/a\} \equiv (\nu a)P$: similar proof.

11. $(\nu ab)P \equiv (\nu ba)P$: the last rule is $\triangleright$-RES. We know $(\nu b)P \triangleright \varphi$ with $a \notin \mathfrak{n}(\varphi)$. By induction on $(\nu b)P \triangleright \varphi$ we can prove $P \triangleright \varphi$, from which we can get $(\nu a)P$ and then $(\nu ba)P$.

12. $(\nu ba)P \equiv (\nu ab)P$: same proof.
13. $(\nu aP) \mid Q \equiv \nu a(P \mid Q)$ with $a \notin \mathrm{fn}(Q)$. If the last rule is $\triangleright$-PAR-R, coming from $Q \triangleright \varphi$, in which case we conclude easily. If the last rule is $\triangleright$-PAR-L, coming from $\nu aP \triangleright \varphi$, we get $P \triangleright \varphi$ (like in the proof of the previous case) from which $(\nu a)(P \mid Q) \triangleright \varphi$ follows. It is worth noting that if $a \in \mathfrak{n}(\varphi)$, $\varphi$ must be trivial ($a \triangleright a$ or $a \leqslant a$).

14. $\nu a(P \mid Q) \equiv (\nu aP) \mid Q$ with $a \notin \mathrm{fn}(Q)$. This is the most difficult case in the proof of the present lemma. Intuitively, we need to put together all contributions from $P$ so that they are independent of $Q$. First, as before, from $\nu a(P \mid Q) \triangleright \varphi$ we get $P \mid Q \triangleright \varphi$.

We treat the case where $\varphi = b_0 \triangleright c_0$ (the cases $b_0 \leqslant c_0$ and $c_0 \leqslant b_0$ are simpler). The derivation of $P \mid Q \triangleright \varphi$ at hand is built up using a certain number of instances of rule $\triangleright$-COMBINE involving processes $P$ and $Q$, which we summarise as follows: there exist names $b_0, \dots, b_n$ and $c_0, \dots, c_m$ such that:

- either $P \triangleright b_n \triangleright c_m$ or $Q \triangleright b_n \triangleright c_m$;

- $b_i \leqslant b_{i+1}$ is derived from $P$ or $Q$, i.e. either $P \triangleright b_i \leqslant b_{i+1}$ or $Q \triangleright b_i \leqslant b_{i+1}$, and the same holds for $c_j \leqslant c_{j+1}$.

We show that we can construct a derivation where name $a$ is not used, which means that we eliminate occurrences of $a$ in the $b_i$s and the $c_j$s. For this, we proceed as follows:

(a) we replace every derivation of the shape $Q \triangleright \gamma$, where $\gamma$ is a formula involving the $b_i$s or the $c_j$s, and $a \in \mathfrak{n}(\gamma)$, with a derivation of $P \triangleright \gamma$: this is possible thanks to Lemma 15 (because $a \notin \mathrm{fn}(Q)$, so $\gamma$ must be reflexive).

We obtain this way the property that whenever $Q \triangleright \gamma$ for some $\gamma$ involving the $b_i$s or the $c_j$s, $a \notin \mathfrak{n}(\gamma)$.

(b) Therefore, if $b_i = a$ for some $i$, we have $i > 0$ since $a \notin \mathfrak{n}(\phi)$, and $P \triangleright b_{i-1} \leqslant b_i = a$.

If $i < n$, we also have $P \triangleright a \leqslant b_{i+1}$, which allows us to deduce, using rule $\triangleright$-COMBINE, $P \triangleright b_{i-1} \leqslant b_{i+1}$. We thus got rid of an occurrence of $a$ in the $b_i$s.

If $i = n$, since $P \triangleright b_n \triangleright c_m$ and $a = b_n$, we deduce $P \triangleright b_{n-1} \triangleright c_m$. Also in this case, we got rid of an occurrence of $a$ in the $b_i$s.

(c) We proceed like this as long as $a$ appears in the $b_i$s, and do the same to get rid of all occurrences of $a$ among the $c_j$s.

We are thus left with a set of formulas $\gamma$ such that: (i) either $P \triangleright \gamma$ or $Q \triangleright \gamma$, and (ii) $a \notin \mathfrak{n}(\gamma)$. Moreover, these formulas can be combined to yield $\varphi = b_0 \triangleright c_0$. Whenever we have a derivation of $P \triangleright \gamma$, we can use rule $\triangleright$-RES to obtain a derivation of $(\nu a)P \triangleright \gamma$. We then transform all derivations of formulas from either $(\nu a)P$ or $Q$ into the corresponding derivation from $(\nu a)P \mid Q$, using either rule $\triangleright$-PAR-L or $\triangleright$-PAR-R.

We conclude by applying rule $\triangleright$-COMBINE $n + m$ times, to finally derive $(\nu a)P \mid Q \triangleright \varphi$.

This concludes the induction on the derivation of $P \equiv Q$. $\square$

<figure><img src="image_4.png" /></figure>
**Definition 19.** We define a relation $\sqsubseteq^\varphi$ between labels as follows: (i) $\alpha_1(x) \sqsubseteq^\varphi \alpha_2(x)$ and $\bar{\alpha}_1(x) \sqsubseteq^\varphi \bar{\alpha}_2(x)$ when $\varphi = \alpha_2 \le \alpha_1$, and (ii) $[\varphi_1]\tau\sqsubseteq^\varphi[\varphi_2]\tau$ when $\varphi_1, \varphi \vdash \varphi_2$. We write $\sqsubseteq_P$ for the smallest preorder containing all $\sqsubseteq^\varphi$ when $P \triangleright \varphi$.

**Lemma 20.** If $\varphi_1, \varphi_2 \vdash \varphi_3$ then $(\sqsubseteq^{\varphi_3}) \subseteq (\sqsubseteq^{\varphi_1} \sqsubseteq^{\varphi_2}) \cup (\sqsubseteq^{\varphi_2} \sqsubseteq^{\varphi_1})$.

*Proof.* We suppose $\mu\sqsubseteq^{\varphi_3}\mu'$. If $\mu$ is a conditional $\tau$, Lemma 8 is enough to conclude. Otherwise, we make an exhaustive case analysis on $\varphi_1, \varphi_2 \vdash \varphi_3$ and $\sqsubseteq^{\varphi_3}$, there a quite a few, but easy, cases. The proof has been mechanized, but we write below the main cases after removing some symmetric cases.

1. $a \le b, b \le c \vdash a \le c$: from $\mu\sqsubseteq^{a\le c}\mu'$ we know that either (we ignore when $\mu, \mu'$ are output labels, we also write $\{a\}$ instead of $\{a\}(x)$):

$$ \begin{array}{lclcl} c & \sqsubseteq^{a\le c} & a & \rightsquigarrow & c & \sqsubseteq^{b\le c} \\ \{a\} & \sqsubseteq^{a\le c} & \{c\} & \rightsquigarrow & \{a\} & \sqsubseteq^{a\le b} \\ \{c\} & \sqsubseteq^{a\le c} & a & \rightsquigarrow & \{c\} & \sqsubseteq^{b\le c} \\ \{a\} & \sqsubseteq^{a\le c} & c & \rightsquigarrow & \{a\} & \sqsubseteq^{a\le b} \\ & & & & \{b\} & \sqsubseteq^{b\le c} \\ & & & & \{b\} & \sqsubseteq^{b\le c} \end{array} $$

2. $a \le c, b \le c \vdash a \gamma b$:

$$ \begin{array}{lclcl} \{a\} & \sqsubseteq^{a\gamma b} & b & \rightsquigarrow & \{a\} & \sqsubseteq^{a\le c} \\ \{b\} & \sqsubseteq^{a\gamma b} & a & \rightsquigarrow & \{b\} & \sqsubseteq^{b\le c} \end{array} $$

3. $a \gamma b, c \le a \vdash c \gamma b$:

$$ \begin{array}{lclcl} \{c\} & \sqsubseteq^{c\gamma b} & b & \rightsquigarrow & \{c\} & \sqsubseteq^{c\le a} \\ \{b\} & \sqsubseteq^{c\gamma b} & c & \rightsquigarrow & \{b\} & \sqsubseteq^{a\gamma b} \end{array} $$

4. $a \gamma b, c \le b \vdash a \gamma c$:

$$ \begin{array}{lclcl} \{c\} & \sqsubseteq^{a\gamma c} & a & \rightsquigarrow & \{c\} & \sqsubseteq^{c\le b} \\ \{a\} & \sqsubseteq^{a\gamma c} & c & \rightsquigarrow & \{a\} & \sqsubseteq^{a\gamma b} \end{array} $$

**Lemma 21.** $\sqsubseteq_P \sqsubseteq_Q \subseteq (\sqsubseteq_P \cup \sqsubseteq_Q)^*$.

*Proof.* By definition we know that $\mu\sqsubseteq^\varphi\mu'$ for some $\varphi$ such that $P \mid Q \triangleright \varphi$. First, remark that the cases mirror $(a \gamma b\sqsubseteq^\varphi b \gamma a)$ and discard $(\psi\sqsubseteq^\varphi\psi)$ are handled immediately.

There exists a trivial $\psi$ such that $\psi \vdash_P \mid_Q \varphi$. By Lemma 11 we know that $\vdash_P \mid_Q \subseteq (\vdash_P \cup \vdash_Q)^*$, namely there is a sequence $\zeta_1, \zeta_2, \dots, \zeta_n$ (with $\psi = \zeta_1$ and $\varphi = \zeta_n$) such that $\zeta_1 \vdash_{R_1} \dots \zeta_{n-1} \vdash_{R_{n-1}} \zeta_n$ with $R_i \in \{P, Q\}$. Since $\zeta_i \vdash_{R_i} \zeta_{i+1}$ we know that $\sqsubseteq^{\zeta_{i+1}} \subseteq (\sqsubseteq^{\zeta_i} \cup \sqsubseteq_{R_i})^*$ by Lemma 20.

We write $\mathcal{R}$ for $\sqsubseteq_P \cup \sqsubseteq_Q$. Hence $\sqsubseteq^{\zeta_i} \subseteq \mathcal{R}^*$ implies $\sqsubseteq^{\zeta_{i+1}} \subseteq \mathcal{R}^*$, since $\sqsubseteq_{R_i} \subseteq \mathcal{R}$. Since $\psi$ is trivial $\sqsubseteq^\zeta = \sqsubseteq^\psi \subseteq \sqsubseteq_P$, we conclude by induction on $n$: $\sqsubseteq^\zeta = \sqsubseteq^\varphi \subseteq \mathcal{R}^*$.

*Proof.* This breaks into proofs of $\vdash_P \mid_Q \subseteq (\vdash_P \cup \vdash_Q)^*$ where $\vdash_R$ is the relation $\{(\varphi_1, \varphi_3) | \varphi_1, \varphi_2 \vdash \varphi_3, R \triangleright \varphi_2\}$ and of $\varphi_1 \vdash_R \varphi_3$ implies $\sqsubseteq^{\varphi_3} \subseteq (\sqsubseteq^{\varphi_1} \cup \sqsubseteq_R)^*$. $\square$
**Lemma 22 (Composition of extended $\leq$ and $\gamma$).** On extended names, $\leq$ is transitive and $\gamma$ can be extended on the left (or on the right), but cannot in general be derived from $\leq$.

1. If $\alpha \leq \beta$ and $\beta \leq \gamma$ are defined, so is $\alpha \leq \gamma$ and $\alpha \leq \beta$, $\beta \leq \gamma \vdash \alpha \leq \gamma$.

2. If $\alpha \leq \beta$ and $\beta \gamma$ $\gamma$ are defined, so is $\alpha \gamma$ $\gamma$ and $\alpha \leq \beta$, $\beta \gamma \vdash \alpha \gamma$.

3. In general $\alpha \leq \beta$ and $\gamma \leq \beta$ do not imply $\alpha \gamma$.

*Proof.* The first two items need a careful case analysis:

1. to prove $\alpha \leq \beta$, $\beta \leq \gamma \vdash \alpha \leq \gamma$, we have four cases for $\alpha, \beta, \gamma$:

(a) $a, b, c$: then $a \leq b, b \leq c \vdash a \leq c$ by transitivity of $\leq$,

(b) $a, b, \{c\}$: then $a \leq b, b \gamma \vdash a \gamma c$ by left extension of $\gamma$,

(c) $a, \{b\}, \{c\}$: then $a \gamma b, c \leq b \vdash a \gamma c$ by right extension of $\gamma$,

(d) $\{a\}, \{b\}, \{c\}$: then $b \leq a, b \leq c \vdash c \leq a$ by transitivity of $\leq$.

2. to prove $\alpha \leq \beta$, $\beta \gamma \vdash \alpha \gamma$, we have 4 well-defined cases for $\alpha, \beta, \gamma$:

(a) $a, b, c$: then $a \leq b, b \gamma \vdash a \gamma c$ by left extension of $\gamma$,

(b) $a, b, \{c\}$: then $a \leq b, b \leq c \vdash a \leq c$ by transitivity of $\leq$,

(c) $a, \{b\}, c$: then $a \gamma b, c \leq b \vdash a \gamma c$ by right extension of $\gamma$,

(d) $a, \{b\}, \{c\}$: impossible since $\{b\} \gamma \{c\}$ is undefined,

(e) $\{a\}, b, c$: impossible since $\{a\} \leq b$ is undefined,

(f) $\{a\}, b, \{c\}$: impossible since $\{a\} \leq b$ is undefined,

(g) $\{a\}, \{b\}, c$: then $b \leq a, c \leq b \vdash c \leq a$ by transitivity of $\leq$,

(h) $\{a\}, \{b\}, \{c\}$: impossible since $\{b\} \gamma \{c\}$ is undefined.

And finally a counterexample for (3) is when $\alpha = \beta = \gamma = \{a\}$ since we always have $\{a\} \leq \{a\}$ but $\{a\} \gamma \{a\}$ is undefined. $\square$

**Corollary 23.** If $\alpha(x) \sqsubseteq_P \alpha_1(x)$ and $\alpha \gamma \beta$ is defined, then $\alpha_1 \gamma \beta$ is defined and $[\alpha \gamma \beta] \tau \sqsubseteq_P [\alpha_1 \gamma \beta] \tau$.

*Proof.* Remark that $\alpha(x) \sqsubseteq_P \alpha_1(x)$ is equivalent to $P \triangleright \alpha_1 \leq \alpha$ and by definition of $\sqsubseteq_P$, it is enough to prove $\alpha \gamma \beta$, $\alpha_1 \leq \alpha \vdash \alpha_1 \gamma \beta$ which is an instance of the Lemma 22.

*Remark 24.* For visible labels, $\sqsubseteq_P$ needs to be closed neither by transitivity nor by reflexivity, as the first item of Lemma 22 indicates.

**Lemma 25.** If $A \triangleright \varphi$ and $A$ is a parallel composition of preorder processes, then there are some $\varphi_1, \dots, \varphi_n \in A$ and a reflexive $\psi$ such that $\sqsubseteq^\varphi = \sqsubseteq^\psi \sqsubseteq^\varphi_1 \dots \sqsubseteq^\varphi_n$.

*Proof.* First remark that if $\psi_1$ and $\psi_2$ are reflexive, then there is some $\psi$ such that $\sqsubseteq^\psi_1 \sqsubseteq^\psi_2 \subseteq \sqsubseteq^\psi$. Also remark that for all $\varphi$, if $\psi_1$ is reflexive, then there is a reflexive $\psi_2$ for which $\sqsubseteq^\varphi \sqsubseteq^\psi_1 \subseteq \sqsubseteq^\psi_2 \sqsubseteq^\varphi$. It is now enough to prove the weaker statement with reflexive $\psi$ interleaving with the $\varphi_i$s. Moreover this weaker statement is transitive so we can just use induction on $A \triangleright \varphi$ now:

- $a/b \triangleright b \leq a$: trivial ($\sqsubseteq^b \leq a \subseteq \sqsubseteq^b \leq a$).

- the case for $\triangleright$-PAR-* is trivial as well,
- ▷-COMBINE needs an induction of its own:

* ⊢-REFL $A ▷ a ≤ a$: $\varphi$ is then indeed reflexive

* ⊢-IN $\varphi \in A$: indeed $\sqsubseteq \varphi \subseteq \sqsubseteq \varphi$,

* ⊢-MIRROR $\sqsubseteq^{a \Upsilon b} = \sqsubseteq^{b \Upsilon a}$.

* ⊢-TRANS since $a ≤ b, b ≤ c \vdash a \Upsilon c$ we use Lemma 20.

* ⊢-JOIN same as above with $a ≤ b, c ≤ b \vdash a \Upsilon c$

* ⊢-EXTJOIN same with $a ≤ b, b \Upsilon c \vdash a \Upsilon c$.

□

**Lemma 26.** If $\mu_{\sqsubseteq P|Q} \mu'$ and $a \notin \mathrm{fn}(\mu)$, $\mathrm{fn}(\mu')$, $\mathrm{fn}(Q)$ then $\mu_{\sqsubseteq (\nu a P)|Q} \mu'$.

*Proof.* We use Lemma 21 to get a sequence $\mu_0, \mu_1, \dots, \mu_n$ with $\mu = \mu_0$ and $\mu' = \mu_n$ and $\mu_i \sqsubseteq \varphi_i \mu_{i+1}$ with for each $i$, $P ▷ \varphi_i$ or $Q ▷ \varphi_i$. Suppose $a \in \mathrm{fn}(\varphi_i)$ and $Q ▷ \varphi_i$, then wlog. since $\varphi_i$ is trivial and we can suppose that in fact $P ▷ \varphi_i$. We then regroup all subsequences $\varphi_i, \dots, \varphi_j$ entailed by $P$ together (and we do the same with $Q$) to obtain after some reindexing: $\mu_{j_1} \sqsubseteq_P \mu_{j_2} \sqsubseteq_Q \mu_{j_3} \sqsubseteq_P \dots$ such that for all $k$, $a \notin \mathrm{fn}(\mu_{j_k})$. Then we can write in fact $\mu_{j_1} \sqsubseteq_{\nu a P} \mu_{j_2} \sqsubseteq_Q \mu_{j_3} \sqsubseteq_{\nu a P} \dots$ and we can conclude that $\mu_{\sqsubseteq (\nu a P)|Q} \mu'$.

**Lemma 27.** If $\mu_{\sqsubseteq P|Q} \mu'$ and $a \notin \mathrm{fn}(\mu)$, $\mathrm{fn}(Q)$ then for some $\lambda$ such that $a \notin \mathrm{fn}(\lambda)$, $\mu_{\sqsubseteq (\nu a P)|Q} \lambda \sqsubseteq_P \mu'$.

*Proof.* As in the proof of Lemma 26 we get $\mu = \mu_{j_1} \sqsubseteq_P \mu_{j_2} \sqsubseteq_Q \dots \sqsubseteq_P \mu_{j_n} = \mu'$ except $a$ may appear in $\mu' = \mu_{j_n}$, but not in any other $\mu = \mu_{j_k}$ if $k < n$. We choose $\lambda = \mu_{j_{n-1}}$, the rest is the same.

**Lemma 28.** If $\varphi_1 = \alpha \Upsilon \gamma$ is defined and $\varphi_2 \vdash_P \varphi_1$, then either

1. for some $\beta$, $\beta(x) \sqsubseteq \psi \alpha(x)$ and $\varphi_2 = \beta \Upsilon \gamma$, or

2. for some $\beta$, $\beta(x) \sqsubseteq \psi \gamma(x)$ and $\varphi_2 = \alpha \Upsilon \beta$ (this case being unnecessary if $\mathrm{fn}(\alpha) \not\subseteq \mathrm{n}(\varphi_2)$).

**Lemma 29.** If $P \xrightarrow{\mu} P'$ and $\eta \sqsubseteq_P \mu$ then $P \xrightarrow{\eta} P'$. Conversely, whenever $P \xrightarrow{\eta} P'$ there exists $\mu$ such that $\eta \sqsubseteq_P \mu$ and $P \xrightarrow{\mu} P'$, of which we can have a proof of smaller size that does not end with a preorder rule.

*Proof.* Both direction are proved by simple inductions.

**Notation 3** We adopt the following notation in writing derivations, to denote either an application of the first part of Lemma 29 (i.e. an application of several preorder rules), or a recursive case analysis on the rules deriving $P \xrightarrow{\mu} P'$ until a non-preorder rule is reached, by application of the second part of Lemma 29.

$$ \frac{P \xrightarrow{\mu'} P'}{[\mu \sqsubseteq_P \mu']}, \qquad P \xrightarrow{\mu} P' $$

Lemma 30 justifies the fact that we can use the shortcut $\tau$ for a $[\varphi] \tau$ transition with “some reflexive $\varphi$” as well as “any reflexive $\varphi$”.
**Lemma 30.** The following are equivalent:

1. $P \xrightarrow{[\psi]\tau} P'$ for some reflexive $\psi$,

2. $P \xrightarrow{[\psi]\tau} P'$ for all reflexive $\psi$,

3. $P \xrightarrow{[\varphi]\tau} P'$ and there is a name $a \in \mathfrak{n}(\varphi) \setminus \mathfrak{fn}(P)$.

*Proof.* First remark that if $\psi$ is reflexive then for all $\Gamma$, $\Gamma \vdash \psi$, which means $[\varphi]\tau \sqsubseteq_P [\psi]\tau$ for any $\varphi$, so we only need to prove (iii) $\Rightarrow$ (i) which is equivalent to saying $[\psi]\tau \sqsubseteq_P [\varphi]\tau$ for some reflexive $\psi$, which in turn follows from Lemma 15.

□

**Lemma 31.** If $(\nu a)P \xrightarrow{\mu} P_1$ then $P_1 = (\nu a)P'$ for some $P'$ such that $P \xrightarrow{\mu} P'$.

*Proof.* Using Lemma 29 we know that $(\nu a)P \xrightarrow{\mu_1} P_1$ for some $\mu_1$ such that $\mu \sqsubseteq_{\nu a P \mu_1}$, and that this transition is coming from a reduction $P \xrightarrow{\mu_1} P'$ with $P_1 = (\nu a)P'$. Since $\Phi(\nu a P) \subseteq \Phi(P)$ we know $\mu \sqsubseteq_P \mu_1$ so we can derive $P \xrightarrow{\mu} P'$.

We are now ready to prove that transitions commute with $\equiv$: The next lemma follows from an analysis similar to the proof of Lemma 18. Lemma 41 is the most complex case in the proof of congruence of $\sim$, for which Lemmas 18 and 41 are needed. Lemma 42 is useful for the completeness proof.

**Lemma 32.** If $P \equiv Q$ and $P \xrightarrow{\mu} P'$ then $Q \xrightarrow{\mu} \equiv P'$.

*Proof.* More generally, we prove by induction on the derivation of $P \equiv Q$ that for all $\mu$, $((P \xrightarrow{\mu} P' \Rightarrow Q \xrightarrow{\mu} \equiv P')$ and $(Q \xrightarrow{\mu} Q' \Rightarrow P \xrightarrow{\mu} \equiv Q'))$.

Then in most cases we begin by an induction on the derivation of $P \xrightarrow{\mu} P'$. We factor out the cases corresponding to preorder rules using Lemma 29 twice: once to get $\mu_1 \sqsubseteq_P \mu$ and $P \xrightarrow{\mu_1} P'$ on which we can use the induction hypothesis to prove $Q \xrightarrow{\mu_1} Q' \equiv P'$, and once to get $Q \xrightarrow{\mu} Q'$, since $\mu_1 \sqsubseteq_Q \mu$ (Lemma 18). Hence, we can always assume that the last rule is not a preorder rule and therefore decomposes the structure of $P$.

1. Congruence: we suppose the result holds for $P \equiv Q$, and we prove it for $C[P] \equiv C[Q]$. Assuming $(\forall \mu, P \xrightarrow{\mu} P' \Rightarrow Q \xrightarrow{\mu} \equiv P')$ we prove, by induction on $C[P] \xrightarrow{\mu} P_1$, that $C[Q] \xrightarrow{\mu} Q_1 \equiv P_1$. We assume the last rule is deconstructing $C[P]$ into smaller parts (as if it were an induction on $C$):

(a) $C = []$: immediate.

(b) $C = \Sigma\pi_i.R_i + \rho.C'$: if a $\pi_i$ branch is chosen, $P_1$ does not depend on $P$ and $C[Q] \xrightarrow{\mu} P_1$. If the $\rho$ branch is chosen $P_1 = (\nu x)(\varphi | C'[P])$ where $\varphi$ is an arc. Then $C[Q] \xrightarrow{\mu} (\nu x)(\varphi | C'[Q]) \equiv P_1$.

(c) $C = \nu a C'$: immediate (the side condition is the same, and if $P_1 \equiv Q_1$ then $\nu a P_1 \equiv \nu a Q_1$).

(d) $C = C' | R$ and the last rule is PAR (or symmetrically): we obtain $C'[P] \xrightarrow{\mu} P_2$ with $P_1 = P_2 | R$ and by induction $C'[Q] \xrightarrow{\mu} Q_2 \equiv P_2$. Using PAR, $C'[Q] | R \xrightarrow{\mu} Q_2 | R \equiv P_1$.
(e) $C = R | C'$ and the last rule is PAR (or symmetrically): same, but easier.

(f) $C = C' | R$ or $C = R | C'$ and the last rule is one of the communication rules, e.g. $\rightarrow$-COMM-L:

$C'[P] \xrightarrow{\bar{a}(x)} P_2$ and $R \xrightarrow{c(x)} R'$ with $P_1 = (\nu x)(P_2 | R')$. By induction, $C'[Q] \xrightarrow{\bar{a}(x)} Q_2 \equiv P_2$ so by applying $\rightarrow$-COMM-L again, $C'[Q] | R \xrightarrow{[a \Upsilon c] \tau} \equiv (\nu x)(P_2 | R')$.

2. Equivalence properties: reflexivity and transitivity are straightforward; symmetry is handled by the generality of the statement.

3. $P | 0 \equiv P$: straightforward: the last rule must be $\rightarrow$-PAR-L.

4. $P \equiv P | 0$: straightforward.

5. $(P | Q) | R \equiv P | (Q | R)$: there are a lot of cases, of which the first below is the only trivial one:

(a) $\rightarrow$-PAR-R: $R \xrightarrow{\mu} R'$ so two applications of $\rightarrow$-PAR-R are enough to get $P | (Q | R) \xrightarrow{\mu} \equiv (P | Q) | R'$.

(b) $\rightarrow$-PAR-L, preorder rules and Lemma 29 to get $\mu_{\sqsubseteq P|Q} \mu_1$, then a $\rightarrow$-PAR-R rule to get $Q \xrightarrow{\mu_1} Q'$. Getting back $P | (Q | R) \xrightarrow{\mu_1} P | (Q' | R)$ is easy, what is more tricky is to get right the label $\mu$: for that we use again Lemma 29 thanks to the fact that $\mu_{\sqsubseteq P|(Q|R)} \mu_1$, in turn implied by $\mu_{\sqsubseteq P|Q} \mu_1$ (since $\Phi(P | Q) \subseteq \Phi((P | Q) | R) = \Phi(P | (Q | R))$ by rule $\triangleright$-PAR-L and Lemma 18).

$$ \begin{array}{c} \text{PAR-R} \\ \text{PAR-L} \end{array} \quad \frac{\begin{array}{c} Q \xrightarrow{\mu_1} Q' \\ P | Q \xrightarrow{\mu_1} P | Q' \\ \boxed{\mu_{\sqsubseteq P|Q} \mu_1} \\ P | Q \xrightarrow{\mu} P | Q' \end{array}}{(P | Q) | R \xrightarrow{\mu} (P | Q') | R} \rightsquigarrow \frac{\begin{array}{c} Q \xrightarrow{\mu_1} Q' \\ Q | R \xrightarrow{\mu_1} Q' | R \\ P | (Q | R) \xrightarrow{\mu_1} P | (Q' | R) \\ \boxed{\mu_{\sqsubseteq P|(Q|R)} \mu_1} \\ P | (Q | R) \xrightarrow{\mu} P | (Q' | R) \end{array}}{\text{PAR-L}} \quad \begin{array}{c} \text{PAR-R} \\ \text{PAR-L} \end{array} \end{array} $$

(c) $\rightarrow$-PAR-L, preorder rules and Lemma 29 to get $\mu_{\sqsubseteq P|Q} \mu_1$, then a $\rightarrow$-PAR-R rule to get $P \xrightarrow{\mu_1} P'$. Only the top of the proof tree is modified (from $Q$ to $P$), the rest of the derivation is the same.

(d) $\rightarrow$-COM-L rule ($\varphi = \alpha \Upsilon \gamma$), preorder rules on the left premise to get $\mu = \alpha(x) \sqsubseteq_P | Q \alpha_1(x)_1$, then a $\rightarrow$-PAR-R rule to get $Q \xrightarrow{\alpha_1(x)} Q'$. By Lemma 23 we can have $\varphi_1 = \alpha_1 \Upsilon \gamma$ such that $[\varphi] \tau_{\sqsubseteq_P | Q} [\varphi_1] \tau$ from which we conclude as previously $[\varphi] \tau_{\sqsubseteq_P | (Q|R)} [\varphi_1] \tau$ to get the final transition from Lemma 29. Same proof for $\rightarrow$-COM-R.

$$ \begin{array}{c} \text{PAR-R} \\ \text{COM-L} \end{array} \quad \frac{\begin{array}{c} Q \xrightarrow{\alpha_1(x)} Q' \\ P | Q \xrightarrow{\alpha_1(x)} P | Q' \\ \boxed{\alpha(x) \sqsubseteq_P | Q \alpha_1(x)} \\ P | Q \xrightarrow{\alpha(x)} P | Q' \end{array}}{(P | Q) | R \xrightarrow{[\varphi] \tau} \nu x((P | Q') | R')} \rightsquigarrow \frac{\begin{array}{c} Q \xrightarrow{\alpha_1(x)} Q' \\ Q | R \xrightarrow{[\varphi_1] \tau} \nu x(Q' | R') \\ P | (Q | R) \xrightarrow{[\varphi_1] \tau} P | \nu x(Q' | R') \\ \boxed{[\varphi] \tau_{\sqsubseteq_P | (Q|R)} [\varphi_1] \tau} \\ P | (Q | R) \xrightarrow{[\varphi] \tau} P | \nu x(Q' | R') \end{array}}{\text{COM-L}} \quad \begin{array}{c} \text{PAR-R} \\ \text{PAR-L} \end{array} \end{array} $$
(e) $\rightarrow$-COM-* rule, preorder rules, then a $\rightarrow$-PAR-L rule: it is the same proof as above: the transition with the label $[\varphi_1]\tau$ from $P$ | ($Q$ | $R$) is easy to obtain, the rest is the same.

6. $P$ | ($Q$ | $R$) $\equiv$ ($P$ | $Q$) | $R$: similar proof.

7. $P$ | $Q \equiv Q$ | $P$: the last rule is either:

(a) $\rightarrow$-PAR-R or $\rightarrow$-PAR-L, that complement each other, or

(b) $\rightarrow$-COM-L rules, resulting in a process of the form $(\nu x)(P' | Q')$ with $P \xrightarrow{\alpha(x)} P'$, $Q \xrightarrow{\gamma(x)} Q'$ and $\mu = [\alpha \gamma \gamma]\tau$. The application of the rule $\rightarrow$-COM-R will give the transition $[\gamma \gamma \alpha]\tau$ which is convertible to $\mu$ through the rule $\rightarrow$-TAU-$\Delta$ since $\alpha \gamma \gamma \vdash \gamma \gamma \alpha$.

8. $Q$ | $P \equiv P$ | $Q$: same proof.

9. $(\nu a)P \equiv (\nu b)P\{b/a\}$ when $b \notin \text{fn}(P)$: this case boils down to a proof of if $P \xrightarrow{\mu} P'$ then $P_\sigma \xrightarrow{\mu_\sigma} P'_\sigma$ where $\sigma$ is an injective substitution (whose domain does not intersect with $\text{bn}(\mu)$).

10. $(\nu b)P\{b/a\} \equiv (\nu a)P$: similar proof.

11. $(\nu ab)P \equiv (\nu ba)P$: last rule is $\rightarrow$-RES, we get $(\nu b)P \xrightarrow{\mu} P_1$, then using Lemma 29 we get $(\nu b)P \xrightarrow{\mu_1} (\nu b)P'$ and $P \xrightarrow{\mu_1} P'$ with $\mu \subseteq_P \mu_1$, and again with Lemma 29 we get $P \xrightarrow{\mu} P'$ and apply $\rightarrow$-RES twice.

12. $(\nu ba)P \equiv (\nu ab)P$: same proof.

13. $(\nu aP) | Q \equiv \nu a(P | Q)$: the last non-preorder rule can be of two kinds:

(a) the last rule is a $\rightarrow$-PAR-* rule. If $Q$ does the transition, we are done. If $\nu aP$ does the transition $\mu$, then we get a transition $\mu_1$ with $\mu \subseteq_{\nu aP} \mu_1$ from $P$ using Lemma 29. $P | Q$ can also make the transition $\mu_1$, and since $\mu \subseteq_{\nu aP} \mu_1$ implies $\mu \subseteq_{\nu a(P|Q)} \mu_1$ we get the transition $\mu$ from $\nu a(P | Q)$.

(b) If the last rule is a $\rightarrow$-COM-* rule then $\mu = [\varphi]\tau$, and $\nu aP$ does some transition $\mu$ to what must be $\nu aP'$ with $P \xrightarrow{\mu_1} P'$ and $\mu \subseteq_{\nu aP} \mu_1$. Composing $P$ with $Q$ (in the case of $\rightarrow$-COM-*) yields a transition $[\varphi_1]\tau$ with $[\varphi_1]\tau \subseteq_{\nu aP}[\varphi]\tau$ which implies $[\varphi_1]\tau \subseteq_{\nu a(P|Q)}[\varphi]\tau$, so Lemma 29 is again used twice.

14. $\nu a(P | Q) \equiv (\nu aP) | Q$: in this case, again, one must pay close attention to interference between restriction and preorder judgements. From the transition $\mu$ from $\nu a(P | Q)$ we get the same transition from $P | Q$, but after an application of Lemma 29 we have $\mu \subseteq_{P|Q} \mu_1$ with a transition $\mu_1$ that can be broken into either $P \xrightarrow{\mu_1} P'$ or $Q \xrightarrow{\mu_1} Q'$ (in the case of a $\rightarrow$-PAR-* rule), or both $P \xrightarrow{\mu} P'$ and $Q \xrightarrow{\chi} Q'$ (in the case of a $\rightarrow$-COM-* rule). The problem is, we have to recover all the contributions from $P$ in such a way that $\nu aP$ can achieve as much. Notably $\mu$ or $\mu_1$ may mention $a$. We treat the three cases separately:

(a) the case of the $\rightarrow$-PAR-R rule has two subcases. First when $a \notin \text{fn}(\mu_1)$, it boils down to Lemma 26. If $\mu_1$ is a visible action then the object of $\mu_1$ must stay fresh, but we know already that $\text{obj}(\mu_1) \cap \text{fn}(P) = \emptyset$ which implies $\text{obj}(\mu_1) \cap \text{fn}(\nu aP) = \emptyset$.

The case $a \in \text{fn}(\mu_1)$ is not possible when $\mu_1$ is a visible action because then, $\text{fn}(\mu_1) \subseteq \text{fn}(Q)$ and $a \notin \text{fn}(Q)$. In the case $\mu_1$ is of the form $[\varphi_1]\tau$, we apply Lemma 30 to get that $Q \xrightarrow{\tau} Q'$ and thus $(\nu aP) | Q \xrightarrow{\tau} (\nu aP)$ |
$Q'$ from which we can easily derive any transition between the same processes with any label of the form $[\varphi]\tau$ (and $\mu$ must be of this form).

$$ \frac{Q \xrightarrow{\mu_1} Q'}{\frac{P | Q \xrightarrow{\mu_1} P | Q'}{[\mu \sqsubseteq_P Q \mu_1]}} \rightsquigarrow \frac{Q \xrightarrow{\mu_1} Q'}{(\nu a P) | Q \xrightarrow{\mu_1} (\nu a P) | Q'} \\ \frac{P | Q \xrightarrow{\mu} P | Q'}{(\nu a)(P | Q) \xrightarrow{\mu} (\nu a)(P | Q')} \quad a \notin \mathbf{n}(\mu) \quad (\nu a P) | Q \xrightarrow{\mu} (\nu a P) | Q' $$

(b) The case of rule $\rightarrow$-PAR-L: the action $\mu_1$, coming originally from $P$, may contain $a$ but we use Lemma 27 to obtain a transition along $\lambda$, to which we can apply $Q$'s original role in the transformation of $\mu_1$ into $\mu$ (combined to the role of $\nu a P$).

The following derivations illustrate the reasoning exposed above.

$$ \frac{P \xrightarrow{\mu_1} P'}{\frac{P | Q \xrightarrow{\mu_1} P' | Q}{[\mu \sqsubseteq_P Q \mu_1]}} \rightsquigarrow \frac{P \xrightarrow{\lambda} P'}{\nu a P \xrightarrow{\lambda} \nu a P'} \quad a \notin \mathbf{n}(\lambda) \\ \frac{P | Q \xrightarrow{\mu} P' | Q}{(\nu a)(P | Q) \xrightarrow{\mu} (\nu a)(P' | Q)} \quad a \notin \mathbf{n}(\mu) \quad (\nu a P) | Q \xrightarrow{\mu} (\nu a P') | Q' \\ \frac{[\mu \sqsubseteq_P Q \lambda]}{(\nu a P) | Q \xrightarrow{\mu} (\nu a P') | Q} $$

(c) The case of the $\rightarrow$-COM-L rule ($\rightarrow$-COM-R being symmetric): this time $\mu = [\varphi]\tau$ is obtained from some $[\varphi_1]\tau$ such that $[\varphi]\tau \sqsubseteq_P Q[\varphi_1]\tau$ (as usual, using Lemma 29) and $[\varphi_1]\tau$ is obtained from two transitions: $P \xrightarrow{\alpha(x)} P'$ and $Q \xrightarrow{\gamma(x)} Q'$ with $\varphi = \alpha \gamma$. We write $\mu$ for $\alpha(x)$ and $\chi$ for $\gamma(x)$.

Lemma 27 allows us to decompose $\sqsubseteq_P Q$ into $[\varphi]\tau \sqsubseteq_P Q[\varphi_2]\tau \sqsubseteq_P Q[\varphi_1]\tau$. We use Lemma 13 to decompose $\varphi_2 \vdash_P^* \varphi_1$ into $\varphi_2 \vdash_P \varphi_3 \vdash_P \varphi_1$ such that $\mathrm{fn}(\mu) \cap \mathbf{n}(\varphi_3) = \emptyset$. We apply Lemma 28 to get $\beta$ such that $\beta(x) \sqsubseteq_P \alpha(x)$ and $\varphi_3 = \beta \gamma$. Since $a \notin \mathbf{n}(\varphi_3)$, we know that $a \notin \mathbf{n}(\beta)$, so we can apply the restriction rule on the transition along $\beta(x)$. Furthermore, since $\varphi_2 \vdash_P \varphi_3$ and $a$ is in none of both, we know by transitivity that $[\varphi]\tau \sqsubseteq_P Q[\varphi_3]\tau$. We write $\eta$ for $\beta(x)$ below:

$$ \frac{P \xrightarrow{\mu} P'}{\frac{P | Q \xrightarrow{[\varphi_1]\tau} (\nu x)(P' | Q')}{[\varphi]\tau \sqsubseteq_P Q[\varphi_1]\tau}} \rightsquigarrow \frac{P \xrightarrow{\eta} P'}{\nu a P \xrightarrow{\eta} \nu a P'} \quad a \notin \mathbf{n}(\eta) \\ \frac{P | Q \xrightarrow{[\varphi]\tau} (\nu x)(P' | Q')}{(\nu a)(P | Q) \xrightarrow{[\varphi]\tau} (\nu a)(\nu x)(P' | Q')} \quad a \notin \mathbf{n}(\varphi) \quad (\nu a P) | Q \xrightarrow{[\varphi_3]\tau} (\nu x)((\nu a P') | Q') \\ \frac{[\varphi]\tau \sqsubseteq_P Q[\varphi_3]\tau}{(\nu a P) | Q \xrightarrow{[\varphi]\tau} (\nu x)((\nu a P') | Q')} $$
This concludes the induction.

**Lemma 33.** If $P \triangleright \varphi$ then $P | \varphi \sim P$.

*Proof.* We prove that $\mathcal{R} = \{(P | \varphi, P) | P \triangleright \varphi\}$ is a simulation ($\mathcal{R}^{-1}$ is clearly one). Suppose $P | \varphi \xrightarrow{\mu} P_1$. Using Lemma 29 we get $\mu_1$ such that $\mu_{\sqsubseteq P | \varphi} \mu_1$, and a proof of $P | \varphi \xrightarrow{\mu_1} P'$ with a non preorder rule as last rule. This rule must be a PAR rule coming from $P$ so in fact $P_1 = P' | \varphi$ with $P \xrightarrow{\mu_1} P'$. Since $\Phi(P | \varphi) = \Phi(P)$ by Lemma 17 we know that $\mu_{\sqsubseteq P} \mu_1$ and we apply Lemma 29 again to get $P \xrightarrow{\mu} P'$ and indeed $P' | \varphi \mathcal{R} P'$.

**Lemma 34.** $\equiv$ is a bisimulation.

*Proof.* Almost direct consequence of Lemmas 18 and 32. The correspondence between transitions is exact, hence the only non-trivial case is for the $[\varphi]\tau$ transition because one would want $P' | \varphi \equiv Q' | \varphi$ instead of just $P' \equiv Q'$. This holds because $\equiv$ is a congruence.

**Definition 35 (Bisimulation up to $\sim$).** A relation $\mathcal{R}$ is a bisimulation up to bisimilarity if it validates the clauses of the usual bisimulation, except when requiring that $P_1 \mathcal{R} Q_1$ we only require $P_1 \sim P_2$ and $Q_1 \sim Q_2$ with $P_2 \mathcal{R} Q_2$.

**Lemma 36.** If $\mathcal{R}$ is a bisimulation up to bisimilarity, then $\mathcal{R} \subseteq \sim$.

*Proof.* We prove $\sim \mathcal{R} \sim$ is a bisimulation. The only unusual transition $\mu$ is when $\mu = [\varphi]\tau$, but from $P \sim P_1 \mathcal{R} Q_1 \sim Q$ and $P \xrightarrow{\mu} P'$ we know:

- that $P_1 \xrightarrow{\mu} P'_1$ and $(P' | \varphi) \sim (P'_1 | \varphi)$ from the $\sim$ game,

- that $Q_1 \xrightarrow{\mu} Q'_1$ and $(P'_1 | \varphi) \sim \mathcal{R} \sim (Q'_1 | \varphi)$ from the $\mathcal{R}$ up-to game,

- that $P \xrightarrow{\mu} P'$ and $(Q'_1 | \varphi) \sim (Q' | \varphi)$ from the second $\sim$ game.

So the case for a $[\varphi]\tau$ transition is no more difficult than usual: we conclude by transitivity of $\sim$.

**Lemma 37.** $P \sim Q$ implies $(\nu a)P \sim (\nu a)Q$ for all $a$.

*Proof.* We prove $\mathcal{R} \triangleq \{(\nu a P, \nu a Q) | P \sim Q\}$ is a bisimulation up to bisimilarity (Lemma 36), which is relatively easy using Lemma 31. The only interesting case is for a conditional $\tau$ transition. If $\nu a P \xrightarrow{[\varphi]\tau} \nu a P'$ then $P \xrightarrow{[\varphi]\tau} P'$ and using $\sim$, $Q \xrightarrow{[\varphi]\tau} Q'$ with $(P' | \varphi) \sim (Q' | \varphi)$. Since we want to relate $(\nu a)P' | \varphi$ and $(\nu a)Q' | \varphi$ we $\sim$-rewrite them into $(\nu a)(P' | \varphi)$ and $(\nu a)(Q' | \varphi)$ (using Lemma 34) which are indeed related through $\mathcal{R}$. The condition about $\triangleright$ is ensured by compositionality of $\triangleright$ (Lemma 16).

**Definition 38 (Bisimulation up to $\sim$ and $\nu$).** A relation $\mathcal{R}$ is a bisimulation up to restriction and bisimilarity if it validates the clauses of the usual bisimulation, except that the outcomes of the transitions, $P_1$ and $Q_1$, are requested to satisfy $P_1 \sim (\nu \tilde{a}) P_2$ and $Q_1 \sim (\nu \tilde{a}) Q_2$ with $P_2 \mathcal{R} Q_2$, where $\tilde{a}$ stands for a (possibly empty) tuple of names.
**Lemma 39.** If $\mathcal{R}$ is a bisimulation up to restriction and bisimilarity then $\mathcal{R} \subseteq \sim$.

*Proof.* We write $\mathcal{R}^{\nu}$ for $\{(\nu\tilde{a})P, (\nu\tilde{a})Q) \mid P \mathcal{R} Q\}$. We know that $\mathcal{R} \subseteq \mathcal{S} \triangleq \sim\mathcal{R}^{\nu} \sim$ so it is enough to prove that $\mathcal{S}$ is a bisimulation. Suppose $P \sim (\nu\tilde{a})P_1 \mathcal{R}^{\nu} (\nu\tilde{a})Q_1 \sim Q$ with $P_1 \mathcal{R} Q_1$. We start from a transition $P \xrightarrow{\mu} P'$, we use the bisimulation game on $\sim$ and Lemma 31 to deduce $(\nu\tilde{a})P_1 \xrightarrow{\mu} (\nu\tilde{a})P'_1$ with $P_1 \xrightarrow{\mu} P'_1$ and $(P' \mid A) \sim ((\nu\tilde{a})P'_1 \mid A)$ with $A = \varphi$ if $\mu = [\varphi]\tau$ or $A = 0$ otherwise. Using the bisimulation up-to on $\mathcal{R}$ we obtain $Q_1 \xrightarrow{\mu} Q'_1$ with $(P'_1 \mid A) \sim (\nu\tilde{c})P_2 \mathcal{R}^{\nu} (\nu\tilde{c})Q_2 \sim (Q'_1 \mid A)$ for some $P_2 \mathcal{R} Q_2$. We also get $(\nu\tilde{a})Q_1 \xrightarrow{\mu} (\nu\tilde{a})Q'_1$ from which using the game on the second $\sim$, $Q \xrightarrow{\mu} Q'$ with $((\nu\tilde{a})Q'_1 \mid A) \sim (Q' \mid A)$.

We now compose what we have: $(P' \mid A) \sim ((\nu\tilde{a})P'_1 \mid A)$ and $(P'_1 \mid A) \sim ((\nu\tilde{c})P_2)$. We can get from the latter $((\nu\tilde{a})P'_1 \mid A) \sim ((\nu\tilde{a}\tilde{c})P_2)$ using Lemmas 34 and 37, and then compose them using transitivity of $\sim$; similarly for $Q: (Q' \mid A) \sim ((\nu\tilde{a}\tilde{c})Q_2)$. Since $P_2 \mathcal{R} Q_2$, the pair of $P' \mid A$ and $Q' \mid A$ is in $\mathcal{S}$.

**Definition 40 (Bisimulation up to $\sim$ and $\sigma$).** A relation $\mathcal{R}$ is a bisimulation up to bisimilarity and injective substitution if it validates the clauses of the usual bisimulation, except that the outcomes of the transitions, $P_1$ and $Q_1$, are requested to satisfy $P_1 \sim P_{2\sigma}$ and $Q_1 \sim Q_{2\sigma}$ with $P_2 \mathcal{R} Q_2$, where $\sigma$ stands for an injective name substitution.

*Proof.* We prove $\sim \mathcal{R}_{\sigma} \sim$ is a bisimulation where $\mathcal{R}_{\sigma}$ stands for $\{(P_{\sigma}, Q_{\sigma}) \mid P \mathcal{R} Q \text{ and } \sigma \text{ is injective}\}$.

**Lemma 41.** $P \sim Q$ implies $P \mid R \sim Q \mid R$ for all $R$.

*Proof.* We show that

$$ \mathcal{R} \triangleq \{(P \mid R, Q \mid R) \mid P \sim Q\} $$

is a bisimulation up to restriction and bisimilarity. The condition about induced $\varphi$ can be dealt with using Lemma 16: since $(\forall\psi, P \triangleright \psi \Leftrightarrow Q \triangleright \psi)$ by definition of $\sim$, we have $P \mid R \triangleright \varphi$ implies $Q \mid R \triangleright \varphi$ and symmetrically.

Now suppose $P \mid R \xrightarrow{\mu} P_1$ with $\text{bn}(\mu) \cap \text{fn}(P, Q, R) = \emptyset$. We can suppose by Lemma 29 that for some $\mu_1$ with $\mu \sqsubseteq_P R\mu_1$, $P \mid R \xrightarrow{\mu_1} P_1$, and that the last rule applied is not a preorder rule. Since $\Phi(P \mid R) = \Phi(Q \mid R)$, $\mu \sqsubseteq_Q R\mu_1$, and it is enough to get $Q \mid R \xrightarrow{\mu_1} Q_1$ to prove $Q \mid R \xrightarrow{\mu} Q_1$. There are two cases in the bisimulation game, depending on $\mu_1$:

*Proof.* We prove $\{(P \mid R, Q \mid R) \mid P \sim Q\}$ is a bisimulation up to restriction and bisimilarity, and (thanks to Lemmas 16 and 29) we only focus on the clause about $[\varphi]\tau$ transitions, where Lemma 29 gives $\varphi_1$ s.t. $[\varphi]\tau \sqsubseteq_P R[\varphi_1]\tau$ and $Q \mid R$.

We prove that $\mathcal{R} = \{(P \mid R, Q \mid R) \mid P \sim Q\}$ is a bisimulation up to restriction and bisimilarity. Lemma 16 handles the first clause about conditions, and Lemma 29 the second one about visible transitions. Lemma 29 also helps handling a $[\varphi]\tau$ transition from $P \mid R$ to $P_1$ by saying it comes from a $[\varphi_1]\tau$
transition from $P$, or $R$, or both, and such that $[\varphi]\tau\sqsubseteq_P R[\varphi_1]\tau$. From that, getting a transition $[\varphi]\tau$ from $Q \mid R$ to $Q_1$ is easy, but one must relate $P_1 \mid \varphi$ and $Q_1 \mid \varphi$ in $\mathcal{R}$ using three different assumptions:

1. $R \xrightarrow{[\varphi_1]\tau} R'$. Then $P \mid R' \mid \varphi \sim \mathcal{R} \sim Q \mid R' \mid \varphi$. (up to $\sim$)

2. $P \xrightarrow{[\varphi_1]\tau} P'$. Then $P' \mid \varphi_1 \sim Q' \mid \varphi_1$, that implies $P' \mid R \mid \varphi \sim \mathcal{R} \sim Q' \mid R \mid \varphi$. Indeed $\varphi_1$ is absorbed by $\varphi$ since $P \mid Q \mid \varphi \triangleright \varphi_1$. (up to $\sim$)

3. $P$ and $R$ synchronised into $(\nu x)(P' \mid R')$. Then $P' \sim Q'$ and we can relate $(\nu x)(P' \mid R') \mid \varphi$ to $(\nu x)(Q' \mid R') \mid \varphi$ (up to $\sim$ and $\nu$). $\square$

**Lemma 42.** For any $P$, $Q$ and $\varphi$, $P \xrightarrow{[\varphi]\tau} Q$ iff $P \mid \varphi \xrightarrow{\tau} Q \mid \varphi$.

**Theorem 43 (Characterisation).** $P \simeq Q$ iff $P \sim Q$.

*Proof (Sketch).* The proof follows a standard pattern, and exploits the lemmas stated above. For completeness, we define tester processes, corresponding to the three clauses in Def. 6. The first one is handled using $[\varphi]\tau \cdot \bar{w}$. We use $\varphi$ for the second clause (by Lemma 42). To test, e.g., $\xrightarrow{\{a\}(x)}$, we use $\bar{a}(y) \cdot (z/y \mid \bar{w} \mid w)$. $\square$

## 3.3 Protected Names and Cocapabilities

Protected prefixes act as cocapabilities, by expressing the ability to react to an interaction offer from the context (cf. $P_0$ in Section 1). We can exploit this idea to define an extension of i/o-types [14,8] for $\pi P$, by introducing *cocapability types* $\overline{o}T$ and $\overline{1}T$.

We refer to Appendix B for a description of this type system.

# 4 Axiomatisation

We now move to the axiomatisation of $\sim$, which is given by the laws of Figure 2.

The overall strategy to define the axiomatisation differs from the standard approach. This is mainly due to the handling of restriction, and its interplay with the state component defined by the toplevel preorder processes. Intuitively, pushing restrictions under prefixes can be done only if the toplevel prefixes of a process have somehow been saturated. As a consequence, restriction must be handled together with prefixes and sums. We first show how equational laws allow us to relate processes at toplevel only, and then derive an axiomatisation for full processes.

## 4.1 Preliminaries

As is usually the case in axiomatisations, we first study the processes consisting only of sums, leaving the treatment of parallel composition for later.

We make two remarks, before embarking in the presentation of the equational laws for sums. The first remark is that in $\pi P$, we have to deal with preorder processes, that act somehow like a persistent state, and are used in stating
the equational laws. The second remark is that the treatment of restriction in the axiomatisation requires some particular care, essentially because of the presence of preorder processes. Moreover, contrarily to what is usually the case, the restriction has to be dealt with together with prefixes and sums, as we show below.

We first focus on processes without restriction, for which the axiomatisation can be presented using simpler laws. The ideas presented in this case are at work, in a somewhat more complicated fashion, when handling restriction in Section 4.4.

We introduce a dedicated notation to factor out the preorder part in processes.

**Notations and Terminology.** We use $A$ to range over processes that consist of $\varphi$ processes only, which we call *preorder processes*. We often view such processes as multisets of conditions. We use notation $A, P$ to denote a process that can be written, using the monoid laws for $|\cdot|$, as $A \mid P$, where $P$ does not contain toplevel arcs. Note that $A$ may contain restrictions, corresponding to the definition of join processes (given towards the end of Section 2.1), but extrusion is not allowed to decompose a process as $A, P$. Note that we could have adopted a more complex definition, in order to decompose, for instance, $(\nu u)(u/a \mid u/b \mid c/d \mid \overline{nm}.P)$ into $a \gamma b \mid c/d, \overline{nm}.P$ (which involves an application of name extrusion), but this simpler definition is sufficient for our purposes.

Accordingly, $A, S$ stands for $A \mid S$, where $S$ is a sum process, and $0$ is written $\emptyset, 0$.

We use the following notion of measure to reason by induction on processes.

**Definition 44 (Measure on processes).** Given a $\pi P$ process $P$, we define $|P|$ as the maximum number of prefixes in summands of $P$, i.e., $|\sum_i \pi_i.P_i| = \max_i (1 + |P_i|)$ (hence $|0| = 0$), $|(\nu a)P| = |P|$, $|P \mid Q| = |P| + |Q|$, and $|a/b| = 0$.

We write $\vdash P = Q$ whenever $P$ and $Q$ can be related by equational reasoning using the laws of Figure 2.

We omit the laws for equational reasoning (equivalence, substitutivity). We will reason up to these laws, and up to the standard laws expressing that $|$ and $+$ obey the laws of commutative monoids, and that $+$ is idempotent, in the remainder.

As usual, expansion allows us to rewrite the parallel composition of two sum processes into a sum, the third summand describing synchronisation in $\pi P$.

Note that $\alpha$-conversion for input prefixes follows from Laws L26 and L24, by deriving the following equalities (and similarly for the other visible prefixes):

$$a(y).P \stackrel{L24}{\cong} a(x).(\nu y)(x/y \mid P) \stackrel{L26}{\cong} a(x).(\nu y')(x/y' \mid P\{y'/y\}) \stackrel{L24}{\cong} a(y').P\{y'/y\}.$$

The remaining laws are more specific to $\pi P$, and are analysed below, in Propositions 46, 49 and 52. The latter results are used to establish completeness of the axiomatisation.

The laws are sound:

**Lemma 45.** The laws of Figure 2 relate bisimilar processes.
Proof (Sketch). For laws 30-36, we establish a “saturation property”, expressing the fact that when erasing a preorder process $\varphi$ or a prefix $\pi$ that mentions $a$, we generate all processes $\varphi$ or $\pi$ could induce. The other laws are easy. $\square$

**Standard structural laws**

<table><tr><td>L1</td><td>(P<sub>1</sub> | P<sub>2</sub>) | P<sub>3</sub> = P<sub>1</sub> | (P<sub>2</sub> | P<sub>3</sub>)</td><td>L4</td><td>(S<sub>1</sub> + S<sub>2</sub>) + S<sub>3</sub> = S<sub>1</sub> + (S<sub>2</sub> + S<sub>3</sub>)</td></tr><tr><td>L2</td><td>P<sub>1</sub> | P<sub>2</sub> = P<sub>2</sub> | P<sub>1</sub></td><td>L5</td><td>S<sub>1</sub> + S<sub>2</sub> = S<sub>2</sub> + S<sub>1</sub></td></tr><tr><td>L3</td><td>P<sub>1</sub> | 0 = P<sub>1</sub></td><td>L6</td><td>π.P + π.P = π.P</td></tr></table>

**Expansion law** (we can suppose $x \neq y$, $\text{bn}(\pi_i) \notin \text{fn}(T)$, $\text{bn}(\rho_j) \notin \text{fn}(S)$.)

$$L7 \quad \sum_i \pi_i.P_i \mid \sum_j \rho_j.R_j = \sum_i \pi_i.(P_i \mid T) + \sum_j \rho_j.(S \mid R_j) + \sum_{i,j} [\alpha \gamma \beta]\tau.(\nu xy)(x/y \mid P_i \mid R_j) \quad \begin{array}{l} \text{when } \alpha \gamma \beta \text{ is defined.} \\ \text{and } \{\pi_i, \rho_j\} = \{\bar{\alpha}(x), \beta(y)\} \end{array}$$

**Laws for preorder processes**

<table><tr><td>L8</td><td>a &le; b | b &le; c = a &le; b | b &le; c | a &le; c</td><td>L9</td><td>a &le; b | c &le; b = a &le; b | c &le; b | a &gamma; c</td></tr><tr><td>L10</td><td>a &le; b | b &gamma; c = a &le; b | b &gamma; c | a &gamma; c</td><td>L11</td><td>a &le; a = 0</td></tr></table>

**Laws for prefixes** (counterparts of Laws L16-L19 for output are omitted)

<table><tr><td>L12</td><td>[φ]τ.P = [φ]τ.(φ | P)</td><td>L13</td><td>φ, S + π.P = φ, S + π.(φ | P)</td></tr><tr><td>L14</td><td>[a &le; a]τ.P = [b &gamma; b]τ.P</td><td>L15</td><td>[a &gamma; b]τ.P = [a &gamma; b]τ.P + [a &le; b]τ.P</td></tr><tr><td>L16</td><td>a(x).P = a(x).P + {a}(x).P</td><td>L17</td><td>[a &gamma; b]τ.P = [a &gamma; b]τ.P + [b &gamma; a]τ.P</td></tr><tr><td>L18</td><td>b/a, S + a(x).P = b/a, S + a(x).P + b(x).P</td><td></td><td></td></tr><tr><td>L19</td><td>a/b, S + {a}(x).P = a/b, S + {a}(x).P + {b}(x).P</td><td></td><td></td></tr><tr><td>L20</td><td>b/a, S + [a &le; c]τ.P = b/a, S + [a &le; c]τ.P + [b &le; c]τ.P</td><td></td><td></td></tr><tr><td>L21</td><td>a/b, S + [c &le; a]τ.P = a/b, S + [c &le; a]τ.P + [c &le; b]τ.P</td><td></td><td></td></tr><tr><td>L22</td><td>b/a, S + [a &gamma; c]τ.P = b/a, S + [a &gamma; c]τ.P + [b &gamma; c]τ.P</td><td></td><td></td></tr><tr><td>L23</td><td>b/a, S + [a &gamma; c]τ.P = b/a, S + [a &gamma; c]τ.P + [c &le; b]τ.P</td><td></td><td></td></tr><tr><td>L24</td><td>α(y).P = α(x).(νy)(x/y | P) if x &notin; fn(P)</td><td></td><td></td></tr><tr><td>L25</td><td>ᾱ(y).P = ᾱ(x).(νy)(y/x | P) if x &notin; fn(P)</td><td></td><td></td></tr></table>

**Laws for restriction** (counterparts of Laws L31 and L32 for output are omitted; $a \le b \in A^\ddagger$ stands for $a \le b \in A$ and $a \ne b$, and similarly for $a \gamma b$.)

$$L26 \quad (\nu b)P = (\nu a)(P\{a/b\}) \quad \text{if } a \notin \text{fn}(P) \quad L27 \quad (\nu c)(\nu d)P = (\nu d)(\nu c)P$$

$$L28 \quad P \mid (\nu a)Q = (\nu a)(P \mid Q) \quad \text{if } a \notin \text{fn}(P) \quad L29 \quad (\nu a)0 = 0$$

$$L30 \quad (\nu a)A = \{ \begin{array}{l} b \le c \mid b \le a, a \le c \in A^\ddagger \} \uplus \{ b \gamma c \mid b \le a, c \le a \in A^\ddagger \} \\ \uplus \{ b \gamma c \mid a \gamma c, b \le a \in A^\ddagger \} \uplus \{ \varphi \in A \mid a \notin n(\varphi) \} \end{array}$$

$$L31 \quad (\nu a)(A, S + a(x).P) = (\nu a)(A, S + \sum_{a \le b \in A^\ddagger} b(x).(\nu a)(A | P) + \sum_{\begin{subarray}{l} \forall a \gamma b \in A^\ddagger \\ b \le a \le A^\ddagger \end{subarray}} (b)(x).(\nu a)(A | P))$$

$$L32 \quad (\nu a)(A, S + \{a\}(x).P) = (\nu a)(A, S + \sum_{b \le a \in A^\ddagger} \{b\}(x).(\nu a)(A | P))$$

$$L33 \quad (\nu a)(A, S + [a \le c]τ.P) = (\nu a)(A, S + \sum_{a \le b \in A^\ddagger} [b \le c]τ.(\nu a)(A | P)) \quad a \ne c$$

$$L34 \quad (\nu a)(A, S + [c \le a]τ.P) = (\nu a)(A, S + \sum_{b \le a \in A^\ddagger} [c \le b]τ.(\nu a)(A | P)) \quad a \ne c$$

$$L35 \quad (\nu a)(A, S + [a \gamma c]τ.P) = (\nu a)(A, S + \sum_{a \le b \in A^\ddagger} [b \gamma c]τ.(\nu a)(A | P) + \sum_{\begin{subarray}{l} \forall a \gamma b \in A^\ddagger \\ b \le a \le A^\ddagger \end{subarray}} [c \le b]τ.(\nu a)(A | P))$$

$$L36 \quad (\nu a)(A, S + \pi.P) = (\nu a)(A, S + \pi.(\nu a)(A | P)) \quad a \notin n(\pi)$$

<caption>**Fig. 2.** An axiomatisation of $\sim$</caption>

## 4.2 Laws for preorder processes.

Laws L8-L11 are used to saturate preorder processes, as expressed by the following result.
**Proposition 46.** If $A_1, S_1 \sim A_2, S_2$, then there exists $A^*$ such that $\vdash A_i, S_i = A^*, S_i$ ($i = 1, 2$), and $A^* = \coprod \{\varphi \mid \varphi \text{ not reflexive and } A_1 \succcurlyeq \varphi\}$.

(Note that we could have picked $A_2$ instead of $A_1$ above.)

*Proof.* We define a rewriting relation on preorder processes, and write $A \overset{\gamma}{\to} A'$ whenever $A'$ is obtained from $A$ using one of the laws L8-L11, oriented from left to right, as a rewrite rule modulo associativity and commutativity of parallel composition. We furthermore impose that no reflexive condition is added in a rewrite step, nor a condition that is already contained in the preorder process.

We then prove the following three properties about $\overset{\gamma}{\to}$:

1. If $A \overset{\gamma}{\to} A'$, then $A \sim A'$: this is a consequence of Lemma 45 (or, alternatively, by Lemma 33).

2. For any (finite) $A$, there is no infinite $\overset{\gamma}{\to}$-chain emanating from $A$. Indeed, the rules defining $\overset{\gamma}{\to}$ do not introduce any new name. Moreover, a new arc or join can only be added if it is not already present. Since there are finitely many conditions built on a finite set of names, $\overset{\gamma}{\to}$ terminates.

3. Suppose $A$ is a $\overset{\gamma}{\to}$-normal form. Then, for any non-reflexive $\varphi$, if $A \succcurlyeq \varphi$, then $\varphi$ appears in $A$ (which we write $\varphi \in A$).

This follows by induction on the derivation of $A \succcurlyeq \varphi$. The only interesting case is for the $\succcurlyeq$-COMBINE rule, i.e. we know that $A \succcurlyeq \Gamma$ and $\Gamma \vdash \varphi$. We conclude by associating to rules $\vdash$-TRANS, $\vdash$-JOIN and $\vdash$-EXTJOIN laws L8, L9 and L10 respectively.

The observations above entail the expected property. □

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

We say that $A$ is a *saturated preorder process* whenever $A^* \equiv A$. We use $A^*$ to range over such processes. We can remark that even if $A$ contains only arcs, $A^*$ may contain restrictions, because of induced conditions involving $\gamma$.

## 4.3 Laws for Prefixes and Sums

We comment on the laws for prefixes in Figure 2. We first remark that rewriting a sum process using these laws yields a sum process, and the same holds for the laws for preorder processes.

Law L12 expresses the fact that the condition $\varphi$ should be enforced after a $[\varphi]\tau$ transition (see the third clause of the definition of $\sim$, Definition 6). Law L13 propagates $\varphi$s in depth, expressing the persistence of condition processes ($\varphi$).

Law L14 is used to equate all plain $\tau$ prefixes.

Laws L24-L25 are analogous to law L12, because they are related to how the process is observed after the prefix has been fired (see transition rules IN, OUT, PR-I and PR-O, as well as Fact 1).

Laws L18-L23 describe how arcs act on prefixes, by triggering new interaction possibilities.
The next lemma relates transitions of sum processes and the laws for prefixes.
In the statement, we say that two prefixes $\pi$ and $\pi'$ only differ in their bound names whenever either $\pi$ and $\pi'$ are visible actions of the same kind, in which case they have the same subject name, or they are a conditional $\tau$, in which case $\pi = \pi'$.

**Lemma 47.** If $A, S \xrightarrow{\mu} A, P$ then $\vdash A, S = A, S + \pi.Q$ for some $\pi$ and $Q$ such that $\mu$ and $\pi$ only differ in their bound names and $\pi.Q \xrightarrow{\mu} P$.

*Proof.* Suppose $S$ is of the form $S_1+\pi'.Q$ and that the transition $S \xrightarrow{\mu} P$ is coming from $\pi'.Q \xrightarrow{\mu'} P$ and in fact (Lemma 29) from $\pi'.Q \xrightarrow{\mu'} P$ such that $\mu \sqsubseteq_A S \mu'$. Since $\Phi(A, S) = \Phi(A)$ we know also that $\mu \sqsubseteq_A \mu'$.

Then we have directly $\pi \sqsubseteq_A \pi'$. We prove by induction on $\pi \sqsubseteq_A \pi'$ that for all $S, \vdash A, S + \pi'.Q = A, S + \pi'.Q + \pi.Q$.

- Reflexivity of $\sqsubseteq$ is handled by the fact that $+$ is idempotent.

- Transitivity (e.g. $\pi_3 \sqsubseteq_A \pi_2 \sqsubseteq_A \pi_1$) is handled by monoid laws for $+$. We write $Q_i$ for $\pi_i.Q$ below. We know by induction that:

(1) $\vdash A, S + Q_1 = A, S + Q_1 + Q_2$ (for all $S$) and

(2) $\vdash A, S + Q_2 = A, S + Q_2 + Q_3$ (for all $S$). Then:

$$ \vdash A, S + Q_1 = (1) $$

$$ \vdash A, S + Q_1 + Q_2 = (\equiv) $$

$$ \vdash A, (S + Q_1) + Q_2 = (2) $$

$$ \vdash A, (S + Q_1) + Q_2 + Q_3 = (\equiv) $$

$$ \vdash A, (S + Q_3) + Q_1 + Q_2 = (1) $$

$$ \vdash A, (S + Q_3) + Q_1 = (\equiv) $$

$$ A, S + Q_1 + Q_3 $$

so now we can only have to prove it for $\pi \sqsubseteq \varphi \pi'$ when $A \vdash \varphi$. Note that using the reasoning about we can work up to transitivity.

- We now decompose $\sqsubseteq \varphi$ when $A \vdash \varphi$. Lemma 25 tells us<fnref n="3" /> there are some $\varphi_1, \dots, \varphi_n \in A$ and a reflexive $\psi$ such that $\sqsubseteq \varphi = \sqsubseteq \psi \sqsubseteq \varphi_1 \dots \sqsubseteq \varphi_n$ so in fact we only need to prove the result when $\varphi$ is actually in $A$ or when it is reflexive:

• $\varphi$ is reflexive and $\alpha(x) \sqsubseteq^a \alpha(x)$: nothing to do ($+$ idempotent)

• $\varphi$ is reflexive and $\{a\}(x) \sqsubseteq^a \{a\}(x)$: Law L16

• $\varphi \in A$ and $\alpha(x) \sqsubseteq^{\beta \le \alpha} \beta(x)$: this yields several cases:

* $a(x) \sqsubseteq^b \alpha b(x)$: Law L18

* $\{a\}(x) \sqsubseteq^a \{b\}(x)$: Law L19

* $\{a\}(x) \sqsubseteq^a \{b\} b(x)$: decompose $a \gamma b$ back into $u/a \mid u/b$ (Law L30) then from $b(x)$ get $u(x)$ by L18, then $\{u\}(x)$ (L16) and then $\{a\}(x)$ (L19).

• $\varphi$ is reflexive and $[\varphi_1]\tau \sqsubseteq^\varphi [\varphi_2]\tau$: either $+$ idempotent or L15 is sufficient.

• $\varphi \in A$ and $[\varphi_1]\tau \sqsubseteq^\varphi [\varphi_2]\tau$ when $\varphi_1, \varphi \vdash \varphi_2$: this yields several cases again, we can break $\vdash$ into compositions of $\vdash^i$, again reasoning up to transitivity:

<footnote n="3">³ in fact, the $\psi$ is not absolutely necessary, but we make this analysis using a more precise version of $\sqsubseteq$ using $\vdash^i$ instead of $\vdash$ so the case analysis is less verbose</footnote>
* $[a \le b] \tau \sqsubseteq^b \le^c [a \le c] \tau$: instance of L21

* $[a \le c] \tau \sqsubseteq^b \le^c [a \gamma b] \tau$: instance of L23 (using L17)

* $[a \gamma b] \tau \sqsubseteq^c \le^a [c \gamma b] \tau$: instance of L22

* $[a \gamma b] \tau \sqsubseteq^c \le^b [a \gamma c] \tau$: instance of L22 (using L17)

* $[b \le c] \tau \sqsubseteq^a \le^b [a \le c] \tau$: instance of L20

* $[b \le c] \tau \sqsubseteq^a \le^c [a \gamma b] \tau$: instance of L23

* $[c \le a] \tau \sqsubseteq^a \gamma b [c \gamma b] \tau$: same as below

* $[c \le b] \tau \sqsubseteq^a \gamma b [a \gamma c] \tau$: from $a \gamma b$ we can get some $u/a$ and $u/b$. Then, from $[a \gamma c] \tau$ we can add the summand $[u \gamma c] \tau$ (L22), then $[c \le u] \tau$ (L15), then $[c \le b] \tau$ (L21). □

Laws L15-L23 can be used to “saturate” the topmost prefixes in sums. We express this using the equivalence below, and rely on Lemma 47 to prove Prop. 49:

**Definition 48 (Head sum normal form, $\asymp_h$).** Given two sum processes $S$ and $T$, we write $S \prec_h T$ whenever for any summand $\pi.P$ of $S$, there exists a summand $\pi.Q$ of $T$ with $\pi.P \sim \pi.Q$. We let $S \asymp_h T$ stand for $S \prec_h T \wedge T \prec_h S$.

**Proposition 49.** Whenever $A^*, S_1 \sim A^*, S_2$, where $S_1, S_2$ are two sum processes, there are $S'_1, S'_2$ s.t. $\vdash A^*, S_i = A^*, S'_i$ (for $i = 1, 2$) and $S'_1 \asymp_h S'_2$.

*Proof.* We first use law L13 to replicate $A^*$ under all prefixes in $S_1$ and $S_2$, which is useful later in the proof. We therefore suppose that for any summand $\pi.P$ of $S_1$ or $S_2$, $P = A^* | P_0$ for some $P_0$.

We prove the following property:

$$ \frac{A^*, S_1 \sim A^*, S_2}{\pi.P \in S_1} \Rightarrow \exists Q \quad \begin{array}{l} \vdash A^*, S_2 = A^*, S_2 + \pi.Q \\ \pi.P \sim \pi.Q \end{array} \qquad (1) $$

by running the bisimulation game with a label $\mu$ such that $\pi$ and $\mu$ differ only on their object (that should be fresh in $\mu$): $\pi.P \xrightarrow{\mu} P'$, yielding $A^*, S_1 \xrightarrow{\mu} A^* | P'$; the game returns a transition $A^*, S_2 \xrightarrow{\mu} A^* | Q'$. Using Lemma 47 we get $Q$ such that $A^*, S_2 = A^*, S_2 + \pi.Q$ and $\pi.Q \xrightarrow{\mu} Q'$. We now have to prove that $\pi.P \sim \pi.Q$. There are two cases:

1. if $\mu$ is a visible action, then, by definition of $\sim$, we have $A^* | P' \sim A^* | Q'$. We can now observe that $P' \sim A^* | P'$ and $Q' \sim A^* | Q'$, because $A^*$ has been replicated under prefixes. We thus deduce $P' \sim Q'$, which, by congruence, gives $\mu.P' \sim \mu.Q'$. Using the appropriate law among L24-25, we deduce $\pi.P \sim \mu.P'$ and $\pi.Q \sim \mu.Q'$, which implies $\pi.P \sim \pi.Q$.

2. if $\mu = [\varphi]\tau$ then $\pi = \mu$ and $P' = P$, $Q' = Q$. The bisimulation game yields $\varphi | A^* | P' \sim \varphi | A^* | Q'$ and by the same reasoning as before, $\varphi | P' \sim \varphi | Q'$. By congruence $[\varphi]\tau.(\varphi | P') \sim [\varphi]\tau.(\varphi | Q')$, and by L12, $[\varphi]\tau.P' \sim [\varphi]\tau.Q'$ i.e. $\pi.P \sim \pi.Q$.

We have now (1). Equation (1) implies that $\vdash A^*, S_2 = A^*, S_2 + T_2$ with $S_1 \prec_h S_2 + T_2$ and $T_2 \prec_h S_1$.
Using the symmetry on $S_2 + T_2$ (and not on $S_2$), we get $T_1$ such that $\vdash A^*, S_1 = A^*, S_1 + T_1$ with $S_2 + T_2 \prec_h S_1 + T_1$ and $T_1 \prec_h S_2 + T_2$. Since $S_1 \prec_h S_2 + T_2$ as well, we can conclude $S_1 + T_1 \prec_h S_2 + T_2$ and thus $S'_1 \asymp_h S'_2$ with $\vdash S'_i = S_i + T_i$. $\square$

**Remark 50 (On the definition of $\asymp_h$).** In the definition of $\prec_h$, we impose $\pi.P \sim \pi.Q$, and not simply $P \sim Q$. The equivalence induced by the choice of the latter condition would indeed be too discriminating. To see why, consider $P_0 = a(x).c/x$ and $Q_0 = a(x).0$. Obviously, $c/x \not\sim 0$. On the other hand, we have $P_0 \sim Q_0$: after a $\xrightarrow{a(y)}$ transition on both sides, we must compare $(\nu x)(c/x | y/x)$ and $(\nu x)(y/x)$, and both are bisimilar to 0. In order to derive $\vdash P_0 = Q_0$, we rely on the following property, which explains the shape of laws L24,L25: $a(y).P \sim a(y).Q$ iff $(\nu y)(x/y | P) \sim (\nu y)(x/y | Q)$.

A similar reasoning can be done for the other kinds of visible prefixes.

## 4.4 Laws for Restriction

Laws L26-L29 are standard. The other laws are used to “push” restrictions inside processes. Law L30 is used to eliminate a restriction on a name $a$ in a preorder process, by propagating the information expressed by all $\phi$s that mention $a$. Intuitively, L30 is used after laws L31-L36 have been used to erase all prefixes mentioning the restricted name $a$, pushing the restriction on $a$ inwards. The latter laws describe a kind of “synchronous application” of the prefix laws seen above.

Below are some equalities that are derivable using the laws for restriction:

$$ \begin{array}{l@{\qquad}l@{\qquad}l} (\nu a)(b/a \mid a/c) = b/c & (\nu a)(a/b \mid \bar{a}(x).P) = \{\bar{b}\}(x).P & \bar{a}(x).x = \bar{a}(x).\{x\} \\ (\nu a)(S+a(x).P) = (\nu a)S & (\nu a)(S+b(x).P) = (\nu a)(S+b(x).(\nu a)P) & \text{if } a \neq b \end{array} $$

It can be noted that axiomatisations often treat restriction separately, by first focusing on a restriction-free calculus. In $\pi P$, because of preorders, we cannot in general push restrictions on top of sum processes, so the situation is more complex.

It can be noted that we cannot rely on a law like $(\nu a)(S_1 + S_2) = (\nu a)S_1 + (\nu a)S_2$, for two reasons. On the one hand, we do not allow sum of restricted processes. On the other hand, a restricted process has in general a preorder component in $\pi P$, so the left hand side of the equation would rather look like $(\nu a)(A, S_1 + S_2)$, and we need to exploit the information contained in $A$ when pushing restrictions under prefixes.

We first present a technical lemma about $\Delta$.

**Lemma 51.** Suppose $a \neq b$.

1. If $A \Delta a \leq b$ then for some $x \neq a$, $a \leq x \in A$ and $A \Delta x \leq b$.

2. If $A \Delta b \leq a$ then for some $x \neq a$, $x \leq a \in A$ and $A \Delta b \leq x$.

3. If $A \Delta a \gamma b$ then for some $x \neq a$,

(a) $a \leq x \in A$ and $A \Delta x \gamma b$, or

(b) $\{a \gamma x, x \gamma a, x \leq a\} \cap A \neq \emptyset$ and $A \Delta b \leq x$.
*Proof.* By induction on the derivation of $A \triangleright \cdot$.

**Proposition 52 (Pushing restriction inwards).**

For any $A, S$, where $A$ is a preorder process and $S$ is a sum process, and for any set of names $\tilde{a}$, there exist $A'$ and $S'$, where $S'$ is a sum process and $A'$ is a preorder process such that $\vdash (\nu\tilde{a})(A, S) = A'$, $S'$ and $|(\nu\tilde{a})(A, S)| \ge |A'|, |S'|$.

*Proof.* Using name extrusion, we pull all toplevel restrictions of $A, S$ in order to derive $\vdash A, S = (\nu\tilde{a})(A_0, S_0)$, for some $A_0, S_0$ without toplevel restriction.

We then reason by induction over the number of names in $\tilde{a}$. We apply laws L31-L36 from left to right, until name $a$ does not appear free in any topmost prefix of the sum. At that point, since the restriction on $a$ has been pushed under prefixes, $a$ has no free occurrence in the sum. We can thus use name intrusion, so that law L30 can be applied to get rid of the restriction on $a$ on the preorder part of the process.

This operation is iterated until restrictions are pushed under all prefixes, and law L29 can be used to get rid of the restriction. $\square$

It is often the case that axiomatisations for strong bisimilarity are first given for a calculus without restriction and parallel composition, and then extended to a calculus enriched with these operators. In our case, as discussed above, restriction cannot be handled separately from prefixes. We can however prove a result for the calculus without parallel composition.

**4.5 Axiomatisation of Strong Bisimilarity**

The results presented so far can be put together to establish an axiomatisation on the subcalculus of $\pi P$ in which parallel composition is only used to compose preorder processes.

We first present some observations, that follow from the shape of the prefix rules in Figure 1.

**Fact 1**

1. For any $P$ and $Q$, $a(y).P \sim a(y).Q$ iff $(\nu y)(x/y | P) \sim (\nu y)(x/y | Q)$.

2. For any $P$ and $Q$, $\bar{a}(y).P \sim \bar{a}(y).Q$ iff $(\nu y)(y/x | P) \sim (\nu y)(y/x | Q)$.

3. For any $P$ and $Q$, $\{a\}(y).P \sim \{a\}(y).Q$ iff $(\nu y)(y/x | P) \sim (\nu y)(y/x | Q)$.

4. For any $P$ and $Q$, $\overline{\{a\}(y).P} \sim \overline{\{a\}(y).Q}$ iff $(\nu y)(x/y | P) \sim (\nu y)(x/y | Q)$.

The grammar $P ::= A, \sum_i \pi_i.P_i \mid (\nu a)P$ defines what we call *$|-free$ processes*: only arcs are composed, and the non-preorder part is a sum.

**Proposition 53 (Characterisation on the calculus without parallel composition).** For all $|-free$ processes $P$ and $Q$, $P \sim Q$ iff $\vdash P = Q$.

*Proof.* The right to left implication follows from Lemma 45 and congruence of $\sim$.
Suppose now $P \sim Q$. We reason by induction on $|P| + |Q|$.

By Proposition 52, there are sum-only processes $P_0, Q_0$ with no toplevel restriction such that $\vdash P = P_0$ and $\vdash Q = Q_0$.

We then reason up to associativity and commutativity of parallel composition to write $\vdash P_0 = A_1, S_1$ and $\vdash Q_0 = A_2, S_2$. We have $A_1, S_1 \sim A_2, S_2$, which gives, by Proposition 46, $\vdash A_i, S_i = A^*, S_i$ for $i = 1, 2$, for some $A^*$.

We can then apply Proposition 49 to deduce $\vdash A^*, S_i = A^*, S'_i$, for $i = 1, 2$, for some $S'_1, S'_2$ s.t. $S'_1 \asymp_h S'_2$.

To sum up, we have proved until now $\vdash P = A^*, S'_1, \vdash Q = A^*, S'_2$, and $S'_1 \asymp_h S'_2$.

We now prove, by induction over the number of summands in $S'_1$, that for any such summand $\pi.T_1$, there is a summand $\pi.T_2$ in $S'_2$ s.t. $\vdash \pi.T_1 = \pi.T_2$. Once this will be proved, we shall establish the same way the symmetrical property, which will allow us to deduce $\vdash S'_1 = S'_2$.

Suppose then $\pi.T_1$ is a summand of $S'_1$.

We reason by case analysis on the shape of $\pi$, and suppose $\pi = a(x)$. We know, since $S'_1 \asymp_h S'_2$, that there is a summand $a(x).T_2$ of $S'_2$ such that $a(x).T_1 \sim a(x).T_2$. We have $\vdash a(x).T_i = a(y).(\nu x)(y/x \mid T_i)$, for $i = 1, 2$, by Law L24, induction hypothesis (on $(\nu x)(y/x \mid T_1) \sim (\nu x)(y/x \mid T_2)$) and congruence using the context $a(y).$[].

Moreover, since $a(x).T_1 \sim a(x).T_2$, we know, by Fact 1, that $a(y).(\nu x)(y/x \mid T_1) \sim a(y).(\nu x)(y/x \mid T_2)$. This allows us to rely on the induction hypothesis to show $\vdash a(y).(\nu x)(y/x \mid T_1) = a(y).(\nu x)(y/x \mid T_2)$, which gives us, as announced $\vdash \pi.T_1 = \pi.T_2$.

The other cases for the shape of $\pi$ are treated similarly. $\square$

We now move to the full calculus, by taking into account parallel composition. As is usually the case, this relies on a law for expansion.

The following result states that any process is equivalent to a process that can be written without using parallel composition. Intuitively, such a process can be viewed as a “sum-only process with restriction”.

We can remark that expanding processes involves the introduction of restrictions (in the third sum law L7).

**Lemma 54.** For any $P$, there exists a $|-\text{free process } Q$ s.t. $\vdash P = Q$.

*Proof.* First write $\vdash P = A, P_1$ using the monoid laws for parallel composition. Then, by induction on $|P_1|$, we build $S$ such that $\vdash P_1 = S$ and $|P_1| = |S|$ using law L7. $\square$

We can then extend Proposition 53 to the whole $\pi P$ calculus:

**Theorem 55 (Axiomatisation of $\sim$ in $\pi P$).**

For all $\pi P$ processes $P$ and $Q$, $P \sim Q \iff \vdash P = Q$.

*Proof.* The theorem follows by Proposition 53 and Lemma 54.
*Remark 56 (Discussion about normal forms).* The proofs of the results in this section suggest that we can define a strategy to apply the rules of Figure 2, in order to rewrite a πP process P to its normal form, nf(P), so that P ~ Q iff nf(P) = nf(Q).

For preorder processes, the saturated form is a normal form for ~: if $A_1 \sim A_2$, then, by Proposition 46, $\vdash A_1^* = A_2^*$. By contrast, the proof of Proposition 49 does not compute a canonical form for sum processes. For instance, from the equivalence

$$b/a \mid c/a \mid \bar{a}(x).0 \sim b/a \mid c/a \mid \bar{a}(x).0 + \bar{b}(x).0,$$

Proposition 49 rewrites these processes into $b/a \mid c/a \mid \bar{a}(x).0 + \bar{b}(x).0$, but not into $b/a \mid c/a \mid \bar{a}(x).0 + \bar{b}(x).0 + \bar{c}(x).0$, which could be seen as a normal form for ~, obtained by saturating the sum. Actually, the normal form could even be

$$b/a \mid c/a \mid \bar{a}(x).0 + \bar{b}(x).0 + \bar{c}(x).0 + \{\bar{a}\}(x).0 + \{\bar{b}\}(x).0 + \{\bar{c}\}(x).0,$$

by virtue of several applications of (the counterpart for output of) law L16 with $\pi_1$ an output prefix and $\pi_2$ a protected output.

We leave the rigorous description of this normalisation procedure for future work.

## 4.6 Adapting our Axiomatisation to Explicit Fusions

We can reuse the ideas presented above to describe an axiomatisation for barbed congruence in Explicit Fusions (EF, [16]). EF feature *fusion processes*, of the form $a=b$, which can equate names via $\equiv$: we have $a=b | P \equiv a=b | P\{b/a\}$.

We refer to Appendix C for a description of the axiomatisation.

## 5 Conclusions and Future Work

Working with an preorder on names, using arc processes, has an influence on the behavioural theory of πP, notably through the interplay between arcs and restrictions. The preorder relation between names is represented explicitly in πP processes, using arcs. We do not see any natural “implicit version” of πP, mimicking the relation between Explicit Fusions and Fusions, whereby the extension of the preorder along a communication would not generate an arc.

The stateful nature of the preorder component of πP processes can be related to *frames* in the applied π-calculus [1] and *assertions* in Psi-calculi [2]. Liu and Lin’s proof system for applied π [11] is rather different from our axiomatisation for πP, but has in common the “state component” of processes. One could expect that the same would hold for an equational presentation of bisimilarity in Psi-calculi, possibly relying on some hypotheses on the assertions in order for an axiomatisation to be definable.

Among the natural extensions of this work is the study of the weak version of behavioural equivalence. One fundamental use of types is to help reasoning about processes. With the behavioural theory in the untyped setting in place,
we could study *typed behavioural equivalence*, building on the type system of [8].
Works like [14,5] should be relevant in this direction.

The behavioural theory of πP is based on an operational account. An in-
triguing question is the construction of a denotational model for πP, and the
comparison with known model for π and Fusions.

*Acknowledgements.* We thank Davide Sangiorgi and Fu Yuxi for useful discus-
sions about behavioural equivalence in πP. This work has been supported by
project ANR 12IS02001 PACE and NSF of China (61261130589).

References

1. M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In *Proc. of POPL*, pages 104–115. ACM, 2001.

2. J. Bengtson, M. Johansson, J. Parrow, and B. Victor. Psi-calculi: Mobile processes, nominal data, and logic. In *LICS*, page 39–48. IEEE, 2009.

3. M. Boreale, M. G. Buscemi, and U. Montanari. D-fusion: A distinctive fusion calculus. In *Proc. APLAS*, volume 3302 of *LNCS*, pages 296–310. Springer, 2004.

4. M. Boreale, M. G. Buscemi, and U. Montanari. A general name binding mechanism. In *Proc. TGC*, volume 3705 of LNCS, pages 61–74. Springer, 2005.

5. Y. Deng and D. Sangiorgi. Towards an algebraic theory of typed mobile processes. In *Theor. Comput. Sci.*, 350(2-3):188-212, 2006.

6. Y. Fu. The χ-calculus. In *APDC*, pages 74–81. IEEE Computer Society, 1997.

7. P. Gardner and L. Wischik. Explicit fusions. In *MFCS*, volume 1893 of LNCS, pages 373–382. Springer, 2000.

8. D. Hirschkoff, J.-M. Madiot, and D. Sangiorgi. Name-passing calculi: From fusions to preorders and types. In *LICS*, pages 378–387. IEEE Computer Society, 2013.

9. D. Hirschkoff, J.-M. Madiot, and X. Xu. Long version of this paper. Available from http://madiot.org.

10. C. Laneve and B. Victor. Solos in concert. *Mathematical Structures in Computer Science*, 13(5):657–683, 2003.

11. J. Liu and H. Lin. Proof system for applied pi calculus. In *Proc. IFIP TCS*, volume 323 of *IFIP Advances in Inf. and Comm. Technol.*, pages 229–243. Springer, 2010.

12. J. Parrow and D. Sangiorgi. Algebraic theories for name-passing calculi. *Inf. Comput.*, 120(2):174–197, 1995.

13. J. Parrow and B. Victor. The fusion calculus: expressiveness and symmetry in mobile processes. In *LICS*, pages 176–185. IEEE, 1998.

14. B. C. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. *Mathematical Structures in Computer Science*, 6(5):409–453, 1996.

15. D. Sangiorgi and D. Walker. *The Pi-Calculus: a theory of mobile processes*. Cambridge University Press, 2001.

16. L. Wischik and P. Gardner. Strong bisimulation for the explicit fusion calculus. In *Proc. of FoSSaCS*, volume 2987 of LNCS, pages 484–498, 2004.
# Appendix

## A LTS for a Variant of $\pi P$ with Free Prefixes

We call $\pi P_F$ the variant of $\pi P$ defined by the following grammar, that includes primitive free prefixes (the grammar differs from the one of $\pi P$ only in the definition of prefixes):

$$ \varphi ::= a \leq b \mid a \gamma b \qquad \alpha, \beta ::= a \mid \{a\} \qquad \pi ::= \alpha b \mid \bar{\alpha} b \mid [\varphi]\tau $$

$$ P, Q ::= P \mid Q \mid (\nu a) P \mid a/b \mid \sum_{i \in I} \pi_i . P_i $$

We present below an LTS similar to the one of the $\pi$-calculus as far as restriction is concerned: there are now scope rules. In the following, $\hat{a}, \hat{b}$ range over sets of names that can be either a singleton or empty. When this set is $\{a\}$, we write $(\nu \hat{a})$ for $(\nu a)$ and otherwise for nothing.

Labels: $\mu ::= \bar{\alpha}b \mid \alpha b \mid (\nu b)\bar{\alpha}b \mid (\nu b)\alpha b \mid [\varphi]\tau$.

$$ \begin{array}{l} \overline{\pi.P \xrightarrow{\pi} F P} \rightarrow_{F-PREF} \frac{P \xrightarrow{[\varphi_2]\tau} F P' \quad P \triangleright \Gamma \quad \Gamma, \varphi_1 \vdash \varphi_2}{P \xrightarrow{[\varphi_1]\tau} F P'} \rightarrow_{F-TAU-\Delta} \\ \frac{P \xrightarrow{(\nu \hat{c})\alpha c} F P' \quad P \triangleright \alpha \leq \beta}{P \xrightarrow{(\nu \hat{c})\beta c} F P'} \rightarrow_{F-IN-\Delta} \frac{P \xrightarrow{(\nu \hat{c})\bar{\alpha} c} F P' \quad P \triangleright \alpha \leq \beta}{P \xrightarrow{(\nu \hat{c})\bar{\beta} c} F P'} \rightarrow_{F-OUT-\Delta} \\ \frac{P \xrightarrow{(\nu \hat{b})\bar{\alpha} b} F P' \quad Q \xrightarrow{(\nu \hat{d})\gamma d} F Q'}{P \mid Q \xrightarrow{[\alpha \gamma]\tau} F (\nu \hat{b})(\nu \hat{d})(b/d \mid P' \mid Q')} \rightarrow_{F-COM-L} \frac{\emptyset = \hat{b} \cap \hat{d} = \hat{b} \cap \mathrm{fn}(Q) = \hat{d} \cap \mathrm{fn}(P)}{P \mid Q \xrightarrow{[\alpha \gamma]\tau} F (\nu \hat{b})(\nu \hat{d})(b/d \mid P' \mid Q')} \rightarrow_{F-COM-L} \\ \frac{P \xrightarrow{\mu} F P' \quad a \notin n(\mu)}{(\nu a) P \xrightarrow{\mu} F (\nu a) P'} \rightarrow_{F-RES} \frac{P \xrightarrow{\mu} F P' \quad \mu \in \{\gamma a, \bar{\gamma} a\}}{(\nu a) P \xrightarrow{(\nu a)\mu} F P'} \rightarrow_{F-OPEN} \\ \frac{P \xrightarrow{\mu} F P' \quad \mathrm{bn}(\mu) \cap \mathrm{fn}(Q) = \emptyset}{P \mid Q \xrightarrow{\mu} F P' \mid Q} \rightarrow_{F-PAR-L} \frac{\pi_i . P_i \xrightarrow{\mu} F P'}{\sum_j \pi_i . P_j \xrightarrow{\mu} F P'} \rightarrow_{F-SUM} \end{array} $$

The LTS above induces the following notion of bisimilarity:

**Definition 57 (F-bisimilarity).** A symmetric relation $\mathcal{R}$ is an F-bismimulation iff $P \mathcal{R} Q$ implies

1. for all $\varphi$, $P \triangleright \varphi$ implies $Q \triangleright \varphi$;
2. if $P \xrightarrow{(\nu\hat{b})\bar{\alpha}b} \bar{F} P'$, there is $Q'$, $c$ and $\hat{c}$ s.t.

$$Q \xrightarrow{(\nu\hat{c})\bar{\alpha}c} \bar{F} Q' \text{ and } (\nu\hat{b})(P' | b/f) \mathcal{R} (\nu\hat{c})(Q' | c/f) \text{ with } f \text{ fresh;}$$

3. if $P \xrightarrow{(\nu\hat{b})\alpha b} \bar{F} P'$, there is $Q'$, $c$ and $\hat{c}$ s.t.

$$Q \xrightarrow{(\nu\hat{c})\alpha c} \bar{F} Q' \text{ and } (\nu\hat{b})(P' | f/b) \mathcal{R} (\nu\hat{c})(Q' | f/c) \text{ with } f \text{ fresh;}$$

4. if $P \xrightarrow{[\varphi]\tau} \bar{F} P'$, there is $Q'$ s.t. $Q \xrightarrow{[\varphi]\tau} \bar{F} Q'$ and $P' | \varphi \mathcal{R} Q' | \varphi$.

F-bisimilarity, written $\sim_{\bar{F}}$, is the greatest F-bisimulation.

**Remark 58.** First one could feel that if $P \xrightarrow{\bar{\alpha}b} \bar{F} P'$ and $P \sim Q$ and $Q$ answered as $Q \xrightarrow{\bar{\alpha}c} \bar{F} Q'$, then we should have required that $Q' \triangleright c \le b$. This is a fair requirement, and is already taken care of by the condition $P' | b/f \sim Q' | c/f$. Indeed, $(P' | b/f) \triangleright f \le b$ so we must have $(Q' | c/f) \triangleright f \le b$, and the only way it can entail $f \le b$ is through $c$ (since $f$ is fresh), so we must have $Q' \triangleright c \le b$.

**Proposition 59.** Define $[\alpha(x).P] = (\nu x)\alpha x.[P]$ and $[\bar{\alpha}(x).P] = (\nu x)\bar{\alpha} x.[P]$. For any $P, Q, P \sim Q$ iff $[P] \sim_{\bar{F}} [Q]$.

*Proof.* In all the following, we assume $x$ is fresh. We also use $P, Q, R$ instead of the same letter for the different clauses to ease reference to them. We first prove a tight operational correspondence from $\pi_P$ to $\pi_{P_F}$:

- if $P \triangleright \varphi$ then $[P] \triangleright \varphi$,

- if $P \xrightarrow{\bar{\alpha}(x)} P'$ then for some $y, P_2: P' \equiv (\nu y)(y/x | P_2)$ and $[P] \xrightarrow{(\nu y)\bar{\alpha}y} \bar{F} [P_2]$,

- if $Q \xrightarrow{\alpha(x)} Q'$ then for some $z, Q_2: Q' \equiv (\nu z)(x/z | Q_2)$ and $[Q] \xrightarrow{(\nu z)\alpha z} \bar{F} [Q_2]$,

- if $R \xrightarrow{[\varphi]\tau} R'$ then $[R] \xrightarrow{[\varphi]\tau} \bar{F} [R_2]$ for some $R_2$ such that $R_2 \sim R'$.

and another from $\pi_{P_F}$ back to $\pi_P$ (note that the object $y$ is always bound, and that $x$ can be universally quantified, especially it can be $f$):

- if $[P] \triangleright \varphi$ then $P \triangleright \varphi$,

- if $[P] \xrightarrow{(\nu y)\bar{\alpha}y} \bar{F} P_1$ then for some $P_2, P \xrightarrow{\bar{\alpha}(x)} \equiv (\nu y)(y/x | P_2)$ and $P_1 = [P_2]$,

- if $[Q] \xrightarrow{(\nu z)\alpha z} \bar{F} Q_1$ then for some $Q_2, Q \xrightarrow{\alpha(x)} \equiv (\nu z)(x/z | Q_2)$ and $Q_1 = [Q_2]$,

- if $[R] \xrightarrow{[\varphi]\tau} \bar{F} R_1$ then $R_1 = [R_2]$ for a $R'$ such that $R_2 \sim R'$ and $R \xrightarrow{[\varphi]\tau} R'$.

These two correspondences describe the basic steps necessary to prove that $\{([P], [Q]) | P \sim Q\}$ is a F-bisimulation and that $\{(P, Q) | [P] \sim_{\bar{F}} [Q]\}$ is a bisimulation up to bisimilarity, to finally prove $P \sim Q$ iff $[P] \sim_{\bar{F}} [Q]$.

The correspondence from $\pi_P$ to $\pi_{P_F}$ goes without problem. The $R_2 \sim R'$ condition comes from the fact $(\nu x)(y/x | x/z)$ must be transformed into the bisimilar process $y/z$ when composing $P'$ and $Q'$ into $(\nu x)(P' | Q')$:

$$ \begin{aligned} R' = (\nu x)(P' | Q') &\equiv (\nu x)((\nu z)(x/z | Q_2) | (\nu y)(y/x | P_2)) \\ &\equiv (\nu y z)((\nu x)(y/x | x/z) | Q_2 | P_2) \\ &\sim (\nu y z)(y/z | Q_2 | P_2) = R_2 \end{aligned} $$

In fact, the same reasoning (and the same equation) apply when proving the operational correspondence from $\pi_{P_F}$ back to $\pi_P$. $\square$
Types

$$T ::= 1 \mid iT \mid oT \mid \sharp T \mid \overline{oT} \mid \overline{iT}$$

Subtyping

$$\begin{array}{lclcl}
\overline{\sharp T} \leq iT & \qquad & \overline{\sharp T} \leq oT & \qquad & oT \leq \overline{iT} \\
\overline{iT} \leq iU & \qquad & \overline{iU} \leq iT & \qquad & iT \leq \overline{oT} \\
\qquad & \qquad & \overline{oU} \leq oT & \qquad & \overline{oT} \leq \overline{oU} \\
\qquad & \qquad & \qquad & \qquad & iT \leq \overline{iT} \\
\end{array}$$

Typing rules

$$\begin{array}{lclcl}
\frac{\Gamma \vdash a : oT \qquad \Gamma, x : T \vdash P}{\Gamma \vdash \overline{a}(x) . P} & \qquad & \frac{\Gamma \vdash a : iT \qquad \Gamma, x : T \vdash P}{\Gamma \vdash a(x) . P} & & \\
\frac{\Gamma \vdash a : \overline{oT} \qquad \Gamma, x : T \vdash P}{\Gamma \vdash \overline{\{a\}}(x) . P} & \qquad & \frac{\Gamma \vdash a : \overline{iT} \qquad \Gamma, x : T \vdash P}{\Gamma \vdash \overline{\{a\}}(x) . P} & \qquad & \frac{\Gamma(a) \leq \Gamma(b)}{\Gamma \vdash a/b} \\
\frac{\Gamma \vdash P}{\Gamma \vdash [\varphi] \tau . P} & \qquad & \frac{\Gamma \vdash P \qquad \Gamma \vdash Q}{\Gamma \vdash P \mid Q} & \qquad & \frac{\Gamma \vdash P \qquad \Gamma \vdash Q}{\Gamma \vdash P + Q} \\
\end{array}$$

<caption>**Fig. 3.** A type system for capabilities and cocapabilities</caption>

## B A Type System with Cocapabilities

Figure 3 presents a type for $\pi P$ with *cocapabilities*. Cocapability types are of the form $\overline{oT}$ and $\overline{iT}$, and are used to type protected prefixes.

We have the expected property of type preservation:

**Proposition 60 (Subject reduction).** If $\Gamma \vdash P$ and $P \mapsto P'$, then $\Gamma \vdash P'$.

As with capabilities, a typing hypothesis of the form $a : \overline{iT}$ provides only the right to perform a protected input at $a$. It is possible, for instance, to derive

$$a : \overline{iT}, b : oT \vdash \{a\}(x) \cdot \overline{bx} \cdot 0.$$

Note that it is *not* possible to derive a similar judgement using the encoding of protected prefixes:

$$a : \overline{iT}, b : oT \nvDash (\nu u)(u/a \mid u(x) \cdot \overline{bx} \cdot 0).$$

We leave for future work the investigation of a typed behavioural equivalence based on this type system (intuitively, types can help reasoning about the behaviour processes by constraining the observation capabilities of contexts).

Another direction worth exploring is a finer study of the type system in a version of $\pi P$ with free prefixes, along the lines of [8]. In particular, we expect that usages of protected names correspond to *negative polarities* (while all names in subject positions are positive in [8]).
## C An Axiomatisation for Explicit Fusions

We show how our ideas can be adapted to the calculus of Explicit Fusions [7]. Accordingly, we adopt a presentation of the calculus that follows the lines of $\pi_P$ as we have introduced it.

The grammar of prefixes, conditions and processes is as follows:

$$ \varphi ::= a=b \qquad \pi ::= \bar{a}(x) \mid a(x) \mid [a=b]\tau \qquad P ::= P|Q \mid \nu a P \mid \Sigma_i \pi_i P_i \mid a=b $$

As in $\pi_P$, we adopt primitive bound prefixes. Free prefixes can be encoded: $[ab.P] = (\nu u)a(u).(u=b | P)$. Note in passing that fusions can be represented in $\pi_P$, encoding $a=b$ with $a/b | b/a$.

The following definition is adapted from the efficient bisimulation of [16]. The LTS is defined according to the approach in Figure 1, except in their LTS $P \xrightarrow{\tau} P'$ does not necessarily imply that $P \xrightarrow{[a=b]\tau} P'$ for every $a$ and $b$. So we have to change the third clause of the definition of bisimulation to take this into account. The way we handle objects does not matter, as the resulting bisimilarity is the same.

**Definition 61** ($\sim_{\text{EF}}$). An efficient bisimulation is a symmetric relation $\mathcal{R}$ such that if $PRQ$ then:

1. $P \triangleright a=b$ iff $Q \triangleright a=b$;

2. $P \xrightarrow{\mu} P'$ implies $Q \xrightarrow{\mu} Q'$ for some $Q'$ s.t. $P'RQ'$, for $\mu \neq [\varphi]\tau$;

3. $P \xrightarrow{[a=b]\tau} P'$ implies $a=b | Q \xrightarrow{\tau} Q'$ and $a=b | P'RQ'$.

We write $\sim_{\text{EF}}$ for the largest efficient bisimulation.

We write $\vdash_{\text{EF}} P = Q$ if the equality can be derived using equational reasoning from the laws of Figure 4.

The axiomatisation is considerably simpler than in $\pi_P$. The stateful component of processes encodes an equivalence relation on names. This makes it possible to reason locally, whereby a form of global reasoning is necessary in the laws of Figure 2 for $\pi_P$.

The fact that fusions are symmetric makes protected names unnecessary and simplifies greatly the handling of restriction. Indeed, laws L31-L35 can be dealt with using the simpler law $(\nu a) \sum_i \pi_i P_i = \sum_{i|a \notin n(\pi_i)} \pi_i.(\nu a)P_i$.

**Lemma 62.** For any $P, a, b$, we can derive $\vdash_{\text{EF}} P | a=b = P\{a/b\} | a=b$.

**Proposition 63.** For any $P, Q$, we have $P \sim_{\text{EF}} Q$ iff $\vdash_{\text{EF}} P = Q$.
Standard structural laws.

$$P | (Q | R) = (P | Q) | R \qquad P | Q = Q | P \qquad P | 0 = P$$

$(\nu a)(P | Q) = P | (\nu a)Q$ and $(\nu b)P = (\nu a)P\{a/b\}$ when $a \notin \text{fn}(P)$

$$(\nu a) \sum_i \pi_i.P_i = \sum_{i|a \notin \text{fn}(\pi_i)} \pi_i.(\nu a)P_i$$

Laws for fusions.

$$a=a=0 \qquad a=b \mid a=c = a=b \mid a=c \mid b=c \qquad a=b=b=a \qquad (\nu a)a=b=0$$

Laws for prefixes.

$$a=b | S + \pi.P = a=b | S + \pi.(a=b | P) \qquad [a=b]\tau.P = [a=b]\tau.(a=b | P)$$
$$\pi.P + \pi.P = \pi.P \qquad [a=b]\tau.P = [b=a]\tau.P \qquad a=b | [a=c]\tau.P = a=b | [b=c]\tau.P$$
$$a=b | S + a(x).P = a=b | S + b(x).P \qquad a=b | S + \bar{a}(x).P = a=b | S + \bar{b}(x).P$$

Expansion law.

$$\begin{align*}
\sum_i \pi_i.P_i \mid \sum_j \rho_j.R_j &= \sum_i \pi_i.(P_i | T) + \sum_j \rho_j.(S | R_j) \\
&\quad + \sum_{i,j} [a=b]\tau.(\nu x)(P_i | R_j) \\
&\text{where } \{\pi_i, \rho_j\} = \{\bar{a}(x), b(x)\}
\end{align*}$$

<caption>Fig. 4. Axiomatisation for the Explicit Fusions calculus</caption>