T Chabardès

P Dokládal

M Faessel

M Bilodeau

An affinity score for grains merging and touching grains separation

The physical properties of granular materials on a macroscopic scale derive from their microstructures. The segmentation of CTimages of this type of material is the first step towards simulation and modeling but it is not a trivial task. Non-spherical, elongated or nonconvex objects fail to be separated with classical methods. Moreover, grains are commonly fragmented due to external conditions: aging, storage conditions, or even user-induced mechanical deformations. Grains are crushed into multiple fragments of different shape and volume; those fragments drift from one another in the binder phase. This paper focuses on reconstruction of grains from these fragments using scores that match the local thickness and the regularity of the interface between two objects from a given primary segmentation of the material. An affinity graph is built from those scores and optimized for a given application using a user-generated ground truth on a 2D slice of the tridimensional structures. A minimum spanning tree is generated, and a hierarchical cut is performed. This process allows to reassemble drifted fragments into whole grains and to solve the touching grains problem in tridimensional acquisitions.

Introduction

X-Ray microtomography is now widely used by professionals and non-experts to characterize the structures of materials of interest. However, assessing precisely the structural information by conventional means is difficult due to the size of the acquisitions. Human interactions are unpractical for this amount of data. There is a need for automatic methods of analysis that can harvest the ever-increasing computing power.

This study focuses on composite materials made from a rubbery binder and brittle grains of various shapes and sizes mixed into a homogeneous mixture. Damage occurs when a mechanical shock is applied, causing fragmentation of these grains. The damaged structure affects the behavior of the material. Evaluating the extent of fragmentation may be useful for estimating effects on the reaction of the mixture. Highly clustered fragments and complex shapes require specific methods to identify all connections. The drift of fragments in the binder phase can not be solved using a method only based on the barycenter distance, as e.g. in [START_REF] Lloyd | Least squares quantization[END_REF], see figures [START_REF] Beucher | Segmentation d'Images Morphologie Mathématique[END_REF][START_REF] Gillibert | Stochastic multiscale segmentation constrained by image content[END_REF]. In the first part, we present how to evaluate the shape of the interface between two objects of a given segmentation. Pixels equidistant to two objects border to border forms separation segments. Each pixel of those segments is valued by the distance to border. Measurements are performed on the pixels along the segments such as mean, standard deviation of the pixels value. Some already relate to affinities; others can be transformed to affinities using a Gaussian kernel. In a second part, the grains are reassembled from the derived fragments using the proposed affinity score in combination with a hierarchical clustering, and a set of predetermined measurements done on the unprocessed acquisition.

Materials and 3D images.

The studied materials are composite materials with an elastic binder degraded by a mechanical impact of a falling mass. Those samples were acquired by Xray microtomography with a Skyscan 1172 high-resolution micro-CT system. Images of the work of Gillibert were recovered for comparison purposes [START_REF] Gillibert | Stochastic multiscale segmentation constrained by image content[END_REF]. The introduced method was also tested on our acquisitions. The following acquisitions illustrated in the figure [START_REF] Beucher | Use of watersheds in contour detection[END_REF] are studied:

-MAT1 is a 1014*1155*250 voxels image (3650.4*4158*900 µm 3 ). A mechanical impact is exerced from a 2kg mass falling 15cm. This material has been studied in [START_REF] Gillibert | 3d reconstruction and analysis of the fragmented grains in a composite material[END_REF]. -MAT2 is a 1000*1000*1000 voxels image (2097*2097*2097 µm 3 ). A mechanic impact is exerced from a 2kg mass falling 30cm. This is a new material.

Initial segmentation.

The work presented in this paper requires a primary segmentation on the acquisition. We suppose each fragment for every grain isolated, which effectively induces an over-segmentation, where grains are fragmented. Then, we successively merge pairs of fragments, whose affinity is the highest. Several approaches can be considered to create this over-segmentation. Gillibert and al. used a multiscale stochastic watershed in [START_REF] Gillibert | Stochastic multiscale segmentation constrained by image content[END_REF]. The estimation of the granulometry makes it possible to select appropriate scales to perform several stochastic watersheds and combine them to obtain a correct segmentation for each size of grains. However, this approach is tedious and costly. A less refined approach can be used, as over-segmented fragments will be merged during the clustering process: the resulting affinity will be high in this case. In this study, the image is first binarized using a method close to the Otsu threshold. The watershed is then computed from the inverse of the distance map, and the set of markers is generated by using the h-minima filter.

Other approaches could also be considered, such as using the distance map on the binarized image, as a probability density map to generate random markers for the watershed transformation. The only requirement is to find a right amount of over-segmentation. Every fragment can be split into a small number of objects in the over-segmentation, but no object must gather more than one fragment. In the figure [START_REF] Beucher | Use of watersheds in contour detection[END_REF], two segmentations have been provided for the studied materials.

State of art of fragments merging.

A morphological approach for removing cracks is to use the morphological closing combined with a volumic opening, see [START_REF] Matheron | Some methods for classification and analysis of multivariate observations[END_REF][START_REF] Serra | Image analysis and mathematical morphology[END_REF]. Small connected components are therefore removed, and fragments close in space are merged. The constrained watershed transform introduced by [START_REF] Beucher | Use of watersheds in contour detection[END_REF] used on the closed image can differentiate a fragmented grain from two grains merging. Markers have to be chosen to represent each grain appropriately and are an important parameter in this method. Two approach exists. The first approach is topological and uses the h-minima filter introduced in [START_REF] Soille | Morphological image analysis: principles and applications[END_REF]. The use of the h-minima with the watershed on the distance map is standard, but if the grains are highly fragmented and the fragments are scattered, the algorithm fails to reconstruct grains accurately.

The second approach is based on a method of cluster analysis, the K-means clustering, which aims to partition a set of observations into K clusters, as described in [START_REF] Lloyd | Least squares quantization[END_REF]. The number of clusters can be automatically calculated from a covariance measure. In [START_REF] Gillibert | 3d reconstruction and analysis of the fragmented grains in a composite material[END_REF], the K-means transform is used to generate the appropriate markers for the watershed transformation.

We propose in section 3 a fully automatic method for homogeneous granular material, which can be adapted to heterogeneous material. Based on the previously described affinity score, a maximum spanning tree is built. This maximum spanning tree can be used to form a hierarchy between fragments represented as a dendrogram. The estimation of grains size is used to cut this hierarchy and produce the final result.

State of art of touching objects separation.

Separation of touching objects is a recurring problem in image processing. Classical techniques like Hough-transform [START_REF] Leavers | Shape Detection in Computer Vision Using the Hough Transform[END_REF] or the watershed applied to the inverse of the distance function performs well when the objects of interest possess regular shapes such as spheres. Unfortunately, when shape and size of objects vary considerably or when clusters contain many objects, classical methods may fail to produce the desired separation. Differents approach exists [START_REF] Schmitt | Morphological multiscale decomposition of connected regions with emphasis on cell clusters[END_REF]: morphologybased procedures [START_REF] Beucher | Segmentation d'Images Morphologie Mathématique[END_REF], contour-based techniques [START_REF] Rosin | Shape partitioning by convexity[END_REF], graph theoretic approaches, parametric fitting algorithms and level set approach [START_REF] Dejnozkova | Modelling of Overlapping Circular Objects Based on Level Set Approach[END_REF][START_REF] Schüpp | Fast statistical level sets image segmentation for biomedical applications[END_REF]. Morphological multiscale decomposition can decompose clusters into size-specific scales, carrying markers for each disjoint region [START_REF] Henk | Algebraic framework for linear and morphological scalespaces[END_REF]. Methods exist for shape specific objects. In [20], a method based on a modified version of the pseudo-Euclidean distance transformation is able to split fused ellipses. In [START_REF] Faessel | Touching grain kernels separation by gapfilling[END_REF], a gap-filling method is proposed for elliptic shapes.

2 The morphological affinity score for adjacent objects.

Definitions.

We start from an initial segmentation as described in section 1.2. Let f : D → {0, 1} a binary image, where D is the definition domain. Binary objects We define the set X of N objects as X = {X i } i<N , so that X i ⊂ D and X i ∩ X j = ∅ for i = j. Each X i represents a grain or a fragment. The complement D \ X is the binder.

Distance mapping We define the distance mapping d : D → N labeling each pixel with the distance to the nearest object X i ∈ X according to a chosen metric.

SKIZ by distance function A zone of influence of a object X i of X is the subset of D that are closer to X i than to any other object, and we note it zi(i). A SKIZ is defined as the boundary of all zones of influence. We compute the SKIZ by using the watershed transform. We note this set skiz(X ) and we assume it thin and connected using some connexity .

Triple points The set T of triple points is the set of pixels that are equidistant to three or more distinct objects. We have extended the set T by including pixels on the border of f that are equidistant to two objects. The triple points are the extremities of a given segment of the SKIZ.

Interfaces We define interfaces between X i , X j as part of the segments along the SKIZ. We note I the set of interfaces, and I ij the interface between two distinct objects X i and X j . The distance decreases when going from triple points inwards, as shown in figure [START_REF] Faessel | Segmentation of 3d microtomographic images of granular materials with the stochastic watershed[END_REF]. However, this distance behaves differently when observed closer to the objects of interest. We define an incremental process to thin the skiz into the non-decremental segment.

I 0 = skiz(X ), T 0 = T I i+1 = I i \ T i+1 T i+1 = {a | ∃b a, b ∈ T i , d(b) > d(a)}
Finally, we define I ij = I ∞ ∩ zi(i) ∩ zi(j). Those interfaces are the support for building our new affinity scores. The distance mapping considered along the pixels of an interface gives various information regarding the shape of the interface between two objects. The figure (3.d) illustrates the interfaces I ij between various objects given some initial segmentation (3.b).

Weigths.

In the following part, we propose several measures to weight the interfaces. All proposed weights are w : I → R. However, it is important to notice that the range of w differs regarding to the considered weight. The barycenter distance. The simplest measure already used in [START_REF] Gillibert | 3d reconstruction and analysis of the fragmented grains in a composite material[END_REF] is the Euclidean distance between barycenters of two distinct objects:

w bar (I ij ) = X i -X j L 2
, where X denotes the barycenter of the object labeled X in X . Variance:

w σ 2 (I ij ) = x∈Iij d(x) 2 -w 2
µ (I ij ) the variance of the distance.

Affinities.

We note A, a positive and symetric matrix, with a ij ∈ (0, 1) the affinity score of X i and X j , where a value close to 1 corresponds to two closely related objects and a value close to 0 to distinct objects. All previous weights can be transformed to an affinity. We use a gaussian kernel for all weights that relate to a distance, where σ w is the scale of the kernel, as follows:

A = G(w, σ w ) = 1 √ 2πσ w e -w 2 2σ 2 w
Using the previous equation, we have

A bar , A d , A l , A µ , A σ 2 .
Length-to-surface ratio. Other affinities can be obtained from the previous weigths. Below, we use an affinity based on the surface of the objects. We define s(X) the surface of the object X as s(X) =| {x, x ∈ G(f ), x ∈ X} |, where G(f ) is a morphological gradient of the image f . We now define the new affinity A s as follows:

(a s ) ij = w l (I ij ) min(s(X i ), s(X j ))
Note that w l (I ij ) can be bigger than the surface of an objects, and the resulting affinity has to be bounded to (0, 1).

All those affinities can be used as such with clustering techniques. However, those affinities complement each other and we can combine several affinities as follows:

A = k A k f k (1)
In the next section, we used a linear combination of the affinities A bar , A µ , A σ 2 , A s to merge fragments in a composite material fragmented by mechanical pressure. We have optimized the linear combination by minimizing a score between the resulting merging and a ground truth, as described in section 3.2.

3 Fragments merging.

Minimum spanning and hierarchical cut.

We can use the linear combination of the introduced affinities with several existing clustering methods, such as K-means, spectral clustering, DBSCAN and other. The inconvenience is when the number of fragments increases computational issues appear (running time, instability of convergence, memory consumption). For given materials, we have chosen a hierarchical clustering and we perform a hierarchical cut using an estimated size of grain extracted from a covariance analysis.

The previous affinity matrix is an adjacency The first step of the proposed clustering method is to produce a hierarchy using the minimum spanning tree of the graph 1-A to remove edges of low affinity. We produce a dendrogram from the minimum spanning tree as illustrated in the figure [START_REF] Faessel | Touching grain kernels separation by gapfilling[END_REF]. The strategies employed to build the hierarchy can be of any of the commonly used types: agglomerative or divisive.

Cutting the hierarchy depends on the material that is considered. MAT1 is a homogeneous composite with one size of grains. Therefore, the criterium that we used to cut the hierarchy is volumic. The covariance analysis of the raw data can give us an estimate of the mean size of the grains, see [START_REF] Faessel | Segmentation of 3d microtomographic images of granular materials with the stochastic watershed[END_REF]. We have associated with each cluster the sum of the volumes of the individual objects composing the former. Cutting the hierarchy can be achieved by the pseudo-code [START_REF] Beucher | Segmentation d'Images Morphologie Mathématique[END_REF].

Due to the previous thinning of the SKIZ, the initial graph might not be connected. The missing edges are diverging all along the SKIZ and therefore of low affinities. Moreover, filtering the graph by removing edges that feature low affinity values can be done to process graphs of lower density. Each connected components can be processed afterward independently.

Algorithm 1 Top-down cut of the hierarchy. w(i) is the volume associated to cluster i. L is the volumic limit estimated by the covariance.

1: i ← root of the dendrogram 2: Cut(i) 3: procedure Cut(i) 4: if i is a leaf OR w(i) < L then 5: return i 6: else 7:
return Cut(left child of i), Cut(right child of i)

Optimizing the affinity

The choice of the affinity is crucial to obtain the desired result. One can see that a single affinity that was presented earlier is not sufficient to reassemble the fragments, see figure [START_REF] Beucher | Segmentation d'Images Morphologie Mathématique[END_REF]. The K-means algorithms is based on the barycenter distance and is not able to reassemble fragments that have drifted far away from their original positions. The size distribution of fragments is wide, the drift between similar fragments can be big enough not to be caught by the naive border-to-border distance as illustrated in figure [START_REF] Gillibert | Stochastic multiscale segmentation constrained by image content[END_REF]. We assume that a combination of affinities is the key to obtain better results.

We opted for a linear combination of the four affinities A bar , A µ , A σ 2 and A s . To optimize the affinity, we optimize the segmentation using a user-provided ground truth (GT) on one or more slices of the 3D image.

We construct a bivariate histogram H from the labels of GT and from the labels obtained by hierarchical clustering extracted from the same slices. H = [h ij ] is a M × N sparse matrix where M is the number of detected objects and N the number of objects in the GT. From H , we compute the F 1 score of the segmentation in the following way: A sum of a line i = const, P (i) = j h ij , is the detection rate of label i. The index l = arg max j h ij , is the label corresponding to i in GT. We now compute the true positive T P (i) = h il , the false positive F P (i) = P (i) -T P (i).

The sensitivity and the positive predictive value for every i is: Sens(i) =

T P (i) P (i) and P P V (i) =

T P (i)

T P (i)+F P (i) . A F 1 score is computed for every detected object, with H the harmonic mean: F 1 (i) = H(Sens(i), P P V (i)). The overall F 1 score of the result is the harmonic mean of all scores: F 1 = H(F 1 (i)), 1 ≤ i ≤ M . The vector (f k ) in equation 1 is then determined by minimizing 1 -F 1 . The minimization method is a modification of Powell's method [START_REF] Powel | An efficient method for finding the minimum of a function of several variables without calculating derivatives[END_REF], [START_REF] Press | Numerical Recipes[END_REF]. It performs sequential one-dimensional minimizations along each vector of the directions set.

Results.

Table [START_REF] Beucher | Segmentation d'Images Morphologie Mathématique[END_REF] shows the size of the generated graph for MAT1 and MAT2. One benefit of this method is to be able to work on a compressed representation of the studied materials from the raw tridimensional data. Further compression is achieved by using a -filtering of the weighted graph. Here, edges lower than mean(a) -2 * std(a) have been removed. An appropriate filtering will generate several connected components, which can each be processed independently and in parallel. (6) shows a crop of a result obtained on MAT1. Figure [START_REF] Gillibert | Stochastic multiscale segmentation constrained by image content[END_REF] shows the tridimensional results on MAT1 and MAT2. Some grains are broken down into multiple small fragments, they have been successfully merged. Touching grains have been solved for MAT2 and MAT1 and visually satisfying results have been achieving for the merging of fragments.

Conclusion

We have introduced a method to calculate affinities between objects in tridimensional data such as CT images. Those affinities have been applied to the problem of fragments merging using machine learning algorithm. Oversegmented fragments were also merged, as shown in figure [START_REF] Gillibert | Stochastic multiscale segmentation constrained by image content[END_REF], while every touching grains remains separated. The touching objects problem were therefor also solved with the same approach. Visually satisfying results were obtained for both, see figure [START_REF] Gillibert | Stochastic multiscale segmentation constrained by image content[END_REF]. Those affinities are invariant to scales and are able to characterize objects of various shapes. Many perspectives arise from this preliminary work. Further works should first concern the influence of the primary segmentation and the metric employed to build the interfaces. The proposed method for hierarchical clustering is a proof of concept than could be applied to more advanced clustering technics.

Fig. 1 .

 1 Fig. 1. The fragment 2 is closer to 1 even though it should be associated to 3.

Fig. 2 .

 2 Fig. 2. (a,c) are 2D slices of 3D X-ray microtomographic images of fragmented granular material. (b,d) are the corresponding over-segmentation produced by h-minima markers. (e,f) are results obtained in [8]. (e) Watershed segmentation of the closed image after a h-minima filter. (f) Watershed segmentation using markers computed from the K-means. In (e) and (f), we can observe several grains over-segmentated or under-segmentated.

Fig. 3 .

 3 Fig. 3. The process to generate interfaces is illustrated. In (a) a granular material. (b) an example of segmentation that was used to produce the skiz. In (c), The skiz is drawn in red, the objects in gray, and triple points in blue. In (d) are shown interfaces generated using the Manhattan distance.

Fig. 4 .

 4 Fig. 4. Divergence of the distance along the skiz is observed towards the triple points.

  on the pruned interface: w d (I ij ) = x∈Iij d(x) with d the distance to fragments. Length of the pruned interface: w l (I ij ) = | I ij | the length of each interface. Mean: w µ (I ij ) = w d (I ij )/w l (I ij ) the mean of the distance.

Fig. 5 .

 5 Fig. 5. A simple case of dendrogram built from a maximum spanning tree is illustrated. In (a), Objects are shown in black, and interfaces are valued using a colormap scheme. The affinity used to generate the valued edges is a linear combination of Aµ, A σ 2 and As.The resulting dendrogram is shown in (b), where 3 clusters are visually identified, and the y-axis is 1 -A. We can see that objects 1 and 3 have a lower affinity than 0 and 2, and visually two distinct grains that are connected.

Fig. 6 .

 6 Fig. 6. shows two fragments that heavely drift from one another on the bottom left. (b) shows the over-segmentation. (c) the result of the fragment merging. The round fragment in (b) in the bottom right corner colored in red in blue, is oversegmented. In (c), the two objects were merged one orange grain.)

Fig. 7 .

 7 Fig. 7. Results of the fragments merging method.(a) Slice of reassembled MAT1. (b) Slice of reassembled MAT2. In (a), grains are heavely fragmented such as the green grain in the top-right corner, and heavely clustered such as red and yellow grains in the bottom-right corner. In (b), less fragmentation is observed but there is more connections between grains.

Table 1 .

 1 The graphs generated for MAT1 and MAT2. Here is shown the gain in memory consumption when working on graphs.

	Materials Number of voxels Number of objects Number of edges After -filtering
	MAT1	2.9 * 10 8	720	5106	2456
	MAT2	1.0 * 10 9	4660	28341	12846

Acknowledgment

This work has received funding from DGA and is a collaboration between Transvalor, DGA, CEA Gramat. The acquisitions are carried out at the CEA Gramat, a french public laboratory affiliated to the Commission of Atomic Energy and Alternative Energies.


Damien Pous

On Bisimulation Proofs for the Analysis of Distributed Abstract Machines

We illustrate the use of recent, non-trivial proof techniques for weak bisimulation by analysing a generic framework for the definition of distributed abstract machines based on a message-passing implementation. The definition of the framework comes from previous works on a specific abstract machine; however, its new presentation, as a parametrised process algebra, makes it suitable for a wider range of calculi. A first version of the framework can be analysed using the standard bisimulation up to expansion proof technique. We show that in a second, optimised version, rather complex behaviours appear, for which more sophisticated techniques, relying on termination arguments, are necessary to establish behavioural equivalence.

Introduction

Recently, many calculi encompassing distribution and mobility have been studied as a basis for programming languages. Examples include Join [START_REF] Fournet | JoCaml: A Language for Concurrent Distributed and Mobile Programming[END_REF], Nomadic Pict [START_REF] Unyapoth | Nomadic pict: Correct Communication Infrastructure for Mobile Computation[END_REF], Kells [START_REF] Bidinger | The Kell Calculus: Operational Semantics and Type System[END_REF], Ambients [START_REF] Cardelli | Mobile Ambients[END_REF], Klaim [START_REF] De Nicola | KLAIM: A Kernel Language for Agents Interaction and Mobility[END_REF], Seals [START_REF] Castagna | The Seal Calculus Revisited[END_REF]. The expressive power supplied by the primitives underlying such models raises the question of implementability in a distributed framework. In [START_REF] Sangiorgi | A Distributed Abstract Machine for Safe Ambients[END_REF], a distributed abstract machine is defined, to implement the Safe Ambient Calculus [START_REF] Levi | Mobile Safe Ambients[END_REF]: the PAN. The main ingredients in the definition of this machine are locations -where local processes are executed -and forwarders, that transmit messages between locations. In [START_REF] Hirschkoff | A Correct Abstract Machine for Safe Ambients[END_REF], we defined an optimised version of this machine where useless forwarders can be garbage collected, and less messages are transmitted along the network. We proved that the resulting abstract machine is weak barbed bisimilar to the original one; however due to the lack of adequate up-to techniques or compositionality results, this proof is quite tedious, and cannot easily be used as a basis for further studies.

Motivated by these difficulties, we developed new up-to techniques for weak bisimulation [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF]. These techniques improve on previously known techniques; however, they are developed in a completely abstract setting and their applicability has not yet been evaluated beyond rather simple illustrative examples.

Before focusing on behavioural equivalences and proof techniques, we present the first main contribution of this work, the definition of a framework to reason about distributed implementations of process algebras with mobility. In this framework, a network is represented by a set of locations, or hosts, where arbitrary local processes are executed. The behaviour of local processes is specified by a given LTS, whose labels correspond to the following possible actions:

sending arbitrary messages to other locations, spawning local processes, inside new locations, migrating to another location.

While this framework is the basis of the PAN abstract machine [START_REF] Sangiorgi | A Distributed Abstract Machine for Safe Ambients[END_REF], we dropped most of the hypotheses that were related to the implementation of an Ambientbased calculus. Therefore, it should be suitable to analyse a rather wide range of calculi (this is discussed in Remark 2.1).

We then move to the analysis of this framework, which serves as support for our second main contribution: illustrating a non-trivial use of recent proof techniques to reason about a rather complex system.

A forwarder from location h to location k acts like a substitution that replaces any occurrence of h by k in the whole network: a message sent to h will actually reach k. Accordingly, we prove that a net with a forwarder expands the corresponding substituted net (expansion is the standard behavioural preorder that leads to the correct weak bisimulation up to expansion technique [START_REF] Sangiorgi | The problem of "Weak Bisimulation up to[END_REF]). This result allows one to abstract over the communication framework when validating possible optimisations of local processes.

The main drawback of this framework is the creation of forwarder chains, that slow down the communications between local processes. To address this inefficiency, we introduce an optimisation, inspired from [START_REF] Hirschkoff | A Correct Abstract Machine for Safe Ambients[END_REF], that consists in defining a forwarder relocation mechanism, that contracts forwarder chains. Like in [START_REF] Hirschkoff | A Correct Abstract Machine for Safe Ambients[END_REF], this mechanism breaks the initial proof strategy, as the expansion result does no longer hold. We show in details how the techniques we developed in [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF] make it possible to give nevertheless a modular proof of correctness, where the bisimulation candidates that we manipulate remain tractable and express only local properties of processes.

Being able to work with small bisimulation candidates is quite important: they are much easier to check, and when a small part of the system is refined, there is hope that only some of the proofs will need to be updated. Even more important is the fact that the relations focus on local properties, since this allows one to write explicitly the slight differences between related processes and to reason syntactically about these.

We actually allude in [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF] to an example derived from [START_REF] Hirschkoff | A Correct Abstract Machine for Safe Ambients[END_REF]. It turned out that the development made in a corresponding technical report missed a crucial step in the proof, and, more importantly, contained a mistake. Moreover, the proof presented here for the optimised system is less specific and aims at giving a better illustration of the benefits given by the general techniques of [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF], and of their flexibility.

Outline of the paper. In Sect. 1, we introduce our notations and the notions used in the sequel. We define the initial framework in Sect. 2, and we analyse it in Sect. 3. Section 4 is devoted to the definition of the optimisation, and to the corresponding correctness proof. We conclude with some remarks in Sect. 5.

LTS, Bisimilarity

We consider labelled transition systems (LTS) P, L, → , with domain P, labels or actions in L and transition relation → ⊆ P × L × P. The elements of P are called processes and are denoted by P, Q in this section. L will always implicitly contain a distinguished silent action, noted τ . We let α, β (resp. a, b) range over actions, in L (resp. visible actions, in L\{τ }).

We let R, S, B, E range over binary relations (simply called relations in the sequel) between processes. We denote respectively by R + , R = , R the transitive, reflexive, transitive and reflexive closures of a relation R. P RQ means P, Q ∈ R. The composition of two relations R and S, written RS, is defined by RS { P, Q /P RT and T SQ for some process T }. We also define the inverse of a relation: R -1 { P, Q /QRP }. I is the identity relation, defined by I { P, P /P ∈ P}. We say that R contains S (alternatively, that S is contained in R), written S ⊆ R, if P SQ implies P RQ. Given an action α, the set of transitions along α induces a relation denoted by

α →: α → { P, Q / P, α, Q ∈ →}.
Its inverse is written using a reversed arrow:

a ← = ( a →) -1
, and similarly for other forms of arrows, defined below.

Definition 1.1 (Termination).

A relation R terminates if there is no infinite sequence (P i ) i∈N such that ∀i, P i RP i+1 .

The definitions of behavioural equivalences and preorders will make use of the following weak transition relations.

Definition 1.2 (Weak transitions). α → τ → = if α = τ a → if α = a ∈ L\{τ } α ⇒ τ → α → τ → α ⇒ τ → α → τ →
We can remark the following properties:

τ ⇒ = τ → , τ ⇒ = τ → + , a ⇒ = a ⇒ (note in particular the difference between τ ⇒ and τ ⇒).
Definition 1.3 (Evolution of relations). Let α be an action and R, S two relations. We say that R α-evolves to S if P RQ, P α → P implies Q α ⇒ Q and P SQ for some Q . We say that R evolves silently to S when R τ -evolves to S, and that R evolves visibly to S when R a-evolves to S for any a ∈ L\{τ }. Definition 1.4 (Simulation, Bisimulation, Bisimilarity). Let R be a relation. R is a simulation if it evolves to itself. A bisimulation is a symmetric simulation. Bisimilarity, denoted by ≈, is the union of all bisimulations.

A Framework for Distributed Computation

We let h, k range over a given set of locations. We denote by [k/h] the function that replaces location h by location k. We let σ range over such substitutions, that are naturally extended to the various syntactical categories defined in the sequel. We furthermore assume two sets of (local) processes and messages, denoted respectively by P, Q and M, N . Processes may contain messages, and vice-versa. In order to represent this, we require two operations on these sets:

the addition of a message M to a process P , denoted by "P | {M }", the embedding of a process P into a message, denoted by "reg P ". These operations are supposed to satisfy the following equations:

(P | {M }) | {N } = (P | {N }) | {M } (1)
P | {reg (Q | {M })} = (P | {reg Q}) | {M } (2)
(P | {M })σ = P σ | {M σ} (3)
Nets combine localised processes and messages with a destination:

U ::= 0 (empty net) | h[P ] (process located at h) | U U (parallel composition) | h{M } (pending message) | (νh)U (location restriction) | h k (forwarder located at h) Definition 2.1 (Structural congruence).
Structural congruence is the smallest congruence ≡ such that:

1. parallel composition ( ) forms an abelian monoid, with neutral element 0;

2. (νh)U ≡ (νk)(U [k/h]) if k not free in U ; 3. (νh)U V ≡ (νh)(U V ) if h not free in V ; 4.
(νh)(νk)U ≡ (νk)(νh)U ; and (νh)0 ≡ 0.

Π i U i will denote the parallel composition of the nets U i . The notation for tuples is x and (x, x) will denote the addition of an element x to x. Our notations are naturally extended using tuples; for example, h{ M } and h k will respectively denote Π i h{M i } and Π i h i k.

Definition 2.2 (Dependency relation).

Let U be a net. We call dependency relation of U the relation

≺ U h 0 , h n U ≡ V Π i<n h i h i+1 .
An agent is either a localised process h[P ], or a forwarder h k. We let a, b range over an arbitrary set of visible actions, and we define an LTS over nets:

[Loc] P h,a,U ---→ P h[P ] a → h[P ] U P h,a,mig k ------→ P h[P ] a → h k k{reg P } [Mig] [Fwd] h{M } h k τ → h k k{M } h{M } h[P ] τ → h[P | {M }] [Rcv] [New] U α → U h not free in U, U (νh)U α → (νh)U U α → U U V α → U V [Par] [Cong] U ≡ U α → V ≡ V U α → V h{M} h , a, mig k k h h k a [Mig] τ [Fwd] k k h h h{M} τ [Fwd] k k h h h {M} k k h h k {M} τ [Rcv] k h h k {M} 2 Fig. 1. Nets, Migration, Routing of Messages
This definition depends on a localised LTS, describing the behaviour of local processes: P h,a,K ----→ P stands for "process P , when located at h, evolves to P by performing a visible action a and emitting a request K". Such requests correspond to the primitives granted to local processes. They can be either:

a net U (rule [Loc]), containing messages to send or new localities to spawn; or a migration request mig k (rule [Mig]): the local process wants to suspend its execution and to send its state to k. In that case, the local process gets replaced by a forwarder that will transmit further messages to k.

The two silent transition rules are concerned with the routing of messages: rule [Fwd] defines the behaviour of forwarders: they transmit the messages; and rule [Rcv] performs the actual reception of a message at its final location.

A sequence of transitions is depicted in Fig. 1, where squares and triangles represent respectively localised processes and forwarders; the process located at h migrates to k and the message h {M } is routed to its final destination, k .

We assume the two properties below about the localised LTS:

If P h,
(4) expresses the fact that an additional message should not prevent a process from doing some localised transition. ( 5) prevents local processes from testing the equality of two locations. In some sense, this means that local processes should not be aware of the implementation details of the framework.

Definition 2.3 (Well-formedness).

A net is well-formed if for any of its reducts U , we have U ≡ (ν h)V for some h, V such that:

1. any agent of V is located at a location mentioned in h; 2. for any location h in h, there is exactly one agent located at h in V ; and 3. the dependency relation ≺ V is a partial order, whose maximal elements are the locations hosting localised processes.

In the sequel, we shall often omit the restrictions on locations that should appear in front of a well-formed net (ν h)V : they can be guessed from V .

Hypothesis 2.4. We assume that we are given only well-formed nets.

Remark 2.1 (On the expressiveness of the framework). Locations express only the logical distribution of processes. Hence, the second condition in our definition of well-formedness does not rule out the case where several locations are thought of as residing physically on the same device. Also, unlike in [START_REF] Sangiorgi | A Distributed Abstract Machine for Safe Ambients[END_REF][START_REF] Hirschkoff | A Correct Abstract Machine for Safe Ambients[END_REF], the processes are not required to be distributed along a tree structure, and there is no constraint on the communication topology: since messages may contain locations, π-calculus-like mobility of links is provided by the model. Independently, migration is subjective in our model: the process itself decides to migrate. Objective migration mechanisms (like the passivation available in the Kell-calculus [START_REF] Bidinger | The Kell Calculus: Operational Semantics and Type System[END_REF]) may be simulated by using messages to trigger migrations.

The main constraint imposed by the well-formedness hypothesis comes from the third point: the graph of the dependency relation is a forest whose roots are the localised processes, and no cycle of forwarders should be generated. This could happen, for example, if a process located at h migrates to some location pointing to h. We discuss the role of this hypothesis in Sect. 5. One possibility to prevent the creation of such cycles is to define a partial ordering of the local processes, and insure that all migration requests respect this ordering (this is the case in models like Ambients [START_REF] Cardelli | Mobile Ambients[END_REF], Kells [START_REF] Bidinger | The Kell Calculus: Operational Semantics and Type System[END_REF], or Seals [START_REF] Castagna | The Seal Calculus Revisited[END_REF]).

Reasoning up to Forwarders

In this section, we validate the behaviour of forwarders, by showing that behavioural equivalence is not sensitive to silent transitions ( τ → ⊆ ≈) and to the replacement of a forwarder by a substitution.

Even though this property happens to be sufficient for our needs in the sequel (see Sect. 4.2), it does not allow one in general to reason modulo forwarders in other bisimulation proofs: it is well known that weak bisimulation up to ≈ is not a correct technique [START_REF] Sangiorgi | The problem of "Weak Bisimulation up to[END_REF]. Therefore, we prove a stronger result using expansion ( ), the standard behavioural preorder that leads to the correct "bisimulation up to " technique. Interestingly, this allows us to use the up to transitivity technique enjoyed by expansion, so that our proof is actually easier. Definition 3.1 (Expansion). An expansion relation is a relation R such that for any α ∈ L, whenever P RQ we have:

-if P α → P then Q α → Q and P RQ for some Q , -if Q α → Q then P α ⇒ P and P RQ for some P .
Expansion, denoted by , is the union of all expansion relations. Theorem 3.2 (Bisimulation up to Expansion [START_REF] Sangiorgi | The problem of "Weak Bisimulation up to[END_REF]). Let R be a symmetric relation. If R evolves to R , then R ⊆ ≈.

Theorem 3.3 (Expansion up to Transitivity).

Let R be a relation. If for any α ∈ L, whenever P RQ we have:

-if P α → P then Q α → Q and P R Q for some Q , -if Q α → Q then P α ⇒ P and P RQ for some P , then R ⊆ .
Notice that transitivity is allowed only on one side in the previous theorem. Nevertheless, this is sufficient for the proof of the following proposition:

Proposition 3.4. Let U, V be two nets. If U τ → V then U V .
Proof. We show that the following relation is an expansion up to transitivity:

R τ → ∪ { h{reg P } h{M } W, h{reg (P | {M })} W } .
We need the up to transitivity technique to analyse the two cases below:

U ≡ h{M } h[P ] W R h[P | {M }] W ≡ V [Rcv] U a → h{M } h k k{reg P } W [Mig] R h k k{M } k{reg P } W [Fwd] R h k k{reg P | {M }} W a ← V [R, Mig] U ≡ h{reg P } h{M } h k R h{reg (P | {M })} h k ≡ V U τ → h{M } h k k{reg P } [Rcv] R h k k{M } k{reg P } [Fwd] R h k k{reg (P | {M })} τ ← V [R, Rcv]
The other cases are similar or straightforward.

The smallest bisimulation relation containing τ → is τ ⇒. Hence, proving the weaker result τ → ⊆ ≈ without using this expansion-based technique would require to check that τ ⇒ is a bisimulation, which is less tractable: while U and V differ only slightly when U τ → V , this is no longer the case when U τ ⇒ V .

We now define a forwarder erasure relation, that replaces a forwarder by the corresponding substitution and we show that this relation is contained in . Definition 3.5 (Forwarder erasure). We call forwarder erasure the following relation:

E { (νh)(h k U ), U [k/h] } .
Proposition 3.6. Let U, V be two nets. If U EV , then U V .

Proof. We check that E is an expansion relation: let U = (νh)(W h k) and

V = W [k/h].
-If U α → U , by using Hypothesis (5), we obtain V α → V with U EV , except in the following case, corresponding to the rule [Fwd]:

U ≡ (νh)(W h{M } h k) τ → (νh)(W h k k{M }) ≡ U ,
where we just check that U EV .

-If V α → V , again, by using Hypothesis (5), we obtain U α → U with U EV , except in the two following cases:

V ≡ W [k/h] k{M } k[P ] τ → W [k/h] k[P | {M }] ≡ V [Rcv] U ≡ (νh)(W h{M } h k k[P ]) τ → (νh)(W h k k{M } k[P ]) [Fwd] τ → (νh)(W h k k[P | {M }]) E V [Rcv] V ≡ W [k/h] k k k{M } τ → W [k/h] k k k {M } ≡ V [Fwd] U ≡ (νh)(W h{M } h k k k ) τ → (νh)(W h k k{M } k k ) [Fwd] τ → (νh)(W h k k k k {M }) E V [Fwd]
E and τ → are confluent and terminating relations (for the termination of τ →, we rely on the fact that the dependency relation of a well-formed net is a partial order). This allows us to define normal forms of nets, that will be used in Sect. 4: Definition 3.7 (Normalisation). We denote respectively by U ↓ and e(U ) the normal forms of U w.r.t. τ → and E. We say that a net U is normal

(resp. E- normal) if U = U ↓ (resp. U = e(U ↓ )).
By the two previous propositions, we have that a net expands its E-normal form. This makes it possible to restrict to E-normal nets in bisimulation proofs (see the proof of Theorem 4.17 for an example).

Theorem 3.8. For any well-formed net U , we have:

U e(U ↓ ) .
Proof. By definition of U ↓ and e(U ), this follows from Props. 3.4 and 3.6.

Notice that ( τ → ∪ E) is terminating and confluent, and that E preserves τ →normal forms. In particular, we have e(U ↓ ) ≡ e(U ) ↓ . The strategy that we impose in this theorem to compute the normal form of U is hence somehow arbitrary. However, this will ease the development in Sect. 4.

Optimisations of the Behaviour of Forwarders

The forwarder chains that are generated along the evolution of a net are the source of inefficiencies. For example, the message {M } in Fig. 1 will have to go trough three locations before reaching its final destination. In this section, we define an optimisation of the framework, that contracts such forwarder chains, and we prove the correctness of this optimisation, by showing that simple forwarders, as defined in the previous section, are behaviourally equivalent to the optimised ones.

Definition of the Optimisation

Optimised nets extend the syntax of nets by annotating pending messages with a list of locations: h{M } k ; introducing blocked forwarders: h k; adding a second kind of messages: relocation messages h go k .

Intuitively, the list that decorates a pending message contains the set of forwarder locations the message did pass through. Messages emitted by the underlying local processes will have an empty list, which will allow us to omit their annotation. Relocation messages are received only by blocked forwarders. Their effect is to redirect such forwarders to a destination closer to the location they indirectly point to.

We shall use the terminology 'simple net' to denote a net as defined in Sect. 2. Structural congruence is extended to optimised nets in the obvious way. We define over this extended syntax an optimised LTS, written α → o , by taking the rules of the initial LTS and replacing the silent transition rules ([Fwd] and [Rcv]) with the three rules below.

h{M } h h k τ → o h k k{M } h, h [OFwd] h{M } h h[P ] τ → o h[P | {M }] h go h [ORcv] h go k h k τ → o h k [OUpd]
When a forwarder transmits a message, it registers its location (rule [OFwd]), and enters a blocked state so that it will temporarily block further potential messages. Upon reception at the final location, a relocation message is broadcasted to the locations registered in the message (rule [ORcv]). The blocked forwarders located at these locations will finally update their destination accordingly (rule [OUpd]). This behaviour is illustrated in Fig. 2, where reversed, grey triangles correspond to blocked forwarders. Notice that forwarders have to block until they receive the relocation message: otherwise, a timestamps mechanism would be required, so that a forwarder can cleverly chose between two possibly distinct relocation messages. The definition of dependency relation is adapted by considering all forwarders uniformly, be they blocked or not. We have: Proposition 4.1. In the optimised LTS, for any reduct U of a simple, wellformed net, there exist h, V such that U ≡ (ν h)V and the following conditions hold:

1. the properties required in Def. 2.3 are satisfied; 2. for any blocked forwarder h k, h appears exactly once in the annotation of a pending message (h {M } h , with h ∈ h), or as the destination of a relocation message (h go h ); in both cases, we have h ≺ V h ; 3. any location registered in a pending message, or appearing as the target of a relocation message hosts a blocked forwarder.

In the sequel, we shall implicitly assume that any optimised net that we manipulate satisfies these hypotheses.

Correctness of the Optimisation

Unlike in the previous section, we cannot rely on expansion-based up-to techniques: neither silent transitions, nor the erasure of forwarders are contained in expansion. This comes from the race conditions introduced by the blocking behaviour of forwarders: for example, in Fig. 2, the message {N } has to wait for arrival of {M }. The very 'controlled' nature of expansion -the right-hand-side process has to be as fast as the left-hand-side process, at each step -cannot take into account the fact that {N } is closer to its destination at the end.

However, by proving that in the optimised setting, a net is bisimilar to its Enormal form (Theorem 4.16), the following restricted version of the bisimulation up to ≈ technique will be sufficient to prove the equivalence between the two systems (Theorem 4.17): we can restrict to τ →-normal forms, so that there is no silent challenge to play. , so that we need some bisimulation proof technique in order to be able to work with small and local candidate relations. We use for that the following technique from [START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF]. The following proposition will be used to prove the third point of Def. 4.3. ⇒ terminates, then B is a simulation.

We now have enough technical devices to embark in the proof of correctness. We first prove a lemma that will allow us to route messages to their destination. Lemma 4.6. Let U ≡ V h 0 {M } h be a net. Then we have:

U ≡ V h 0 {M } h Π i<n F i (h i , h i+1 ) h n [P ] U τ ⇒ o V h go h n Π i<n h i h n h n [P | { N } | {M }] k h n where F i (h, k) is either:
a forwarder: h k, or a blocked forwarder, together with a relocation message: h k h go k , or a blocked forwarder whose location is registered in a message blocking some other forwarders: h k k{N } h, k k k .

N and k are the messages and forwarder locations collected in Π i<n F (h i , h i+1 ).

Proof. The decomposition of U comes from the well-formedness hypothesis. We prove the reduction by induction over n: if n = 0 we just apply the rule [ORcv], otherwise we reason by case analysis on the shape of F 0 (h 0 , h 1 ):

a simple forwarder: h 0 h 1 : we transmit the message with rule [OFwd], apply the induction hypothesis (IH), and relocate the forwarder using rule [OUpd]:

U τ → o V h 0 h 1 h 1 {M } h0, h Π 0<i<n F (h i , h i+1 ) h n [P ] [OFwd] τ ⇒ o V h 0 h 1 (h 0 , h) go h n Π 0<i<n h i h n h n [P | { N } | {M }] k h n (IH) τ → o V h 0 h n Π i<n h i h n h n [P | { N } | {M }] k h n [OUpd]
a blocked forwarder with a relocation message: h 0 k h 0 go h 1 : we relocate the forwarder with rule [OUpd] and fall back into the previous case.

h 0 k h 1 {N 1 } h0, k1 k 1 k 1 : we apply the induction hypothesis to the message at h 1 , and transmit the initial message trough the relocated forwarder:

U τ ⇒ o V h 0 {M } h h 0 h 1 h 0 go h n Π 0<i<n h i h n h n [P | {N 1 , N }] k 1 k 1 k k (IH) τ → o V h 0 {M } h Π i<n h i h n h n [P | {N 1 , N }] k 1 k 1 k k [OUpd] τ → o 3 V h go h n Π i<n h i h n h n [P | {N 1 , N } | {M }] k 1 k 1 k k [OFwd,ORcv,OUpd] τ → o
does not commute with visible actions: some relocation of forwarders is involved. To handle this, we introduce the following relation, that allows one to reorganise step by step the forwarder structure of a net. Definition 4.7. We denote by S the swapping relation, defined as the symmetric closure of the following relation:

{ h h h k U, h k h k U } .
Our goal is to prove that (S∪ Again, thanks to the up-to technique, we avoid manipulation of complex relations, and focus on nets that differ only slightly (as in Def. 4.7).

Lemma 4.8. If U τ → o V and U a → o U then U τ ⇒ o S τ ⇐ o a ← o V . Proof. It holds that U τ → o a ← o V , except in the following case: U ≡ W h{M } h h[P ] τ → o W h[P | {M }] h go h ≡ V [ORcv] U a → o W h{M } h h k k{reg P } ≡ U [Mig]
where we have

V a → o W h k k{reg P | {M }} h go h ≡ V . [Mig]
We reason by case analysis on the agent located at k:

a localised process k[Q]: by routing to k the messages exhibited in U and V , we obtain:

U τ ⇒ o W (h, h) k k[Q | {reg P } | {M }] V τ ⇒ o W h h h k k[Q | {reg P | {M }}]
(the only message to route in V is almost at its final destination, and the relocation message has already been sent to the blocked forwarders located at h, so that the latter gets relocated under h instead of k).

Finally, we relocate these forwarders with n applications of the swapping relation, n being the length of h:

U τ ⇒ o S n τ ⇐ o V .
a forwarder k k : like in the previous case, we first route the available messages to their destination, say k :

U τ ⇒ o W (h, k, h) k k [Q | {reg P } | {M }] , V τ ⇒ o W h h h k k k k [Q | {reg P | {M }}] .
Here we need an additional application of the swapping relation to relocate h to k , before being able to relocate the forwarders at h:

U τ ⇒ o S n+1 τ ⇐ o V .
a blocked forwarder k k . We reason like in the previous case by first routing the message that blocks this forwarder to its destination.

-U ≡ W h{M } h h h h k τ → o W h h h {M } h, h h k ≡ U .
By routing the messages, we obtain:

U τ ⇒ o W h k h k k [Q | {M }] , V τ ⇒ o W h k h k k [Q | {M }] ≡ V .
If k = k , we are done. Otherwise, there is a forwarder k k , and we need one application of the swapping relation in order to relocate the forwarder located at h in V .

-U ≡ h h h {M } h h k τ → o h h h k k{M } h , h ≡ U
By routing the messages, we obtain:

U τ ⇒ o W h h h k k [Q | {M }] ≡ U , V τ ⇒ o W h k h k k [Q | {M }] ≡ V .
If k = k , we are done. Otherwise, there is a forwarder k k , and we need two applications of the swapping relation in order to relocate the forwarder located at h in both nets:

U ≡ W h h k k h k k [Q | {M }] S W h k k k h k k [Q | {M }] S W h k k k h k k [Q | {M }] ≡ V
This analysis also applies for the symmetric cases, where the silent transitions are played by the net with 'flat' forwarders. Proof. Using Prop. 4.1, the only critical pair is

U = V h{M } h h{N } k h k, U τ → o V h{M } h h k k{N } h, k = U 1 [OFwd] U τ → o V h{N } k h k k{M } h, h = U 2 [OFwd]
By using Lemma 4.6 on U 1 , we can route the message {N } to some location k :

U 1 τ ⇒ o V h{M } h h k (h, k) go k k [P | {N }] (Lemma 4.6) τ → o V h{M } h h k k go k k [P | {N }] [OUpd] τ → o 3 V ( k, h) go k h k k [P | {N } | {M }] ≡ U [OFwd,ORcv,OUpd]
The same reasoning about U 2 leads to U 2 τ ⇒ o U . Proof. We call size of a net U the triple s(U ) = n, r, l , where n is the number of pending messages, r the number of relocation messages, and l the number of forwarders that are not blocked. These triples are ordered lexicographically. We check that U SV implies s(U ) = s(V ), and that this size strictly decreases along silent transitions (recall that τ ⇒ o contains at least one transition). We now show that E ⊆ ≈. In order to avoid confusion, we consider in the sequel bisimilarity as a relation between rooted LTSs that share the same set of labels: U, → ≈ V, will denote the fact that U with labelled transition relation →, is bisimilar to V , with labelled transition relation .

Notice that we do not extend the erasure relation E to optimised nets; like e(.) it will only be used to reason about simple nets. -If U a → o U , then U is a simple net, and we check that

V a → o V with U EV . -If U τ → o U
, the interesting case is the following, when n > 1:

U ≡ (νh 0 )(W h 0 {M } Π i<n h i h i+1 h n [P ]) U τ → o U ≡ (νh 0 )(W h 0 h 1 h 1 {M } h0 Π 0<i<n h i h i+1 h n [P ]) U E V ≡ W [h 1 /h 0 ] h 1 {M [h 1 /h 0 ]} Π 0<i<n h i h i+1 h n [P [h 1 /h 0 ]])
By routing the message in both processes, we obtain:

U τ ⇒ o U ≡ (νh 0 )(W Π i<n h i h n h n [P | {M }]) V τ ⇒ o V ≡ W [h 1 /h 0 ] Π 0<i<n h i h n h n [P [h 1 /h 0 ] | {M [h 1 /h 0 ]}])
These processes are not related by E, we need first to relocate in U the forwarder located at h 0 under h 1 , using a 'reversed' application of S:

U τ ⇒ o U S (νh 0 )(W h 0 h 1 Π 0<i<n h i h n h n [P | {M }]) E V τ ⇐ o V .
-The cases where V α → o V are handled similarly.

Remark that we can also prove that (E ∪ S ∪ τ → o ) is a controlled relation. This would be useful if we had to reason up to E on some silent transitions. Notice that U ↓o is always a simple net: it does not contain any blocked forwarder, relocation message, nor pending, annotated messages. Furthermore, we have that an optimised net U is a normal net iff U = U ↓o . The normalisation of a simple net by τ → and τ → o does not necessarily lead to the same net: U ↓ ≡ U ↓o . However, these nets differ only by some rearrangement of their forwarders: they are related by S . As expressed by the proposition below, in order to obtain the same net, we just need to erase all the forwarders. Proposition 4.15. For any simple net U , we have: e(U ↓ ) ≡ e(U ↓o ) .

Proof. U SV entails e(U ) ≡ e(V ), therefore it is sufficient to prove that U ↓ S U ↓o . We proceed by well-founded induction on U , using the termination of τ →:

-If U is a normal net, we have U ↓ = U = U ↓o . -If U τ → U , since U is simple, U ≡ V h 0 {M } Π i<n h i h i+1 h n [P ] and: U τ → U τ ⇒ V Π i<n h i h i+1 h n [P | {M }] ≡ U 1 U τ ⇒ o V Π i<n h i h n h n [P | {M }] ≡ U 2 (Lemma 4.6)
We check that U 1 S n U 2 , and we have U 1 τ ⇒ o U 1↓o so that from Prop. 4.12,

U 2 τ ⇒ o U 2 with U 1↓o (S ∪ τ → o ) U 2 .
Furthermore, since S preserves normal forms, U 1↓o S U 2 , and U 2 = U 2↓o Finally, by induction, U 1↓ S U 1↓o and U

↓ = U 1↓ S U 1↓o S U 2↓o = U ↓o .
It follows that a net is bisimilar to its E-normal form, which leads to the final proof of correctness. The challenges offered by U, → are handled symmetrically.

Concluding Remarks

The bisimilarity proof in [START_REF] Hirschkoff | A Correct Abstract Machine for Safe Ambients[END_REF]. In the GCPAN [START_REF] Hirschkoff | A Correct Abstract Machine for Safe Ambients[END_REF], which is an optimisation of the PAN [START_REF] Sangiorgi | A Distributed Abstract Machine for Safe Ambients[END_REF], we actually add counters to the forwarders and garbage collect forwarders whose counter is 0, to which no message will be sent anymore. We can build on the results presented here to give a complete correctness proof, by validating each optimisation step. Because in PAN local processes satisfy the requirement of our framework, the PAN with relocating forwarders is equivalent to the original machine. Furthermore, adding counters to the machine does not affect this. We then show that the relation that removes a forwarder with counter 0 is a strong bisimulation. Finally, correctness of the GCPAN is established by checking that the identity relation is a bisimulation up to strong bisimilarity relating the previous nets and GCPAN nets.

Forwarder cycles. In this paper, we assumed that no forwarder cycles can appear during the evolution of a net (Hyp. 2.4). However, Theorem 4.17, that states the correctness of the optimisation, holds without this assumption. Indeed, in both systems, all forwarders belonging or pointing to a cycle, and messages routed along such forwarders, will get trapped in the cycle, rendering this part of the net behaviourally equivalent to the empty net:

-In the initial system, any message trapped in a cycle will keep moving indefinitely along the cycle, producing infinitely many silent transitions (the relation τ → remains confluent, but does no longer terminate). -In the optimised system, messages reaching the cycle will progressively block its forwarders ( τ → o still terminates, but it is no longer confluent: the shape of the final blocked cycle depends on the order of the reductions).

Furthermore, cycles can only be created by the visible rule [Fwd], and we can check that the set of messages and forwarders trapped in a cycle does not depend on the setting we chose. Hence, in the proof of Theorem 4.17, we could safely remove the cycles and lost messages that appear on both sides, the same way as we normalise processes along the bisimulation game.

  a,K ----→ P , then for any message M, P | {M } h,a,K ----→ P | {M }. (4) P h,a,K ----→ P iff for any substitution σ, P σ hσ,a,Kσ -----→ P σ.

Fig. 2 .

 2 Fig. 2. Optimised Forwarder Behaviour

Theorem 4 . 2 (

 42 Bisimulation up to Bisimilarity). Let R be a symmetric relation, if R evolves silently to itself and visibly to ≈ R ≈, then R ⊆ ≈. Like in Sect. 3, the smallest bisimulation relations containing τ → o or E contain at least τ ⇒ o

Definition 4 . 3 (

 43 Controlled relation). A relation B is a controlled relation if the following conditions hold: 1. B evolves to B , 2. B + τ ⇒ terminates, 3. B ⊆ ≈.

Theorem 4 . 4 (

 44 Bisimulation up to a Controlled relation[START_REF] Pous | Up-to Techniques for Weak Bisimulation[END_REF]). Let B be a controlled relation, if a symmetric relation R evolves to B R ≈, then R ⊆ ≈.

Proposition 4 . 5 .

 45 If B is a relation evolving to B and such that B + τ

τ

  → o ) is a controlled relation: this entails τ → o ⊆ ≈, but also makes it possible to give a nice proof of E ⊆ ≈ (Prop. 4.13), by using Theorem 4.4. The three following lemmas establish progressively that (S ∪ τ → o ) evolves to (S ∪ τ → o ) , so that this relation satisfies the first point of Def. 4.3.

Lemma 4 . 9 .

 49 If U SV and U α → o U then U τ ⇒ o S α ⇐ o V .Proof. It is immediate for visible challenges α = a: we have U S a ← o V . When α = τ , the interesting cases are those where the silent transition U τ → o U is the transmission of a message trough one of the two forwarders being swapped:

→

  o is locally confluent.

Lemma 4 .

 4 11. S τ ⇒ o terminates.

Proposition 4 .

 4 12. (S ∪ τ → o ) is a controlled relation. Proof. First we check that (S∪ τ → o ) satisfies the first two requirements of Def. 4.3: (1) comes from Lemmas 4.8, 4.9, and 4.10; by remarking that (S ∪ τ → o ) + τ ⇒ o = (S τ ⇒ o ) + , Lemma 4.11 gives (2). For (3), by Prop. 4.5, we have that (S ∪ τ → o ) is a simulation. Moreover, τ ← o is a simulation (as is always the case). By combining these two results we obtain that the symmetric relation (S ∪ τ ↔ o ) = ((S ∪ τ → o ) ∪ τ ← o ) is a simulation, and hence a bisimulation, so that (S ∪ τ → o ) ⊆ (S ∪ τ ↔ o ) ⊆ ≈.

Proposition 4 .

 4 13. Let U, V be simple nets.If U EV then U, → o ≈ V, → o .Proof. We show that the symmetric closure of the erasure relation E is a bisimulation up to the controlled relation (S ∪ τ → o ) (Theorem 4.4).

Lemmas 4 .

 4 11 and 4.10 ensure that τ → o defines a unique normal form for any net (termination of S τ ⇒ o entails termination of τ → o ). Definition 4.14. Let U be an optimised net. We denote by U ↓o the normal form of U w.r.t. τ → o .

Theorem 4 .

 4 16. Let U be an optimised net, we have:U, → o ≈ e(U ↓ ), → o .Proof. From Prop. 4.12, τ → o ⊆ ≈, and U ≈ U ↓o . We conclude with Props. 4.13 and 4.15: U ↓o ≈ e(U ↓o ) ≡ e(U ↓ ).

Theorem 4 .

 4 17 (Correctness of the optimisation). For any simple net U , we have:U, → o ≈ U, → .Proof. Using Theorems 4.16 and 3.8, we can suppose w.l.o.g. thatU is E-normal. Let R U, → o , U, → U is E-normal .We show that the symmetric closure of R is a bisimulation up to ≈ (Theorem 4.2): since U is normal, there are only visible challenges to play. Suppose U a → o U . The LTSs do not differ on visible actions, hence we have U a → U . U is not necessarily E-normal, so that U , → o R U , → does not hold. However, by Theorems 4.16 and 3.8, we have: U , → o ≈ e(U ↓ ), → o R e(U ↓ ), → ≈ U , → .

Acknowledgements. I would like to thank Daniel Hirschkoff, whose great help and comments have been essential during the preparation of this paper.


Jean Cochet-Terrasson

S T Éphane Gaubert

POLICY ITERATION ALGORITHM FOR ZERO-SUM STOCHASTIC GAMES WITH MEAN PAYOFF

We give a policy iteration algorithm to solve zero-sum stochastic games with finite state and action spaces and perfect information, when the value is defined in terms of the mean payoff per turn. This algorithm does not require any irreducibility assumption on the Markov chains determined by the strategies of the players. It is based on a discrete nonlinear analogue of the notion of reduction of a super-harmonic function. ALGORITHME D'IT ÉRATION SUR LES POLITIQUES POUR LES JEUX STOCHASTIQUES À SOMME NULLE AVEC GAIN MOYEN R ÉSUM É. Nous donnons un algorithme d'itération sur les politiques pour résoudre les jeux stochastiques à somme nulle, avec espaces d'état et d'action finis, en information parfaite, lorsque la valeur du jeu est définie en termes de gain moyen par tour. Cet algorithme ne demande pas que les chaînes de Markov déterminées par les stratégies des deux joueurs soient irréductibles. Il repose sur un analogue discret non-linéaire de la notion de réduite d'une fonction surharmonique.

VERSION ABR ÉG ÉE EN FRANC ¸AIS

Une application f définie sur R n est dite polyédrale si l'on peut recouvrir R n par un nombre fini de polyèdres de sorte que la restriction de f à chacun des polyèdres soit affine.

Une application f : R n → R n est dite contractante pour une norme • si f (x)-f (y) ≤

x -y . Kohlberg [12] a démontré que si f : R n → R n est polyédrale et contractante pour une norme quelconque, on peut trouver des vecteurs v et η dans R n tels que f (v + tη) = v + (t + 1)η, pour tout réel t assez grand. Nous appellerons demi-droite une application de la forme t → v + tη, et nous dirons qu'elle est invariante (relativement à f ) si elle

vérifie la propriété précédente. L'intérêt d'une demi-droite invariante est qu'elle détermine le taux de croissance des orbites de f , χ(f ) := lim k→∞ f k (x)/k, où l'on désigne par f k la k-ième itérée de f , et où x désigne un vecteur quelconque de R n . On vérifie en effet que

χ(f ) = η.
Dans cette note, nous donnons un algorithme pour calculer une demi-droite invariante lorsque l'application polyédrale f est croissante au sens large (pour l'ordre partiel usuel de R n ) ainsi qu'additivement homogène, ce qui signifie qu'elle commute avec l'addition d'un vecteur constant. Voir [START_REF] Gaubert | The Perron-Frobenius theorem for homogeneous, monotone functions[END_REF] pour plus de détails sur cette classe d'applications. Ce travail est motivé par l'étude des jeux stochastiques à deux joueurs et à somme nulle, en information parfaite, avec gain moyen. Lorsque l'espace d'états est {1, . . . , n}, et lorsque les espaces d'actions sont finis, l'opérateur de programmation dynamique du jeu vérifie les hypothèses précédentes. La coordonnée χ i (f ) fournit la valeur du jeu lorsque l'état initial est i.

Notre algorithme étend l'itération sur les politiques de Howard [START_REF] Howard | Dynamic Programming and Markov Processes[END_REF], qui s'applique au cas à un seul joueur. Hoffman et Karp [START_REF] Hoffman | On nonterminating stochastic games[END_REF] ont donné une première généralisation au cas à deux joueurs, cependant, leur méthode exige que les matrices de Markov induites par un couple quelconque de stratégies stationnaires des deux joueurs soient irréductibles. Sinon, on rencontre des itérations dégénérées, dans lesquelles la nouvelle stratégie qui est choisie n'améliore pas nécessairement la valeur de la précédente. L'algorithme peut alors cycler.

Nous résolvons ici cette difficulté en incorporant dans chaque itération dégénérée un analogue non-linéaire du calcul de la réduite d'une fonction surharmonique, ce qui revient à résoudre un problème auxiliaire d'arrêt optimal (à un joueur), assurant ainsi la terminaison de l'algorithme. Ceci étend au cas stochastique les algorithmes développés par Gunawardena et les auteurs [START_REF] Gaubert | The duality theorem for min-max functions[END_REF][START_REF] Cochet-Terrasson | A constructive fixed point theorem for min-max functions[END_REF] dans le cas des jeux déterministes. La preuve exploite des résultats d'Akian et du second auteur [START_REF] Akian | Spectral theorem for convex monotone homogeneous maps, and ergodic control[END_REF], sur la structure de l'ensemble des points fixes d'une application convexe, croissante, additivement homogène. L'existence d'un algorithme polynômial pour calculer χ(f ) est un problème ouvert [START_REF] Condon | The complexity of stochastic games[END_REF][START_REF] Bjorklund | A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games[END_REF][START_REF] Jurdziński | A deterministic subexponential algorithm for solving parity games[END_REF]. Signalons qu'une version préliminaire du présent travail est apparue dans [START_REF] Cochet-Terrasson | Algorithmes d'itération sur les politiques pour les applications monotones contractantes[END_REF].

Présentons maintenant l'analogue non-linéaire de la notion de fonction surharmonique réduite utilisé dans l'algorithme. Soit g : R n → R n une application convexe, croissante, additivement homogène, telle que χ(g) = 0. Un vecteur u ∈ R n est dit harmonique (relativement à g) si g(u) = u. Il est dit surharmonique si g(u) ≤ u. Rappelons quelques définitions et résultats de [START_REF] Akian | Spectral theorem for convex monotone homogeneous maps, and ergodic control[END_REF]. Supposons qu'il existe au moins un vecteur harmonique, u. Nous définissons le sous-différentiel de g au point u, ∂g(u Une stratégie (stationnaire, en boucle fermée) est une application σ de {1, . . . , n} dans

) := {M ∈ R n×n | g(x) -g(u) ≥ M (x -u), ∀x ∈ R n },
∪ 1≤i≤n A i telle que σ(i) ∈ A i .
Pour toute stratégie σ, nous désignons par f (σ) l'application de R n dans lui même dont la i-ième coordonnée est donnée par f

(σ) i = f σ(i) i
.

Algorithme 1 (Itération sur les politiques pour les jeux stochastiques). Donnée : Une application f dont les coordonnées sont de la forme [START_REF] Bjorklund | A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games[END_REF]. Résultat : Une demi-droite invariante de f .

(1) Initialisation. Choisir une stratégie arbitraire σ 1 , et calculer une demi-droite invariante de f (σ1) , w (1) (t) = v (1) + tη (1) . Poser k = 1.

(

) Si f • w k (t) = w k (t + 1 2
) a lieu pour t assez grand, l'algorithme s'arrête.

(3) Sinon, améliorer la stratégie en sélectionnant une nouvelle strategie σ k+1 telle

que f • w k (t) = f (σ k+1 ) • w k (t)
(i) = σ k (i) si f i • w k (t) = f (σ k ) i
• w k (t) pour t assez grand.

(4) Calculer une demi-droite invariante arbitraire w(t) = v + tη de f (σ k+1 ) . Si η = η (σ k ) , on pose w k+1 = w. Si η = η (σ k ) , l'itération est qualifiée de dégénérée, et on pose

w k+1 = Q f (σ k+1 ) w k . On définit v k+1 et η (σ k+1 ) par w k+1 (t) = v k+1 + tη (σ k+1 ) .
( Ce résultat est démontré à l'aide du Théorème 1. On montre notamment que χ(f

) 5
(σ k+1 ) ) ≤ χ(f (σ k ) ), et que si χ(f (σ k+1 ) ) = χ(f (σ k ) ), on a w k+1 ≤ w k , w k+1 i = w k i pour tout i ∈ C(f (σ k+1 ) ), et C(f (σ k+1 ) ) ⊂ C(f (σ k ) ).

INTRODUCTION

A map f defined on R n is polyhedral if there is a covering of R n by finitely many polyhedra such that the restriction of f to any of these polyhedra is affine. A self-map f of [START_REF] Kohlberg | Invariant half-lines of nonexpansive piecewise-linear transformations[END_REF] showed that if f is a polyhedral self-map of R n that is nonexpansive in some norm, then, there exist

R n is nonexpansive in a norm • if f (x) -f (y) ≤ x -y . Kohlberg
two vectors v and η in R n such that f (v + tη) = v + (t + 1)η, for all t ∈ R large enough. A map of the form t → v + tη is called a half-line. It is invariant if it satisfies the latter
property. The interest of an invariant half-line is that its linear part determines the growth rate of the orbits of f , χ(f ) := lim k→∞ f k (x)/k. Here, f k denotes the k-th iterate of f , and x is an arbitrary vector of R n . If f has an invariant half-line t → v + tη, then, χ(f ) does exist and is equal to η.

In this note, we give an algorithm to compute an invariant half-line, when the polyhedral map f satisfies the following conditions. We require f to be order-preserving, meaning that x ≤ y =⇒ f (x) ≤ f (y), where ≤ denotes the standard ordering of R n . We also require f to be additively homogeneous, meaning that it commutes with the addition of a constant vector. These two conditions imply that f is nonexpansive in the sup-norm.

(See [START_REF] Gaubert | The Perron-Frobenius theorem for homogeneous, monotone functions[END_REF] for more background on this class of nonlinear maps.)

This work is motivated by the study of zero-sum two players stochastic games with perfect information and mean payoff. When the state space is {1, . . . , n}, and when the action spaces are finite, the dynamic programming operator of the game satisfies the previous assumptions. The coordinate χ i (f ) gives the value of an infinite game with mean payoff, in which the initial state is i and the payoff of the infinite trajectory induced by a pair of strategies of the two players is defined as the Cesaro limit of the expectations of the payoffs of the successive transitions.

Our algorithm extends Howards' policy iteration algorithm [START_REF] Howard | Dynamic Programming and Markov Processes[END_REF], which applies to the one player case. Hoffman and Karp [START_REF] Hoffman | On nonterminating stochastic games[END_REF] gave a partial extension to the two players case.

However, their method requires every Markov chain associated to a pair of stationary feedback strategies of the two players to be irreducible. If this assumption does not hold, degenerate iterations may occur, in which the new strategy which is selected may not have an improved value. Then, the algorithm may cycle.

We solve this difficulty by computing a non-linear analogue of a reduced super-harmonic function, at each degenerate iteration, which requires solving an auxiliary (one player) optimal stopping problem. This is intimately related with Perron's method in the study of the Dirichlet problem. The present algorithm extends the ones which have been developed by the authors and Gunawardena [START_REF] Gaubert | The duality theorem for min-max functions[END_REF][START_REF] Cochet-Terrasson | A constructive fixed point theorem for min-max functions[END_REF] in the case of deterministic games. Its proof exploits earlier results of Akian and the second author [START_REF] Akian | Spectral theorem for convex monotone homogeneous maps, and ergodic control[END_REF], on the structure of the fixed point set of a convex order-preserving additively homogeneous map. The existence of a polynomial time algorithm to compute χ(f ) is an open question [START_REF] Condon | The complexity of stochastic games[END_REF], even in the deterministic case [START_REF] Bjorklund | A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games[END_REF][START_REF] Jurdziński | A deterministic subexponential algorithm for solving parity games[END_REF].

Finally, we note that a preliminary account of the present work has appeared in [START_REF] Cochet-Terrasson | Algorithmes d'itération sur les politiques pour les applications monotones contractantes[END_REF].

REDUCED SUPER-HARMONIC VECTORS AND POLICY ITERATION ALGORITHM

We first present the non-linear analogue of a result of classical potential theory, on which the algorithm relies. Assume that g is a self-map of R n that is convex, order preserving, additively homogeneous, with χ(g) = 0. We say that a vector u ∈ R n is harmonic (with respect to g) if g(u) = u, and that it is super-harmonic if g(u) ≤ u. Let us recall some definitions and results of [START_REF] Akian | Spectral theorem for convex monotone homogeneous maps, and ergodic control[END_REF]. Assume that there exists at least one harmonic vector, u.

The subdifferential of g at point u is defined by ∂g(u)

:= {M ∈ R n×n | g(x) -g(u) ≥ M (x -u), ∀x ∈ R n }.
This set consists of stochastic matrices. We say that a node is critical if it belongs to a recurrence class of some matrix M ∈ ∂g(u). The set of critical nodes is independent of the choice of the harmonic vector u. Indeed, when g arises from a stochastic control problem with ergodic reward, a node is critical iff it is recurrent for some stationary optimal strategy. If I is any subset of {1, . . . , n}, we denote by r I the restriction from R n to R I , such that (r I x) i := x i , for all i ∈ I. For all u ∈ R n , we define u I := r I u.

Let J := {1, . . . , n}\I. We define the map g I := r I •g, and we denote by ı I the canonical map identifying R I × R J to R n , which sends (y, z) to the vector u such that u i = y i for all i ∈ I and u i = z i for all i ∈ J.

Theorem 1. Let g denote a convex, order preserving, and additively homogeneous selfmap of R n . Assume that g admits at least one harmonic vector. Let C denote the set of critical nodes of g, let N denote the complement of C in {1, . . . , n}, and let u denote a super-harmonic vector. Then, any of the following conditions defines uniquely the same vector v: (i) v is harmonic and coincides with u on C; (ii) v is the smallest super-harmonic vector that dominates u on C; (iii) v coincides with u on C and its restriction to N is the unique fixed point of the map y → g N (ı N (y, u C )).

We denote by Q g u the unique harmonic vector v defined in Theorem 1. When g(x) = M x is a linear operator, and M is a stochastic matrix, Q g u coincides with the reduced super-harmonic vector of u with respect to the set C. When g is a max-plus linear operator, the operator Q g coincides with the spectral projector which has been defined in the maxplus literature, see [START_REF] Cochet-Terrasson | A constructive fixed point theorem for min-max functions[END_REF]. For this reason, we call Q g the (nonlinear) spectral projector of g.

Let us now explain how to compute Q g u when g is polyhedral. Assume that every coordinate g i is given as follows:

g i (x) = max b∈Bi r b i + P b i x , (1)
where B i is a finite set, r b i ∈ R, and P b i is a stochastic (row) vector. Note first that an invariant half-line of g can be computed by applying the multichain policy iteration algorithm of Denardo and Fox [START_REF] Denardo | Multichain Markov Renewal Programs[END_REF]. This provides χ(g), together with an harmonic vector of g when χ(g) = 0. Once an harmonic vector of g is known, the set of critical nodes can be computed by the algorithm of [1, §

. Hence, to compute v := P g u, it suffices to apply the standard fixed point iteration to the latter map. Alternatively (experiments indicate this is faster), one may note that the vector y solution of y = g N (ı N (y, u C )) is the value of an optimal stopping problem, in which the process dies when reaching the set C.

This vector can be computed by the original policy iteration algorithm of Howard [START_REF] Howard | Dynamic Programming and Markov Processes[END_REF].

We now define a spectral projector acting on half-lines. We assume that g is a polyhedral, convex, order preserving, and additively homogeneous self-map of R n . Let η := χ(g), and define ḡ(x) := lim t→∞ g(x + tη) -(t + 1)η. Since g is polyhedral, the limit is attained for all sufficiently large t. Indeed, if the coordinates of g are of the form (1), we have ḡi (x) = max b∈ Bi -η i + r b i + P b i x, where Bi is the set of actions b attaining the maximum in max b∈Bi P b i η. We define the set of critical nodes of g, C(g), to be the set of critical nodes of ḡ. An half-line

w(t) = v + tη is super-invariant if g • w(t) ≤ w(t + 1),
for t large enough.

Corollary 1. Assume that g is a polyhedral, convex, order preserving, and additively homogeneous self-map of R n . Assume that w(t) = v + tη is a super-invariant half-line of g with η = χ(g). Then, there exists a unique invariant half-line of g which coincides with w on the set of critical nodes of g. It is given by t → Q ḡ v + tη.

We define Q g w to be the map t → Q ḡ v + tη. In order to present the algorithm, we assume that every coordinate of f is given by:

f i (x) = inf a∈Ai f a i (x) , (2)
where A i is a finite set, and f a i is a polyhedral order preserving, additively homogeneous, and convex map from R n to R. We call (stationary, feedback) strategy a map σ from {1, . . . , n} to ∪ 1≤i≤n A i such that σ(i) ∈ A i . For all strategies σ, we denote by f (σ) the self-map of R n the i-th coordinate of which is given by f

(σ) i = f σ(i) i
.

Algorithm 1 (Policy iteration for stochastic games). Input: A map f the coordinates of which are of the form (2). Output: An invariant half-line of f .

(1) Initialisation. Select an arbitrary strategy σ 1 . Compute an invariant half-line of f (σ1) , w (1) (t) = v (1) + tη (1) . Set k = 1.

(

) If f • w k (t) = w k (t + 1 2
) holds for t large enough, the algorithm halts.

(3) Otherwise, improve the strategy, by selecting a strategy σ k+1 such that f •w k (t) = f (σ k+1 ) • w k (t), for t large enough. The choice of σ k+1 must be conservative,

meaning that σ k+1 (i) = σ k (i) if f i • w k (t) = f (σ k ) i
• w k (t), for t large enough.

(4) Compute an arbitrary invariant half-line

w(t) = v + tη of f (σ k+1 ) . If η = η (σ k ) ,
we set w k+1 = w. If η = η (σ k ) , we say that the iteration is degenerate. Set

w k+1 = Q f (σ k+1
) w k , and define v k+1 and η (σ k+1 ) by w k+1 (t) = v k+1 +tη (σ k+1 ) .

(5) Increment k by one and go to step 2.

Theorem 2. A strategy cannot be selected twice, and so, the algorithm terminates.

This result is proved using Theorem 1. We show, as intermediate results, that χ(f (σ k+1 ) ) ≤ χ(f (σ k ) ), and that, when χ(f

(σ k+1 ) ) = χ(f (σ k ) ), we have w k+1 ≤ w k , w k+1 i = w k i for all i ∈ C(f (σ k+1 ) ), and C(f (σ k+1 ) ) ⊂ C(f (σ k ) ).
Let us give the missing details in the implementation of Algorithm 1, when every map f a i is given by f a i = sup b∈B a i r ab i + P ab i x, where B a i is a finite set, r ab i ∈ R, and P ab i is a stochastic vector. Then, for all strategies σ, f σ is the dynamic programming operator of a Markov decision process with finite state and action spaces. Recall that an invariant half-line of f (σ) can be computed by applying the policy iteration algorithm for multichain Markov decision processes [START_REF] Denardo | Multichain Markov Renewal Programs[END_REF]. The next state is to evaluate the asymptotic behaviour of

f i (x) = 1 2 max j: (i,j)∈E r ij + x j + min j: (i,j)∈E r ij + x j
arises as the dynamic programming operator of a variant with mean payoff of the "tug of war" game [START_REF] Peres | Tug-of-war and the infinity Laplacian[END_REF] and in a class of auction games [START_REF] Lazarus | Combinatorial games under auction play[END_REF]. Let us apply the algorithm to the complete graph with 3 nodes, with the weights r 11 = 1, r 12 = 2, r 13 = 7, r 21 = 3, r 22 = 3, r 23 = 4, r 31 = 8, r 32 = 5, r 33 = 1. The action space in every state i can be identified with {1, . . . , 3}. Let us choose the greedy strategy σ 1 , such that σ 1 (1) = 1, σ 1 (2) = 1, σ 1 (3) = 3. The corresponding operator is given by f (σ1) (x) = (1 +

x 1 + max(1 + x 1 , 2 + x 2 , 7 + x 3 ))/2, (3 + x 1 + max(3 + x 1 , 3 + x 2 , 4 + x 3 ))/2, (1 +

x 3 + max(8 + x 1 , 5 + x 2 , 1 + x 3 ))/2 T . We compute an invariant half-line of f (σ1) by the algorithm of [START_REF] Denardo | Multichain Markov Renewal Programs[END_REF]. We obtain for instance w 1 = v 1 + tη 1 , where v 1 = (0.5, 0, 1) T and η 1 = (λ, λ, λ) T , with λ := 4.25. Since f (w 1 (t)) < f (σ1) (w 1 (t)), we improve the policy. We get σ 2 (1) = 1, σ 2 (2) = 2, σ 2 (3) = 3. One can check, again by the algorithm of [START_REF] Denardo | Multichain Markov Renewal Programs[END_REF], that χ(f (σ2) ) = (λ, λ, λ) T , and so, the iteration is degenerate. Using the algorithm of [1, § 6.3], we get that the set C of critical nodes of f (σ2) is {1, 3}, and so, N = {2}. Let g := f (σ2) . By Corollary 1, the image of w 1 by the spectral projector Q g is of the form z + tη (1) , where z 1 = v 1 1 , z 3 = v 1 3 , and z 2 is obtained by solving the equation 4.25 + z 2 = (3 + z 2 + max(3 + z 1 , 3 + z 2 , 4 + z 3 ))/2. The unique solution is z 2 = -0.5 (in general, this solution could be found by the basic policy iteration algorithm of [START_REF] Howard | Dynamic Programming and Markov Processes[END_REF]). So, w (2) (t) = (0.5, -0.5, 1) T + t(λ, λ, λ) T is an invariant half-line of f (σ2) .

Since f (w 2 (t)) = w 2 (t + 1), the algorithm stops, showing that χ(f ) = (λ, λ, λ) T .

  Nous définissons l'application g I := r I • g, et désignons par ı I l'application identifiant canoniquement R I × R J à R n , laquelle envoie (y, z) vers le vecteur x tel que x i = y i pour tout i ∈ I et x i = z i pour tout i ∈ J. Définissons l'application ḡ(x) := lim t→∞ g(x + tη) -(t + 1)η. Les coordonnées de ḡ sont données par ḡi (x) = max b∈ Bi -η i +r b i +P b i x, où Bi est l'ensemble des b atteignant le maximum dans l'expression max b∈Bi P b

	Nous définissons maintenant un opérateur analogue à Q g agissant sur les demi-droites.
	Nous supposons pour cela que g : R n → R n est polyédrale, convexe, croissante, et additi-
	vement homogène, et que sa i-ième coordonnée est donnée par l'expression (1) ci-dessous,
	dans laquelle B i est un ensemble fini, r b i ∈ R, and P b i est un vecteur (ligne) stochastique.
	Soit η := χ(g).
	Théorème 1. Soit g : R n → R n une application convexe, croissante, additivement ho-
	mogène, admettant au moins un vecteur harmonique. Soit C l'ensemble des noeuds cri-
	tiques de g, N := {1, . . . , n} \ C, et soit u un vecteur surharmonique. L'une quelconque
	des conditions suivantes définit de manière unique le même vecteur v : (i) v est harmonique
	et coïncide avec u sur C ; (ii) v est le plus petit vecteur surharmonique majorant u sur C ;
	(iii) v coïncide avec u sur C, et sa restriction à N est l'unique point fixe de l'application
	y → g N (ı N (y, u C )).
	Nous notons Q g u l'unique vecteur harmonique v défini dans le Théorème 1. Lorsque
	g(x) = M x est linéaire, et que la matrice M est stochastique, Q g u coïncide avec la réduite
	du vecteur surharmonique u relativement à l'ensemble C. Le calcul de Q g u est équivalent
	à la résolution d'un problème d'arrêt optimal, qui peut être menée par itération sur les
	politiques [6].

et notons que cet ensemble est formé de matrices stochastiques. Un noeud est dit critique s'il appartient à une classe de récurrence d'une des matrices M ∈ ∂g(u). L'ensemble des noeuds critiques est indépendant du choix du vecteur harmonique u. En fait, lorsque g provient d'un problème de contrôle stochastique avec critère ergodique, un noeud est critique si et seulement si il est récurrent pour une stratégie stationnaire optimale. Pour tout sous-ensemble I ⊂ {1, . . . , n}, et pour tout vecteur x ∈ R n , nous notons r I x ∈ R N la restriction de x, définie par (r I x) i := x i , Nous posons x I := r I x, Soit J := {1, . . . , n} \ I. i η. L'ensemble des noeuds critiques de g, C(g), est par définition l'ensemble des noeuds critiques de ḡ. Nous dirons qu'une demi-droite w(t) est surinvariante si g • w(t) ≤ w(t + 1), pour t assez grand. Corollaire 1. Soit g : R n → R n une application polyédrale, convexe, croissante, et additivement homogène. Soit w(t) = v + tη une demi-droite surinvariante de g, telle que η = χ(g). Il existe une unique demi-droite invariante de g qui coïncide avec w sur l'ensemble des noeuds critiques de g. Elle est donnée par t → Q ḡ v + tη. Nous posons Q g w(t) := Q ḡ v + tη. Dans la suite, nous supposons que chaque coordonnée f i de f est donnée par (2), où A i est un ensemble fini, et où chaque f a i est une application polyédrale croissante, additivement homogène, et convexe, de R n dans R.

  f • w(t), where w(t) is an half-line, as t tends to infinity. Computing the sum of two half-lines, multiplying an half-line by a scalar, and computing the infimum or supremum of two half-lines when t tends to infinity, are linear time operations. It follows that f • w(t) can be evaluated (Step 2) in a time which is linear in the size of the coding of the operator f , and a strategy σ k+1 satisfying the conditions of Step 3 is obtained as a byproduct of this evaluation.

Example 1. Consider a directed graph, with set of nodes 1, . . . , n and set of arcs E ⊂ {1, . . . , n} 2 , in which each arc (i, j) is equipped with a weight r ij ∈ R. The map f defined by: