Aurélien Deharbe

Frédéric Peschanski

The Omniscient Garbage Collector: a Resource Analysis Framework (extended abstract)

The notion of resource plays a central role in concurrent systems. In its purest form a resource is simply a unique identity one can create, use and ultimately destruct. In this paper we propose a simple yet effective characterization of resource usages and develop for it a complete analysis framework. We address qualitative issues such as the classification of resources and whether two systems exhibit similar patterns of resource usages -namely equivalent resource profiles. From the quantitative point of view, we develop the omniscient garbage collector (OGC), which decides precisely when a resource can be reclaimed or reused. This allows to bound precisely the number of resources consumed by a given system. To illustrate the approach, we study experimentally the resource consumption of pi-calculus processes using a prototype analysis tool. We propose two different resource abstractions for pi-processes: one based on the labelled transitions for open systems, and another one for closed systems. The latter notably provides a refined view of behaviors, less opaque than reductions. Beyond this experiment, the proposed framework is quite generic and can apply to many different formalisms and situations.

I. INTRODUCTION

The notion of resource plays a central role in the study of computational systems, and even more critically in the realm of concurrency. If we abstract from its internal structure, a resource becomes a pure name [START_REF] Gordon | Notes on nominal calculi for security and mobility[END_REF], i.e. an object with a globally unique and testable identity. This is the specialty of nominal calculi in general, and the π-calculus [START_REF] Sangiori | The π-calculus: a Theory of Mobile Processes[END_REF] in particular. Despite their lack of structure, the pure names display the primordial life-cycle of resources: (1) dynamic allocation, (2) arbitrary usage orderings, and (3) non-trivial garbage collection semantics, the latter point being central in our study.

Our work begins with a very simple graphical characterization of resource usages. To analyze these so-called resource graphs, we develop a recursive computation principle upon which most of our algorithms are built, together with an inductive principle to reason about their properties and a modular characterization of their complexity. Beyond the algorithmic contingency, our principal means of abstraction is a formal language -namely the resource profile -that can be roughly seen as a "regular-language up-to α-conversion" over resource usages. Testing resource profile equivalence reveals, we think, much about the internal behavior of the compared systems. This comes at the price of PSPACE-hardness in terms of computational complexity.

Resource consumption represents the quantitative facet of our study. An interesting indicator is the resource bound which confines the number of resources required for the correct execution of a given system. Ultimately, the least of such bounds -namely the resource index -represents a profound semantic characteristic of the behavior under study. In practice, the objective is to design an allocator for resources which is able to reuse as much locations as possible, while maintaining a strong invariant of conflict-freedom. Computing the resource index requires an omniscient garbage collector, a NP-complete problem tightly connected to the perfect coloring of so-called conflict graphs.

Beyond the complexity results, we aim at the development of practical tools for the analysis of resource usage in concurrent systems. Using an early prototype, we propose a couple of experiments of resource consumption in the realm of the π-calculus. To illustrate the versatility of the approach, we propose two different resource abstractions for π-processes: one based on the labelled transitions for open systems, and another one for closed systems. The latter notably provides a refined view of behaviors, less opaque than reductions. For this we introduce "slice-π", a rather standard π-calculus extended with an alternative restriction operator that allows to "slice" the behaviors so that a flexible notion of environment is reintroduced. In all the experiments we observe the same phenomenon -which reinforces a strong belief -that the apparent intractability of some of the proposed algorithms, especially the computation of the resource index, is largely compensated by the small size of the objects on which they apply. Indeed, most of the examples we explored (especially the "classical" π-calculus benchmarks), yield very small conflict graphs in comparison to the state space of the analyzed processes: in the order of at most a few dozen nodes for systems with more that 100 000 states! Moreover, it seems rather improbable that highly irregular conflict graphs can be easily constructed except on purpose. Complementarily, less tight but still low resource bounds can be computed very efficiently.

The outline of the paper is as follows. In Section II we establish the resource model that forms the theoretical basis of our analysis framework. The latter is developed in Section III in three steps: (1) a procedure of lattice completion resulting in generic recursive computation and inductive reasoning principles, (2) the omniscient garbage collector for the computation of resource bounds and index, and (3) an algorithmic approach to the resource equivalence problem. Our experimental study with the π-calculus is described in Section IV. A panorama of related work is given in Section V.

In this extended abstract the justification of mathematical statements is most of the time omitted or discussed informally. The complete proofs are detailed in a dedicated appendix.

II. RESOURCE MODEL

The purpose of a resource model is to abstract the manipulation of dynamic resources from concrete system behaviors, so that we can reason about them in isolation.

Definition 1 (resource graph):

Let R be a countably infinite set of resource variables ranging over X, Y, Z, . . . A resource graph G is a connected directed graph R, V, E, α, γ, δ with :

• R ⊆ R a finite 1 set of resource variables, also denoted by vars(G).

• V a finite set of vertices, and E ⊆ V × V a finite set of edges, such that there is a unique root v ⊥ ∈ V s.t. ∀v ∈ V, (v, v ⊥ ) / ∈ E and a unique tail v ⊤ s.t. ∀v ∈ V, (v ⊤ , v) / ∈ E.

• α(resp. γ, δ) : V → 2 R an allocation (resp. usage, delete) function(s) such that:

α(v ⊥ )∪α(v ⊤ )∪γ(v ⊥ )∪ γ(v ⊤ ) ∪ δ(v ⊥ ) ∪ δ(v ⊤ ) = ∅.
An example of a resource graph is depicted on the left part of Fig. 1. It has eight resource variables A . . . H (the emphasized vertices and dashed edges will be explained later) and is sufficiently non-trivial so that it exhibits most of the "corner cases" of the model.

The properties of resource graphs we are interested in can be characterized as properties about finite paths, falling in two categories: complete paths and lassos. Definition 2 (complete path and lasso): A complete path of a resource graph G with edge set E is of the form

ρ = v ⊥ → • • • → v ⊤ with pairwise distinct vertices. A lasso is a finite path ρ = v 1 → • • • → v n such that v 1 = v ⊥ and ∀i, j, 1 ≤ i < j ≤ n, v i = v j and ∃e, 1 < e ≤ n, v n → v e ∈ E.
The vertex v e is called the entry of the lasso and v n its exit.

There are only two complete paths in the graph of Fig. 1:

v ⊥ → v 1 → v k → . . . → v 6 → v 8 → v 11 → v ⊤ with v k = v 2 or v k = v 3 . There are six lassos, an example being v ⊥ → v 1 → v 3 → v 4 → . . . → v 6 → v 8 with entry v 4 .
We impose only minimal constraints on the nature and usage of resources in resource graphs, although some usage patterns must be enforced.

Definition 3:

A resource graph G has correct resource usage iff for each resource X ∈ vars(G) it has at most one vertex v such that X ∈ α(v), and for each finite path

ρ = v 1 → • • • → v n of G there is at most one vertex v in ρ such that X ∈ δ(v). Moreover, if ∃j, 1 ≤ j ≤ n s.t. X ∈ γ(v j ) then ∃i, 1 ≤ i ≤ j s.t. X ∈ α(v i ) and: • if ρ is a complete path then: ∃k, j ≤ k ≤ n s.t. X ∈ δ(v k )
• if ρ is a lasso with entry v e then:

• (dynamic) ∃k, j ≤ k ≤ n s.t. X ∈ δ(v k ) if i ≥ e or ∀l, e ≤ l ≤ n, X / ∈ γ(v l ) • (static) ∀k, 1 ≤ k ≤ n, X / ∈ δ(v k ) otherwise.
The reasons behind most constraints are obvious, i.e. any resource is allocated only once globally, and deleted at most once in each path. For a resource used in a given path, a basic principle is that it must be preceded by an allocation and followed by a deletion. However, some subtlety arise because of the cyclic nature of the lassos. Suppose a resource X allocated at some vertex v i and used at v j (j ≥ i) in a lasso with entry v e . There are two cases to consider depending on whether X should "survive" the cycle or not. In the dynamic case X must be deleted at some vertex v k with k ≥ j. This corresponds to two possible situations: (1) the allocation is performed after the lasso entry (thus, within the cycle), or (2) the resource is not used within the cycle. Considering the lasso

v ⊥ → v 1 → v 3 → v 4 → . . . → v 6 → v 8
with entry v 4 in Fig. 1, then situation (1) applies to resources A and B and situation (2) applies to resource H which is allocated before the entry but not used within the cycle. Complementarily, if the allocation of X is performed before the entry and it is used within the cycle, then X must "survive" the cycle and is thus said a static resource. For the lasso v ⊥ → v 1 → v 3 → . . . → v 11 with entry v 3 the resources E (allocated at v 1 and used at v 3 ) and G (allocated at v 3 and used at v 5 ) are static resources. This leads to a fundamental classification between inactive (i.e. unused), static, and otherwise dynamic resources.

Definition 4 (resource classification):

Let G a resource graph with vertex set V .    inactive(G) def = {X | ∀v ∈ V, X / ∈ γ(v)} static(G) def = {X | X is static in a lasso of G} dynamic(G) def = vars(G) \ (static(G) ∪ inactive(G))
In our example the sets are static(G) = {E, G}, inactive(G) = {F } and dynamic(G) = {A, B, C, D, H}.

Our principal means to abstract from the relatively lowlevel resource graphs is to characterize resource usage as a formal language. Definition 5 (resource profile): Let G a resource graph. Its resource profile is the language based on alphabet 2 vars(G) defined as follows:

R G def = ⊙ 1≤i≤n use(v i ) • [⊙ e≤j≤n use(v j )] * | v 1 → • • • → v e → • • • → v n a lasso of G ∪ ⊙ 1≤i≤n use(v i ) | v 1 → • • • → v n a complete path of G with use(v) def = { X | X ∈ γ(v) ∩ static(G)} ∪ (γ(v) ∩ dynamic(G))
For example, for the lasso allocation and deletion events. The reason is that they fundamentally only play a role for the static/dynamic distinction. This explains why the static resources are explicitly recorded otherwise the information would be lost. Moreover, we only exploit language union, concatenation and Kleene star, i.e. regular language constructors. This is to abstract away from the branching structure of the graph, which play only an indirect role wrt. resource usage. Note however that the language R G is not itself regular since the names of resource variables are purely symbolic and subject to a form of α-conversion. This is in fact a crucial aspect of the model to enforce the purity of resource names.

v ⊥ → v 1 → v 3 → v 4 → v 5 → v 6 → v 8 with entry v 4 ,
The resource profile also record a fundamental information for our further analyzes: the resource conflicts. A conflict happens when a resource Y is used between (at least) two uses of another resource X. This means that X cannot be garbage collected at the time Y is used. This information is easily characterized in the resource graphs.

Definition 6 (conflict relation):

Let X, Y ∈ vars(G) be two distinct resources and ρ a path of G. A conflict between X and Y occurs in ρ, denoted by X♯ ρ Y , if:

• ρ = v ⊥ → + v i → * v j → * v k → • • • and either X ∈ γ(v i ) ∩ γ(v k ) and Y ∈ γ(v j ), or Y ∈ γ(v i ) ∩ γ(v k ) and X ∈ γ(v j ). • Moreover, if ρ is a lasso v 1 → • • • → v e → • • • → v n and X is static in ρ, a conflict between X and Y occurs if there exists i such that e ≤ i ≤ n and Y ∈ γ(v i ).
If there is a path ρ such that X♯ ρ Y then X and Y are said in conflict, which is denoted X♯Y .

The conflict graph obtained for our illustrative example is depicted on the right part of Fig. 1 (for the moment, we ignore the numeric annotations of the nodes). For example we have a conflict B♯D generated by the sub-path v 7 → v 9 → v 10 since D ∈ γ(v 7 ), B ∈ γ(v 9 ) and D ∈ γ(v 10 ). This corresponds to the first case of the definition. For the second case, a conflict such as A♯G comes from the fact that A ∈ γ(v 4 ) and G ∈ γ(v 5 ) with v 5 occurring in a lasso after its entry v 4 and before its exit (in this case v 8 ).

An obvious but fundamental property is that the resource conflicts are preserved by the resource profile abstraction.

Proposition 1: A resource conflict X♯Y occurs in G iff there is a word of the form w 1 .a.w 2 .b.w 3 .c.w 4 in R G with X ∈ a, Y ∈ b, X ∈ c or Y ∈ a, X ∈ b, Y ∈ c.
Most importantly, resource variables can be unified if they are not in conflict, which leads to the following notion.

Definition 7 (conflict-free equivalence): An equivalence relation E over a set of resource variables is said conflict-free if (X, Y ) ∈ E =⇒ ¬(X♯Y ).

From this we can finally define a proper notion of equivalence for resource profiles. The quotient R G E corresponds to the renaming of each use X by its equivalence class in E, i.e. [X] E . Hence, resource profiles are equivalent up-to conflict-free renamings. The condition vars(G) ∩ vars(H) = ∅ may appear as a strong constraint, but it is necessary to emphasize the arbitrary role played by the names of resource variables. If we allowed the same variable X to occur on both sides of the equivalence, then we would artificially equate the corresponding resources with no other criterion than their name ! Thankfully, we can always perform a kind of α-conversion to satisfy the disjointedness requirement.

Proposition 2: Let σ be a bijective renaming of the resource variables of a given graph G such that dom(σ) ∩ ran(σ) = ∅. Then we have R G ≈ R Gσ with Gσ def = Rσ, V, E, ασ, γσ, δσ the image of G by σ.

Beyond resource profile equivalence, we are interested in quantitative aspects of resource usages. These rely on the notion of resource bounds and resource index.

Definition 9 (resource bound and index):

A graph G has resource bound k ∈ N iff there exists a total renaming σ of vars(G) onto ran(σ) with dom(σ) ∩ ran(σ) = ∅ and card(ran(σ)) = k, and such that R G ≈ R Gσ . The resource index of G is the smallest χ ∈ N such that G has bound χ.

Suppose for example a graph with 3 variables and resource bound k = 2. This means at least 2 of the variables can be unified without contradicting the conflict graph. This is witnessed by the following proposition.

= {X = σ k (X) | X ∈ vars(G)} is a conflict-free equivalence denoting k distinct equivalence classes.
The resource index -the lowest resource bound -is a very accurate quantitative witness of resource consumption, although in practice finding less tight but still decent upper bounds is also pertinent.

III. RESOURCE ANALYSIS

Based on the simple yet operative resource model defined in the previous Section, we now begin the elaboration of our practical resource analysis framework.

A. Lattice completion and graph recursor

Our starting point is a slight modification of the resource graphs, providing us: (1) a generic computation principle, (2) a corresponding reasoning principle for establishing the correctness of the algorithms, and (3) a modular characterization of their worst-case complexity. For the sake of concision, we only detail a few of the many analyzes that can be described this way, some other examples are discussed more informally.

Definition 10 (lattice completion):

Let G = R, V, E, α, γ, δ be a resource graph. Define L def = { ρ e,n | ρ e,n = v 1 → • • • → v e → • • • → v n is a lasso of G with entry v e }. The lattice-completed resource graph is G def = R, V, E, Ω, α, γ, δ with: E def = E \ {v n → v e | ρ e,n ∈ L} ∪ {v n → v ⊤ | ρ e,n ∈ L} Ω def = {v n → v e | ρ e,n ∈ L}
In the example of Fig. 1 the highlighted vertices v 2 , v 3 and v 4 are the lasso entries of the graph. In the completion procedure, the edges (with dashed arrows) that point to these entries are cut from the graph and redirected towards v ⊤ (this redirection is not depicted). The Ω component contains the edges that generate the cycles in the graph, which we of course need to remember for deciding certain properties (such as whether a given vertex is an entry of some lasso).

The completion procedure corresponds, algorithmically speaking, to a graph decomposition into nested strongly connected components (SCCs). The algorithm has quadratic worstcase complexity and produces an acyclic graph with interesting ordering properties.

Proposition 4: Let G a completed resource graph with vertices V and edges E. Then (V, E) is a complete lattice with E the reflexive and transitive closure of E.

From now on we will assume that resource graphs are properly completed, and will denote by G its completion G.

Definition 11 (graph recursor):

Let G be a resource graph with vertex set V . The graph recursor for f :

Y × V → X (vertex function) and g : 2 X → Y (edge function) at v ∈ V is: rec v G (f, g) def = f (g {rec v ′ G (f, g)} | v ′ → v in G} , v)
We abbreviate rec v ⊤ G (f, g) as rec G (f, g). The recursor can be implemented by a simple topological sort traversal of the completed graph, starting from v ⊥ and ending at the desired termination vertex v (trivially, termination occurs at worst at v ⊤ , the top-element of the ordering). Each edge is visited at most once so the traversal has linear complexity. Consequently, the recursor has a naturally modular worst-case complexity.

Proposition 5: Let G a resource graph with vertex set V and edge set E. The worst-case complexity of a graph recur-

sor rec v G (f, g) is O (card(V ) × C f + card(E) × C g ) where C f (resp. C g ) is the worst-case complexity of f (resp. g).
Because these depend on the concrete data-structures employed, we do not detail the operands C f and C g of the complexity calculations. However, all the recursive computations described below are efficient polytime algorithms. Beyond computation, most of our correctness proofs rely on a simple yet effective inductive principle.

Lemma 1 (graph inductor): Let P : V → {true, false} be a predicate and G a resource graph with vertex set V . Then ∀v ∈ V, P(v) if and only if:

P(v ⊥ ) and ∀v ′ → v in G, P(v ′ ) =⇒ P(v).
A global graph property P G then corresponds to proving the local property P G (v ⊤ ) using the inductor principle.

We now illustrate the recursor/inductor framework by computing the sets of live variables (allocated, used and not freed) and active variables (allocated and used, possibly freed) at a given vertex.

Definition 12 (live and active variables):

Let G a resource graph. We define the live and active variables at vertex v by the following recursors:

live v (G) def = rec v G (λx, v.(x ∪ γ(v)) \ δ(v), ∪) active v (G) def = rec v G (λx, v.x ∪ γ(v), ∪)
To illustrate the inductor principle, we will use it to demonstrate the following property.

Proposition 6: P(v) def = X ∈ active v (G) iff ∃u, u → * v s.t. X ∈ γ(v).
Proof: The recursor we consider is:

active v (G) = rec v G (f, ) with f (x, v) def = x ∪ γ(v).
• (base case) We must prove P(v ⊥ ). The left-hand side of the iff is false since we have active

v (G) = f ( ∅, v ⊥ ) = γ(v ⊥ ) = ∅.
This is because v ⊥ has no predecessor and γ(v ⊥ ) = ∅ by definition. The righthand side is also trivially false for the same reason. Hence P(v ⊥ ) is true.

• (inductive case) The hypothesis of induction is that P(v ′ ) holds for any predecessor v ′ of v. We have to consider two sub-cases. First, we suppose that X ∈ active w (G) for some predecessor w of v.

Now, if we write active

v (G) = f ( W, v) then clearly active w (G) ⊆ W and thus active w (G) ⊆ active v (G) = ( W ) ∪ γ(v), hence X ∈ active v (G). Moreover, by hypothesis of induction ∃u, u → * w s.t. X ∈ γ(u) and from u → * w → v we conclude P(v) is true. The second sub-case is if X / ∈ active v ′ (G) for any (direct) predecessor v ′ of v.

By hypothesis of induction this means X /

∈ γ(w) for any (direct or indirect) predecessor w of v. In this case it is a trivial fact that X ∈ active v (G) iff X ∈ γ(v) and thus P(v) is also true in this case.

Applying Lemma 1 we conclude that the property P(v) is true for any vertex v of G.

We can generalize such local property by considering them at the tail v ⊤ . For instance, the resources that are still live in v ⊤ have been used and not freed, hence because the graph has correct usage they are exactly the static resources. Similarly we can compute the set of inactive variables.

Proposition 7:

static(G) = live v ⊤ (G) inactive(G) = vars(G) \ active v ⊤ (G)
A relatively simple recursor can also be defined for the algorithmic construction of an automaton recognizing the language of a given resource profile.

Lemma 2: R G is recognized by the finite automaton:

A G def = Q, q v ⊥ , δ, F s.t. (Q, δ, F ) = rec v ⊤ G (f, ) with: f(x, v) def =              ({q v ⊥ }, {}, {q v ⊥ }) if x = {} (Q ∪ {q v }, δ ′ , {q}) if x = {(Q, δ, F )}, with δ ′ def = δ ∪ {q use(v) ----→ q v | q ∈ F } ∪ {q v use(v ′ ) ----→ q v ′ | v → v ′ ∈ Ω G }
For our running example the resulting automaton (equivalent but slightly simplified so that it fits the page) is depicted on Fig. 2. Note that the only accepting state is the one generated for v ⊤ . Moreover if the construction yields an automaton that has roughly the shape of the initial resource graph, in practice many factorizations can be performed on-the-fly.

For the computation of the resource conflicts, we have two complementary algorithmic approaches: (1) define a dedicated recursor for the task (as implemented in our toolset, cf. Section IV), or (2) detect the conflicts directly on the automaton A G . The latter is possible since as explained previously the language R G encodes the conflict graph of G. For example the conflict B♯D can be found by the sequence of states q 6 , q 7 , q 8 , q 9 . For the conflict A♯G we can follow e.g. the loop q 5 , q 6 , q 2 , q 3 , q 4 , q 5 .

B. The Omniscient Garbage Collector

The α-convertibility of the variables in resource profiles is the principal obstacle to the development of efficient analysis algorithms. Our approach of the problem is inspired by the memory allocation metaphor. We want to assign unambiguously unique locations to the resource variables. Of course, we should use as few locations as possible, which underlies an important notion of garbage collection. Definition 13 (allocator): Let L be an ordered set of locations [ℓ 1 , . . . , ℓ n ] such that n ≤ card(vars(G)). An allocator µ is a mapping from variables to locations. It is a safe allocator iff, whenever X♯Y then µ(X) = µ(Y ). An omniscient allocator is a safe allocator that minimizes n.

Conflict-freedom is the only and fundamental requirement of the allocation problem. Indeed, we can use less resources (i.e. reuse resource locations) as long as this does not creates a contradiction in the conflict graph. This intuition can be characterized formally.

Lemma 3: Let µ be a safe allocator for a resource graph G. Then µ is a renaming such that R G ≈ R Gµ and card(ran(µ)) is a resource bound for G.

The effective computation of resource bounds naturally relates to the algorithmics of graph coloring [START_REF] Jensen | Graph coloring problems[END_REF].

Proposition 8: Let ♯ be the conflicts of a given resource graph G, and let µ ♯ be a proper coloring of ♯. Then µ ♯ is a safe allocator for G.

The simplest of all (imperfect) coloring algorithms: first-fit coloring provides us with an interesting resource bound that can be computed quite efficiently. In the right part of Fig. 1, the numbered labels of the nodes correspond to colorings of the conflict graph. The numbers on the left (before the open parenthesis) correspond to first fit coloring using the node ordering H, G, A, B, C, D, E. First, H can be colored by (location) 1 and so is G since it is not connected to H. Next, A and B must use color 2 since they are connected to G. The color 1 can be reused for C since it is not yet connected to a colored node. The node D is connected to C (color 1) and B (color 2) and thus must be colored 3. Finally, E is connected to nodes colored up-to 3 and thus has color 4. The resource bound found is 4 and is less than d G + 1 = 6.

For the resource index we need an omniscient allocator, which essentially corresponds to the perfect coloring of the conflict graph.

Proposition 10: Let µ ♯ be the safe allocator corresponding to the perfect coloring of the conflicts ♯ of a resource graph G. Then µ ♯ is an omniscient allocator for G. Moreover, card(ran( µ ♯ )) is the resource index of G.

For our example the resource index χ is 3, it is also the chromatic number of the conflict graph. The associated perfect coloring is shown in Fig. 1 by the numbers within parentheses. The strategy here is to use the color 2 for both B and C. This way D can reuse color 1 and thus E has color 3 instead of 4.

This leads to our first prominent complexity result.

Theorem 1: Computing the resource index χ of a resource graph is NP-complete. This can be seen as a somewhat negative result, although we remark that the perfect coloring algorithm only applies to the conflict graph and not the complete resource graph. In most practical cases the former should be much smaller than the latter. Furthermore, interesting properties of separability can often be exploited.

q ⊥ start q1 q2 q3 q4 q5 q6 q ⊤ q7 q8 q9 {H} { E} { E} { E} {A} { G} {A} {B} {B} {D} {B} {B} {C,D} { E}
Proposition 11: Let ♯ be a conflict graph. If ♯ = i ♯ i then µ ♯ = i µ ♯i . Moreover if for some resource X we have ∀Y ∈ ♯, X = Y ∨ X♯Y then χ ♯ = 1 + χ ♯\{X} .
These are basic properties of graph coloring. First, disconnected components of the conflict graphs can be colored separately. In our example conflict graph this is the case of the sub-graph with node H and the one consisting of all the other resources. The second property is also useful in practice. In our example, the vertex E is connected to all the other vertices of the conflict graph (except H). The subgraph without E has chromatic number 2 and the second property tells us that the chromatic number of the complete graph is 3.

C. Algorithmic resource profile equivalence

We approach the resource profile equivalence problem in three successive algorithmic steps. In the first step, we compute omniscient allocators for the two resource graphs to compare.

Proposition 12: Let µ G and µ H be omniscient allocators for respective resource graphs G and

H. Then R G ≈ R H iff R G µ G ≈ R H µ H .
We now face a new intermediate problem, which is to find a bijection between the (allocated) resource variables of G and H that can be lifted to a conflict-free equivalence. This exactly corresponds to finding an isomorphism between the conflict graphs of G and H. Lemma 4: Let µ G and µ H be omniscient allocators for respective resource graphs G and H. Moreover, let γ be an isomorphism between the conflicts of the profiles R G µ G and R H µ H , and

E γ def = {X = Y | X ∈ dom(γ) ∧ Y = γ(X)}. Then R G ≈ R H iff R G µ G E γ = R H µ H E γ .
We remind the reader that graph isomorphism defines the GI complexity class (in NP). Now, since R G and R H are composed only of regular constructors and α-conversion does not apply anymore, we finally reduced the resource equivalence problem to the well-studied problem of equating regular languages, which is notoriously a PSPACE-complete problem. We might question whether a better algorithm could be found for the resource profile equivalence problem. The answer is no and the reason is that ultimately, regular language equivalence can be reduced polynomially to the resource equivalence problem (considering the reflexive case of ≈).

Definition D(x) def = P Process P, Q ::= 0 (inert) | new(x) P (observable) | local(x) P (inobservable) | α.P (prefix) | P | Q (parallel) | D[ã] (call) Action α ::= τ (silent) | ab (output) | a(x) (input)
Hence our second fundamental complexity result.

Theorem 2: Resource profile equivalence is PSPACE-hard.

IV. APPLICATION: RESOURCE ANALYSIS OF π-CALCULUS PROCESSES

In this section we describe the experimental application of our framework for the analysis of resource consumption in πcalculus processes. By lack of space, the presentation remains mostly informal.

A. A π-calculus refresher

The syntax of the variant of the π-calculus we cover in the experiment2 is given in Fig. 3. The semantics of the language for most constructors can be found in many sources (e.g. [START_REF] Sangiori | The π-calculus: a Theory of Mobile Processes[END_REF]). Informally, the process 0 has no transition. The scope of a name x can be restricted by either new(x) or local(x) and for the labelled transition semantics the two constructs are assumed synonymous (this will be different in reduction semantics). A prefixed process α.P denotes a transition with a label corresponding to the action α and continuing as process P . There are four kinds of labels depending on the action α:

• a label τ is generated by a silent action τ .

• a label ab is generated by an input action a(x) for any name b received along channel a and bound to the variable x (in early semantics).

• a label ab is generated by an output action ab of datum b along channel a, under the provision that a and b are not restricted (i.e. in the scope of a new or a local).

• a label aνb is a bound output generated by an output action ab where b is restricted, unlike a.

The construct P | Q expresses the parallel composition (in terms of interleaving) of the sub-processes P and Q. These cover the independent evolution of the processes, or alternatively the synchronization for a composition of the form ab.P | a(x).Q. The latter generates a transition with label τ and a continuation of the form: P | Q{a/x}. Finally, the language has tail calls that corresponds to possibly recursive unfoldings of process definitions.

B. Abstracting transition labels

The first step of our experiment is to generate a resource graph that reflects the behavior of a π-calculus process in terms of resource usage. A natural interpretation consists in interpreting almost directly the labelled transition system (LTS) as a resource graph. Under this interpretation, each transition P µ -→ Q is associated to three vertices v P , v µ and v Q and the edges (v P , v µ ) and (v µ , v Q ). The resource usage is then specified by the values associated to α(v µ ), γ(v µ ) and δ(v µ ). Schematically, we have:

• any transition P aνb --→ Q creates a resource X b and is interpreted as:

v P α{X b },γ{X b },δ{} v Q • any transition P ab -→ Q such that there is a resource X b for b is interpreted as: v P α{},γ{X b },δ{} v Q • any other transition P µ -→ Q is interpreted as: v P α{},γ{},δ{} v Q
In this first abstraction, the rationale is: every data sent to the environment count as resource uses. Hence, any bound output counts as the creation of a fresh resource as well as a use, and each output of a name associated to a resource counts as a simple use. There are possible variations, such as counting the channel itself as a use (e.g. recording a use with ba in case b is associated to a resource X b ), or also taking input into consideration. It is then possible to distinguish between input or output resource uses. In all these possible interpretations, the leitmotiv is that resource profile equivalence should be a necessary (although insufficient) condition for bisimilarity 3 . We also require the destruction of resources through δ's. A simple and effective heuristic is to insert a δ{X b } when there is no further free occurrence of the name b in the process. This simple form of garbage collection is implemented by all the analysis tools for the pi-calculus that we are aware of.

Let us consider as a first example the following process:

P def = new(c) ac.bc.P
This is a special case of a common pattern for generating fresh names. Here, the restricted name c is sent first along a and then b towards the environment. The whole process is then iterated, leading to the following derivations:

P aνc --→ bc.P bc -→ P → • • •
The first output along a corresponds to a bound output since c is restricted but the further output is not bound anymore. Given a resource variable X c representing the name c once required fresh, we obtain the following resource graph:

v ⊥ α{Xc},γ{Xc} v1 γ{Xc},δ{Xc} v2 v ⊤
A theoretically acceptable alternative would to have an infinite system generating an infinite number of resources. Although the version with the least fixpoint shows that exactly one resource is required for this behavior, the resource index is invariantly 1 because there can be no conflict for this process in any acceptable interpretation.

A minimal conflict can be generated by e.g.: new(a) new(b) ca.cb.ca.0 A slightly complexified variant of this process is as follows:

Q def = new(a) new(b) ca.cb.da.d(x).cx.0 C[X] def = new(d) [Q | X]
The resource graph corresponding to C[d(y).dy.0] is4 : This maintains the conflict X a ♯X b and thus the resource index of the system is 2, whereas if we consider the variant C[d(y).dc.0] then the resource graph becomes:

v ⊥ α{Xa},
v ⊥ α{Xa},γ{Xa} v1 α{X b },γ{X b },δ{X b } v2 δ{Xa} v3 v4 v5 v ⊤
The conflict X a ♯X b is no more and hence the resource index is 1 in this case. This illustrates the profoundly semantic nature of the proposed resource abstraction. Indeed, the behavior of X within the context C[X] can be as complex as required so that in the general case (beyond finite control) one cannot decide whether the conflict should take place or not. This abstraction has been implemented in a prototype tool and we analyzed several examples from the HAL environment [START_REF] Ferrari | Verifying mobile processes in the hal environment[END_REF]. At present, the tool only support finite control processes and the construction of the resource graph is purely semantic. Since we do not need to preserve the whole branching structure, we can apply a few heuristics to reduce the size of the resource graphs, but in the worst case it can be as large as (but no larger than) the full LTS e.g. as produced by HAL. The problem of producing the smallest possible resource graph is open and we conjecture that its complexity is high. Table I gives the figures we obtain for the examples that are particularly interesting for the considered abstraction.

For each example, we give the size of the LTS produced by HAL and we compare it with the size of the resource graph we obtain. This measure is not really significant but it still emphasizes the fact that there is an important potential of abstraction when constructing the resource graphs. A metric much more significant is the resource index that we obtain using our omniscient garbage collector.

The heap example models a set of interacting memory cells. Each cell is a process with an input and an output channel and stores a single datum. The cells are composed in parallel, which induces a large LTS resulting from the interleaving of many internal synchronizations. Since most branching is created by pure interleaving and τ transitions, the resource graphs we obtain are rather small in comparison. The resource index for heap n is n -1 is all cases, which is an invariant in the general case. This in fact counts the number of competing cells in the system, with a single non-conflicting case (the two "entry" cells are not competing with each other).

The buffer example is a variant of the heap but with less internal synchronizations and in proportion more exchanges with the environment. Hence, we observe more resources to take into account. In consequence, the size of the resource graph is not reduced in large proportions anymore. However, the resource index is still very small, with a suggested invariant of a resource index n for buffer n , all cells being in competition.

These two examples exhibit a rather low amount of conflicts if compared to the size of their state-space. This means that perfect coloring, despite its high computational complexity, is not a difficult problem in these particular cases. We firmly believe that this is the case in many realistic examples, although this remains to be confirmed experimentally.

Another interesting example is the GSM and its variants that model a simplified form of the handover protocol for gsm mobile networks. These examples show rather complex name exchanges but are quite small in term of control. What we find particularly interesting is that the different variants all result in the same resource graph (up-to resource variable renamings) and of course the same resource index. This confirms, rather surprisingly (we expected at best the same resource profiles), that in terms of resource usage the three examples are basically the same.

C. Refining reductions

Abstracting from the labelled transitions is quite natural but requires a very powerful observer. In comparison, the reduction semantics are much less demanding. However, they only apply on closed systems. An intermediate approach is to model part of the observer within the system. For this we allow a process behavior to be sliced from the point of view of the environment. A process of the form local(x) P considers x as a "normal" π-calculus restriction but explicitly decorated by a tag "inobservable". In comparison, in new(x) P the name x is tagged "observable". Names can also be assigned the tag "observed" although not in their initial state. Now, a standard reduction P → Q of the π-calculus is refined so that it produces a "labelled" reduction of the form Λ ⊢ P µ -→ Λ ′ ⊢ Q in the slice-π variant. The component Λ is a set of names tagged as observable. A name a with the observable tag is such that either a ∈ Λ if lacks the observed tag, and otherwise we have a ∈ Λ. Of course, it might not be the case that {a, a} ⊆ Λ. The inobservable names are simply absent from Λ.

For each reduction P → Q we have either:

• an open reduction of the form:

Λ ⊢ P b --→ (Λ\{b})∪{b} ⊢ Q when the
reduction is a synchronization passing an observable or inobservable but not yet observed name b along an observable channel a. As a side-effect, the name b is tagged as observable and also as observed.

• a transparent reduction of the form: • an opaque reduction of the form: The complete semantics of this "slice-π" variant is provided in appendix. The main interest of this refinement is that (not unlike barbs [START_REF] Sangiori | The π-calculus: a Theory of Mobile Processes[END_REF]) it opens up some part of the behavior of the processes, and still maintains a one-to-one correspondence with the standard reductions.

Λ ⊢ P b - → Λ ⊢ Q when the
Λ ⊢ P • -→ Λ ⊢ Q in any other case. {} ⊢ new(a) new(b) S(a, b) x1 ---→ {a, b, x 1 } ⊢ P (a) | Q ′ (a, b) | Q(a, b) | R(b) x2 ---→ {a, b, x 1 , x 2 } ⊢ P (a) | Q ′ (a, b) | Q ′ (a, b) | R(b) x1 -→ {a, b, x 1 , x 2 } ⊢ P (a) | Q(a, b) | Q ′ (a, b) | R(b) x2 -→ {a, b, x 1 , x 2 } ⊢ S(a, b) . . . {} ⊢ local(a) new(b) S(a, b) • -→ {b, x 1 } ⊢ P (a) | Q ′ (a, b) | Q(a, b) | R(b) • -→ {b, x 1 , x 2 } ⊢ P (a) | Q ′ (a, b) | Q ′ (a, b) | R(b) x1 ---→ {b, x 1 , x 2 } ⊢ P (a) | Q(a, b) | Q ′ (a, b) | R(b) x2 ---→ {b, x 1 , x 2 } ⊢ S(a, b) . . .
In terms of resource graphs, the interpretation is now quite similar to the labelled abstraction:

• any reduction Λ ⊢ P b --→ Λ ′ ⊢ Q creates a resource X b and is interpreted as: v Λ⊢P α{X b },γ{X b },δ{} v Λ ′ ⊢Q • any reduction Λ ⊢ P b - → Λ ⊢ Q such that there is a resource X b for b is interpreted as: v Λ⊢P α{},γ{X b },δ{} v Λ⊢Q • any other reduction Λ ⊢ P • -→ Λ ⊢ Q is interpreted as: v Λ⊢P α{},
def = a(y).Q ′ (a, b, y) Q ′ (a, b, y) def = by.Q(a, b) R(b) def = b(z).R(b) S(a, b) def = P (a) | Q(a, b) | Q(a, b) | R(b)
Fig. 4 shows representative reductions of the first process with a observable (on the left) and a inobservable (on the right). In the observable case the names a and b are recorded in the first reduction as observable (i.e. put explicitly in the Λ component of the state). In the same reduction, the name x generated by P is opened (i.e. marked observed) by the synchronization with the leftmost process Q. A "second" x is opened in the next reduction by the synchronization between P and the rightmost Q. The "two" x's must be alpha-converted hence the introduction of x 1 and x 2 in the reductions. The Λ component of the transition contains {x 1 , x 2 } because these two observable names are actually observed. If we compare this behavior with the one of the right-hand side, a is there tagged inobservable since it is introduced by the local construct. This means it is not a member of the component Λ of the state, unlike b. This means that the names x 1 and x 2 are now introduced as observable but not yet observed because they are transmitted along a. In terms of resources graphs, the left-hand side reductions yield a conflict X x1 ♯X x2 that is absent in the rightmost process. The processes have indeed distinct resource indices: respectively 2 and 1. We thus obtain a level of flexibility that is quite comparable to the labelled abstraction, but without the need for an idealistically powerful observer.

Based on this abstraction, we designed a simple example inspired by the infamous dining philosophers. The idea is that the environment is modeled as a process that acknowledges through an observable channel eat the fact that a philosopher actually starts eating. All the other channels (ending points for the philosophers, the forks, etc.) are created inobservables (hence restricted with local instead of new). The resource conflicts occur when distinct philosophers eat at the same time on the table, by transmitting the philosopher channel along the environment observable eat. As a side effect, the philosophers, initially inobservable, inherit both the observable and observed tags in a dynamic way.

The results for some instances of the philo n examples are listed in Table II. The size of the reduction graph grows exponentially since we modelled various sub-processes running in parallel (e.g. 13 processes for philo 4 ). The resource graphs we obtain using similar heuristics as in the labelled case are much smaller but in a similar order of magnitude in terms of growth. The resource index (and hence the maximum conflict) is quite reassuring in that the number of philosophers who actually competing for food remain below the number of fork pairs, ensuring the correctness of the protocol. Although simpler analyzes are of course possible for this example, the experiment emphasizes the fact that the resource index captures a deep semantic information, tightly related to the chosen resource abstraction.

Last but not least, none of our experiments (except those made on purpose) expose a large resource index. In fact, the perfect coloring of the conflict graphs was almost immediate in all the examples, despite the high complexity of the algorithm. In the current version of the tool we use a simple and rather slow CSP-solver for the task. This largely covers our current needs but state-of-the art SAT solvers could be used for more demanding scenarios. In cases perfect coloring would become unfeasible, we can still compute less tight but still interesting resource bounds very efficiently, using e.g. first-fit coloring.

By lack of time, we could not experiment the second abstraction on more significant examples. And at the time of writing, the tool -in a very early stage of development -still lacks support for computing resource equivalence problems.

V. RELATED WORK

Resource control and analysis is a vast topic of research. Considered in their purest form, resources are pure names naturally leading to nominal calculi [START_REF] Gordon | Notes on nominal calculi for security and mobility[END_REF] in general, and in particular the π-calculus [START_REF] Sangiori | The π-calculus: a Theory of Mobile Processes[END_REF] and its numerous variants. This is a rather abstract and open-ended setting, thus not a very prolific source of effective analysis algorithms. One approach is to enrich the semantics, as e.g. in [START_REF] Amadio | Resource control for synchronous cooperative threads[END_REF] where a resource bound analysis is proposed for a reactive synchronous variant of the π-calculus. For more classical (and abstract) variants, related studies address decidability issues often in connection with Petri nets, such as e.g. [START_REF] Amadio | On decidability of the control reachability problem in the asynchronous pi-calculus[END_REF], [START_REF] Rosa-Velardo | Decidability problems in petri nets with names and replication[END_REF] and [START_REF] Hüchting | A theory of name boundedness[END_REF]. The latter introduces the name-bounded processes, a significant class of infinitestate systems for which the boundedness question is answered positively. It is particularly remarkable that reachability is also decidable for this class. In comparison, we assume the finiteness of resource graphs, and deliberately de-emphasize the means by which they are obtained practically. Indeed, a key feature of our framework is its independence from any particular formalism. Furthermore, for a given formalism multiple resource abstractions can be experimented as illustrated in Section IV. The abstraction of active restrictions proposed in [START_REF] Hüchting | A theory of name boundedness[END_REF] only applies on reductions for closed systems. It is also different from the resource model we propose around the slice-π calculus, and to illustrate this aspect we consider the following process:

P (a) def = new(x) [ax.0 | a(y).P (y)] | τ.new(z) za.0
In the abstraction we propose, the resource index of new(a) P (a) is 1 because the processes new(z) za are deadlocked after the initial τ . However, since the name a is always free in these deadlocked processes the whole process has an infinite number of active restrictions. This particular example can be of course optimized but the deadlocked process can be complexified at will. Hence, we discuss a finer-grained abstraction that cannot be decided locally. Relying on an essentially semantic abstraction is not without consequences. For instance, our current implementation only works with finite control π-calculus processes. It is a very intriguing and open question wether interesting sub-classes of infinite systems with finite resource graphs could be determined, probably starting with variants of the name-bounded class itself. Another related abstraction is that of barbed semantics [START_REF] Sangiori | The π-calculus: a Theory of Mobile Processes[END_REF] that also refine reductions but considering in this case the non-restricted channels as observables. This is to ultimately characterize an adequate notion of process equivalence -namely strong barbed congruence -when the reductions with observables are closed under context. While we could observe the channels instead of (or together with) the data, we require our refinement to remain in one-to-one correspondence with the plain reductions. Also particularly notable in [START_REF] Hüchting | A theory of name boundedness[END_REF] is the prominent role played by the notion of garbage collection something already observed in e.g. the history-dependent-automata [START_REF] Ferrari | Verifying mobile processes in the hal environment[END_REF] or in the π-graphs [START_REF] Peschanski | A petri net interpretation of open reconfigurable systems[END_REF]. This is a side note but to our knowledge, HD-Automata Laboratory (HAL) is the only tool allowing the generation of early labelled transition system from (finitary) π-calculus processes. Indeed, the generation of the early LTS is not trivial especially because it requires the determination of the active names [START_REF] Montanari | Checking bisimilarity for finitary picalculus[END_REF], a notion tightly connected to the live variables of resource graphs.

Graph coloring relates to the very well-known problem of register allocation in compiler back-ends [START_REF] Chaitin | Register allocation and spilling via graph coloring (with retrospective)[END_REF]. However, the behavior of registers is quite specific. For example, one can always choose not to allocate a register, or release it prematurely and defer to the central memory. Hence, the coloring can be both partial and imperfect, allowing many optimization heuristics that do not apply at all in our case. This still naturally connects our study with the well-studied notion of register automata and related formalisms e.g. variable automata [START_REF] Grumberg | Variable automata over infinite alphabets[END_REF]. One major difference is that we map the resource variables to a finite (and hopefully least) number of locations. Hence, our automata are "quasi-regular" only introducing a (non-trivial) notion of α-conversion. This is enough as long as we address pure nominal questions, however if we look "into" resources then a connection with the above-mentioned frameworks seems highly probable. This is especially the case if we address resource control issues such as in e.g. [START_REF] Degano | Nominal automata for resource usage control[END_REF] (automata-based approach) or [START_REF] Kobayashi | Resource usage analysis for the pi-calculus[END_REF] (typechecking-based approach). if case: Suppose X♯Y in a given resource graph G. According to Definition 6 there is a path ρ = v 1 → • • • → v n such that X♯ ρ Y with 3 possible causes. First, if ρ is a complete path then there exist i, j, k, If ρ is a lasso with entry v e , 1 < e ≤ n then we have two sub-cases to consider. The first sub-case is identical to the previous one, the second sub-case corresponding to a cyclic conflict (second case of Definition 6). If we suppose that X is static and Y dynamic (the other cases being symmetric), the we have some i, j, 1 < i < e ≤ j ≤ n such that X ∈ use(v i ) (by Definition 3 supposing G has correct usage) and Y ∈ use(v j ). Hence in R G the cycle is unfolded once thus if we let a = c = use(v i ) and b = use(v j ) then w ρ is of the expected form w ρ = w 1 .a.w 2 .b.w 3 .c.w 4 .

1 < i ≤ j ≤ k < n such that X ∈ γ(v i ), Y ∈ γ(v j ), X ∈ γ(v k ) or Y ∈ γ(v i ), X ∈ γ(v j ), Y ∈ γ(v k ).

only-if case:

We suppose in a resource profile R G there is a word w = w 1 .a.w 2 .b.w 3 .c.w 4 such that X ∈ a, Y ∈ b and X ∈ c (the other cases are similar). By Definition 5 we know that w is generated by either a finite path ρ = v 1 → • • • → v n that is either a complete path or a lasso of G. If it is a complete path then w is of the form w 1 .{ X, a ′ }.w 2 .{Y, b}.w 3 .{ X, c ′ }.w 4 and in the path ρ we have i, j, k such that X ∈ γ(v i ), Y ∈ γ(v j ), X ∈ γ(v k ) and thus X♯ ρ Y . If ρ is a lasso there we have either the same situation as previously (a succession of X, Y, X in the path) or w corresponds to the unfolding of a word of the form w ′ .(w ′′ ) * and w ′′ = w ′′

B. Lattice completion and graph recursor

Proof: (of Proposition 4) A standard result of lattice theory is that if a finite ordered set S has a greatest (resp. a least) element and every pair of elements has a meet (resp. a join), then S is a lattice. Moreover, every finite lattice is a complete lattice.

Let G def = R, V, E, Ω, α, γ, δ be a complete resource graph. We interpret G has a partial ordering considering V as the carrier set and the reflexive and transitive closure of E as the ordering relation. This is indeed an proper partial ordering since the completion procedures removes and cycles, and thus the graph structure is that of a directed acyclic graph (DAG). Moreover, by definition we have v ⊤ (resp. v ⊥ ) is a greatest (resp. least) element of the ordering. Now, let v and v ′ be two vertices of G. Suppose (v, v ′ ) has no meet, which means that (1) either they have no lower bound or (2) that the set

M def = {M ⊆ V | m ∈ W, m → * v ∧ m → * v ′ }
has no maximal element. Case (1) would contradict the existence of v ⊥ . For case (2) the contradiction originates from the connectivity of the resource graph. Hence the meet of (v, v ′ ) does exist. In conclusion, G is a complete lattice.

Proof: (of Lemma 1)

The existence and constructibility of the least fixed point is justified by Knaster-Tarski's fixed point theorem for complete lattices (standard proof as found in many textbooks).

Proof: (of Proposition 7)

According to definition 3, a resource is static means it is used (and thus allocated) at some point, and not deleted in at least one path of the resource graph. This suggests the following local property.

P(v) def = X ∈ live v (G) implies ∃u, u → * v s.t. X ∈ γ(u) and ∀w, w → + v then X / ∈ δ(w)
For the base case, we have live v ⊤ (G) = ∅ hence P(v ⊥ ) is vacuously true.

For the inductive case we suppose P(v ′ ) to hold for any vertex v ′ such that there is an edge v ′ → v. We now proceed by contraction, supposing that P(v) does not hold, which means X ∈ live v (G) but the right-hand side of the implication is false. Now the two main sub-cases is whether X ∈ live v ′ (G) or not, for v ′ a direct predecessor of v. If X is live at v ′ then the only way contradict the right-hand side of the implication is to have X ∈ delta(v) but by definition of live v (G) this may not be the case. Now if live v ′ (G) is false, then it must be the case that X ∈ gamma(v) \ delta(v) for X ∈ live v (G) to be true, which automatically makes the right-hand side true because the graph is assumed to have correct usage.

By Lemma 1 we thus conclude that P(v) holds for any vertex v. Now, since the resource graph G is assumed with correct usage, a variable X that is used but not deleted must be static, and according to properties P and Q we have X ∈ live v⊤ G hence the result.

Proof: (of Lemma 2).

For a given vertex v ∈ V , rec v G (f, ) defines an automaton A v G and we have A G = A v ⊤ G by definition. There is a trivial isomorphism between the graph G and its corresponding automaton A G . Here the graph G is interpreted as the original resource graph before the completion procedure. Each vertex has a corresponding state q v and the resource usage at v is reflected by a transition from each state q of a predecessor v ′ of v with destination q v . Note also that at the end of step v the only final state is q v . Of course, before reaching the vertex v ⊤ the automaton only reflects a part of the graph that we denote by

G v such that G v ⊤ = G. Because G v lacks a top element, we simply add v → v ⊤ except if v ⊤ is already a vertex of G v (which means that v = v ⊤ anyway)
. At v we must also add the deletions for the active variables appearing in complete paths. This modifications required for the graph to be with correct usage is not difficult and will not be detailed.

By induction we can prove that R G v is recognized by the finite state automaton A G v . For the base case at v ⊥ , rec v ⊥ G (f, ) yields an automat that recognizes only the empty language, as required. For the inductive case we suppose that for each predecessor of v, the automaton A v ′ G recognizes the language R G v ′ . For each complete path in one of the R G v ′ 's there are two possibilies. Either v closes the path so that it becomes the entry of a lasso, and in this case R G v recognizes, from an "old" word w 1 .w 2 a "new" word of the form w

1 .w 2 .use(v)(w 2 .use(v)) * . In A v G a new transition q v use(v)
----→ q v ′ is inserted, which exactly corresponds to the "switch" from the old to the new word. Otherwise, if only a complete path is uncovered, then the recognized word w becomes w.use(v) and a corresponding transition is built in A v G . Since the words on the one side and the states/transitions on the other side are both assembled with set union, the automaton A v G recognizes the whole R R v G . Following the inductive principle of Lemma 1 the proof is completed.

C. Omniscient garbage collector

Proof: (of Lemma 3) That E µ is a conflict-free equivalence is by the safety condition in Definition 13. We now define

E ′ def = {X = [X] Eµ | X ∈ vars(G)}, which is also trivially a conflict-free equivalence. It is a simple fact that R G E ′ = R G E µ E ′ and thus R G ≈ R G E µ as required.
Moreover, µ is by definition total on vars(G) and is onto ran(µ). It is also the case that vars(G)∩ran(µ) = ∅, hence following definition 9 we can conclude card(ran(µ)) is a resource bound for G.

Proof: (of Proposition 8)

The proper coloring of a graph is such that no two adjacent vertices possess the same color. Hence, if µ ♯ is a proper coloring of a conflict graph over vars(G) then X♯Y (i.e. X and Y are adjacent in the conflict graph) implies µ ♯ (X) = µ ♯ (Y ) for any X, Y ∈ vars(G), hence µ ♯ is a safe allocator for G.

Proof: (of Proposition 9)

This is a standard result of graph coloring.

Proof: (of Proposition 10)

Let µ be a perfect coloring of the conflicts ♯ of a resource graph G. By Proposition 8 we know that it is already a safe allocator and according to Lemma 3 G has resource bound k = card(ran( µ)). The existence of a proper coloring -hence a safe allocator -µ such that card(ran(µ)) < k would contradict the fact that µ is perfect, i.e. that it minimizes the number of colors used to decorate the conflict vertices.

The number k -the chromatic number of ♯ -is thus a minimal resource bound, i.e. the resource index of G.

Proof: (of Theorem 1)

For the NP-hardness part of the proof, the objective is to start with an arbitrary graph ♯ that must be perfectly colored. It is simpler to consider the nodes of ♯ to be a set of resources variables in R and to consider a natural ordering ≤ on R. To reduce the problem in terms of the resource index computation, we must construct a resource graph G such that its conflict graph is ♯ itself. The construction does not require much creativity so we only sketch it. First we construct a sequence C containing the edges of ♯ following a lexicographic ordering on variable pairs, and we remove all the symmetric pairs. This ordering is required so that no interference is created among the conflicts. Now, we take each conflict X♯Y in order and we simply create a sub-path u → v → w such that X ∈ γ(u) ∩ γ(w) and Y ∈ γ(v). At the first occurrence of a variable X we add a resource creation event, and we similarly add a deletion even at the last occurrence. Finally we add the root and tail vertices. The length of the resulting path is a function linear in card(C) and thus also in the number of edges in the graph ♯. It is a simple fact to then demonstrate that the path exhibit the conflicts in ♯. Now finding an omniscient allocator solves the initial perfect coloring problem.

For the completeness part we know that the conflict graph can be implemented by a polynomial graph recursor. Then perfecct graph coloring is exactly what remains to be performed. We remark that card(dom(γ E )) = card(ran(γ E )) by a simple consideration of language equivalence (the alphabets must be the same on both sides of language equality) and moreover γ E • γ -1 E = id since E is symmetric. In consequence γ E is an isomorphism, which is enough to conclude the proof.

only-if case:

We suppose R G µ G E γ = R H µ H Eγ for a given isomorphism γ. According to the definition of ≈ this means R G µ G ≈ R H µ H and by Proposition 12 we have R G ≈ R H as required.

Proof: (of Theorem 2)

We adopt a constructive proof by considering the basic language of regular expressions. A regular expression e is defined inductively on an alphabet Σ as either:

• empty language: e = ∅ Regular expressions notoriously characterize the regular languages. We will denote by L e the regular language specified by a regular expression e.

For our hardness proof, we will mimic the construction of non-deterministic finite automata (NFA) from regular expressions. However in our case, for each kind of regular expression we will produce a resource graph with correct resource usage. The construction is relatively simple and tedious to formalize so we adopt a semi-formal presentation.

We first build the structure of resource graph G e corresponding to a regular expression e is a tuple R e = 2 Σ∪{ǫ} , V e , E e , α e , γ e , δ e constructed recursively as follows: The only non-trivial case is the last one, because in resource graph we must generate lassos, i.e. paths generated from non-reflexive transitive concatenation closures. Hence use the following encoding: e * = ǫ + e + . Now, the graph G e obtained finally only lacks proper allocations and deletions (i.e. the α e and δ e components). Since allocations must be unique, the only possibility is to allocate all the resources (i.e. symbols of the initial regular expression) at a "dummy" bottom node. Then we have to delete the resources just "before" the top node at the end. This gives the longest possible lifespan for the variables.

The final construction is thus something like the following:

v ⊥ αΣ v e ⊥ G e δΣ v e ⊤ v ⊤
By a simple structural induction, it is easy (albeit cumbersome) to demonstrate that the profile R Ge is indeed exactly the language L e specified by the regular expression e. The proof simply corresponds to the inductive construction of an isomorphism between the construction of a NFA recognizing e on the one side, and the automaton A Ge constructed using the recursor described in the paper. Our construction of the resource graph is in fact exactly the construction of a NFA from a regular expression, up-to some subtilities (e.g. root and tails vertices, unfolding of Kleene star, etc.). We thus omit the formalities here.

Hence, deciding R Ge 1 ≈ R Ge 2 results in establishing L e1 = L e2 . Since R Ge is obtained from a regular expression e in polytime, the reduction is completed and we can conclude PSPACE-hardness for the considered problem.

APPENDIX 2: THE SLICE-PI CALCULUS

Fig. 1 .

 1 Fig. 1. Example of a resource graph (left) and the associated conflict graph with first fit (resp. perfect) coloring (right).

Definition 8 (

 8 resource profile equivalence): Let G and H be resource graphs. Their profiles R G and R H are equivalent, denoted by R G ≈ R H , iff either R G = R H or vars(G) ∩ vars(H) = ∅ and there exists a conflict-free equivalence E over vars(G) ∪ vars(H) such that R G E = R H E .

Proposition 3 :

 3 Let k a resource bound for a graph G witnessed by a renaming σ k . Then E σ k def

Proposition 9 :

 9 Let G be a resource graph with conflict graph ♯. Then G has resource bound d G + 1 where d G def = max X∈vars(G) {Y | X♯Y }. Moreover, d G can be computed in linear time in the size of ♯.

Fig. 2 .

 2 Fig. 2. An automaton recognizing the profile of the resource graph of Fig.1.

Fig. 3 .

 3 Fig. 3. The syntax of the π-calculus (with slices).

  reduction is a synchronization passing an observed name b (i.e. b ∈ Λ) along an observable channel (i.e. a ∈ Λ).

Fig. 4 .

 4 Fig. 4. Reductions of slice-π processes with a observable (left) or inobservable (right).

=

  γ{},δ{} v Λ⊢Q To illustrate the abstraction, we consider the processes new(a) new(b) S(a, b) vs. local(a) new(b) S(a, b) with: new(x) ax.P (a) Q(a, b)

APPENDIX 1 :

 1 PROOF DETAILS A. Resource model Proof: (of Proposition 1)

  We suppose the former, the latter being symmetric. Moreover we suppose X dynamic and Y static, the other cases being similar. Let w ρ = n i=1 use(v i ) by the word generated in R G by ρ. Now define a def = use(v i ), b def = use(v j ) and c def = use(v j ). We thus have X ∈ a, Y ∈ b and X ∈ c. Moreover, by Definition 5 w ρ = w 1 .a.w 2 .b.w 3 .c.w 4 for some (possibly empty) words w 1 , . . . , w 4 , hence the property.

  1 .a.w ′′ 2 .b.w ′′ 3 and thus c = a and in consequence X♯ ρ Y . Proof: (of Proposition 2) We trivially have vars(Gσ) = Rσ = vars(G)σ. From the hypothesis dom(σ) ∩ ran(σ) = ∅, we thus obtain vars(G) ∩ vars(Gσ) = ∅. Now let E σ def = {X = σ(X) | X ∈ vars(G)} the equivalence relation associated σ. Now suppose (Z, Z ′ ) ∈ E σ such that Z♯Z ′ . Since σ is a bijection we have Z ∈ vars(G) and Z ′ = σ(Z 1 ) ∈ vars(Gσ) or the converse (since E σ is symmetric).Moreover since the resource graph is not modified beyond variable renaming, Z♯Z ′ iff Z♯σ -1 Z ′ ⇐⇒ Z♯Z. This contradicts Definition 6 which imposes the conflict relation to be irreflexive, hence ¬(Z♯Z ′ ) as required. Proof: (of Proposition 3) Following definition 9 it is easy to obtain R G E σ k = R Gσ E σ k . Hence since vars(G) ∩ vars(Gσ) = ∅ by definition 8 it must be the case that E σ k is a conflict-free equivalence as required. Moreover since card(ran(σ k )) = k and σ is total and onto, it follows naturally that π k def = {C | ∀X, Y ∈ C, [X] Eσ k = [Y ] Eσ k } has cardinality k.

Proof: (of Proposition 11 These

 11 are basic properties of graph coloring algorithms.D. Resource profile equivalenceProof: (of Proposition 12)By Lemma 3 we know that R G ≈ R G µ G and R H ≈ R G µ H .The result thus follows trivially by symmetry and transitivity arguments.Proof: (of Lemma 4) if case: The hypothesis is R G ≈ R H and since µ G and µ H are safe allocators, we have R G µ G ≈ R H µ H by Lemma 3.This implies the existence of a conflict-free equivalenceE such that R G µ G E = R H µ H E by definition of ≈. Now, let γ E def = {X → Y | X ∈ vars(G µ G ), Y ∈ vars(H µ H ), (X, Y ) ∈ E}.

•

  empty symbol: e = ǫ • singleton: e = x for any symbol x ∈ Σ • union: e = e 1 + e 2 with e 1 , e 2 regular expressions • concatenation: e = e 1 .e 2 with e 1 , e 2 regular expressions • Kleene star: e = e ′ * with e ′ a regular expression.

TABLE II

 II

	.	EXPERIMENTAL RESULTS FOR THE RESOURCE
		ABSTRACTION ON REDUCTIONS.

The consideration of infinite resource graphs is an interesting generalization of our theoretical framework. However, the whole algorithmic approach would not apply anymore. On the contrary, the class of infinite systems with finite resource graphs is particularly inspiring.

For the sake of concision, we omit the constructs of non-deterministic choice and match/mismatch. Note that our prototype tool has support for both.

We do not provide in this paper a formal proof that "bisimilarity implies resource profile equivalence" but this is rather trivial since resource profiles, under the labelled abstraction, encode partial trace sets of behaviors.

A single-hole process context C[X] is a function from process expression extended by a single occurrence of a variable X to process expressions, such that C[P ] = C[X]{P/X} for a standard notion of substitution of variables by processes. Here for example C[d(y).dy.0] = new(d) Q | d(y).dy.0 .

A. Syntax

The syntax of the slice-π calculus is as follows:

The structural congruence the least relation on processes satisfying:

• P ≡ Q by a renaming of bound variables

B. Semantics

A system term in slice-π is of the form Λ ⊢ P where Λ is a set of names and P a process term. A reduction in slice-π is of the form Λ ⊢ P µ -→ Λ ′ ⊢ P ′ where µ is a label either:

•

b for an open reduction when first observing b.

• b for a transparent reduction when observing b once more.

• • for an opaque reduction.

The reduction rules are as follows:

Step:


Dr Stéphane Villepontoux
email: stephane.villepontoux@univ-montp3.frst.villepontoux@gmail.com

Talking about ecotourism is not easy. Why? Because this word is complex

Since the 2000s, the World Tourism Organization makes the first campaigns of communication on ecotourism introduced as the new alternative development model capable of implementing sustainable tourism.

From this period, the suffix "eco" plays on the double logic "ecology and economy" to show that it is possible to make "good tourism" and reconcile the imperatives of ecology and economy.

Why such positioning? Because it is impossible to ignore the negative effects of massive tourism and its international impacts. But also that today the tourism industry is an important economic resource for developed societies in where free time become a consumer time.

And the situation is hardly in developing regions, because there is a lack of control of the activity. In many emerging countries, the relationship between economic impact and pressure on resources used and consumed is even more unbalanced.

In general, we can say that if the arguments in favor of tourism development are real (employment, development, standard of living), the effects on the environment and societies are so deep that the growth of activity can not compensate for the damage.

To solve this problem and find a balance, it's necessary to reconcile environmental protection and sustainable local development.

How to implement a logical win-win without stopping the tourist machine?

The solution lies in the discourse and theoretical modeling. Solution lies in a harmonious relationship exchange (good exchange) between two major players (the visitor and resident) and an area of mediation (the natural environment). The visitor respects the natural environment and enjoys the beautiful scenery. The natural environment is preserved and stay as a living resource for the locals. And the exchanges between tourists and local people can allow mutual enrichment, both economically and culturally.

But in practice, things are really different.

First, the tourist is an holiday and leisure consumer seeking to satisfy a need to escape. And ecotourism constitute an offer among others.

Then, the natural environment is not a static space. It is a living and dynamic ecosystem that is changing and evolving. This is not a museum that we visit but a resource space for anyone occupies or exploits.

Finally if local people can be opened to meet and exchange, there is not necessarily interested by development. Note that for traditional societies, live closer to nature is not a desire, but a daily reality.

From these first elements of conceptualization, we can see the difficulties of a truly sustainable tourism.

Yet, in practice, we see an explosion of ecotourism trips in connection with also a strong request growth (around 25 to 30% over the last fifteen years). But the phenomenon is difficult to quantify.

What is certain is that the phenomenon exploded. And the success of the application has adverse effects, particularly on the receiving countries, mainly in developing countries which concentrate the great natural areas of the globe.

In addition, there is no trademark "ecotourism", or label or official charter, so any tour operator can claim an "ecotourism" approach for business. This abundance creates confusion and lack of control opens the door to any abuse.

If massive tourism has its adverse effects, massive ecotourism also creates perverse effects. To attract tourists, countries created protected areas, and do not hesitate to move people to create a "virgin nature" effect. To see that, the Natural Park of Nechisar in southwestern Ethiopia is a good example. Since 2005, in response to competition from other reserves in Africa, an arsenal of regulations law limited the exploitation of resources (hunting, fishing, and gathering firewood) to accentuate the wild character of the site (Guyot, 2004). To survive, people are forced to accept small jobs service to tourists (guides, crafts, folklore). Today, the park receives more than 20,000 visitors each year.

Nachisar situation is not an isolated case. Since ten years, many parks, reserves and protected areas have been created in the world. Often, the first justification is to promote the dissemination of international tourism from major websites to other areas outside of development.

But the phenomenon also asks the question of demand and the travelers responsibility in the production of these protected areas.

Source : SV -CRISES 2013

Without going into details, we can see on this table that individual motivation for ecotourism can be the result of a trade-off between sometimes conflicting expectations, good intentions and personal needs. The best example is renting a luxury eco-lodge in the jungle.

In front of these abuses, contradictions and perverse effects, the balance of ecotourism may appear nuanced. We can say that this sustainable tourism model has gradually moved away from its original intention. What was originally a militant approach, becoming a fashion? Still, the search for a sustainable balance between societies and their environment is always waiting.

In conclusion, I suggest a perspective through a last example, in France.

The "Oysters road in Charente" seeks to reconcile tourism, environment and human activity. The particularity of this tourism offer is that it is not just a consumer product. This is the result of a project approach, involving public authorities and private economic actors to share and live their territory. And it works well! Through this example, we can finally ask if ecotourism is the goal. Is it not rather the result of a contractual approach around a project area? Is not the real issue in the search for shared governance? The future is open.

Source : SV -CRISES 2013

  Source : SV -CRISES 2013

  Source : SV -CRISES 2013Created in the middle of the seventies by the military government, local people have been driven from their territory of life sometimes violently. Ethnic conflicts have become common in this region of Rif.

Source : SV -CRISES 2013


Michaël Delqué

Thibaut Sylvestre

Hervé Maillotte

Cyril Cambournac

Pascal Kockaert

Marc Haelterman

Experimental observation of the elliptically polarized fundamental vector soliton of isotropic Kerr media

We report the experimental observation of the elliptically polarized fundamental vector soliton of isotropic Kerr media and its unique polarization evolution. This was achieved in the spatial domain in a nonbirefringent CS 2 planar waveguide.

The vector nature of polarized light propagating in nonlinear dispersive or diffractive media [1][2][3] has led to the discovery of a novel class of solitary-wave solution of the two coupled nonlinear Schrödinger (NLS) equations. [4][5][6][7][8] As initially demonstrated theoretically in birefringent media by Christodoulides and Joseph 7 and by Tratnik and Sipe, 8 these solutions are stationary polarization bound states, thus leading to the concept of the vector soliton. A few years later, Haelterman and Sheppard 9 demonstrated analytically and numerically the existence of such vector solitons in isotropic Kerr media, i.e., without linear birefringence. In addition to both the well-known linearly and circularly polarized NLS solitons, they found new solutions that consist of elliptically polarized fundamental vector solitons (EPVSs). In particular, they exhibit a nonuniform transverse ellipticity profile, and their global polarization state regularly rotates during propagation. This property is reminiscent of the self-induced nonlinear birefringence that is due to cross-phase modulation between the two circular polarization components of the soliton. Until now, to our knowledge no experimental demonstration of EPVSs in isotropic media had been made. In this Letter we report the experimental observation and characterization of a spatial EPVS generated in a Kerr liquid planar waveguide.

The experiment, schematically sketched in Fig. 1, is performed ina3c mlong CS 2 liquid planar slab waveguide. The step-index waveguide is made from a 15 m thick CS 2 layer sandwiched between two SK5 glass plates, whose index difference is ⌬n = 0.04. 10 A beat length of L = 1.7 m much longer than the waveguide length was measured, which ensures the quasiisotropic condition to generate and maintain the EPVS. As a pump laser source we use a compact passively Q-switched microchip Nd:YAG laser emitting 600 ps Gaussian pulses at a repetition rate of 6.7 kHz and at a wavelength of 532 nm (the mean power is 30 mW). The high power stability ͑Ͻ1 % rms͒ as well as the smooth circular TEM 00 beam profile of the laser allows one to generate a spatial soliton with excellent transverse stability and therefore to measure its polarization state accurately. The elliptic polarization state of the input beam was adjusted by means of a quarter-wave plate. A couple of cylindrical lenses ͑Lx1,Lx2͒ were inserted to adjust horizontal size x of the beam (soliton width) without changing vertical size y. At the waveguide's output, a second quarterwave plate and a Wollaston biprism (W) were used to extract either the ͑E x , E y ͒ linearly polarized components or the ͑U , V͒ circularly polarized components, depending on orientations on the wave plate and the prism. First, to get access to the global polarization state we directly observe the energy ratio between the linearly polarized components. Second, we measure the ellipticity factor across the transverse beam profile by means of the circularly polarized components, using the following definition:

q͑x͒ = ͓͉U͑x͉͒ 2 -͉V͑x͉͒ 2 ͔ / ͓͉U͑x͉͒ 2 + ͉V͑x͉͒ 2 ͔.
The results of our experiment are detailed in Fig. 2. Figures 2(a)-2(c) illustrate the E x and E y profiles at the waveguide's input and output in linear and soliton regimes, respectively. Figures 2(d)-2(f) exhibit the U and V intensity profiles in the same conditions. Additionally, in Figs. 2(d)-2(f) we have plotted (dotted curves) measured ellipticity factor q. Let us recall that the values q = ± 1, 0 represent circular and linear polarization, respectively. The first quarter-wave plate is then tuned such that the input ellipticity factor is 0.29, and it is of course constant all across the transverse beam profile, as shown by the dotted curve in Fig. 2(d). For this degree of ellipticity, one can see from Fig. 2(a) that the power of the E y polarization is much less than that of the E x polarization. Figures 2(b We note clear diffraction of the beam whose full width at half-maximum (FWHM) is twofold compared with that of the input beam. The elliptic polarization is still flat across the beam, and no polarization rotation occurs. Note, however, that a small change in the U / V ratio appears because of the residual birefringence of optical elements in the setup.

When the soliton regime is reached, i.e., for a mean pump power of 4 mW (maximum intensity of 4.4 ϫ 10 11 Wm -2 ), self-focusing compensates exactly for diffraction: the beam's output FWHM is equal to the input FWHM. The results of this soliton regime are presented in Figs. 2(c) and 2(f), which show clear reshaping of the input Gaussian beams into hyperbolic secant-shaped profiles at the output for both linear and circular polarization. In addition, the E y polarization shown in Fig. 2(c) has much more energy than in the linear regime, meaning global polarization rotation of the soliton. As the ellipticity factor is rather small, one can approximate global polarization orientation angle by tan 2 ͑͒ϷIx/ Iy. Thus, in our experiment, the global soliton polarization rotation is out -in Ϸ / 5. Moreover, we can see from Fig. 2(f) that the polarization state is no longer uniform across the entire beam, and the ellipticity factor exhibits a difference of ⌬q = 0.23 between the center and the wings of the beam, as predicted by theory. 9 We also measured different widths for the U and V beams of 53 and 45 m, respectively. As a matter of fact, nonlinear reshaping of the U and V circular polarizations of the beam occurs during propagation without energy exchange, leading to different widths for the U and V beams. At this point it is important to claim that the vector soliton is fully formed and stabilized. Note also that a complete experimental analysis of the polar-ization state of the EPVS by Stokes parameters is currently being conducted.

We have been able to reproduce these observations numerically with a set of two coupled NLS equations that govern propagation of polarized light in isotropic Kerr media. Let us rewrite the incoherently coupled NLS equations on the basis of circular polarization 9,10 :

ץU ץz = i 2k ץ 2 U ץx 2 + i␥͓͑1-B͉͒U͉ 2 + ͑1+B͉͒V͉ 2 ͔U, ץV ץz = i 2k ץ 2 V ץx 2 + i␥͓͑1-B͉͒V͉ 2 + ͑1+B͉͒U͉ 2 ͔V. ͑1͒
Here z is the propagation direction coordinate and x is the free transverse dimension of the planar waveguide. U , V=͑E x ± iE y ͒ / ͱ 2 are the left-handed and the right-handed circularly polarized components of the electric field and E x and E y are the associated orthogonal linearly polarized components, respectively. k is the effective wave vector, ␥ =2n 2 / 0 is a nonlinear coefficient, n 2 = 3.5ϫ 10 -18 m 2 W -1 (see, e.g., Ref. 11) is the nonlinear refractive index, and 0 is the vacuum field wavelength. B = xyyx / xxxx is the polar- ization susceptibility ratio. We consider here, for the Kerr nonlinearity, the molecular reorientation effect of CS 2 , which prevails in the picosecond regime. In this case B =3/4, and we can expect a strong nonlinear birefringence. 12 We performed numerical simulations by using the above experimental parameters. The theoretical results are illustrated in Fig. 3 and show excellent agreement with the experimental results depicted in and E y (dashed curves), intensity profiles of, respectively, the input beam (FWHM, 49 m), the output beam at low power (FWHM, 100 m), and the output beam in the soliton regime (FWHM, 51 m). (d), (e), (f) Intensity profiles for left-handed U (solid curves) and right-handed V (dashed curves) circular polarization and ellipticity factor q (dotted curve). Note that in the soliton regime FWHM͑U͒ =53 m is different from FWHM͑V͒ =45 m. Fig. 2. In particular, we can clearly see that there is no energy exchange between opposite circular polarization components in Figs. 2(e) and 2(f). We also retrieved theoretically the curvature of the ellipticity factor across the transverse profile [⌬q = 0.3; dotted curve in Fig. 2(f)], which is a specific feature of EPVSs propagating in a nonbirefringent medium because it results from mutual reshaping between opposite circular polarization.

To clearly identify soliton propagation, we numerically calculated in Fig. 4 the longitudinal evolution of the total field intensity (contour plots) in both the linear and the soliton regimes over a longer distance (10 cm) than in Figs. 2 and3 (3 cm). Figure 4(c) also shows a contour plot that illustrates the evolution of polarization ellipticity factor q in the soliton regime. Once again the linear regime shows strong diffraction-induced beam widening, whereas the nonlinear regime exhibits soliton reshaping and further invariant propagation of the vector soliton. Moreover, Fig. 4(c) shows that, once polarization ellipticity q has decreased at the center of the spatial soliton, it remains constant all along the propagation.

To conclude, with the help of an original polarization-measurement setup we have confirmed experimentally the existence of the so-called elliptically polarized fundamental vector soliton theoretically predicted in 1994 for isotropic Kerr media. 9 Our observations confirmed its characteristic polarization evolution and, in particular, the curve-shaped elliptic polarization profile across the beam. Finally, with a view to potential applications, one can deduce from these experiments that the nonlinear isotropic medium acts as a power-dependent variable and tunable wave plate. More fundamentally, the EPVS is the stable solution after symmetry breaking of multimode vector solitons in Kerr media, as described in Refs. 10 and 12.

Fig. 1 .

 1 Fig. 1. Experimental setup.

Fig. 3 .

 3 Fig. 3. Theoretical results. (a), (b), (c) E x (solid curves) and E y (dashed curves), intensity profiles for, respectively, the input beam (FWHM, 49 m), the output beam at low power (FWHM, 100 m), and the output beam in the soliton regime (FWHM, 49 m). (d), (e), (f) Corresponding U (solid curves), V (dashed curves), and q (dotted curves) profiles. Note that in the soliton regime FWHM͑U͒ =53 m is different from FWHM͑V͒ =49 m. Parameters are k = 1.94 ϫ 10 7 m -1 , ␥ = 4.1ϫ 10 -11 mW -1 , and maximum input intensity I = 4.5ϫ 10 11 Wm -2 .

Fig. 2 .

 2 Fig. 2. Experimental results. (a), (b), (c) E x (solid curves)and E y (dashed curves), intensity profiles of, respectively, the input beam (FWHM, 49 m), the output beam at low power (FWHM, 100 m), and the output beam in the soliton regime (FWHM, 51 m). (d), (e), (f) Intensity profiles for left-handed U (solid curves) and right-handed V (dashed curves) circular polarization and ellipticity factor q (dotted curve). Note that in the soliton regime FWHM͑U͒ =53 m is different from FWHM͑V͒ =45 m.

0146-9592/05/243383-3/$15.00 © 2005 Optical Society of America

OPTICS LETTERS / Vol. 30, No. 24 / December 15, 2005

December 15, 2005 / Vol. 30, No. 24 / OPTICS LETTERS