# Occurrence counting analysis for the pi-calculus

Jérôme Feret

► To cite this version:

Jérôme Feret. Occurrence counting analysis for the pi-calculus. GEometry and Topology in COncurrence theory (Satellite Workshop from CONCUR 2000), Eric Goubault, Aug 2000, University Park, United States. pp.1–18, 10.1016/S1571-0661(05)01155-2. inria-00527933

HAL Id: inria-00527933

https://inria.hal.science/inria-00527933v1

Submitted on 15 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
Occurrence Counting Analysis
for the π-calculus

Jérôme Feret

Laboratoire d'Informatique de l'École Normale Supérieure
ENS-LIENS, 45, rue d'Ulm, 75230 PARIS cédex 5, FRANCE

**Abstract**

We propose an abstract interpretation-based analysis for automatically proving non-trivial properties of mobile systems of processes. We focus on properties relying on the number of occurrences of processes during computation sequences, such as mutual exclusion and non-exhaustion of resources.

We design a non-standard semantics for the π-calculus in order to explicitly trace the origin of channels and to solve efficiently problems set by α-conversion and non-deterministic choices. We abstract this semantics into an approximate one. The use of a relational domain for counting the occurrences of processes allows us to prove quickly and efficiently properties such as mutual exclusion and non-exhaustion of resources. At last, dynamic partitioning allows us to detect some configurations by which no infinite computation sequences can pass.

# 1 Introduction

We are interested in automatically proving non-trivial properties of mobile systems of processes. We focus on properties relying on a good description of the multiset of processes that occur inside computation sequences, such as mutual exclusion and non-exhaustion of resources, for instance.

We propose an abstract interpretation-based analysis for the full π-calculus [19,18]. Since, the π-calculus is a communication-based formalism, no analysis can be done without a good approximation of the control-flow. Following Venet's methodology [23], we introduce a non-standard semantics to explicitly capture the origin of channels and to describe non-uniform distributions of processes. Our semantics considers the full π-calculus and is optimized to deal efficiently with non-deterministic choices (no useless thread is created).

We use the abstract interpretation framework [8,6,10] to derive an approximate semantics to analyze both the interaction between processes and the number of occurrences of these processes. We propose a well adapted
domain to detect quickly mutual exclusion and non-exhaustion of resources. Our approach relies on the use of a relational domain the height of which is quadratic on the number of distinct counted processes. This relational domain helps in calculating properties of interest in a non-relational domain, by reduction. Complexity problems are solved by using approximated algorithms for calculating this reduction. Number of occurrences of processes defines a good criterion for partitioning: we use dynamic partitioning [3] to abstract precisely the trace semantics of mobile systems, which allows us to detect a set of configurations such that no infinite computation sequence can pass by a configuration in this set. Our methodology may very likely be adapted to other formalisms, such as the mobile ambients [4] for instance.

In Section 3, we define the standard semantics of the π-calculus. We define our non-standard semantics in Section 4. We design a generic abstract analysis in Section 5, and instantiate it in Section 6. We show how to use dynamic partitioning in Section 7.

## 2 Related work

Counting occurrences and analyzing the control flow of a system are deeply related. We cannot count number of occurrences of processes in a system without a good knowledge of its control flow, but counting occurrences helps in getting a more precise knowledge of the control flow by detecting mutual exclusion between processes and by providing a good criterion for partitioning. Our analysis can directly be combined with our previous analysis [14] to infer a non-uniform description of the interactions between the processes, but can also be adapted to many other flow analyses [2,23].

Only a very few analyses for counting occurrences of processes have been published. [15] proposes an exponential analysis for counting occurrences of processes inside ambients. [20] uses context-dependent counts for inferring a more accurate description of the internal structure of processes at the expense of a higher time complexity (an exponential number of processes are distinguished). These analyses encounter the same problem: when a process occurs several times, they cannot decide whether this process is still occuring one or several times after being computed, so they have to consider the two possible cases, which leads to both a loss of precision and an exponential explosion. The use of both a relational domain for globally abstracting sets of multisets of processes and an approximated reduction allows us to solve this problem efficiently. We obtain a very accurate analysis which is polynomial on the number of distinguished processes.

## 3 π-calculus

The π-calculus [18,19] is used for describing mobile systems of processes which communicate channel names via channels. We consider a lazy synchronous
version of the polyadic π-calculus, inspired by the lazy asynchronous version introduced by Turner [21] and the chemical abstract machine [1] in which communication primitives are very simple, while ensuring the same expres- sive power. Let Channel be a countable set of channel names, the standard semantics of the π-calculus, given in Figure 1, relies on the use of both a re- duction relation to define results of process computations, and a congruence relation to reveal redexes.

**Example 3.1** We model by a mobile system $\mathcal{S}$ an ftp protocol for a server which cannot establish more than three simultaneous connections:

$$ \mathcal{S} := (\nu \text{ port})(\mathbf{Allocate} | \text{port!}] | \text{port!}] | \text{port!}]) $$

where

$$ \mathbf{Allocate} := *\text{port?}[(\nu \text{ in})(\nu \text{ out})(\nu \text{ query}) \\ (\text{in!}[\text{query}] \\ | \text{in?}[\text{response}].(\text{out!}[\text{response}] | \text{port!}))) $$

Each message port![] occurring at top level symbolizes an available connec- tion. When a customer requests an available connection, three channel names query , in and out are created. The customer sends its query, represented by the channel query , via the channel in . The server computes this query and sends it back via the channel out . A new message port![] is then spawn, which symbolizes that the connection is released. We shall notice that many compu- tational aspects are abstracted away, since we present only an approximation of a realistic server. We finally propose a short computation for S as follows:

$$ \begin{align*} \mathcal{S} &= (\nu \text{ port}) \\ &\rightarrow (\nu \text{ port})(\nu \text{ in}_1)(\nu \text{ out}_1)(\nu \text{ query}_1) \\ &\qquad ( \mathbf{Allocate} | \text{port!}] | \text{port!}] | \text{port!}] \\ &\qquad | \text{in}_1![\text{query}_1] \\ &\qquad | \text{in}_1?[\text{response}].(\text{out}_1![\text{response}] | \text{port!})) \\ &\rightarrow (\nu \text{ port})(\nu \text{ in}_1)(\nu \text{ out}_1)(\nu \text{ query}_1) \\ &\qquad ( \mathbf{Allocate} | \text{port!}] | \text{port!}] | \text{port!}] \\ &\qquad | \text{out}_1![\text{query}_1]) \end{align*} \quad \square $$

As illustrated in the above example, the configuration of a mobile system is at any stage congruent with a configuration of the form $(\nu c)(P_1 | \dots | P_n)$, where c is a sequence of channel names, and $P_1, \dots, P_n$ are syntactic copies of sub-processes which have been substituted during communications. Nerver- theless, standard semantics allows to trace neither the origin of those processes, nor the origin of the channels they have declared.

## 4 Non-standard semantics

A non-standard semantics [23] is a refined semantics, which explicitly speci- fies the link between channels and the instances of processes which have de- clared them. It identifies any instance of a process by an unambiguous marker
<table><tr><td>P</td><td>::=</td><td>action.P</td><td>(Action)</td></tr><tr><td></td><td>|</td><td>(P | P)</td><td>(Parallel composition)</td></tr><tr><td></td><td>|</td><td>(P + P)</td><td>(Non-deterministic choice)</td></tr><tr><td></td><td>|</td><td>Ø</td><td>(End of a process)</td></tr></table>

<table><tr><td>action</td><td>::=</td><td>c![x<sub>1</sub>, ..., x<sub>n</sub>]</td><td>(Message)</td></tr><tr><td></td><td>|</td><td>c?[x<sub>1</sub>, ..., x<sub>n</sub>]</td><td>(Input guard)</td></tr><tr><td></td><td>|</td><td>*c?[x<sub>1</sub>, ..., x<sub>n</sub>]</td><td>(Replication guard)</td></tr><tr><td></td><td>|</td><td>(&nu; x)</td><td>(Channel creation)</td></tr></table>

where $c, x_1, ..., x_n, x \in Channel$, $n \ge 0$. Input guard, replication guard and channel creation are the only name binders, i.e in $c?[x_1, ..., x_n]P$, $*d?[y_1, ..., y_p]Q$ and $(\nu x)R$, occurrences of $x_1, ..., x_n$ in $P$, $y_1, ..., y_p$ in $Q$ and $x$ in $R$ are considered bound. Usual rules about scoping, substitution and $\alpha$-conversion apply. We denote by $\mathcal{FN}(P)$ the set of free names of $P$, i.e names which are not under the scope of a binder and by $\mathcal{BN}(P)$ the set of bound names of $P$.

(a) Syntax

<table><tr><td>(&nu; x)P &equiv; (&nu; y)P[x &leftarrow; y]</td><td>if y &notin; &Fcal{N}(P)</td><td>(&alpha;-conversion)</td></tr><tr><td>P | Q &equiv; Q | P</td><td></td><td>(Commutativity)</td></tr><tr><td>P | (Q | R) &equiv; (P | Q) | R</td><td></td><td>(Associativity)</td></tr><tr><td>P | Ø &equiv; P</td><td></td><td>(End of a process)</td></tr><tr><td>(&nu; x)(&nu; y)P &equiv; (&nu; y)(&nu; x)P</td><td></td><td>(Swapping)</td></tr><tr><td>((&nu; x)P) | Q &equiv; (&nu; x)(P | Q)</td><td>if x &notin; &Fcal{N}(Q)</td><td>(Extrusion)</td></tr></table>

where $x, y \in Channel$

(b) Congruence relation

<table><tr><td>c![x<sub>1</sub>, ..., x<sub>n</sub>]P | c?[y<sub>1</sub>, ..., y<sub>n</sub>]Q &rarr; P | Q&#771;</td><td>(communication)</td></tr><tr><td>c![x<sub>1</sub>, ..., x<sub>n</sub>]P | *c?[y<sub>1</sub>, ..., y<sub>n</sub>]Q &rarr; P | Q&#771; | *c?[y<sub>1</sub>, ..., y<sub>n</sub>]Q</td><td>(res. fetching)</td></tr><tr><td>P + Q &rarr; P</td><td>(left choice)</td></tr><tr><td>P + Q &rarr; Q</td><td>(right choice)</td></tr></table>

$$ \frac{P \to Q}{(\nu x)P \to (\nu x)Q} \qquad \frac{P' \equiv P \quad P \to Q \quad Q \equiv Q'}{P' \to Q'} \qquad \frac{P \to P'}{P | Q \to P' | Q} $$

where $c, x, x_1, ..., x_n, y_1, ..., y_n \in Channel$

and $\tilde{Q} = Q[y_1 \leftarrow x_1, ..., y_n \leftarrow x_n]$

(c) Reduction relation

<caption>Fig. 1. The chemical semantics</caption>
in order to distinguish each instance of a recursive process from all others. Then, the origin of channel names is easily traced by identifying each channel name with the marker of the process which has created it. In [14] we propose a non-standard semantics which considers the full π-calculus without non-deterministic choices. We redefine it in order to take them into account efficiently, without adding further reduction rules nor considering useless syntactic components. This allows for an easier analysis by making abstract domains smaller while giving a good intuition on the potential evolutions of the analyzed systems. For that purpose, we restrict the set of computations to those where non-deterministic choices are made as soon as possible. In such computations, no further communication nor resource fetching is performed while there are non-deterministic choices at the top level. This assumption does not change the subset of reachable standard configurations which contain no non-deterministic choice at top level.

Let Lbl be an infinite set of labels, we denote by $\mathcal{M}$ the set of all binary trees the leaves of which are not labelled ($\varepsilon$) and the nodes of which are labelled with a pair $(i, j)$ where both $i$ and $j$ are in Lbl. The tree, having a node labelled $a$, a left sibling $t_1$ and a right sibling $t_2$ is denoted by $N(a, t_1, t_2)$. We use $\mathcal{M}$ as a set of markers and denote by $\Sigma$ the set $LBL \times Lbl$. $\Sigma$ is used in labelling non-standard transitions. We consider a closed mobile system $\mathcal{S}$ in the π-calculus and assume without any loss of generality that two channel binders of $\mathcal{S}$ are never used on the same channel name. We locate syntactic components of $\mathcal{S}$ by marking each sign ? or ! occurring in $\mathcal{S}$ with distinct labels in Lbl. A non-standard configuration is a set of thread instances, where a thread instance is a triplet composed with a syntactic component, a marker and an environment. The syntactic component is a copy of a sub-process of $\mathcal{S}$, the marker is calculated at the creation of the thread and the environment specifies the semantic value of each free name in the syntactic component. Thread instances are created at the beginning of the system computation and during execution. In both cases, several threads are spawned, corresponding to a set of syntactic components, in accordance to which non-deterministic choices are made. Applying the function Agent, defined as follows, to either $\mathcal{S}$ for initial threads, or to the continuation of running processes, gives the set of all possibilities for the set of spawned syntactic components.

$$
\begin{align*}
Agent(\emptyset) &= \{\{\}\} \\
Agent(x^i[x_1, \dots, x_n]P) &= \{\{x^i[x_1, \dots, x_n]P\}\} \\
Agent(y^i[y_1, \dots, y_n]P) &= \{\{y^i[y_1, \dots, y_n]P\}\} \\
Agent(*y^i[y_1, \dots, y_n]P) &= \{\{*y^i[y_1, \dots, y_n]P\}\} \\
Agent(P | Q) &= \{A \cup B \mid A \in Agent(P), B \in Agent(Q)\} \\
Agent(P + Q) &= Agent(P) \cup Agent(Q) \\
Agent((\nu x)P) &= Agent(P)
\end{align*}
$$

The markers of initial threads are $\varepsilon$, while the markers of new threads are calculated recursively from the marker of the threads whose computation has
led to their creation:

* when an execution does not involve fetching a resource, the marker of the computed thread is just passed to the threads in its continuation;

* when a resource is fetched, the markers of the new threads created from the continuation of the resource are $N((i, j), id_*, id_!)$, where $(i,id_*,E_*)$ is the fetched resource thread and $(j,id_!,E_!)$ the message sender thread.

Environments map each free channel name of syntactic components to a pair $(a, b)$ where $a$ is a bound channel name of $S$, and $b$ is a marker. Intuitively, $a$ refers to the binder $(\nu a)$ which has been used in declaring the channel, and $b$ is the marker of the thread which has declared it. While threads are running, environments are calculated in order to mimic the standard semantics.

We denote by $C$ the set of all non-standard configurations. Our non-standard semantics is given in Figure 2. The function $C_0$ gives the set of possible initial configurations, while the relation $\to_2$ defines non-standard computation steps. Each non-standard communication steps are labelled with a pair $(i, j) \in \Sigma$, where $i$ is the label of the message receiver and $j$ is the label of the message sender. There is a bisimulation between standard and non-standard semantics, provided that we restrict the set of standard computations to those where all non-deterministic choices are always made before communications and resource fetching. The proof relies on the fact that non-standard computations cannot yield conflicts between the markers of the threads.

# 5 Abstraction

The set of all possible non-standard configurations a system may take during a finite computation sequence is given by its collecting semantics [7] and can be expressed as the least fixpoint of the following $\cup$-complete endomorphism $F$ on the complete lattice $\wp(\Sigma^* \times C)$:

$$F(X) = \{(\varepsilon, C) \mid C \in C_0(S)\} \cup \{(u.\lambda, C) \mid \exists(u, C') \in X, C' \xrightarrow{\lambda} \to_2 C\}$$

We use abstract interpretation [8] to design an abstract domain in which a decidable description of $Coll(S)$ will be computed. Our abstract domain is the reduced product of two domains: the first one describes the control-flow of $S$; the second one counts occurrences of its processes. Since the $\pi$-calculus is a communication-based formalism, any further analysis requires a good approximation of the communication topology. Several analyses [2,22,23,14] have already been proposed. For the sake of simplicity, we use a naive uniform analysis to abstract the control-flow of systems, but it could be enriched by using the non-uniform analysis proposed in [14]. We introduce the set $BN(S)^2$ as the set of all possible interactions between agents of the system $S$; intuitively the pair $(x, y)$ denotes that the channel name $x$ may be bound to a channel created by the binder $(\nu y)$. Our first abstract domain is then the complete
$$C_0(\mathcal{S}) = \{(p, \varepsilon, E_p) \mid p \in \text{Cont}\} \mid \text{Cont} \in \text{Agent}(\mathcal{S})\}$$

$$\text{where } E_p = \begin{cases} \mathcal{FN}(p) & \to \mathcal{BN}(\mathcal{S}) \times \mathcal{M} \\ x & \mapsto (x, \varepsilon) \end{cases}$$

(a) Set of initial non-standard configurations

If C is a non-standard configuration,

if there are $\lambda, \mu$ in C,

with $\lambda=(y^i[y_1, ..., y_n]P, id_?, E_?)$ and $\mu=(x^j[x_1, ..., x_n]Q, id_!, E_!)$

such that $E_?(y) = E_!(x)$,

if $Cont_P$ is in Agent(P) and $Cont_Q$ is in Agent(Q),

then $C \xrightarrow{(i,j)}_2 C'$

where $C' = (C \setminus \{\lambda, \mu\}) \cup (f_?(Cont_P)) \cup (f_!(Cont_Q)),$

$$f_? : Ag \mapsto \left( Ag, id_?, \begin{cases} z \mapsto E_?(z) & \text{if } z \in \mathcal{FN}(Ag) \cap \mathcal{FN}(y^i[y_1, ..., y_n]P) \\ y_k \mapsto E_!(x_k) & \text{if } y_k \in \mathcal{FN}(Ag) \\ z \mapsto (z, id_?) & \text{if } \begin{cases} z \in \mathcal{FN}(Ag) \cap \mathcal{BN}(y^i[y_1, ..., y_n]P) \\ z \notin \{y_k | k \in [|1; n|]\} \end{cases} \end{cases} \right)$$

$$\text{and } f_! : Ag \mapsto \left( Ag, id_!, \begin{cases} z \mapsto E_!(z) & \text{if } z \in \mathcal{FN}(Ag) \cap \mathcal{FN}(x^j[x_1, ..., x_n]Q) \\ z \mapsto (z, id_!) & \text{if } z \in \mathcal{FN}(Ag) \cap \mathcal{BN}(x^j[x_1, ..., x_n]Q) \end{cases} \right)$$

(b) Non-standard communication

If C is a non-standard configuration,

if there are $\lambda, \mu$ in C,

with $\lambda=(*y^i[y_1, ..., y_n]P, id_?, E_?)$ and $\mu = (x^j[x_1, ..., x_n]Q, id_!, E_!)$

such that $E_?(y) = E_!(x)$,

if $Cont_P$ is in Agent(P) and $Cont_Q$ is in Agent(Q),

then $C \xrightarrow{(i,j)}_2 C'$

where $C' = (C \setminus \{\mu\}) \cup (f_?(Cont_P)) \cup (f_!(Cont_Q)),$

$id_* = N((i, j), id_?, id_!)$,

$$f_? : Ag \mapsto \left( Ag, id_*, \begin{cases} z \mapsto E_?(z) & \text{if } z \in \mathcal{FN}(Ag) \cap \mathcal{FN}(y^i[y_1, ..., y_n]P) \\ y_k \mapsto E_!(x_k) & \text{if } y_k \in \mathcal{FN}(Ag) \\ z \mapsto (z, id_?) & \text{if } \begin{cases} z \in \mathcal{FN}(Ag) \cap \mathcal{BN}(y^i[y_1, ..., y_n]P) \\ z \notin \{y_k | k \in [|1; n|]\} \end{cases} \end{cases} \right)$$

$$\text{and } f_! : Ag \mapsto \left( Ag, id_!, \begin{cases} z \mapsto E_!(z) & \text{if } z \in \mathcal{FN}(Ag) \cap \mathcal{FN}(x^j[x_1, ..., x_n]Q) \\ z \mapsto (z, id_!) & \text{if } z \in \mathcal{FN}(Ag) \cap \mathcal{BN}(x^j[x_1, ..., x_n]Q) \end{cases} \right)$$

(c) Non-standard resource fetching

<caption>Fig. 2. Non-standard semantics</caption>
lattice $\wp(\mathcal{BN}(\mathcal{S})^2)$ related to our concrete domain via a Galois connection $(\alpha_{\text{com}}, \gamma_{\text{com}})$ defined as follows:

$$ \alpha_{\text{com}}(A) = \left\{ (x, y) \;\middle|\; \begin{array}{l} \exists(u, C) \in A, \exists(P, id_1, E) \in C, \exists id_2 \in \mathcal{M} \\ \text{such that } x \in \mathcal{FN}(P) \text{ and } E(x) = (y, id_2) \end{array} \right\} \\ \\ \gamma_{\text{com}}(A^{\sharp}) = \left\{ (u, C) \;\middle|\; \begin{array}{l} \forall(P, id_1, E) \in C, \forall x \in \mathcal{FN}(P), \forall y \in \mathcal{BN}(S) \\ \text{[}\exists id_2, E(x) = (y, id_2)] \implies (x, y) \in A^{\sharp} \end{array} \right\} $$

The second domain counts both the number of occurrences of processes and the number of performed transitions inside computations. We denote by $\Pi$ the set of all sub-processes of $S$. Let $\mathcal{V}$ be the set $\Pi + \Sigma$. We consider $\wp(\mathbb{N}^{\mathcal{V}})$, the complete lattice of the sets of natural number functions defined on $\mathcal{V}$. $\wp(\mathbb{N}^{\mathcal{V}})$ is related to our concrete domain via a Galois connection $(\alpha_{\mathbb{N}^{\mathcal{V}}}, \gamma_{\mathbb{N}^{\mathcal{V}}})$, defined as follows:

$$ \alpha_{\mathbb{N}^{\mathcal{V}}}(A) = \left\{ \left\{ \begin{array}{l} \mathcal{V} \to \mathbb{N} \\ v \in \Pi \mapsto \text{Card}(\{(P, id, E) \in C \mid v = P\}) \\ \lambda \in \Sigma \mapsto |u|_{\lambda} \end{array} \right\} \;\middle|\; (u, C) \in A \right\} \\ \\ \gamma_{\mathbb{N}^{\mathcal{V}}}(A^{\sharp}) = \left\{ (u, C) \;\middle|\; \begin{array}{l} \exists f \in A^{\sharp}, \forall \lambda \in \Sigma, |u|_{\lambda} = f(\lambda), \\ \forall v \in \Pi, \text{Card}(\{(P, id, E) \in C \mid v = P\}) = f(v) \end{array} \right\} $$

The complete lattice, $(\mathcal{N}_{\mathcal{V}}, \sqsubseteq_{\mathcal{N}_{\mathcal{V}}}, \sqcup_{\mathcal{N}_{\mathcal{V}}}, \perp_{\mathcal{N}_{\mathcal{V}}}, \sqcap_{\mathcal{N}_{\mathcal{V}}}, \top_{\mathcal{N}_{\mathcal{V}}})$, left as a parameter of our abstraction, is related to $\wp(\mathbb{N}^{\mathcal{V}})$ by a Galois connection $(\alpha_{\mathcal{N}_{\mathcal{V}}}, \gamma_{\mathcal{N}_{\mathcal{V}}})$ which satisfies the condition: $\gamma_{\mathcal{N}_{\mathcal{V}}}(\perp_{\mathcal{N}_{\mathcal{V}}}) = \emptyset$. We require three abstract primitives which satisfy the following soundness hypotheses:

* required : $\wp(\Pi) \times \mathcal{N}_{\mathcal{V}} \to \mathcal{N}_{\mathcal{V}}$ \\ $\gamma_{\mathcal{N}_{\mathcal{V}}}(v^{\sharp}) \cap \{f \mid f(p) \ge 1, \forall p \in A\} \subseteq \gamma_{\mathcal{N}_{\mathcal{V}}}(\text{required}(A, v^{\sharp}))$

* trans : $\mathcal{N}_{\mathcal{V}} \times \mathbb{N}^{\mathcal{V}} \to \mathcal{N}_{\mathcal{V}}$ \\ $\{x \mapsto f(x) + g(x) \mid g \in \gamma_{\mathcal{N}_{\mathcal{V}}}(v^{\sharp})\} \subseteq \gamma_{\mathcal{N}_{\mathcal{V}}}(\text{trans}(v^{\sharp}, f))$

* $\rho : \mathcal{N}_{\mathcal{V}} \to \mathcal{N}_{\mathcal{V}}$ \\ $\gamma_{\mathcal{N}_{\mathcal{V}}}(v^{\sharp}) \subseteq \gamma_{\mathcal{N}_{\mathcal{V}}}(\rho(v^{\sharp}))$

Roughly speaking, $\rho$ is a reduction, it maps each abstract value to another one which represents the same set but in which properties are easier to establish. Particularly, it will be used for proving that an abstract value represents the empty set. At each abstract computation step, required is used to extract from the abstract value the representation of configurations which simultaneously contain all the processes required by the computation step and trans is used to calculate the representation of the result of the computation step by taking into account newly spawned and destroyed processes.

We define our abstract domain $(C^{\sharp}, \sqsubseteq, \sqcup, \perp, \sqcap, \top)$ as the complete lattice $(\wp(\mathcal{BN}(S)^2) \times \mathcal{N}_{\mathcal{V}})$, where $\sqsubseteq$, $\sqcup$, $\perp$, $\sqcap$ and $\top$ are defined pairwise. $C^{\sharp}$ is related to $\wp(\Sigma^* \times C)$ by a Galois connection $(\alpha, \gamma)$, where $\alpha(A) = \alpha_{\text{com}}(A)$, $[\alpha_{\mathcal{N}_{\mathcal{V}}} \circ \alpha_{\mathbb{N}^{\mathcal{V}}}] (A))$ and $\gamma(A, B) = \gamma_{\text{com}}(A) \cap [\gamma_{\mathbb{N}^{\mathcal{V}}} \circ \gamma_{\mathcal{N}_{\mathcal{V}}}] (B)$. Our abstract semantics is defined by a transition relation $\rightsquigarrow$ on our abstract domain $C^{\sharp}$, given in Figure
3. Soundness hypotheses on abstract primitives ensure the soundness of our abstract transition:

**Proposition 5.1** If $(u, C) \in \gamma(C^\sharp)$ and $C \xrightarrow{\lambda} \bar{C}$, then there exists $\bar{C}^\sharp$ such that $C^\sharp \xrightarrow{\lambda} \bar{C}^\sharp$ and $(u.\lambda, \bar{C}) \in \gamma(\bar{C}^\sharp)$.

As a consequence, the abstract counterpart $\mathbb{F}^\sharp$ of $\mathbb{F}$, defined by

$$ \mathbb{F}^{\sharp}(C^{\sharp}) = (\alpha(\{(\varepsilon, C) \mid C \in \mathcal{C}_0(\mathcal{S})\})) \sqcup C^{\sharp} \sqcup (\sqcup \{\overline{C}^{\sharp} \mid \exists \lambda \in \Sigma, C^{\sharp} \xrightarrow{\lambda} \overline{C}^{\sharp}\}) $$

satisfies the soundness condition $\mathbb{F}(C) \subseteq \gamma(\mathbb{F}^\sharp(\alpha(C)))$. Using Kleene's theorem, we obtain the soundness of our analysis:

**Theorem 5.2** $\text{lf}_{p_0}\mathbb{F} \subseteq \bigcup_{n \in \mathbb{N}} [\gamma \circ \mathbb{F}^{\sharp^n}](\perp)$

Following [6,7], we compute a sound approximation of our abstract semantics by using a widening operator $\nabla : C^\sharp \times C^\sharp \to C^\sharp$ which satisfies the following properties:

* $\forall C_1^\sharp, C_2^\sharp \in C^\sharp, C_1^\sharp \sqcup C_2^\sharp \subseteq C_1^\sharp \nabla C_2^\sharp$

* $(C_n^\sharp) \in (C^\sharp)^N$, the sequence $(C_n^\nabla)$ 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 abstract iteration of $\mathbb{F}^\sharp$ is then defined as follows:

$$ \left\{ \begin{array}{l} \mathbb{F}_0^\nabla = \perp \\ \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{else} \end{cases} \end{array} \right. $$

**Theorem 5.3** Abstract iteration[10,11] Abstract iteration $(\mathbb{F}_n^\nabla)$ is ultimately stationary and its limit $\mathbb{F}^\nabla$ satisfies $\text{Coll}(\mathcal{S}) \subseteq \gamma(\rho(\mathbb{F}^\nabla))$.

# 6 Detecting exhaustion of resources and mutual exclusion

We only need to define an abstract domain to approximate set of tuples of natural numbers, in which abstract primitives can be precisely and efficiently implemented. We reject the use of usual numerical domains: we are unlikely to design a precise primitive required in non-relational domain, without using an exponential partitioning; we think that the domain of linear inequalities among a finite set of variables [12] is too expensive because we deal with too many variables. We propose the use of a product of two domains. The first domain is
Let $(c^{\sharp}, v^{\sharp}) \in C^{\sharp}$, $u \in \mathcal{BN}(S)$, $y^i[y_1, \dots, y_n]P$ and $x!^j[x_1, \dots, x_n]Q$ two sub-processes, $\text{Cont}_? \in \text{Agent}(P)$, $\text{Cont}_! \in \text{Agent}(Q)$, such that:

• $(y, u) \in c^{\sharp}$

• $(x, u) \in c^{\sharp}$

• $V \stackrel{\Delta}{=} \rho(\text{required}(\{y^i[y_1, \dots, y_n]P; x!^j[x_1, \dots, x_n]Q, v^{\sharp}\}) \neq \bot_{\mathcal{N}_V})$

then $(c^{\sharp}, v^{\sharp}) \overset{(i,j)}{\rightleftharpoons} (c'^{\sharp}, v'^{\sharp})$, where

• $c'^{\sharp} = c^{\sharp} \cup \{(y_k, t) \mid k \in [|1; n|], t \in \mathcal{BN}(S) \text{ and } (x_k, t) \in c^{\sharp}\} \cup \{(x, x) \mid \exists p \in \text{Cont}_?, x \in (\mathcal{BN}(P) \cap \mathcal{FN}(p)) \setminus \{y_k \mid k \in [|1; n|]\}\} \cup \{(x, x) \mid \exists q \in \text{Cont}_!, x \in \mathcal{BN}(Q) \cap \mathcal{FN}(q)\}$

• $v'^{\sharp} = \text{trans}(V, \delta)$

with

$$ \forall x \in \Pi, \delta(x) = \begin{cases} -1 & \text{if } x \in \{y^i[y_1, \dots, y_n]P, x!^j[x_1, \dots, x_n]Q\} \setminus (\text{cont}_? \cup \text{cont}_!) \\ +1 & \text{if } x \in (\text{cont}_? \cup \text{cont}_!) \setminus \{y^i[y_1, \dots, y_n]P, x!^j[x_1, \dots, x_n]Q\} \\ 0 & \text{otherwise} \end{cases} $$

$$ \forall \lambda \in \Sigma, \delta(\lambda) = \begin{cases} +1 & \text{if } \lambda = (i, j) \\ 0 & \text{otherwise} \end{cases} $$

(a) Abstract communication

Let $(c^{\sharp}, v^{\sharp}) \in C^{\sharp}$, $u \in \mathcal{BN}(S)$, $*y^i[y_1, \dots, y_n]P$ and $x!^j[x_1, \dots, x_n]Q$ two sub-processes, $\text{Cont}_* \in \text{Agent}(P)$, $\text{Cont}_! \in \text{Agent}(Q)$, such that:

• $(y, u) \in c^{\sharp}$

• $(x, u) \in c^{\sharp}$

• $V \stackrel{\Delta}{=} \rho(\text{required}(\{*y^i[y_1, \dots, y_n]P; x!^j[x_1, \dots, x_n]Q, v^{\sharp}\}) \neq \bot_{\mathcal{N}_V})$

then $(c^{\sharp}, v^{\sharp}) \overset{(i,j)}{\rightleftharpoons} (c'^{\sharp}, v'^{\sharp})$, where

• $c'^{\sharp} = c^{\sharp} \cup \{(y_k, t) \mid k \in [|1; n|], t \in \mathcal{BN}(S) \text{ and } (x_k, t) \in c^{\sharp}\} \cup \{(x, x) \mid \exists p \in \text{Cont}_*, x \in (\mathcal{BN}(P) \cap \mathcal{FN}(p)) \setminus \{y_k \mid k \in [|1; n|]\}\} \cup \{(x, x) \mid \exists q \in \text{Cont}_!, x \in \mathcal{BN}(Q) \cap \mathcal{FN}(q)\}$

• $v'^{\sharp} = \text{trans}(V, \delta)$

$$ \text{with } \forall x \in \Pi, \delta(x) = \begin{cases} -1 & \text{if } x \in \{x!^j[x_1, \dots, x_n]Q\} \setminus \text{cont}_* \\ +1 & \text{if } x \in (\text{cont}_* \cup \text{cont}_!) \setminus \{x!^j[x_1, \dots, x_n]Q\} \\ 0 & \text{otherwise} \end{cases} $$

$$ \text{and } \forall \lambda \in \Sigma, \delta(\lambda) = \begin{cases} +1 & \text{if } \lambda = (i, j) \\ 0 & \text{otherwise} \end{cases} $$

(b) Abstract resource fetching

<caption>Fig. 3. Abstract transition relation</caption>
based on the use of the interval lattice and is used for expressing properties of interest. This domain can represent all the information we need to express 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 [17] and is used for expressing more complex properties, such as mutual exclusion for instance, which allows for more precise calculations in the first domain. The power of our analysis directly follows from an unexpensive algorithm, straightforwardly adapted from Linear Constraint Programming, to calculate an approximated reduction between these two domains.

The complete lattice ($\mathcal{I}_V, \sqsubseteq_{\mathcal{I}_V}, \sqcup_{\mathcal{I}_V}, \perp_{\mathcal{I}_V}, \sqcap_{\mathcal{I}_V}, \top_{\mathcal{I}_V}$) is the functional domain of the natural numbers intervals, where lattice operations are defined point-wise. A family ($\nabla^n_{\mathcal{I}_V}$) of widening operators on $\mathcal{I}_V$ is defined as follows:

$$ [f \nabla^n_{\mathcal{I}_V} g](x) = f(x) \nabla^n g(x) \\ \text{where } \begin{cases} [[a; b]] \nabla^n [[c; d]] = [[\min\{a; c\}; \infty[ & \text{if } d > \max\{b; n\} \\ I \nabla^n J = I \cup J & \text{otherwise} \end{cases} $$

The complete lattice ($\mathcal{K}_V, \sqsubseteq_{\mathcal{K}_V}, \cup_{\mathcal{K}_V}, \top_{\mathcal{K}_V}, \cap_{\mathcal{K}_V}, \perp_{\mathcal{K}_V}$) of linear equality systems between the finite set of variables $V$ is described with its lattice operations in [17]. This domain uses Gauss reduction in order to normalize systems. Moreover, since there are no infinite increasing chain [17], we can choose $\cup_{\mathcal{K}_V}$ as a widening operator. Our numerical domain is then the product $\mathcal{I}_V \times \mathcal{K}_V$. Generic primitives are expressed as follows:

$$ \bullet \textit{ required}(P, (i, s)) = (i', s) \text{ where } \begin{cases} i'(x) = i(x) \cap [[1; +\infty[ & \forall x \in P \\ i'(x) = i(x) & \forall x \in \Pi \setminus P \end{cases} $$

$$ \bullet \textit{ trans} \left( \left( i, \left\{ \sum_{v \in V} a_v^k v = b_k, \forall k \in [[1; m]] \right\} , f \right) = (i', s') \right. $$

$$ \text{where} \begin{cases} i'(x) = \{k + f(x) | \forall k \in i(x)\} \cap [[0; +\infty[ \\ s' = \left\{ \sum_{v \in V} a_v^k (v - f(v)) = b_k, \forall k \in [[1; m]] \right\} \end{cases} $$

We now present a reduction [9] $\rho$ between $\mathcal{I}_V$ and $\mathcal{K}_V$. A reduction consists in taking into account linear constraints in order to narrow the domain of interval variables. 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 Gauss reduction, 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 solving this problem. The first step aims at narrowing infinite intervals into finite ones. It uses Gauss reduction 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, which allows to narrow infinite intervals into finite ones, with a worst-case in $O(n^3)$. 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 for propagating unidirectionnally intervals from non-diagonal to diagonal variables. The result is a good reduction with a worst-case in $O(n^4)$.

We now propose some examples of mobile systems analyzed with our prototype. For the sake of brevity, we have selected for each example a subset of significant constraints captured by our analysis; full results are available in [13]. In these constraints, the number of occurrences of a process $c?^i[x_1, ..., x_n]P$ or $c!^i[x_1, ..., x_n]P$ is denoted by $\#(i)$, while $\#(i, j)$ denotes the number of times a communication reduction labelled with $(i, j)$ is used.

**Example 6.1** Our first example is the ftp protocol proposed in Example 3.1:

$$S := (\nu \text{ port})(\textbf{Allocate } | \text{ port!}^5[] | \text{ port!}^6[] | \text{ port!}^7[]))$$

where

$$\textbf{Allocate} := *\text{port?}^0[] (\nu \text{ in})(\nu \text{ out})(\nu \text{ query}) \\ (\text{in}^1[\text{query}] \\ | \text{in}^2[\text{response}].(\text{out}^3[\text{response}] | \text{port!}^4[]))$$

$$\left\{ \begin{array}{l} \#(0) = 1, \#(i) \in [|0; 3|], \forall i \in \{1; 2; 4\} \\ \#(3) \in [|0; \infty|] \\ \#(i) \in [|0; 1|], \forall i \in [|5; 6; 7|] \\ \#(1) + \#(4) + \#(5) + \#(6) + \#(7) = 3 \\ \#(3) = \underline{\underline{\pi}}(2, 1) \end{array} \right.$$

Our analysis has proved that only three physical channels are required to simulate this protocol. □

**Example 6.2** We now propose an example of mutual exclusion:

$$S := \left( \begin{array}{l} (\nu \text{ a})(\nu \text{ b})(\nu \text{ c})(\nu \text{ d}) \\ (*\text{a}^0[x](x!^1[a] + (c?^2[]d!^3[]))) \\ |*\text{b}^4[x](x!^5[b] + (c!^6[]))) \\ |a!^7[b]) \end{array} \right)$$

$$\left\{ \begin{array}{l} \#(i) \in [|0; 1|], \forall i \in \{1; 2; 5; 6; 7\} \\ \#(3) = 0 \\ \#(1) + \#(2) + \#(5) + \#(6) + \#(7) = 1 \end{array} \right.$$

Our analysis has proved that the sub-process ($d!^3$[]]) is unreachable by detecting a mutual exclusion between the sub-processes ($c?^2$[]d!^3[]]) and ($c!^6$[]]). □
# 7 Detecting deadlocks

We use both our abstraction of the collecting semantics and dynamic partitioning tools [3] to solve the problem of detecting sets of non-standard configurations such that no infinite sequence of computations can pass by them. For that purpose, we analyze the trace semantics of the mobile system $\mathcal{S}$, which is defined as a transition system $(G, A \subseteq G \times G)$ where $G = \text{Coll}(\mathcal{S})$ is the set of states and $A = \{(u, C), \lambda, (u.\lambda, C') \mid (u, C) \in \text{Coll}(\mathcal{S}), C \xrightarrow{\lambda} C'\}$ is the set of transitions. This is also the least fixpoint of an $\cup$-complete endomorphism $\mathbb{F}$ on the complete lattice $(\mathcal{T}, \sqsubseteq_{\mathcal{T}}, \cup_{\mathcal{T}}, \perp_{\mathcal{T}}, \cap_{\mathcal{T}}, \top_{\mathcal{T}})$ of transition systems on the alphabet $\Sigma$, the set of states of which is a subset of the set $(\Sigma^* \times \mathcal{C})$. Lattice operations are the usual set operations, while $\mathbb{F}((G, A))$ is the transition system $(G', A')$ defined as follows:

$$ 
\left\{ 
\begin{array}{l} 
G' = \{(\varepsilon, C) \mid C \in \mathcal{C}_0(\mathcal{S})\} \cup \{(u.\lambda, C) \mid \exists(u, C') \in G, C' \xrightarrow{\lambda} C\} \\ 
A' = \{((u, C), \lambda, (u.\lambda, C')) \mid (u, C) \in G, C \xrightarrow{\lambda} C'\} 
\end{array} 
\right. 
$$

We abstract the trace semantics to compute a finite approximation in a finite time. We approximate infinite transition systems by finitely partitioning their set of states. An abstract transition system is then defined as a transition system on a finite set of states, and a function mapping each state to the set of concrete states it represents. Let $\mathbb{P}$ be a finite subset of the lattice $\wp(\mathbb{N}^\nu)$, such that $\emptyset \notin \mathbb{P}$, $\bigcup \mathbb{P} = \mathbb{N}^\nu$ and $\forall a, a' \in \mathbb{P}, a \neq a' \Rightarrow a \cap a' = \emptyset$. We introduce our abstract domain $\mathcal{T}^\sharp$ as the set of all pairs $((G^\sharp, A^\sharp), f)$ such that $(G^\sharp, A^\sharp)$ is a transition system on the alphabet $\Sigma$, where $G^\sharp$ is the quotient of $\mathbb{P}$ by an equivalence relation and $f$ is a function mapping each element of $G^\sharp$ to an abstract element of $\mathcal{C}^\sharp$. $\mathcal{T}^\sharp$ is partially pre-ordered by the relation $\sqsubseteq_{\mathcal{T}^\sharp}$ where $((\mathbb{P}_{/\sim_1}, A_1^\sharp), f_1) \sqsubseteq_{\mathcal{T}^\sharp} ((\mathbb{P}_{/\sim_2}, A_2^\sharp), f_2)$ if and only:

$$ 
\left\{ 
\begin{array}{l} 
\forall q^\sharp, q'^\sharp \in \mathbb{P}, q^\sharp \sim_1 q'^\sharp \implies q^\sharp \sim_2 q'^\sharp \\ 
\forall q^\sharp \in \mathbb{P}, f_1([q^\sharp]_{\sim_1}) \sqsubseteq f_2([q^\sharp]_{\sim_2}) \\ 
\forall q^\sharp, q'^\sharp \in \mathbb{P}, \forall \lambda \in \Sigma, ([q^\sharp]_{\sim_1}, \lambda, [q'^\sharp]_{\sim_1}) \in A_1^\sharp \implies ([q^\sharp]_{\sim_2}, \lambda, [q'^\sharp]_{\sim_2}) \in A_2^\sharp 
\end{array} 
\right. 
$$

Since there is no canonical choice for the equivalence relation, we are unlikely to define an abstraction function. So, we use a relaxed version of abstract interpretation [10], which only relies on the use of a concretization function
$\gamma_T$ which relates the abstract domain to the concrete one, defined as follows:

$$ \gamma_T((\mathbb{P}_{/\sim}, A^{\sharp}), f) = (G, A) $$
$$ \text{where} \quad \left\{ \begin{array}{@{}l@{}} G = \bigcup_{q^{\sharp} \in \mathbb{P}} [(\gamma(f([q^{\sharp}]_{\sim}))) \cap (\gamma_{\mathbb{N}\nu}(q^{\sharp}))] \\ A = \left\{ (q, \lambda, q') \middle| \exists q^{\sharp}, q'^{\sharp} \in \mathbb{P}, \begin{array}{@{}l@{}} \left\{ \begin{array}{@{}l@{}} q \in (\gamma(f([q^{\sharp}]_{\sim}))) \cap (\gamma_{\mathbb{N}\nu}(q^{\sharp})) \\ q' \in (\gamma(f([q'^{\sharp}]_{\sim}))) \cap (\gamma_{\mathbb{N}\nu}(q'^{\sharp})) \\ ([q^{\sharp}]_{\sim}, \lambda, [q'^{\sharp}]_{\sim}) \in A^{\sharp} \\ q \xrightarrow{\lambda} q' \end{array} \right\} \\ \text{if } (t^{\sharp}, q^{\sharp}) \in \mathbb{P} \text{, if } (t^{\sharp}, q'^{\sharp}) \in \mathbb{P} \end{array} \right\} $$

We give in Figure 4 the definition of both an abstract counterpart $\mathbb{F}^{\sharp}$ of $\mathbb{F}$ and an accelerator of convergence $\mathbb{G}^{\sharp}$. Intuitively, $\mathbb{G}^{\sharp}$ merges the states of the abstract transition system, as soon as we are unable to prove that no infinite derivation can pass by a state they represent. $\mathbb{G}^{\sharp}$ uses a generic primitive relation, denoted by $finite \in \wp(\mathcal{T}^{\sharp} \times \mathbb{P})$, such that for all $t^{\sharp} = ((\mathbb{P}_{/\sim}, A^{\sharp}), f)$ in $\mathcal{T}^{\sharp}$, for all $q_0^{\sharp}$ in $\mathbb{P}$, if $(t^{\sharp}, q_0^{\sharp})$ in $finite$ then all derivations in transition system $\gamma_T(t^{\sharp})$ passing by a configuration $c_0$ in $\gamma(f([q_0^{\sharp}]_{\sim})) \cap \gamma_{\mathbb{N}\nu}(q_0^{\sharp})$ are finite. $\mathbb{F}^{\sharp}$ and $\mathbb{G}^{\sharp}$ satisfy the soundness property: for all $t^{\sharp}$ in $\mathcal{T}^{\sharp}$, $[\mathbb{F} \circ \gamma_T](t^{\sharp}) \subseteq_T [\gamma_T \circ \mathbb{F}^{\sharp} \circ \mathbb{G}^{\sharp}](t^{\sharp})$. Furthermore, the sequence $[\mathbb{F}^{\sharp} \circ \mathbb{G}^{\sharp}]^n((\mathbb{P}, \emptyset), \emptyset)$ is ultimately stationary and, thanks to Theorem 4.1.1.0.2 in [6], its limit $l^{\sharp}$ satisfies $lfp_{\perp_T} \mathbb{F} \subseteq \gamma_T(l^{\sharp})$.

**Theorem 7.1** Let $((\mathbb{P}_{/\sim}, A), f) = l^{\sharp}$. For all $q$ in $\mathbb{P}$, for all $C$ in $\gamma(f([q^{\sharp}]_{\sim})) \cap (\gamma_{\mathbb{N}\nu}(q^{\sharp}))$, there is no infinite computation sequence in the system $S$ which passes by the state $C$ if $(l^{\sharp}, q) \in finite$.

Our last task is to instantiate $\mathbb{P}$ and the primitive finite. A good choice for $\mathbb{P}$ consists in partitioning the set $\mathbb{N}^{\nu}$ in accordance to the values of the variables of $\mathcal{V}$ which have a bounded behavior. For that purpose, we consider $v \subseteq V$ and a family $(M_x)$ in $\mathbb{N}^{\nu}$, such that $\forall f \in \alpha_{\mathbb{N}^{\nu}}(\mathrm{Coll}(S))$, $f(x) \in [|0; M_x|]$. We take $\mathbb{P} = \mathbb{N}^{\nu}_{/\sim}$ where $\sim$ is defined by: $g \sim h$ if and only if $(\forall x \in v, g(x) \in [|0; M_x|] \text{ and } g(x) = h(x)) \text{ or } (\exists x_1, x_2 \in v, g(x_1) > 1 \text{ and } h(x_2) > 1)$. Both $v$ and $(M_x)$ are given by the analysis presented in Section 5. The primitive finite is given by the following algorithm. Let $(t^{\sharp}, f) \in \mathcal{T}^{\sharp}$ and $q_0^{\sharp} \in \mathbb{P}$, we introduce Available $\subseteq \Sigma$ defined by $\lambda \in Available$ if and only if there is a derivation in the transition system $t^{\sharp}$ stemming from $q_0^{\sharp}$ and containing a transition labelled with $\lambda$. The following soundness proposition is valid:

**Proposition 7.2** $\forall \lambda \in \Sigma$, if there is a derivation in the transition system $\gamma_T(t^{\sharp}, f)$ which stems from a configuration in $\gamma(f([q_0^{\sharp}]_{\sim})) \cap (\gamma_{\mathbb{N}\nu}(q_0^{\sharp}))$ and which contains a transition labelled with $\lambda$, then $\lambda \in Available$.

We denote by $\mapsto_2$ the subset of $\dashrightarrow_2$ which only contains the computation steps labelled with an elements of Available. Following [16], we try to build a well-founded set in which we will interpret $(C, \mapsto_2)$ via a morphism. Success in doing this will prove that any derivation in the system $\gamma_T(t^{\sharp}, f)$ which passes by a configuration in $\gamma(f([q_0^{\sharp}]_{\sim})) \cap (\gamma_{\mathbb{N}\nu}(q_0^{\sharp}))$ is finite.
$\mathbb{F}_P^\sharp((\mathbb{P}/\sim, A), f) = ((\mathbb{P}/\sim, A'), f')$ where

$$
\[
\left\{
\begin{array}{@{}l@{\quad}l@{}}
  \left\{
    \begin{array}{@{}l@{}}
      f'(x) = f(x) \nabla h(x) \\
      h(x) = \bigsqcup \left\{
        \begin{array}{@{}l@{}}
          (c^\sharp, v^\sharp \sqcap_{\mathcal{N}_v} \alpha_{\mathcal{N}_v}(u')) \\
          \quad \left|
            \begin{array}{@{}l@{}}
              u' \in x, \quad v^\sharp \sqcap_{\mathcal{N}_v} \alpha_{\mathcal{N}_v}(u') \neq \perp_{\mathcal{N}_v}, \\
              \quad (c^\sharp, v^\sharp) = \alpha(\{(\varepsilon, C) \mid C \in \mathcal{C}_0(S)\}) \\
              \quad \text{or } \exists u \in \mathbb{P}, \exists \lambda \in \Sigma \text{ such that} \\
              \quad \quad f([u]_\sim) \sqcap (\top_{\text{com}}, \alpha_{\mathcal{N}_v}(u)) \overset{\lambda}{\rightsquigarrow} (c^\sharp, v^\sharp)
            \end{array}
          \right\}
        \end{array}
      \right\} & \text{(a) counterpart function} \\
      A' = A \cup \left\{
        \begin{array}{@{}l@{}}
          ([u]_\sim, \lambda, [u']_\sim) \\
          \quad \left|
            \begin{array}{@{}l@{}}
              \exists (c^\sharp, v^\sharp) \in \mathcal{C}^\sharp, \\
              \quad f([u]_\sim) \sqcap (\top_{\text{com}}, \alpha_{\mathcal{N}_v}(u)) \overset{\lambda}{\rightsquigarrow} (c^\sharp, v^\sharp) \\
              \quad v^\sharp \sqcap_{\mathcal{N}_v} \alpha_{\mathcal{N}_v}(u') \neq \perp_{\mathcal{N}_v}
            \end{array}
          \right\}
        \end{array}
      \right\} &
\end{array}
\right.
\]
$$

$$
\begin{array}{l}
\mathbb{G}_P^\sharp((\mathbb{P}/\sim, A), f) = ((\mathbb{P}/\sim', A'), f') \text{ where} \\
\left\{
\begin{array}{@{}l@{\quad}l@{}}
  a \sim' b \iff & a \sim b \text{ or } \{((\mathbb{P}/\sim, A), f), a\); (((\mathbb{P}/\sim, A), f), b)\} \cap \text{finite} = \emptyset \\
  f'([a]_{\sim'}) = & \bigsqcup_{x \in [a]_{\sim'}} f([x]_{\sim}) \\
  A' = & \{([a_0]_{\sim'}, \lambda, [a]_{\sim'}) \mid ([a_0]_{\sim}, \lambda, [a]_{\sim}) \in A\}
\end{array}
\right.
\end{array}
\qquad
\begin{array}{@{}l@{}}
  \text{(b) quotient function} \\
  \text{(a) counterpart function}
\end{array}
$$

<caption>Fig. 4. Abstract trace semantics</caption>

We introduce the relation $\curvearrowright$ between the subprocesses of $S$ such that $\forall p, q \in \Pi, p \curvearrowright q$ if and only if at least one of the following conditions is satisfied:

* $p$ has the particular form $x!^j[]Q, q \in \bigcup Agent(Q)$, and there exists $i \in Lbl$ such that $(i, j) \in Available$;

* $p$ has the particular form $x?^i[]P, q \in \bigcup Agent(P)$, and there exists $j \in Lbl$ such that $(i, j) \in Available$;

* $p$ has the particular form $x!^j[]Q$, and there exists a process of the particular form $*y?^i[]P$ such that $q \in \bigcup Agent(P)$ and $(i, j) \in Available$.

We define the relation *finite* by: $((t^\sharp, f), q_0^\sharp) \in \text{finite} \iff (\Pi, \curvearrowright) \text{ is acyclic.}$

Soundness hypotheses are satisfied since if $(\Pi, \curvearrowright)$ is acyclic, then $(\Pi, \curvearrowright^+)$ is a
well founded order and the multiset extension $[16]$ of $\curvearrowright^+$ gives a well founded
order $\curvearrowright_{\text{Mul}}^+$ on $\mathbb{N}^{\mathbb{N}}$. The function $\Phi: (C, \mapsto_2) \to (\mathbb{N}^{\mathbb{N}}, \curvearrowright_{\text{Mul}}^+)$ defined by
$\Phi(C)(p) = \text{Card}(\{(P, id, E) \in C \mid P = p\})$ is then a morphism.

**Example 7.3** We propose to analyze the following mobile system:

$$
\begin{array}{l}
S := (\nu \text{ push})(\nu \text{ pop}) \\
\qquad ((*\text{push}^1[]((\text{pop}^2[] | \text{push}^3[]))) | *\text{pop}^4[] | *\text{push}^5[] | \text{push}^6[]))
\end{array}
$$

This system describes the behavior of a stack. The height of the stack is
symbolized by the number of processes pop!²[] that occurs at the top level.
Push (resp. pop) operations are symbolized by communication with the resource *push?¹[]* (resp. *pop?⁴[]*). Finally, a communication with the resource *push?⁵[]* symbolizes that further push operations are no longer allowed.

Occurrence counting analysis gives the following properties:

$$ 
\left\{ 
\begin{array}{l}
\pi(1) = 1, \pi(2) \in [|0; +\infty|[, \pi(3) \in [|0; 1|], \\
\pi(4) = 1, \pi(5) = 1, \pi(6) \in [|0; 1|], \\
\underline{\pi}(1, 6) \in [|0; 1|], \underline{\pi}(5, 3) \in [|0; 1|], \underline{\pi}(5, 6) \in [|0; 1|], \\
\underline{\pi}(1, 3) \in [|0; \infty|[, \underline{\pi}(4, 2) \in [|0; \infty|[.
\end{array}
\right. 
$$

We denote by $v \subseteq \mathcal{V}$ the set of variables $\{\text{push}!^3[]; \text{push}!^6[]; (1, 6); (5, 3); (5, 6)\}$ and we take $\mathbb{P} = \mathbb{N}^\nu/\sim$ where $g \sim h$ if and only if $(\forall x \in v, g(x) \in [|0; 1|] \text{ and } g(x) = h(x)) \text{ or } (\exists x_1, x_2 \in v, g(x_1) > 1 \text{ and } h(x_2) > 1)$.

Our deadlock analysis then gives the abstract transition system $(t^\#; f)$ where $t^\#$ is given as follows:

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

By applying our primitive relation *finite*, we prove that no infinite computation sequence can pass by a configuration in $\gamma_{\mathbb{N}^\nu}(q_1) \cup \gamma_{\mathbb{N}^\nu}(q_2)$, which means that executions of our system are bound to terminate as soon as a communication (5, 3) or a communication (5, 6) is performed. $\square$

# 8 Conclusion

We have designed a powerful framework to prove properties on the potential behavior of a mobile system. Our analysis allows to detect, in polynomial time on the number of sub-processes of the mobile system, mutual exclusion and non-exhaustion of resources. Our analysis has succeeded in analyzing very quickly a few nested concrete systems, featuring unbounded communication topologies, with the expected level of accuracy. Deadlock detection is a much more difficult problem and our proposed approach is likely to require exponential time. However it gives interesting results on unbounded systems, which are out of reach of model checking methods. We are likely to refine our initial partitioning in order to get a quicker analysis.

This framework is likely to be enriched by using [14] in order to detect non-uniform confidentiality properties between processes, and to allow the analysis of mobile systems in hostile context. This will lead to a very powerful modular
analysis for mobile systems. To scale up, for large nested mobile systems, the
analysis must be more approximate to ensure short execution time.

Acknowledgement

We deeply thank anonymous referees for their significant comments on an
early version. We wish also thank Patrick and Radhia Cousot, Arnaud Venet,
Jorge Pinto and Antoine Miné, for their comments and discussions.

References

[1] G. Berry and G. Boudol. The chemical abstract machine. *Theoretical Computer Science*, 96:217-248, 1992.

[2] C. Bodei, P. Degano, F. Nielson, and H.R Nielson. Control flow analysis for the π-calculus. In *Proceedings of CONCUR '98*, Lecture Notes in Computer Science. Springer-Verlag, 1998.

[3] F. Bourdoncle. Abstract interpretation by dynamic partitioning. *Journal of Functional Programming*, 2(4), 1992.

[4] L. Cardelli and A. D. Gordon. Mobile ambients. In *Foundations of Software Science and Computational Structures*, volume 1378 of *Lecture Notes in Computer Science*, pages 140–155. Springer, 1998.

[5] C.K. Chiu and J.H.M. Lee. Interval linear constraint solving using the preconditioned interval gaus-seidel method. In *Proceedings of the Twelfth International Conference on Logic Programming*, Logic Programming, pages 17–32. The MIT Press, 1995.

[6] P. Cousot. *Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique des programmes*. PhD thesis, Université Scientifique et Médicale de Grenoble, 1978.

[7] P. Cousot. Semantic foundations of program analysis. In S.S. Muchnick and N.D. Jones, editors, *Program Flow Analysis: Theory and Applications*, chapter 10, pages 303–342. Prentice-Hall, Inc., Englewood Cliffs, 1981.

[8] P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In *Conference Record of the Fourth ACM Symposium on Principles of Programming Languages*, pages 238–252, Los Angeles, California, U.S.A., 1977.

[9] P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In *Proceedings of the Sixth Conference on Principles of Programming Languages POPL '79*. ACM Press, 1979.

[10] P. Cousot and R. Cousot. Abstract interpretation frameworks. *Journal of logic and computation*, 2(4):511–547, August 1992.
[11] P. Cousot and R. Cousot. Comparing the Galois connection and widening-narrowing approaches to abstract interpretation. In *Programming Language Implementation and Logic Programming, Proceedings of the Fourth International Symposium, PLILP'92*, volume 631 of *Lecture Notes in Computer Science*, pages 269-295. Springer-Verlag, 1992.

[12] P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In *Proceedings of the Fifth Conference on Principles of Programming Languages*. ACM Press, 1978.

[13] J. Feret. Conception de π-sa : un analyseur statique générique pour le π-calcul. Mémoire de dea, SPP, september 1999. Electronically available at http://www.di.ens.fr/~feret/dea/dea.ps.

[14] J. Feret. Confidentiality analysis of mobile systems. In *Seventh International Static Analysis Symposium (SAS'00)*, volume 1824 of *LNCS*. Springer-Verlag, 2000.

[15] R. R. Hansen, J. G. Jensen, F. Nielson, and H. R. Nielson. Abstract interpretation of mobile ambients. In *Proc. SAS'99*, number 1694 in Lecture Notes in Computer Science, pages 134-148. Springer-Verlag, 1999.

[16] Jean-Pierre Jouannaud. Rewrite proofs and computations. In Helmut Schwichtenberg, editor, *Proof and Computation*, volume 139 of *Computer and Systems Sciences*, pages 173-218. Springer-Verlag, 1995.

[17] M. Karr. Affine relationships among variables of a program. *Acta Informatica*, pages 133-151, 1976.

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

[19] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes. *Information and Computation*, 100:1-77, 1992.

[20] H. Riis Nielson and F. Nielson. Shape analysis for mobile ambients. In *Proc. POPL'00*, pages 142-154. ACM Press, 2000.

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

[22] A. Venet. Abstract interpretation of the π-calculus. In *Proc. of the Fifth LOMAPS Workshop on Analysis and Verification of High-Level Concurrent Languages*, volume 1192 of *Lecture Notes in Computer Science*, pages 51-75. Springer-Verlag, 1996.

[23] A. Venet. Automatic determination of communication topologies in mobile systems. In *Proceedings of the Fifth International Static Analysis Symposium SAS'98*, volume 1503 of *Lecture Notes in Computer Science*, pages 152-167. Springer-Verlag, 1998.