# Dependency analysis of Mobile Systems

Jérôme Feret

► To cite this version:

Jérôme Feret. Dependency analysis of Mobile Systems. the European Symposium on Programming (ESOP'02), Apr 2002, Grenoble, France. pp.314–330, 10.1007/3-540-45927-8_22. inria-00527924

HAL Id: inria-00527924

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

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
# Dependency Analysis of Mobile Systems*

Jérôme Feret

jerome.feret@ens.fr

Département d'Informatique de l'École Normale Supérieure
ENS-DI, 45, rue d'Ulm, 75230 PARIS Cedex 5, FRANCE

http://www.di.ens.fr/~feret

**Abstract.** We propose an Abstract Interpretation-based static analysis for automatically detecting the dependencies between the names linked to the agents of a mobile system. We focus our study on the mobile systems written in the π-calculus. We first refine the standard semantics in order to restore the relation between the names and the agents that have declared them. We then abstract the dependency relations that are always satisfied by the names of the agents of a mobile system. That is to say we will detect which names are always pair-wisely equal, and which names have necessarily been declared by the same recursive instance of an agent.

## 1 Introduction

We are interested in analyzing automatically the behaviour of mobile systems of agents. Agent distribution in such systems may dynamically change during the computation sequences, which makes their analysis difficult. We address the problem of proving non-uniform properties about the interactions between the agents of a mobile system; such properties allow distinguishing between several recursive instances of a same agent. We especially intend to infer the dependency relations between the names communicated to each agent. This means that we will calculate whether they are pair-wisely equal (and / or) whether they have been pair-wisely declared by the same recursive instance of an agent.

**Previous works.** In previous articles [7,8], we proposed several analyses for mobile systems expressed in the π-calculus. In [7], we already proposed a non-uniform abstraction of the interactions between the agents of a mobile system. This analysis takes into account the dynamic creation of both names and agents, which is an inherent feature of mobility: it assigns a unique marker to each agent instance and stamps each channel with the marker of the agent instance which has declared it. Group creation [3] allows proving that a channel name is confined inside the scope of a given recursive instance, but it can only infer equality or disequality constraints between the groups, and cannot prove any equality constraint by composing disequality constraints. In [7], the algebraic

<footnote>* This work was supported by the RTD project IST-1999-20527 "DAEDALUS" of the European FP5 programme.</footnote>
properties of markers allow handling more complex properties: we can prove that a channel name is first sent to the next instance and then returned to the previous one; thus, we prove it is returned to the instance which has declared it.

**Contribution.** The main two drawbacks of [7] are that the properties it captures are very low level and are not easily understandable, and that the only calculated properties are those which involve a comparison between the marker of a channel name and the marker of the agent it is communicated to.

We propose here a more abstract parametric analysis which handles a wider class of properties. It can especially express some relations between names, even if there is no relation between their markers and the marker of the agent instance they are communicated to. Nevertheless, this raises some complexity problems we propose to solve by designing several domains: there is then a trade-off between information partitioning, and the accuracy of information propagation. Reduced product makes these domains collaborate. At this point, [7] can be seen as a particular instantiation of the parametric domain. We also propose two particular domains that aim at discovering and propagating explicit equality and disequality relations among channel names and among markers.

We briefly present, in Sect. 2, the standard semantics of the π-calculus. We recall the non-standard semantics of [7] in Sect. 3 and derive a new generic abstraction of it in Sect. 4. We design some domains in Sect. 5 and describe outlines for reduction in Sect. 6.

## 2 π-calculus

The π-calculus is a formalism well-fitted for describing the behaviour of mobile systems. It is based on the notion of name passing. We use a lazy synchronous version of the π-calculus which is inspired from [11,1]. Let $\mathcal{N}$ be an infinite set of channel names; agents are built according to the following syntax:

$$ P, Q ::= \mathbf{0} \mid \text{action}.P \mid (P \mid Q) \mid (P + Q) \mid (\nu x)P \mid [x \diamond y]P \\ \text{action} ::= c![\bar{x}] \mid c?[\bar{x}] \mid *c?[\bar{x}] $$

where $c, x, y \in \mathcal{N}$, $\bar{x}$ is a tuple of channel names, and $\diamond \in \{=; \neq\}$. Input guards, replication guards and name restrictions are the only name binders, i.e, in $c? [x_1, ..., x_n]P, *d? [y_1, ..., y_n]Q$ and $(\nu x)R$, occurrences of $x_1, ..., x_n$ in $P$, $y_1, ..., y_p$ in $Q$ and $x$ in $R$ are said to be bound. Usual rules about scoping, substitution and $\alpha$-conversion apply. We denote by $fn(P)$ the set of the free names of $P$, i.e, the names which are not under the scope of any binder, and by $bn(P)$ the set of the bound names of $P$. The agent $P \mid Q$ denotes the parallel composition of two agents $P$ and $Q$ which performs $P$ and $Q$ simultaneously. The agent $P + Q$ denotes a non-deterministic choice between two agents $P$ and $Q$ which performs either $P$ or $Q$: the choice is internal and does not depend on the other agents. $[x \diamond y]P$ denotes a matching guard: the agent $P$ can be activated if the guard $[x \diamond y]$ is satisfied and it does not require that the agent $P$ interacts with another agent of the system. We use a lazy version of replication: the agent $*c? [\bar{x}]P$ duplicates itself each time it communicates with another agent.
*Example 1.* We use, as an illustration, the following system $\mathcal{S}$ [12] throughout the paper:<fnref n="1" />

$$ \mathbf{Next} ::= *make?^0[\mathit{last}](\nu \mathit{next})(\mathit{edge}!^1[\mathit{last}; \mathit{next}] | \mathit{make}!^2[\mathit{next}]) $$

$$ \mathbf{Last} ::= \mathit{make}^?^3[\mathit{last}].\mathit{edge}!^4[\mathit{last}; \mathit{first}] $$

$$ \mathbf{Test} ::= \mathit{edge}^?^5[x; y].[x =^6 y][x \neq^7 \mathit{first}]\mathit{ok}!^8[] $$

$$ \mathcal{S} ::= (\nu \mathit{make})(\nu \mathit{edge})(\nu \mathit{first})(\nu \mathit{ok})(\mathbf{Next} | \mathbf{Last} | \mathbf{Test} | \mathit{make}!^9[\mathit{first}]). $$

The system $\mathcal{S}$ creates a communication ring between several monitors. Each channel name created by the restrictions ($\nu$ first) and ($\nu$ next) denotes a monitor. The message edge![x; y] represents a connection between the monitors respectively denoted by x and y. The first monitor is created by the restriction ($\nu$ first). The resource Next can then be used to connect the last created monitor with a newly created one. The thread Last is used to connect the last created monitor with the first one. The thread Test is used to test whether a monitor is linked with itself and, in such a case, whether it is not the first monitor. We intend to prove that the first matching pattern of Test may be satisfied, although the second matching pattern can never be satisfied. This result is out of the range of any uniform analysis [2] which can give no more accurate result than the fact that monitors can be linked to each other. □

## 3 Non-standard Semantics

We refine the standard semantics in order to explicitly specify the link between channel names and the agent recursive instances that have declared them: we assign to each instance of an agent an unambiguous marker, and stamp each channel name with the marker of the instance of the agent which has declared it. We consider a closed mobile system $\mathcal{S}$ in the $\pi$-calculus, we may assume, without any loss of generality, that no one name occurs twice as an argument of an input guard, a replication guard or a name restriction. Let $\mathcal{L}$ be an infinite set of labels. We locate each syntactic component of $\mathcal{S}$ by labeling each action and each matching pattern with a distinct label. We describe each configuration of $\mathcal{S}$ by a set of thread instances. Each thread instance is a triplet composed of a syntactic component which, for the sake of simplicity, will often be denoted by its label, an unambiguous marker and an environment which specifies the semantic values of the syntactic channel names of the thread. An environment assigns to each syntactic channel name a pair composed of a channel name a and a thread marker id, meaning that the channel name has been declared by the name restriction ($\nu$ a) of a thread the marker of which was id.

Thread instances are created at the beginning of the system computation and when agents interact. In both cases, several threads are spawned, in accordance to which non-deterministic choices are made. The function $\beta$, defined below, applied to a labeled agent, its marker and its environment, returns the set of all possible combination sets of spawned thread instances:

<footnote n="1">¹ We have labeled each syntactic component, as explained in Sect. 3.</footnote>
$$ \beta((\nu n)P, id, E) = \beta(P, id, (E[n \mapsto (n, id)])) $$

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

$$ \beta(P + 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(\text{action.P}, id, E) = \{((\text{action.P}, id, E_{|\text{fn}(\text{action.P})}))\} $$

$$ \beta([x \diamond^i y]P, id, E) = \{([x \diamond^i y]P, id, E_{|\text{fn}([x \diamond^i y]P)})\} $$

Markers are the history of the resource duplications which have led to the creation of the agent instances: they are binary trees the nodes of which are labeled with a pair of labels, and the leaves of which are unlabeled ($\epsilon$). The markers of initial threads are $\epsilon$, while new thread markers are calculated as follows: when a computation step does not involve fetching a resource, markers of computed threads are just passed to the threads of their continuations; when a resource is fetched, the marker of the new threads created from the continuation of the resource is $N((i, j), id_*, id_1)$ where i and id_* are the label and the marker of the resource, j and id_1 are the label and the marker of the message sender.

The set of initial configurations and the computation rules are given in Fig. 1. Standard and non-standard semantics are in bisimulation, provided that we restrict ourselves to the set of standard computations where all non-deterministic choices are made before other computation steps.

**Example 2.** Here is the non-standard configuration for our mobile system $\mathcal{S}$, reached after having replicated the resource **Next** twice, and after having made the last spawned agent labeled by 1 communicated with the thread **Test**:

$$ \left\{ \begin{array}{l} \left( \begin{array}{l} 0, \epsilon, \begin{cases} \text{make} \to (\text{make}, \epsilon) \\ \text{edge} \to (\text{edge}, \epsilon) \end{cases} \end{array} \right) \\ \left( \begin{array}{l} 1, id_1, \begin{cases} \text{edge} \to (\text{edge}, \epsilon) \\ \text{last} \to (\text{first}, \epsilon) \\ \text{next} \to (\text{next}, id_1) \end{cases} \end{array} \right) \\ \left( \begin{array}{l} 2, id_2, \begin{cases} \text{make} \to (\text{make}, \epsilon) \\ \text{next} \to (\text{next}, id_2) \end{cases} \end{array} \right) \\ \left( \begin{array}{l} 3, \epsilon, \begin{cases} \text{make} \to (\text{make}, \epsilon) \\ \text{edge} \to (\text{edge}, \epsilon) \\ \text{first} \to (\text{first}, \epsilon) \end{cases} \end{array} \right) \\ \left( \begin{array}{l} 6, \epsilon, \begin{cases} x \to (\text{next}, id_1) \\ y \to (\text{next}, id_2) \\ \text{first} \to (\text{first}, \epsilon) \\ \text{ok} \to (\text{ok}, \epsilon) \end{cases} \end{array} \right) \end{array} \right. \quad \text{where} \quad \begin{cases} id_1 = N((0, 9), \epsilon, \epsilon) \\ id_2 = N((0, 2), \epsilon, id_1) \end{cases} $$

It turns out that there is no generic relation between the marker of the agent **6** and the markers of the names linked to the variables **x** and **y**, so both [12,7] will fail to prove that the second matching pattern is not satisfiable. □

Moreover, in accordance with the following proposition, we can simplify the shape of the markers without losing marker allocation consistency which ensures
$$C_0(S) = \beta(S, \varepsilon, \emptyset)$$

(a) Non-standard initial configurations.

$$\frac{E_?(y) = E_!(x), \mathit{Cont}_P \in \beta(P, id_?, E_?_{[y_i \mapsto E_!(x_i)]}), \mathit{Cont}_Q \in \beta(Q, id_!, E_!)}{C \cup \{(y?^i[y]P, id_?, E?); (x!^j[\bar{x}]Q, id_!, E_! )\} \to (C \cup \mathit{Cont}_P \cup \mathit{Cont}_Q)}$$

$$\frac{E_*(y) = E_!(x), \mathit{Cont}_P \in \beta(P, N((i, j), id_*, id_!), E_*_{[y_i \mapsto E_!(x_i)]}), \mathit{Cont}_Q \in \beta(Q, id_!, E_!)}{C \cup \left\{ \begin{array}{l} (*y?^i[y]P, id_*, E_*); \\ (x!^j[\bar{x}]Q, id_!, E_! ) \end{array} \right\} \to (C \cup \{ (*y?^i[y]P, id_*, E_*) \} \cup \mathit{Cont}_P \cup \mathit{Cont}_Q)$$

$$\frac{E(x) \diamond E(y), \mathit{Cont}_P \in \beta(P, id, E)}{C \cup \{([x \diamond^i y]P, id, E)\} \to C \cup \mathit{Cont}_P}$$

(b) Non-standard transition system.

**Fig. 1.** Non-standard semantics.

that no one marker can be assigned twice to the same syntactic agent during a computation sequence.

**Proposition 1.** Let $\phi_1$ and $\phi_2$ be the two following functions:

$$\phi_1: \left\{ \begin{array}{rcl} \mathrm{Id} & \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} \mathrm{Id} & \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 with 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.

# 4 Abstract Semantics

We denote by $\mathrm{Id}$ the set of all markers, by $\mathcal{E}(V)$ the set of all environments over the set of syntactic names $V$, by $\Sigma$ the set $\mathcal{L}^2$ and by $\mathcal{C}$ the set of all non-standard configurations. We are actually interested in $\mathcal{C}(S)$, the set of all the configurations a system $S$ may take during any finite sequence of computation steps. This is the *collecting semantics* [4], which can be expressed as the least fix point of the following $\cup$-complete endomorphism $\mathbb{F}$ on the complete lattice $\wp(\mathcal{C})$:

$$\mathbb{F}(X) = \beta(S, \varepsilon, \emptyset) \cup \{\bar{C} \in \mathcal{C} \mid \exists C \in X, C \to \bar{C}\}.$$
The least fix point of such an endomorphism is usually not decidable, so we use a relaxed version of the Abstract Interpretation framework [5] to compute a sound—but not necessary complete—approximation of it.

We assume we are given a family ($G_V$, $\sqsubseteq_V$, $\sqcup_V$, $\perp_V$)$_{V \subseteq bn(S)}$ of abstract domains of properties. For each $V \subseteq bn(S)$, $G_V$ is used for globally abstracting the marker and the environment of a thread instance that uses the set of free names $V$. The relation $\sqsubseteq_V$ is a pre-order which describes the relative amount of information between those properties. Each abstract property is related to $\wp(Id \times \mathcal{E}(V))$ by a monotonic concretization function $\gamma_V$. The operator $\sqcup_V$ maps each finite set of properties to a weaker property: for each finite $A \subseteq G_V$, $\forall a \in A$, $a \sqsubseteq_V (\sqcup_V A)$. $\perp_V$ is the least element in $G_V$ with respect to $\sqsubseteq_V$. We assume that $\gamma_V$ is strict, that is to say, $\gamma_V(\perp_V) = \emptyset$. Then, our main abstract domain ($C^\#$, $\sqsubseteq^\#$, $\sqcup^\#$, $\perp^\#$) is the set of functions mapping each syntactic component $P$ of $S$ to an element of $G_{fn(P)}$. The domain structure ($\sqsubseteq^\#$, $\sqcup^\#$ and $\perp^\#$) is defined pointwise. The abstract domain $C^\#$ is related to $\wp(C)$ by the concretization function $\gamma$ that maps each abstract property $f \in C^\#$ to the set of configurations $C \in C$ such that $\forall (p, id, E) \in C$, $(id, E) \in \gamma_{fn(p)}(f(p))$.

During a communication or resource fetching step, we have to describe the relations among the markers and the environments of two threads: a message receiver and a message sender. For that purpose, we also assume that we are given a family ($G_{V_?}^{V_?}$) of abstract properties$^2$. For any $V_?, V_! \in \wp(bn(S))$, each property in $G_{V_?}^{V_?}$ is related by a concretization function $\gamma_{V_?}^{V_?}$ to the elements of $\wp((Id \times \mathcal{E}(V_?)) \times (Id \times \mathcal{E}(V_!)))$ which satisfy this property.

Let $V$, $V_?$ and $V_!$ be three parts of $bn(S)$. We now introduce some primitives to handle elements in $G_V$ and $G_{V_?}^{V_?}$, and to relate $G_{V_?}$ and $G_{V_!}$ to $G_{V_?}^{V_?}$:

- initial environment abstraction: $\varepsilon_\emptyset \in G_\emptyset$ satisfies $\{(\varepsilon, \emptyset)\} \subseteq \gamma_\emptyset(\varepsilon_\emptyset)$;

- abstract restriction: $\forall x \in bn(S) \setminus V$, $\nu_x : G_V \to G_{V \cup \{x\}}$ satisfies:

$$ \left\{ (id, E) \in Id \times \mathcal{E}(V \cup \{x\}) \mid \left. \begin{array}{l} (id, E|_V) \in \gamma_V(A), \\ E(x) = (x, id) \end{array} \right\} \subseteq \gamma_{V \cup \{x\}}(\nu_x(A)); $$

- abstract extension: $\forall X \subseteq bn(S) \setminus V$, $new_X^\top : G_V \to G_{V \cup X}$ satisfies:

$$ \{(id, E) \in Id \times \mathcal{E}(V \cup X) \mid (id, E|_V) \in \gamma_V(A)\} \subseteq \gamma_{V \cup X}(new_X^\top(A)); $$

- abstract garbage collection: $\forall X \subseteq V$, $gc_X : G_V \to G_X$ satisfies:

$$ \{(id, E|_X) \in Id \times \mathcal{E}(X) \mid (id, E) \in \gamma_V(A)\} \subseteq \gamma_X(X); $$

- abstract matching: match : $((V \times \{=; \ne\} \times V) \times G_V) \to G_V$ satisfies:

$$ \{(id, E) \in Id \times \mathcal{E}(V) \mid (id, E) \in \gamma_V(A), E(x) \diamond E(y)\} \subseteq \gamma_V(match(x \diamond y, A)). $$

- abstract product: $\bullet : G_{V_?} \times G_{V_!} \to G_{V_?}^{V_?}$ satisfies:

$$ \gamma_{V_?}(A?) \times \gamma_{V_!}(A!) \subseteq \gamma_{V_?}^{V_?}(A? \bullet A!); $$

- abstract projections: $fst^\# : G_{V_?}^{V_?} \to G_{V_?}$ and $snd^\# : G_{V_?}^{V_?} \to V_!$ satisfy:

$$ \text{fst}(\gamma_{V_?}^{V_?}(A)) \subseteq \gamma_{V_?}(\text{fst}^\#(A)) \text{ and } \text{snd}(\gamma_{V_?}^{V_?}(A)) \subseteq \gamma_{V_?}(\text{snd}^\#(A)); $$

- abstract synchronization: sync : $\wp(V_? \times V_!) \times G_{V_?}^{V_?} \to G_{V_?}^{V_?}$ satisfies:

$$ \{(((id, E_?), (id_!, E_!)) \in \gamma_{V_?}^{V_?}(A) | \forall (a, b) \in S, E_?(a) = E_!(b)\} \subseteq \gamma_{V_?}^{V_?}(sync(S, A)); $$

<footnote>$^2$ The abstract domain $G_{V_?}^{V_?}$ is not assumed to be a pre-order, because it is only used to make intermediary calculi, and not to make iterations.</footnote>
- abstract marker allocation: fetch : $\mathcal{L}^2 \times \mathcal{G}_{V_?}^{V_1} \to \mathcal{G}_{V_?}^{V_1}$ satisfies:

$$ \left\{ \left( (id_*, E_?), (id_!, E_!)(id_?, E_?) \mid ((id_?, E_?), (id_!, E_!)) \in \gamma_{V_?}^{V_1}(A) \mid id_* = N((i, j), id_?, id_! ) \right) \right\} \subseteq \gamma_{V_?}^{V_1}(fetch((i, j), A)). $$

The abstract semantics is then given by an initial abstract element $C_0^\#(S) \in C^\#$ and an abstract transition relation $\dashrightarrow^\#$ in Fig. 2. Their definitions use the following abstract extraction function:

$$ \begin{align*} \beta^\#((\nu n)P, A) &= \beta^\#(P, \nu_n(A)) \\ \beta^\#(\mathbf{0}, A) &= \bot^\# \\ \beta^\#(P + Q, A) &= \bigsqcup^\# \{\beta^\#(P, A); \beta^\#(Q, A)\} \\ \beta^\#(P | Q, A) &= \bigsqcup^\# \{\beta^\#(P, A); \beta^\#(Q, A)\} \\ \beta^\#(action.P, A) &= \{action.P \mapsto gc_{fn(action.P)}(A)\} \\ \beta^\#([x \diamond^i y]P, A) &= \{[x \diamond^i y]P \mapsto gc_{fn([x \diamond^i y]P)}(A)\} \end{align*} $$

$$ C_0^\#(S) = \beta^\#(S, \varepsilon_\emptyset) $$

(a) Abstract initial configuration.

$$ \frac{\left\{ \begin{array}{l} \lambda = y^{?i}[\bar{y}]P, \mu = x^{!j}[\bar{x}]Q, \\ E_s = \text{syn}_x^y \left( \begin{array}{cc} C^\#(\lambda) & \leftarrow C^\#(\mu) \\ \bar{y} & \rightarrow \bar{x} \end{array} \right) \end{array} \right.}{C^\# \dashrightarrow^\# \bigsqcup^\# \{C^\#; \beta^\#(P, \text{fst}^\#(E_s)); \beta^\#(Q, \text{snd}^\#(E_s))\}} \\ \\ \frac{\left\{ \begin{array}{l} \lambda = *y^{?i}[\bar{y}]P, \mu = x^{!j}[\bar{x}]Q, \\ E_s = \text{fetch} \left( (i, j), \left( \text{syn}_x^y \left( \begin{array}{cc} C^\#(\lambda) & \leftarrow C^\#(\mu) \\ \bar{y} & \rightarrow \bar{x} \end{array} \right) \right) \right) \end{array} \right.}{C^\# \dashrightarrow^\# \bigsqcup^\# \{C^\#; \beta^\#(P, \text{fst}^\#(E_s)); \beta^\#(Q, \text{snd}^\#(E_s))\}} \\ \\ \frac{\diamond \in \{=; \neq\}, \lambda = [x \diamond^i y]P}{C^\# \dashrightarrow^\# \bigsqcup^\# \{C^\#; \beta^\#(P, \text{match}(x \diamond y, C^\#))\}} $$

(b) Abstract transition system.

<caption>Fig. 2. Abstract semantics.</caption>

Furthermore, abstract communication and resource fetching require the following synchronization function, which merges the abstract environments of two communicating syntactic components, and mimics the communication of a part of the sender environment.

$$ \text{syn}_x^y \left( \begin{array}{cc} A_? & \leftarrow A_! \\ \bar{y} & \rightarrow \bar{x} \end{array} \right) = \text{sync} \left( \left\{ (y; x) \right\} \cup \left( \bigcup \left\{ (y_i; x_i) \right\} \right), \left( \text{new}_{\{y_1; \dots; y_n\}}^{\top}(A_?) \right) \bullet A_! \right) $$
**Theorem 1.** $C_0^\sharp$ and $\to_\sharp$ satisfy the following soundness property:

1. $C_0(S) \subseteq \gamma(C_0^\sharp(S));$

2. $\forall C^\sharp \in C^\sharp, \forall C \in \gamma(C^\sharp), \forall \bar{C} \in C, C \to \bar{C} \implies \exists \bar{C}^\sharp \in C^\sharp, \begin{cases} C^\sharp \to_\sharp \bar{C}^\sharp \\ \bar{C} \in \gamma(C^\sharp). \end{cases}$

So, the abstract counterpart $\mathbb{F}^\sharp$ to $\mathbb{F}$ defined by:

$$ \mathbb{F}^\sharp(C^\sharp) = \bigsqcup^\sharp (\{C_0^\sharp(S)\} \cup \{\bar{C}^\sharp \mid C^\sharp \to_\sharp \bar{C}^\sharp\}) $$

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

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

A widening operator [6] may be then used to compute a sound and decidable approximation of the abstract semantics.

# 5 Analyses

We propose in this section five abstract domains of properties. The first two domains describe properties of interest which can directly be understood by the user. The last three domains represent complex properties which are used to complete the two first domains by reduction.

## 5.1 Dependencies Among Agent Names

### 5.1.1 Abstract Domain of Equality and Disequality Relations

We introduce an abstract domain for describing equality and disequality relations among a finite set of variables. Let $\mathcal{V}$ be a set of variables, we introduce for all finite subsets of $V \subseteq \mathcal{V}$ the abstract domain $T_V$ of all non-oriented graphs $(G, R)$ such that $G$ is a partition of $V$. Given a finite subset $V$ of $\mathcal{V}$ and $X = (G, R) \in T_V$, we introduce two binary relations over $V$ as follows:

$$ - a =_X b \overset{\Delta}{\iff} \exists \mathcal{X} \in G, \{a, b\} \subseteq \mathcal{X}, $$

$$ - a \neq_X b \overset{\Delta}{\iff} \exists \mathcal{X} \in G, \exists \mathcal{Y} \in G, a \in \mathcal{X}, b \in \mathcal{Y}, (\mathcal{X}, \mathcal{Y}) \in R. $$

The domain $T_V$ is partially ordered by the $\leq_V$ relation defined as follows:

$$ \forall X, Y \in T_V, X \leq_V Y \overset{\Delta}{\iff} \begin{cases} \forall x, y \in V, x =_Y y \Rightarrow x =_X y \\ \forall x, y \in V, x \neq_Y y \Rightarrow x \neq_X y. \end{cases} $$
For every set $I$, each element $A$ in $T_V$ is related to the set of functions $\gamma_V^I(A)$, defined as follows:

$$ \gamma_V^I(A) = \left\{ f \in \mathcal{F}(V, I) \mid \forall x, y \in V, \begin{cases} x =_A y \implies f(x) = f(y) \\ x \neq_A y \implies f(x) \neq f(y) \end{cases} \right\}. $$

We also define some primitives over our abstract domain as follows: let $(G_X, R_X)$ be an element in $T_V$,

- given $(G_Y, R_Y) \in T_V$, $(G_X, R_X) \unlhd (G_Y, R_Y) = (G', R') \in T_V$ where

• $G' = \{x \cap y \mid x \in G_X, y \in G_Y, x \cap y \neq \emptyset\}$

• $R' = \{(x_1 \cap y_1, x_2 \cap y_2) \in (G')^2 \mid (x_1, x_2) \in R_X \text{ and } (y_1, y_2) \in R_Y\}$

- given $V' \subseteq V \setminus V$, and $(G_Y, A_Y) \in T_{V'}$, $(G_X, A_X) \oplus (G_Y, A_Y) \in T_{V \cup V'}$, and $((G_X, A_X) \oplus (G_Y, A_Y)) = (G_X \cup G_Y, A_X \cup A_Y)$;

- given $V' \subseteq V$, $\text{proj}_{V'}(G_X, R_X) = (G', R') \in T_{V'}$ where

• $G' = \{A \cap V' \mid A \in G_X, A \cap V' \neq \emptyset\}$,

• $R' = \{(A \cap V', A' \cap V') \in (G')^2 \mid (A, A') \in R\}$;

- given $x \in bn(S) \setminus V$, $\text{fresh}_x(G_X, R_X) \in T_{V \cup \{x\}}$ and $\text{fresh}_x(G_X, R_X) = (G_X \cup \{\{x\}\}, R_X \cup (\{\{x\}\} \times G_X) \cup (G_X \times \{\{x\}\}))$;

- given $V' \subseteq bn(S) \setminus V$, $\text{new}_{V'}(G_X, R_X) \in T_{V \cup V'}$ and $\text{new}_{V'}(G_X, R_X) = (G_X \cup \{\{v'\} \mid v' \in V'\}, R_X) \in T_{V \cup V'}$;

- given $x, y \in V$, and $\diamond \in \{=; \neq\}$, $\text{set}(x \diamond y, (G_X, R_X)) \in T_V$ and:

• $\text{set}(x = y, (G_X, R_X)) = ((G_X)/\sim, (R_X)/\sim)$, if not $x \neq (G_X, R_X) y$, where $\forall X, Y \in G_X, X \sim Y \stackrel{\Delta}{\rightleftharpoons} X = Y$ or $(x, y) \in (X \times Y) \cup (Y \times X)$,

• $\text{set}(x \neq y, (G_X, R_X)) = (G_X, R_X \cup \{(A, B); (B, A)\})$, if not $x = (G_X, R_X) y$, where $A, B \in G_X$ such that $x \in A$ and $y \in B$,

• $\text{set}(x \diamond y, (G_X, R_X))$ is undefined, otherwise.

The union $\cup$ gives the lowest upper bound of two properties; the intersection $\cap$ gathers the description of two disjoint sets of variables; the projection $\text{proj}$ restricts the set of the variables; the operator $\text{fresh}$ adds a new variable the value of which is assumed to be distinct from the value of the other variables; the operator $\text{new}$ adds a set of variables without any assumption about their values; the operator $\text{set}$ simply adds a new constraint.

Then, we lift $T_V$ by adding an extra element $\perp_V$. Its concretization $\gamma_V^I(\perp_V)$ is the empty set of functions. Abstract union is lifted by $A \cup \perp_V = \perp_V \cup A = A$, abstract intersection by $A \cap \perp_V = \perp_V \cap A = \perp_V \cup \perp_V'$. Other primitives are defined to be strict, that is to say:

$$ \text{fresh}_{\perp}(\perp_V) = \text{proj}_{\perp}(\perp_V) = \text{set}(\perp, \perp_V) = \perp_V $$

Furthermore, undefined images in set are identified with $\perp_V$.
### 5.1.2 Equality and Disequality Relations Among Channel Names

We first abstract the equality and the disequality relations between the channel names of each agent. We set, for that purpose, $V = bn(S)$ and we introduce, for each $V \subseteq bn(S)$, the abstract domain $G_V = T_V \cup \{\perp_V\}$. $G_V$ is related to $\wp(Id \times \mathcal{E}(V))$ by the following concretization function:

$$ \gamma_V(A) = \{(id, E) \mid E \in \gamma_V^{(bn(S) \times Id)}(A)\}, \text{ when } A \neq \perp_V. $$

The same way, we describe relations between the names of two agents: we introduce $V' = \{x_i \mid x \in bn(S), i \in \{?, !\}\}$, and we define for each subset pair $(V?, V!)$ of $bn(S)^2$, $G_{V?}^{V!}$ as being the set $T_{V'} \cup \{\perp_{V'}\}$ where $V' = \{x_i \mid i \in \{?, !\}, x \in V_i\}$.

We now give primitive definitions: we set $\varepsilon_{\emptyset} = (\emptyset, \emptyset)$; we set $\nu x = \text{fresh}_x$ since, at its creation, a fresh name cannot have been communicated to any other variables; we define the extension $new_X^\top$ (resp. the garbage collection $gc_X$) by $new_X$ (resp. $\text{proj}_X$); we set $\text{match}(x \diamond y, A) = \text{set}(x \diamond y, A)$; product $A_? \bullet A!$ is obtained by first renaming the variable $x$ into $x_?$ (resp. $x!$) in $A_?$ (resp. in $A!$) and then intersecting the two results using $\emptyset$; projection $fst^\sharp(A)$ (resp. $\text{snd}^\sharp(A)$) is obtained by first using the projection $\text{proj}_{V?}$ (resp. $\text{proj}_{V!}$) and then renaming the variable $x_?$ (resp. $x!$) into $x$; synchronization is defined by $\text{sync}(\{x = y\} \cup X, A) = \text{sync}(X, \text{set}(x = y, A))$ and $\text{sync}(\emptyset, A) = A^3$; we set $\text{fetch}((i, j), A) = A$ since the allocation of new markers does not change the marker of channel names.

### 5.1.3 Equality and Disequality Relations Among Markers

We then abstract the equality and the disequality relations between the marker of an agent and the markers of its names. We set $V = bn(S) \uplus \{\text{agent}\}^4$, and we introduce, for each $V \subseteq bn(S)$, the abstract domain $G_V = T_{V'} \cup \{\perp_{V'}\}$ where $V' = V \cup \{\text{agent}\}$. $G_V$ is related to $\wp(Id \times \mathcal{E}(V))$ by the following concretization function:

$$ \gamma_V(A) = \left\{ (id, E) \mid \left( \left( \left( \begin{array}{ll} V \cup \{\text{agent}\} & \rightarrow \text{Id} \\ v \in V & \rightarrow \text{snd}(E(v)) \\ \text{agent} & \rightarrow \text{id} \end{array} \right) \in \gamma_{V \cup \{\text{agent}\}}^{Id}(A) \right) \right\}, $$

when $A \neq \perp_V$.

The same way, we describe relations between the markers of two agents: we introduce $V' = \{x_i \mid x \in bn(S) \uplus \{\text{agent}\}, i \in \{?, !\}\}$, and define, for each subset pair $(V?, V!)$ of $bn(S)^2$, $G_{V?}^{V!}$ as being the set $T_{V'} \cup \{\perp_{V'}\}$ where $V' = \{x_i \mid i \in \{?, !\}, x \in V_i \uplus \{\text{agent}\}\}$.

Primitives are all defined as in the previous domain, except for the primitives $\varepsilon_{\emptyset}$, $\nu$, $\text{match}$ and $\text{fetch}$: we set $\varepsilon_{\emptyset} = (\{\text{agent}\}, \emptyset)$ since it describes an agent with an empty environment; we set $\nu x(A) = \text{match}(\text{agent} = x, \text{new}_{\{x\}}(A))$ because the marker of a newly created name is the marker of the thread which has declared it;

<footnote n="3">³ This primitive is well-defined due to an associativity criterion.</footnote>

<footnote n="4">⁴ $A \uplus B$ denotes the disjoint union of A and B.</footnote>
we define $match(x = y, A) = set(x = y, A)$ and $match(x \neq y, A) = A$, since two different names do not necessarily have distinct markers; we set $fetch((i, j), A) = fresh_{agent_i}(proj_{j' \setminus \{agent_{i'}\}}(A))$ since, when duplicating a resource, the marker is fresh and distinct from any other existing marker.

## 5.2 Marker Analysis

We aim at describing the markers associated with an agent and its channel names. For the sake of simplicity, we use Prop. 1 and approximate every tree marker $id$ by the word $\phi_1(id)$ of $\Sigma^*$ written along its right comb. Then, we want to compute, for each agent $P$, an approximation of the set $Int(P)$, defined as follows:

$$ \left\{ \left( \begin{array}{c} \text{id}, \left\{ \begin{array}{l} \text{fn}(P) \rightarrow (\Sigma \cup \text{bn}(S))^* \\ y \rightarrow (a_y \cdot \phi_1(b_y)) \end{array} \right\} \\ \exists C \in C(S), \exists \text{id} \in \text{Id}, \exists E \in \mathcal{E}(\text{fn}(P)), \\ (P, \text{id}, E) \in C \\ \forall y \in \text{fn}(P), E(y) = (a_y, b_y) \end{array} \right) \right\}. $$

We will first describe the general shape of markers, and then infer some relational algebraic properties on them. By reduction, we will use this information to synthesize equality and disequality relations between channel names and between markers.

### 5.2.1 Shape Analysis

Shape analysis consists in distinctly abstracting, for each agent $P$, the set of markers which can be associated to an instance of $P$ and to each of its channel name. Our abstraction is built upon the lattice Reg of regular languages over the alphabet $(bn(S) \cup \Sigma)$. For each $V \subseteq bn(S)$, we define $G_V = \text{Reg} \times \mathcal{F}(V, \text{Reg})$. For all $(A, f) \in G_V$, $\gamma_V(A, f) \subseteq \text{Id} \times \mathcal{E}(V)$ is the set of all the elements $(id, E)$ which satisfy: $\phi_1(id) \in A$ and $\forall x \in V, y. \phi_1(id_x) \in f(x)$ where $(y, id_x) = E(x)$.

Abstract union is defined point-wisely. Since the domain is not relational, we define, for each $V_?, V_!$ in $bn(S)$, the domain $G_{V_?}^{V_!}$ as the Cartesian product $G_{V_?} \times G_{V_!}$, and the primitives $\bullet$, $first^\ddagger$, $second^\ddagger$ as the canonical pair construction and projection functions. Other abstract primitives are defined as follows:

$$ - \varepsilon_\emptyset = (\varepsilon, \emptyset); $$

$$ - \nu x(id^\ddagger, f^\ddagger) = (id^\ddagger, f^\ddagger[x \mapsto x.id^\ddagger]); $$

$$ - \text{new}_X^\top(id^\ddagger, f^\ddagger) = (id^\ddagger, f^\ddagger[x \mapsto \text{bn}(S).\Sigma^*, \forall x \in X]); $$

$$ - gc_X(id^\ddagger, f^\ddagger) = (id^\ddagger, f^\ddagger|_X); $$

$$ - \text{match}(x = y, (id^\ddagger, f)) = \begin{cases} [- \to \emptyset] & \text{if } f(x) \cap f(y) = \emptyset \\ f[x, y \mapsto f(x) \cap f(y)] & \text{otherwise;} \end{cases} $$

$$ - \text{match}(x \neq y, A) = A; $$

$$ - \text{sync}(\{x = y\} \cup X, A) = \text{sync}(X, \text{match}(x = y, A)) \text{ and } \text{sync}(\emptyset, A) = A; $$

$$ - \text{fetch}((i, j), ((id_?, f_?), (id_!, f_!))) = ((id_!(i, j), f_?), (id_!(i, j), f_!)). $$

There can be infinite increasing sequences in Reg, so we need a widening operator to ensure the convergence of our analysis in a finite amount of time.
### 5.2.2 Global Numerical Abstraction

Numerical abstraction captures the relations between the markers which are associated to an agent and to its channel names. This abstraction is built upon the lattice of the affine relations among a set of numerical variables [9]. Each word is first approximated by its Parikh vector [10], then we abstract the relations between occurrence numbers of letters in markers. For each $V \subseteq bn(S)$, we denote by $\mathcal{X}_V$ the set of variables $\{p^\lambda | \lambda \in \Sigma\} \cup \{c^{(\lambda,v)} | \lambda \in \Sigma \cup bn(S), v \in V\}$. The variable $p^\lambda$ is used to describe the number of occurrences of $\lambda$ in the right comb of the markers of the instances of the agent $p$, while $c^{(\lambda,v)}$ is used to count the number of occurrences of $\lambda$ in the marker associated to the syntactic name $v$ when $\lambda \in \Sigma$, or in determining whether $v$ is bound to a channel created by an instance of the restriction $(\nu, \lambda)$ when $\lambda \in bn(S)$. $G_V$ is the set of affine equality relations among the variables of $\mathcal{X}_V$. For all $\mathcal{K}$ in $G_V$, $\gamma_V(\mathcal{K}) \subseteq \text{Id} \times \mathcal{E}(V)$ is the set of the elements $(id, E)$ such that the assignment

$$ \{p^\lambda \to |id|_\lambda, c^{(\lambda,v)} \to |y.id_c|_\lambda \text{ where } (y, id_c) = E(c)\} $$

is a solution of $\mathcal{K}$.

In the same manner, for each $V_?, V_! \subseteq bn(S)$, we denote by $\mathcal{X}_{V_?}^{V_!}$ the set of variables $\{p_i^\lambda | \lambda \in \Sigma, i \in \{?, !\}\} \cup \{c_i^{(\lambda,v)} | \lambda \in \Sigma, i \in \{?, !\}, v \in V_i\}$. We also define $G_{V_?}^{V_!}$ as the set of affine equality relations among the variables of $\mathcal{X}_{V_?}^{V_!}$. For all $\mathcal{K}$ in $G_{V_?}^{V_!}$, $\gamma_{V_?}^{V_!}(\mathcal{K}) \subseteq \text{Id} \times \mathcal{E}(V)$ is the set of elements $((id?, E?), (id?, E!))$ such that the assignment:

$$ \{p_i^\lambda \to |id_i|_\lambda, c_i^{(\lambda,v)} \to |y.id_c|_\lambda \text{ where } (y, id_c) = E_i(c)\} $$

is a solution of $\mathcal{K}$.

Most primitives can be encoded using affine operators described in [9]. Positive abstract matching and synchronization are simply defined by adding new affine constraints in the system. These constraints specify that the Parikh's vectors coordinates of the synchronized channel names are pair-wisely equal; negative abstract matching is the identity function. Abstract resource fetching fetch((i, j), K) is obtained using an affine projection to keep only constraints not involving variables of the form $p_i^\lambda$, then adding the constraints $p_i^\lambda = p_i^\lambda$ for all $\lambda \in \Sigma$, and last replacing each occurrence of the variable $p_i^{(i,j)}$ by the expression $p_i^{(i,j)} - 1$.

**Example 3.** In our example, the analysis detects that:

- in each agent labeled **1**, the variable **next** is linked to a name created by the $(\nu \text{ next})$ restriction, while the variable **last** is linked to a name, either created by an instance of the $(\nu \text{ next})$ restriction, or by an instance of the $(\nu \text{ first})$ restriction. We also detect that, in the case where the variable **last** is linked to a name created by the $(\nu \text{ next})$ restriction, this variable is linked to the name created by the previous recursive instance of the one which has created the name communicated to the variable **next**;
- in each agent labeled 4, the variable **first** is linked to a name created by the (ν **first**) restriction, while the variable **last** is linked to a name either created by an instance of the (ν **right**) restriction or by an instance of the (ν **first**) restriction.

These properties are deduced from the following invariants:

$$
\left\{
\begin{array}{ll}
f(1) \text{ satisfies} & \begin{cases} c^{\text{next,next}} = 1 \\ c^{\text{first last}} + c^{\text{next last}} = 1 \\ c^{(0,2),\text{next}} = c^{(0,2),\text{last}} + c^{\text{next last}} \end{cases} \\
f(4) \text{ satisfies} & \begin{cases} c^{\text{next last}} + c^{\text{first last}} = 1 \\ c^{\text{first first}} = 1 \end{cases}
\end{array}
\right.
$$

where $f$ denotes the result of the analysis.

Nevertheless, our abstract domain is not expressive enough to merge these
two environments, and detects no insightful information for the agent labeled 6.
That is why we introduce a partitioned domain. □

5.2.3 Partitioned Numerical Abstraction

We propose to partition the set of the interactions between channels and agents
in order to get more accurate results. To avoid complexity explosion, we do not
globally abstract environments, we only compare pair-wisely the right comb of
the markers. Let $\psi^5$ be a linear form defined on $\mathbb{Q}^\Sigma$. We introduce the set $\mathcal{G}_V$ of
functions which map $(V \times bn(S)) \unlhd ((V \times bn(S))^2)$ onto the set of affine subspaces
of $\mathbb{Q}^2$. For all $f \in \mathcal{G}_V$, $\gamma_V(f) \subseteq \text{Id} \times \mathcal{E}(V)$ is the set of the elements $(id, E)$ such
that:

- $\forall x \in V$, such that $E(x) = (c_x, id_x)$.
  $(\psi([\lambda \to |\phi_1(id)|_\lambda]), \psi([\lambda \to |\phi_1(id_x)|_\lambda])) \in f(x, c_x);$

- $\forall x \in V, \forall y \in V$, such that $E(x) = (c_x, id_x)$ and $E(y) = (c_y, id_y)$,
  $(\psi([\lambda \to |\phi_1(id_x)|_\lambda]), \psi([\lambda \to |\phi_1(id_y)|_\lambda])) \in f((x, c_x), (y, c_y)).$

Because of the precision of the partitioning, we cannot afford much calculi in
this domain. This domain will only be used to propagate information we got
from the global numerical abstraction.

We now give primitive definitions. For $V_?, V_! \subseteq bn(S)$, we define $G_{V_?}^{V_!}$ as the Cartesian product $G_{V_?} \times G_{V_!}$. The concretization $\gamma_{V_?}^{V_!}$ is defined pair-wise. Pair construction and projection functions are the canonical ones. Other abstract primitives are defined as follows:

- abstract union is defined by applying the affine union component-wise;

- we define $\nu_x(f)$ to be the following element:

$$
f[(x, x) \to \{(n, n) \mid n \in (Q)\}, ((x, x), (-, -)) \to \mathbb{Q}^2, ((-, -), (x, x)) \to \mathbb{Q}^2];
$$

<footnote n="5">⁵ This abstraction must be done with several linear forms chosen according to a pre-
analysis and Thm. 3.</footnote>
$$ - \text{match}(x = y, f) = f \left[ \begin{array}{l} ((x, c), (y, c)) \to f((x, y), (c, y)) \cap \{(n, n) \mid n \in \mathbb{Q}\} \\ ((x, c), (y, d)) \to \emptyset, \text{ if } c \neq d \end{array} \right]; $$

$$ - \text{match}(x \neq y, f) = f; $$

$$ - gc_X(f) = f_{\{(x,-),(y,-)) \mid x,y \in X\}}; $$

$$ - \text{new}_X^\top(f) = f \left[ \begin{array}{l} x, c \to \mathbb{Q}^2, x \in X; \\ (x, c), (-, -) \to \mathbb{Q}^2, x \in X; \\ (-, -), (x, c) \to \mathbb{Q}^2, x \in X \end{array} \right]; $$

$$ - \text{sync}(\{y_k = x_k \mid k \in K\}, (f,g)) = (f', g) \text{ where} $$

$$ f' = f[(y_i, c), (y_j, d)) \to f((y_i, c), (y_j, d)) \cap g((x_i, c), (x_j, d)), \forall i, j \in K]; $$

$$ - \text{fetch}((i,j), (f,g)) = (f[(y, c) \to \mathbb{Q}^2], g). $$

We shall notice that no information is calculated by abstract name creation and abstract marker allocation. Nevertheless, during synchronization, the description of the communicated names is copied to the description of the receiver environment. A complete reduction of properties would lead to a time complexity explosion. We use a partial reduction. On the first hand, we use thread markers as pivots and replace each abstract element $f$ with the following element:

$$ f\left[\left((x, c), (y, d)\right) \to f((x, c), (y, d)) \cap \left\{(x, y) \mid \exists z, \begin{array}{l} (z, y) \in f(y, d), \\ (z, x) \in f(x, c) \end{array}\right\}\right], $$

and on the other hand, we always perform reductions between global numerical abstraction and partitioned numerical abstraction: global numerical analysis is used to collect all the information, which is then projected onto each case of the partition.

**Example 4.** For $\Psi$, we choose the linear form which maps each vector to the sum of its components. Our analysis succeeds in proving that the second pattern matching, in the example, is not satisfiable. Along the abstract iteration, the analyzer proves that in agent **6**, the names linked to the variables **x** and **y** have been respectively declared:

1. by the action ($\nu$ first) of a thread with a **0** marker length and the action ($\nu$ first) of a thread with a **0** marker length;

2. or by the action ($\nu$ first) of a thread with a **0** marker length and by the action ($\nu$ next) with a **1** marker length;

3. or by the action ($\nu$ next) of a thread $t_1$ and by the action ($\nu$ next) of a thread $t_2$ such that the length of the marker of $t_2$ is equal to the length of the marker of $t_1$ plus **1**;

4. or by the action ($\nu$ next) of a thread the length of the marker of which was arbitrary and by the action ($\nu$ first) of a thread the length of the marker of which was **0**.

Then it detects that the matching pattern ([$x = y$]) can only be satisfied for the case **1** and it discovers that in agent **7**, all the syntactic channel names **x**, **y** and **first** are bound to a channel created by the action ($\nu$ first) the thread marker of which is $\varepsilon$ and concludes that the second pattern matching ([$x \neq first$]) cannot be satisfied. $\square$
# 6 Reduced Product

We run our analysis with a reduced product of these five domains. There are several kinds of reductions: we use the information about equality of channel names and equality of markers to refine marker analysis; conversely, we use the information obtained in marker analysis to infer information about disequalities of channel names and disequalities of markers; we also make reductions between the global and partitioned numerical abstractions; we use the results obtained in marker analysis to prove equality relations between name markers. For the sake of the brevity, we only describe this last kind of reduction, which is the most difficult one. Marker analysis may discover that two markers are recognized by the same automaton $\mathcal{A}$ and have the same Parikh's vector, but these two conditions do not ensure that these two markers are the same. We give in Thm. 3 a decidable sufficient condition on the automaton $\mathcal{A}$ to ensure the equality of such markers.

Let $\Sigma$ be a finite alphabet, $\phi$ be a linear function from the vector space $\mathbb{R}^{\Sigma}$ into the vector space $\mathbb{R}^m$, and $\mathcal{A}$ be an automaton $(Q, \to, i, f)$ such that the set $Q$ is finite, the relation $\to$ is a part of $Q \times \Sigma \times Q$ and $i$ and $f$ are parts of $Q$.

**Definition 1.** We define the set $\text{Path}(\mathcal{A})$ of acyclic derivation sequences in $\mathcal{A}$ as the set of sequences $q_0 \xrightarrow{\lambda_1} \dots \xrightarrow{\lambda_n} q_n$ such that $q_0 \in i$, $q_n \in f$, for all $i, j \in [0; n]$, $i \neq j \implies q_i \neq q_j$, and for all $i \in [1; n]$, $(q_{i-1}, \lambda_i, q_i) \to$.

**Definition 2.** Let $q$ be a particular state in $Q$. We define the set $\text{Cycle}(\mathcal{A}, q)$ of elementary cycles of $\mathcal{A}$ stemming from the state $q$, as the set of sequences $q = q_0 \xrightarrow{\lambda_0} q_1 \dots q_n \xrightarrow{\lambda_n} q_{n+1} = q$ such that for all $i \in [1; n]$, $q_i \neq q$, and for all $i \in [0; n]$, $(q_i, \lambda_i, q_{i+1}) \to$.

**Definition 3.** Let $q_0 \xrightarrow{\lambda_1} \dots \xrightarrow{\lambda_n} q_n$ be a sequence in $\mathcal{A}$, we define its affine description $\mathcal{P}(q_0 \xrightarrow{\lambda_1} \dots \xrightarrow{\lambda_n} q_n)$ as the vector $\phi([\lambda \to |\lambda_1 \dots \lambda_n|_{\lambda}])$.

**Definition 4.** Let $a = q_0 \xrightarrow{\lambda_1} \dots \xrightarrow{\lambda_n} q_n$ be an acyclic derivation sequence in $\text{Path}(\mathcal{A})$, we define the family $\mathcal{F}(a)$ of affine descriptions of the cycle of the derivation $a$ as the family $(\mathcal{P}(c))_{c \in \bigcup\{\text{Cycle}(q_i) \mid i \in [0; n]\}}$.

**Theorem 3.** If

1. for all $q \in Q$, $\text{Card}(\text{Cycle}(\mathcal{A}, q)) \le 1$,

2. for all $a \in \text{Path}(\mathcal{A})$, $\mathcal{F}(a)$ is linearly independent in $\mathbb{R}^m$,

3. for all distinct acyclic derivations $a, a' \in \text{Path}(\mathcal{A})$, the two affine sets $\mathcal{P}(a) + \text{Vect}(\mathcal{F}(a))$ and $\mathcal{P}(a') + \text{Vect}(\mathcal{F}(a'))$ are disjoint,

then

$$ \forall u, v \in \Sigma^*, [u, v \text{ recognized by } \mathcal{A} \text{ and } \phi[\lambda \to |u|_{\lambda}] = \phi[\lambda \to |v|_{\lambda}]] \implies u = v. $$

Roughly speaking, the first condition ensures that the automaton $\mathcal{A}$ contains no embedded cycle. Then, from the description of a word Parikh's vector, we can deduce which main acyclic derivation is to be used to recognize this word (third condition), and how many times each cycles are to be used (second condition).
# 7 Conclusion

We have proposed a new parametric framework for automatically inferring the description of the dependency between the channel names used by the agents of a mobile system. We claim that this framework is very generic since [2,12,7,3] may all be seen as a particular use of it.

We have proposed several abstract domains to deal with this framework. They allowed us to prove some properties which cannot be obtained with [2,12,7,3].

**Acknowledgments.** We deeply thank anonymous referees for their significant comments on an early version of this paper. We wish also to thank Patrick and Radhia Cousot, Arnaud Venet, Antoine Min, Francesco Logozzo and Xavier Rival 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 *Proc. CONCUR'98*, LNCS. Springer-Verlag, 1998.

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

4. 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.

5. P. Cousot and R. Cousot. Abstract interpretation frameworks. *Journal of logic and computation*, 2(4):511–547, August 1992.

6. P. Cousot and R. Cousot. Comparing the Galois connection and widening--narrowing approaches to abstract interpretation. In *Proc. PLILP'92*, LNCS. Springer-Verlag, 1992.

7. J. Feret. Confidentiality analysis of mobile systems. In *Proc. SAS'00*, LNCS. Springer-Verlag, 2000.

8. J. Feret. Occurrence counting analysis for the π-calculus. *ENTCS*, 39.2, 2001. Workshop on GEometry and Topology in CONcurrency theory, PennState, USA, August 21, 2000.

9. M. Karr. Affine relationships among variables of a program. *Acta Informatica*, pages 133–151, 1976.

10. R. J. Parikh. On context-free languages. *Journal of the ACM*, 13:570–581, 1966.

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

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