Abstract Interpretation of Mobile Systems

Jérôme Feret

► To cite this version:

Jérôme Feret. Abstract Interpretation of Mobile Systems. Journal of Logic and Algebraic Programming, 2004, special issue on the pi-calcucus, 63 (1), pp.59-130. 10.1016/j.jlap.2004.01.005. hal-04947676

HAL Id: hal-04947676

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

Submitted on 14 Feb 2025

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
Abstract Interpretation of Mobile Systems<fnref n="1" />

Jérôme Feret

Département d'Informatique de l'École Normale Supérieure,
75230 PARIS Cedex 5, FRANCE

**Abstract**

We propose an Abstract Interpretation-based context-free analysis for mobile systems written in the π-calculus. Our analysis automatically captures a sound – but not complete – description of the potential behavior of a mobile system interacting with an unknown context. It focuses on both the control flow and the occurrence number of agents during computation sequences.

Control flow analysis detects all the possible interactions between the agents of a system, but also the potential interactions with the context. In order to deal with dynamic creation of both names and agents which is an inherent feature of mobility, our analysis distinguishes between recursive instances of the same agent. This way, we are able to prove the integrity of an *ftp*-server used by an unbounded number of clients. Occurrence counting analysis just consists in abstracting the occurrence number of instances of agents. Our abstraction is relational; this makes us able to detect both quickly and precisely mutual exclusion and non-exhaustion of resources.

*Key words:* mobility, π-calculus, static analysis, abstract interpretation, control flow analysis, occurrence counting analysis, worst case analysis.

# 1 Introduction

The development of large scale communicating distributed systems demands the design of methods for analyzing mobile systems. In such systems, agent distribution dynamically changes during computation, making their analysis a very difficult task. Furthermore, the size of these systems, such as the Internet for instance, is large enough to prevent a single person from knowing the whole system. This is why we are interested in validating properties on a

<footnote n="1">¹ This work was supported by the RTD project IST-1999-20527 “DAEDALUS” of the European FP5 programme.</footnote>
mobile system which belongs to a bigger one, called its context, without having
precise knowledge of this context. We propose a fully automatic Abstract
Interpretation-based analysis for detecting and proving some properties of
such mobile systems.

In this study, we focus on mobile systems described in the π-calculus [22, 23]
which is a formalism well suited for understanding the problems related to mo-
bility. The π-calculus describes systems of agents which may interact via the
communication of channel names through channels. When receiving a channel
name, an agent gets some control over this name: it can communicate with
other agents sharing this name or even communicate this name to other agents.
The expressive power of the π-calculus also follows from a replication mecha-
nism, which allows the spawning of number of instances of a same agent. Thus,
each instance of each agent opens its own channels and can then communi-
cate their names to other agents. The semantics of the π-calculus is usually
described up to a congruence relation. This relation allows agents to interact
by solving conflict between channel names and making the agents move in the
syntactic description of the system. Nevertheless, because of this congruence
relation, it would be very difficult to derive an abstraction of the usual se-
mantics of the π-calculus. To solve this problem, we introduce a non-standard
semantics. This non-standard semantics is fully operational (i. e. it requires
no congruence relation). It uses a fresh name allocation scheme, in order to
provide fresh names to opened channels, and describes configurations as sets
of agents, so that the congruence relation is no longer required. Moreover, this
fresh name allocation scheme allows us to encode some interesting properties
in the semantics, such as the fact that two channels have been opened by the
same instance of an agent, or by two successive instances of an agent.

Having chosen the appropriate semantics, we use the Abstract Interpretation
framework to design decidable analyses of the π-calculus. This framework is
highly generic: it can be applied to various analyses, provided some abstract
primitives are given. Moreover, it is extensible: it allows us to build the (ap-
proximated reduced) product of several analyses expressed in this framework.
We then use our framework to address two orthogonal issues: the control flow
and the occurrence counting. Control flow analysis consists in detecting the
set of agent instances that can receive the names of the channels opened by a
given instance of an agent. This analysis is context-free: it will detect which
channel names can be communicated to the context. It is also non-uniform
in the sense that it distinguishes between recursive instances of agents. It can
prove, for instance, that a name can be communicated to only one other in-
stance of an agent, and not to the other ones. In the case of the ftp-server,
it detects that the server can return a query only to the correct client even
in the case where an unbounded number of clients are created. Occurrence
counting analysis consists in abstracting the occurrence number of instances
of agents during computation sequences. It is especially useful to detect mu-
tual exclusion. It also helps in discovering a bound to the number of agents
during computation sequences, so that we can verify that some part of the
systems will not exceed physical limits imposed by the implementation of the
system. In the case of the ftp-server, we can automatically infer the maximum
number of simultaneous client sessions. Our approach relies on the use of a
reduced product between a non-relational and a relational domain. Complex-
ity problems are solved by using approximated algorithms for calculating a
reduction between these two domains.

As a result we get a polynomial analysis which has been implemented in
OCAML. The corresponding prototype can be used on the web at:

http://www.di.ens.fr/~feret/prototypes/prototypes.html.en

Some examples and a short tutorial are also provided.

Related works are discussed in Sect. 2. The standard semantics of the π-calculus is given in Sect. 3. It is first refined in Sect. 4 and extended to open systems in Sect. 5. A generic abstract analysis is designed in Sect. 6. It is instantiated in both Sect. 7 and Sect. 8 to get, respectively, a control flow and an occurrence counting analysis. Complexity results and analysis times are given in Sect. 9.

## 2 Related work

*Flow analysis.* Control flow analyses focus on the explicit flow of information. Nielson *et al.* use abstract interpretation in [1–3] to infer a uniform description of the interactions between agents and apply Seidl’s solver to get a cubic implementation of their analysis in [25]. Hennessy and Riely have designed a type-based analysis with the same expressive power in [19]. These analyses use explicit information flow to detect whether some security constraints specified using a security level cannot be violated. Nevertheless, these analyzes are uniform (or *mono-variant*). They cannot distinguish between distinct instances of the same agent. For example, it is impossible to give distinct security levels to distinct instances of the same agent. System specification could be rewritten so that several instances of a given agent are syntactically distinguished from the others. Therefore, this requires a human intervention to guess which replication have to be syntactically unfolded and how many instances have to be distinguished. Our analysis requires no human analysis, and can find interesting properties even if an arbitrary number of instances have to be distinguished. Moreover, it is not obvious in many cases that there exists a syntactic rewriting of the system so that several different recursive instances can be distinguished on purely syntactic ground and where the security policy
is checkable using purely uniform analyses.

Cardelli et al. use group creation in [4] to assign dependent security levels to channel names. A group can be associated with each recursive instance of an agent, and can then be used to prevent names of channels from exiting the scope of the instance which has opened these channels. Nevertheless, our analysis is much more expressive: we can infer algebraic comparisons between agent instances, which allows us to express the fact that an instance of an agent can only communicate with the next instance of it or with the previous one. As a consequence, we can prove that the name of a channel is sent back to the instance which has previously opened this channel, even if this name is not confined into the scope of this recursive instance.

Venet has already proposed a non-uniform analysis in [30,31]. This analysis infers a sound non-uniform description of the topology of communications between the agents of *friendly systems* [22], in which replication guards cannot be nested and systems are closed. The main contributions with respect to Venet's work are:

(1) the extension of the non-uniform analysis to agents with nested replication guards;

(2) the extension to open systems acting in a possibly unknown context;

(3) the occurrence counting analysis.

*Occurrence counting analysis.* Only very few analyses for counting occurrences of agents have been published. Nevertheless, this problem is very close to the problem of approximating the behavior of a Petri net, and of occurrence counting in mobile ambients. In [18], Nielson et al. propose an exponential analysis for counting occurrences of agents inside ambients. In [26], they use context-dependent counts for inferring a more accurate description of the internal structure of agents, at the expense of a higher time complexity (an exponential number of agents are distinguished). These analyses rely on the use of a non-relational domain to abstract the content of an ambient. Then, they use disjunctive completion, and abstract the set of all the potential contents of a syntactic ambient as the power set of this abstract domain. These two analyses encounter the same problem: in the case that several instances of the same agent may coexist, when one instance of this agent performs a computation step, these analyses cannot decide whether only one or several instances remain after this computation step, so they have to consider the two possible cases, which leads to both a loss of precision and an exponential explosion in complexity. The use of an approximated reduced product between a relational domain and a non-relational domain to globally abstract sets of multi-sets of agents allows us to solve this problem efficiently. Thus we obtain a very accurate analysis which is polynomial in the number of syntactic agents (i.e. polynomial in the size of the initial system configuration).
*Behavioral types.* In [20], Kobayashi and Igarashi use CCS processes as types for mobile systems and check some behavioral invariants expressed in modal logic. Nevertheless, describing causality between actions leads to an explosion of the size of the types. Another problem is that their type system cannot express properties that deal with the dynamic creation of channel names. Rajamani and Rehof have extended this type system in [28], so that it handles dynamic name creation. But type checking is undecidable in general. So, they will have to propose an approximation in future work.

*Modular analysis.* Context-free semantics is an important issue in static analysis. It allows the analysis of only a part of a system, without much knowledge of its context. It can be used to abstract the behavior of an instance of an agent, and detect which names may escape the scope of this part. This can be used to detect dead code, for instance. Rajamani and Rehof propose a modular analysis in [28]. Having abstracted the behavior of two modules, they can calculate an approximation of the parallel composition of them. But this analysis is very restrictive because module types must satisfy some *assume-guarantee* properties.

*Security analysis.* In the Dolev-Yao's model [13], a system is usually proved not to be vulnerable to a given class of attackers. Such classes are then described by a set of rules which explain how an attacker can interact with a system. In our approach, the class of the attacker is actually any system expressed in the π-calculus. The benefit is that our context-free analysis is complete with respect to the model, so that we can use our results to analyze a module. The main drawback of our approach is that we cannot express other attacks. For instance, we could imagine that an attacker could guess some sensitive information, by observing the time of execution of some agents.

## 3 π-calculus

We introduce in this section the π-calculus and a standard semantics for it. The π-calculus is a formalism used to describe mobile systems. It describes a system as a set of agents which exchange information over channels. These communications enable agent synchronization, but also dynamic modification of the system topology: agents can open new channels, they can also pass control over some channels to other agents, and they can even dynamically create other agents. Here, we consider a lazy version of the synchronous polyadic π-calculus [22] with internal choice operator. In the polyadic π-calculus, agents can communicate tuples of channel names. We use the lazy version of replication introduced in [29, Chap. 7]: agent creations are performed only when they are required by a communication. This is not a limitation as full replication can be encoded with lazy replication (Cf. [29, page:102]).
## 3.1 Syntax

Let $\mathcal{N}$ be a countable set of channel names and $\mathcal{L}$ a countable set of labels. The syntax of agents is described in Fig. 1(a). Syntactic components are identified by distinct labels in $\mathcal{L}$. Input guard, replication guard and name restriction act as name binders, i.e in the agents $c^{?j}[x_1, ..., x_n]P, *d^{?j}[y_1, ..., y_p]Q$ and $(\nu x)R$, the occurrences of $x_1, ..., x_n$ in $P, y_1, ..., y_p$ in $Q$ and $x$ in $R$ are bound. We also assume that no name occurs twice in a whole system, as an argument of an input guard, a replication guard or a name restriction. Usual rules about scope, substitution and $\alpha$-conversion apply. We denote by $fn(P)$ the set of free names in $P$, i.e names that are not under the scope of a binder, and by $bn(P)$ the set of bound names in $P$.

## 3.2 Semantics

We now informally introduce the semantics of the $\pi$-calculus. The agent $aP$ first computes the action $a$ before launching the continuation $P$. The agent $(\nu x)P$ opens a new channel, named $x$, the agent $P$ can use this channel for communicating, it can also send the name $x$ to the other agents. In $(P | Q)$, $P$ and $Q$ are two concurrent agents which may behave independently, or interact by communicating. The formula $(P \oplus Q)$ denotes an internal choice between two agents. Either $P$ or $Q$ is run, while the other fades away; the choice between $P$ and $Q$ does not depend on the other agents. The agent $\mathbf{0}$ does nothing. The agent $c^i[x_1, ..., x_n]P$ sends a message via the channel named $c$, this message is the tuple of channel names $(x_1, ..., x_n)$. The agent $c^{?i}[y_1, ..., y_n]P$ waits for a message on the channel named $c$, and binds the channel names $y_1, ..., y_n$ to the received channel names. The agent $*c^{?i}[y_1, ..., y_n]P$ is a *resource*: it replicates itself just before receiving a message: a new instance of $P$ is launched with $y_1, ..., y_n$ bound to the received channel names while $*c^{?i}[y_1, ..., y_n]P$ waits for the next message.

The operational semantics is given by both a congruence relation in Fig. 1(b) and a reduction relation in Fig. 1(c). The congruence relation allows agents to interact, while the reduction relation describes agent computations. Some rules in the congruence relation make agents move inside the syntactic tree: they assert the associativity and commutativity of the parallel composition. Some others extend the scope of names to the agents they are communicated to: $\alpha$-conversion solves conflicts between names, swapping selects the name the scope of which we wish to extend, and extrusion extends its scope to another agent. The reduction relation describes agents' communications. A communication is allowed when there are two concurrent agents, such that the first one sends a message on a channel, while the second one waits for a message on
$P ::= aP$ (action)

| $(\nu x)P$ (name restriction)

| $(P | P)$ (parallel composition)

| $(P \oplus P)$ (internal choice)

| **0** (nil)

$a ::= c!^j[x_1, ..., x_n]$ (output guard)

| $c?^i[x_1, ..., x_n]$ (input guard)

| $*c?^i[x_1, ..., x_n]$ (replication guard)

where $c, x_1, ..., x_n, x \in \mathcal{N}, i, j \in \mathcal{L}$ and $n \ge 0$.

(a) Syntax

($\nu x)P \equiv (\nu y)P[x \leftarrow y]$ if $y \notin fn(P)$ (α-conversion)

$P | Q \equiv Q | P$ (commutativity)

$P | (Q | R) \equiv (P | Q) | R$ (associativity)

$P | 0 \equiv P$ (end of an agent)

($\nu x)0 \equiv 0$ (garbage collecting)

($\nu x)(\nu y)P \equiv (\nu y)(\nu x)P$ (swapping)

($((\nu x)P) | Q \equiv (\nu x)(P | Q)$ if $x \notin fn(Q)$ (extrusion)

where $x, y \in \mathcal{N}$.

(b) Congruence relation

$c!^j[x_1, ..., x_n]P \mid c?^i[y_1, ..., y_n]Q \xrightarrow{(i,j)} P \mid \tilde{Q}$ (comm.)

$c!^j[x_1, ..., x_n]P \mid *c?^i[y_1, ..., y_n]Q \xrightarrow{(i,j)} P \mid \tilde{Q} \mid *c?^i[y_1, ..., y_n]Q$ (replication)

$P \oplus Q \stackrel{\oplus}{\longrightarrow} P$ (left choice)

$P \oplus Q \stackrel{\oplus}{\longrightarrow} Q$ (right choice)

$\frac{P \xrightarrow{\lambda} Q}{(\nu x)P \xrightarrow{\lambda} (\nu x)Q} \qquad \frac{P' \equiv P \quad P \xrightarrow{\lambda} Q \quad Q \equiv Q'}{P' \xrightarrow{\lambda} Q'} \qquad \frac{P \xrightarrow{\lambda} P'}{P \mid Q \xrightarrow{\lambda} P' \mid Q}$

where $c, x, x_1, ..., x_n, y_1, ..., y_n \in \mathcal{N}, i, j \in \mathcal{L}, \lambda \in \{\oplus\} \cup (\mathcal{L} \times \mathcal{L})$, and $\tilde{Q} = Q[y_1 \leftarrow x_1, ..., y_n \leftarrow x_n]$.

(c) Reduction relation

<caption>Fig. 1. Standard operational semantics</caption>
the same channel (we also request that both messages have the same parity). The results of such a communication are obtained by applying the substitution of the λ-calculus in the continuation of the message receiver. When the receiver is a resource, it is just syntactically replicated before performing the communication; this way the resource is still available after the communication. We have labelled each choice reduction step with the symbol $\oplus$ and each communication reduction step with the labels of both agents involved in the communication: this will allow us to relate the state of a system to the history of the computation steps that have led to this state.

### 3.3 Examples

We now propose some examples to illustrate both this semantics and the kind of properties we are interested in. We will find that the semantics we have considered is not precise enough to handle the properties we are interested in.

**Example 1** An ftp-server can be described by the system given in Fig. 2. The first resource repeatedly creates a new client which sends a query to a server. This query is composed of a query **request**, and an address **address**. The client sends its query again in the case that it receives a failure report denoted by the agent **address![]**. The second resource describes the server. When this one receives a query, it replicates itself. Then, either it uses an available port and computes the query or it reports a failure to the client by spawning the agent **address![]**. Available ports are denoted by agents **port![]**. Data processing just consists in a communication between two agents of the server, through the channel the name of which is **deal**: most computational features are abstracted away. After this communication, the port is released, while the answer is sent back to the client. An instance of the agent **email![rep]** is left as a trace of the session.

Our analysis will prove both the integrity and the non-exhaustion of this system: it will discover that each time an agent **email![rep]** is spawned, the names **email** and **rep** are respectively bound to the names of two channels opened by the restrictions ($\nu$ **address**) and ($\nu$ **request**) of the same instance of a resource, and so the server returns its computed answer to the correct client; it also captures the fact that no more than three instances of the syntactic agent **deal![data]** can occur simultaneously, which means that no more than three simultaneous sessions can be active in the same time.

**Example 2** We propose in Fig. 3 a mobile system which creates a ring of processes, with a token passed around this ring. The names of the channels opened by name restrictions ($\nu$ **left0**) and ($\nu$ **right**) denote the processes of the ring. The first part of the system describes the ring creation. The first pro-
<figure><img src="image_2.png" /><figcaption>Fig. 2. An ftp-server</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>Fig. 3. A ring of processes</figcaption></figure>
cess is created by the restriction ($\nu$ left0). An agent mon![v1; v2] denotes a connection between two processes. Then, each time the first resource is replicated, a new process is created and linked to the previous process, which has been passed as an argument of the replication. The second resource replication closes the ring by linking the last created process to the first created process. The second part of the system describes the execution of the processes: an additional resource spawns a resource for each process of the ring. Then a token is put into the ring of processes: the token is denoted by syntactic copies of the agents next![] and left0![]. The name of this agent describes the token location. When the token is available, the corresponding process can replicate its resource, and as a result the process enters its critical section. The critical section is exited when the two agents crit![] and crit?[] have interacted; the token is then passed to the next process.

Our analysis can prove both the integrity and the non-exhaustion of this system: it discovers that each time an agent mon![left;right] is spawned, either the name left is linked to the channel opened by the restriction ($\nu$ left0), or both names left and right are linked to two channels opened by instances of the restriction ($\nu$ right), but the channel linked to the name left has been opened by the previous instance of it, which means that a process of the ring can only be connected to either the first one or to the next one; it captures the fact that only one simultaneous instance of the syntactic agent crit![] can exist. That is to say, that only one process of the ring can enter its critical section at a given time.

**Remark 3** The standard semantics is not well suited to express and capture integrity properties, because the link between agent instances and the names of the channel they have opened is not encoded explicitly. For instance, if we think about the example of the ftp-server and if we cleverly choose the names of opened channels by indexing them with the instance number of the client resource, we obtain after two sessions of the server a system of the following form<fnref n="2" />:

$$ (\nu \bar{c})(\nu \text{ address}_1)(\nu \text{ request}_1)(\nu \text{ address}_2)(\nu \text{ request}_2) \\ (S' | \text{address}_1)!^{10}[\text{request}_1] | \text{address}_2)!^{10}[\text{request}_2]). $$

It appears explicitly that request answers are returned at good addresses. However, we could have chosen the names differently and obtained the following $\alpha$-equivalent configuration:

$$ (\nu \bar{c})(\nu \text{ address}_2)(\nu \text{ request}_1)(\nu \text{ address}_1)(\nu \text{ request}_2) \\ (S' | \text{address}_2)!^{10}[\text{request}_1] | \text{address}_1)!^{10}[\text{request}_2]) $$

<footnote n="2">² This term only shows explicitly the information we are interested in. The variable $S'$ denotes the rest of the system and the notation ($\nu \bar{c}$) denotes a sequence of restrictions for all implicit names.</footnote>
in which this property is lost.

The link between the recursive instances of an agent and the names of the channels they have opened could be easily hard-coded: it would be enough to open a new channel named **p** for each recursive instance of an agent, and then encoding the relation that this instance has opened a given channel name **n** by spawning an agent **has-opened**![^p; n], where **has-opened** is the name of a channel opened at the beginning of the system computation. Nevertheless, it would be very difficult to abstract this relation. All the more so since we are also interested in more complex properties, such as whether two channels have to be opened by two successive instances of an agent. Moreover, we do not know statically which complex properties are required to prove easier ones.

The purpose of the next section is to design a semantics in which channel name origin is carefully traced and can easily be abstracted.

# 4 Refining the semantics

The non-standard semantics is a refined semantics which aims at explicitly specifying the links between the channels and the instances of agents which have opened them. Any instance of an agent is identified unambiguously by a marker in order to distinguish that instance from all others. Each time a channel is opened, the name of this channel is tagged with the marker of the agent instance which has opened this channel, so that the origin of channel names is easily traced. Venet, in [31], has presented such a non-standard semantics, but it applies only to a small part of the π-calculus, called the *friendly systems* [22]. In particular, it requires replication guards not to be nested, and the system to be closed. We propose here a new non-standard semantics in order to relax those restrictions.

This section will be organized as follows: we first describe our marker allocation scheme, then we propose a naive fully operational semantics for describing the behavior of closed mobile systems, and we finally improve this semantics in order to reduce the number of computation steps. We deal with open systems in the next section.

## 4.1 Fresh name allocation

As explained before, α-conversion prevents expressing the link between recursive instances and the names of the channels they have opened. To avoid the use of α-conversion, we propose a name allocation scheme which ensures the
freshness of allocated names. Such a scheme has already been proposed by
De Bruijn in [11]. Nevertheless, our requirement is quite different. De Bruijn's
naming scheme allows α-conversion to be avoided, in order to simplify some
manual proofs. We also expect our scheme to allow us to express some in-
tegrity properties. For instance, we would like to express in our semantics the
fact that two names are denoting channels which have been opened by the
same instance of a given agent. Furthermore, as we want to make static anal-
yses, we want to capture invariants on allocated markers. For that purpose,
we want the scheme not to depend on the interleaving order. To solve that
problem, we propose to tag each instance of agent by a marker which encodes
the history of the replications which have led to its creation. Each name will
then be tagged with the marker of the agent which has opened the channel
denoted by this name.

We denote by $\mathcal{M}$ the set of all binary trees the leaves of which are all labelled with $\varepsilon$ and the nodes of which are labelled with pairs $(i, j)$ where both $i$ and $j$ are in $\mathcal{L}$. The tree having a node labelled with $a$, a left sibling $t_1$ and a right one $t_2$ is denoted by $N(a, t_1, t_2)$. Markers are binary trees in $\mathcal{M}$. Initial agent instances are tagged with the marker $\varepsilon$, while the marker of each new agent instance is calculated recursively from the marker of the agent instances the computation of which has lead to its creation:

* when a computation step does not involve replicating a resource, the marker of the computed agent is just passed to its continuation;

* when a resource is replicated, a new marker is deterministically allocated to the spawned instance: it is given by $N((i, j), id_i, id_j)$ where $i$ is the label of the resource, $id_i$ is the marker of the resource, $j$ is the label of the agent instance which replicates the resource and $id_j$ is the marker of this agent instance.

Marker allocation consistency is expressed by the following proposition:

**Proposition 4** *During each computation sequence, two distinct instances of the same agent are always tagged with distinct markers.*

**PROOF.** The proof of Prop. 4 can be made by induction on the length of the computation sequence. It relies on the fact that each tagged agent instance contains explicitly both the label and the markers of an agent instance which has necessarily been consumed to spawn this instance. $\square$

Moreover, in accordance with the following proposition, we can simplify the
shape of the markers without losing marker allocation consistency:
**Proposition 5** Let $\phi_1$ and $\phi_2$ be the two following functions:

$$ \phi_1: \left\{ \begin{array}{rcl} \mathcal{M} & \to & (\mathcal{L}^2)^* \\ N(a, b, c) & \mapsto & \phi_1(c).a \\ \varepsilon & \mapsto & \varepsilon \end{array} \right. $$

$$ \phi_2: \left\{ \begin{array}{rcl} \mathcal{M} & \to & \mathcal{L}^* \\ N((i, j), b, c) & \mapsto & \phi_2(c).j \\ \varepsilon & \mapsto & \varepsilon. \end{array} \right. $$

Marker allocation remains consistent when replacing each marker by its image by $\phi_1$ or $\phi_2$.

Such simplifications allow us to reduce the cost of our analysis, but also lead to a loss of accuracy, since they merge information related to distinct computation sequences of the system.

**Example 6** Coming back to the example of the ftp-server, with this allocation scheme, the first instance of the client resource will be tagged with the marker $id_1 = N((1, 16), \varepsilon, \varepsilon)$, while the second instance will be tagged with the marker $id_2 = N((1, 5), \varepsilon, N((1, 16), \varepsilon, \varepsilon))$. So that the configuration reached after two sessions of the server will be of the following form:

$$ (\nu \bar{c})(\nu \text{ address}_{id_1})(\nu \text{ request}_{id_1})(\nu \text{ address}_{id_2})(\nu \text{ request}_{id_2}) \\ (S' | \text{ address}_{id_1}!)^{10}[\text{ request}_{id_1}] | \text{ address}_{id_2}!)^{10}[\text{ request}_{id_2}], $$

where the names are indexed by the marker of the threads which have opened the channels they denote. We did not indicate the marker of agent instances which depends on the number of attempts required to establish the connection with the server. It appears explicitly that the names **address**$_{id_i}$ and **request**$_{id_i}$ communicated to an instance of the agent labelled **10** denote two channels opened by the same recursive instance of an agent.

## 4.2 Naive semantics

We now propose a fully operational semantics of the $\pi$-calculus, in which the channel names are allocated in accordance to the previously proposed fresh name allocation scheme. Furthermore, we get rid of the congruence relation by orienting it, and simulating it by additional operational rules.

### 4.2.1 Definition

Let us first consider the case of a closed mobile system $S$ in the $\pi$-calculus. The subset of $\mathcal{L}$ used in labeling $S$ is denoted by $\mathcal{L}_{\text{used}}$. A non-standard configuration is a set of thread instances, where a thread instance is a triplet composed of a syntactic component, a marker and an environment. The syntactic component is a copy of a sub-term of $S$, the marker is calculated at
the creation of the thread and the environment specifies the semantic value of each free name of the syntactic component: it maps each free name of the syntactic component to a pair $(x, id)$, where $x$ is a bound name of $S$ and $id$ is a marker. Intuitively, $(x, id)$ refers to the name of the channel opened by the instance of the restriction $(\nu x)$ tagged with the marker $id$. While threads are running, environments are calculated in order to mimic the standard semantics. The translation of a labelled system $S$ into a set of initial threads and non-standard computation rules are given in Fig. 4.

Roughly speaking, the initial configuration contains only one thread: the system itself, tagged with the marker of the initial thread, $\epsilon$. Since the system is closed, its environment is empty. Structural rules mimic and orient the congruence relation. A thread the syntactic component of which is composed of two concurrent agents can be replaced by the two corresponding threads. Name restriction consists in opening a channel denoted by a fresh name, and binding the corresponding variable to this name in the environment of the continuation. The fresh name is obtained by tagging the name used in the restriction by the marker of the agent which has opened the corresponding channel. A thread the syntactic component of which is the empty agent can be removed. Choice rules mimic choice reduction rules. A thread the syntactic component of which is a choice between two agents can be replaced by a thread corresponding to one of these agents. Communication rules mimic communication reduction rules. The synchronization condition is checked in the environment of the communicating threads. Name passing is described by explicit substitution in environments. In the case that a resource is replicated, a fresh marker is inferred in accordance with our marker allocation scheme.

**Example 7** We consider the following system:

$$ (\nu a)(*a^1[]((\nu b)(b!^2[b]0 | a!^3[]0)) | a!^4[]0), $$

and propose a computation sequence for it in the naive non-standard semantics in Fig. 5. The initial state $C_0$ is just a single thread the syntactic component of which is the system, the marker of which is $\epsilon$ and the environment of which is empty. The first computation step $C_0 \xrightarrow{\epsilon} n C_1$ consists in opening a new channel, named $(a, \epsilon)$, since it is opened using the restriction $(\nu a)$ of a thread the marker of which is $\epsilon$. The second computation step $C_1 \xrightarrow{\epsilon} n C_2$ consists in decomposing the thread into two concurrent threads; thus the marker of the single thread is just passed to both threads. The third computation step $C_2 \xrightarrow{(1,4)} n C_3$ is a communication between the two threads. Since the first one is a resource, it is still available after the communication. The thread which has sent the message is consumed and new threads, corresponding to the continuation of the communicating threads are spawned. The continuation of the resource is tagged with a new marker $N((1,4), \epsilon, \epsilon)$ obtained from both the labels and the markers of both communicating threads, while the marker
$$C_0^n(S) = (S, \varepsilon, \emptyset)$$

(a) Initial configuration

$$C \cup \{(P \mid Q, id, E)\} \xrightarrow{\varepsilon} n C \cup \{(P, id, E_{|fn(P)}); (Q, id, E_{|fn(Q)})\}$$

$$C \cup \{((\nu x)P, id, E)\} \xrightarrow{\varepsilon} n C \cup \{(P, id, E[x \to (x, id)]_{|fn(P)})\}$$

$$C \cup \{(\mathbf{0}, id, E)\} \xrightarrow{\varepsilon} n C$$

(b) Structural rules

$$C \cup \{P \oplus Q, id, E\} \xrightarrow{\oplus} n C \cup \{(P, id, E_{|fn(P)})\}$$

$$C \cup \{P \oplus Q, id, E\} \xrightarrow{\oplus} n C \cup \{(Q, id, E_{|fn(Q)})\}$$

(c) Choice rules

$$E_?(y) = E_!(x)$$

$$C \cup \left\{ \begin{array}{l} (y?^i[\bar{y}]P, id?, E?); \\ (x!^j[\bar{x}]Q, id!, E!) \end{array} \right\} \xrightarrow{(i,j)}_n C \cup \left\{ \begin{array}{l} (P, id?, E?[\bar{y} \to E_!(\bar{x})]_{|fn(P)}); \\ (Q, id!, E_{!|fn(Q)}) \end{array} \right\}$$

$$E_?(y) = E_!(x), \quad id_* = N((i, j), id?, id!)$$

$$C \cup \left\{ \begin{array}{l} (*y?^i[\bar{y}]P, id?, E?); \\ (x!^j[\bar{x}]Q, id!, E!) \end{array} \right\} \xrightarrow{(i,j)}_n C \cup \left\{ \begin{array}{l} (*y?^i[\bar{y}]P, id?, E?); \\ (P, id_*, E?[\bar{y} \to E_!(\bar{x})]_{|fn(P)}); \\ (Q, id!, E_{!|fn(Q)}) \end{array} \right\}$$

(d) Communication rules

Fig. 4. Naive semantics
$$C_0 \xrightarrow{\epsilon} C_1 \xrightarrow{\epsilon} C_2 \xrightarrow{(1,4)} C_3 \xrightarrow{\epsilon} C_4 \xrightarrow{\epsilon} C_5 \xrightarrow{\epsilon} C_6 \xrightarrow{(1,3)} C_7 \xrightarrow{*} C_8$$

where

$$C_0 = \{((\nu a)((*a^?1[(\nu b)(b!^2[b]0 | a!^3[0])) | a!^4[0]), \varepsilon, \emptyset))\}$$

$$C_1 = \{((*a^?1[(\nu b)(b!^2[b]0 | a!^3[0])) | a!^4[0], \varepsilon, [a \mapsto (a, \varepsilon)])\}$$

$$C_2 = \left\{ \begin{array}{l} (*a^?1[(\nu b)(b!^2[b]0 | a!^3[0]), \varepsilon, [a \mapsto (a, \varepsilon])]); \\ (a!^4[0], \varepsilon, [a \mapsto (a, \varepsilon)]) \end{array} \right\}$$

$$C_3 = \left\{ \begin{array}{l} (*a^?1[(\nu b)(b!^2[b]0 | a!^3[0]), \varepsilon, [a \mapsto (a, \varepsilon])]); \\ ((\nu b)(b!^2[b]0 | a!^3[0]), N((1,4), \varepsilon, \varepsilon), [a \mapsto (a, \varepsilon))); \\ (0, \varepsilon, \emptyset) \end{array} \right\}$$

$$C_4 = \left\{ \begin{array}{l} (*a^?1[(\nu b)(b!^2[b]0 | a!^3[0]), \varepsilon, [a \mapsto (a, \varepsilon])]); \\ ((\nu b)(b!^2[b]0 | a!^3[0]), N((1,4), \varepsilon, \varepsilon), [a \mapsto (a, \varepsilon)]) \end{array} \right\}$$

$$C_5 = \left\{ \begin{array}{l} (*a^?1[(\nu b)(b!^2[b]0 | a!^3[0]), \varepsilon, [a \mapsto (a, \varepsilon])]); \\ ((b!^2[b]0 | a!^3[0]), N((1,4), \varepsilon, \varepsilon), [a \mapsto (a, \varepsilon), b \mapsto (b, N((1,4), \varepsilon, \varepsilon))]) \end{array} \right\}$$

$$C_6 = \left\{ \begin{array}{l} (*a^?1[(\nu b)(b!^2[b]0 | a!^3[0]), \varepsilon, [a \mapsto (a, \varepsilon])]); \\ (b!^2[b]0, N((1,4), \varepsilon, \varepsilon), [b \mapsto (b, N((1,4), \varepsilon, \varepsilon))]); \\ (a!^3[0], N((1,4), \varepsilon, \varepsilon), [a \mapsto (a, \varepsilon)]) \end{array} \right\}$$

$$C_7 = \left\{ \begin{array}{l} (*a^?1[(\nu b)(b!^2[b]0 | a!^3[0]), \varepsilon, [a \mapsto (a, \varepsilon])]); \\ (b!^2[b]0, N((1,4), \varepsilon, \varepsilon), [b \mapsto (b, N((1,4), \varepsilon, \varepsilon))]); \\ ((\nu b)(b!^2[b]0 | a!^3[0]), N((1,3), \varepsilon, N((1,4), \varepsilon, \varepsilon)), [a \mapsto (a, \varepsilon)]); \\ (0, \varepsilon, \emptyset) \end{array} \right\}$$

$$C_8 = \left\{ \begin{array}{l} (*a^?1[(\nu b)(b!^2[b]0 | a!^3[0]), \varepsilon, [a \mapsto (a, \varepsilon])]); \\ (b!^2[b]0, N((1,4), \varepsilon, \varepsilon), [b \mapsto (b, N((1,4), \varepsilon, \varepsilon))]); \\ (b!^2[b]0, N((1,3), \varepsilon, N((1,4), \varepsilon, \varepsilon)), [b \mapsto (b, N((1,3), \varepsilon, N((1,4), \varepsilon, \varepsilon))]); \\ (a!^3[0], N((1,3), \varepsilon, N((1,4), \varepsilon, \varepsilon)), [a \mapsto (a, \varepsilon)]) \end{array} \right\}$$

<caption>Fig. 5. A computation sequence in the naive semantics</caption>
of the thread which has sent the message is just passed to its continuation. The next computation step, $C_3 \xrightarrow{\varepsilon} C_4$, is a garbage collection: it consists in removing the thread corresponding to the empty agent. The fifth computation step $C_4 \xrightarrow{\varepsilon} C_5$ opens a channel. Its name is given by $(b, N((1, 4), \varepsilon, \varepsilon))$ since it is opened by the restriction $(\nu b)$ of a thread the marker of which is $N((1, 4), \varepsilon, \varepsilon)$. Then in the computation step $C_5 \xrightarrow{\varepsilon} C_6$ a single thread is cut into two concurrent threads, which allows us to go on with the recursion: the computation step $C_6 \xrightarrow{(1,3)} C_7$ allows the system to spawn another instance of the resource with the fresh marker $N((1, 3), \varepsilon, N((1, 4), \varepsilon, \varepsilon))$. There is no confusion between recursive instances and the names of the channels they have opened: we can notice that in each thread corresponding to the agent labelled $b!^2[b]$, the marker of the thread and the marker of the name communicated to the variable $b$ are the same. $\square$

### 4.2.2 Correspondence

The correspondence between the standard and the naive non-standard semantics is established by a translation function $\Pi$. We define the translation $\Pi(C)$ of a non-standard configuration $C$ as follows:

$$ \Pi(C) = (\nu c_1)...(\nu c_k)(\overline{E}(t_1)| ... |\overline{E}(t_l)) $$

where $\{c_i | i \in [1; k]\} = \{E(x) | (P, id, E) \in C, x \in fn(P)\}$, $C = \{t_i | i \in [1; l]\}$ and $\overline{E}$ is the function which substitutes each free name of an agent by its image in the environment. The system $\Pi(C)$ is well defined thanks to associativity, commutativity, and swapping rules. We have also assumed<fnref n="3" /> that $\mathcal{N} \times \mathcal{M}$ was a subset of $\mathcal{N}$.

The standard and the non-standard semantics are in weak bisimulation, as expressed by the following theorem:

**Theorem 8** We have $\mathcal{S} = \Pi(C_0^n(\mathcal{S}))$, and for any non-standard configurations $C$ and for any word $u \in (\mathcal{L}^2 \cup \{\oplus\})^*$ such that $C_0^n(\mathcal{S}) \xrightarrow{u}^* C$, we have:

$$ (1) C \xrightarrow{\varepsilon} C' \implies \Pi(C) \equiv \Pi(C'); $$

$$ (2) \forall \lambda \in \mathcal{L}^2 \cup \{\oplus\}, C \xrightarrow{\lambda} C' \implies \Pi(C) \xrightarrow{\lambda} \Pi(C'); $$

$$ (3) \forall \lambda \in \mathcal{L}^2 \cup \{\oplus\}, \Pi(C) \xrightarrow{\lambda} P \implies \exists D, \exists E, \begin{cases} C \xrightarrow{\varepsilon} * D \xrightarrow{\lambda} E \\ \Pi(E) \equiv P. \end{cases} $$

The proof of Thm. 8 is shown in appendix A.

<footnote n="3">³ We consider in fact that a tagged name is a name, since there exists a bijection between the set of the tagged names and the set of the names.</footnote>
## 4.3 Efficient semantics

We now propose to reduce the number of reduction steps in order to make analysis design easier, and also to obtain a more efficient analysis. We will first consider a semantics in where all structural steps are automatically performed. Then we will introduce another semantics in where choice steps are also dealt in the same way.

### 4.3.1 Strongly bisimilar semantics

The binary relation $\xrightarrow{\varepsilon}^n$ is netherian and locally confluent. So, it is confluent [12], and we can define its limit $\downarrow$ as follows:

$$a \downarrow b \text{ if and only if } a \xrightarrow{\varepsilon}^* b \text{ and } \nexists c, b \xrightarrow{\varepsilon}^n c.$$

We now express explicitly this limit by designing an extraction function $\beta^i$ which performs all structural rules in parallel. The definition of $\beta^i$ is given in Fig. 6.

$$\begin{align*}
\beta^i((\nu n)P, id, E) &= \beta^i(P, id, (E[n \mapsto (n, id)])) \\
\beta^i(\mathbf{0}, id, E) &= \emptyset \\
\beta^i(P | Q, id, E) &= \beta^i(P, id, E) \cup \beta^i(Q, id, E) \\
\beta^i(P \oplus Q, id, E) &= \{(P \oplus Q, id, E_{|fn(P \oplus Q)})\} \\
\beta^i(aP, id, E) &= \{(aP, id, E_{|fn(aP)})\}
\end{align*}$$

<caption>Fig. 6. Extraction function</caption>

**Proposition 9** For any non-standard configuration C, we have $C \downarrow \bigcup_{t \in C} \beta^i(t)$.

The proof of Prop. 9 is shown in the appendix B.

We define the intermediate semantics as the transition system $(\{C_0^i(S)\}, \rightarrow_i)$, where the set of the initial states $\{C_0^i(S)\}$ and the computation rule $\rightarrow_i$ are given as follows:

* $C_0^i(S) = \beta^i(C_0^n(S))$,

* $\forall \lambda \in (\mathcal{L}^2 \cup \{\oplus\}), a \xrightarrow{\lambda}^i b \text{ if and only if } \exists c, a \xrightarrow{\lambda}^n c \text{ and } c \downarrow b$.

**Example 10** We come back to the previously given system:

$$(\nu a)(*a^{?1})((\nu b)(b^{?2}[b]0 \mid a^{?3}[0]) \mid a^{?4}[0]),$$
$$D_0 \xrightarrow{\substack{(1,4) \\ i}} D_1 \xrightarrow{\substack{(1,3) \\ i}} D_2$$

where

$$ 
\begin{aligned}
D_0 &= \left\{ 
\begin{array}{l}
(*a^?[])(\nu b)(b!^2[b]0 \mid a!^3[]0), \varepsilon, [a \mapsto (a, \varepsilon)]; \\
(a!^4[]0, \varepsilon, [a \mapsto (a, \varepsilon)])
\end{array}
\right\} \\
D_1 &= \left\{ 
\begin{array}{l}
(*a^?[])(\nu b)(b!^2[b]0 \mid a!^3[]0), \varepsilon, [a \mapsto (a, \varepsilon)]; \\
(b!^2[b]0, N((1,4), \varepsilon, \varepsilon), [b \mapsto (b, N((1,4), \varepsilon, \varepsilon))]) \\
(a!^3[]0, N((1,4), \varepsilon, \varepsilon), [a \mapsto (a, \varepsilon)])
\end{array}
\right\} \\
D_2 &= \left\{ 
\begin{array}{l}
(*a^?[])(\nu b)(b!^2[b]0 \mid a!^3[]0), \varepsilon, [a \mapsto (a, \varepsilon)]; \\
(b!^2[b]0, N((1,4), \varepsilon, \varepsilon), [b \mapsto (b, N((1,4), \varepsilon, \varepsilon))]) \\
(b!^2[b]0, N((1,3), \varepsilon, N((1,4), \varepsilon, \varepsilon)), [b \mapsto (b, N((1,3), \varepsilon, N((1,4), \varepsilon, \varepsilon)))]) \\
(a!^3[]0, N((1,3), \varepsilon, N((1,4), \varepsilon, \varepsilon)), [a \mapsto (a, \varepsilon)])
\end{array}
\right\}
\end{aligned}
$$

<caption>Fig. 7. A computation sequence in the intermediate semantics</caption>

and give a computation sequence for it in Fig. 7. It appears explicitly that structural computation steps are not described anymore. They are all performed implicitly at the beginning of the system, and after each communication or choice computation step: this way, the initial state $D_0$ is equal to the state $C_2$ while the whole computation sequence $C_0 \xrightarrow{\varepsilon} n C_1 \xrightarrow{\varepsilon} n C_2$ becomes implicit, then the single computation step $D_1 \xrightarrow{(1,4)} i D_2$ encodes the computation sequence $C_2 \xrightarrow{(1,4)} n C_3 \xrightarrow{\varepsilon} n C_4 \xrightarrow{\varepsilon} n C_5 \xrightarrow{\varepsilon} n C_6$, and the single computation step $D_2 \xrightarrow{(1,3)} i D_3$ encodes the computation sequence $C_6 \xrightarrow{u}^* n C_7 \xrightarrow{n}^* C_8$.

The standard and the intermediate semantics are in strong bisimilation (up to $\equiv$), as expressed by the following theorem:

**Theorem 11** We have $S \equiv \Pi(C_0^i(S))$, and for all non-standard configurations $C$ and for all word $u \in (\mathcal{L}^2 \cup \{\varepsilon; \oplus\})^*$ such that $C_0^i(S) \xrightarrow{u}^* C$, we have:

$$ (1) \quad \forall \lambda \in \mathcal{L}^2 \cup \{\oplus\}, \quad C \xrightarrow{\lambda} i C' \implies \Pi(C) \xrightarrow{\lambda} \Pi(C'); $$

$$ (2) \quad \forall \lambda \in \mathcal{L}^2 \cup \{\oplus\}, \quad \Pi(C) \xrightarrow{\lambda} P \implies \exists D, \left\{ \begin{array}{l} C \xrightarrow{\lambda} i D \\ \Pi(D) \equiv P. \end{array} \right. $$

The proof of Thm. 11 is shown in appendix B.
### 4.3.2 Efficient semantics

We propose to focus on communication rules and also to factor choice rules. To do this, we have to restrict the set of the traces: to make things easier, we propose to consider only the traces in which communications are delayed until no choices can be made.<fnref n="4" />

We denote by $\rightarrow \rightarrow$ the binary relation $\xrightarrow{\epsilon} n \cup \xrightarrow{\oplus} n$. The reduction relation $\rightarrow$ is nœtherian, but not locally confluent. We define the relation $\implies$ as follows:

$$a \implies b \text{ if and only if } a \xrightarrow{\epsilon} b \text{ and } \nexists c, b \rightarrow c.$$

Since $\rightarrow$ is not confluent, $\implies$ is not deterministic. We now express explicitly its action by designing an extraction function $\beta$ which computes the set of all the successors of a given configuration. The definition of $\beta$ is given in Fig. 8(a).

**Proposition 12** For any non standard configuration C, we have:

$$\{b | C \implies b\} = \{\bigcup Cont_t | \forall t \in C, Cont_t \in \beta(t)\}.$$

The proof of Prop. 12 is shown in appendix C.

Intuitively, $\beta$ gives the set of all the choices when spawning a continuation. To spawn a continuation for a thread the syntactic component of which is a choice $(P \oplus Q)$, we either spawn a continuation choice for $P$ or a continuation choice for $Q$. Spawning a continuation for a thread the syntactic component of which is a parallel composition $(P | Q)$, consists in choosing a continuation for $P$, choosing a continuation for $Q$, and spawning concurrently these two continuations.

We now define the efficient semantics as the transition system $(C_0^e(S), \rightarrow_e)$:

* $C_0^e(S) = \beta(S, \epsilon, \emptyset)$

* $\forall \lambda \in \mathcal{L}^2, a \xrightarrow{\lambda} e b \text{ if and only if } \exists c, a \xrightarrow{n} c \text{ and } c \implies b$.

An explicit definition of $(C_0^e(S), \rightarrow_e)$ is given in Fig. 8.

The following theorem establishes the correspondence between the standard and the efficient semantics:

**Theorem 13** For any initial non-standard configuration $C_0 \in C_0^e(S)$, there

<footnote n="4">⁴ We have also considered in [14, Sect. 3.3] restricting the set of the traces to those for which choices are made only when necessary, which comes down considering external choices instead of internal ones.</footnote>
$$ \beta((\nu x)P, id, E) = \beta(P, id, (E[x \mapsto (x, id)])) $$

$$ \beta(\mathbf{0}, id, E) = \{\emptyset\} $$

$$ \beta(P \oplus Q, id, E) = \beta(P, id, E) \cup \beta(Q, id, E) $$

$$ \beta(P | Q, id, E) = \{A \cup B \mid A \in \beta(P, id, E), B \in \beta(Q, id, E)\} $$

$$ \beta(aP, id, E) = \{(aP, id, E_{|fn(aP)})\} $$

(a) Extraction function

$$ C_0^e(S) = \beta(S, \varepsilon, \emptyset) $$

(b) Initial configurations

$$ \frac{\left\{ \begin{array}{l} E_?(y) = E!(x), \\ Ct_P \in \beta(P, id?, E? [y_i \mapsto E!(x_i)]), \\ Ct_Q \in \beta(Q, id!, E!) \end{array} \right.}{C \cup \left\{ \begin{array}{l} (y?^i[\bar{y}]P, id?, E?), \\ (x!^j[\bar{x}]Q, id!, E!) \end{array} \right\}} \stackrel{(i,j)}{\longrightarrow}_e (C \cup Ct_P \cup Ct_Q) $$

$$ \frac{\left\{ \begin{array}{l} E_*(y) = E!(x), \\ Ct_P \in \beta(P, N((i, j), id_*, id!), E_* [y_i \mapsto E!(x_i)]), \\ Ct_Q \in \beta(Q, id!, E!) \end{array} \right.}{C \cup \left\{ \begin{array}{l} (*y?^i[\bar{y}]P, id_*, E_*), \\ (x!^j[\bar{x}]Q, id!, E!) \end{array} \right\}} \stackrel{(i,j)}{\longrightarrow}_e (C \cup \{(*y?^i[\bar{y}]P, id_*, E_*)\} \cup Ct_P \cup Ct_Q) $$

(c) Communication rules

<caption>Fig. 8. Efficient semantics</caption>
exists $k \in \mathbb{N}$ such that $S \xrightarrow{\oplus^k} * \Pi(C_0)$ and for all non-standard configurations $C$ and for all word $u \in (\mathcal{L}^2)^*$ such that $C_0 \xrightarrow{u} * C$, we have:

$$ (1) \quad \forall \lambda \in \mathcal{L}^2, C \xrightarrow{\lambda} _e C' \implies \exists k \in \mathbb{N}, \exists P, \Pi(C) \xrightarrow{\lambda} P \xrightarrow{\oplus^k} * \Pi(C'); $$

$$ (2) \quad \forall \lambda \in \mathcal{L}^2, \Pi(C) \xrightarrow{\lambda} P \implies \exists D, \left\{ \begin{array}{l} C \xrightarrow{\lambda} _e D \\ \text{and} \\ \quad \exists k > 0, P \xrightarrow{\oplus^k} + \Pi(D) \\ \quad \text{or } P \equiv \Pi(D). \end{array} \right. $$

The proof of Thm. 13 is shown in appendix C.

**Remark 14** There is no bisimulation between the standard and the efficient semantics. We have restricted both the set of traces to those where choices are always performed before communications, and the set of states to those where no choice appears at the top level. Therefore, these restrictions do not change the properties we want to observe on mobile systems.

# 5 Context-free semantics

## 5.1 Construction

We now extend our non-standard semantics to open systems. An open system $S$ is a part of a bigger closed system, the rest of which is called its context. The context is a set of agents, concurrently running with $S$. We represent this context by the set of channel names it shares with the system $S$, we call such names the *unsafe names*, and approximate its behavior as if it was an intruder who was able to compose any possible agent working on these channel names. An interaction between the system $S$ and its context may only consist in a communication between an agent $p_S$ of the first and an agent $p_{\text{cont}}$ of the second, via a channel the name of which is unsafe. This communication is called *spying* when $p_{\text{cont}}$ is the receiver, and *spoiling* when $p_{\text{cont}}$ is the message sender. When spying, the context listens to obtain new channel names which become unsafe. When spoiling, the context may pass any name to $S$, either an unsafe name denoting a channel opened by a binder of the system $S$ or a name denoting a channel opened by the context itself; as a consequence, we have to introduce an infinite set of unsafe names for the channels that the context may have opened. Eventually, spoiling may lead to the replication of a resource, which requires the allocation of an unambiguous marker, otherwise the consistency of the semantics would not be preserved.

Since $\alpha$-conversion allows us to choose the names of the new channels opened by the context, we may assume that those channels have been declared by
recursive instances of a single agent. By choosing cont?, conti ∈ L \ Lused and ext ∈ N \ bn(S), such channels will be seen as if they had been created by the restriction (ν ext) of a recursive instance of an agent the marker of which is t_n, where t_n is recursively defined as follows:

$$ \begin{cases} t_0 = N((cont?, cont_1), \epsilon, \epsilon) \\ t_{n+1} = N((cont?, cont_1), \epsilon, t_n). \end{cases} $$

Thus the set of the names of the channel opened by the context can be chosen as the set { (ext, t_n) | n ∈ N } , which we denote by en. We also assume that all spoiling messages are recursive instances of a single agent the first action of which is labelled with 0 ∈ L \ (Lused ∪ { cont?; conti } ). The coherence of our semantics mainly relies on the fact that during a computation sequence, there cannot be two different instances of a single agent with the same marker. We guarantee this property by associating to each spoiling message a fresh marker in the set { t_n | n ∈ N } .

A non-standard configuration is now a triple (C, U, F), where C is a set of threads, U is a set of channel names, and F is a set of markers. The set C contains the running threads. The set U contains all the name (a, id) such that the channel opened by the restriction (ν a) of the agent instance tagged with the marker id is unsafe. The set F contains fresh markers which have not been used as markers for spoiling message. At the beginning of the system, free names have to be chosen among the set of initial unsafe names. We make no assumptions about the past of the system, so that distinct free names can be bound to the same unsafe name. This is especially useful when analyzing an instance of a resource without any knowledge of the relations between channel names that have been communicated to it.

The transition relation ⇑ takes into account the computations inside the mobile system S, as well as the computations involving the system S and its context. Initial non-standard configurations and computation rules are given in Fig. 9.

## 5.2 Coherence

We propose to establish a relation between the non-standard semantics of closed and open systems. Let S_I(x_1, ..., x_n) be an open system the set of the free names of which are exactly the set {x_i | i ∈ [1; n]} . We want to construct a projection function Π_τ, such that:

* any non-standard computation sequence τ of a closed system of the form (ν c_1)...(ν c_k)(S_I(c_{i_1}, ..., c_{i_n}) | S_c(c_{j_1}, ...c_{j_l})), is mapped to a non-standard
$$ C_0^o(S) = \left\{ (Ct, en, \{t_n | n \in \mathbb{N}\}) \mid \begin{array}{l} Ct \in \beta(S, \varepsilon, E), \\ E \in (fn(S) \to en) \end{array} \right\} $$

(a) Initial configurations

$$ \frac{C \xrightarrow{\lambda} e C'}{(C, U, F) \stackrel{\lambda}{\rightleftharpoons} (C', U, F)} $$

(b) Internal interactions

$$ \frac{t = (x^j[x_1, \dots, x_n]P, id, E), \ E(x) \in U, \ Ct \in \beta(P, id, E)}{(C \cup \{t\}, U, F) \stackrel{(0,j)}{\rightleftharpoons} (C \cup Ct, U \cup \{E(x_k) | k \in [1; n]\}, F)} $$

(c) Spied communication

$$ \frac{\left\{ \begin{array}{l} t = (y^i[y_1, \dots, y_n]P, id, E), \\ E(y) \in U, \ c_1, \dots, c_n \in U, \\ Ct \in \beta(P, id, E[y_k \mapsto c_k]) \end{array} \right.}{(C \cup \{t\}, U, F) \stackrel{(i,0)}{\rightleftharpoons} (C \cup Ct, U, F)} $$

(d) Spoiled communication

$$ \frac{\left\{ \begin{array}{l} t = (*y^i[y_1, \dots, y_n]P, id, E), \\ E(y), c_1, \dots, c_n \in U, \\ \text{id}_! \in F, \\ \text{id}_* = N((i, 0), \text{id}, \text{id}_!), \\ \text{Ct} \in \beta(P, \text{id}_*, E[y_k \mapsto c_k]) \end{array} \right.}{(C \cup \{t\}, U, F) \stackrel{(i,0)}{\rightleftharpoons} (C \cup \{t\} \cup \text{Ct}, U, F \setminus \{\text{id}_!\})} $$

(e) Spoiled resource replication

<caption>Fig. 9. Context-free non-standard semantics</caption>
computation sequence of the open system $S_I$;

* reciprocally for any non-standard computation sequence $\tau'$ of the open system $S_I$, there exists a computation sequence $\tau$ of a closed system of the form $(\nu c_1)...(\nu c_k) (S_I(c_{i_1}, ..., c_{i_n}) | S_c(c_{j_1}, ...c_{j_l}))$, such that $\tau' = \Pi_\tau(\tau)$.

Let $\mathcal{L}_I \subseteq \mathcal{L}$ be the subset of the labels occurring in $S_I$ and $\mathcal{N}_I \subseteq \mathcal{N}$ be the subset of the names used in name restrictions of $S_I$. The function lab maps each syntactic component beginning with an action to the label of this action. We introduce two one-to-one functions in order to interpret names and agents created by the context of $S_I$: let $\Phi_M$ be a one-to-one map from the set $(\mathcal{L} \times \mathcal{M})$ into the set $\{t_n | n \in \mathbb{N}\}$, and $\Phi_N$ be a one-to-one function from the set $(\mathcal{N} \times \mathcal{M})$ into the set $en$. We now define the projection $\Pi_\tau(S_I, \Phi_M, \Phi_N)$ which transforms each computation sequence of a closed mobile system $S = (\nu \bar{c})(S_I(c_{i_1}, ..., c_{i_n}) | S_c(c_{j_1}, ...c_{j_l}))$ into a computation sequence of the part $S_I$ of the system $S$. We assume without any loss of generality that $fn(S_I) = \{c_{i_k} | k \in \llbracket 1; n \rrbracket\}$, and that no name occurs twice as an argument of a name binder.

We first project each syntactic component label, by replacing each label which does not occur in $S_I$ by the unique label of the context, that is to say the 0 label.

**Definition 15** The projection $\Pi_I(l)$ of a syntactic component label $l \in \mathcal{L}$ is defined as follows:

$$ \Pi_I(l) = \begin{cases} l & \text{if } l \in \mathcal{L}_I \\ 0 & \text{otherwise.} \end{cases} $$

We then apply the syntactic component label projection pair-wise on transition labels.

**Definition 16** The projection $\Pi_\lambda(i, j)$ of transition label $(i, j) \in \mathcal{L}^2$ is defined as follows:

$$ \Pi_\lambda(i, j) = (\Pi_I(i), \Pi_I(j)). $$

Next, we project the instance markers of the syntactic components of $S_I$. In such a marker, only the right sibling can be the marker of a syntactic component of the context, as we know that the replicated resource necessarily belongs to $S_I$. When a resource is replicated by a message of the context, we replace its syntactic component, and calculate a coherent marker according to $\Phi_M$.
**Definition 17** *Marker projection is defined as follows:*

$$ \Pi_{\mathcal{M}}^{\mathcal{M}}: \left\{ \begin{array}{ll} N((i, j), t_1, t_2) & \mapsto N(\Pi_{\lambda}(i, j), \Pi_{\mathcal{M}}^{\mathcal{M}}(t_1), \Pi_{\mathcal{M}}^{\mathcal{M}}(t_2)) & \text{if } j \in \mathcal{L}_{\mathrm{I}} \\ N((i, j), t_1, t_2) & \mapsto N(\Pi_{\lambda}(i, j), \Pi_{\mathcal{M}}^{\mathcal{M}}(t_1), \Phi_{\mathcal{M}}(j, t_2))) & \text{if } j \notin \mathcal{L}_{\mathrm{I}} \\ \varepsilon & \mapsto \varepsilon. \end{array} \right. $$

We now project channel names. For a channel having been opened by a name restriction of $S_{\mathrm{I}}$, we just project the marker. For those having been opened by the context, we replace the name restriction by the unique restriction ($\nu \ \mathrm{ext}$) of the context, and calculate the coherent marker according to $\Phi_{\mathcal{N}}$.

**Definition 18** *Channel name projection is defined as follows:*

$$ \Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(x, id_x) = \begin{cases} (x, \Pi_{\mathcal{M}}^{\Phi_{\mathcal{M}}}(id_x)) & \text{if } x \in \mathcal{N}_{\mathrm{I}} \\ \Phi_{\mathcal{N}}(x, id_x) & \text{otherwise.} \end{cases} $$

We can easily project an instance of a syntactic component of $S_{\mathrm{I}}$ by projecting its marker, and each channel inside its environment.

**Definition 19** *Thread projection is defined as follows:*

$$ \Pi_{t}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(P, id, E) = (P, \Pi_{\mathcal{M}}^{\Phi_{\mathcal{M}}}(id), [x \mapsto \Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(E(x))]). $$

Then, we can project a configuration by projecting all the threads the syntactic component of which is a sub-term of $S_{\mathrm{I}}$, and removing the other threads:

**Definition 20** *Configuration projection is defined as follows:*

$$ \Pi_{C}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(C) = \{ \Pi_{t}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(P, id, E) \mid (P, id, E) \in C, \mathrm{lab}(P) \in \mathcal{L}_{\mathrm{I}} \}. $$

We can now define the projection of a computation sequence. At each computation step, we obtain the set of the threads by projecting all the instances of syntactic components of $S_{\mathrm{I}}$, and throwing away instances of syntactic components of the context. Unfortunately, the set of unsafe names, and the set of fresh markers, cannot be constructed without any knowledge of the previous computation steps, so we construct them incrementally: at each computation step, we insert spied names into the set of unsafe names, and remove the used markers from the set of fresh markers. We also ignore all computation steps only involving the context.

**Definition 21** *Computation sequence projection is then defined as follows:* Let $\tau = C_0 \xrightarrow{\lambda_1} e \dots \xrightarrow{\lambda_n} e C_n$ be a non-standard computation sequence, with
$C_0 \in \mathcal{C}_0^e(S)$. We define the projection of $\tau$, $\Pi_\tau(S_I, \Phi_M, \Phi_N)(\tau)$ as the non-standard computation sequence:

$$ (A_0, U_0, F_0) \underset{\sim}{\overset{\Pi_\lambda(\lambda_{a_1})}{\rightleftharpoons}} \dots \underset{\sim}{\overset{\Pi_\lambda(\lambda_{a_p})}{\rightleftharpoons}} (A_p, U_p, F_p) $$

of the open system $S_I$, where

* $a_1, \dots, a_p$ is the strictly ascending sequence of the elements of the set $\{i \in \llbracket 1; n \rrbracket \mid \lambda_i \in \mathcal{L}^2 \setminus (\mathcal{L} \setminus \mathcal{L}_I)^2\}$;

* the initial configuration $(A_0, U_0, F_0)$ is the following triple:

$$ (\Pi_C^{\Phi_M, \Phi_N}(C_0), en, \{t_n \mid n \in \mathbb{N}\}); $$

* for $k \in \llbracket 1; p \rrbracket$, the configuration $(A_k, U_k, F_k)$ is then defined as follows:

$$ \cdot A_k = \Pi_C^{\Phi_M, \Phi_N}(C_{a_k}), $$

$$ \cdot U_k = \begin{cases} U_{k-1} & \text{if } \text{fst}(\lambda_{a_k}) \in \mathcal{L}_I, \\ U_{k-1} \cup \{\Pi_N^{\Phi_M, \Phi_N}(E(x_r)) \mid r \in \llbracket 1; n \rrbracket\} & \text{otherwise,} \end{cases} $$

where, in the last case, $t = (x_1^j[x_1, \dots, x_n]P, id, E)$ denotes the unique thread in $C_{a_{k-1}} \setminus C_{a_k}$ which matches this notation;

$$ \cdot F_k = \begin{cases} F_{k-1} & \text{if } \text{snd}(\lambda_{a_k}) \in \mathcal{L}_I \text{ or if } \xrightarrow{\lambda_{a_k}}_e \text{ is not a resource replication,} \\ F_{k-1} \setminus \{\Phi_M(\text{snd}(\lambda_{a_k}), id) \mid (P, id, E) \in C_{a_{k-1}} \setminus C_{a_k}\} & \text{otherwise.} \end{cases} $$

We establish the relation between the non-standard semantics of closed and open systems, as follows:

**Theorem 22 (Soundness)** Let $\tau = C_0 \dots C_n$ be a non-standard computation sequence of the following closed system:

$$ (\nu c_1) \dots (\nu c_k)(S_I(c_{i_1}, \dots, c_{i_n}) \mid S_c(c_{j_1}, \dots, c_{j_l})), $$

with $C_0 \in \mathcal{C}_0^e(S)$. Then $\Pi_\tau(S_I, \Phi_M, \Phi_N)(\tau) = (A_0, U_0, F_0) \dots (A_p, U_p, F_p)$ is a non-standard computation sequence of the open system $S_I$ and $(A_0, U_0, F_0) \in \mathcal{C}_0^e(S)$.

**Theorem 23 (Completeness)** Let $\tau'$ be the non-standard computation sequence of an open system $S_I$, that we denote by:

$$ (C_0, U_0, F_0) \underset{\sim}{\overset{(i_1, j_1)}{\rightleftharpoons}} \dots \underset{\sim}{\overset{(i_n, j_n)}{\rightleftharpoons}} (C_n, U_n, F_n), $$

where $(C_0, U_0, F_0) \in \mathcal{C}_0^e(S)$.

Then there exists:

* a closed system $S_* = (\nu \bar{c})(S_I(c_{i_1}, \dots, c_{i_n}) \mid S_c(c_{j_1}, \dots, c_{j_l}))$,
* two one-to-one functions $\Phi_N$ and $\Phi_M$,

* a non-standard computation sequence $\tau$ of the system $S_*$,

such that $\Pi_{\tau}(S_I, \Phi_M, \Phi_N)(\tau) = \tau'$.

Soundness is ensured by construction. Completeness relies on the existence of a most general context which can be used in simulating any context. It is given in Fig. 10. It uses a global channel, named **unsafe** via which unsafe names are sent an arbitrary amount of times. It is made off four kinds of resources. The resource **new** opens a new unsafe channel; the resource **repli** is used to replicate the information that a channel name is unsafe, so that a context may use each unsafe name an arbitrary number of time; the resource **spy$_k$** collects an unsafe channel $c$, and receive through this channel a message of arity $k$; the resource **spoil$_k$** collects an unsafe channel $c$, and $k$ unsafe names, and sends the $k$ names through the channel $c$. Resources **spy$_0$** and **spoil$_0$** only enforce some synchronization with the system. In Fig. 10, $n$ denotes the greatest arity of the messages occurring in the system part we analyze. Thus the closed system can be chosen as the following one:

$$S_* = (\nu \text{ unsafe})(\nu x_1)...(\nu x_p) \\ (\text{unsafe!}[x_1] | \dots | \text{unsafe!}[x_p] | S_I(x_{i_1}, \dots, x_{i_n}) | S_c(\text{unsafe})).$$

The non-standard computation sequence is obtained by mimicking spied and spoiled computation steps in $S_c$. The full proof of Thms. 22 and 23 is shown in appendix D.

$S_c = (\nu \text{ new})$ 
( **new** | **repli** 
| **spy$_0$** | ... | **spy$_n$** 
| **spoil$_0$** | ... | **spoil$_n$** 
| **new!** )

where

* **new** := $\ast$new?[]((\nu channel)(unsafe![channel] | new![]))

* **repli** := $\ast$unsafe?[x](unsafe![x] | unsafe![x])

* **spy$_i$** := $\ast$unsafe?[c]c?[y$_1$, ..., y$_i$](unsafe![y$_1$] | ... | unsafe![y$_i$])

* **spoil$_i$** := $\ast$unsafe?[c]unsafe?[x$_i$]...unsafe?[x$_i$]c![x$_1$, ..., x$_i$]

<caption>Fig. 10. The most general context</caption>
Abstract Interpretation is a theory of the approximation of semantics. It formalizes the idea that the semantics can be more or less precise according to the considered level of observation. In static analysis, abstract interpretation is used to derive a decidable semantics from a concrete one. Because of the upper-approximation, the result is not complete: this means that not all the properties of the program are discovered, nevertheless, the result is sound: this means that all the captured properties are correct.

In this section, we introduce a generic abstraction to approximate the behavior of a mobile system. It could apply indeed to any transition system. This abstraction does not yet depend on the abstracted properties: they are left as a parameter of our analysis. Hence, our framework is highly generic, and we can make a reduced product between several analyses. We will use this framework to derive an analysis of the control flow in Sect. 7, and an analysis of the occurrence number of the agents in Sect. 8.

## 6.1 Generic abstraction

We denote by $\mathcal{C}$ the set of the non-standard configurations and by $\Sigma$ the set of the transition labels. We are actually interested in the set $\mathcal{C}(\mathcal{S})$ of all the configurations that a system may take during a finite sequence of computation steps. This is given by its collecting semantics, which is defined in [6]. It can be expressed as the least fixpoint of a $\cup$-complete endomorphism $\mathbb{F}$ on the complete lattice $\wp(\Sigma^* \times \mathcal{C})$ defined as follows:

$$ \mathbb{F}(X) = (\{\varepsilon\} \times C_0^o(\mathcal{S})) \cup \{ (u.\lambda, C') \mid \exists C \in \mathcal{C}, (u, C) \in X \text{ and } C \overset{\lambda}{\rightleftharpoons} C' \}. $$

This least fixpoint is usually not decidable, so we use the Abstract Interpretation framework [7] to compute a sound – but not necessarily complete – approximation of it. More precisely, we use the relaxed version of Abstract Interpretation [8], in which the abstract domain is not supposed to be complete under least upper bound; furthermore, no abstraction function is required.

**Definition 24** An abstraction is a tuple $(\mathcal{C}^{\sharp}, \sqsubseteq^{\sharp}, \sqcup^{\sharp}, \perp^{\sharp}, \gamma, C_0^{\sharp}, \rightsquigarrow, \nabla)$ which satisfies:

(1) $(\mathcal{C}^{\sharp}, \sqsubseteq^{\sharp})$ is a pre-order;

(2) $\sqcup^{\sharp} : \wp_{finite}(\mathcal{C}^{\sharp}) \to \mathcal{C}^{\sharp}$ is such that $\forall A^{\sharp} \in \wp_{finite}(\mathcal{C}^{\sharp}), \forall a^{\sharp} \in A^{\sharp}, a^{\sharp} \sqsubseteq^{\sharp} \sqcup^{\sharp}(A^{\sharp});$

(3) $\perp^{\sharp} \in \mathcal{C}^{\sharp}$ satisfies $\forall a^{\sharp} \in \mathcal{C}^{\sharp}, \perp^{\sharp} \sqsubseteq^{\sharp} a^{\sharp};$
(4) $\gamma: C^{\sharp} \to \wp(\Sigma^* \times C)$ is a monotonic map;

(5) $C_0^{\sharp} \in C^{\sharp}$ is such that $\{\varepsilon\} \times C_0^0(S) \subseteq \gamma(C_0^{\sharp})$;

(6) $\rightsquigarrow \in \wp(C^{\sharp} \times \Sigma \times C^{\sharp})$ is an abstract deterministic labelled transition relation over $C^{\sharp}$ such that: $\forall C^{\sharp} \in C^{\sharp}, \forall (u, C) \in \gamma(C^{\sharp}), \forall \lambda \in \Sigma, \forall \overline{C} \in C,$

$$C \overset{\lambda}{\hookrightarrow} \overline{C} \implies \exists \overline{C}^{\sharp} \in C^{\sharp}, (C^{\sharp} \overset{\lambda}{\hookrightarrow} \overline{C}^{\sharp} \text{ and } (u.\lambda, \overline{C}) \in \gamma(\overline{C}^{\sharp}));$$

(7) $\nabla: C^{\sharp} \times C^{\sharp} \to C^{\sharp}$ is a widening operator which satisfies:

* $\forall C_1^{\sharp}, C_2^{\sharp} \in C^{\sharp}, C_1^{\sharp} \sqsubseteq^{\sharp} C_1^{\sharp} \nabla C_2^{\sharp}$ and $C_2^{\sharp} \sqsubseteq^{\sharp} C_1^{\sharp} \nabla C_2^{\sharp}$,

* $\forall (C_n^{\sharp})_{n \in \mathbb{N}} \in (C^{\sharp})^N$, the sequence $(C_n^{\nabla})_{n \in \mathbb{N}}$ defined as

$$\begin{cases} C_0^{\nabla} = C_0^{\sharp} \\ C_{n+1}^{\nabla} = C_n^{\nabla} \nabla C_{n+1}^{\sharp} \end{cases}$$

is ultimately stationary.

The set $C^{\sharp}$ is an abstract domain. It captures the properties we are interested in, and abstracts away the other properties. The pre-order $\sqsubseteq^{\sharp}$ describes the amount of information which is known about the properties that we approximate. We only use a pre-order to allow some concrete properties to be described by several unrelated abstract elements. The abstract union $\sqcup^{\sharp}$ is used to gather the information described by several abstract elements. For the sake of generality, it does not necessarily compute the least upper bound of a finite set of abstract elements (this least bound may not even exist). The abstract element $\perp^{\sharp}$ denotes the empty set and it provides the basis for our abstract iteration. The function $\gamma$ is a concretization function which maps each abstract property to the set of the concrete elements which satisfy this property. The abstract element $C_0^{\sharp}$ describes the properties satisfied by the system initial configurations. The relation $\rightsquigarrow$ is used to mimic the concrete transition system in the abstract domain and the operator $\nabla$ is used to ensure the convergence of the analysis in finitely many iterations.

Given an abstraction $(C^{\sharp}, \sqsubseteq^{\sharp}, \sqcup^{\sharp}, \perp^{\sharp}, \gamma, C_0^{\sharp}, \rightsquigarrow, \nabla)$, the abstract counterpart $\mathbb{F}^{\sharp}$ to $\mathbb{F}$ defined as:

$$\mathbb{F}^{\sharp}(C^{\sharp}) = \sqcup^{\sharp} \left( \left\{ \overline{C}^{\sharp} \mid \exists \lambda \in \Sigma, C^{\sharp} \overset{\lambda}{\hookrightarrow} \overline{C}^{\sharp} \right\} \cup \{C_0^{\sharp}; C^{\sharp}\} \right).$$

satisfies the soundness condition $\forall C^{\sharp} \in C^{\sharp}, \mathbb{F} \circ \gamma(C^{\sharp}) \subseteq \gamma \circ \mathbb{F}^{\sharp}(C^{\sharp})$. Since $\mathbb{F}$ is monotonic, we have $\forall n \in \mathbb{N}, \forall C^{\sharp} \in C^{\sharp}, \mathbb{F}^n \circ \gamma(C^{\sharp}) \subseteq \gamma \circ \mathbb{F}^{\sharp n}(C^{\sharp})$. On the other hand, since $\mathbb{F}$ is a $\cup$-complete endomorphism, we have $lfp_0 \mathbb{F} = \bigcup_{n \in \mathbb{N}} \mathbb{F}^n(\emptyset)$. As a consequence, we obtain the soundness of our analysis:

**Theorem 25** $lfp_0 \mathbb{F} \subseteq \bigcup_{n \in \mathbb{N}} [\gamma \circ \mathbb{F}^{\sharp n}](\perp^{\sharp})$.
Following [6], we compute a sound and decidable approximation of our abstract semantics by using the widening operator $\nabla$:

**Theorem 26** The abstract iteration [8, 9] of $\mathbb{F}^\sharp$ defined as follows:

$$ egin{cases} \mathbb{F}_0^{\nabla} = \perp^{\sharp} \\ \mathbb{F}_{n+1}^{\nabla} = \begin{cases} \mathbb{F}_n^{\nabla} & \text{if } \mathbb{F}^\sharp(\mathbb{F}_n^{\nabla}) \subseteq \mathbb{F}_n^{\nabla} \\ \mathbb{F}_n^{\nabla} \nabla \mathbb{F}^\sharp(\mathbb{F}_n^{\nabla}) & \text{otherwise} \end{cases} \end{cases} $$

is ultimately stationary and its limit $\mathbb{F}^{\nabla}$ satisfies $\mathcal{C}(\mathcal{S}) \subseteq \gamma(\mathbb{F}^{\nabla})$.

## 6.2 Abstraction algebra

Our framework is highly extensible. We now give some operations over abstractions to compose them.

**Proposition 27 (Product)** Let $(C_1^\sharp, \sqsubseteq_1^\sharp, \sqcup_1^\sharp, \perp_1^\sharp, \gamma_1, C_{0_1}^\sharp, \rightsquigarrow_1, \nabla_1)$ and $(C_2^\sharp, \sqsubseteq_2^\sharp, \sqcup_2^\sharp, \perp_2^\sharp, \gamma_2, C_{0_2}^\sharp, \rightsquigarrow_2, \nabla_2)$ be two abstractions.

The following tuple $(C^\sharp, \sqsubseteq^\sharp, \sqcup^\sharp, \perp^\sharp, \gamma, C_0^\sharp, \rightsquigarrow, \nabla)$ where

* $C_1^\sharp = C_1^\sharp \times C_2^\sharp$;

* $\sqsubseteq^\sharp, \sqcup^\sharp, \perp^\sharp$ and $\nabla$ are defined pair-wise;

* $\gamma : \begin{cases} C^\sharp \to \wp(\Sigma^* \times C) \\ (a_1^\sharp, a_2^\sharp) \mapsto \gamma_1(a_1^\sharp) \cap \gamma_2(a_2^\sharp); \end{cases}$

* $C_0^\sharp = (C_{0_1}^\sharp, C_{0_2}^\sharp)$;

* $\rightsquigarrow$ is defined by:

$$ (a_1, a_2) \rightsquigarrow (b_1, b_2) \text{ if and only if } a_1 \rightsquigarrow_1 b_1 \text{ and } a_2 \rightsquigarrow_2 b_2 $$

is also an abstraction.

**Proposition 28 (Reduction)** Let $(C^\sharp, \sqsubseteq^\sharp, \sqcup^\sharp, \perp^\sharp, \gamma, C_0^\sharp, \rightsquigarrow, \nabla)$ be an abstraction, and $\rho$ be a reduction operator$^5$ $\rho : C^\sharp \to C^\sharp$ which satisfies:

$$ \forall a^\sharp \in C^\sharp, \gamma(a^\sharp) \subseteq \gamma(\rho(a^\sharp)). $$

The following tuple $(C^\sharp, \sqsubseteq^\sharp, \sqcup^\sharp, \perp^\sharp, \gamma, C_{0_\rho}^\sharp, \rightsquigarrow_\rho, \nabla)$ where

* $C_{0_\rho}^\sharp = \rho(C_0^\sharp)$;

* $\rightsquigarrow_\rho$ is defined by:

$$ a \rightsquigarrow_\rho c \text{ if and only if there exists } b \in C^\sharp, \text{ such that } \rho(a) \rightsquigarrow b \text{ and } c = \rho(b) $$

<footnote>$^5$ $\rho$ simplifies the properties obtained in the abstract domain.</footnote>
is also an abstraction.

Furthermore, $\rho$ can also be used to simplify the final result of the abstract iteration.

The proof of Prop. 27 and Prop. 28 is shown in appendix E.

# 7 Control flow analysis

We now use this framework to derive an analysis of the control flow. This analysis requires an abstract domain for describing sets of marker tuples. In the first subsection, we introduce the generic control flow analysis, independently of the chosen abstract domain. In the next subsection, we propose three different choices of abstract domains, so that we get three different analyses.

## 7.1 Generic control flow analysis

We propose to compute a description of both the potential interactions between the agents of a mobile system, and the potential interactions between its agents and a hostile context. For that purpose, we will compute for each syntactic name restriction an approximation of the set of the syntactic agents that may receive the name of a channel opened by an instance of this name restriction. As we want a non-uniform description, we will also compute a comparison between the markers of the agents which have opened channels and the ones of the agents to which the names of those channels have been communicated. Due to the approximation, some of the discovered interactions may be ineffective. But the analyzer detects all the interactions. So, if the analyzer does not detect an interaction between two components, there cannot be any interaction between them.

The main difficulty is to synthesize comparisons between markers throughout computation steps. We use the marker of the agent instance to which channel names are communicated as a pivot to synthesize the comparison between the markers of the agent instances which have opened these channels. Furthermore, we use synchronization conditions on the channel names via which the communication is performed to establish a comparison between the markers of all the involved agent instances. Our main strategy is easy: we first gather all the information we have about the marker pairs (this means we will abstract sets of marker tuples). Then, synchronization conditions give equality relations between some tuple components. If these equality relations are satisfiable, the abstract computation step is enabled and we compute, for each
new agent instance, the comparison between the marker of the new instance and the markers of the instances which had opened the channels.

We introduce for each $n \in \mathbb{N}$ an abstract pre-order $(Id_n^\sharp, \sqsubseteq_n)$ to represent sets of $n$-tuples of thread markers. Thus, each $Id_n^\sharp$ is related to $\wp(\mathcal{M}^n)$ by a monotonic concretization function $\gamma_n$. We introduce some abstract primitives to handle these domains: a representation of the empty set $\perp_n^\sharp$, a representation of the initial marker $\varepsilon^\sharp$, an abstraction of the set of the context markers $t^\sharp$, an abstract union $\sqcup_n$, a widening operator $\nabla_n$, an associative abstract concatenation $\bullet$ that is a correct abstraction of tuple concatenation, an abstract join sync to enforce synchronization conditions, an abstract projection $\Pi$ and an abstract push operator push which is used to calculate the abstraction of the set of the new markers when replicating a resource. These primitives shall satisfy the following properties:

(1) $\gamma_n(\perp_n^\sharp) = \emptyset$;

(2) $\varepsilon \in \gamma_1(\varepsilon^\sharp)$;

(3) $\{t_n \mid n \in \mathbb{N}\} \subseteq \gamma_1(t^\sharp)$;

(4) $\forall A \in \wp_{\text{finite}}(Id_n^\sharp), \sqcup_n(A) \in Id_n^\sharp$ and $\forall a^\sharp \in A, a^\sharp \sqsubseteq_n \sqcup_n(A)$;

(5) $\nabla_n : (Id_n^\sharp)^2 \to Id_n^\sharp$ is a widening operator;

(6) $\forall a \in Id_n^\sharp, b \in Id_m^\sharp, (a \bullet b) \in Id_{n+m}^\sharp$ and

$$ \left\{ (id_i)_{i \in [1; n+m]} \mid \begin{array}{l} (id_i)_{i \in [1; n]} \in \gamma_n(a^\sharp), \\ (id_{i+n})_{i \in [1; m]} \in \gamma_m(b^\sharp) \end{array} \right\} \subseteq \gamma_{n+m}(a \bullet b); $$

(7) $\forall a^\sharp \in Id_n^\sharp, \forall A \in \wp([1; n]^2), \text{sync}(A, a^\sharp) \in Id_n^\sharp$ and
$\{(id_i)_{i \in [1; n]} \mid (id_i) \in \gamma_n(a^\sharp), \forall (k, l) \in A, id_k = id_l\} \subseteq \gamma_n(\text{sync}(A, a^\sharp));$

(8) $\forall a^\sharp \in Id_n^\sharp, \forall p \in \mathbb{N}, \forall (s_k)_{k \in [1; p]} \in [1; n]^{[1:p]}$ one-to-one sequence,
$\prod_{(s_k)} (a^\sharp) \in Id_p^\sharp$ and $\{(id_{s_k})_{k \in [1; p]} \mid (id_i)_{i \in [1; n]} \in \gamma_n(a^\sharp)\} \subseteq \gamma_p(\prod_{(s_k)} (a^\sharp));$

(9) $\forall a^\sharp \in Id_3^\sharp, \text{push}(a^\sharp) \in Id_2^\sharp$ and
$\{(N((i, j), id_1, id_2), id_3) \mid (id_1, id_2, id_3) \in \gamma_3(a^\sharp)\} \subseteq \gamma_2(\text{push}(a^\sharp))$.

Moreover we define the operator $dpush \in (Id_1^\sharp \to Id_2^\sharp)$ by:

$$ \forall a \in Id_1^\sharp, dpush(a) = \text{sync}(\{(1, 2)\}, a \bullet a). $$

The operator $dpush$ satisfies the following property:

$$ \forall a \in Id_1^\sharp, \{(id, id) \mid id \in \gamma_1(a)\} \subseteq \gamma_2(dpush(a)). $$

We denote by $\mathcal{P}$ the set of syntactic components of $\mathcal{S}$. We introduce $\nu n(\mathcal{S})$ as the set of the syntactic names used in name restrictions, including the name $\text{ext}$. We then denote by $I$ the set $\{(p, x, y) \mid p \in \mathcal{P}, x \in \text{fn}(p), y \in \nu n(\mathcal{S})\}$. $I$ is the set of the possible interactions between agents of $\mathcal{S}$. In the case that
$y \neq ext$, the interaction $(p, x, y)$ denotes the fact that the variable $x$ of an instance of the agent $p$ may be linked to the name of a channel opened by the restriction $(\nu y)$; the interaction $(p, x, ext)$ denotes the fact that the variable $x$ of an instance of the agent $p$ may be linked to the name of a channel opened by the context.

In this way, our abstraction $(C^{\sharp}, \sqsubseteq^{\sharp}, \sqcup^{\sharp}, \perp^{\sharp}, \gamma, C_0^{\sharp}, \rightsquigarrow_{cfa}, \nabla)$ is defined as follows:

* $C^{\sharp} = ((I \to id_2^{\sharp}) \times (\nu n(S) \to id_1^{\sharp}))$;

* $\sqsubseteq^{\sharp}, \sqcup^{\sharp}, \nabla$ are defined component-wise and pair-wise respectively from $(\sqsubseteq_2, \sqsubseteq_1), (\sqcup_2, \sqcup_1)$ and $(\nabla_2, \nabla_1)$;

* $\perp^{\sharp}$ is given by the pair of functions which relate any elements respectively to $\perp_2^{\sharp}$ and $\perp_1^{\sharp}$;

* the concretization $\gamma(f, g)$ is the set $(\Sigma^* \times A)$ where $A$ is the set of configurations $(C, U, F)$ which satisfy:

(1) $(P, id_P, E) \in C, x \in fn(P), E(x) = (y, id_x) \implies (id_P, id_x) \in \gamma_2(f(P, x, y)),$

(2) $(x, id) \in U \implies id \in \gamma_1(g(x));$

* $C_0^{\sharp}$ and $\rightsquigarrow_{cfa}$ are given in Figs. 12-14.

An abstract configuration is given by two functions. The first one maps each interaction $(P, x, y)$ to the description of the set of marker pairs $(id_P, id_x)$ such that, in the instance of $P$ tagged with the marker $id_P$, the variable $x$ may be linked to the name of the channel opened by the instance of the name restriction $(\nu y)$ tagged with the marker $id_x$. The second one maps each name $x$ to a description of the set of the markers $id$ such that a channel opened by the instance of the name restriction $(\nu x)$ tagged with the marker $id$ may be communicated to the context. Abstract transition rules just mimic the non-standard ones. Their definition uses an abstract extraction function $\beta^{\sharp}$ defined in Fig. 11.

$$ \beta^{\sharp}((\nu n)P, id^{\sharp}, E^{\sharp}) = \beta^{\sharp}(P, id^{\sharp}, E^{\sharp}[(n, n) \mapsto dpush(id^{\sharp})]) $$

$$ \beta^{\sharp}(\mathbf{0}, id^{\sharp}, E^{\sharp}) = \perp^{\sharp} $$

$$ \beta^{\sharp}(P \oplus Q, id^{\sharp}, E^{\sharp}) = \sqcup^{\sharp}\{\beta^{\sharp}(P, id^{\sharp}, E^{\sharp}); \beta^{\sharp}(Q, id^{\sharp}, E^{\sharp})\} $$

$$ \beta^{\sharp}(P | Q, id^{\sharp}, E^{\sharp}) = \sqcup^{\sharp}\{\beta^{\sharp}(P, id^{\sharp}, E^{\sharp}); \beta^{\sharp}(Q, id^{\sharp}, E^{\sharp})\} $$

$$ \beta^{\sharp}(aP, id^{\sharp}, E^{\sharp}) = (([aP, m, n] \mapsto E^{\sharp}(m, n), \forall m \in fn(aP), n \in \nu n(S)], \emptyset) $$

<caption>Fig. 11. Abstract semantics: abstract extraction</caption>

The function $\beta^{\sharp}$ is an abstract counterpart to $\beta$. It calculates all the interactions obtained by spawning a continuation having a description of both its marker and its environment: given $P \in \mathcal{P}$, $id^{\sharp} \in Id_1^{\sharp}$ and $E^{\sharp} \in ((bn(S) \times \nu n(S)) \to Id_2^{\sharp})$, the element $\beta^{\sharp}(P, id^{\sharp}, E^{\sharp})$ belongs to the abstract domain $C^{\sharp}$ and satisfies the following soundness property:
$$C_0^\sharp = \sqcup^\sharp \{\beta^\sharp(S, \epsilon^\sharp, [(n, ext) \mapsto \epsilon^\sharp \bullet t^\sharp, \forall n \in fn(S)]); \emptyset, [ext \mapsto t^\sharp]\}$$

<caption>Fig. 12. Abstract semantics: initial configurations</caption>

Let $(f_{\text{can}}^{\sharp}, f_{\text{esc}}^{\sharp})$ be an abstract configuration,
if there are $\lambda = y?^i[y_1, \dots, y_n]P$, $\mu = x!^j[x_1, \dots, x_n]Q$,
if $\sqcup_4 \{A(u) \mid u \in \nu n(S)\} \neq \perp_4^{\sharp}$,
then $(f_{\text{can}}^{\sharp}, f_{\text{esc}}^{\sharp}) \rightsquigarrow_{\text{cfa}} \sqcup^{\sharp} \{(f_{\text{can}}^{\sharp}, f_{\text{esc}}^{\sharp}); \beta^{\sharp}(P, id_{P}^{\sharp}, E_{P}^{\sharp}); \beta^{\sharp}(Q, id_{Q}^{\sharp}, E_{Q}^{\sharp})\}$ where

* $A(u) = \text{sync}(\{2, 4\}, f_{\text{can}}^{\sharp}(\lambda, y, u) \bullet f_{\text{can}}^{\sharp}(\mu, x, u))$,

* $id_{P}^{\sharp} = \sqcup_{1}\{\prod_{(1)}(A(u)) \mid u \in \nu n(S)\}$,

* $id_{Q}^{\sharp} = \sqcup_{1}\{\prod_{(3)}(A(u)) \mid u \in \nu n(S)\}$,

* $E_{P}^{\sharp} = [(m, n) \mapsto \sqcup_{2}\{I_{P}(m, n, u) \mid u \in \nu n(S)\}, \forall m \in fn(P), n \in \nu n(S)]$ where $I_{P}(m, n, u) = \begin{cases} \prod_{(1,6)} \text{sync}(\{3, 5\}, A(u) \bullet f_{\text{can}}^{\sharp}(\mu, x_i, n)) & \text{if } m = y_i \\ \prod_{(1,6)} \text{sync}(\{1, 5\}, A(u) \bullet f_{\text{can}}^{\sharp}(\lambda, m, n)) & \text{otherwise,} \end{cases}$

* $E_{Q}^{\sharp} = [(m, n) \mapsto \sqcup_{2}\{I_{Q}(m, n, u) \mid u \in \nu n(S)\}, \forall m \in fn(Q), n \in \nu n(S)]$ where $I_{Q}(m, n, u) = \prod_{(3,6)} \text{sync}(\{3, 5\}, A(u) \bullet f_{\text{can}}^{\sharp}(\mu, m, n))$.

(a) Abstract communication

Let $(f_{\text{can}}^{\sharp}, f_{\text{esc}}^{\sharp})$ be an abstract configuration,
if there are $\lambda = *y?^i[y_1, \dots, y_n]P$, $\mu = x!^j[x_1, \dots, x_n]Q$,
if $\sqcup_4 \{A(u) \mid u \in \nu n(S)\} \neq \perp_4^{\sharp}$,
then $(f_{\text{can}}^{\sharp}, f_{\text{esc}}^{\sharp}) \rightsquigarrow_{\text{cfa}} \sqcup^{\sharp} \{(f_{\text{can}}^{\sharp}, f_{\text{esc}}^{\sharp}); \beta^{\sharp}(P, id_{P}^{\sharp}, E_{P}^{\sharp}); \beta^{\sharp}(Q, id_{Q}^{\sharp}, E_{Q}^{\sharp})\}$ where

* $A(u) = \text{sync}(\{2, 4\}, f_{\text{can}}^{\sharp}(\lambda, y, u) \bullet f_{\text{can}}^{\sharp}(\mu, x, u))$,

* $id_{P}^{\sharp} = \sqcup_{1}\{\prod_{(1)}(\text{push}(\prod_{(i,j)}(A(u)))) \mid u \in \nu n(S)\}$,

* $id_{Q}^{\sharp} = \sqcup_{1}\{\prod_{(3)}(A(u)) \mid u \in \nu n(S)\}$,

* $E_{P}^{\sharp} = [(m, n) \mapsto \sqcup_{2}\{I_{P}(m, n, u) \mid u \in \nu n(S)\}, \forall m \in fn(P), n \in \nu n(S)]$ where

$$I_P(m, n, u) = \begin{cases} \text{push}(\prod_{(i,j)} \text{sync}(\{3, 5\}, A(u) \bullet f_{\text{can}}^{\sharp}(\mu, x_i, n))) & \text{if } m = y_i \\ \text{push}(\prod_{(i,j)} \text{sync}(\{1, 5\}, A(u) \bullet f_{\text{can}}^{\sharp}(\lambda, m, n))) & \text{otherwise,} \end{cases}$$

* $E_{Q}^{\sharp} = [(m, n) \mapsto \sqcup_{2}\{I_{Q}(m, n, u) \mid u \in \nu n(S)\}, \forall m \in fn(Q), n \in \nu n(S)]$ where $I_{Q}(m, n, u) = \prod_{(3,6)} \text{sync}(\{3, 5\}, A(u) \bullet f_{\text{can}}^{\sharp}(\mu, m, n))$.

(b) Abstract resource replication

<caption>Fig. 13. Abstract semantics: internal interactions</caption>
Let $(f_{\text{can}}^{\sharp}, f_{\text{esc}}^{\sharp})$ be an abstract configuration,
if there is $\mu = x!^j[x_1, \dots, x_n]Q$,
if $\sqcup_3\{A(u) \mid u \in \nu n(S)\} \neq \perp_3^{\sharp}$,
then $(f_{\text{can}}^{\sharp}, f_{\text{esc}}^{\sharp}) \rightsquigarrow_{\text{cfa}} \sqcup^{\sharp}\{(f_{\text{can}}^{\sharp}, f_{\text{esc}}^{\sharp}); \beta^{\sharp}(Q, id_Q^{\sharp}, E_Q^{\sharp}); (\emptyset, \text{Escape}^{\sharp})\}$ where

• $A(u) = \text{sync}(\{(2, 3)\}, f_{\text{can}}^{\sharp}(\mu, x, u) \bullet f_{\text{esc}}^{\sharp}(u)),$

• $id_Q^{\sharp} = \bigsqcup_{(1)} \{ \prod_{(1)} (A(u)) \mid u \in \nu n(S) \},$

• $E_Q^{\sharp} = [(m, n) \mapsto \bigsqcup_2 \{I_Q(m, n, u) \mid u \in bn(S)\}, \forall m \in fn(Q), n \in \nu n(S)]$ where $I_Q(m, n, u) = \prod_{(1,5)} \text{sync}(\{1, 4\}, A(u) \bullet f_{\text{can}}^{\sharp}(\mu, m, n)),$

• $\text{Escape}^{\sharp} = [m \mapsto \mathcal{E}(m), \forall m \in \nu n(S)]$ where $\mathcal{E}(m) = \bigsqcup_{(5)} \{\prod_{(5)} (\text{sync}(\{(1,4)\}, A(u) \bullet (f_{\text{can}}^{\sharp}(\mu, x_k, m)))) \mid 1 \le k \le n\}$.

(a) Abstract spied communication

Let $(f_{\text{can}}^{\sharp}, f_{\text{esc}}^{\sharp})$ be an abstract configuration,
if there is $\lambda = y?^i[y_1, \dots, y_n]P$,
if $\sqcup_3\{A(u) \mid u \in \nu n(S)\} \neq \perp_3^{\sharp}$,
then $(f_{\text{can}}^{\sharp}, f_{\text{esc}}^{\sharp}) \rightsquigarrow_{\text{cfa}} \sqcup^{\sharp}\{(f_{\text{can}}^{\sharp}, f_{\text{esc}}^{\sharp}); \beta^{\sharp}(P, id_P^{\sharp}, E_P^{\sharp})\}$ where

• $A(u) = \text{sync}(\{(2, 3)\}, f_{\text{can}}^{\sharp}(\lambda, y, u) \bullet f_{\text{esc}}^{\sharp}(u)),$

• $id_P^{\sharp} = \bigsqcup_{(1)} \{ \prod_{(1)} (A(u)) \mid u \in \nu n(S) \},$

• $E_P^{\sharp} = [(m, n) \mapsto \bigsqcup_2 \{I_P(m, n, u) \mid u \in \nu n(S)\}, \forall m \in fn(P), n \in \nu n(S)]$ where $I_P(m, n, u) = \begin{cases} id_P^{\sharp} \bullet (f_{\text{esc}}^{\sharp}(n)) & \text{if } m = y_k \\ \prod_{(1,5)} \text{sync}(\{1, 4\}, A(u) \bullet f_{\text{can}}^{\sharp}(\lambda, m, n)) & \text{otherwise.} \end{cases}$

(b) Abstract spoiled communication

Let $(f_{\text{can}}^{\sharp}, f_{\text{esc}}^{\sharp})$ be an abstract configuration,
if there is $\lambda = *y?^i[y_1, \dots, y_n]P$,
if $\sqcup_3\{A(u) \mid u \in \nu n\} \neq \perp_3^{\sharp}$,
then $(f_{\text{can}}^{\sharp}, f_{\text{esc}}^{\sharp}) \rightsquigarrow_{\text{cfa}} \sqcup^{\sharp}\{(f_{\text{can}}^{\sharp}, f_{\text{esc}}^{\sharp}); \beta^{\sharp}(P, id_P^{\sharp}, E_P^{\sharp})\}$ where

• $A(u) = \text{sync}(\{(2, 3)\}, f_{\text{can}}^{\sharp}(\lambda, y, u) \bullet f_{\text{esc}}^{\sharp}(u)),$

• $id_P^{\sharp} = \bigsqcup_{(1)} \{ \prod_{(1,0)} (\text{push}((\prod_{(1,0)} \text{sync}(\{1,4\}, A(u) \bullet f_{\text{can}}^{\sharp}(\lambda, m, n) \bullet t^{\sharp}))) \mid u \in \nu n(S) \},$

• $E_P^{\sharp} = [(m, n) \mapsto \bigsqcup_2 \{I_P(m, n, u) \mid u \in \nu n(S)\}, \forall m \in fn(P), n \in \nu n(S)]$ where

$$
I_P(m, n, u) = \begin{cases} (id_P^{\sharp} \bullet f_{\text{esc}}^{\sharp}(n)) & \text{if } m = y_k \\ \text{push}((\prod_{(1,0)} \text{sync}(\{1,4\}, A(u) \bullet f_{\text{can}}^{\sharp}(\lambda, m, n) \bullet t^{\sharp}))) & \text{otherwise.} \end{cases}
$$

(c) Abstract spoiled resource replication

<caption>Fig. 14. Abstract semantics: external interactions</caption>
**Proposition 29** $\forall P \in \mathcal{P}, \forall id \in \gamma_1(id^\#), \forall E \in (fn(P) \to (\nu n(\mathcal{S}) \times \mathcal{M}))$ such that $\forall m \in fn(P), \forall n \in \nu n(\mathcal{S}), \forall id_n \in \mathcal{M}, [E(m) = (n, id_n) \implies (id, id_n) \in \gamma_2(E^\#(m, n))], we have:$

$$ \Sigma^* \times (\beta(P, id, E) \times \{\emptyset\} \times \wp(\{t_n | n \in \mathbb{N}\})) \subseteq \gamma(\beta^\#(P, id^\#, E^\#)). $$

The proof of Prop. 29 is shown in appendix F.

We now give some intuition about the abstract transition rules. For the sake of brevity, we focus on abstract communication. Abstract communication between two syntactic components $\lambda$ and $\mu$ simulates all the possible communications between instances of both $\lambda$ and $\mu$. These communications are first quantified by the channel used by the communication, and more precisely, by the name restriction $(\nu u)$ used in opening this channel. So, for each $u \in \nu n(\mathcal{S})$, we compute an abstraction $A(u)$ of the 4-tuples of markers $(id_\lambda, id_\mu, id_\nu, id_\mu)$ such that $id_\lambda, id_\mu$ may be simultaneously the markers of an instance of $\lambda$ and $\mu$ while $id_\nu$ and $id_\mu$ may be the markers of the instance that has opened the channel named $u$. We obviously enforce the synchronization condition between the second and the fourth components of those tuples, which allows us to detect relations between the first and the third ones. The abstract communication is allowed only if the set of 4-tuples is not empty. In that case, we add the new interactions caused by the continuation of both $\lambda$ and $\mu$. These continuations are calculated using the abstract extraction $\beta^\#$. Continuation marker descriptions are obtained by projecting $A(u)$ onto, respectively, its first and its third components. To calculate abstract environments, we have to deal with interaction communication. An interaction is communicated by abstractly concatenating it with each $A(u)$, enforcing the synchronization with the good agent marker, and then projecting the result in accordance with the marker of the agent it is passed to. New open channels are dealt automatically by the abstract extraction.

**Theorem 30** $(C^\#, \sqsubseteq^\#, \sqcup^\#, \perp^\#, \gamma, C_0^\#, \rightsquigarrow_{cfa}, \nabla)$ is an abstraction.

The proof of Thm. 30 is shown in appendix F.

## 7.2 Abstract domains

Various domains can be used to instantiate the family of parametric domains $(Id_n^\#)_{n \in \mathbb{N}}$, depending on the expected complexity and accuracy. We propose three particular instantiations. The first one abstracts away the information about markers. The result is a uniform control flow analysis. The second one keeps only the equality relations among markers, and gives an analysis which has similar behavior to with group creation [4]. The third one allows algebraic
comparisons of markers which is, to the best of our knowledge, beyond the
scope of the analyses previously presented in the literature.

7.2.1 Uniform control flow analysis

Uniform control flow analysis consists in detecting the potential interactions
between syntactic components, without keeping any information about mark-
ers. For each name restriction (ν x), it will capture an upper-approximation of
the set of the syntactic components to which the names of the channels opened
by this restriction may be communicated. Such an analysis can easily be ob-
tained by instantiating all the elements of the family (Id_n^#)$_{n \in N}$ with the lattice
({⊥, ⊤}, ⊑). The domain {⊥, ⊤} is related to ℘(Id^n) by the concretization
function γ_n defined by γ_n(⊥) = ∅ and γ_n(⊤) = Id^n.

The abstract primitives are then defined as follows:

• ε# = ⊤;

• t# = ⊤;

• ∀A ∈ ℘({⊥; ⊤}), ⋃_n (A) =
  ⎧
  ⎨
  ⎩
    ⊥ if ⊤ ∉ A
    ⊤ otherwise;

• since there is no infinite sequence in {⊥; ⊤} we can use the abstract union
as a widening operator;

• ∀a, b ∈ {⊥, ⊤}, (a • b) =
  ⎧
  ⎨
  ⎩
    ⊥ if a = ⊥ or b = ⊥
    ⊤ if a = ⊤ and b = ⊤;

• ∀a ∈ {⊥, ⊤}, sync(A, a) = a, Π_X (a) = a and push(a) = a. (i,j)

The resulting analysis is always at least as precise as the analysis proposed
in [1,3]. Nielson et al.'s analysis computes the least element of a Moore family
defined as the solution set of a constraint system. Since our abstract union
is exact, and we do not use widening operator, the result of our abstract
semantics is the least fixpoint of the abstract endomorphism induced by C₀# and ↪→cfa. This least fixpoint is also the least element of a Moore family defined
as the solution set of a constraint system. Then, comparing the constraints
involved in both analyses, it turns out that our constraint system is implied
by Nielson et al.'s one. So, any solution of Nielson et al.'s system is also a
solution of our system and the least solution of ours is more precise than
Nielson et al.'s one. Roughly speaking, Nielson et al.'s analysis does not take
into account action sequentiality: the constructed system only depends on the
syntactic action set. Furthermore, it cannot infer distinct interaction sets for
two distinct occurrences of the same channel name.
### 7.2.2 Confinement

We now focus on the equality relations between markers. This allows us to analyze whether or not the name of a channel can be communicated only to the recursive instance which has opened this channel.

For that purpose, we use a graph-based domain to represent equality relations between components of tuples. Each vertex describes a component; a path between two vertices expresses the fact that the two related components are always equal. We then lift that domain with an extra element in order to represent a non-satisfiable property. We first define the set $\mathcal{G}_n$ of all the undirected graphs having vertices in $[[1; n]]$. The transitive closure of a graph $(\mathcal{G}, \frown)$ is denoted by $(\mathcal{G}, \frown^*)$. The pre-order, the concretization function and the abstract primitives are defined on $\mathcal{G}_n$ as follows:

* $\forall \frown_1, \frown_2 \in \wp([1; n]^2), ([1; n], \frown_1) \subseteq_n ([1; n], \frown_2) \iff \frown_2 \subseteq \frown_1,$

* $\forall ([1; n], \frown) \in \mathcal{G}_n, \gamma_n([1; n], \frown) = \{(id_i)_{i \in [1;n]} | k \frown l \Rightarrow id_k = id_l\};$

* we also use $\sqcup_n$ as a widening operator since $\mathcal{G}_n$ is height bounded;

* $\varepsilon^\# = (\{1\}, \emptyset);$

* $t^\# = (\{1\}, \emptyset);$

* $\forall A \in \wp(\mathcal{G}_n), \sqcup_n(A) = ([1; n]; \frown_\cup)$
where $i \frown_\cup j \iff \forall ([1; n], \frown) \in A, i \frown^* j;$

* $\forall a = ([1; n], \frown_a) \in \mathcal{G}_n, b = ([1; m], \frown_b) \in \mathcal{G}_m, (a \bullet b) = ([1; n+m], \frown_\bullet)$
where $i \frown_\bullet j \iff \begin{cases} i \frown_a j & \text{if } i, j \in [1; n] \\ (i-n) \frown_b (j-n) & \text{if } i, j \in [n+1; n+m] \end{cases}$;

* $\forall ([1; n], \frown) \in \mathcal{G}_n, A \in \wp([1; n]^2), \text{sync}(A, ([1; n], \frown)) = ([1; n], A \cup \frown);$

* $\forall a = ([1; n], \frown_a) \in \mathcal{G}_n, \Pi(a) = ([1; p], \frown_\Pi)$
where $s = (s_k)_{k \in [1;p]}$ and $i \frown_\Pi j \iff i, j \in [1; p], s_i \frown_a^* s_j;$

* $\forall a \in \mathcal{G}_3, \text{push}(a) = ([1; 2], \emptyset);$

Roughly speaking, the partial order is the opposite of the constraint set inclusion because, the more constraints, the fewer solutions. The concretization of a graph is the set of all the tuples the components of which satisfy the equality relations described by the edges of this graph. The representation of the empty word is just a graph with one vertex. So is the set representation of the context markers. Gathering some abstract elements consists in intersecting the constraint sets they are described with. Abstract concatenation is just a non-relational union of two graphs, after a renaming of the vertices of the second one. Synchronization consists in adding new constraints. Projection consists in restricting the set of the vertices, keeping equality relations on the remaining vertices. When replicating a resource, we know that the new instance marker is fresh, but we can get no information of this fact. Before applying union and projection, we must close graphs, if not we may lose information.
We then lift each $G_n$ by adding an extra element $\perp_n$. This element $\perp_n$ is the least element of $(G_n \cup \{\perp_n\})$. The concretization of $\perp_n$ is the empty set. Abstract union is lifted as follows:

$$ \sqcup_n(\emptyset) = \perp_n \\ \sqcup_n(A \cup \{\perp_n\}) = \sqcup_n(A). $$

All other abstract primitives are lifted to be strict, which means that they return the good element in $(\perp_i)_{i \in \mathbb{N}}$ with respect to their image domain as soon as one of their arguments is in $(\perp_i)_{i \in \mathbb{N}}$.

As in [4], this analysis can only prove that the name of a channel is confined inside the scope of the recursive instance which has opened this channel. It is unable to prove that the name of a channel which first exits the scope of the agent instance which has opened it, can then only be sent back to the recursive instance which has opened it. The main problem is that we can only propagate equality relations. When the name of a channel is communicated to an agent having a distinct marker than the one of the agent which has opened this channel, we have no information anymore. Then, if the channel name is returned to the agent which has previously opened the channel, we cannot infer the right relation. In order to do that we need an algebraic comparison between markers.

### 7.2.3 Non-uniform analysis with algebraic comparisons

We now propose an abstract domain which deals with abstract algebraic comparisons between markers. Following Prop. 5, we only abstract the right comb of each tree. We choose $m \in \{1; 2\}$, in accordance with the chosen simplification function $\phi_1$ or $\phi_2^6$. We introduce $\Sigma_m$ as the alphabet $\mathcal{L}^m$ of the letters occurring in markers. We use a reduced product between two abstractions. Our first abstraction consists in abstracting component-wise the shape of the markers associated to threads. The second one infers a comparison between the Parikh vectors of the markers.

#### 7.2.3.1 Regular approximation.
We approximate the marker shape in regular languages. For the sake of efficiency, we only use the regular languages which can be described by a set of initial letters, a set of last letters and a succession relation between letters. The result is an efficient abstract domain of languages, the height of which is quadratic in the cardinal of the alphabet $\Sigma_m$, and abstract primitives can be computed with a $O(|\Sigma_m|^2)$ worst-case time cost.

<footnote n="6">⁶ Both functions have been introduced in Sect. 4, Prop. 5.</footnote>
We introduce the set $Id^{\text{Reg}}$ of tuples $(i, f, t, b)$ such that $i, f \in \wp(\Sigma_m)$, $t \in (\Sigma_m \to \wp(\Sigma_m))$ and $b \in \{0; 1\}$. Each element $(i, f, t, b) \in Id^{\text{Reg}}$ is related to a language on $\Sigma_m$ via a concretization function $\gamma^{\text{Reg}}$ defined as follows:

$$ u \in \gamma^{\text{Reg}}(i, f, t, b) \iff \left\{ \begin{array}{l} |u| > 0 \implies u_1 \in i \\ |u| > 0 \implies u_{|u|} \in f \\ \forall i \in \llbracket 1; |u| \rrbracket, |u|_{i+1} \in t(u_i) \\ |u| = 0 \implies b = 1. \end{array} \right. $$

Roughly speaking, $i$ is the set of the initial letters of the language words, $f$ is the set of the final letters. The set $t(a)$ is the set of letters which may immediately follow an occurrence of the letter $a$. The boolean $b$ is equal to 1 if the empty word belongs to the language.

The abstract domain $Id^{\text{Reg}}$ is then fitted with a complete lattice structure $(Id^{\text{Reg}}, \perp^{\text{Reg}}, \subseteq^{\text{Reg}}, \cap^{\text{Reg}}, \cup^{\text{Reg}}, \perp^{\text{Reg}}, \top^{\text{Reg}})$ as follows:

* $\perp^{\text{Reg}} = (\emptyset, \emptyset, [\lambda \mapsto \emptyset], 0)$;

* $\subseteq^{\text{Reg}}, \cup^{\text{Reg}}$ and $\cap^{\text{Reg}}$ are defined component-wise from the usual set operations $\subseteq$, $\cup$ and $\cap$;

* $\top^{\text{Reg}} = (\Sigma_m, \Sigma_m, [\lambda \mapsto \Sigma_m], 1)$.

Furthermore, the language containing only the empty word is described by $(\emptyset, \emptyset, [\lambda \mapsto \emptyset], 1)$ and is denoted by $\varepsilon^{\text{Reg}}$. At last, we can define the primitive $\text{push}^{\text{Reg}} : Id^{\text{Reg}} \times \Sigma_m \to Id^{\text{Reg}}$ which adds a letter at the end of all the words of a language by $\text{push}^{\text{Reg}}((i, f, t, b), \lambda) = (i', f', t', b')$ where:

$$ \left\{ \begin{array}{ll} i' = & \begin{cases} i \cup \{\lambda\} & \text{if } b = 1 \\ i & \text{otherwise;} \end{cases} \\ f' = & \begin{cases} \{\lambda\} & \text{if } b = 1 \text{ or } i \neq \emptyset \\ \emptyset & \text{otherwise;} \end{cases} \\ t' = & \begin{bmatrix} a \mapsto \begin{cases} t(a) \cup \{\lambda\} & \text{if } a \in f \\ t(a) & \text{otherwise;} \end{cases} \\ b' = 0. \end{array} \right. $$

The emptiness test is given by the following equivalence:

$$ \gamma^{\text{Reg}}(i, f, t, b) \neq \emptyset \iff b = 1 \text{ or } \exists a_0, \dots, a_n, \begin{cases} a_0 \in i, a_n \in f, \\ \forall k \in \llbracket 0; n \rrbracket, a_{k+1} \in t(a_k). \end{cases} $$

We then introduce the set $Id_n^{\text{Reg}}$ of the $n$-tuples of $Id^{\text{Reg}}$. It is related to $\wp(Id^n)$ by the following concretization function:

$$ \gamma_n((A_i)_{i \in \llbracket 1; n \rrbracket}) = \{(id_i)_{i \in \llbracket 1; n \rrbracket} \mid \forall i \in \llbracket 1; n \rrbracket, \phi_m(id_i) \in \gamma^{\text{Reg}}(A_i)\}. $$
Then the associated abstract primitives are defined as follows:

• $\varepsilon^{\#} = \varepsilon^{\text{Reg}}$;

• $t^{\#} = (\{a_m\}, \{a_m\}, t_m, 0)$,

where $a_1 = \text{cont}_i, a_2 = (\text{cont}_?, \text{cont}_i)$ and $t_m = \begin{cases} x \mapsto \{a_m\} & \text{if } x = a_m \\ x \mapsto \emptyset & \text{otherwise;} \end{cases}$

• $\sqcup_n$ applies $\sqcup^{\text{Reg}}$ component-wisely;

• $\Pi$ (resp. •) is the classical projection (resp. concatenation) of tuples;

• $\text{sync}(A, Q)_i = \bigcap^{\text{Reg}}\{Q_j \mid (i, j) \text{ in the reflexive and transitive closure of } A\}$;

• since there is no infinite ascending sequences, we define our widening operator $\nabla_n$ to be $\sqcup^n$;

• $\text{push}_{\lambda}(a, b, c) = \text{push}^{\text{Reg}}(b, \lambda)$.

### 7.2.3.2 Numerical approximation.
Our second abstraction captures relational comparisons between the occurrence number of each pattern inside sets of marker pairs. For each $n \in \mathbb{N}$, we introduce a set $\mathcal{V}_n$ of distinct variables $\{x_i^{\lambda} \mid i \in [1; n]\}, \lambda \in \Sigma_m\}$. The abstract domain $\wp(\mathbb{N}^{\mathcal{V}_n})$ is related to $\wp(\text{Id}^n)$ by the monotonic map $\gamma_n$:

$$ \gamma_n(A) = \{(id_i)_{i \in [1; n]} \mid \exists(n_t)_{t \in \mathcal{V}_n} \in A, \forall x_i^{\lambda} \in \mathcal{V}_n, n_{x_i^{\lambda}} = |\phi_m(id_i)|_{\lambda}\}. $$

The power set $\wp(\mathbb{N}^{\mathcal{V}_n})$ is then related to a numerical domain. Many relational numerical domains have been introduced in the literature [10, 17, 21, 24]. We propose two choices in accordance with the expected trade-off between complexity and accuracy. They both use the complete lattice of affine equality systems among a set of variables. This domain is described with its lattice operations in [21]. Given a set of variables $\mathcal{V}$, we denote by $\mathcal{K}_{\mathcal{V}}$ the domain of the affine equality systems among the elements of $\mathcal{V}$.

#### 7.2.3.2.1 Component-wise affine comparison

The first choice for abstracting a set of word tuples consists in abstracting the affine relations between the occurrence number of $\lambda$ in each tuple component, for each $\lambda$ in $\Sigma_m$. This way, we introduce $\text{Id}_n^{\text{Rel}}$ as the complete lattice $(\Sigma_m \to \mathcal{K}_{\{x_i \mid i \in [1; n]\}})$ defined point-wise.

We then define abstract primitives as follows:

• $\varepsilon^{\#}$ maps each letter in $\Sigma_m$ to the system composed of the only constraint $x_1 = 0$;

• $t^{\#}$ maps each letter in $\Sigma_m$ to the system composed of the only constraint $x_1 = 0$, except the letter $a_m$ which is mapped to the system that contains no constraint, where $a_1 = \text{cont}_i$ and $a_2 = (\text{cont}_?, \text{cont}_i)$;

• $\sqcup_n$ applies the affine hull point-wise;
• $\Pi_{(i_1, \dots, i_p)}(f)(\lambda)$ is obtained by using Gaussian elimination to collect all the constraints involving only the variables $\{x_{i_k}\}$ in the system $f(\lambda)$, and then by renaming each variable $x_{i_k}$ into the variable $x_k$;

• $\forall f \in Id_p^{\text{Rel}}, g \in Id_q^{\text{Rel}}, f \bullet g$ maps each letter $\lambda \in \Sigma_m$ to the system composed of the constraints in $f(\lambda)$ and those in $g(\lambda)$, where each occurrence of a variable matching $x_i$ in the constraints of $g(\lambda)$ is replaced by the variable $x_{i+p}$;

• for each $\lambda \in \Sigma_m$, $\text{sync}(\{(i_1, j_1), \dots, (i_p, j_p)\}, f)(\lambda)$ is obtained by inserting all the constraints of the form $x_{i_k} = x_{j_k}$, for $k \in [1; p]$, in the system $f(\lambda)$;

• since there is no infinite ascending sequence, we define our widening operator $\nabla_n$ to be $\bigsqcup_n$;

• $\text{push}(f)$ is obtained by first replacing each occurrence of the variable $x_2$ in the constraints of the system $f(\lambda)$ by the expression $x_2 - 1$, and then applying the abstract projection $\Pi_{(2,3)}$.

### 7.2.3.2.2 Global affine comparison

The second choice consists in abstracting globally all constraints. Roughly speaking, the variable $x_i^\lambda$ denotes the occurrence number of $\lambda$ in the $i$-th component of marker tuples. We introduce $Id^{\text{Rel}}$ as the complete lattice $\mathcal{K}_{\mathcal{V}_n}$ of affine equality systems on the set of variables $\mathcal{V}_n$. Lattice operations are described in [21]. We describe the remaining primitives as follows:

• $\varepsilon^\#$ is given by the system $\{x_1^\lambda = 0, \forall \lambda \in \Sigma\}$;

• $t^\#$ is given by the system $\{x_1^\lambda = 0, \forall \lambda \in \Sigma \setminus \{a_m\},$ where $a_1 = \text{cont}_1$ and $a_2 = (\text{cont}_2, \text{cont}_3)$;

• given $K \in Id_p^{\text{Rel}}$ and $K' \in Id_q^{\text{Rel}}$, we obtain the abstract concatenation of $K$ and $K'$, by renaming each variable $x_i^\lambda$ to $x_{i+p}^\lambda$ in $K'$, and gathering all the constraints of the two systems;

• $\text{sync}(\{(i_1, j_1), \dots, (i_p, j_p)\}, K)$ corresponds to inserting all the constraints of the form $x_{i_k}^\lambda = x_{j_k}^\lambda, \forall k \in [1; p], \lambda \in \Sigma$ in $K$;

• $\Pi_{(i_1, \dots, i_p)}(K)$ corresponds to collecting all the constraints involving only the variables $\{x_{i_k}^\lambda\}$ and then renaming each variable $x_{i_k}^\lambda$ into the variable $x_k^\lambda$;

• $\text{push}(K)$ is obtained by replacing first in each constraint each occurrence of $(i,j)$ the variable $x_2^{(i,j)}$ by the expression $x_2^{(i,j)} - 1$ and then applying the abstract projection $\Pi_{(2,3)}$.

**Remark 31** The global affine comparison domain has not been implemented yet.
We now describe results obtained on our examples. All these results are ob-
tained by setting $m = 2$. In the description of these results, we make no
distinction between a marker and its abstraction by $\Phi_2$.

**Example 32** In the ftp-server example, the analyzer proves that the name of a channel opened by the restriction ($\nu$ **address**) can only be communicated to the variable **email** or to the variable **address**, and that the name of a channel opened by the restriction ($\nu$ **request**) can only be communicated to the variable **request**, to the variable **data** or to the variable **rep**. More specifically, it discovers that each time an agent **email**![**rep**] is spawned, there exist $p,q$ in $\mathbb{N}$ such that the agent marker is $(1, 16).(1, 5)^p.(2, 4).(6, 3).(2, 12)^q.(2, 4).(6, 3)$; the variable **email** is linked to the name of a channel opened by the restriction ($\nu$ **address**) of the instance the marker of which was $(1, 16).(1, 5)^p$; and the variable **rep** is linked to the name of a channel opened by the restriction ($\nu$ **request**) of the instance the marker of which was $(1, 16).(1, 5)^p$. This is enough to prove that both variables **email** and **data** are linked to names of channels opened by the same instance of the client resource and so the answer to a query can only be sent back to the correct client.

**Example 33** In the token-ring example, the analyzer discovers that in each instance of an agent **mon**![**left**, **right**], the variable **left** is either bound to the name of a channel opened by an instance of the (**ν** **right**) restriction or to the name of a channel opened by an instance of the (**ν** **left0**) restriction, and the variable **right** is always bound to the name of a channel opened by an instance of the (**ν** **right**) restriction. More specifically, in the case where the variable **left** is bound to the name of a channel opened by an instance of the (**ν** **right**) restriction, it discovers that there exists $n \in \mathbb{N}$ such that the instance marker of **mon**![**left**, **right**] is $(1, 6)(1, 3)^{n+1}$; the variable **left** is linked to the name of a channel opened by the restriction (**ν** **right**) of the instance the marker of which was $(1, 6)(1, 3)^n$; and the variable **right** is linked to the name of a channel opened by the restriction (**ν** **right**) of the instance the marker of which was $(1, 6)(1, 3)^{n+1}$. This is enough to prove that each process can only be linked to either the next one or to the first one.

**Remark 34** Our confinement analysis is not simply an abstraction of our non-uniform analysis since two distinct markers may be recognized by the same automaton while containing the same occurrence number of each pattern (i.e having the same Parikh vector [27]). The equality of the Parikh vectors implies the equality of the markers if they are recognized by an automaton that contains only one acyclic path between an initial and a final state, without embedded cycle, and such that the set of the Parikh vectors of the cycles of this automaton are linearly independent. Nevertheless, we may use a reduced product of both our confinement analysis and our non-uniform control flow analysis to solve
this problem.

**Remark 35** The uniform analysis is not complete with respect to the non-uniform one, this means, that computing the non-uniform analysis and then abstracting the result in order to ignore marker information can give more accurate results than directly computing the result of the uniform analysis. This is illustrated in example 36.

**Example 36** We consider the following mobile system:

$$ (ν a)(ν b)(ν x) \\ ( *x?¹[z]((ν t)z!²[t]t!³[z]) \\ | * repli?⁴[]x!⁵[a] \\ | * repli?⁶[]x!⁷[b] \\ | * a?⁸[i]i?⁹[j]trace!¹⁰[j] \\ ) $$

This system is composed of four resources. The second and the third ones allow the spawning of an unbounded number of agents either of the form $x!⁵[a]$ or of the form $x!⁷[b]$. The first resource can be replicated by an agent either of the form $x!⁵[a]$ or of the form $x!⁷[b]$, nevertheless the behavior of the spawned instance is deeply bound to which kind of agent has replicated the resource:

* when the resource is replicated with an agent of the form $x!⁵[a]$: a channel is opened; its name $t$ is sent via the channel named $a$, so that $t$ can be send to an instance of the fourth resource; this instance can then receive the name $a$ via the channel denoted by $t$; then the instance of the first resource can send the name $a$ via the channel named $t$, so that the instance of the fourth resource can receive the name $a$ via the channel named $t$ and send it through the channel named *trace*; then an intruder can get the name $a$, by spying the channel named *trace*;

* when the resource is replicated with an agent of the form $x!⁷[b]$: a channel is opened, its name $t$ is sent via the channel named $b$, but cannot be received, so the instance is stuck, and no intruder can get the name $b$.

The non-uniform analysis captures the fact that the name $b$ cannot be spied by an intruder, while the uniform does not. Roughly speaking, the main reason is that the non-uniform analysis relates the names communicated to an agent with the history of the replications which have led to the creation of this agent, while the uniform analysis abstracts this information away.
We now propose to count the occurrence number of agents during computa-
tion sequences. We first abstract away any information about markers and
environments. This way, a configuration is just seen as a multi-set of syntac-
tic agents. In order to capture many more properties, we relate occurrence
number of agents to the number of performed transitions. In this section, we
are not interested in channels and markers, so we will denote a configuration
(C, U, F) by its set of threads C.

Our abstraction requires an abstract domain to describe natural number fam-
ilies. In the first subsection, we introduce a generic analysis, independently of
this domain. In the next subsection, we propose a well-suited abstract domain.

8.1 Generic analysis

We denote by $\mathcal{P}$ the set of syntactic components of $\mathcal{S}$ and choose a set $\mathcal{T}$ of variables used to count performed transitions. Since the number of transition labels is quadratic, we may want to quotient this set into equivalence classes, in order to deal with fewer variables. The set $(\mathcal{L}_{\text{used}} \cup \{0\})^2$ is related to $\mathcal{T}$ by an onto map $\psi$. We propose three natural choices for $\mathcal{T}$ and $\psi$ in accordance with the expected trade-off between accuracy and efficiency:

(1) we can use one extra variable by assigning
$\mathcal{T} = \{0\}$ and $\forall i, j \in \mathcal{L}_{\text{used}} \cup \{0\}, \psi(i, j) = 0,$

(2) we can use a linear number of extra variables by assigning
$\mathcal{T} = \{(0, j) \mid j \in \mathcal{L}_{\text{used}} \cup \{0\}\}$ and $\forall i, j \in \mathcal{L}_{\text{used}} \cup \{0\}, \psi(i, j) = (0, j),$

(3) we can use a quadratic number of extra variables by assigning
$\mathcal{T} = (\mathcal{L}_{\text{used}} \cup \{0\})^2$ and $\forall i, j \in \mathcal{L}_{\text{used}} \cup \{0\}, \psi(i, j) = (i, j).$

Let $V$ be the set $\mathcal{P} \cup \mathcal{T}$. We introduce an abstraction $\Pi_{\mathbb{N}V}$ which maps each concrete configuration $(u, C)$ in $\Sigma^* \times \mathcal{C}(\mathcal{S})$ to a family of natural numbers indexed by the set $V$, as follows:

$$
(\Pi_{\mathbb{N}V}(u, C))_v = \begin{cases} \text{Card}(\{(P, id, E) \in C \mid P = v\}) & \text{if } v \in \mathcal{P} \\ \sum_{\lambda \in \psi^{-1}(v)} |u|_{\lambda} & \text{if } v \in \mathcal{T}. \end{cases}
$$

**Proposition 37** Let $(u_1, C_1)$ and $(u_2, C_2)$ be two configurations such that $C_1 \cap C_2 = \emptyset$, then for any $v \in V$, we have $\Pi_{\mathbb{N}V}(u_1 \cdot u_2, C_1 \cup C_2)_v = (\Pi_{\mathbb{N}V}(u_1, C_1))_v + (\Pi_{\mathbb{N}V}(u_2, C_2))_v$.

We then consider $\wp(\mathbb{N}^V)$, the complete lattice of sets of natural number families indexed by $V$. The power set $\wp(\mathbb{N}^V)$ is related to our concrete domain $\wp(\Sigma^* \times$
$C(S))$ via a concretization function $\gamma_{\mathbb{N}^V}$, where $\forall A^{\sharp}, \gamma_{\mathbb{N}^V}(A^{\sharp})$ is defined as follows:

$$ \{(u, C) \in \Sigma^* \times C(S) \mid \Pi_{\mathbb{N}^V}(u, C) \in A^{\sharp}\}. $$

We then introduce a generic pre-order $(\mathcal{N}_V, \sqsubseteq_{\mathcal{N}_V})$ to represent sets of natural number families indexed by $V$. It is related to $\wp(\mathbb{N}^V)$ via a monotonic concretization $\gamma_{\mathcal{N}_V}$. Furthermore, we introduce several generic primitives: a representation $\perp_{\mathcal{N}_V}$ of the empty set, an abstract union $\cup_{\mathcal{N}_V}$, a widening operator $\nabla_{\mathcal{N}_V}$, an abstract counterpart + to the addition, an abstract counterpart – to the subtraction, an abstract synchronization $sync_{\mathcal{N}_V}$. We also require the abstraction of some elementary family: an abstract element $0_{\mathcal{N}_V}$ to represent the singleton containing the 0 family which associates 0 to each element in $V$, and $\forall v \in V$, an abstract element $1_{\mathcal{N}_V}(v)$ to represent the singleton containing the family $\delta^v$ which associates 1 to the element $v$ and 0 to any other elements.

These primitives should satisfy the following properties:

(1) $\gamma_{\mathcal{N}_V}(\perp_{\mathcal{N}_V}) = \emptyset$,

(2) $\forall a \in \mathcal{N}_V, \perp_{\mathcal{N}_V} \sqsubseteq_{\mathcal{N}_V} a$,

(3) $\forall A \in \wp_{\text{finite}}(\mathcal{N}_V), \cup_{\mathcal{N}_V}(A) \in \mathcal{N}_V$ and $\forall a \in A, a \sqsubseteq_{\mathcal{N}_V} \cup_{\mathcal{N}_V}(A)$,

(4) $\nabla_{\mathcal{N}_V}$ satisfies Def. 24.(7),

(5) $\forall a^{\sharp}, b^{\sharp} \in \mathcal{N}_V, (a^{\sharp} + b^{\sharp}) \in \mathcal{N}_V$ and $\{(a_v + b_v)_{v \in V} \mid a \in \gamma_{\mathcal{N}_V}(a^{\sharp}), b \in \gamma_{\mathcal{N}_V}(b^{\sharp})\} \subseteq \gamma_{\mathcal{N}_V}(a^{\sharp} + b^{\sharp})$,

(6) $\forall a^{\sharp}, b^{\sharp} \in \mathcal{N}_V, (a^{\sharp} - b^{\sharp}) \in \mathcal{N}_V$ and $\{(a_v - b_v)_{v \in V} \mid a \in \gamma_{\mathcal{N}_V}(a^{\sharp}), b \in \gamma_{\mathcal{N}_V}(b^{\sharp}), \forall v \in V, a_v \ge b_v\} \subseteq \gamma_{\mathcal{N}_V}(a^{\sharp} - b^{\sharp})$,

(7) $\forall a^{\sharp} \in \mathcal{N}_V, I \in \wp(\mathcal{L}), sync_{\mathcal{N}_V}(I, a^{\sharp}) \in \mathcal{N}_V$ and $\{a \mid a \in \gamma_{\mathcal{N}_V}(a^{\sharp}), \forall i \in I, a_i \ge 1\} \subseteq \gamma_{\mathcal{N}_V}(sync_{\mathcal{N}_V}(I, a^{\sharp}))$,

(8) $0_{\mathcal{N}_V} \in \mathcal{N}_V$ and $(0)_{i \in V} \in \gamma_{\mathcal{N}_V}(0_{\mathcal{N}_V})$,

(9) $\forall v \in V, 1_{\mathcal{N}_V}(v) \in \mathcal{N}_V$ and $(\delta_i^v)_{i \in V} \in \gamma_{\mathcal{N}_V}(1_{\mathcal{N}_V}(v))$.

Roughly speaking, + is an abstract counterpart to the component-wise addition, – is an abstract counterpart to the component-wise subtraction, $sync_{\mathcal{N}_V}$ is used to extract from an abstract value the representation of the configurations which simultaneously contain all the agents required by a computation step.

We define an abstract transition system $(C_0^{\mathcal{N}_V}, \sim_{\mathcal{N}_V})$ in Fig. 15. It uses an abstract extraction function $\beta_{\mathcal{N}_V}$ which computes an approximation of the syntactic agents which are spawned at the beginning of the system or when launching a continuation. Internal choice $\oplus$ and parallel composition $|$ are just abstracted by their respective abstract counterparts $\cup_{\mathcal{N}_V}$ and $+$.

**Proposition 38** $\forall P \in \mathcal{P}, \forall id \in \mathcal{M}, \forall E \in (fn(P) \to (\nu n(S) \times \mathcal{M})), \text{ we have} \\ \text{Cont} \in \beta(P, id, E) \implies (\varepsilon, \text{Cont}) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(\beta_{\mathcal{N}_V}(P)).$
The proof of Prop. 38 is shown in appendix G.

The initial abstract configuration is obtained by applying $\beta_{N_v}$ to the initial
system. An abstract communication between two syntactic components la-
belled i and j from an abstract state $C^\sharp$ first consists in computing a descrip-
tion of the set of the configurations described in $C^\sharp$ in which both syntactic
components may occur simultaneously. If this set is empty, the components
are mutually exclusive and the abstract communication is disabled. Other-
wise, the result of the communication is obtained by translation: decreasing
the occurrence number of the communicating agents which are not resources,
and adding the description of both continuations. External interactions are
dealt with in the same way, but only one agent is involved. We do not bother
about the control flow, since we use a reduced product between this analysis
and one of our control flow analyses.

**Theorem 39** ($\mathcal{N}_V, \sqsubseteq_{\mathcal{N}_V}, \cup_{\mathcal{N}_V}, \perp_{\mathcal{N}_V}, \gamma_{\mathcal{N}V} \circ \gamma_{\mathcal{N}_V}, C_0^{\mathcal{N}_V}, \rightsquigarrow_{\mathcal{N}_V}, \nabla_{\mathcal{N}_V}$) is an abstraction.

The proof of Thm. 39 is shown in appendix G.

## 8.2 Abstract domain

We only need to define an abstract domain to approximate sets of indexed
family of natural numbers in which abstract primitives can be precisely and
efficiently implemented. On the one hand, the primitive $sync_{N_v}$ needs to ex-
press the property that several variables may simultaneously be greater than
one, which is a relational information. On the other hand, the shape of the
abstract computation rule suggests that the domain should be closed under
addition. This problem is very similar to abstracting the occurrence number
of ambients [18,26], or even approximating the collecting semantics of a Petri
net. We reject the use of usual numerical domains. We are unlikely to design
a precise primitive $sync_{N_v}$ in non-relational domains. Disjunctive completion
can be used to lift a non-relational domain into a relational one: each configu-
ration is abstracted in a finite non-relational domain, and then the abstraction
of a configuration set is given by the collection of all the abstractions of its
elements. Nevertheless, disjunctive completion often leads to a lack of accu-
racy and an exponential explosion. We cannot afford the domain of linear
inequalities among a finite set of variables [10] because we deal with too many
variables.

We propose the use of a reduced product between two domains: the interval
lattice and the linear equalities lattice described in [21]. The first domain is
based on the use of the interval lattice and is used for expressing properties
of interest. This domain can represent all the properties we need to express
$$ \beta_{N_V}((\nu n)P) = \beta_{N_V}(P) $$

$$ \beta_{N_V}(\mathbf{0}) = 0_{N_V} $$

$$ \beta_{N_V}(P \oplus Q) = \beta_{N_V}(P) \cup_{N_V} \beta_{N_V}(Q) $$

$$ \beta_{N_V}(P | Q) = \beta_{N_V}(P) + \beta_{N_V}(Q) $$

$$ \beta_{N_V}(aP) = 1_{N_V}(aP) $$

(a) Abstract extraction

$$ C_0^{N_V} = \beta_{N_V}(S) $$

(b) Initial configuration

Let $v^\sharp$ be an abstract configuration,
if there are $i, j \in \mathcal{L}_{\text{used}} \cup \{0\}$,
such that $\text{sync}_{N_V}(\{\text{agent}(l) \mid l \in \{i, j\} \setminus \{0\}\}, v^\sharp) \neq \perp_{N_V}$,
then
$v^\sharp \stackrel{(i,j)}{\rightsquigarrow}_{N_V}(\text{sync}_{N_V}(\{\text{agent}(l) \mid l \in \{i, j\} \setminus \{0\}\}, v^\sharp) + \text{Act}(i) + \text{Act}(j) + 1_{N_V}(\psi(i, j)))$,
where

• $\forall l \in \mathcal{L}_{\text{used}} \setminus \{0\}, \text{agent}(l) \in \mathcal{P} \subset V$ is the syntactic agent labelled with $l$,

• $\text{Act}(l) = \begin{cases} 0_{N_V} & \text{if } l = 0 \\ \beta_{N_V}(P) - 1_{N_V}(aP) & \text{if } \text{agent}(l) = aP \\ \beta_{N_V}(P) & \text{and } a \text{ matches } y^l[\bar{y}] \text{ or } x^l[\bar{x}] \\ \beta_{N_V}(P) & \text{if } \text{agent}(l) \text{ matches } *y^l[\bar{y}]P. \end{cases}$

(c) Abstract transition rule

<caption>Fig. 15. Occurrence counting analysis</caption>

non-exhaustion of resources, but it cannot calculate them precisely without being refined. The second domain is based on the use of linear equalities between variables [21] and is used for expressing more complex properties, such as mutual exclusion, which allows for more precise calculations in the first domain. The power of our analysis directly comes from the use of an inexpensive algorithm, straightforwardly adapted from Linear Constraint Programming, to calculate an approximated reduction between these two domains.
### 8.2.1 Interval domain

The complete lattice ($\mathcal{I}$, $\sqsubseteq_{\mathcal{I}}$, $\sqcup_{\mathcal{I}}$, $\perp_{\mathcal{I}}$, $\sqcap_{\mathcal{I}}$, $\top_{\mathcal{I}}$) is the functional domain of natural number intervals, where lattice operations are defined point-wisely. The abstract domain $\mathcal{I}$ is related to $\wp(\mathbb{N}^V)$ via the monotonic map $\gamma_{\mathcal{I}}$ defined by:

$$ \gamma_{\mathcal{I}}(f) = \{u \in \mathbb{N}^V \mid \forall i \in V, u_i \in f(i)\}. $$

A family ($\nabla_{\mathcal{I}}^n$) of widening operators on $\mathcal{I}$ is defined as follows:

$$ [f \nabla_{\mathcal{I}}^n g](x) = f(x) \nabla^n g(x) \\ \text{where } \llbracket a; b \rrbracket \nabla^n \llbracket c; d \rrbracket = \begin{cases} \llbracket \min\{a; c\}; +\infty \rrbracket & \text{if } d > \max\{b; n\} \\ \llbracket \min\{a; c\}; \max\{b; d\} \rrbracket & \text{otherwise.} \end{cases} $$

We can easily define abstract primitives in $\mathcal{I}$ as follows:

* $(f +_{\mathcal{I}} g) = [x \to f(x) + g(x)]$,

* $(f -_{\mathcal{I}} g) = [x \to (f(x) - g(x)) \cap \llbracket 0; +\infty \rrbracket]$,

* $\text{sync}_{\mathcal{I}}(I, f) = \left[ x \to \begin{cases} f(x) \cap \llbracket 1; +\infty \rrbracket & \text{if } x \in I \\ f(x) & \text{otherwise} \end{cases} \right]$,

* $0_{\mathcal{I}} = [x \to \llbracket 0; 0 \rrbracket]$,

* $1_{\mathcal{I}}(v) = \left[ \begin{cases} x \to \llbracket 1; 1 \rrbracket & \text{if } x = v \\ x \to \llbracket 0; 0 \rrbracket & \text{otherwise} \end{cases} \right]$.

### 8.2.2 Linear equalities domain

The complete lattice ($\mathcal{K}$, $\sqsubseteq_{\mathcal{K}}$, $\cup_{\mathcal{K}}$, $\top_{\mathcal{K}}$, $\cap_{\mathcal{K}}$, $\perp_{\mathcal{K}}$) of linear equality systems between the finite set of variables $V$ is described with its lattice operations in [21]. This domain uses Gaussian elimination in order to normalize systems. It is related to the domain $\wp(\mathbb{N}^V)$ via the monotonic function $\gamma_{\mathcal{K}}$ which maps each system to the set of its solutions. Moreover, since there is no infinite ascending chain [21], we can choose $\cup_{\mathcal{K}}$ as a widening operator. To define the addition $+_{\mathcal{K}}$ and the subtraction $-_{\mathcal{K}}$ of two systems, we compute a particular solution of each system $O_1$ and $O_2$, and a linear direction $\vec{H}_1$ and $\vec{H}_2$. Then we use the following equalities:

$$ (O_1 + \vec{H}_1) +_{\mathcal{K}} (O_2 + \vec{H}_2) = (O_1 + O_2) + (\vec{H}_1 \cup_{\mathcal{K}} \vec{H}_2), $$

$$ (O_1 + \vec{H}_1) -_{\mathcal{K}} (O_2 + \vec{H}_2) = (O_1 - O_2) + (\vec{H}_1 \cup_{\mathcal{K}} \vec{H}_2). $$

Such a decomposition can be extracted from the normal form in linear time, so the cost of affine addition and subtraction is cubic.
Other primitives are defined as follows:

* $\text{sync}_K(I, K) = K,$

* $0_K = \{x = 0, \forall x \in V,$

* $1_K(v) = \begin{cases} x = 1 & \text{if } x = v \\ x = 0 & \text{otherwise.} \end{cases}$

Roughly speaking, synchronization cannot be directly checked in $\mathcal{K}$. So we define it as the identity. Linear constraints will therefore be used to prove that synchronization interval constraints are incompatible, by reduction. Other primitive definitions are straightforward.

### 8.2.3 Approximated reduced product

Our numerical domain is the product $(\mathcal{I} \times \mathcal{K})$. It is partially ordered by the pair-wise order $\sqsubseteq_{\mathcal{I}} \times \sqsubseteq_{\mathcal{K}}$. It is related to $\wp(\mathbb{N}^V)$ by the concretization function $\gamma_{\mathcal{N}_V}$ where $\gamma_{\mathcal{N}_V}(i, s)$ is defined as $\gamma_{\mathcal{I}}(i) \cap \gamma_{\mathcal{K}}(s)$. Generic primitives are expressed as follows:

* $\perp_{\mathcal{N}_V}, \cup_{\mathcal{N}_V}, \nabla_{\mathcal{N}_V}, +, \sqsubseteq_{\mathcal{N}_V}, 0_{\mathcal{N}_V}, 1_{\mathcal{N}_V}$ are defined pair-wisely,

* $\text{sync}_{\mathcal{N}_V}(A, (i, s)) = \rho(i', s)$, where $\begin{cases} i'(x) = i(x) \cap [1; +\infty| & \forall x \in A \\ i'(x) = i(x) & \forall x \in \mathcal{P} \setminus A, \end{cases}$ and $\rho$ satisfies $\forall a \in \mathcal{I} \times \mathcal{K}, \gamma_{\mathcal{N}_V}(a) \sqsubseteq_{\mathcal{N}_V} \gamma_{\mathcal{N}_V}(\rho(a))$.

The definition of $\text{sync}_{\mathcal{N}_V}$ uses a reduction operator $\rho$ which satisfies the following property:

$$ \forall a \in \mathcal{I} \times \mathcal{K}, \gamma_{\mathcal{N}_V}(a) \sqsubseteq_{\mathcal{N}_V} \gamma_{\mathcal{N}_V}(\rho(a)). $$

Roughly speaking, the operator $\rho$ is a reduction, it simplifies constraints without losing any solution. We now present a reduction $\rho$ between $\mathcal{I}$ and $\mathcal{K}$. It consists in taking into account linear constraints in order to narrow interval ranges. For instance, the system of constraints $\{x + y = 12, x \in [3; 15], y \in [4; 19]\}$ can be reduced to the system $\{x + y = 12, x \in [3; 8], y \in [4; 9]\}$. Linear constraints are likely to be combined, via Gaussian elimination, in order to give new linear constraints which will allow for further reductions. Therefore, generating the whole set of such combinations is likely to require an exponential time of execution.

We propose a two-step polynomial algorithm for computing an approximate solution to this problem. The first step aims at narrowing infinite intervals into finite ones. It uses Gaussian elimination to obtain a positive representation of systems of linear equalities, that is to say, an equivalent system of equations
such that if a variable occurs with a strictly negative coefficient in an equation, then this variable occurs with a negative coefficient in each equation. Positive representations contain only a few undefined forms<fnref n="7" />, which allows narrowing most of the infinite intervals into finite ones with a $O(|V|^3)$ worst-case. The second step is inspired by [5]: it consists in obtaining a triangular system of constraints of the form $a_1.x_1 + ... + a_n.x_n \in I$ where $I$ is an interval. This system is then used to propagate unidirectionally intervals from non-diagonal to diagonal variables. The result is a good reduction with a $O(|V|^4)$ worst-case. In the case that the algorithm discovers an unsatisfiable constrain, the result of the reduction is set to $\perp_{N_V}$.

**8.2.3.1 Solving undefined forms** Let $V_{inf}$ be a subset of $V$ and $K$ a finite system of linear constraints on the variables $V$. We denote by $K$ the system of equations:

$$ \left\{ \sum_{v \in V} a_i^v.v = b_i, \forall i \in [1; n] \right. . $$

We first define a positive form with respect to $V_{inf}$ as follows:

**Definition 40** $K$ is in positive form with respect to $V_{inf}$ if and only if $\forall v \in V, \exists i_1, i_2 \in [1; n]$ such that $a_{i_1}^v < 0 < a_{i_2}^v \Rightarrow v \notin V_{inf}$.

This way, the variables which may occur in the matrix describing $K$ with both a positive and a negative coefficient are known to be bounded<fnref n="8" />. Such a form can be computed by using the Gaussian elimination with a $O(|V|^3)$ worst-case time cost. A positive form contains only few undefined forms. For each constraint in which all variables with an infinite range occur with the same sign, we can narrow the range of variables that occurs in this constraint into finite intervals. A dynamic resolution of such a system leads to a reduction step in $O(|V|^2)$.

**8.2.3.2 Narrowing finite intervals** The second step is inspired by [5]: it consists in obtaining a triangular system of constraints of the form $a_1.x_1 + ... + a_n.x_n \in I$ where $I$ is an interval. This system is then used to propagate unidirectionally intervals from non-diagonal to diagonal variables. The result is a good reduction with a $O(|V|^4)$ worst-case time cost.

We use three kinds of reductions:

<footnote n="7">⁷ An undefined form is a subtraction between two unbounded intervals</footnote>

<footnote n="8">⁸ $V_{inf}$ denotes the set of the variables which are not proved to be bounded.</footnote>
(1) Gaussian elimination:

$$ \begin{cases} x + y + z = 1 \\ x + y + t = 2 \end{cases} \implies \begin{cases} x + y + z = 1 \\ t - z = 1, \end{cases} $$

(2) interval propagation:

$$ \begin{cases} x + y + z = 3 \\ x \in [0; 5] \\ y \in [0; 6] \\ z \in [0; 8] \end{cases} \implies \begin{cases} x + y + z = 3 \\ x \in [0; 3] \\ y \in [0; 6] \\ z \in [0; 8], \end{cases} $$

(3) redundancy introduction:

$$ \begin{cases} x + y - z = 3 \\ x \in [1; 2] \end{cases} \implies \begin{cases} x + y - z = 3 \\ y - z \in [1; 2] \\ x \in [1; 2]. \end{cases} $$

We first use Gaussian elimination to get a normal form of the linear constraint system, we then use interval propagation to narrow the range of the interval of the pivot of each constraint. Then, we forget about the pivot using redundancy introduction. We then get a new system involving only variables which were not a pivot of a constraint in the previous one. We then proceed recursively with it until constraints contain some variables. We then consider all the constraints we have computed which form a triangular system. We propagate the information we have collected on the interval ranges backward, by applying interval propagation from non-diagonal variables to diagonal ones, starting from the last constraint and ending with the first one.

### 8.2.4 Examples

We now describe some examples of mobile systems analyzed with our prototype. For the sake of brevity and simplicity, we do not present linear constraints. They are not of interest when considering the result as they are used internally to improve the interval information. Interval constraints are tagged with the actions of syntactic agents.

**Example 41** We give in Fig. 16 the result of occurrence analysis of the ftp-server. This result ensures that no more than three syntactic instances of the syntactic agent **deal**![**data**] can simultaneously occur. So we can conclude that no more than three sessions can be active at the same time. This constraint is proved using the linear constraint which proves that the sum of the number of available ports **port**![] and activated sessions **deal**![**data**] is always equal to three.
**Example 42** We give in Fig. 17 the occurrence analysis result for the token-
ring. This result ensures that only one syntactic instance of the agent *crit*![]
may occur at any time. So only one process can proceed its critical section at
the same time.

**Remark 43** The analysis cannot succeed in proving that the occurrence num-
ber of the syntactic agent **mon**![**left**,**left0**] is less than or equal to 1 without
counting the number of performed transitions. On the other hand, only a linear
number of extra variables are required to prove this property.

9 Complexity and benchmarks

9.1 About the complexity of our analyses

We briefly describe the complexity in the worst case of our analyses in Figs. 18 and 19. We denote by *n* the number of syntactic components in the initial system. The first line denotes the cost to scan all the possible labels of transition steps. The second line denotes the maximum number of stages in one abstract iteration. The third line denotes the cost to perform an abstract transition, it includes both abstract operation cost and information propagation. The worst-case time complexity of an analysis is then the product of those three partial worst-case time complexities.

In the third column of Fig. 18, *m* is a parameter of our analysis which denotes
analysis precision. We have *m* ∈ {1; 2} and in the case when *m* = 1 each tran-
sition label is abstracted by its second component, while the two components
are kept when *m* = 2. In Fig. 19, *i* is also a parameter of our analysis such
that the number of variables is in *O*(*n*<sup>*i*</sup>). It is equal to 0 when no occurrence
analysis is done; it is equal to 1 when only syntactic agents are counted; it is
also equal to 1 when we also count the number of sent messages; it is equal to
2 when we count performed transitions.

To obtain the worst-case time complexity of the product of two analyzes, we
add pair-wise the complexities due to transition label scanning, the maximum
number of iterations, and the cost of an abstract transition and then make
the product of these three complexities. So, for instance, the analysis obtained
as the product between our non-uniform global analysis with *m* = 2 and our
occurrence counting analysis with *i* = 2, has a *O*(n<sup>2</sup> × n<sup>7</sup> × n<sup>10</sup>) worst-case
time cost.
<figure><img src="image_4.png" /><figcaption>Fig. 16. The ftp-server occurrence analysis</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Fig. 17. The token-ring occurrence analysis</figcaption></figure>
<table><caption>Fig. 18. Control flow analysis complexity</caption><thead><tr><th></th><th>0-CFA</th><th>confinement</th><th>non-uniform<br>comp.-wise<br>m &isin; {1; 2}</th><th>non-uniform<br>global<br>m &isin; {1; 2}</th></tr></thead><tbody><tr><th>label scan</th><td>O(n<sup>2</sup>)</td><td>O(n<sup>2</sup>)</td><td>O(n<sup>2</sup>)</td><td>O(n<sup>2</sup>)</td></tr><tr><th>iteration height</th><td>O(n<sup>3</sup>)</td><td>O(n<sup>3</sup>)</td><td>O(n<sup>2 &times; m + 3</sup>)</td><td>O(n<sup>2 &times; m + 3</sup>)</td></tr><tr><th>transition complexity</th><td>O(n<sup>4</sup>)</td><td>O(n<sup>4</sup>)</td><td>O(n<sup>2 &times; m + 4</sup>)</td><td>O(n<sup>3 &times; m + 4</sup>)</td></tr><tr><th>total cost</th><td>O(n<sup>9</sup>)</td><td>O(n<sup>9</sup>)</td><td>O(n<sup>4 &times; m + 9</sup>)</td><td>O(n<sup>5 &times; m + 9</sup>)</td></tr></tbody></table>

<table><caption>Fig. 19. Occurrence counting analysis complexity</caption><thead><tr><th></th><th>occurrence counting analysis<br>i &isin; {0; 1; 2}</th></tr></thead><tbody><tr><th>scan</th><td>O(n<sup>2</sup>)</td></tr><tr><th>iteration height</th><td>O((n<sup>i</sup>)<sup>2</sup>)</td></tr><tr><th>transition complexity</th><td>O((n<sup>i</sup>)<sup>4</sup>)</td></tr><tr><th>total cost</th><td>O(n<sup>6 &times; i + 2</sup>)</td></tr></tbody></table>

<table><caption>Fig. 20. The ftp-server analysis time</caption><thead><tr><th>ftp-server<br>n = 16</th><th>0-CFA</th><th>non-uniform<br>comp.-wise<br>m = 1</th><th>non-uniform<br>comp.-wise<br>m = 2</th></tr></thead><tbody><tr><td>i = 0, |V| = 0</td><td>0.03s</td><td>0.22s</td><td>0.21s</td></tr><tr><td>i = 1, |V| = n</td><td>0.44s</td><td><strong>0.71s</strong></td><td><strong>0.71s</strong></td></tr><tr><td>i = 1, |V| = 2 &times; n</td><td>1.40s</td><td><strong>2.16s</strong></td><td><strong>2.13s</strong></td></tr><tr><td>i = 2, |V| = n<sup>2</sup> + n</td><td>1.42s</td><td><strong>2.17s</strong></td><td><strong>2.15s</strong></td></tr></tbody></table>

## 9.2 Analysis time

We report in Figs. 20 and 21 CPU-time used in analyzing our examples on a PENTIUM III, 500 MHz CPU with 128 MB RAM. We write the time in boldface when the analysis has succeeded in proving all the properties we were interested in.
<table><caption>Fig. 21. The token ring analysis time</caption><thead><tr><th>Token-ring</th><th>0-CFA</th><th>non-uniform<br>comp.-wise</th><th>non-uniform<br>comp.-wise</th></tr></thead><tbody><tr><td>n = 12</td><td></td><td>m = 1</td><td>m = 2</td></tr><tr><td>i = 0, |V| = 0</td><td>0.03s</td><td>0.15s</td><td>0.14s</td></tr><tr><td>i = 1, |V| = n</td><td>0.24s</td><td>0.43s</td><td>0.44s</td></tr><tr><td>i = 1, |V| = 2 × n</td><td>0.68s</td><td><b>0.86s</b></td><td><b>0.88s</b></td></tr><tr><td>i = 2, |V| = n² + n</td><td>0.79s</td><td><b>1.01s</b></td><td><b>1.04s</b></td></tr></tbody></table>

# 10 Conclusion

We have proposed a parametric framework for automatically inferring the properties of mobile systems. We have first introduced a powerful non-standard semantics which explicitly encodes the link between agents and the channels they have opened. This non-standard semantics handles the full π-calculus and allows us to describe the behavior of a system part, abstracting away the behavior of its context. We have proved both the soundness and the completeness of this abstraction. This means that our semantics takes into account the behavior of any context specified in the π-calculus and that each behavior described by our semantics can effectively be obtained by choosing an appropriate context written in the π-calculus.

We have then proposed a generic decidable approximation of this non-standard semantics. As an example, we proposed to focus on the properties which rely on both control flow and agent occurrence number. Our control flow analysis has successfully detected and proved some complex integrity properties: we have proved that in the case of an *ftp*-server used by an unbounded number of clients, the server always returns each query to the correct client and that, in the case of a token ring, each process of the ring can only pass the token to the next or to the first process of the ring. We can also capture information about causality, since our analysis captures comparison between the history of the replications that have led to the creation of agents. The analysis of the agent occurrence number has successfully detected and proved non-exhaustion of resources and mutual exclusion: in the case of the *ftp*-server, the analysis has discovered that the server can only run three simultaneous sessions, while in the case of the token ring, the analysis has proved that only one process of the ring can be in its critical section at a given time.

In this framework, we only capture properties about configurations. We plan to use our analyses to provide partitioning criteria, so that we can capture decidable approximations of system traces. This way we will be able to check
behavioral properties, in which channel instances are distinguished. Because of the approximation, we will only consider the properties such that the set of the traces that satisfies these properties are closed under inclusion. Moreover, our framework can very likely apply to other formalisms as well as to real languages. It may be a great challenge to infer the same kind of properties when agent dynamic creation is also controlled by complex data properties.

## Acknowledgements

We deeply thank anonymous referees for their significant comments on early versions of this paper. We wish also to thank Patrick and Radhia Cousot, and Arnaud Venet, for their insightful comments and discussions. We are also very grateful to Bruno Blanchet, Francesco Logozzo, Antoine Miné, David Monniaux, Xavier Rival, Eben Upton and Yves Verhoeven who helped us in correcting previous versions of this work.

## References

[1] C. Bodei, P. Degano, F. Nielson, and H. Riis Nielson. Control flow analysis for the π-calculus. In *Proc. CONCUR'98*, LNCS. Springer-Verlag, 1998.

[2] C. Bodei, P. Degano, F. Nielson, and H. Riis Nielson. Static analysis of processes for no read-up and no write-down. In *Proc. FoSSaCS'99*, LNCS. Springer-Verlag, 1999.

[3] C. Bodei, P. Degano, F. Nielson, and H. Riis Nielson. Static analysis for the π-calculus with applications to security. *Information and Computation*, 165, 2000.

[4] L. Cardelli, G. Ghelli, and A. D. Gordon. Secrecy and group creation. In *Proc. CONCUR'00*, LNCS. Springer-Verlag, 2000.

[5] C. K. Chiu and J. H. M. Lee. Interval linear constraint solving using the preconditioned interval Gauss-Seidel method. In *Proc. ICLP'95*, Logic Programming. The MIT Press, 1995.

[6] P. Cousot. Semantic foundations of program analysis. In *Program Flow Analysis: Theory and Applications*, chapter 10. Prentice-Hall, Inc., 1981.

[7] P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In *Proc. POPL'77*. ACM Press, 1977.

[8] P. Cousot and R. Cousot. Abstract interpretation frameworks. *Journal of Logic and Computation*, 2(4), 1992.
[9] P. Cousot and R. Cousot. Comparing the Galois connection and widening-narrowing approaches to abstract interpretation. In Proc. PLILP'92, LNCS. Springer-Verlag, 1992.

[10] P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proc. POPL'78. ACM Press, 1978.

[11] N. G. de Bruijn. Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indagationes Mathematicae, 34(5), 1972.

[12] N. Dershowitz and J.-. Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B). Elsevier Science Publishers, 1990.

[13] D. Dolev and A. C. Yao. On the security of public key protocols (extended abstract). In Proc. FOCS'81. IEEE Press, 1981.

[14] J. Feret. Conception de π-sa : un analyseur statique générique pour le π-calcul. Graduate thesis, École Polytechnique, september 1999. Electronically available at http://www.di.ens.fr/~feret/dea/dea.ps.

[15] J. Feret. Confidentiality analysis of mobile systems. In Proc. SAS'00, LNCS. Springer-Verlag, 2000.

[16] J. Feret. Occurrence counting analysis for the π-calculus. In Proc. GETCO'00, volume 39.2 of ENTCS. Elsevier Science Publishers, 2001.

[17] P. Granger. Static analysis of linear congruence equalities among variables of a program. In Proc. TAPSOFT'91, LNCS. Springer-Verlag, 1991.

[18] R. R. Hansen, J. G. Jensen, F. Nielson, and H. Riis Nielson. Abstract interpretation of mobile ambients. In Proc. SAS'99, LNCS. Springer-Verlag, 1999.

[19] M. Hennessy and J. Riely. Resource access control in systems of mobile agents. In Proc. HLCL'98, volume 16.3 of ENTCS. Elsevier Science Publishers, 1998.

[20] A. Igarashi and N. Kobayashi. A generic type system for the π-calculus. In Proc. POPL'01. ACM, 2001.

[21] M. Karr. Affine relationships among variables of a program. Acta Informatica, 1976.

[22] R. Milner. The polyadic π-calculus: a tutorial. In Proceedings of the International Summer School on Logic and Algebra of Specification. Springer-Verlag, 1991.

[23] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes. Information and Computation, 1992.

[24] A. Miné. The octagon abstract domain. In Proc. AST'01 in WCRE'01. IEEE Press, 2001.
[25] F. Nielson and H. Seidl. Control-flow analysis in cubic time. In Proc. ESOP'01, LNCS. Springer-Verlag, 2001.

[26] H. Riis Nielson and F. Nielson. Shape analysis for mobile ambients. In Proc. POPL'00. ACM Press, 2000.

[27] R. J. Parikh. On context-free languages. Journal of the ACM, 13, 1966.

[28] S. K. Rajamani and J. Rehof. A behavioral module system for the π-calculus. In Proc. SAS'01, LNCS. Springer-Verlag, 2001.

[29] D. N. Turner. The Polymorphic π-Calculus: Theory and Implementation. PhD thesis, Edinburgh University, 1995.

[30] A. Venet. Abstract interpretation of the π-calculus. In Proc. LOMAPS'97, LNCS. Springer-Verlag, 1997.

[31] A. Venet. Automatic determination of communication topologies in mobile systems. In Proc. SAS'98, LNCS. Springer-Verlag, 1998.

A Correspondence between the standard and the naive semantics

In this section we give the proof of Thm. 8, which formalizes the relation
between the standard and the naive semantics.

**Theorem 8** We have $\mathcal{S} = \Pi(\mathcal{C}_0^n(\mathcal{S}))$, and for any non-standard configurations $C$ and for any word $u \in (\mathcal{L}^2 \cup \{\oplus; \ominus\})^*$ such that $\mathcal{C}_0^n(\mathcal{S}) \xrightarrow{u} \mathcal{n}^* C$, we have:

$$
(1) C \xrightarrow{\epsilon} \mathcal{n} C' \implies \Pi(C) \equiv \Pi(C');
$$

$$
(2) \forall \lambda \in \mathcal{L}^2 \cup \{\oplus\}, C \xrightarrow{\lambda} \mathcal{n} C' \implies \Pi(C) \xrightarrow{\lambda} \Pi(C');
$$

$$
(3) \forall \lambda \in \mathcal{L}^2 \cup \{\oplus\}, \Pi(C) \xrightarrow{\lambda} P \implies \exists D, \exists E, \begin{cases} C \xrightarrow{\varepsilon} \mathcal{n}^* D \xrightarrow{\lambda} \mathcal{n} E \\ \Pi(E) \equiv P. \end{cases}
$$

**PROOF.** We have $\mathcal{C}_0^n(\mathcal{S}) = (\mathcal{S}, \varepsilon, \emptyset)$, then $\Pi(\mathcal{C}_0^n(\mathcal{S})) = \mathcal{S}$. Let $C$ be a non-standard configuration and $u$ a word in $(\mathcal{L}^2 \cup \{\varepsilon; \oplus\})^*$ such that $\mathcal{C}_0^n(\mathcal{S}) \xrightarrow{u} \mathcal{n}^* C$,

(1) let $C'$ be a non-standard configuration such that $C \xrightarrow{\epsilon} \mathcal{n} C'$, we want to
prove that $\Pi(C) \equiv \Pi(C')$ by case analysis on $C \xrightarrow{\epsilon} \mathcal{n} C'$:

(a) in the case that $C \xrightarrow{\epsilon} \mathcal{n} C'$ consists in decomposing a thread into two concurrent threads, we have $\Pi(C) \equiv \Pi(C')$ thanks to the associativity and commutativity congruence rules;

(b) in the case that $C \xrightarrow{\epsilon} \mathcal{n} C'$ consists in removing a thread the syntactic component of which is the empty agent, we have $\Pi(C) \equiv \Pi(C')$ thanks to the "end of an agent" congruence rule;
(c) in the case that $C \xrightarrow{\varepsilon} {}_n C'$ consists in opening a channel, we have $\Pi(C) \equiv \Pi(C')$ thanks to the extrusion rule, the swapping rule, and the consistency of the marker allocation scheme (Cf. Prop. 4).

(2) let $C'$ be a non-standard configuration such that $C \xrightarrow{\lambda} {}_n C'$, we have $\Pi(C) \xrightarrow{\lambda} \Pi(C')$: in the case that $C$ only contains the threads involved in the non-standard computation step, the property is true by definition of the two relations and thanks to the fact that a standard computation step can be performed inside name restriction; then we use the fact that a standard computation step can be performed both within parallel composition and within name restriction to prove it in the general case.

(3) let $P$ be a standard configuration such that $\Pi(C) \xrightarrow{\lambda} P$. The binary relation $\xrightarrow{\varepsilon} {}_n$ is nœtherian and locally confluent. So, following [12], we can take a non-standard configuration $D$ such that $C \xrightarrow{\varepsilon} {}_n^* D$ and such that for any configuration $E, D \xrightarrow{\varepsilon} {}_n E$. In accordance with Thm. 8.(1), we have $\Pi(C) \equiv \Pi(D)$, then since $\xrightarrow{\lambda}$ is compatible with $\equiv$, we get that $\Pi(D) \xrightarrow{\lambda} P$. Besides, we can deduce from the fact that $D$ cannot be reduced by a computation step labelled with $\varepsilon$, that the syntactic component of every thread of $D$ is either of the form $P \oplus Q$ or of the form $aP$. So the computation step $\Pi(D) \xrightarrow{\lambda} P$ can be lifted in the non-standard semantics, so that we can choose a non-standard configuration $E$ such that $D \xrightarrow{\lambda} {}_n E$ and $\Pi(E) \equiv P$. $\square$

## B Correspondence between the standard and the intermediate semantics

In this section we give the proof of Thm. 11, which formalizes the relation between the standard and the intermediate semantics.

**Proposition 9** For any non-standard configuration $C$, we have $C \Downarrow \bigcup_{t \in C} \beta^i(t)$.

**PROOF.** Since the relation $\beta^i$ separately acts on each thread, it is enough to prove the property in the case that $C$ is a singleton $\{(P, id, E)\}$. This is done by induction on the syntax of $P$:

* in the case that $P = 0$,
we have $\{(0, id, E)\} \xrightarrow{\varepsilon} {}_n \emptyset$ and $\beta^i(0, id, E) = \emptyset$,
so $\{(0, id, E)\} \Downarrow \beta^i(0, id, E)$;

* in the case that $P = (\nu n)Q$, we have $\{(P, id, E)\} \xrightarrow{\varepsilon} {}_n \{(Q, id, E[n \mapsto (n, id)]]\}$,
and by induction $\{(Q, id, E[n \mapsto (n, id)]]\} \Downarrow \beta^i(Q, id, E[n \mapsto (n, id)]]$),
since $\beta^i(P, id, E) = \beta^i(Q, id, E[n \mapsto (n, id)])$,
we obtain $\{(P, id, E)\} \Downarrow \beta^i(P, id, E);$

* in the case that $P = (P_1 | P_2)$,
we have $\{(P_1 | P_2, id, E)\} \xrightarrow{\varepsilon} {}_n\{(P_1, id, E_{|fn(P_1)}); (P_2, id, E_{|fn(P_2)})\}$,
and by induction $\forall i \in \{1; 2\}$, $\{(P_i, id, E_{|fn(P_i)})\} \Downarrow \beta^i(P_i, id, E_{|fn(P_i)})$,
since $^9 \beta^i(P_1 | P_2, id, E) = \beta^i(P_1, id, E_{|fn(P_1)} \cup \beta^i(P_2, id, E_{|fn(P_2)})$,
we obtain $\{(P_1 | P_2, id, E)\} \Downarrow \beta^i(P_1 | P_2, id, E);$

* otherwise we have $\beta^i(P, id, E) = \{(P, id, E_{|fn(P)})\}$,
and $\{(P, id, E_{|fn(P)})\} \Downarrow \{(P, id, E_{|fn(P)})\}$,
so $\{(P, id, E)\} \Downarrow \beta^i(P, id, E).$ $\square$

**Theorem 11** We have $\mathcal{S} \equiv \Pi(C_0^i(\mathcal{S}))$, and for all non-standard configurations $C$ and for all word $u \in (\mathcal{L}^2 \cup \{\varepsilon; \oplus\})^*$ such that $C_0^i(\mathcal{S}) \xrightarrow{u} {}_i^*C$, we have:

$$
(1) \quad \forall \lambda \in \mathcal{L}^2 \cup \{\oplus\}, \quad C \xrightarrow{\lambda} {}_i C' \implies \Pi(C) \xrightarrow{\lambda} \Pi(C');
$$

$$
(2) \quad \forall \lambda \in \mathcal{L}^2 \cup \{\oplus\}, \quad \Pi(C) \xrightarrow{\lambda} P \implies \exists D, \begin{cases} C \xrightarrow{\lambda} {}_i D \\ \Pi(D) \equiv P. \end{cases}
$$

**PROOF.** The proof of these properties mainly relies on Thm. 8 and the fact that $\xrightarrow{\lambda} {}_i$ is defined as the composition of $\xrightarrow{\lambda} {}_n$ and $\Downarrow$: in accordance with Thm. 8, we know that $\mathcal{S} = \Pi(C_0^n(\mathcal{S}))$, then by definition of $C_0^i(\mathcal{S})$, we have $C_0^n(\mathcal{S}) \xrightarrow{\varepsilon} {}_n^* C_0^i(\mathcal{S})$, and so we can deduce from Thm. 8.(1) that $\mathcal{S} \equiv \Pi(C_0^i(\mathcal{S}))$. Then let us take a non-standard configuration $C$ and word $u \in (\mathcal{L}^2 \cup \{\varepsilon; \oplus\})^*$ such that $C_0^i(\mathcal{S}) \xrightarrow{u} {}_i^* C$,

(1) let $C'$ be a non-standard configuration such that $C \xrightarrow{\lambda} {}_i C'$, there exists another non-standard configuration $D$ such that $C \xrightarrow{\lambda} {}_n D \xrightarrow{\varepsilon} {}_n^* C'$, we obtain from Thm. 8.(2) that $\Pi(C) \xrightarrow{\lambda} \Pi(D)$ and from Thm. 8.(1) that $\Pi(D) \equiv \Pi(C')$, so $\Pi(C) \xrightarrow{\lambda} \Pi(C')$;

(2) let $P$ be a standard configuration such that $\Pi(C) \xrightarrow{\lambda} P$, following Thm. 8.(3), there exists two non-standard configurations $D$ and $E$, such that $C \xrightarrow{\varepsilon} {}_n^* D$, $D \xrightarrow{\lambda} {}_n E$ and $\Pi(E) \equiv P$, moreover, since $C_0^i(\mathcal{S}) \xrightarrow{u} {}_i^* C$, we know that for any non-standard configuration $D'$, we have $C \not\xrightarrow{\varepsilon} {}_n D'$, this means that $D = C$, so we have $C \xrightarrow{\lambda} {}_n E$ and $\Pi(E) \equiv P$, then we introduce the non-standard configuration $F$ such that $E \Downarrow F$, we know from Thm. 8.(1) that $\Pi(E) \equiv \Pi(F)$, and by definition of $\xrightarrow{\lambda} {}_i$ that $C \xrightarrow{\lambda} {}_i F$, so we can conclude that $P \equiv \Pi(F)$ and $C \xrightarrow{\lambda} {}_i F$. $\square$

<footnote n="9">⁹ We use the property that $\beta^i(R, id, E) = \beta^i(R, id, E_{|fn(R)})$ which can be easily proved for all agents $R$ by induction on the syntax of $R$.</footnote>
C Correspondence between the standard and the efficient semantics

In this section we give the proof of Thm. 13, which formalizes the relation between the standard and the efficient semantics.

**Proposition 12** For any non standard configuration C, we have:

$$ \{b | C \implies b\} = \{\bigcup Cont_t | \forall t \in C, Cont_t \in \beta(t)\}. $$

**PROOF.** Since the $\beta$ relation separately acts on each thread, it is enough to prove the property in the case that C is a singleton $\{(P, id, E)\}$. This is done by induction on the syntax of P:

* in the case that $P = 0$, only the garbage collection rule applies to the thread $(P, id, E)$ and no rule applies on the empty set, so we conclude that $\{b | \{(0, id, E)\} \implies b\} = \{\emptyset\} = \beta(0, id, E)$;

* in the case that $P = (\nu n)Q$, only the name restriction rule can apply: we have $\{(P, id, E)\} \xrightarrow{\varepsilon} {}_n\{(Q, id, E[n \mapsto (n, id)]\}$, $\{b | \{Q, id, E[n \mapsto (n, id)]\} \implies b\} = \beta(Q, id, E[n \mapsto (n, id)])$ (by the induction hypothesis), and $\beta(P, id, E) = \beta(Q, id, E[n \mapsto (n, id)])$, so we obtain $\{b | \{(P, id, E)\} \implies b\} = \beta(P, id, E)$;

* in the case that $P = (P_1 | P_2)$, only the rule which decomposes the thread can apply: we have $\{(P_1 | P_2, id, E)\} \xrightarrow{\varepsilon} {}_n\{(P_1, id, E_{|fn(P_1)}); (P_2, id, E_{|fn(P_2)})\}$, so, since $\dashrightarrow$ separately acts on each thread, we obtain $\{b | \{(P, id, E)\} \implies b\} = \{b_1 \cup b_2 | \forall i \in \{1; 2\}, \{(P_i, id, E)\} \implies b_i\}$; moreover by induction we know that for $i$ in the set $\{1; 2\}$, we have $\{b_i | \{(P_i, id, E_{|fn(P_i)})\} \implies b\} = \beta(P_i, id, E_{|fn(P_i)})$, then by definition of $\beta(P_1 | P_2, id, E)$, we obtain$^{10}$ $\{b | \{(P_1 | P_2, id, E)\} \implies b\} = \beta(P_1 | P_2, id, E)$;

* in the case that $P = (P_1 \oplus P_2)$, only the two choice rules can apply: we have either $\{(P_1 \oplus P_2, id, E)\} \xrightarrow{\oplus} {}_n\{(P_1, id, E_{|fn(P_1)})\}$ or $\{(P_1 \oplus P_2, id, E)\} \xrightarrow{\oplus} {}_n\{(P_2, id, E_{|fn(P_2)})\}$, so $\{b | \{(P_1 \oplus P_2, id, E)\} \implies b\} = \cup_{i \in \{1; 2\}} \{b | \{(P_i, id, E)\} \implies b\}$; moreover by induction we know that for $i$ in the set $\{1; 2\}$, we have that $\{b_i | \{(P_i, id, E_{|fn(P_i)})\} \implies b\} = \beta(P_i, id, E_{|fn(P_i)})$, so since$^{10}$ $\beta(P_1 \oplus P_2, id, E) = \beta(P_1, id, E_{|fn(P_1)}) \cup \beta(P_2, id, E_{|fn(P_2)})$, we obtain $\{b | \{(P_1 \oplus P_2, id, E)\} \implies b\} = \beta(P_1 \oplus P_2, id, E)$;

* otherwise we have $\beta(P, id, E) = \{(\{P, id, E_{|fn(P)}\})\}$, and $\forall b, \{(P, id, E_{fn(P)})\} \dashrightarrow b$, so $\{b | \{(P, id, E)\} \implies b\} = \beta(P, id, E)$.

**Theorem 13** For any initial non-standard configuration $C_0 \in C_0^e(S)$, there

<footnote>$^{10}$ We use the property that $\beta(R, id, E) = \beta(R, id, E_{|fn(R)})$ which can be easily proved for all agents R by induction on the syntax of R.</footnote>
exists $k \in \mathbb{N}$ such that $S \xrightarrow{\oplus^k} \Pi(C_0)$ and for all non-standard configurations $C$ and for all word $u \in (\mathcal{L}^2)^*$ such that $C_0 \xrightarrow{u}^*_e C$, we have:

$$ (1) \quad \forall \lambda \in \mathcal{L}^2, C \xrightarrow{\lambda} {}_e C' \implies \exists k \in \mathbb{N}, \exists P, \Pi(C) \xrightarrow{\lambda} P \xrightarrow{\oplus^k} \Pi(C'); $$

$$ (2) \quad \forall \lambda \in \mathcal{L}^2, \Pi(C) \xrightarrow{\lambda} P \implies \exists D, \left\{ \begin{array}{l} C \xrightarrow{\lambda} {}_e D \\ \text{and} \\ \text{and } \begin{cases} \exists k > 0, P \xrightarrow{\oplus^k} \Pi(D) \\ \text{or } P \equiv \Pi(D). \end{cases} \end{array} \right. $$

**PROOF.** Let $C_0 \in \mathcal{C}_0^e(S)$ be an initial configuration, since $\mathcal{C}_0^e(S) = \beta(S, \varepsilon, \emptyset)$, we obtain that $\mathcal{C}_0^n(S) \dashrightarrow {}^* C_0$, then by definition of $\dashrightarrow$ and thanks to Thm. 8.(1) and Thm. 8.(2), there exists $k \in \mathbb{N}$ such that $\Pi(\mathcal{C}_0^n(S)) \xrightarrow{\oplus^k} {}^* \Pi(C_0)$, since $S = \Pi(\mathcal{C}_0^n(S))$ we get that $S \xrightarrow{\oplus^k} {}^* \Pi(C_0)$. Then let us take a non-standard configuration $C$ and a word $u \in (\mathcal{L}^2)^*$ such that $C_0 \xrightarrow{u} {}_e^* C$,

(1) let $C'$ be a non-standard configuration such that $C \xrightarrow{\lambda} {}_e C'$, by definition of $\xrightarrow{\lambda} {}_e$, there exists another non-standard configuration $D$ such that we have $C \xrightarrow{\lambda} {}_n D \dashrightarrow {}^* C'$; moreover, we obtain from Thm. 8.(2) that $\Pi(C) \xrightarrow{\lambda} \Pi(D)$ and we deduce from Thm. 8.(1) and Thm. 8.(2) that there exists $k \in \mathbb{N}$, such that $\Pi(D) \xrightarrow{\oplus^k} {}^* \Pi(C')$;

(2) let $P$ be a standard configuration such that $\Pi(C) \xrightarrow{\lambda} P$, following Thm. 8.(3), there exist two non-standard configurations $D$ and $E$ which satisfy $C \xrightarrow{\varepsilon} {}^*_n D$, $D \xrightarrow{\lambda} {}_n E$ and $\Pi(E) \equiv P$; since $\mathcal{C}_0^i(S) \xrightarrow{u} {}_e^* C$, we know that for any non-standard configuration $D'$, we have $C \dashrightarrow D'$, this means that $D = C$ and $\lambda \neq \oplus$, so we have $C \xrightarrow{\lambda} {}_n E$ and $\Pi(E) \equiv P$, then we introduce the non-standard configuration $F$ such that $E \implies F$, by definition of $\xrightarrow{\lambda} {}_e$, we have $C \xrightarrow{\lambda} {}_e F$; moreover we have either $E \xrightarrow{\varepsilon} {}^*_n F$ and thanks to Thm. 8.(1) $\Pi(E) \equiv \Pi(F)$, or $E \dashrightarrow {}^* E'$ $\xrightarrow{\oplus} {}_n E'' \dashrightarrow {}^* F$, and thanks to Thm. 8.(1) and Thm. 8.(2), there exists $k > 0$ such that $\Pi(E) \xrightarrow{\oplus^+} {}^* \Pi(F)$. $\square$

## D Correspondence between the semantics of closed and open systems

In this section we give the proof of Thms. 22 and 23, which formalize the relation between the semantics of closed and open systems.

We first recall Def. 21:

**Definition 21** Computation sequence projection is then defined as follows:
Let $\tau = C_0 \xrightarrow{\lambda_1} e \dots \xrightarrow{\lambda_n} e C_n$ be a non-standard computation sequence, with $C_0 \in C_0^e(S)$. We define the projection of $\tau$, $\Pi_\tau(S_I, \Phi_M, \Phi_N)(\tau)$ as the non-standard computation sequence:

$$ (A_0, U_0, F_0) \xrightarrow{\Pi_\lambda(\lambda_{a_1})} \dots \xrightarrow{\Pi_\lambda(\lambda_{a_p})} (A_p, U_p, F_p) $$

of the open system $S_I$, where

* $a_1, \dots, a_p$ is the strictly ascending sequence of the elements of the set $\{i \in \llbracket 1; n \rrbracket \mid \lambda_i \in \mathcal{L}^2 \setminus (\mathcal{L} \setminus \mathcal{L}_I)^2\}$;

* the initial configuration $(A_0, U_0, F_0)$ is the following triple:

$$ (\Pi_{C}^{\Phi_{M}, \Phi_{N}}(C_0), e n, \{t_n \mid n \in \mathbb{N}\}); $$

* for $k \in \llbracket 1; p \rrbracket$, the configuration $(A_k, U_k, F_k)$ is then defined as follows:

$$ \cdot A_k = \Pi_{C}^{\Phi_{M}, \Phi_{N}}(C_{a_k}), $$

$$ \cdot U_k = \begin{cases} U_{k-1} & \text{if } \mathrm{fst}(\lambda_{a_k}) \in \mathcal{L}_I, \\ U_{k-1} \cup \{\Pi_{\mathcal{N}}^{\Phi_M, \Phi_N}(E(x_r)) \mid r \in \llbracket 1; n \rrbracket\} & \text{otherwise,} \end{cases} \text{ where, in the last case, } t = (x_1^j[x_1, \dots, x_n]P, id, E) \text{ denotes the unique thread in } C_{a_{k-1}} \setminus C_{a_k} \text{ which matches this notation;} $$

$$ \cdot F_k = \begin{cases} F_{k-1} & \text{if } \mathrm{snd}(\lambda_{a_k}) \in \mathcal{L}_I \text{ or if } \xrightarrow{\lambda_{a_k}}_e \text{ is not a resource replication,} \\ F_{k-1} \setminus \{\Phi_M(\mathrm{snd}(\lambda_{a_k}), id) \mid (P, id, E) \in C_{a_{k-1}} \setminus C_{a_k}\} & \text{otherwise.} \end{cases} $$

Then we introduce some lemma to help proving the correspondence.

The following lemma shows that the extraction function $\beta$ and the configuration projection commute:

**Lemma 44** Let $(P, id, E)$ be a thread such that $P$ is a sub-term of $S_I$, then we have:

$$ \beta(P, \Pi_{\mathcal{M}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(id), [x \mapsto \Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(E(x))]) = \Pi_{C}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(\beta(P, id, E)). $$

**PROOF.** This lemma can easily be proved by induction on the syntax of $P$. We use the fact that each sub-term of a sub-term of $S_I$ is also a sub-term of $S_I$. $\square$

The following lemma establishes the fact that communications between two threads of the context leave the threads of the system $S_I$ unchanged:

**Lemma 45** Let $\tau = C_0 \xrightarrow{\lambda_1} e \dots \xrightarrow{\lambda_n} e C_n$ be a non-standard computation sequence, with $C_0 \in C_0^e(S)$; we denote by $(A_0, U_0, F_0) \dots (A_p, U_p, F_p)$ the computation sequence $\Pi_\tau(S_I, \Phi_M, \Phi_N)(\tau)$, then we have $\Pi_{C}^{\Phi_M, \Phi_N}(C_n) = A_p$.
**PROOF.** We prove Lem. 45 by induction over the integer $n - a_p$.

(1) in the case that $n = a_p$, we have $\Pi_C^{\Phi_M, \Phi_N}(C_n) = A_p$ by Def. 21;

(2) we now suppose that there exists $m_0 \in \mathbb{N}$ such that Lem. 45 is satisfied provided that $n - a_p < m_0$, we now prove it in the case that $n - a_p = m_0$: we know from the induction hypothesis that $\Pi_C^{\Phi_M, \Phi_N}(C_{n-1}) = A_p$, then we have $\lambda_n \in (\mathcal{L} \setminus \mathcal{L}_I)^2$, so we can conclude that both the set $C_{n-1} \setminus C_n$ and the set $C_n \setminus C_{n-1}$ only contain threads the label of which is in $\mathcal{L} \setminus \mathcal{L}_I$, thus with respect with Def. 21, we obtain that $\Pi_C^{\Phi_M, \Phi_N}(C_n) = \Pi_C^{\Phi_M, \Phi_N}(C_{n-1})$, since $\Pi_C^{\Phi_M, \Phi_N}(C_{n-1}) = A_p$, we conclude that $\Pi_C^{\Phi_M, \Phi_N}(C_n) = A_p$. $\square$

The following lemma establishes some soundness conditions:

**Lemma 46** Let $\tau = C_0 \xrightarrow{\lambda_1} e \dots \xrightarrow{\lambda_n} e$ $C_n$ be a non-standard computation sequence, with $C_0 \in C_0^e(S)$. We consider the following computation sequence:

$$ \Pi_{\tau}(S_I, \Phi_M, \Phi_N)(\tau) = (A_0, U_0, F_0)...(A_{a_p}, U_{a_p}, F_{a_p}). $$

Then, $\forall (P, id, E) \in C_n$ with $lab(P) \notin \mathcal{L}_I$:

(1) $\forall x \in fn(P)$, we have $\Phi_N(E(x)) \in U_p$;

(2) $\Phi_M(lab(P), id) \in F_p$.

**PROOF.** These two properties are easily proved by induction on $n$.

(1) (a) in the case that $n = 0$, we have $p = 0$; let $(P, id, E)$ be a thread in $C_0$ with $lab(P) \notin \mathcal{L}_I$; we have $C_0 \in C_0^e(S)$, let $x$ be a free name in $P$; since $lab(P) \notin \mathcal{L}_I$, we have $x \notin \mathcal{N}_I$; then $E(x) = \Pi_{\mathcal{N}}^{\Phi_M, \Phi_N}(x, \varepsilon) = \Phi_N(x, \varepsilon) \in en = U_0$;

(b) we suppose that there exists $n_0 \in \mathbb{N}$ such that Prop. 46.(1) is satisfied for any $n$ smaller than $n_0$. We now prove this property for $n = n_0+1$: let $(P, id, E)$ in $C_{n_0+1}$ with $lab(P) \notin \mathcal{L}_I$, and $x$ be a free name in $P$; we denote $(y, id_y) = E(x)$;

* in the case that there exists $j$ smaller than $n_0$ such that $(P, id, E)$ in $C_j$: by the induction hypothesis, there exists $o$ smaller than $p$ such that $\Phi_N(E(x)) \in U_o \subseteq U_p$;

* in the case that $y \notin \mathcal{N}_I$, we have $\Phi_N(E(x)) \in en = U_0 \subseteq U_p$;

* otherwise we necessarily have $\lambda_{n_0+1} \in ((\mathcal{L} \setminus \mathcal{L}_I) \times \mathcal{L}_I)$, and there exists a thread $t = (z!^j[z_1, ..., z_n]P, id_t, E_t) \in C_{n_0} \setminus C_{n_0+1}$ such that $E(x) \in \{E_t(z_l) | l \in [1; n]\}$, so by definition of $U_p$, we get that $\Phi_N(E(x)) \in U_p$.

(2) (a) in the case that $n = 0$, we have $p = 0$ and $F_p = \{t_n | n \in \mathbb{N}\}$, so $\Phi_M(\{(lab(P), id) | (P, id, E) \in C_0, lab(P) \notin \mathcal{L}_I\}) \subseteq F_p$;
(b) we suppose that there exists $n_0 \in \mathbb{N}$ such that Prop. 46.(2) is satisfied for any $n$ smaller than $n_0$. We now prove this property for $n = n_0+1$: let $(P, id, E)$ in $C_{n_0+1}$ with $lab(P) \notin \mathcal{L}_I$;

* in the case that $(P, id, E) \in C_{n_0}$ and $\lambda_{n_0+1} \in (\mathcal{L} \setminus \mathcal{L}_I)^2$: we have $\Phi_{\mathcal{M}}(lab(P), id) \in F_p$, by the induction hypothesis;

* in the case that $(P, id, E) \in C_{n_0}$ and $\lambda_{n_0+1} \notin (\mathcal{L} \setminus \mathcal{L}_I)^2$: we know by the induction hypothesis that $\Phi_{\mathcal{M}}(lab(P), id) \in F_{p-1}$, then the marker $\Phi_{\mathcal{M}}(lab(P), id)$ is also in $F_p$, otherwise we would have $(P, id, E) \in C_{n_0} \setminus C_{n_0+1}$, which is absurd;

* in the case that $(P, id, E) \notin C_{n_0}$, we have $\Phi_{\mathcal{M}}(lab(P), id) \in F_p$, otherwise there would exist an integer $i < p$ such that $\Phi_{\mathcal{M}}(lab(P), id) \in F_i \setminus F_{i+1}$, and so there would exist an integer $j < n_0 + 1$ such that $(P, id, E) \in C_j \setminus C_{j+1}$ which is in contradiction with the fact that $(P, id, E) \in C_{n_0+1}$ thanks to Prop. 4.

So in any case, we have $\Phi_{\mathcal{M}}(lab(P), id) \in F_p$. $\square$

**Theorem 22 (Soundness)** Let $\tau = C_0...C_n$ be a non-standard computation sequence of the following closed system:

$$ (\nu c_1)...(\nu c_k)(\mathcal{S}_I(c_{i_1}, ..., c_{i_n}) | \mathcal{S}_c(c_{j_1}, ...c_{j_l})), $$

with $C_0 \in \mathcal{C}_0^o(\mathcal{S})$. Then $\Pi_{\tau}(\mathcal{S}_I, \Phi_{\mathcal{M}}, \Phi_{\mathcal{N}})(\tau) = (A_0, U_0, F_0)...(A_p, U_p, F_p)$ is a non-standard computation sequence of the open system $\mathcal{S}_I$ and $(A_0, U_0, F_0) \in \mathcal{C}_0^o(\mathcal{S})$.

**PROOF.** Soundness is ensured by construction: we prove Thm. 22 by induction on the length of the computation sequences:

(1) We first prove that $(A_0, U_0, F_0) \in \mathcal{C}_0^o(\mathcal{S})$: we have $C_0 \in \mathcal{C}_0^o(\mathcal{S})$; so $C_0 \in \beta(\mathcal{S}, \varepsilon, \emptyset)$; so by definition of $\beta$, we have $C_0 \in \{A \cup B \mid A \in \beta(\mathcal{S}_I, \varepsilon, [c_{i_k} \mapsto (c_{i_k}, \varepsilon)]), B \in \beta(\mathcal{S}_c, \varepsilon, [c_{j_k} \mapsto (c_{j_k}, \varepsilon)])\}$; then we decompose $C_0$ into $A \cup B$ with $A \in \beta(\mathcal{S}_I, \varepsilon, [c_{i_k} \mapsto (c_{i_k}, \varepsilon)])$ and with $B \in \beta(\mathcal{S}_c, \varepsilon, [c_{j_k} \mapsto (c_{j_k}, \varepsilon)])$. Moreover, we have $A_0 = \Pi_{\mathcal{C}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(C_0) = \Pi_{\mathcal{C}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(A) \cup \Pi_{\mathcal{C}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(B)$; since $\Pi_{\mathcal{C}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(B) = \emptyset$, we have $A_0 = \Pi_{\mathcal{C}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(A)$. Thanks to Lem. 44, since $A \in \beta(\mathcal{S}_I, \varepsilon, [c_{i_k} \mapsto (c_{i_k}, \varepsilon)])$, we obtain $A_0 \in \beta(\mathcal{S}_I, \Pi_{\mathcal{M}}^{\Phi_{\mathcal{M}}}(id), [c_{i_k} \mapsto \Phi_{\mathcal{N}}(c_{i_k}, \varepsilon)])$; so, since $\Phi_{\mathcal{N}} : (\mathcal{N} \times \mathcal{M} \to en)$, we obtain the fact that $A_0 \in \cup\{\beta(\mathcal{S}_I, \varepsilon, E) \mid E \in fn(P) \to en\}$; then since $U_0 = en$ and $F_0 = \{t_n \mid n \in \mathbb{N}\}$, we obtain, by definition of $\mathcal{C}_0^o$, that $(A_0, U_0, F_0) \in \mathcal{C}_0^o(\mathcal{S})$.

(2) We now assume that Thm. 22 is satisfied for any non-standard computation sequence $\tau$ containing at most $n$ computation steps, and we prove that it is also satisfied for any non-standard computation sequence $\tau$ of containing $n+1$ computation steps: let $\tau = C_0...C_n \xrightarrow{\lambda} e C_{n+1}$ be a non-standard computation sequence of length $n+1$; by the induction
hypothesis $\Pi_{\tau}(S_I, \Phi_M, \Phi_N)(C_0...C_n)$ is a non-standard computation sequence of the open system $S_I$, which we can denote:

$$ (A_0, U_0, F_0)...(A_{a_p}, U_{a_p}, F_{a_p}) $$

then we discuss several cases depending of $\lambda = (i, j)$:

(a) in the case that $\lambda \in (\mathcal{L} \setminus \mathcal{L}_I)^2$: by definition of $\Pi_{\tau}(S_I, \Phi_M, \Phi_N)$, $\Pi_{\tau}(S_I, \Phi_M, \Phi_N)(\tau) = \Pi_{\tau}(S_I, \Phi_M, \Phi_N)((C_0, U_0, F_0)...(C_n, U_n, F_n))$; so $\Pi_{\tau}(S_I, \Phi_M, \Phi_N)(\tau)$ is a non-standard computation sequence of the open system $S_I$;

(b) in the case that $\lambda \in \mathcal{L}_I^2$ and $\xrightarrow{\lambda}$ is a communication rule: there exist two threads $t_? = (y?^i[y]P, id?, E_?)$ and $t_! = (x!^j[x], id!, E_!)$ in $C_n$ which satisfy that $E_?(y) = E_!(x)$ and $\lambda = (i, j)$, and two continuations $Cont_? \in \beta(P, id?, E_?[y_i \mapsto x_i])$ and $Cont_! \in \beta(Q, id!, E_!)$ such that $C_{n+1} = (C_n \setminus \{t_?; t_!\}) \cup Cont_? \cup Cont_!$; we have:

$$ \left\{ \begin{array}{l} (\Pi_{\lambda}(t_?), \Pi_{\lambda}(t_!)) \in (A_p)^2 \text{ (thanks to Lem. 45 and since } (i, j) \in \mathcal{L}_I^2), \\ \Pi_{\lambda}^{\Phi_M, \Phi_N}(E_?(y)) = \Pi_{\lambda}^{\Phi_M, \Phi_N}(E_!(x)) \text{ (since } E_?(y) = E_!(x)), \\ \Pi_{t_?}^{\Phi_M, \Phi_N}(Cont_?) \in \beta(P, \Pi_{\lambda}^{\Phi_M}(id_?), E_?'_?) \text{ (thanks to Lem. 44),} \\ \text{where } E_?'_? = [x \mapsto \Pi_{\lambda}^{\Phi_M, \Phi_N}(E_?[y_k \mapsto E_!(x_k)](x))] \\ \Pi_{t_?}^{\Phi_M, \Phi_N}(Cont_?) \in \beta(Q, \Pi_{\lambda}^{\Phi_M}(id_!), [x \mapsto \Pi_{\lambda}^{\Phi_M, \Phi_N}(E_!(x))]), \\ \text{(thanks to Lem. 44)} \end{array} \right. $$

$$ \text{so } (A_p, U_p, F_p) \xrightarrow{\lambda} (A_p \setminus \{\Pi_t^{\Phi_M, \Phi_N}(t_?); \Pi_t^{\Phi_M, \Phi_N}(t_!}\}) \cup \Pi_t^{\Phi_M, \Phi_N}(Cont_?) \cup \Pi_t^{\Phi_M, \Phi_N}(Cont_!), U_p, F_p); \text{ then since } \Pi_{\lambda}(\lambda) = \lambda, \text{ we can conclude that} \\ (A_p, U_p, F_p) \xrightarrow{\Pi_{\lambda}(\lambda)} (\Pi_C^{\Phi_M, \Phi_N}(C_{n+1}), U_p, F_p); $$

(c) in the case that $\lambda \in \mathcal{L}_I^2$ and $\xrightarrow{\lambda}$ is a replication rule: there exist two threads $t_? = (*y?^i[y]P, id?, E_?)$ and $t_! = (x!^j[x], id!, E_!)$ in $C_n$ which satisfy that $E_?(y) = E_!(x)$ and $\lambda = (i, j)$, and two continuations $Cont_? \in \beta(P, N((i, j), id?, id_!), E_?[y_i \mapsto x_i])$ and $Cont_! \in \beta(Q, id!, E_!)$ such that $C_{n+1} = (C_n \setminus \{t_?\}) \cup Cont_? \cup Cont_!$; since $(i, j) \in \mathcal{L}_I^2$, we have $\Pi_M^{\Phi_M}(N((i, j), id?, id_!)) = N((i, j), \Pi_M^{\Phi_M}(id_?), \Pi_M^{\Phi_M}(id_!))$; then:

$$ \left\{ \begin{array}{l} (\Pi_{\lambda}(t_?), \Pi_{\lambda}(t_!)) \in (A_p)^2 \text{ (thanks to Lem. 45 and since } (i, j) \in \mathcal{L}_I^2), \\ \Pi_{\lambda}^{\Phi_M, \Phi_N}(E_?(y)) = \Pi_{\lambda}^{\Phi_M, \Phi_N}(E_!(x)) \text{ (since } E_?(y) = E_!(x)), \\ \Pi_{t_?}^{\Phi_M, \Phi_N}(Cont_?) \in \beta(P, id_*, E_*) \text{ (thanks to Lem. 44),} \\ \text{where } id_* = N((i, j), \Pi_M^{\Phi_M}(id_?), \Pi_M^{\Phi_M}(id_!)) \\ \text{and } E_* = [x \mapsto \Pi_{\lambda}^{\Phi_M, \Phi_N}(E_?[y_k \mapsto E_!(x_k)](x))], \\ \Pi_{t_?}^{\Phi_M, \Phi_N}(Cont_?) \in \beta(Q, \Pi_M^{\Phi_M}(id_!), [x \mapsto \Pi_{\lambda}^{\Phi_M, \Phi_N}(E_!(x))]) \\ \text{(thanks to Lem. 44)} \end{array} \right. $$
so we have $(A_p, U_p, F_p) \stackrel{\lambda}{\mapsto} (A_p \setminus \{\Pi_t^{\Phi_M, \Phi_N}(t_!))\} \cup \Pi_t^{\Phi_M, \Phi_N}(Cont_?) \cup \Pi_t^{\Phi_M, \Phi_N}(Cont_!), U_p, F_p$; then since $\Pi_\lambda(\lambda) = \lambda$, we can conclude that $(A_p, U_p, F_p) \stackrel{\Pi_\lambda(\lambda)}{\mapsto} (\Pi_C^{\Phi_M, \Phi_N}(C_{n+1}), U_p, F_p)$;

(d) in the case that $i \in \mathcal{L}_I$, $j \notin \mathcal{L}_I$ and $\stackrel{\lambda}{\to}_e$ is a communication rule: there exist two threads $t_? = (y?^i[y]P, id_?, E_?)$ and $t_! = (x!^j[x], id_!, E_!)$ in $C_n$ which satisfy that $E_?(y) = E_!(x)$ and $\lambda = (i, j)$, and two continuations $Cont_? \in \beta(P, id_?, E_?[y_i \mapsto x_i])$ and $Cont_! \in \beta(Q, id_!, E_!)$ such that $C_{n+1} = (C_n \setminus \{t_?; t_!\}) \cup Cont_? \cup Cont_!$; we have:

$$
\left\{
\begin{array}{ll}
\Pi_\lambda(t_?) \in A_p \text{ (thanks to Lem. 45 and since } i \in \mathcal{L}_I), & \\
\Pi_{\mathcal{N}}^{\Phi_M, \Phi_N}(E_?(y)) = \Pi_{\mathcal{N}}^{\Phi_M, \Phi_N}(E_!(x)) \in U_p \text{ (since } E_?(y) = E_!(x), & \\
\qquad \text{and thanks to Lem. 46.(1)),} & \\
\Pi_t^{\Phi_M, \Phi_N}(Cont_?) \in \beta(P, \Pi_M^{\Phi_M}(id_?), E_?'_?) \text{ (thanks to Lem. 44),} & \\
\qquad \text{where } E_?'_? = [x \mapsto \Pi_{\mathcal{N}}^{\Phi_M, \Phi_N}(E_?[y_k \mapsto E_!(x_k)])(x)] & \\
\{\Pi_{\mathcal{N}}^{\Phi_M, \Phi_N}(E_!(x_k))\} \subseteq U_p \text{ (thanks to Lem. 46.(1));} &
\end{array}
\right.
$$

so $(A_p, U_p, F_p) \overset{(i,0)}{\rightleftarrows} (A_p \setminus \{\Pi_t^{\Phi_M, \Phi_N}(t_?)\} \cup \Pi_t^{\Phi_M, \Phi_N}(Cont_?), U_p, F_p)$;
since $\Pi_\lambda(\lambda) = (i, 0)$, $(A_p, U_p, F_p) \overset{\Pi_\lambda(\lambda)}{\rightleftarrows} (\Pi_C^{\Phi_M, \Phi_N}(C_{n+1}), U_p, F_p)$;

(e) in the case that $i \in \mathcal{L}_I$, $j \notin \mathcal{L}_I$ and $\stackrel{\lambda}{\to}_e$ is a replication rule: there exist two threads $t_? = (*y?^i[y]P, id_?, E_?)$ and $t_! = (x!^j[x], id_!, E_!)$ in $C_n$ which satisfy that $E_?(y) = E_!(x)$ and $\lambda = (i, j)$, and two continuations $Cont_? \in \beta(P, N((i, j), id_?, id_!), E_?[y_i \mapsto x_i])$ and $Cont_! \in \beta(Q, id_!, E_!)$ such that $C_{n+1} = (C_n \setminus \{t_?\}) \cup Cont_? \cup Cont_!$; we have:

$$
\left\{
\begin{array}{ll}
\Pi_\lambda(t_?) \in A_p \text{ (thanks to Lem. 45 and since } i \in \mathcal{L}_I), & \\
\Pi_{\mathcal{N}}^{\Phi_M, \Phi_N}(E_?(y)) = \Pi_{\mathcal{N}}^{\Phi_M, \Phi_N}(E_!(x)) \in U_p \text{ (since } E_?(y) = E_!(x) & \\
\qquad \text{and thanks to Lem. 46.(1)),} & \\
\Pi_t^{\Phi_M, \Phi_N}(Cont_?) \in \beta(P, id_*, E_*), \text{ (thanks to Lem. 44),} & \\
\qquad \text{where } id_* = N((i, 0), \Pi_M^{\Phi_M}(id_?), \Phi_M(j, id_!)) & \\
\qquad \text{and } E_* = [x \mapsto \Pi_{\mathcal{N}}^{\Phi_M, \Phi_N}(E_?[y_k \mapsto E_!(x_k)])(x)], & \\
\{\Pi_{\mathcal{N}}^{\Phi_M, \Phi_N}(E_!(x_k))\} \subseteq U_p \text{ (thanks to Lem. 46.(1)),} & \\
\Phi_M(j, id_!) \in F_p \text{ (thanks to the Lem. 46.(2));} &
\end{array}
\right.
$$

so $(A_p, U_p, F_p) \overset{(i,0)}{\rightleftarrows} (A_p \cup \Pi_t^{\Phi_M, \Phi_N}(Cont_?), U_p, F_p \setminus \{\Phi_M(j, id_!)\})$; then since we gave $\Pi_\lambda(\lambda) = (i, 0)$, we can conclude that $(A_p, U_p, F_p) \stackrel{\Pi_\lambda(\lambda)}{\rightleftarrows} (\Pi_C^{\Phi_M, \Phi_N}(C_{n+1}), U_p, F_p \setminus \{\Phi_M(j, id_!)\})$;

(f) in the case that $i \notin \mathcal{L}_I$, $j \in \mathcal{L}_I$ and $\stackrel{\lambda}{\to}_e$ is a communication rule:
there exist two threads $t_? = (y^i[y]P, id_?, E_?)$ and $t_! = (x!^j[x], id_!, E_!)$ in $C_n$ which satisfy that $E_?(y) = E_!(x)$ and $\lambda = (i, j)$, and two continuations $Cont_? \in \beta(P, id_?, E_?[y_i \mapsto x_i])$ and $Cont_! \in \beta(Q, id_!, E_!)$ such that $C_{n+1} = (C_n \setminus \{t_?; t_!\}) \cup Cont_? \cup Cont_!$; we have:

$$ \left\{ \begin{array}{l} \Pi_{\lambda}(t_!) \in A_p \text{ (thanks to Lem. 45 and since } j \in \mathcal{L}_I), \\ \Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(E_!(y)) = \Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(E_?(x)) \in U_p \text{ (since } E_?(y) = E_!(x) \\ \text{and thanks to Lem. 46.(1)),} \\ \Pi_{t}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(Cont_!) \in \beta(Q, \Pi_{\mathcal{M}}^{\Phi_{\mathcal{M}}}(id_!), [x \mapsto \Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(E_!(x))), \\ \text{(thanks to Lem. 44)}; \end{array} \right. $$

so $(A_p, U_p, F_p) \overset{(0,j)}{\rightleftharpoons} (A_p \setminus \{\Pi_t^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(t_! )\} \cup \Pi_t^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(Cont_!), U_p \cup \{\Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(E_!(x_k))\}, F_p)$; since $\Pi_{\lambda}(\lambda) = (0, j)$, we can conclude that:

$$ (A_p, U_p, F_p) \overset{\Pi_{\lambda}(\lambda)}{\rightleftharpoons} (\Pi_{C}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(C_{n+1}), U_p \cup \{\Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(E_!(x_k))\}, F_p); $$

(g) in the case that $i \notin \mathcal{L}_I$, $j \in \mathcal{L}_I$ and $\xrightarrow{\lambda}_e$ is a replication rule: there exist two threads $t_? = (*y^i[y]P, id_?, E_?)$ and $t_! = (x!^j[x], id_!, E_!)$ in $C_n$ which satisfy that $E_?(y) = E_!(x)$ and $\lambda = (i, j)$, and two continuations $Cont_? \in \beta(P, N((i, j), id_?, id_!), E_?[y_i \mapsto x_i])$ and $Cont_! \in \beta(Q, id_!, E_!)$ such that $C_{n+1} = (C_n \setminus \{t_?; t_!\}) \cup Cont_? \cup Cont_!$; we have:

$$ \left\{ \begin{array}{l} \Pi_{\lambda}(t_!) \in A_p \text{ (thanks to Lem. 45 and since } j \in \mathcal{L}_I), \\ \Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(E_!(y)) = \Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(E_?(x)) \in U_p, \text{ (since } E_?(y) = E_!(x) \\ \text{and thanks to Lem. 46.(1)),} \\ \Pi_{t}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(Cont_!) \in \beta(Q, \Pi_{\mathcal{M}}^{\Phi_{\mathcal{M}}}(id_!), [x \mapsto \Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(E_!(x))]), \\ \text{(thanks to Lem. 44)}; \end{array} \right. $$

so $(A_p, U_p, F_p) \overset{(0,j)}{\rightleftharpoons} (A_p \setminus \{\Pi_t^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(t_! )\} \cup \Pi_t^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(Cont_!), U_p \cup \{\Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(E_!(x_k))\}, F_p)$; since $\Pi_{\lambda}(\lambda) = (0, j)$, we get $(A_p, U_p, F_p) \overset{\Pi_{\lambda}(\lambda)}{\rightleftharpoons} (A_{p+1}, U_p \cup \{\Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(E_!(x_k))\}, F_p)$. $\square$

**Lemma 47** Let $S_*$ be a closed system of the following form:

$$ (\nu \bar{c})(S_I(c_{i_1}, \dots, c_{i_p}) | S_c(c_{j_1}, \dots, c_{j_q})), $$

we denote by $\mathcal{L}_I$ the set of the label occurring in $S_I$. Let $\tau = C_0 \longrightarrow_*^e C_n$ be a non-standard computation sequence, with $C_0 \in C_0^e(S)$ and $\Phi_{\mathcal{M}} : \mathcal{L} \times \mathcal{M} \to \{t_n | n \in \mathbb{N}\}$ and $\Phi_{\mathcal{N}} : \mathcal{N} \times \mathcal{M} \to \text{en}$ be two one-to-one maps, then:
(1) for any marker id occurring in a state of the computation sequence $\tau$ such that id matches $N((i, j), id_?, id_!)$, we have:

• $i \in \mathcal{L}_I \Rightarrow \begin{cases} \text{either } id_? = \varepsilon, \\ \text{or } id_? \text{ matches } N((i', j'), id_?, id_!) \text{ where } i' \in \mathcal{L}_I; \end{cases}$

• $j \in \mathcal{L}_I \Rightarrow \begin{cases} \text{either } id_! = \varepsilon, \\ \text{or } id_! \text{ matches } N((i', j'), id_?, id_!) \text{ where } i' \in \mathcal{L}_I; \end{cases}$

(2) let $id_1$ and $id_2$ be two markers occurring in a state of the computation sequence $\tau$ such that $\Pi_{\mathcal{M}}^{\mathcal{M}}(id_1) = \Pi_{\mathcal{M}}^{\mathcal{M}}(id_2)$, then $id_1 = id_2$;

(3) let $c_1$ and $c_2$ be two names in $\mathcal{N} \times \mathcal{M}$ occurring in a state of the computation sequence $\tau$ such that $\Pi_{\mathcal{N}'}^{\mathcal{M}, \mathcal{N}}(c_1) = \Pi_{\mathcal{N}'}^{\mathcal{M}, \mathcal{N}}(c_2)$, then $c_1 = c_2$.

PROOF.

(1) Prop. (1) can be proved using both the fact that:

(a) if the label $i$ of a thread $t$ is in the set $\mathcal{L}_I$, then either its marker is $\varepsilon$, or there exists a marker $i'$ such that the syntactic agent labelled with $i'$ contains the sub-term labelled with $i$, and that the marker of the thread $t$ is necessarily of the form $N((i', j), id_?, id_!)$ where $i' \in \mathcal{L}_I$,

(b) a marker of the form $N((i, j), id_?, id_!)$ can be created only when a thread the label of which is $i$ and the marker of which is $id_?$ interacts with a thread the label of which is $j$ and the marker of which is $id_!$;

(2) Prop. (2) can be proved by induction over the height of the markers; this induction only uses Prop. (1) and the fact that the subtree of a marker occurring in a state of $\tau$ necessarily occurs in a previous state of $\tau$;

(3) Prop. (3) follows from Prop. (2) and the fact that whenever a channel name has been opened by a restriction in $\mathcal{S}_I$, its marker is also the marker of a former thread the label of which is in $\mathcal{L}_I$. $\square$

**Theorem 23 (Completeness)** Let $\tau'$ be the non-standard computation sequence of an open system $\mathcal{S}_I$, that we denote by:

$$ (C_0, U_0, F_0) \overset{(i_1, j_1)}{\rightleftharpoons} \dots \overset{(i_n, j_n)}{\rightleftharpoons} (C_n, U_n, F_n), $$

where $(C_0, U_0, F_0) \in \mathcal{C}_0^o(\mathcal{S}_I)$.

Then there exists:

• a closed system $\mathcal{S}_* = (\nu \bar{c})(\mathcal{S}_I(c_{i_1}, \dots, c_{i_n}) | \mathcal{S}_c(c_{j_1}, \dots, c_{j_n}))$,

• two one-to-one functions $\Phi_{\mathcal{N}}$ and $\Phi_{\mathcal{M}}$,

• a non-standard computation sequence $\tau$ of the system $\mathcal{S}_*$,

such that $\Pi_{\tau}(\mathcal{S}_I, \Phi_{\mathcal{M}}, \Phi_{\mathcal{N}})(\tau) = \tau'$.

We will prove the following stronger result:
**Proposition 48** Let $\tau'$ be the non-standard computation sequence of an open system $S_1$, defined as follows:

$$ (A_0, U_0, F_0) \underset{\sim}{\overset{(i_1, j_1)}{\rightleftharpoons}} \dots \underset{\sim}{\overset{(i_n, j_n)}{\rightleftharpoons}} (A_n, U_n, F_n), $$

where $(A_0, U_0, F_0) \in C_0^0(S_1)$. Let $\mathcal{L}_1 \subseteq \mathcal{L}$ be the subset of the labels occurring in $S_1$ and $\mathcal{N}_1 \subseteq \mathcal{N}$ be the subset of the names occurring in name restrictions of $S_1$.

Then there exists:

* a closed system of the form:

$$ \mathcal{S}_* = (\nu \text{ unsafe})(\nu x_1)\dots(\nu x_p) \\ (\text{unsafe!}[x_1] | \dots | \text{unsafe!}[x_p] | \mathcal{S}_I(x_{i_1}, \dots, x_{i_n}) | \mathcal{S}_c(\text{unsafe})) $$

where

$$ \mathcal{S}_c = (\nu \text{ new}) \\ ( \textbf{new} | \textbf{repli} \\ | \textbf{spy}_0 | \dots | \textbf{spy}_n \\ | \textbf{spoil}_0 | \dots | \textbf{spoil}_n \\ | \text{new!} ] ) $$

and

* **new** := *new?*[]((ν channel)(unsafe![channel] | new![]))

* **repli** := *unsafe?*![x](*unsafe?*![x] | unsafe![x])

* **spyi** := *unsafe?*![c]c?*[y_1, ..., y_i](*unsafe?*![y_1] | ... | unsafe![y_i])

* **spoil**i := *unsafe?*![c]unsafe?*[x_1]...unsafe?*[x_i]c![x_1, ..., x_i]

* a non-standard computation sequence $\tau$ of the closed system $S_*$,

* two into maps $\Phi_N$ and $\Phi_M$, such that:

$$ \cdot \Phi_N : \left\{ (y, id_y) \left| \begin{array}{l} y \notin \mathcal{N}_1, \exists (P, id, E) \in \bigcup C_i, \text{lab}(P) \in \mathcal{L}_1, \\ \exists x \in \text{fn}(P), E(x) = (y, id_y) \end{array} \right. \right\} \to \text{en}; $$

$$ \cdot \Phi_M : \left\{ id \left| \begin{array}{l} \exists (P, N((i, 0), id_?, id_!), E) \in \bigcup C_i, \\ \text{lab}(P) \in \mathcal{L}_1 \end{array} \right. \right\} \to \{t_n \mid n \in \mathbb{N}\}. $$

such that:

$$ (1) \Pi_{\tau}(S_1, \Phi_M, \Phi_N)(\tau) = \tau^{\prime 11}; $$

<footnote n="11">11 we make abusively no distinction neither between $\Phi_N$ and any one-to-one extension of it defined over the set $\mathcal{N} \times \mathcal{M}$, nor between $\Phi_M$ and any one-to-one extension of it defined over the set $\mathcal{M}$</footnote>
(2) for any unsafe name $(x, id_x) \in U_n$, that occurs in a state of $\tau'$, there exists a thread in the last state of $\tau$ of the form (unsafe![y], id, E) with $\Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(E(y)) = (x, id_x)$.

**PROOF.** We prove Prop. 48 by induction on the length of the computation sequence $\tau'$:

(1) in the case that $\tau'$ is of the form $(A_0, U_0, F_0) \in C_0^o(S_I)$, there exists $E \in \text{fn}(S_I) \to \text{en}$ such that $A_0 \in \beta(S_I, \varepsilon, E)$; we also have $U_0 = \text{en}$ and $F_0 = \{t_n \mid n \in \mathbb{N}\}$;
we take $\Phi_{\mathcal{M}} : \emptyset \to \{t_n \mid n \in \mathbb{N}\}$; we denote by $e_1, \dots, e_u$ the elements of the set $\{E(x) \mid x \in \text{fn}(S_I)\}$, we take $\Phi_{\mathcal{N}} : \{c_{i_k} \mid k \in \llbracket 1; u \rrbracket\} \to \text{en}$, such that for any $k \in \llbracket 1; u \rrbracket$, we have $\Phi_{\mathcal{N}}(c_{i_k}) = e_i$; thanks to Lem. 44, we have $\beta(S_I, \varepsilon, E) = \Pi_C^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(\beta(S_*, \varepsilon, \Phi_{\mathcal{N}}^{-1} \circ E))$; so we can choose $C_0 \in \beta(S_*, \varepsilon, \Phi_{\mathcal{N}}^{-1} \circ E)$ such that $A_0 = \Pi_C^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(C_0)$;

• we have $(A_0, U_0, F_0) = \Pi_{\tau}(S_I, \Phi_{\mathcal{M}}, \Phi_{\mathcal{N}})(C_0)$;

• for any unsafe name $(x, id_x) \in U_0$ occurring in $A_0$, there exists by construction a thread of the form (unsafe![y], id, E) with $\Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(E(y)) = (x, id_x)$;

(2) in the case that $\tau'$ is of the form $(A_0, U_0, F_0) \dots (A_{p-1}, U_{p-1}, F_{p-1}) \stackrel{\lambda}{\rightleftarrows} (A_p, U_p, F_p)$; we assume by the induction hypothesis that there exist:

• a non-standard computation sequence $\tau = C_0 \dots C_n$ of the closed system $S_*$ such that $C_0 \in C_0^e(S_*)$,

• two into maps $\Phi_{\mathcal{N}}$ and $\Phi_{\mathcal{M}}$, such that:

$$ \cdot \Phi_{\mathcal{N}} : \left\{ \begin{array}{l} (y, id_y) \qquad \begin{array}{l} y \notin \mathcal{N}_I, \exists(P, id, E) \in \cup C_i, \\ \text{lab}(P) \in \mathcal{L}_I, \\ \exists x \in \text{fn}(P), E(x) = (y, id_y) \end{array} \end{array} \right\} \to \text{en}, \\ \cdot \Phi_{\mathcal{M}} : \left\{ \begin{array}{l} id \qquad \exists(P, N((i, 0), id_?, id_!), E) \in \cup C_i, \\ \text{lab}(P) \in \mathcal{L}_I \end{array} \right\} \to \{t_n \mid n \in \mathbb{N}\}; $$

such that:

• $\Pi_{\tau}(S_I, \Phi_{\mathcal{M}}, \Phi_{\mathcal{N}})(\tau) = (A_0, U_0, F_0) \dots (A_{p-1}, U_{p-1}, F_{p-1})$;

• for any unsafe name $(x, id_x) \in U_n$ that occurs in a state of $\tau'$, there exists a thread in the last state of $\tau$ of the form (unsafe![y], id, E) with $\Pi_{\mathcal{N}}^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(E(y)) = (x, id_x)$.

We proceed by case analysis in accordance with the kind of the next computation step:

(a) in the case that $(A_{p-1}, U_{p-1}, F_{p-1}) \stackrel{\lambda}{\rightleftarrows} (A_p, U_p, F_p)$ is a communication rule: there exist two threads $t_? = (y?^i[\bar{y}]P, id_?, E_?)$ and $t_! = (x!^j[\bar{x}]Q, id_!, E_!)$ with $E_?(y) = E_!(x)$, two continuations $\text{Cont}_? \in \beta(P, id_?, E_?[y_i \mapsto E_!(x_i)])$ and $\text{Cont}_! \in \beta(Q, id_!, E_!)$ such that $A_p = (A_{p-1} \setminus \{t_?; t_!\}) \cup \text{Cont}_? \cup \text{Cont}_!$; moreover, we have $\Pi_C^{\Phi_{\mathcal{M}}, \Phi_{\mathcal{N}}}(C_n) =$
$A_{p-1}$, so by definition of $\Pi_C^{\Phi_M, \Phi_N}$ the state $C_n$ contains two threads $t'_? = (y?^i[\bar{y}]P, id'_?, E'_?)$ and $t'_! = (x!^j[\bar{x}]Q, id'_!, E'_!)$ with $\Pi_M^{\Phi_M}(id'_?) = id_?, \Pi_M^{\Phi_M}(id'_!) = id_!$, $\Pi_N^{\Phi_M, \Phi_N} \circ E'_? = E_?$ and $\Pi_N^{\Phi_M, \Phi_N} \circ E'_! = E_!$; thanks to Lem. 44, there also exist $Cont'_? \in \beta(P, id'_?, E'_? [y_k \mapsto E'_!(x_k)])$ and $Cont'_! \in \beta(Q, id'_?, E'_!)$ such that $\Pi_C^{\Phi_M, \Phi_N}(Cont'_?) = Cont_?$ and $\Pi_C^{\Phi_M, \Phi_N}(Cont'_!) = Cont_!$;

we set $C_{n+1} = (C_n \setminus \{t'_?; t'_!\}) \cup Cont'_? \cup Cont'_!$;

* thanks to Lem. 47.(3), since $E_?(y) = E_!(x)$, we have $E'_?(y) = E'_!(x)$; so we have $C_n \xrightarrow{\lambda} C_{n+1}$; moreover $\Pi_C^{\Phi_M, \Phi_N}(C_{n+1}) = A_p$; so $\Pi_\tau(S_I, \Phi_M, \Phi_N)(C_0...C_n \xrightarrow{\lambda} C_{n+1}) = \tau'$;

* the last computation step of $\tau'$ does not involve unsafe name and the computation step $C_n \xrightarrow{\lambda} e C_{n+1}$ does not consume any thread of the form (unsafe![y], id, E); so by the induction hypothesis, we get that for any unsafe name $(x, id_x) \in U_n$ occurring in a state of $\tau'$, there exists a thread in the last state of $\tau$ of the form (unsafe![y], id, E) with $\Pi_N^{\Phi_M, \Phi_N}(E(y)) = (x, id_x)$;

(b) in the case that $(A_{p-1}, U_{p-1}, F_{p-1}) \stackrel{\lambda}{\rightleftharpoons} (A_p, U_p, F_p)$ is a resource replication; there are two threads $t_? = (*y?^i[\bar{y}]P, id_?, E_?)$ and $t_! = (x!^j[\bar{x}]Q, id'_?, E'_?)$ with $E_?(y) = E_!(x)$, two continuations $Cont_? \in \beta(P, N((i, j), id_?, id'_?), E_?[y_i \mapsto E_!(x_i)])$ and $Cont'_! \in \beta(Q, id'_?, E'_!)$ such that $A_p = (A_{p-1} \setminus \{t_?\}) \cup Cont_? \cup Cont'_!$; moreover, we have $\Pi_C^{\Phi_M, \Phi_N}(C_n) = A_{p-1}$, so by definition of $\Pi_C^{\Phi_M, \Phi_N}$ there exist two threads $t'_? = (*y?^i[\bar{y}]P, id'_?, E'_?)$ and $t'_! = (x!^j[\bar{x}]Q, id'_?, E'_?)$ in $C_n$ with $\Pi_M^{\Phi_M}(id'_?) = id_?, \Pi_M^{\Phi_M}(id'_!) = id_!$, $\Pi_N^{\Phi_M, \Phi_N} \circ E'_? = E_?$ and $\Pi_N^{\Phi_M, \Phi_N} \circ E'_! = E_!$; moreover we have $\Pi_M^{\Phi_M}(N((i, j), id'_?, id'_!)) = N((i, j), id_?, id'_!)$; thanks to Lem. 44, there also exist two continuations $Cont'_! \in \beta(Q, id'_?, E'_!)$ and $Cont'_? \in \beta(P, N((i, j), id'_?, id'_!), E'_?[y_k \mapsto E'_!(x_k)])$ such that the properties $\Pi_C^{\Phi_M, \Phi_N}(Cont'_?) = Cont_?$ and $\Pi_C^{\Phi_M, \Phi_N}(Cont'_!) = Cont_!$ are satisfied;

we set $C_{n+1} = (C_n \setminus \{t'_?\}) \cup Cont'_? \cup Cont'_!$;

* thanks to Lem. 47.(3), since $E_?(y) = E_!(x)$, we have $E'_?(y) = E'_!(x)$; so we have $C_n \xrightarrow{\lambda} C_{n+1}$; moreover $\Pi_C^{\Phi_M, \Phi_N}(C_{n+1}) = A_p$; so $\Pi_\tau(S_I, \Phi_M, \Phi_N)(C_0...C_n \xrightarrow{\lambda} C_{n+1}) = \tau'$;

* the last computation step of $\tau'$ does not involve unsafe name and the computation step $C_n \xrightarrow{\lambda} e C_{n+1}$ does not consume any thread of the form (unsafe![y], id, E); so by the induction hypothesis, we get that for any unsafe name $(x, id_x) \in U_n$ occurring in a state of $\tau'$, there exists a thread in the last state of $\tau$ of the form (unsafe![y], id, E) with $\Pi_N^{\Phi_M, \Phi_N}(E(y)) = (x, id_x)$;

(c) in the case that $(A_{p-1}, U_{p-1}, F_{p-1}) \stackrel{\lambda}{\rightleftharpoons} (A_p, U_p, F_p)$ is a spied communication: there is a thread $t_! = (x!^j[x_1, ..., x_k]Q, id_!, E_!)$ with $E_!(x) \in U_{p-1}$, a continuation $Cont_! \in \beta(Q, id_!, E_!)$ such that $A_p = (A_{p-1} \setminus \{t_!\}) \cup Cont_!$, and $U_p = U_{p-1} \cup \{E_!(x_i) | i \in [1; k]\}$; moreover, we have