Jérôme Poineau
email: jerome.poineau@math.unistra.fr

POLYNOMIAL APPROXIMATION OF BERKOVICH SPACES AND DEFINABLE TYPES

Keywords: 2010 Mathematics Subject Classification. 14G22, 12J25, 14P10, 03C98 Berkovich spaces, non-Archimedean analytic geometry, maximally complete fields, spherically complete fields, semi-algebraic sets, definable types

We investigate affine Berkovich spaces over maximally complete fields and prove that they may be approximated by simpler spaces when the only functions we need to evaluate are polynomials of bounded degree. We derive applications to semi-algebraic sets and recover a result of E. Hrushovski and F. Loeser which claims that points of Berkovich spaces give rise to definable types (a model-theoretic notion of tameness).

Introduction

In the late eighties, V. Berkovich came up with a new definition of p-adic analytic spaces, and more generally analytic spaces over a complete valued field k. It is remarkable that, in this setting, the affine line A 1,an k over k always contains many points in addition to those belonging to k. This feature, which may seems disturbing at first sight, leads to numerous interesting consequences. For instance, it lets the space A 1,an k carry a nice topology, where properties such as path-connectedness and local compactness are satisfied, regarless of the fact that the field k may be totally disconnected and not locally compact.

On the other hand, due precisely to this abundance of extra points, Berkovich spaces are often difficult to describe explicitely. A noteworthy exception is that of the analytic line A 1,an k over an algebraically closed field k. In this situation, V. Berkovich managed to give a complete classification of the points, which are gathered into four types. The simplest case is that of maximally complete fields, where only three types remain, which all correspond to avatars of generic points of discs (the type being determined by a condition on the radius).

In this paper, we are interested in the case of a general affine space A n,an k over a maximally complete field (not necessarily algebraically closed). Let us say at once that we will not give a description which is as explicit as the one provided by V. Berkovich for the line (we believe such a task to be hopeless in general) but a succession of "approximations". More precisely, if we fix a point x in A n,an and a degree d for polynomials in n variables, we will show how to construct a simple space S x,d (similar to the disc mentionned before in dimension 1, more complicated in higher dimension) which determines the value of any polynomial of degree at most d at the point x.

As an application, in the last part of the paper, we prove semi-algebraicity results. We also explain how to recover, in a geometric fashion, the fact, observed by E. Hrushovski and F. Loeser, that points of affine Berkovich spaces give rise to definable types (a model-theoretic notion of tameness) 1 .

Approximation in dimension 1

Let (k, |.|) be a field endowed with a (possibly trivial) non-Archimedean absolute value, with respect to which it is complete. We will have a special interest in fields k that are maximally complete. Let us recall that this condition means that the field k has no non-trivial immediate extension, i.e. with the same residue field and the same value group. By a theorem of I. Kaplansly (see [START_REF] Kaplansky | Maximal fields with valuations[END_REF]), it is equivalent to the spherical completeness of the field: a family of embedded discs cannot have an empty intersection. This last condition is the only one we shall use in this paper. It is easy to check that trivially valued fields and complete discrete valuation fields are maximally complete. For a more complicated example, consider the extension F ((t Q )) of a field F given by series q∈Q a q t q with a well-ordered support. For more on this subject (such as a mixed-characteristic analogue of the previous construction), we advise the reader to have a look at B. Poonen's nice paper [START_REF] Poonen | Maximally complete fields[END_REF].

In this first section, we will be interested in the affine analytic line A 1,an k over the field k, in the sense of V. Berkovich. We refer to [START_REF] Vladimir | Spectral theory and analytic geometry over non-Archimedean fields[END_REF] for basic results concerning Berkovich spaces. Actually, in this paper, we will not need much beyond the first chapter of the book.

Let us choose some notations. We will denote T the variable on A 1,an k . For any integer d, we denote k[T ] ≤d the k-vector space of polynomials of degree at most d. 1 It is unfortunate that two notions of type appear in this paper. The model-theoretic notion is not to be confused with the one used by V. Berkovich to classify the points of the line.

Let P be an irreducible polynomial. We denote η P,0 the unique point in A 1,an k such that P (η P,0 ) = 0. Let r > 0. The Shilov boundary of the affinoid domain {|P | ≤ r}, which coincides with its topological boundary, contains a unique point, that we denote η P,r . From a model-theoretic point of view, this is the generic type of the subset {|P | ≤ r}.

Let us denote D 0 = {η T,1 } and for every integer d ≥ 1,

D d = {η P,r , P ∈ k[T ] ≤d , r ≥ 0}.
Remark 1.1. For any points x = y ∈ D d , there exists a polynomial

P ∈ k[T ] ≤d such that |P (x)| = |P (y)|.
Let us add a few words on V. Berkovich's classifications of the points of A 1,an k (see [START_REF] Vladimir | Spectral theory and analytic geometry over non-Archimedean fields[END_REF], § 1.4). When the field k is algebraically closed and maximally complete, he proves that every point is of the form η T -a,r , with a ∈ k and r ≥ 0. We would like to adapt this classification when the condition of being algebraically closed is removed. In this case, polynomials of degree bigger than 1 cannot be decomposed into polynomials of degree 1 and they have to enter the picture too. Actually, we believe that V. Berkovich's result should, in general, be thought of as a kind of approximation of A 1,an k , where only polynomials of degree 1 are considered. We observe that his construction may actually be generalized in any degree.

Theorem 1.2. Assume that k is maximally complete. Let x be a point of A 1,an k . For any integer d ≥ 0, there exists a unique point x d in D d with the following property:

∀P ∈ k[T ] ≤d , |P (x d )| = |P (x)|.
In addition, x d ≥ x and

x d = inf({y ∈ D d | y ≥ x}).
Proof. The uniqueness follows from remark 1.1. Let us assume that we found Let us now assume that there exists A ∈ k[T ] ≤d+1 such that |A(x)| < |A(x d )|. We may assume that A is monic of degree d + 1.

x d = η Q,r
Let k d denote the set {P (x), P ∈ k[T ] ≤d }. It is a finite-dimensional normed k-vector space. Since k is spherically complete, k d is spherically complete too (cf. [START_REF] Bosch | Non-Archimedean analysis[END_REF], 2.4.4).

For any polynomial P in k[T ] ≤d , let us consider the ball

E P = D(P (T )(x), |(T d+1 -P (T ))(x)|) inside k d . Let P, Q ∈ k[T ] ≤d . If |(T d+1 -P (T ))(x)| ≤ |(T d+1 -Q(T ))(x)|, then |P (T )(x) -Q(T )(x)| ≤ |(T d+1 -Q(T ))(x)|, hence P (T )(x) ∈ E Q and E P ⊂ E Q .
Since k d is spherically complete, there exists P 0 ∈ k[T ] ≤d such that P 0 (T )(x) belongs to all the E P 's. Let R 0 (T ) = T d+1 -P 0 (T ) and

r = |(R 0 (T ))(x)| = inf P ∈k[T ] ≤d (|(T d+1 -P (T ))(x)|). Let R ∈ k[T ] ≤d+1 be a monic polynomial of degree d + 1. An easy computation shows that |R(x)| = max(r, |(R -R 0 )(x d )|). Using |(A -R 0 )(x)| = |(A -R 0 )(x d )|, |A(x)| < |A(x d )| and |R 0 (x)| ≤ |A(x)|, we find |R 0 (x)| < |R 0 (x d )|.
In particular, R 0 is irreducible. We want to prove that η R 0 ,r satisfies the property of the statement.

Since η R 0 ,r and x d are at least x, they are comparable. From the inequality |R 0 (x d )| > r, we deduce that x d ≥ η R 0 ,r ≥ x. Hence we have x d = (η R 0 ,r ) d . Now, for every monic polynomial R of degree d + 1, we have

|R(η R 0 ,r )| ≤ max(r, |(R -R 0 )(η R 0 ,r )|) = max(r, |(R -R 0 )(x d )|) = |R(x)|
and we are done.

′ ≥ d, we have (x d ′ ) d = x d . Corollary 1.3. Assume that k is maximally complete. The map A 1,an k → lim ← - d≥0 D d is a bijection.
Remark 1.4. It is also possible to describe the union of the sets D d . In the case where k is maximally complete, it contains all the points except some of type 1: those associated to the absolute values

P (T ) ∈ k[T ] → |P (α)| ∈ R + ,
where α is an element of k, the completion of an algebraic closure of the field k, which is transcendental over k.

Approximation in higher dimensions

In this second part, we would like to extend the approximation result of the previous section to the case of a general affine analytic space A n,an k , with n ∈ N. We will denote T = (T 1 , . . . , T n ) the variables on A n,an k . We endow N n with the following order relation:

(d 1 , . . . , d n ) < (d ′ 1 , . . . , d ′ n ) if n i=1 d i < n i=1 d ′ i or n i=1 d i = n i=1 d ′ i and ∃j ∈ [[0, n -1]], ∀i ≤ j, d i = d ′ i and d j+1 < d ′ j+1 . Let d ∈ N n . We denote k[T ] ≤d the k-vector space of polynomials of degree at most d. Let R ⊂ R + . We denote S d,R (or S d when R = R + ) the set of subsets of A n,an k of the form 1≤i≤r {|P i | ≤ r i }, with P i ∈ k[T ] ≤d and r i ∈ R. Let D d,R be the union of the Shilov boundaries of elements of S d,R .
If K is a non-empty compact subset of A n,an k , we let . K denote the sup-norm on K.

Lemma 2.1. Let K be a compact subset of A n,an k . Let d ∈ N n and assume that there exists a monic polynomial R 0 of degree d such that, for any monic polynomial R of degree d, we have R 0 K ≤ R K . Then, for any monic polynomial R of degree d, we have

R K = max( R 0 K , R -R 0 K ). Theorem 2.2. Assume that k is maximally complete. Let K be a non-empty compact subset of A n,an k . Let d ∈ N n . There exists a unique set S K,d in S d containing K such that ∀P ∈ k[T ] ≤d , P S K,d = P K .

Moreover, we have

S K,d = P ∈k[T ] ≤d {|P | ≤ P K } ∈ S d,R , where R ⊂ R + is the image of k[T ] ≤d by the sup-norm . K .
Proof. The uniqueness and the last statement are clear. Let us prove the existence of S K,d by induction on d.

If d = 0, choose S 0 = A n,an k . Let d ∈ N n \ {0}. Let d ′
be the predecessor of d and assume we found S K,d ′ in S K,d ′ that satisfies the conditions of the statement. Let E be the separated completion of k[T ] ≤d ′ with respect to the semi-norm . K . It is a spherically complete k-vector space. Let j : k[T ] ≤d ′ → E be the canonical morphism.

The family of balls D P = D(j(P (T )), T d -P (T ) K ) P ∈k[T ] ≤d ′ is nested.

Let j(P 0 (T )) be an element in the intersection. Let R 0 (T ) = T d -P 0 (T ) and

r = R 0 (T ) K = inf P ∈k[T ] ≤d ′ ( T d -P (T ) K ).
Let us now set

S K,d = S K,d ′ ∩ {|R 0 | ≤ r}.
This is an element of S d,R that contains K. For any polynomial P of degree smaller than d, we have P K = P S K,d ′ = P S K,d . Moreover, by lemma 2.1, for every monic polynomial R of degree d, we have

R K = max( R 0 K , R -R 0 K ) = max(r, R -R 0 S K,d ).
Using the fact that R 0 S K,d = r, we deduce that

R K = R S K,d .
Remark 2.3. As we found out after we wrote this paper, our construction is not unrelated to that of [HL10], § 5.1. Proof. Choose for η 1 , . . . , η r the points of the Shilov boundary of the k-affinoid space S K,d of the theorem.

Remark 2.5. If the compact K is a singleton {x}, the result of theorem 2.2 in dimension 1 seems to be weaker than that of theorem 1.2, but it is actually easy to see that they are equivalent. As a matter of fact, the sets S x,d are finite unions of virtual discs of the form {|P | ≤ r}, where P is an irreducible factor of a polynomial that appears in the definition of S d . If x belongs to the disc {|P | ≤ r}, then the point η P,r satisfies the properties of theorem 1.2.

Remark 2.6. Even when K is a singleton {x}, the generalisation to higher dimension needs to be handled with some care. For example, it is not true that the set S x,d may be written in the form

{|P 1 (T 1 )| ≤ r 1 } ∩ {|P 1 (T 1 , T 2 )| ≤ r 2 } ∩ • • • ∩ {|P 1 (T 1 , . . . , T n )| ≤ r n }.
Let us give an example. We will assume that the characteristic of k is not 2. Let r, s ∈ [0, 1) with s < r 3 . Let us consider the point η r in A 1,an k which is the unique point in the Shilov boundary of {|T 1 | ≤ r}. Around this point, the fonction 1+T 1 has a square root given by the usual development

√ 1 + T 1 = 1 + 1 2 T -1 8 T 2 + . . . Let x in A 2,an
k be the point in the fiber over η r which is the unique point in the Shilov boundary of

{|T 2 - √ 1 + T 1 | ≤ s}. The subset S x,(2,0) is not the naive {|T 1 | ≤ r} ∩ {|T 2 -(1 + 1 2 T - 1 8 T 2 )| ≤ s} but {|T 1 | ≤ r} ∩ {|T 2 2 -(1 + T 1 )| ≤ s} ∩ {|T 2 -1| ≤ s}.
Remark 2.7. It is not true either that the set S x,d has a unique point in its Shilov boundary in general. Let us consider the point η 1 in A 1,an k (with variable T 1 ) and the point x in A 3,an k (with variables T 1 , T 2 , T 3 ) over it defined by the equations

T 2 = T 4 1 and T 3 = T 6 1 . It is possible to check that S x,(3,0) = {|T 1 | ≤ 1} ∩ {|T 2 | ≤ 1} ∩ {|T 3 | ≤ 1} ∩ {T 2 1 T 2 -T 3 = T 2 1 T 3 -T 2 2 = T 3 2 -T 2 3 = 0}.
This is a Zariski closed subset of the unit closed ball in A 3,an k , which has two irreducible components (defined one by T 2 -T 4 1 = T 3 -T 6 1 = 0, the other by T 2 = T 3 = 0), hence two points in its Shilov boundary. We are grateful to N. D. Elkies, who kindly communicated this example to us (see [START_REF] Elkies | Degree of generators of irreducible components[END_REF]).

Corollary 2.8. Assume that k is maximally complete. Let d ∈ N n . Let P be a family of polynomials of degrees at most d. Let (r P ) P ∈P be a family of real numbers. Assume that the subset of A n,an k defined by

K = P ∈P {|P | ≤ r P } is compact. Then it belongs to S d .
Proof. We may assume that K is non-empty. It is easy to check that

K = Q∈k[T ] ≤d {|Q| ≤ Q K }.
By theorem 2.2, the latter set belongs to S d .

Remark 2.9. The result fails if the degrees are not bounded. Assume that k is not trivially valued. Let r > 0. Let (α n ) n≥0 be a sequence of elements of k such that the sequence of real numbers (|α n | r n ) n≥0 is decreasing and has a positive limit. Let us consider the intersection

{|T 1 | ≤ r} ∩ n≥1 |T 2 - n i=0 α i T i 1 | ≤ |α n+1 |r n+1
in A 2,an k . It is compact but not affinoid. For example, one may check that over η r , it contains only one point, which is of type 4 over H (η r ). Corollary 2.10. Assume that k is algebraically closed and maximally complete. Let d ∈ N n . Let I be a linearly ordered set and (V i ) i∈I be a decreasing family of non-empty elements of S d (k). Assume that there exists a disc D(0, s) with s ∈ R n + that contains all the V i 's. Then the intersection i∈I V i is non empty.

Proof. If k is trivially valued, it is a result about Zariski closed subsets of A n k and we conclude by the noetherianity of the Zariski topology.

Let us now assume that k is not trivially valued. Let D = D(0, s) ⊂ A n,an k . Let i ∈ I. There exists an integer p i , polynomials P i,1 , . . . , P i,p i in k[T ] ≤d and real numbers r i,1 , . . . , r i,p i such that

V i = 1≤j≤p i x ∈ k n |P i,j | ≤ r i,j .

Let us set

W i = 1≤j≤p i x ∈ A n,an k |P i,j | ≤ r i,j ∩ D.
If J is a finite subset of I, the intersection i∈J W i contains i∈J V i , hence is non-empty. Since D is compact, we deduce that i∈I W i is non-empty. By the preceeding corollary, it belongs to S d . Since k is algebraically closed and not trivially valued, it has a k-point, which necessarily belongs to i∈I V i .

Remark 2.11. The result fails if we do not assume that the W i belong to some disc (in dimension at least 2 and for non-trivially valued fields). Consider for instance {|T 1 -1| ≤ r} ∩ n≥0 {|T 1 T 2 | ≤ r n }, for some r ∈ (0, 1).

Definable types

In this last part of the paper, we would like to apply some model-theoretic notions in the setting of Berkovich spaces. We refer to [START_REF] Marker | Model theory: An introduction[END_REF] for the basic definitions and results of model theory. We will use freely the rather intuitive notions of language, formula (built from the language possibly with variables and quantifiers) and sentence (formula with no free variable).

Since we work with Berkovich spaces, it is natural to consider valued fields (k, |.|). From the model-theoretic point of view, we will use the language L div , which is the language of rings (+, -, ., 0, 1) endowed with an extra binary predicate "div", with div(x, y) interpreted as |x| ≤ |y|. We will work with the theory "ACVF" of algebraically closed valued fields with non-trivial valuation. One may check that the axioms needed may actually be written down in the language L div . Beware that there is no restriction on the rank of the valuation. For this reason, we will need to be careful when turning to Berkovich spaces. Remark that there is no way to get around this pitfall since valuations cannot be forced to have rank 1 by first-order formulas.

Let us recall one of the basic results of the theory, which is essentially due to A. Robinson (see [START_REF] Robinson | Complete theories[END_REF]). Theorem 3.1. i) The theory ACVF eliminates quantifiers: every formula is equivalent to a formula with no quantifiers. ii) Any embedding K ⊂ L of algebraically closed valued fields with non-trivial valuations is elementary: a sentence with parameters in K holds in K if, and only if, it holds in L. (The theory ACVF is said to be model-complete.)

We plan to apply model-theoretic results to Berkovich spaces. In this setting, it is sometimes important to consider trivially valued fields, hence we would rather not exclude them in our model-theoretic arguments. It is of course possible to define the theory of algebraically closed trivially valued fields with the language L div . Let us remark that, in this case, the binary predicate div is redondant since the formula div(x, y) is equivalent to x = 0 ∨ (x = 0 ∧ y = 0). In other words, this theory is equivalent to the theory of algebraically closed fields, which is model-complete and eliminates quantifiers (see [START_REF] Marker | Model theory: An introduction[END_REF], §3.2).

In the sequel, we will allow ourselves to use model-completeness and quantifier elimination for algebraically closed valued fields, regardless of the fact that the valuation is trivial or not. Beware that this forces us to consider only trivially valued extensions of trivially valued fields.

We now introduce one more definition, that of a type. This model-theoretic notion is analogous to the notion of point of a Berkovich space. Definition 3.2. Let p be a set of formulas with parameters in A ⊂ k and free variables from u = (u 1 , . . . , u n ). We say that p is a type if p ∪ Th A (k) is satisfiable, where Th A (k) denotes the set of sentences with parameters in A that hold in k. We say that a type p is complete if, for any formula ϕ(u), either ϕ(u) or ¬ϕ(u) belongs to p.

The basic example of type is constructed as follows. Let K be an algebraically closed extension of k (with trivial valuation if k has trivial valuation). Let a ∈ K n . The set of formulas ϕ(u) with parameters in A ⊂ k such that ϕ(a) holds in K is a complete type, denoted tp K (a/A). It is also possible to associate a complete type to any point x of A n,an k (either directly or by using the previous construction and considering tp L (|T 1 (x)|, . . . , |T n (x)|/A), where L is any algebraically closed extension of H (x)).

The converse statement is true, with some restrictions for the part concerning Berkovich spaces. General model-theoretic arguments (see [START_REF] Marker | Model theory: An introduction[END_REF], corollary 4.1.4) show that, for any complete type p with parameters in A, there exists an elementary extension K of k and a point a ∈ K n such that p = tp K (a/A). But it may well happen that the valuation of K has a rank greater than 1, which prevents it from defining a point in A n,an k . The generic type of the open unit ball gives such an example, since the valuation group of any of its realizations contains an infinitesimal below 1. Definition 3.3. Let p be a type with parameters in A ⊂ k and free variables from u = (u 1 , . . . , u n ). The type p is said to be definable over B ⊂ k if, for every formula ϕ(u, v) (without parameters), the exists a formula d p (ϕ)(v) with parameters in B such that, for any a ∈ A m , the formula ϕ(u, a) belongs to p if, and only if, d p (ϕ)(a) holds in k.

As we said above, points of affine Berkovich spaces give rise to types, but not always definable types. In A 1,an k with k algebraically closed and |k| = R + , for instance, definable types correspond to points of type 1, 2 or 3, but not 4 (consider the formula ϕ(u, a, b) : |u -a| ≤ |b| ; see [START_REF] Haskell | Definable sets in algebraically closed valued fields: elimination of imaginaries[END_REF], lemma 2.3.8, for more on this question). Therefore, if k is algebraically closed and maximally complete and if |k| = R + , every point in A 1,an k corresponds to a definable type. But even over such a field, points of type 4 may appear again in higher dimensions. Indeed the residue field H (x) of a point x of type 2 in A 1,an k fails to be maximally complete (in the non-trivially valued case). Hence, the fiber of the projection A 2,an k → A 1,an k over the point x, which is isomorphic to A 1,an H (x) , contains points of type 4 (see remark 2.9).

In [START_REF] Hrushovski | Non-archimedean tame topology and stably dominated types[END_REF], lemma 13.1.1, E. Hrushovski and F. Loeser explain that, over an algebraically closed and maximally complete field k with value group R + , points of A n,an k , for any n, correspond to (stably dominated) definable types. The proof is quite short but it makes use of the relation between types which are orthogonal to the value group and stably dominated types, as well as a criterion for a type to be stably dominated over an algebraically closed and maximally complete field, two difficult results from [START_REF] Haskell | Stable domination and independence in algebraically closed valued fields[END_REF]. As the reader may have guessed from the previous discussion, this result came to the author as a true surprise!

In what follows, we will try to explain in geometric terms what being a definable type means and recover E. Hrushovski and F. Loeser's result using our work from the previous sections. The rough idea is that points in D are definable types, which follows easily from quantifier elimination, and that other points are "approximated" by those (in the sense of corollary 2.4). This approximation is good enough for type-definability. Indeed, to check it, we only need to consider one formula at a time and, any formula being finite, it is possible to bound the degree of the polynomials that appear in it.

Let us first recall the definition of a semi-algebraic set (see [START_REF] Ducros | Parties semi-algébriques d'une variété algébrique p-adique[END_REF] définition 1.2). Since S is definable over k, this proves that the subset of the statement is definable over k, hence strictly semi-algebraic by quantifier elimination.

Definition 3.4. A subset V of A n,an k is called semi-algebraic (resp. strictly semi-algebraic) if it is a finite boolean combination of subsets of the form {|P | ≤ λ|Q|} with P, Q ∈ k[T ] and λ ∈ R + (resp. λ ∈ {0, 1}).
Remark 3.6. When k is algebraically closed, the statement exactly means that the type p x corresponding to the point x is definable (over k). Let ϕ(u, v) be a formula with u and v of lengths n and m. We want to find a formula d x (ϕ)(v) such that, for any y ∈ k m , ϕ(u, y) belongs to p x if, and only if, d x (ϕ)(y) holds in k. By quantifier elimination, we may assume that ϕ is a quantifier-free formula. In this case, it defines a strictly semi-algebraic subset V of A m+n,an k . We now are in the situation of the theorem and any formula defining

{y ∈ k m | x ∈ V ∩ π -1 (y)} will do.
The fact that a point over k corresponds to a definable type will enable us to extend it canonically over extensions K/k. Corollary 3.7. Assume that k is maximally complete and algebraically closed. Let n be an integer and x be a point in A n,an k such that |H (x)| = |k|. Let (S d ) d∈N n be the family of subsets associated to x by theorem 2.2.

Let K/k be an extension of complete valued fields. If k is trivially valued, assume that K is trivially valued too. Let π : A n,an K → A n,an k be the natural morphism. There exists a unique point σ

K (x) ∈ A n,an K such that ∀d ∈ N n , ∀P ∈ K[T ] ≤d , P π -1 (S d ) = |P (σ K (x))|.
Moreover, the point σ K (x) may also be characterized by the following property:

∀P ∈ K[T ], |P (σ K (x))| = P π -1 (x) .
Proof. We may assume that K is algebraically closed. Then it is an elementary extension of k. The point x corresponds to a type p x over k, which is definable by remark 3.6. We define a type q = p x |K over K using the following recipe (and the notations of the remark). For any v ∈ K m , the formula ϕ(u, v) belongs to q exactly when d x (ϕ)(v) holds in K. To check that this indeed defines a type over K, we only need to check that finite subsets of formulas of q are consistent with the theory of K. Let ϕ 1 (u, v 1 ), . . . , ϕ r (u, v r ) ∈ q. By definition of the d x (ϕ)'s and the fact that p x is a type, the sentence ∀w 1 , . . . , w r , belongs to p x . Hence it also belongs to q, which means that q corresponds to a point of A n,an K . We will denote it σ K (x).

1≤i≤r d x (ϕ i )(w i ) → ∃u,
Let d ∈ N n . There exists polynomials P 1 , . . . , P t ∈ k[T ] d and real numbers r 1 , . . . , r t ∈ {0, 1} such that

S d = 1≤i≤t {|P i | ≤ r i }.
Let us consider a formula ϕ(u, v) expressing the fact that the sup-norm on S d of a polynomial P of degree at most d is realized at the point we consider. More precisely, the formula ϕ(u, v) looks like

∀ polynomial P of degree at most d, ∀a, |Q 1 (a)| ≤ r 1 ∧ • • • ∧ |Q t (a)| ≤ r t → |P (a)| ≤ |P (u)| ∧ ∃a, |Q 1 (a)| ≤ r 1 ∧ • • • ∧ |Q t (a)| ≤ r t ∧ |P (a)| = |P (u)| ,
where v encodes the coefficients of the Q i 's.

When v is specialized to the tuple v 0 that corresponds to the coefficients of the P i 's, the formula ϕ(u, v 0 ) belongs to the type p x , so d ϕ (v 0 ) holds in k, hence in K. By definition, ϕ(u, v 0 ) then belongs to the type q = p x |K, which exactly means that, for any polynomial P of degree at most d, |P (σ K (x))| is equal to the sup-norm of P on π -1 (S d ) (which is defined by the same inequalities as S d ). We have now proved the existence of a point x K satisfying the required conditions. Its uniqueness is clear, as well as the last statement.

Remark 3.8. In [START_REF] Vladimir | Spectral theory and analytic geometry over non-Archimedean fields[END_REF], § 5.2, V. Berkovich introduced a notion of "peaked point" for points that may be canonically lifted over extensions of the base field. (The definition is actually given in terms of norms and is quite close to the last condition of corollary 3.7.) We studied this notion further in [START_REF] Poineau | Les espaces de Berkovich sont angéliques[END_REF], under the name of "universal point", and proved, in particular, that any point over an algebraically closed valued field is universal (see corollaire 3.14). The interested reader will find properties of the map σ K as well as applications of the notion in those two references. Proof. When V is strictly semi-algebraic, the proof goes exactly like the proof of theorem 3.5, because corollary 3.7 enables us to use the same S d 's to define the point σ H (y) (x) in each fiber π -1 (y).

To handle the general case, we now use the same trick as in the proof of [START_REF] Ducros | Parties semi-algébriques d'une variété algébrique p-adique[END_REF], proposition 1.6. We may assume that V is defined by a formula obtained by conjonctions, disjonctions and negations of atomic formulas of the form ). This proves that V ′ is semi-algebraic.

  with the required properties and prove the second part of the statement. Since Q has degree at most d, we have |Q(x)| = |Q(η Q,r )| = r. Hence x belongs to {|Q| ≤ r} and x ≤ η Q,r = x d . Now let y = η R,s ∈ D d such that y ≥ x. We have s = |R(y)| ≥ |R(x)| = |R(x d )|, hence y ≥ x d and we are done. Let us now prove the existence of x d by induction on d. If d = 0, the result is obvious. Let d ≥ 0 be an integer and assume we found x d . If |P (x d )| = |P (x)| for any P ∈ k[T ] ≤d+1 , we put x d+1 = x d and we are done.

  The theorem enables us to define a map x ∈ A 1,an k → x d ∈ D d . It sends the point x to the closest point x d on the graph D d . Remark that, for any d

Corollary 2. 4 .

 4 Assume that k is maximally complete. Let K be a non-empty compact subset of A n,an k . Let d ∈ N n and R ⊂ R + be the image of k[T ] ≤d by the sup-norm . K . There exists a finite number of points η 1 , . . . , η r in D d,R such that ∀P ∈ k[T ] ≤d , P K = max 1≤i≤r (|P (η i )|).

For

  d ∈ N n , let S d (k) be the family of subsets of k n of the form 1≤i≤p {|P i | ≤ r i }, with P 1 , . . . , P p ∈ k[T ] ≤d and r 1 , . . . , r p ∈ R + .

  Theorem 3.5. Assume that k is maximally complete. Let n, m be integers. Let x be a point in A n,an k such that |H (x)| = |k| and V be a strictly semi-algebraic subset of A n+m,an k . Let π : A n+m,an k → A m,an k be the projection on the last m coordinates. Then the subset{y ∈ A m,an k (k) | x ∈ V ∩ π -1 (y)} is strictly semi-algebraic.Proof. Let us denote (T , T ′ ) with T of length n and T ′ of length m the variables on A n+m,an k . The formula defining V may be constructed using conjonctions, disjonctions and negations of atomic formulas of the form |Q(T , T ′ )| ≤ |R(T , T ′ )|. Let d be the maximum of the degrees in T of the polynomials appearing in the formula. By theorem 2.2, there exists polynomials P 1 , . . . , P t ∈ k[T ] and real numbers r 1 , . . . , r t ∈ |H (x)| = |k| such that, if we denoteS = 1≤i≤t {|P i (T )| ≤ r i }, we have ∀P ∈ k[T ] ≤d , P S = |P (x)|.Remark that we may assume that all the r i are 0 or 1. Let K/k be an extension of valued fields with K algebraically closed (and trivially valued in case k is) such that ∀P ∈ k[T ], ∃a ∈ K n , P S = |P (a)|. (One may for example choose an algebraic closure of H (x) and let a be the image of T by the evaluation morphism k[T ] → H (x) ֒→ K.) Let y ∈ k m . It is easy to check that we have |Q(x, y)| ≤ |R(x, y)| if, and only if, ∀α ∈ S(K), ∃β ∈ S(K), |Q(α, y)| ≤ |R(β, y)|.

  1≤i≤r ϕ i (u, w i ) holds in an elementary extension of k, hence in k and K. Since |H (x)| = |k|, for every d ∈ N n , the sentence ψ d (u) defined by ∀ polynomial P of degree d, ∃v, |P (u)| = |v|

Theorem 3. 9 .

 9 Assume that k is maximally complete, algebraically closed and non-trivially valued. Let n, m be integers. Let x be a point in A n,an k such that |H (x)| = |k| and V be a (resp. strictly) semi-algebraic subset of A n+m,an k . Let π : A n+m,an k → A m,an k be the projection on the last m coordinates. Then the subset {y ∈ A m,an k| σ H (y) (x) ∈ V ∩ π -1 (y)}is (resp. strictly) semi-algebraic.

  |P i (T , T ′ )| ≤ λ i |Q i (T , T ′ )| for i ∈ [[1, p]].Let us now consider the space A n+m+p,an k and denote S 1 , . . . , S p the p last variables. Define a stricly semi-algebraic subset W of A n+m+p,an k by replacing, for i ∈ [[1, p]], the i th atomic formula by|P i (T , T ′ )| ≤ |S i Q i (T , T ′ )|.Let us also denote π : A n+m+p,an k → A m+p,an k the projection on the last m + p coordinates. By the strictly algebraic case, the setW ′ = {z ∈ A m+p,an k | σ H (z) (x) ∈ W ∩ π -1 (z)} is strictly semi-algebraic. Let y ∈ A m,an k. Let y λ be the point of A m+p,an k associated to the semi-normP (T ′ , S) = u≥0 p j (T ′ )S u → max u≥0 (|p j (y)|λ u ).The subset W ∩π -1 (y λ ) is a semi-algebraic subset of A n,an H (y λ ) defined by a boolean combination of the formulas|P i (T , y)| ≤ λ i |Q i (T , y)| for i ∈ [[1, p]]. It contains the point σ H (y λ ) (x) exactly when the subset V ∩ π -1 (y) of A n,an H (y) contains the point σ H (y) (x). So the set V ′ of the statement is equal to {y ∈ A m,an k | y λ ∈ W ′ }. If |A(T ′ , S)| ≤ |B(T ′ , S)|, with A = u≥0 a(T ′ )S u and B = v≥0 b(T ′ )S v (each of the sum actually containing a finite number of non-zero terms), is one of the inequations defining W ′ , we see that |A(y λ )| ≤ |B(y λ )| if, and only if, max u≥0 (|a(y)|λ u ) ≤ max v≥0 (|b(y)|λ v

Acknowledgements

In 2010, I was given the opportunity to attend the summer conference of the MRC program on model theory of fields in Snowbird Resort, Utah. I would like to thank all the participants who explained the basics of model theory to me, with much patience and insight.

supported by the ANR project Berko.


Pascal Ginisty
email: pascal.ginisty@ifts-sls.com

Jeremy Olivier
email: jeremy.olivier@univ-pau.fr

Jean Vaxelaire
email: jean.vaxelaire@univ-pau.fr

Vincent Lafitte

CORRELATIONS BETWEEN FLOC CHARACTERISTICS AND DRAINABILITY PROPERTIES: HOW TO DEFINE A GOOD FLOCCULATION ?

Keywords: Flocculation& Mixing systems, sludge dewatering, thickeners, laboratory filters, pretreatment chemicals

Sludge conditioning is a pre-treatment to improve the removal of water during the thickening process with a wide range of commercially available products. Laboratory tests are usually needed to make the selection of a conditioner and its dosage, but mixing control is required during flocculation to obtain quantitative, repeatable and comparable data. A specific device (bootest) was developed to optimize sludge flocculation at lab scale and combines a sludge reactor for flocculation and a drainage cell. Experiments made with this device enabled to propose a "drainability index", a useful tool to qualify a "good flocculation" for a drainage process.

Introduction

It is usually recognized that sludge management is a major problem in water and wastewater treatment, as it can account for up to 50% of total operating costs. The effectiveness and cost of sludge treatment and disposal operations are strongly affected by its volume and, consequently, by its water content or solids concentration, so thickening and dewatering are important steps in the total sludge processing train and has serious impact on subsequent operations. Thickening devices enable to remove free water from sludge. Amongst devices, gravity belt thickeners are a relative, cheap, simple and efficient technology which enables to increase the sludge dry solids content from 1-3% to 6-10% [START_REF] Bogner | Mechanical sludge treatment and drying methods as process steps for sewage sludge disposal" Facing sludge diversities: Challenge, risks and opportunities[END_REF]. Sludge conditioning is a mean to improve the removal of water during the thickening process. Chemical products are classically used to neutralize or destabilize the chemical or physical forces acting on colloidal and particulate matters, suspended in the sludge, to form, under different mechanisms, larger aggregates called "flocs" [START_REF] Lottito | Models of sewage sludge conditioning[END_REF]. Chemical conditioning of sludges usually includes the use of organic polymers, commercially available with different ramification degree, average molecular weight and charge density [START_REF] Moody | Optimising usage of pre-treatment chemicals[END_REF]. The ability of sludge to thick depends not only on the type and dosage of polymers but also on the mixing conditions between sludge and chemicals [START_REF] Ginisty | Role of flocculent injection and mixing conditions in sludge flocculation[END_REF]. Laboratory tests are described in literature for selecting conditioner type and optimal dosage and for predicting machine performance. They consist in sludge flocculation in quantitative, repeatable and comparable conditions and in a filtration under gravity of conditioned sludge on the filter cloth of a belt thickener. Recent development enables to carry out these two operations in a single device called "bootest" [START_REF] Ginisty | New Laboratory Developments for sludge flocculation[END_REF]. The drainability of the flocculated sludge could be a parameter, easily and quickly obtainable. A recent published standard (EN 14701-4, 2010) showed specifically the repeatability and reproductibility of this characterization method. Results obtained with classical filtration cell may be used for scaling up belt thickeners [START_REF] Severin | Advances in predicting belt press performance from Lab data[END_REF] [START_REF] Severin | Model and analysis of belt drainage thickening[END_REF] and correlations were proposed to link (linearly) the final quantity of sludge with the solids content of the raw sludge by parameters depending on floc properties [START_REF] Olivier | Gravity drainage of activated sludge : from laboratory experiments to industrial process[END_REF] [START_REF] Olivier | Etudes des filtres à bandes pour la déshydratation mécanique des boues résiduaires urbaines[END_REF]. Few studies results have been published concerning the relationship between floc characteristics and their drainability. Large, loose or bulky flocs with great proportion of free filtrate are often required for thickening [START_REF] Spinosa | Effect of polyelectrolyte characterization on equipment Performance" Fundamental Aspects of sludge characterization and dewatering[END_REF]. They are generally obtained with structured high molecular weight emulsion polymers or high cross-linked polymers with a higher dosage [START_REF] Ginisty | New laboratory developments for belt thickener optimization[END_REF]. Nevertheless, the characterization of a good flocculation for a drainage process in an industrial equipment has never been well defined. As drainage tests are easy to carry out quickly at lab scale, we proposed in this paper to define a "drainability index" allowing to qualify a good separation in a belt thickener. The sludge drainability has to be linked to flocs characteristics which strongly depend on the operating conditions applied for their formation. The aim of this work is to correlate floc characteristics with their drainability.

Materials and methods

Sludge flocculation

Sludge flocculation experiments were carried out in a new kind of device called "bootest" developed by IFTS. It is composed of two sludge flocculators (diameter: 90 mm) and two drainage cells with automatic transfer from one to another (Figure 1). The two flocculators are stirred in the same conditions. Mixing time and impeller speed and position (depending on the volume of sludge) are measured and controlled. Drainage cells are equipped with filter cloth reference Si030904 from Rai-Tillières (French manufacturer). The mass of filtrate is recorded during the test by a weight sensor connected to a computer. The parameters for drainage kinetics are the ratio of the filtrate mass over the sludge initial mass (M/M 0 ) at different times as recommended in EN 14701-4. Preliminary work pointed out excellent repeatability of flocculation obtained with this equipment [START_REF] Ginisty | New Laboratory Developments for sludge flocculation[END_REF].

Flocculation kinetics control device

Optimum mixing time for sludge flocculation at a given speed (700 tr/min) was obtained with a torque rheometer (Thermo Scientific Haake Mars III) described as an efficient tool to control floc growth / breakage [START_REF] Ginisty | A review of laboratory devices to control sludge flocculation kinetics[END_REF]. The principle is illustrated on figure 2.

Polyelectrolytes

Cationic polymer of different charge density, molecular weight, physico-chemical form (powder, emulsion) and structure (linear chain, crosslinked backbone, structured) were supplied by French manufacturer SNF FLOERGER. Quantity of polyelectrolyte solution was fixed according to the required dose of polyelectrolyte by quantity of dry sludge (kg/T DS).

Results and discussion

Definition of a drainability index

A good drainage process requires three goals to be achieved:  A high solids content factor (increase of sludge dryness)  A fast kinetic of filtrate release  A high capture rate

Dryness characterization

Solids concentration factor can be assessed by the ratio of the thickened sludge dryness and the initial solids content of the sludge.

The thickened sludge dryness was measured according EN 14701-4 when the curve M / M 0 = f (t) reaches a horizontal asymptote.

Kinetics characterization

Drainage kinetics can be assessed by the measurement of the time required to recover 90% of the total mass of filtrate as illustrated figure 3. An adimensional number was defined by dividing this time by a sizing parameter of belt thickener which is equal to 60 seconds for classical industrial machines.

Characterization of capture rate

A good capture rate is characterized by a low concentration of suspended matters in the filtrate. Consequently, a filtrate quality parameter (P 3 ) was defined, as the ratio between the residual concentration of suspended matters in the filtrate and the initial solids content of the sludge.

Drainability index

A good drainage is simultaneously characterized by a high value of P 1 and low values of P 2 and P 3 . That is why the following equation has been considered to define the drainability index: Indexes α and β were defined by analyzing 92 experiments carried out on 5 different sludges (activated, digested, water supply treatment, drilling, mineral synthetic) flocculated by polymers of different nature and dosage. They were determined for P 2 α and P 3 -β contribution to be equivalent to P1 in most of analyzed cases. A good drainage requires a P 1 value between 3 (case of concentrated sludges) and 10 (case of diluted sludges). The analysis of drainage tests led to: α= 3, β = 0.25. Consequently, E g values ranged between 27 (case of P1 = P 2 -α = P 3 -β = 3) and 1000 (case of P1 = P 2 -α = P 3 -β = 10). In order to limit the variation range the expression of the drainability index was modified as follows:

ln ln 60

Definition of a good drainage

For a good drainage, following values of parameters are required: a) For P 1 , a value between 3 and 10 is usually required. Consequently, the parameter is rejected for P 1 < 3 b) For P 2 , the reference is 60 seconds for industrial equipment of big size. The parameter is rejected for t 90 > 60 s (or P 2 > 1). Consequently, the minimum value of P 2 -α is equal to 1. In the best drainage test, we observed a t 90 equal to 5 seconds and the corresponding value of P 2 -α was equal to 1730. c) For P 3 , the maximal value of SM r /Si 0 was fixed at 0.01 to obtain a correct ratio. The parameter is rejected for Si o /SM r < 100. Consequently, the minimum value of P 3 -β is equal to 3.2.

The compilation of all the data enable to specify the following limit cases: Limit case n°1: parameters are simultaneously equal to the minimum and maximum values which were previously specified :

P 1 = 3, P 2 = 1, P 3 = 0.01 → E g = 2.2
Limit case N°2: Owing to a bad flocculation, sludge flow through the filter cloth without solids retention : P 1 = 1 (no sludge concentration), P 2 = 0.017 (instantaneous flowing through the filter cloth : t 90 = 1s) , P 3 = 1 (no solids retention) → E g = 12.2

Analysis of data points out that a drainage is good when the three parameters are simultaneously accepted and are characterized by a drainability index between 6 and 10.5. Table 1 summarizes the different cases and corresponding drainability index values.

Influence of flocculation conditions on the drainability index

It is well known that flocculation conditions influences strongly the efficiency of a drainage process [START_REF] Ginisty | Role of flocculent injection and mixing conditions in sludge flocculation[END_REF] [5] [10] [START_REF] Ginisty | New laboratory developments for belt thickener optimization[END_REF]. Figure 5 gives an example for the influence of one of the flocculation parameters (P 2 ) and consequently on the drainability index. An increase of mixing time modifies particle size distribution and then alters the drainage kinetics. Nevertheless, an optimal mixing time for flocculation can be obtained regarding to the fact that a too long mixing leads to flocs shearing. The most significant parameters on drainability index were found to be (by decreasing order of importance): polymer structure, sludge mass by unit area and mixing time. In the ranges specified previously, sludge concentration, polymer charge density and polymer dosage have a minor influence. For polymer dosage, this result was unexpected. However, in another work, Olivier has already [START_REF] Olivier | Etudes des filtres à bandes pour la déshydratation mécanique des boues résiduaires urbaines[END_REF] observed that equivalent drainage kinetics can be obtained in wide range of polymer dosage.

Conclusion

This work proposes a new methodology to qualify drainage process and define a drainability index which includes the 3 most important aspects of drainage: concentration ratio, kinetics of water release and quality of filtrate. It highlights the importance of flocculation conditions on the value of drainability index and identifies the most significant parameters. Nevertheless, opposite effects of flocculation conditions on each parameter can be hidden in the drainaibility index and further work is needed to study separately their effect on each parameter and to broaden the range of their variation.

Acknowledgements

The authors gratefully acknowledge the financial support received for this research from the Agence Nationale de la Recherche (ANR-08-ECOT-018-004).

Nomenclature

E g : drainability index M: mass of filtrate after drainage (g) M o : mass of sludge before drainage (g) P 1 : concentration factor P 2 : kinetic parameter P 3 : filtrate quality parameter Si f : final solids content (after drainage process) (%) Si 0 : initial solids content (% or g/kg) SM r : residual concentration of suspended matters (g/kg) t: drainage time (s) t 90 : drainage time to eliminate 90% of the total volume of filtrate (s)

11th World Filtration Congress -Session L14 -Pretreatment

Figure 1 :

 1 Figure 1: Sludge flocculation device ("bootest")

Figure 2 :

 2 Figure 2: Principle of torque rheometer measurement

Figure 3 :

 3 Figure 3: Determination of t 90 with a classical drainage curve

  Congress -April 16-20, 2012 -Graz -Austria

Figure 4 :

 4 Figure 4: Drainage curves for different drainability index obtained in various flocculation conditions

Figure 5 : 2 

 52 Figure 5: Influence of mixing time during flocculation on t 90 Experiments were carried out on activated sludges by varying the flocculation operating conditions in the following ranges:  Mixing time : 15 to 35 s  Sludge concentration : 2 to 3.4%  Sludge mass by unit area of filter cloth : 1 to 2 kg/m 2  Polymer dosage : 5 to 10 kg/T DS  Polymer charge density : 40 to 80% of cationicity degree  Polymer structure : linear chain, crosslinked backbone or structured chain.The most significant parameters on drainability index were found to be (by decreasing order of importance): polymer structure, sludge mass by unit area and mixing time. In the ranges specified previously, sludge concentration, polymer charge density and polymer dosage have a minor influence. For polymer dosage, this result was unexpected. However, in another work, Olivier has already[START_REF] Olivier | Etudes des filtres à bandes pour la déshydratation mécanique des boues résiduaires urbaines[END_REF] observed that equivalent drainage kinetics can be obtained in wide range of polymer dosage.

Table 1 :

 1 Correspondence of values for drainability index

	Rejected drainage	E g < 2.2	Bad drainability kinetics
	Medium drainage	2.2 < E g < 6	1 or 2 parameters not accepted
	Good drainage	6 < E g < 10.5	All parameters values are accepted
	Limit drainage	10.5 < E g < 12.3	To be analyzed carefully according the case
	Rejected drainage	Eg > 12.3	No flocculation
	Figure 4 illustrates drainage curves corresponding to different values of the
	drainability index.

11th World Filtration Congress -Session L14 -Pretreatment

11th World Filtration Congress -April 16-20, 2012 -Graz -Austria


Pascal Ginisty
email: pascal.ginisty@ifts-sls.com

Jérémy Olivier

Jean Vaxelaire

S Fortuny

Leon

Influence of flocculation on sewage sludge thickening and dewatering

Keywords: sludge flocculation, bootest, drainability index, dryness limit, thickening, dewatering

come   L'archive ouverte pluridisciplinaire

INTRODUCTION

The effectiveness and cost of sludge treatment and disposal operations are strongly affected by its volume and, consequently, by its water content or solids concentration, so thickening and dewatering are important steps in the total sludge processing train and has serious impact on subsequent operations. Sludge conditioning is a means to improve the removal of water during the thickening and dewatering process. Chemical products are classically used to neutralize or destabilize the chemical or physical forces acting on colloidal and particulate matters, suspended in the sludge, to form larger aggregates called "flocs" with different mechanisms [START_REF] Lottito | Models of sewage sludge conditioning[END_REF]. Due to the complex nature of flocs, sludges display a wide variation of physical, chemical and biological properties. Many parameters such as particle size, surface properties, extracellular polymeric substances, cationic salts may influence significantly their thickenability and dewaterability [START_REF] Wilen | A comprehensive insight into floc characteristics and their impact on compressibility and settleability of activated sludges[END_REF] [START_REF] Mikkelsen | Physico-chemical characteristics of full scale sewage sludge with implication to dewatering[END_REF]. Due to the current problem of anticipating the behaviour of flocs, some laboratory tests were classically used to assess their thickenability and dewaterability such as gravity drainage methods, CST, measurement of the specific resistance and cake solids content in filtration compression cells or funnel-type vacuum units or more specific devices for belt presses [START_REF] Olivier | The prediction of filter belt press dewatering efficiency for activated sludge by experimentation on filtration compression cells[END_REF] or centrifuge [START_REF] Spinosa | Assessment of sludge centrifugability[END_REF]. Thickenability indexes were defined for sedimentation process [6] and a new index for gravity filtration was proposed in recent work to qualify sludge drainability [7]. Flocculation conditions are known to influence markedly sludge drainability and consequently but opposite effects of flocculation conditions on each parameters can be hidden in the drainaibility index. They have also an influence on sludge dewaterability and the optimum for thickenability or dewaterability is generally not the same [START_REF] Olivier | Study of belt presses for mechanical dewatering of sewage sludges[END_REF]. Dewaterability can be described by the concept of the dryness limit defined in the French Standard FD-T 97001 [9] which represents the maximal dryness obtained at an infinite time that could be achieved by filtration-compression test under pressure. Suppliers and users of dewatering equipments agree on the fact that this is fundamental data of sludge to give guarantees on the performances of their machines. Each supplier has its own correlation between the dryness limit and the dryness obtained on their equipment [START_REF] Gazbar | Assessment and improvement of performances of mechanical dewatering processes of sewage sludge[END_REF].This paper deals with the influence of flocculation conditions on sludge thickenability characterized by the drainability index and their subsequent dewaterability characterized by the dryness limit. The role of operating conditions in the determination of this parameter, in view of the revision of the corresponding standard, is also discussed.

MATERIALS AND METHODS

CONF12-010

Sludges

Experiments were carried out on different sludges :

• Diluted activated sludge (0.5% DS, 65% VM), sampled at a municipal wastewater treatment plant near Pau (64, France).

• Common activated sludge (1% DS, 67% VM), sampled at a municipal wastewater treatment plant at La Chatres (77, France).

• Concentrated activated sludge (3% DS, 61% VM), sampled at a municipal wastewater treatment plant near Agen (47, France).

• Water supply treatment sludge (2.5% DS, 26% VM) sampled at Nerac plant (47, France)

Polyelectrolytes

Cationic polymer of different charge density, molecular weight, physico-chemical form (powder, emulsion) and structure (linear chain, cross-linked backbone, structured) were supplied by manufacturers SNF FLOERGER and BASF. Quantity of polyelectrolyte solution was fixed according to the required dose of polyelectrolyte (actives matters) by quantity of dry sludge (kg/T DS).

Flocculation

Diluted activated sludges (like those coming from Pau plant) were flocculated in a conventional apparatus used in wastewater treatment called a "jar tester" composed of six position gang stirrer for agitating the biosolids wastewater in 1 L beakers at a controlled speed (and shear) while polymer flocculants or coagulants are added. The device and protocol can't be applied to other sludge conditioning owing to high solids concentration and higher viscosity of flocculated suspension and different kinetics. Sludge flocculation experiments were made with a new kind of device called "bootest" developed by IFTS and already described in previous work [START_REF] Ginisty | New Laboratory Developments for sludge flocculation[END_REF]. The two flocculators of 90 mm diameter are stirred in the same conditions with measurement and control of time and speed mixing, impeller position (function of the sludge volume) as specified in prEN 14742 [START_REF]Characterization of sludges -Laboratory chemical conditioning procedure (European standard under progress)[END_REF].

Sludge thickening

Drainage tests were made by pouring the flocculated sludge from the jastester to a gravity drainage cell or by transferring it automatically from the flocculator to the drainage part of the bootest. Drainage cells are equipped with filter cloth reference Si030904 from Rai-Tillières (French manufacturer). The mass of filtrate is recorded during the test by a weight sensor connected to a computer. The parameters for drainage kinetics are the ratio of the filtrate mass over the sludge initial mass at different times as recommended in EN 14701-4 [START_REF]Characterization of sludges -filtration properties -Part 4 : Determination of the drainability of flocculated sludge (european standard)[END_REF]. The time required to recover 90% of the total mass of filtrate, the final sludge dryness after thickening and the solids content in the filtrate were specially measured to calculate the drainability index developed in previous work [7] and expressed by the following equation :

Sludge dewatering

Dewatering tests are made in a filtration-compression stand equipped of 3 cylindrical stainless steel cells of 70 mm internal diameter . A perforated disk was located at the bottom of the cylinder to support a synthetic filtering medium (reference of 05-1010-SK-008 from Sefar Fyltis was used in this study). Pressure was applied by a piston moved hydraulically on flocculated thickened sludges by gravity filtration, linked to a displacement sensor to measure cake height. Mass of filtrate versus time was recorded during expression and reached an asymptote where no filtrate was released from the cake by mechanical compression. The corresponding dry solids content of the cake is called dryness limit which corresponds to the dryness of cake obtained in an infinite time as defined in FD-T 97001-1 [9]. For compressible sludges, it is difficult to obtain the asymptote in a reasonable test time and we propose to assess it by extrapolating cumulative curves of filtrate mass versus time according to the simple mathematic model :

The determination of the slope of the model linearized form enables to assess the dryness limit (S ∞ )

RESULTS AND DISCUSSION

Repeatibility

Repeatibility of the measurement of drainability index was evaluated for the concentrated activated sludges sampled near Agen flocculated by cross-linked polymer EM 440 BD with a dosage of 15 kg/T DS, a mixing time and speed of 10 s and 700 tr/min and a charge of sludge of 1.6 kg DS/m 2 . The test carried out 7 times enabled to assess a mean drainability index of 5.46±0.35 with characteristic time t 90 équal to 22±7s, sludge dryness equal to 7.20±0.08% and solids content equal to 0.328±0.038 g/L. The most important variation of the drainability index is linked to the kinetics parameters as it appears with an exponent -3 in the calculation formula. Another tests were carried out 5 times with the diluted activated sludge from Pau and flocculated in a jar-tester by a linear polymer EM 640L with a dosage of 6.2 kg/T DS, a mixing time and speed of 30 s and 300 tr/min and a charge of sludge of 0.45 kg DS/m 2 . The test carried out 5 times showed a mean drainability index of 3.87±0.75 with characteristic time t 90 équal to 44±9s, sludge dryness equal to 4.09±0.12% and solids content equal to 0.206±0.03 g/L. The deviation of the drainability index obtained with a transfer of the flocculated sludge from the flocculator to the drainage cell by an operator is higher than the index obtained by an automatic transfer carried out in the bootest as it was already shown in previous papers [START_REF] Ginisty | New Laboratory Developments for sludge flocculation[END_REF]. Repeatibility of the measurement of the dryness limit of the thickened sludge was only made with 2 tests in the same conditions (pressure : 4 bar, filtration time : 16 h, charge of sludge : 2.4 kg DS/m 2 ). Results showed a mean dryness limit of 30.5± 0.1%.

Influence of flocculation hydrodynamics conditions on drainability index

It is well known that flocculation conditions influences strongly the efficiency of a drainage process, particularly mixing time which is the parameter which is not fixed in the standard prEN 14742 since it depends on sludge and polymer characteristics. [START_REF]Characterization of sludges -Laboratory chemical conditioning procedure (European standard under progress)[END_REF]. Figures 1a-b Experiments carried out on diluted activated sludge show a plateau for the drainability index beyond 30 s mixing time, whereas a 10 s mixing time decreases significantly drainage kinetics, thickened sludge dryness and filtrate quality. The optimum mixing time for concentrated activated sludge is much lower, close to 10 s. Below this value, flocs are not completely formed and a 15 s mixing time, modifies particle size distribution and then alters the drainage kinetics and filtrate quality, leading to a decrease of drainability index from 5.5 to 3.8.

Influence of polymer dosing on drainability index

Polymer dosage is known to affect drainage kinetics [START_REF] Ginisty | New Laboratory Developments for sludge flocculation[END_REF] but equivalent drainage kinetics can be obtained in a wide range of polymer dosing [START_REF] Olivier | Study of belt presses for mechanical dewatering of sewage sludges[END_REF]. Figures 2a-b point out the influence of this parameter on drainability index for diluted and concentrated activated sludge. Experiments carried out on diluted activated sludge show an optimum range of EM 640 L between 6 and 13 kg/t DS. A polymer dosing below 6 kg/T DS affects kinetics parameter, sludge dryness and filtrate quality because flocs are too small whereas a polymer dosing higher than 13 kg/T DS affects only kinetics parameter owing to increase of filtrate viscosity. The same trend is observed with the concentrated activated sludge for which the optimum drainability index falls down from 5.5 to 4.4 at 10 and 20 kg/T DS. At 10 kg/T DS, flocs break down easily when falling on to the filter cloth whereas at 20 kg/T MS, viscosity is too high (the time of measurement of residual suspended matters was 4 times higher).

Influence of polymer nature on drainability index

The mechanism of polymer-induced flocculation depends upon the nature of interaction between polymer and sludge and polymer nature affects strongly floc formation, thickenability and mechanical resistance. Structured high molecular weight emulsion polymers are known to form large and bulky flocs, of high drainability but require higher dosage and mixing time at a given speed than linear polymers. Linear polymers lead to smaller flocs of lower filtration rate and increasing the cationicity has a detrimental effect on performances [START_REF] Ginisty | New laboratory developments for belt thickener optimization[END_REF]. Figure 3a-b point out the influence of polymer structure on diluted activated sludge drainability and the influence of polymer cationicity on concentrated activated sludge. Experiments carried out on diluted activated sludge point out the better drainability index obtained with structured (EM 640 TRM) and crosslinked polymer (EM 640 MBL) comparatively to linear polymers (EM 640 L). The drainability index variations are mainly linked to kinetics parameter rather than thickened sludge dryness and filtrate solids content. Large loose or bulky flocs with great proportion of free filtrate are often required for thickening. Cationicity have a lower influence if flocs are correctly formed, that is the case with high to medium charge density and medium to low molecular weight polyelectrolytes [START_REF] Spinosa | Effect of polyelectrolyte characterization on equipment Performance[END_REF]. A 20% cationicity polymer leads to a drainability index of 5.1 which is close to those obtained with 40 and 50% cationicity polymers (5.4 and 5.5). The predominant influence of polymer structure on drainability index comparatively to polymer cationicity was already shown in other work [7]. Nevertheless it is probably true only in a limited range of cationicity, depending on sludge.

Influence of sludge and corresponding flocculation conditions on dewaterability

Sludges of different origins were flocculated in the optimal way concerning their drainability. Table 1 summarizes their characteristics before dewatering. Dewaterability of these different sludges was assessed by the calculation of their dryness limit. As specified in FD-T 97001-1, the dryness limit was mainly dependent on 3 parameters : solids load, pressure and compression time. Preliminary experiments were carried out to highlight their influence on mineral (synthetic) and organic sludges (concentrated activated sludge) as illustrated in figures 4a-b, 5a-b and 6 ab. Results show opposite behaviour between mineral and activated sludge. Dryness limit of mineral sludges increases slightly from 66 to 69% with charge load in the range 4-25 kg DS/m 2 whereas it decreases from 20 to 14% in a lower range of charge load (2-9 kg DS/m 2 ) for organic sludges. The decrease of dryness of sewage sludges with solids load was observed in other work [START_REF] Olivier | Study of belt presses for mechanical dewatering of sewage sludges[END_REF]. Dryness limit of mineral sludges is independent from compression time in the range 2-16 h because the cake compression kinetics of flocculated thickened sludge is very fast. It is not the case of organic sludge where it takes 16 hours to have complete dewatering, owing to the slow and continuous deformation of the cake during expression [START_REF] Baudez | Rheology and physico-chemistry of sewage sludges for landfilling and spreading[END_REF]. Results show that sludges of highest drainability index don't give the better dewaterability characteristics since the mineral sludges, difficult to thicken by gravity filtration, have highest dryness limit.. Nevertheless, correlation is not only linked to the volatile matter contents. Except for water supply treatment sludges for which the dryness limit was obtained with a too low cake thickness, the dryness obtained on centrifuge correspond to 0.8-0.9 of the dryness limit when the operating conditions are optimized for a dewatering purpose (that was probably not the case for the plant where concentrated activated sludge was sampled).

CONCLUSIONS

For sludge thickening by gravity filtration, drainability index, including all the 3 most important parameters : concentration ratio (ability of sludge to be thickened), kinetics of water release and quality of filtrate (abililty of sludge to be flocculated) is a good tool for flocculation conditions choice, provided that the more adapted laboratory device is used for repeatable experiments as the bootest for concentrated sludges. A good drainability index is due in most cases to a fast kinetics of water release and is mainly modified by polymer nature (structure, cationicity), dosing and mixing time. The concept of "dryness limit" is a good parameter to assess sludge dewaterability and is most significantly modified (depending if sludge is mineral or organic) by solids load, expression pressure and time. A consensus will have to be found for choosing these parameters for the development of a future standard.

Results show that the sludge, which displays the best drainability index, may present a low dewaterability and further work is needed to define a "dewaterability index" which includes flocs mechanical resistance, not taken into account in the drainability index.

SYMBOLS

DS, DM : dry solids or dry matters E g : drainability index M : mass of filtrate after drainage (g) M o : mass of sludge before drainage (g) P 1 : concentration factor P 2 : kinetics parameters P 3 : filtrate quality parameter Si f : dryness of thickened sludge by drainage process (%)

CONF12-010

Si 0 : sludge concentration (% or g/kg) SM r : residual suspended matters (g/kg) S∞ : dryness limit t : compression time (s) t 90 : drainage time to eliminate 90% of the total volume of filtrate (s) VM : volatile matters α, β, a, b, c : constant parameters

Figure 1 :

 1 Figure 1 : Influence of mixing time on drainability index

Figure 2 :

 2 Figure 2 : Influence of polymer dosing on drainability index

Figure 3 :

 3 Figure 3 : Influence of polymer nature on drainability index

Figure 4 :

 4 Figure 4 : Influence of solid load on dryness limit (Pressure : 4 bar, compression time : 16 h and 4 h respectively for mineral and organic sludges )

Figure 5 :

 5 Figure 5 : Influence of pressure on dryness limit (Solids load : 16 and 5 kg DS/m 2 , compression time : 16 h and 4 h respectively for mineral and organic sludges )

Table 1 : Sludge characteristics before dewatering

 1

	Sludge	Activated (common)	Activated (concentrated)	Food industry	Water Supply	Digested	Mineral synthetic
	Polymer	Zetag 9048 FS	EM 540 BD	EM 640 TBD Zetag 8140 Zetag 8185 AN 926 SH
	Nature	cationic crosslinked	Cationic structured	Cationic structured	Cationic linear	Cationinc linear	Anionic linear
	Dosing (kg/T DS)	6.5	15	21	7	26	2
	Sludge dryness (%) after thickening	4.4	7.2	6.3	6.9	4.6	27.7
	Eg	4.3	5.5	2.2	0.3	-3	-1.8

Table 2

 2 summarizes the dryness limit of sludges of different origins in comparison to dryness obtained on industrial

Table 2 : Sludge characteristics after dewatering

 2

	Sludge		Activated (common)	Activated (concentrated)	Food industry	Water Supply	Digested	Mineral synthetic
	Charge load (kg DS/m	2 )	2	2	2	2	2	4
	Pressure (bar)		4	4	4	4	4	4
	Compression time (h)	16	16	16	16	16	16
	Cake thickness (mm)	10	8	8	2	13	3
	Dryness limit (%)		23.4	30.5	24.4	52	22.9	66.4
	Dryness on centrifuge (%)	21.5	18	19	23	21	No data
	Ratio		0.92	0.59	0.78	0.44	0.92	No data


Hugues Evrard

DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation

Formal methods can verify the correctness of a concurrent system by analyzing its model. However, if the actual implementation is written by hand, subtle and hard to detect bugs may be unintentionally introduced, thus ruining the verification effort. In this paper, we present DLC (Distributed LNT Compiler ), a tool that automatically generates distributed implementation of concurrent systems modeled in the LNT language, which can be formally verified using the CADP toolbox.

Introduction

When designing concurrent systems, the use of formal methods often consists in verifying a model of a system, and then writing the actual implementation by hand. The latter is tedious and error-prone, especially in the context of distributed systems, which are notoriously complex. The automatic generation of distributed implementations directly from formal models adresses both difficulties, by speeding-up the production of software, and by letting the programmer operate at the formal model level, with the benefits of formal verification tools. CADP (Construction and Analysis of Distributed Processes) [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] is a mature verification toolbox that can analyze concurrent systems modeled in the LNT [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.1)[END_REF] formal language. In this paper, we present DLC (Distributed LNT Compiler, http://hevrard.org/DLC), a tool which enables the automatic generation of distributed implementations from LNT models. DLC produces several executables that can be deployed on distinct machines. Moreover, DLC let the end user optionally define interactions between the implementation and its environment.

Formal Design with CADP and LNT

The CADP [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] toolbox gathers more than 25 years of research and development in formal methods and offers a comprehensive set of tools including a model checker and a test case generator, among others. The LNT formal language combines a syntax close to mainstream programming languages with powerful concurrency primitives inherited from process algebras. We briefly introduce LNT through a rock-paper-scissors example, illustrated in Fig. 1. For an exhaustive description of LNT including its formal operational semantics, see its manual [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.1)[END_REF].

The weapon type declares the three possible weapons, and requires the equality operator to be defined on its values. Many other types are available in LNT, including array and general first-order constructor types which enable the definition of records, lists, etc. The function wins over uses the case pattern matching statement to define the weapons's circular relation. Again, LNT provides many other statements, such as variable assignment, while and for loops, etc.

The PLAYER process defines a player behavior. Processes are a superset of functions, they additionally enable communication actions, non-determinism and parallel composition. The observable events of a process are actions on gates. An action contains zero or more data offers, whose types form a profile. A channel lists the profiles supported by a gate. Here, a player, identified by its self argument, performs actions on gates GAME and WINNER, which are restricted by channels game and nat, respectively. A player starts by assigning a random weapon to its mine variable. Then, the select nondeterministic choice statement introduces several possible behaviors, separated by "[]": a player is ready to perform either action on gate GAME-actions differ whether the player's weapon is first or second, identifiers are used for distinction. A player subsequently calls the wins over function: if it wins, it performs an action on gate WINNER before looping on a new game; if its opponent wins, then the player stops. Otherwise, it is a draw, and both players loop on a new game.

In LNT, processes interact by multiway rendezvous with value matching, reminiscent of process algebras: one, two or more (multiway) processes synchronize on an action, with the same profile. The value of data offers in received mode (prefixed by "?") of some process is set by other processes. For instance, players can exchange values of type nat and weapon by a rendezvous on gate GAME. The par statement in the MAIN process defines which rendezvous are allowed in a parallel composition of three players: an action on gate WINNER can be realized by any player independently, while an action on gate GAME must synchronize any pair among the player processes (m-among-n synchronization [START_REF] Garavel | A Graphical Parallel Composition Operator for Process Algebras[END_REF]).

DLC takes as input a parallel composition of LNT processes and generates a corresponding distributed implementation. Each process, also named task, is compiled to a distinct executable. Moreover, DLC produces one executable per gate to handle task interactions. Finally, the implementation also contains a starter executable that manages the deployment of other executables. For instance, when we apply DLC on our example, we obtain an executable per player, plus two executables for the gates, and the starter executable.

The starter deploys other executables according to a configuration file which associates executables to machine names. By default, DLC produces a configuration file which can be used as a template, where all executables are required to run on the local host. The configuration file adopts a classical UNIX configuration syntax, which makes it easy to be either written by hand or generated by scripts. For instance, here is a configuration file excerpt: edel-12.grid5000.fr # machine name directory = /tmp/task0_PLAYER0 # working directory on the remote node files = dlc_task0_PLAYER0 # name of the executable edel-36.grid5000.fr ... etc ...

Environment Interaction with Hook Functions

More often than not, the end user wants the generated implementation to interact with other existing systems in its environment, such as a local file system or some web service. DLC enables such interactions through hook functions: user-defined C functions that are called upon action events.

We want hook functions to enable not only the monitoring of actions, but also their control. Within the distributed implementation, tasks and gates use a protocol [START_REF] Evrard | Génération automatique d'implémentation distribuée à partir de modèles formels de processus concurrents asynchrones[END_REF] to handle synchronizations while preserving the mutual exclusion of conflicting (i.e., targeting the same tasks) rendezvous: when a gate detects a possible action, it starts a negotiation that either succeeds and enables the action realization, or fails. Therefore, we distinguish between pre-negotiation hooks that are triggered before a negotiation is started, and post-negotiation hooks that are called once the action is achieved. Moreover, each action is both a global event of the system and a local event for each task involved in it. Accordingly, we also distinguish between global hooks that are executed by gate processes, and local hooks that are executed by task processes. From these categories, DLC provides the three following types of hook functions.

pre-negotiation-global: each gate has a pre-negotiation-global hook that is called before a negotiation starts for an action on that gate. This hook returns a boolean to indicate whether a negotiation must be started for this action. post-negotiation-global: each gate has a post-negotiation-global hook that is called after a negotiation succeeds for an action on that gate. This hook returns a boolean to indicate whether the action must be realized. The action under consideration is passed as an argument to all the three types of hooks. Note that the pre-negotiation-global hook can decide whether a negotiation shall be started or not, but a positive response does not guarantee that the subsequent negotiation is successful. When the negotiation does succeed, it is up to the post-negotiation-global hook to eventually decide to realize the action (now that it is certain to be doable) or to abort the negotiation. All hooks can interact with the environment to make choices or perform side effects.

Hook functions are optional, as DLC can produce a stand-alone implementation without them. Hook functions for a gate g (resp. a task t) must be defined in the file named g.gatehook.c (resp. t.taskhook.c). DLC automatically detects such files and embeds the hook functions into the implementation. Besides, DLC has an option to generate hook function templates for a particular gate or task.

Figure 2 illustrates hook functions on the rock-paper-scissors example. The pre-negotiation-global hook of gate GAME let the user decide, at runtime, which games she allows. The post-negotiation-global hook of gate WINNER is used to play some particular sound depending on which player wins a game.

Overview of Compilation Internals

Figure 3 gives an overview of how DLC proceeds to generate a distributed implementation. DLC relies on the EXEC/CAESAR [START_REF] Garavel | System Design of a CC-NUMA Multiprocessor Architecture using Formal Specification, Model-Checking, Co-Simulation, and Test Generation[END_REF] tool of CADP to obtain a sequential implementation (in C) of each task process. However, the implementation produced by EXEC/CAESAR is not complete: it can list the currently possible actions of a process, but does not decide which action shall be realized. This decision is made by the synchronization protocol, and DLC automatically interfaces the code generated by EXEC/CAESAR with the protocol. Both task and gate protocol logic are implemented once for all in isolated libraries, which nonetheless require information about the specification, such as the interactions allowed on each gate with respect to the parallel composition. DLC extracts and gathers this information into the "specinfo" library, which is also used by the starter to know who is who. Moreover, DLC detects and embeds the optional hook functions. Finally, DLC invokes a C compiler to produce the executables.

Implementation Correctness. The sequential implementation of each task is obtained by the existing EXEC/CAESAR tool of CADP, which has already been employed in a formal context [START_REF] Garavel | System Design of a CC-NUMA Multiprocessor Architecture using Formal Specification, Model-Checking, Co-Simulation, and Test Generation[END_REF]. Interaction between tasks is achieved by a synchronization protocol [START_REF] Evrard | Automatic Distributed Code Generation from Formal Models of Asynchronous Concurrent Processes[END_REF] that we verified [START_REF] Evrard | Génération automatique d'implémentation distribuée à partir de modèles formels de processus concurrents asynchrones[END_REF] using a formal approach that detected possible deadlocks in other protocols of the literature [START_REF] Evrard | Formal Verification of Distributed Branching Multiway Synchronization Protocols[END_REF]. The actual implementation of the protocol logic is done by hand, but it is isolated in generic modules that can be thoroughly tested. The writing of these modules is a onetime effort, since they are reused in all generated implementations. Therefore, for a given LNT specification, the specific code produced by DLC comes down to the task-protocol interface which is glue code, and the "specinfo" library which only represents information in data structures. Finally, hook functions can avoid some valid actions to happen, but they cannot lead the system into an invalid action. All these considerations let us have a decent confidence in the correctness of implementations generated by DLC.

Current Restrictions. DLC presents two main restrictions. First, values exchanged during an action must fit into a 64bits integer, thus records, lists, and arrays must not appear in action data offers. To be removed, this restriction requires serialization primitives for any LNT types, and we look toward CADP tools to provide them. Second, an action can be guarded by a boolean function, i.e., the action is allowed only if its offers let the guard function evaluate to true. Since the code generated by EXEC/CAESAR does not give access to guard functions, DLC currently ignores the restrictions on data offers possibly induced by them. To be removed, this restriction requires to modify EXEC/CAESAR such that the generated code gives access to guard functions.

Conclusion

In this paper, we presented the DLC tool, which enables the automatic generation of a distributed implementation from the LNT formal model of a concurrent system. From an LNT parallel composition of processes, DLC produces several executables that can be easily deployed on distinct machines. We underline the fact that DLC does not require any special annotations in the LNT source. Process interactions by multiway rendezvous with data exchange are managed by a formally verified protocol [START_REF] Evrard | Génération automatique d'implémentation distribuée à partir de modèles formels de processus concurrents asynchrones[END_REF]. The end user can also set up interactions with the environment thanks to the hook functions.

We measured the performance of implementations generated by DLC on several examples [START_REF] Evrard | Automatic Distributed Code Generation from Formal Models of Asynchronous Concurrent Processes[END_REF][START_REF] Evrard | Génération automatique d'implémentation distribuée à partir de modèles formels de processus concurrents asynchrones[END_REF]. Our biggest case study so far is the Raft consensus algorithm: from an LNT specification of about 500 lines, DLC produces more than 9000 lines of C code for a Raft server. Across all examples, results illustrate that implementations generated by DLC can achieve more than 1000 rendezvous in sequence per second (and of course much more when rendezvous are realized concurrently on different gates). Hence, we consider implementations generated by DLC to qualify at least for rapid prototyping.

As regards related work, BIP [START_REF] Quilbeuf | Distributed Implementations of Component-based Systems with Prioritized Multiparty Interactions[END_REF] and Chor [START_REF] Carbone | Deadlock-Freedom-by-Design: Multiparty Asynchronous Global Programming[END_REF] come with deadlock analysis tools and a distributed compiler. Erlang programs can be verified with McErlang [START_REF] Castro | A Case Study on Verifying a Supervisor Component using McErlang[END_REF], and Dreams [START_REF] Proenca | Dreams: a Framework for Distributed Synchronous Coordination[END_REF] generates distributed implementations of Reo models.

Thanks to DLC, a concurrent system can now be modeled in LNT, formally verified with CADP, and automatically compiled to an efficient distributed implementation which is easily deployable and which can interact with its environment. In future work, we plan to get rid of the remaining restrictions of DLC, such that it can handle any LNT specification.

Acknowledgments: the author warmly thanks Frédéric Lang for reviews of this paper, and all other members of the CONVECS team for their support.

Fig. 1 .

 1 Fig. 1. A rock-paper-scissors game modeled in LNT.

Fig. 2 .

 2 Fig. 2. Hook functions enables interactions with the environment

Fig. 3 .

 3 Fig. 3. Overview of DLC architecture.