Adrien Boulanger

Selim Ghazouani

Guillaume Tahar

Guillaume Tahar Closed Geodesics

CLOSED GEODESICS IN DILATION SURFACES

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

We consider in this article the problem of the existence of regular closed geodesics in dilation surfaces. Our main theorem is the following.

Theorem 1. For any closed dilation surface Σ, there is a dense set of directions θ such that the directional foliation F θ has a periodic orbit. Equivalently, the set of directions covered by a cylinder is dense in the circle S 1 .

In particular, any dilation surface Σ carries at least one closed geodesic. This generalises to the context of dilation surfaces a celebrated theorem of Masur [Mas86] for translation surfaces.

As the two equivalent formulations of Theorem 1 suggest, it can be viewed from either a dynamical or geometric perspective. From the geometric point of view, it guarantees that every dilation surface contains the simplest building block that can be imagined, a cylinder, thus giving valuable insight into the geometric structure of the arbitrary dilation surface.

On the dynamical side, this theorem guarantees the ubiquity of periodic orbits in some particular (but very natural) one-parameter families of unidimensional of dynamical systems, in the form of the following corollary.

Corollary 2. For every affine interval exchange transformation T 0 : [0, 1] -→ [0, 1], the set of parameters t such that the map x → T 0 (x) + t mod 1 has a periodic orbit is dense in R.

Results about particular families of dynamical systems of this type are usually difficult to prove; a result analogous to Corollary 2 where T 0 is an arbitrary generalised interval exchange map seems out of reach of current methods.

1.1. Affine structures on surfaces. The question of the existence of closed geodesics can be considered in the wider context of affine (complex or real) structures on surfaces 1 . For Riemannian structures, the existence of closed 1 A real (resp. complex) affine structure on a surface is an atlas of charts taking values in R 2 (resp. C) such that transition maps lie in the group of real affine transformations 1 geodesics as been known for a long time (see for example [START_REF] Gromoll | Periodic geodesics on compact riemannian manifolds[END_REF] and references therein). The case of translation surfaces, which lie in the intersection of the affine and Riemannian world, is now very well understood. On the contrary, for general affine structures very little is known. We therefore pose the following problem.

Problem. Characterise the affine structures on closed surfaces which carry a regular closed geodesic.

Note that a complete solution to this problem is likely to be very difficult, as it contains as a particular case the notoriously hard question of determining whether the billiard flow of every polygonal table has a periodic orbit. We conclude this digression on affine structures with the following conjecture.

Conjecture. The set of real affine structures on a given closed surface Σ carrying a closed geodesic has full measure in the (finite dimensional) parameter space of real affine structures on Σ. This conjecture is supported by considerations on the dynamical nature of the geodesic foliations of generic affine structures, numerical simulations and the genus one case where many examples can be worked out explicitly.

1.2. Dilation surfaces vs general affine surfaces. Dilation surfaces are particular complex affine surfaces whose structural group is the set of transformations of the form z → a • z + b where a is a positive real number and b ∈ C. Whilst it is expected that the generic complex affine surfaces does not have any closed geodesic, the main theorem we prove in this article predicts that any dilation surface does.

We explain what the condition on the structural group defining dilation surfaces implies at the dynamical level. Every (complex or real) affine structure induces a "geodesic" foliation on T 1 Σ the unit tangent bundle of the surface and the existence of a closed regular geodesic is equivalent to the existence of a closed for this foliation. T 1 Σ is a 3-dimensional manifold thus the dynamical system induced by the foliation is essentially 2-dimensional. In the particular case of dilation surfaces, T 1 Σ decomposes into a 1-parameter family of invariant surfaces for the foliation. While this gives no indication as to which affine structures always have periodic orbits, it explains why dilation surfaces are essentially different from the general case:

• the problem for dilation surfaces is about finding periodic orbits in one-parameter families of unidimensional dynamical systems; • the problem for the generic affine surface is about finding a periodic orbit for a given 2-dimensional dynamical system. The analysis of 2-dimensional dynamical systems is far more intricate than that of their 1-dimensional counterparts; furthermore with dilation surfaces we have an entire 1-parameter family of one-dimensional dynamical systems (which are easier to analyse) to find a periodic orbit. This discussion also explains why, despite the fact that in principle it is plausible that a lot of real affine surfaces carry closed geodesics, the dilation case is of a different nature and probably easier to analyse. 1.3. Action of Sl 2 (R) and strategy of proof. We now explain the ideas behind the proof of Theorem 1. It is very much inspired by the translation case, and we remind the reader of the general structure of the proof in this case.

Both moduli spaces of dilation and translation surfaces carry an action of the group Sl 2 (R). This action is naturally defined by the post-composition of the charts defining the dilation/translation structure. It has the following important property : two surfaces are on the same Sl 2 (R)-orbit if and only if they define the same underlying real affine structure. In particular, if a surface has a closed geodesic, it is the case for every surface in its Sl 2 (R)-orbit.

In the translation case, the proof goes by induction on the combinatorial complexity 2 of the surface.

(1) It is easy to check that translation surfaces of lowest complexity, flat tori, always carry closed geodesics.

(2) Assume that we know that all surfaces of complexity lesser than k do carry closed geodesics and consider a translation surface Σ of complexity k. It is not hard to find a sequence (Σ n ) of surfaces in the Sl 2 (R)-orbit of Σ which diverges i.e. does not converge in the moduli space of surfaces of complexity n.

(3) Geometric tools building on the Riemannian structure of translation surfaces allow to show the following dichotomy : either (Σ n ) Gromov-Haussdorff converges (up to passing to a subsequence) towards a translation surface of lesser complexity or the Riemannian diameter of Σ n tends to infinity. (4) In the first case, since having a cylinder is a property that is open in parameter space and by the induction hypothesis, for n large enough Σ n has a closed geodesic. Since Σ n induces the same real affine structure as Σ, so does Σ. (5) An elegant lemma due to Masur and Smillie [MS91][Corollary 5.5] ensures that a translation surface of large diameter contains a long flat cylinder and thus contains a closed geodesic, which concludes the proof.

This strategy relies heavily on the Riemannian nature of translation surfaces to get a rather simple analysis of the ways a sequence of translation surfaces can degenerate; this part of the proof breaks down when trying to generalise it to the case of dilation surfaces. Most of the work done in the present article is to replace the last three points of the strategy outlined above by a suitable analysis of the different ways a sequence of dilation surfaces can degenerate, which we explain thereafter.

2 We define the complexity to be the number of triangles in a triangulation whose set of vertices is the set of singular points 1.4. Exotic dilation surfaces. In order to do so, we introduce a class of objects aimed at providing some sort of appropriate compactification of the moduli space of dilation surfaces having the following properties:

• they contain dilation surfaces as a subset;

• they carry directional foliations and it makes sense to talk about closed geodesics for these objects; • the property of having a closed geodesic is open in their parameter space; • the Sl 2 (R)-action extends to their parameter space in such a way that the property of having a closed geodesic is Sl 2 (R)-invariant; • the parameter space is sequentially compact;

• there is a notion of complexity for these objects that can be decreased by taking limits in the Sl 2 (R)-orbit of any such object; • finally, it is easy to prove that objects of lowest complexity have closed geodesics.

These properties are exactly what is needed to formally implement the inductive scheme of proof discussed in the previous paragraph for translation surfaces.

The construction of such objects, which we call exotic dilation surfaces, and the proof of the above properties occupies the bulk of the article.

• In Section 4, we give a formal definition of exotic dilation surfaces. Very roughly, these are objects obtained by gluing polygons together, but allowing for edges to be glued onto vertices and degenerate (1dimensional) polygons, in order to encode infinite changes of scale that can occur when a dilation surface degenerates (think of a hyperbolic cylinder whose multiplier tends to infinity for instance). • Extending the notions of directional foliations, closed geodesic, the Sl 2 (R)-action is completely straightforward from the definition of an exotic dilation surface and is also done in Section 4. • The first difficult point is to define what it means for a sequence of exotic dilation surfaces to converge; this is done in Section 5 using in a crucial way Delaunay polygonations of dilation surfaces that were first introduced in [Vee97] in the particular setting of complex affine structures.

• The second point is to show that with this unusual notion of convergence, the property of having a closed geodesic is open in parameter space; this is done in Section 6. It is probably fair to say that if a lot of what is done in this article is giving the good formal setting to be able to do proofs, the heart of the mathematical argument is contained in Section 6. • Finally, a minor difficulty is to show that some sequence of elements in the Sl 2 (R)-orbit of any exotic dilation surfaces actually degenerates, which is done in Proposition 12.

With all these elements in place, the reader should be convinced that an inductive scheme of proof as outlined earlier can easily be carried out to prove that every dilation surface carries a closed geodesic. In Section 7 we give a rigorous proof of the slightly more general statement that the set of directions corresponding to a closed geodesic is actually dense in the circle. The proof of this statement follows the same lines but is a little more technically involved.

1.5. An important shortcoming and an open problem. We prove that every dilation surface contains a closed geodesic but unfortunately we were not able to infer anything as to the nature of the cylinder carrying this closed geodesic. In particular, our proof does not preclude the existence of a strict dilation surface all of whose cylinders are flat (although the existence of such a surface seems highly unlikely).

Problem. Show that a dilation surface whose cylinders are all flat is a translation surface.

Acknowledgements.

Dilation surfaces

The symbol Σ will always stand for a compact surface of genus g ≥ 0 with a finite number of boundary components.

2.1. Generalities. The main objects we will deal with in this article are dilation structures, defined as follows.

Definition 1. A dilation structure on a topological surface Σ -possibly with boundary -is given by a finite set S ⊂ Σ, the singularities of Σ, and an atlas of charts A = (U i , ϕ i ) i∈I on Σ \ S such that

• the transition maps are locally restriction of elements of Aff

R * + (C) = {z → az + b | a ∈ R * + , b ∈ C};
• seen in any chart, any connected component of the boundary -if any -must be a straight line; • each singularity in the interior of Σ has a punctured neighbourhood which is affinely equivalent to a punctured neighbourhood of the cone point of a dilation cone; • each singularity on the boundary of Σ has a punctured neighbourhood which is affinely equivalent to a neighbourhood of the centre of a Euclidean angular sector of arbitrary angle.

A particularly simple way of constructing a dilation surface is to glue polygons in the plan by using dilations as illustrated in Figure 1. We will see that, from the perspective of the existence of cylinder, the study can be reduced to the case of dilation surfaces that can be described this way. Such a dilation surface is called polygonable.

Figure 1. The sides of the two polygons are glued according to the colours. Topologically, the resulting surface has genus 2 and has only one singularity which corresponds to the extremal points of these two polygons.

Note that the notion of straight line on the surface is well-defined since changes of coordinates are affine maps. Moreover, in any direction θ ∈ S 1 the foliation by straight lines of C in the direction defined by θ being invariant by dilation maps, it gives rise to a well-defined oriented foliation F θ on any dilation surface. Such a foliation is called a directional foliation. We call the directional foliations the resulting family of foliations, therefore indexed by the circle, that we denote (F θ ) θ∈S 1 . We shall call by extension a straight line any piece of leaves of one this foliations.

Definition 2. Let Σ be a dilation surface.

• A closed geodesic in Σ is a periodic leaf of a directional foliation.

• A saddle connection is a topological segment on the surface Σ \ S which is also a straight line (a piece of leaf of a directional foliation) and whose boundary consists of two singularities.

We conclude this subsection by the following definition which will use to measure the complexity of a dilation surface.

Definition 3. We define the complexity of a polygonable dilation surface as the number of triangles of any triangulation whose set of vertices is exactly the set of singularities of the dilation surface.

The above definition is consistent since this number of triangles does not depend on the choice of such a triangulation. A quick way of proving this fact in two use the well know fact that the Euler characteristic χ(Σ) of the surface Σ equals the number of triangles + number of singularities (which is fixed)number of edges. But the number of triangles is determined by the number of edges since any edge is exactly shared by two triangles and since all triangles have exactly three edges on their boundary. This shows that the number of singularities and the genus determine the number of triangles.

2.2. Cylinders. Cylinders are the geometric counterpart of the periodic orbits of the directional foliations as, in particular, each cylinder contains a periodic orbits. A flat cylinder is a dilation surface with boundary obtained by gluing a pair of the opposite sides of a parallelogram embedded in R 2 . A dilation cylinder is a dilation surface (with boundary) obtained by cutting be a sector of C of angle θ < 2π based at 0. The quotient of C θ by the dilation z → λz with λ > 1 real is called a dilation cylinder.

C θ Figure 2.
On the left a flat cylinder with a periodic leaf in dashed green (corresponding to the only direction in which there is a periodic leaf). On the right an affine cylinder with two periodic leaves of two different directional foliations (whose directions belong to the cone C θ ).

Modulus of a cylinder. In this paragrah we define a notion of modulus that extends the classical notion of modulus for flat cylinders/conformal annuli.

• Recall that the modulus of a flat cylinder obtained from a rectangle of base (z 1 , z 2 ) ∈ C 2 where the sides glued together are those corresponding to z 2 is by definition

| z 2 z 1 |.
The intuition at the level of the flat structure is that the longer and thinner a cylinder is, the bigger its modulus is. • For a dilation cylinder of angle θ and multiplier λ > 1, we define its modulus to be

2 tan θ 2 λ -1 .
This notion is devised to account for how "long and thin" a dilation cylinder is, in a way that a continuous deformation of cylinders from flat to strictly dilation makes the modulus continuous.

Non-polygonable surfaces. The following theorem ensures that dilation surfaces that do not carry cylinders of large angle are polygonable.

Theorem 3 (Veech). Any closed dilation surface which carries at least one singularity and which does not contain any cylinder of angle larger or equal than π is Delaunay polygonable.

This theorem is optimal since cylinders of angle greater than π are not polygonable as shown in Figure 3. See [START_REF] Duryev | Dilation surfaces and their Veech groups[END_REF] for a proof.

Action of SL(2, R)

. We now define a natural action of SL(2, R) on the space of dilation surfaces.

θ Figure 3.
In black, a fundamental domain for the action of z → 2z on a cone of angle θ > π. Any leaf entering the cylinder is trapped within it forever regardless of the direction of the leaf, as the one represented here in red. This property prevents a polygonation to 'connect' both sides of the cylinder.

Let Σ be a dilation surface and consider A ∈ SL(2, R). Let (U i , ϕ i ) i∈I a maximal atlas defining the dilation structure of Σ. Define A • Σ to be the dilation structure defined by the maximal atlas (U i , A • ϕ i ) i∈I where A acts on C via the standard identification C R 2 . This new atlas indeed defines a dilation structure as SL(2, R) centralises the group Aff R * + (C). If the dilation surface was given by gluing a bunch of polygons together, the new surface is also polygonable. Indeed, the image of the initial set of polygons with edges identifications is mapped by the linear action of the matrix A to another set of polygons. Since A is linear, the sides of the polygon that were parallel are still parallel after applying the matrix A so that one can still glue them using dilations of the plane: the resulting dilation surface is the image of Σ under the matrix A, see Figure 4 for an example with the matrix

A := 2 0 0 1/2 Figure 4.
On the right a dilation torus. On the left the image of the polygon defining it under the matrix A defined above.

Delaunay polygonations

3.1. Delaunay polygonation. The goal of this subsection is to define the Delaunay polygonation of a (polygonable) dilation surface. The construction we will give actually is Veech's proof of Theorem 3: to show that surfaces that do not carry cylinders of angle larger than π are polygonable, he showed that the following construction defines a polygonation. We refer to [START_REF] Duryev | Dilation surfaces and their Veech groups[END_REF] for the full proof. We will here only describe it.

The vertices of this polygonation are by definition the singularities of Σ. The edges of the polygonation are saddle connections: a given saddle connection between singularities s 1 and s 2 belong to the edges of the Delaunay triangulation if there is a closed disk in Σ such that s 1 and s 2 belongs to the boundary circle of this disk and such that there are no other singularities in it. A disk in Σ is said to be Delaunay if it does not contain any singularities in its interior but at least 3 on its boundary.

The faces correspond to what is left after suppressing the edges and the vertices: they are convex polygons whose extremal points belongs all to the same Delaunay disks. The Figure on the right illustrates the construction: the black disk is a Delaunay disk whose boundary contains the singularities s i1≤i≤4 corresponds to the singularities. In red the edges of the polygonation and in faded green one of its faces.

s 1 s 2 s 3 s 4 Figure 5
Note that the Delaunay polygonation gives you a way to recover from an 'abstract' polygonable dilation surface a concrete set of polygons that defines it.

3.2.

Polygons up to dilation and their limits. In this paragraph we consider the space of polygons with exactly p ≥ 3 vertices arising from Delaunay polygonation. We consider these polygons as marked and up to dilation, which means that • these polygons are exactly the polygons the vertices of which lie on the same circle; • we keep track of the role of each side which is what we mean by marked;

• a polygon an its image by a rotation are considered to be different (because polygons are considered up to dilation and not similarity). We denote the set described above by P p , which can be parametrised the following way. Consecutive (marked) sides are parametrised by complex numbers z 1 , • • • , z p which are subjected to the following condition

i z i = 0.
Two p-tuples parametrise the same element in P p if and only if they are scalar multiple of one another by a positive real constant. An abstract way to formulate this is that we obtain a natural parametrisation of P p by a subset of the sphere S 2p-1 .

A diverging sequence of polygons is said to converge to a degenerate polygon if it converges in S 2p-1 , in the aforementioned parametrisation. In the following definition we classify, in a way suitable to the analysis done in this paper, some of the possibilities for a sequence of polygons not to converge. Definition 4. (See Figures 6 and7) Let p be fixed. Consider a sequence of polygons (P k ) k∈N in P p . We say that this sequence is

• of convergent type if (P k ) k∈N converges in P p as defines above. Otherwise the polygon is said to degenerate, in which case we distinguish three different ways of doing so; a degenerating sequence of polygons is said to be • of Type 1 if all the vertices of (P k ) k∈N converge towards a given point of the circle containing all vertices of P k . • of Type 2 if the set of vertices of (P k ) k∈N converges towards a set of exactly 2 points of the circle containing all vertices of P k . • of Type 3 if (P k ) k∈N converges geometrically towards a polygon of strictly fewer vertices but at least 3.

long side long side long side

s ∞ s ∞ s ∞ Figure 6.
The three first polygons of a degenerating sequence of type 1 whose vertices all converge toward s ∞ . The terminology long side is explained below. long sides We now introduce the following terminology which will be useful when proving our main theorem.

s 1 ∞ s 2 ∞ s 1 ∞ s 2 ∞ s 1 ∞ s 2 ∞ long side long side long side
• If (P k ) k∈N is of type 1, the longest side of the polygon, corresponding to the closest one from the center of the circle in which it is inscribed, is called the long side while the other sides will be called short.

• If (P k ) k∈N is of type 2, the 2 longest sides, corresponding to the edges going from and out the 2 limits points, will be called the long sides while the others sides are called short.

3.3. Sequence of degenerating dilation surfaces. In this paragraph we consider sequences of dilation surfaces of fixed combinatorial type (that is, fixed genus, fixed number of singularities and prescribed angles at the singularities). We want to define what it means for a such a sequence to degenerate.

Usually, what one would do is to define a moduli space of dilation surfaces and say that a sequence degenerates if the sequence of points in moduli space it defines eventually leaves every compact set. Because we want to avoid these considerations, and also because we want to have a concrete way to tell that a sequence is degenerating, we do things differently here.

Let (Σ n ) n∈N be a sequence of dilation surfaces of same combinatorial type. Up to extracting a subsequence, we can assume that their Delaunay polygonations are all combinatorially equivalent. Precisely this means that for any n, m ∈ N their Delaunay polygonations have the same pattern: one can label for each n the set I of polygons, say as (P n (i)) I∈i , in a way that • the sequence (P n (i)) n∈N has always the same numbers of sides • one can mark the sides of the polygons in a way that the gluing pattern of the sides of the marked polygons (P n (i)) i∈N is constant with respect to the marking. In that case we say that the Σ n 's have constant Delaunay pattern. Definition 5. A sequence (Σ n ) n∈N of constant Delaunay pattern is said to degenerate if at least one of its Delaunay polygons degenerates in the sense of Definition 4.

We conclude this section with some remarks on local constraints being imposed to a degenerating Delaunay polygonations. We will denote by (Σ n ) a sequence of polygonable dilation surfaces of constant Delaunay pattern.

As illustrated in the following figure, one cannot glue the long side of a degenerating polygon of type 1 to the long side of a degenerating polygon of type 2 or of type 1. Another remark, that will be needed in Section 6, is that finitely many degenerating type 2 polygons glued along their long sides must be 'concavely shaped', see Figure 17, as shown in Figure 17.

Exotic dilation surfaces

This section is dedicated to giving a formal definition of exotic dilation surfaces, which are objects generalising dilations surfaces in a way to encode in some way their degenerations. 4.1. An informal account of what exotic dilation surfaces are. We consider a sequence of dilation surfaces (Σ n ) n∈N that is degenerating in the sense given by Definition 5. As in the previous Section, we denote by (P n (i)) i∈I the polygons of the Delaunay polygonation of Σ n . We want the limit Σ ∞ to Figure 9 be "what is left from the Delaunay triangulation" when passing to the limit. At an intuitive level, we will do the following operations (see Figure 10, Figure 11 and Figure 12).

(1) A sequence of Delaunay polygons (P n (i)) n∈N which converges to a polygon P ∞ is kept as it is: the limit will be given by the limit polygon (even if it does not carry has many edges than those of sequence). (2) Delaunay polygons which degenerate in a type 2 fashion are replaced with "two-sided" edges, with infinitely small sides represented by the end points of the edges (see Figure 7). These edges must be thought of as degenerated polygons of Type 2, as discussed in paragraph 3.2. (3) Delaunay polygons which degenerate in a type 1 fashion will eventually be removed, and neighbouring (possibly degenerate) polygons will be glued according to the pattern that these type 2 polygons suggest.

The three first drawings represent some terms of a degenerating dilation surface of genus 2 with one singularity whose 'connecting' flat cylinder degenerates as its modulus goes to infinity. At the level of the Delaunay polygonation, the two parts left after removing the connecting cylinder (the top polygon and the bottom one), converge as all the polygons converge up to dilation. The limit object we want to associate will be given by

• two edges glued along their long sides to form an "infinitely long" cylinder; • a flat torus, which is the "Delaunay limit" of the top part of the Figure ;  • a non flat torus with one boundary component, which is attached to the edge representing the infinitely long cylinder. This is just an informal account of what to expect from the formal construction that is to be explained in the next paragraph. Because in general degenerations (from the point of view of the Delaunay trianulation) can be fairly complicated, the formal construction is a bit involved; and it is good to keep in mind concrete examples as the one we have just explained.

4.2. Exotic dilation surfaces, formal definition. We define an exotic dilation surface to be a dilation surface (potentially with boundary, not necessarily connected) with boundary (which we call the the core dilation surface of the exotic dilation surfaces) and two extra building blocks defined as follows.

An edge is the datum of a (topological) segment with extremities p 1 and p 2 ; together with the datum of a direction θ(p 1 , p 2 ) ∈ S 1 (the direction from p 1 to p 2 , or simply from p 1 ) and a direction θ(p 2 , p 1 ) ∈ S 1 (the direction from p 2 to p 1 , or simply from p 2 ) such that θ(p 1 , p 2 ) = -θ(p 2 , p 1 ). An edge has two sides corresponding formally to the angular sectors [θ(p 1 , p 2 ), θ(p 1 , p 2 )+π] and [θ(p 2 , p 1 ), θ(p 2 , p 1 )+π]. The black edge and the red one of Figure 10 are edges.

(An edge is to be thought of as the limit of a degenerating sequence of polygons of Type 2. We will see in Section 5 that not all such sequences are kept in the limit, only "essential" ones.)

A hole is the datum (topological) segment together with the datum of a direction θ ∈ S 1 and the choice of a sector [θ, θ + π] or [θ -π, θ] which is called the entry of the hole (see Figure 11).

(A hole is to be thought of as the limit of a degenerating sequence of cylinders whose angle goes to π.)

Figure 11. The first three drawing represent some terms of a degenerating dilation surface of genus 2 with one singularity whose "connecting" cylinder degenerates as its angle goes to π.

At the level of the Delaunay polygonation, the two parts left after removing the connecting cylinder converge since all the polygons converge. The limit object we want to associate is a 2-components dilation surface with boundaries that are glued to a hole. Whenever a trajectory enters the hole it never comes out.

An exotic dilation surface (see the right part of Figure 10, 11 and 11) is the data of

• a dilation surface Σ (potentially with boudary, not necessarily connected); • finitely many edges which we call of type C, for example the black edge of Figure 10 is a type C edge (C stands for cylinder) ; • finitely many edges of type P (P stands for triangle); • finitely many holes, for example the black segment in the right part of Figure 11.

with finitely many incidence relations :

(1) sides of of edges of type P or segments of a boundary component of Σ can be attached to an extremity of an edge of any type; (2) a segment of a boundary component can also be attached to the entry side of a hole, or to a marked point of the dilation surface Σ. (3) a side of an edge of type P can also be attached to a point on Σ.

A point on the core dilation surface to which is attached either an edge of type P or a boundary component of the core dilation surface is called an entry point. Another important precision is the following: there is no limit on the number of sides of edges or boundary components that can be attached to either an entry side of hole, an extremity of an edge or an entry point.

Figure 12

These incidence relations are subject to the following directions compatibility restrictions.

(1) If an edge (of whichever type) is attached to a boundary segment of the core dilation surface Σ, the direction from the extremity of the edge that is attached to the boundary component must belong to the (closed) sector of outer directions of the segment (the sector of directions "coming out of the surface").

(2) If an edge (of whichever type) is attached to the side of an edge of type T , the direction from the attaching point must belong to the (closed) angular sector of the side to which it is attached. (3) If a side of an edge of type T or a boundary component of Σ is glued to a point p ∈ Σ and that the angle at p is larger than 2π, the exit angular sector at π must be specified.

Definition 6. An exotic dilation surface is said to be closed is every boundary segment of Σ, every side of an edge of type 1 and every entry side of each hole is attached to something.

4.3.

Directional pseudo-foliation. The interest in putting forward this notion of exotic dilation surface is that it is a good notion to study degeneration of dilation surfaces without loosing any relevant dynamical information. To this end, we extend the notion of directional foliations to exotic dilation surfaces. The main point to address is how to extend a straight line in a coherent way outside Σ. The rules are the following: if a straight line on Σ in a direction θ 0 hits a boundary component, we look at what it is glued to.

• If it is glued to nothing, the trajectory stops.

• If it is glued to a point p on Σ, we continue it from p in direction θ 0 .

• If it is glued to an edge of type C, the trajectory stops.

• If it is glued to a hole, the trajectory stops.

• If it is glued to an extremity of an edge of type T , and if the direction of the edge from the gluing extremity is different from θ 0 , the trajectory exits from the side the angular sector of which θ 0 belongs to. The trajectory is thus continued until it either stops, enters a hole or reenters Σ, from which point it is continued in the classical way.

Definition 7. A closed geodesic is a trajectory as above that is periodic.

We say that two closed geodesics have the same combinatorial structure if the sequence of consecutive edges crossed by each of them is the same (where edges are either edges of the exotic dilation structure or edges of the Delaunay polygonation of Σ).

Definition 8. A cylinder in an exotic dilation surface is either an equivalence class of closed geodesics which have same combinatorial structure, a hole or an edge of type C.

We extend the notion of modulus of cylinder defined in Section 2.2. The modulus of an edge of type C is infinite and the modulus of a cylinder containing a closed geodesic traversing at least one edge of type P is equal 0. We do not define a notion of modulus for holes.

4.4. The Sl 2 (R)-action. We just note here the following easy fact: the action of Sl 2 (R) on the space of dilation surfaces naturally extends to the set of exotic dilation surface. The image of a given exotic dilation surface by a matrix A is the exotic dilation surface • whose core dilation surface is the image of the initial one by A;

• with same edges and holes, same incidence relations;

• whose associated angular sectors are the images by the projective action of A of those of the initial exotic dilation surface. In particular the action is compatible with pseudo-foliations.

Delaunay limits of sequence of dilation surfaces

Having now defined exotic dilation surfaces, we need to define what it means for a sequence of (exotic) dilation surfaces (Σ n ) to converge to Σ ∞ , which is what we do in this Section. Note that we do NOT consider any moduli space of (exotic) dilation surfaces and put a topology on it. We only define a notion of convergent sequences that will be sufficient for our purpose. It is likely that this notion of convergence actually leads to a compactification of the space of dilation surfaces, but we do not pursue this line of research any further here.

Sequence of dilation surfaces.

As previously emphasised a sequence of bounded complexity of exotic dilation surfaces can be described by finitely many parameters: those encoding the finitely many sides of the edges/holes/polygons appearing in the Delaunay polygonation and a finite number of ways to glue these together. From every sequence of bounded complexity dilation surfaces, one can always extract a subsequence of constant pattern. With this in mind, we shall, through the following definition, refine a bit the usual topology one works with on the set of dilation surface of genus g and s singularities. Definition 9. A sequence of exotic dilation surfaces is said to be Delaunayconvergent if

• its exotic structure is combinatorially constant (i.e. each surface has the same number of building blocks and they are all glued together according to the same combinatorial pattern); • the core dilation surfaces of the sequence have constant Delaunay pattern and all of the associated sequences of polygons converge (to a possibly degenerate polygon, see Section 3.2); • the angular sectors associated to edges and holes converge. 5.2. Delaunay pre-limit. We have defined above what it means to converge, we now need to specify the limit. The first step, carried out in this paragraph, is simply to look at the degenerated polygons that are obtained by passing to the limit and build a hybrid object by keeping identification as they were. We will call this object the Delaunay pre-limit. In the next paragraph we will get rid of building blocks that are superfluous.

In the sequel, (T n ) n≥0 is a Delaunay-convergent sequence of exotic dilation surfaces whose associated dilation surfaces are denoted by (Σ n ) n≥0 . By definition of a Delaunay-convergent sequence, for all n ≥ 0,

• the Delaunay polygonation of (Σ n ) n≥0 are all topologically isomorphic, let m be the number of polygons of the Delaunay polygonation of any of the Σ n 's. • We denote by P n (i) for 1 ≤ i ≤ m the polygons of the Delaunay triangulation of Σ n in such a way that for a given i and different values of n the P n (i) are mapped to one another via the homeomorphisms realising the identifications between the Delaunay polygonations of the Σ n 's. By definition of a Delaunay-convergent sequence, the sequences (P n (i)) n≥0 converge in the space of degenerated polygons. • We define P ∞ (i)) to be the limit of (P n (i)) n≥0 if (P n (i)) n≥0 converges to a non-degenerate polygon, to be an edge if (P n (i)) n≥0 degenerates in a type 2 fashion; we do not define anything in the case where (P n (i)) n≥0 degenerates in a type 1 fashion (and we just keep the degenerate polygon that we obtain in the limit) 3 .

Edges which are limits of sequences (P n (i)) n≥0 come with two extremities and a direction from one extremity to another. We keep track of the information of which sides/extremities are glued to what. Thus, at this point, each side of an edge or polygon obtained this way is glued to either (1) a side of another polygon/edge/type 2 degenerated polygon;

(2) an extremity of an edge;

(3) a vertex of a polygon. This is the Delaunay pre-limit. Such a set of polygons/edges together with those identification does not define a exotic dilation surface yet, for the following reasons :

• some edges might be glued along one of their sides to a polygon;

3 An edge is also to be thought of a degenerate polygon, but since type 1 degenerated polygons will eventually be removed, we do not bother giving them a proper name.

Figure 13. The first three drawing represent some terms of a degenerating dilation surface of genus 2 with one singularity. At the level of the Delaunay polygonation, nothing happens on the bottom but one gets a tiny quadrilateral on the top as the relative size of the strip vanishes. This quadrilateron leads to an edge, in green, which we want to get rid of. At the limit, the two sides of the red edge are connected to the red points (formally the bottom surface at the limit has two boundary components).

• there might be collections of edges glued together along their sides;

• some edges do not have a specified type C or T yet;

• we must get rid of Type 2 degenerated polygons as they do not feature the definition of a exotic dilation surface.

The next subsection aims at deleting all unnecessary edges/identifications in order to make the previously defined Delaunay pre-limit an actual exotic dilation surface.

5.3. From Delaunay pre-limit to exotic dilation surface. To clarify the structure, we shall explain all the steps one has to follow in order. These steps, taken altogether, may have to be repeated finitely many times.

Step 1 : Deleting unnecessary edges. We consider all edges one of whose (long) sides is glued to a polygon of the form P ∞ (i). Let e be such an edge. We do the following :

• We delete e.

• Whatever was glued to to the other side of the edge is glued to the side of P ∞ (i) to which e was initially glued to. • Whatever was glued to the extremity of e is glued on to the corresponding vertex of P ∞ (i).

Deleting this unnecessary edges is illustrated for example in Figures 13. We then repeat Step 1 until they is no edge glued along one of its sides to a polygon of the form P ∞ (i).

Figure 14

Step 2 : Grouping together degenerate polygons of Type 2. We simplify the picture further by considering maximal sequences of Type 2 degenerate polygons glued to one another via gluings always involving a long and a short side.

We replace these "trees" of Type 2 polygons by a single Type 2 degenerate polygon. The upshot of this operation is that after this step, the long side of Type 2 degenerate polygon is always glued to either an extremity of an edge or a non-degenerate polygon (it cannot be glued to a side of an edge by virtue of coming from a Delaunay triangulation).

Step 3 : Deleting Type 2s, the hole case. For this step, we consider all Type 2 degenerate polygons whose big side is glued to one of its short sides.

We replace these with a hole, and whatever was glued to the other short sides is glued to the entry of the hole, to the exception of extremity of edges which we do not glue back. See Figure 11.

Step 4 : Deleting Type 2s, the non-degenerate case. We now turn to Type 2, degenerate polygons one of whose long side is glued to a nondegenerate polygon P ∞ (i). Consider such a Type 2 polygon Q. Here we do the following (see Figure 15)

(1) We subdivide the side s of P ∞ (i) which is glued to the long side of Q according to the where are the extremities of the short sides of Q. (2) We subdivide P ∞ (i) into finitely many polygons in such a way that subdivisions of s created become sides of polygons of this subdivision. (3) We glue whatever was glued to the short sides of Q to the sides of the newly created polygons corresponding to the subdivision of e induced by Q.

Step 5 : Deleting Type 2s, the edge case. Finally, we consider the case of Type 2, degenerate polygons whose long side is glued to the extremity of an edge. Again, let Q be such a degenerate polygon and let e be the edge to which its long side is glued. We delete Q, and glue back whatever was glued to small sides of Q to the extremity of e unless it was an edge glued to a small side via its extremity.

Figure 15

Step 6 : Deleting Type 2s, final touch. We then repeat Step 3, 4 and 5 until there are no Type 2 degenerate polygons left (as it might the case that in the process described by Step 4 and Step 5, we will have created cases that should have been dealt with by Step 3, for instance). Since they are but finitely many such degenerate polygons, the process terminates.

Step 7 : Deleting connections between edges. If two edges are glued along their extremities, we disconnect them.

Step 8 : Grouping edges together. Finally, we consider maximal collections of edges consecutively glued together along their long sides. For such a collection

(1) If it loops, we replace it with an edge of type C.

(2) If it does not loop, we replace it with an edge of type T .

At any rate, we deal with identifications on the extremities of the original collection of edges the following way. We distinguish extremities depending on which "end" of the collection of edges they were, and whatever was glued to an extremity of an edge in the initial collection is glue to extremity of the new edge that is on the corresponding extremity (see Figure 10).

The object thus obtained, after performing those eight steps, is an exotic dilation surface; it is by definition the Delaunay limit of the sequence (Σ n ) n∈N .

5.4. Some properties of Delaunay limits. We collect here a pair of obvious but important lemmata that we will be implicitly be using henceforth.

Lemma 4. Let (Σ n ) n∈N be a Delaunay convergent sequence of exotic dilation surfaces. Then its Delaunay limit Σ ∞ is not empty.

Proof. If at least one of the polygons of the Delaunay polygonation of the core dilation surface does not degenerate, then the limit is obviously non-empty. Assume that all these polygons degenerate. Then all degenerated polygons of the Delaunay pre-limit are Type 1 or 2.

• If they are all of Type 1, one can build a chain of consecutive Type 1 polygons, the long side of one always being glued the small side of the next. Such a chain loops, giving rise to a hole. In that case, the limit is non-empty. • Finally, if there is a least one Type 2, there will be at least an edge in the limit, as the only way one can suppress a Type 2 polygon is if one of its long side is glued to a non-degenerate polygon in the pre-limit.

The following lemma is obvious from the construction.

Lemma 5. Let (Σ n ) n∈N be a Delaunay convergent sequence of closed exotic dilation surfaces. Then its Delaunay limit Σ ∞ is closed.

Finally, we have the almost tautological Lemma 6. Let (Σ n ) n∈N be a sequence of exotic dilation surfaces of bounded complexity. Then it has a subsequence which Delaunay converges.

Remark. We have only defined the notion of convergent sequence and not a topology on the space of exotic dilation surfaces. It seems reasonable to expect that there exists a topology whose convergent sequences are Delaunay convergent sequence, but our approach does not yield the construction of such a topology.

Remark. The use of the Delaunay polygonation is probably an artefact for this construction, which might be possible to do in more abstract and intrinsic terms. It would be interesting (and conceptually more satisfactory) to have a definition of Delaunay limits which spares the use of Delaunay polygonations.

Stability of cylinders

This section is dedicated to proving the following Proposition, which can be thought of as the heart of the proof of Theorem 1.

Proposition 7. Let (Σ n ) n∈N be a sequence of closed exotic dilation surfaces Delaunay-converging to a surface Σ ∞ . Assume Σ ∞ carries a cylinder, which covers the direction θ 0 . Then for any , there exists n 0 > 0 such that for all n ∈ N, n ≥ n 0 , Σ n carries a cylinder which covers a direction that is -close to θ 0 . In addition to that, if the cylinder in Σ ∞ is an edge of type C, the modulus of the cylinder in Σ n can be made arbitrarily large for n 0 sufficiently large.

In the proof of Proposition 7, we distinguish upon four cases depending whether the cylinder of Σ ∞ is (1) a hole;

(2) included within the core dilation surface of Σ ∞ ;

(3) an edge of type C;

(4) contains an edge of type T or goes through a boundary component of the core dilation surface of Σ ∞ which is glued to a point. We refer to this latter case as the "infinite dilation ratio" case. The first three cases are pretty much straightforward, only the last one requires a careful analysis (and accounts for the main difficulty that degenerations of dilations surfaces present when compared to translation surfaces).

6.1. The cylinder of Σ ∞ is a hole. If this hole was already a hole in Σ n , there is nothing to prove. Otherwise the hole was formed in the limit, which means that Σ n contained a sequence of Type 1 polygons such that two consecutive polygons in that sequence were glued, the long side of first polygon being glued to a short side of the second. Such a sequence being cyclic, a short side s of the last polygon is glued back to the long side l of the first one. Consider the strip issued from s in the direction orthogonal to that of s and l, for n sufficiently large this strip is well-defined until it hits l (see Figure 16 below) and is thus glued back within itself, which defines a cylinder.

Figure 16

6.2. The cylinder of Σ ∞ is an edge of type C. The argument here follows similar lines as the previous case. Again, if the edge of type C was already an edge of type C in Σ n , then there is nothing to prove. Otherwise, this edge of type C came from a sequence of polygons of type 1 consecutively glued along their long sides. It is easily seen that for n sufficiently large, the segment joining the middle points of two extremal long sides (that are then glued to one another) is contained within the union of all polygons and that it defines in Σ n a closed geodesics which in turn gives rise to a cylinder of very large modulus.

6.3. The cylinder of Σ ∞ is contained within its core dilation surface. There always is a sequence of subsurfaces of (Σ n ) n∈N converging geometrically to the core dilation surface of Σ ∞ . The existence of a cylinder follows from the fact that the property of having a cylinder is open in the parameter space of (standard) dilation surfaces. 6.4. The cylinder of Σ ∞ has infinite dilation ratio. We are now treating the last and main case. Let γ be the closed geodesic of Σ ∞ . Recall that it consists of a sequence of adjacent edges of type T and bits of geodesics going from an entry point of the core dilation surface to a boundary component (itself is glued to either a entry point or an edge of type T ).

Lift of γ in the core dilation surface. Consider a part of the closed geodesic γ in Σ ∞ that is contained in the core dilation surface : this part goes from an entry point p to a boundary component ∂. In Σ n , the entry point of Σ ∞ correspond to either a small side s of a Type 1 triangle or it was already an entry point. For n sufficiently large, all lines issued from s in the direction of the geodesic of Σ ∞ cross the same sides of the Delaunay polygonation of Σ n before intersecting the edge of the traingulation corresponding to the boundary component ∂ of Σ ∞ (see Figure 18. Thus, we obtain for any component of γ travelling from an entry point of Σ ∞ a "lift" to Σ n for n sufficiently large. Such a lift is a strip issued from the edge of the Delaunay triangulation that had been contracted to an entry point in Σ ∞ in the process of constructing Σ ∞ (this strip being reduced to a line segment if the entry point p was already an entry point in Σ n ).

Lift of γ to the whole surface. We are now ready to lift the whole geodesic to Σ n . By hypothesis, γ goes across edges of type T . Such an edge e was in Σ n a collection of adjacent triangles of Type 1 glued along long sides. γ had to enter e via either another edge of type T or a boundary component of the core dilation surface. At any rate, this transition corresponds in Σ n to entering through the short side of one the adjacent triangles of Type 1. Let s 0 be this side.

Recall that we have the following: given two adjacent type 2 polygons P 1 and P 2 whose short sides are on the same side, then the polygon formed by the union of P 1 and P 2 has to be concave, see Figure 17. In particular, this implies that for n sufficiently large, all line segments issued from s 0 ∈ Σ in the direction of γ only cross long sides of the finitely many polygons of Type 2 that are glued along. By definition, θ the direction of γ is not the limiting direction of the long side. Thus if n is sufficiently large, any line segment issued from a short side in the direction of γ is going to exit the collection of triangles of type 1 via the long side of one of the extremal triangles, which we call l.

Figure 17

We can thus consider the strip issued from s 0 of line segment in direction θ which goes straight from s 0 to the boundary of the union of type 1 triangles. Furthermore, when n tends to infinity, the ratio between the intersection of this strip with the extremal long side l can be made arbitrarily small. This strip issued from s 0 either enters a new collection of triangles of type 1 corresponding to another edge of type T in Σ ∞ , for which l is now a short side, and the argument above can be repeated. Otherwise, it enters the core dilation surface via a side s which is the base of a lift of a part of γ in the core dilation surface, defined in paragraph 6.4. The strip issued at s 0 is from that point onwards contained within that lift until it hits the side of the triangulation corresponding to a boundary component of the core dilation surface of Σ ∞ , see Figure 18. This side must be glued to either

• a short side in a collection of type 1 triangles corresponding to an edge of type T in the limit; • an edge of type T .

Figure 18

At any rate the argument can be carried over until the strip issued at s 0 gets back to s 0 . We have therefore managed to embed a strip in such a way that one extremity is glued to back to a segment in the interior of the other extremity (and the ratio between the extremity and the part to which the other extremity is glued can be made arbitrary small provided n is taken sufficiently large). This implies the existence of a cylinder of very large dilation ratio (which would be infinite if the lift of γ in Σ n contains an edge of type T ).

Proof of Theorem 1

In this Section we give a proof of Theorem 1, whose statement we recall for the convenience of the reader Theorem 8. For any closed dilation surface Σ, there is a dense set of directions θ such that the directional foliation F θ has a periodic orbit. Equivalently, the set of directions covered by a cylinder is dense in the circle S 1 . 7.1. Reduction to Proposition 10. We first reduce the proof of Theorem 8 to a statement about exotic dilation surfaces. We assume by contradiction the existence of a dilation surface Σ 0 such that Σ 0 does not have any cylinder covering a direction in an angular sector (θ 1 , θ 2 ) (thought as a subset of RP 1 and not of S 1 ).

• Up to replacing Σ 0 by an element of its SL(2, R)-orbit we can assume that (θ 1 , θ 2 ) contains [0, π 2 ]. • We consider the sequence defined by

Σ n = e n 0 0 e -n • Σ 0 .
Up to passing to a subsequence, we can assume that (Σ n ) n∈N Delaunay converges to an exotic dilation surface Σ ∞ .

• Since the matrix e n 0 0 e -n maps (θ 1 , θ 2 ) onto an angular sector (θ 1 (n), θ 2 (n)) with θ 1 (n) → 0 and θ 2 (n) → π, by virtue of Proposition 7, any cylinder of Σ ∞ is in the horizontal direction (and therefore is either a flat cylinder of an edge of type C). We now want to control the moduli of cylinders of Σ ∞ . We have the following Proposition, whose proof we postpone to paragraph 7.4. Proposition 9. Let Σ be a dilation surface. There exists a constant M = M (Σ) such that any cylinder in Σ has modulus less than Σ.

In particular the modulus of any dilation cylinder of Σ 0 is uniformly bounded by a constant M 0 . Consider such a cylinder C 0 , let θ 0 be its angle and λ 0 > 1 its multiplier. Recall that its modulus is 2 tan θ 0 2 λ-1 . We make the following remark. The image of any angular sector (α 1 , α 2 ) contained in the complement of (θ 1 , θ 2 ) by a matrix of the form e n 0 0 e -n is never more than C|α 2α 1 for a constant C depending only on (θ 1 , θ 2 ). Thus the modulus of any hyperbolic cylinder in Σ n is never more than that of its pre-image in Σ 0 , up to multiplication by a constant depending only on θ 1 and θ 2 . A similar but simpler argument guarantees that the images of flat cylinders in Σ n have modulus uniformly bounded, independently on n. We thus get that cylinders in Σ ∞ have uniformly bounded moduli.

Assuming the existence of a counterexample to Theorem 8, we have constructed a closed exotic dilation surface having the following property : all its cylinders are flat, horizontal with finite modulus. Theorem 8 is thus a consequence of the following Proposition.

Proposition 10. There is no closed exotic dilation surface all of whose cylinders are horizontal and have bounded modulus. 7.2. Proof of Proposition 10. The proof goes by induction on the complexity of the exotic dilation surface. We first prove the following claim to initialise the induction.

Lemma 11 (Initialisation of the induction). A closed exotic dilation surface of complexity 0 which does not contain an edge of type C has a closed geodesic in any direction that is not a direction of an edge or a boundary direction of an angular sector associated to a hole.

Proof. Consider any trajectory in a direction θ satisfying the hypothesis of the lemma. In a complexity 0 exotic dilation surface, a trajectory is just a sequences of edges. In the case where we exclude type C edges, such a trajectory either finishes in a hole or is eventually periodic. At any rate there is a closed geodesic in direction θ.

We can now carry out the induction. Assume that there is no closed exotic dilation surface of complexity less or equal to n satisfying the hypothesis of Proposition 10. Now assume that there is one of complexity n + 1 that does, call it Σ. The core dilation surface of Σ is nonempty, thus Σ has saddle connections in at least two different directions (since it is polygonable). One can then assume that Σ ∞ carries a non-vertical saddle connection, say in a direction d. Being given two directions d 1 and d 2 , we denote by (g d 1 ,d 2 t ) t∈R the Teichmüller flow (i.e. the flow generated by the associated one-parameter subgroup of SL(2, R)) which contracts the direction d 1 and dilates the direction d 2 . The key tool we use to handle this case is contained in the statement of the following Proposition, whose proof we postpone to the next paragraph.

Proposition 12. Let Σ be a dilation surface with boundary and γ a saddle connection in direction d. For any θ ∈]0, π[, if the closure of the orbit in positive time of Σ under g d,d+θ contains a dilation surface of same complexity as the one of Σ then γ must be on the boundary of a hyperbolic cylinder of angle θ.

By Lemma 6 the orbit of Σ under g d has an accumulation point Σ ∞ . The action of the flow decreases the moduli of every vertical cylinder of Σ so that Σ ∞ also satisfies to the assumption of Proposition 10. Then, Proposition 14 implies that Σ ∞ has strictly smaller complexity than Σ since we assumed that the only cylinders that carries Σ ∞ are vertical, which contradicts the induction hypothesis. 7.3. Proof of Proposition 12 (lowering the complexity). This subsection is devoted to the proof of Proposition 12. We simplify a bit the statement of Proposition 12 by making the two following remarks

• one can only take into account the dilation part of the exotic dilation surface, a dilation surface with boundary, since the complexity is defined through it; • once can conjugate everything by an element of SL 2 (R) mapping the direction d to the vertical one and d + θ to the horizontal;

Proposition 12 is then equivalent to Proposition 13. Let Σ 0 a dilation surface with boundaries that carries a horizontal saddle connection and whose orbit under the Teichmüller flow contains a dilation surface with same complexity, then the saddle connection must be the boundary of at least one periodic hyperbolic cylinder of angle π/2.

Proof. By assumption, there is a dilation surface Σ ∞ with the same complexity as Σ 0 together with a sequence of times

t n -→ n→∞ ∞ such that Σ n := g tn (Σ 0 ) -→ n→∞ Σ ∞ .
Note that the property 'carrying a horizontal saddle connection' is a closed property as well as invariant under the action of the Teichmüller flow. In particular, the images of the saddle connection γ must not to collapse for otherwise we will have collided 2 singularities which would have lowered the complexity of Σ ∞ , contradicting the main assumption of Proposition 12.

Therefore, one knows a priori that Σ ∞ has a horizontal saddle connection γ ∞ . We will no longer use the assumption on the complexity of Σ ∞ . The key point of the proof is the Lemma 14. With the notation introduced in Theorem 13 and the paragraph above. The saddle connection γ ∞ of Σ ∞ is the boundary of a periodic hyperbolic cylinder of angle π/2.

Let us postpone the proof of the above key lemma to see first how to use it in order to get the conclusions of Theorem 13. Since the property 'carrying a hyperbolic cylinder (not necessary of angle π/2) whose boundary is a given horizontal saddle connection' is open and invariant under the Teichmüller flow, one knows that Σ 0 also carries a hyperbolic cylinder whose boundary is a horizontal saddle connection. Such a cylinder must be periodic (of angle π/2) since any other angle would lead to a divergent orbit under the Teichmüller flow, contradicting the assumption of Theorem 13.

Proof of Proposition 14. In order to show that Proposition 14 holds, we shall use the developing map associated to the middle point M γ∞ of the saddle connection γ ∞ . We denote by s 1 ∞ and s 2 ∞ the 2 singularities on the boundary of γ ∞ . We start by choosing a 'side' of γ ∞ ; if γ ∞ is on the boundary of Σ ∞ , we choose the 'side' of it toward the interior of the dilation surface and if γ ∞ is not then we choose whichever side (the other choice of side will give us another cylinder in this case). Let us define the 'closest' singularity s min ∞ to γ ∞ (with respect to the choice made on the developing map) on the left of γ as the first singularity encountered when developing disks from M γ∞ in the (closed) half plane whose boundary is γ ∞ which is not either s 1 ∞ or s 2 ∞ , as illustrated on the right.

s 2 ∞ s 1 ∞ M γ∞ s min ∞ γ ∞
The key point is to show that s min ∞ is aligned with γ ∞ . In order to show it, we argue by contradiction (we could have argued by considering the contrapositive of the statement but we decided not to for the sake of clarity). Assume that s min ∞ is included in the open half plane left delimited by γ ∞ . We will reach our contradiction by exhibiting another singularity which is closer to γ ∞ . In order to do so, we rely on the assumption that Σ ∞ is accumulated by images under the Teichmüller flow of Σ 0 . For any n ∈ N we denote analogously by γ n the horizontal saddle connection g tn (γ) of Σ n , by (s i n ) i∈{1,2} the two endpoints of γ n , by M γn the midpoint of γ n and by s min n the closest point to γ n as defined above. Since developing maps are continuous and since Figure 19. The quantity here corresponds to the radii of all small red circles. The assumption that Σ ∞ is the limit of the Σ nn allows us to measure with respect to all the developing maps making errors of size at most with respect to what will be measured with the developing map of Σ ∞ . The red dots corresponds to the singularity of Σ ∞ . On the left what happens on Σ n and on the right on Σ m . The two faded disks correspond to the definitions of s min n and s min m . The arrow symbolises that s min m should be map to a singularity closed to γ n that s min n .

In particular, we proved that there is another horizontal saddle connection continuing γ ∞ , the one relating s min ∞ and one of the two endpoints of γ ∞ . One can now repeat the previous argument with this new saddle connection together with γ ∞ to get another horizontal saddle connection continuing the two previous ones. In the end, one is left with a sequence of saddle connections continuing one another. Since there are at most finitely many horizontal saddle connections in a dilation surface, such a sequence must be periodic. The concatenation of these horizontal saddle connections form a closed curve. Since any two consecutive saddle connections differ only by an angle π, this curve becomes simple if moved slightly toward the left. Such a simple curve must be the boundary of a cylinder and the angle of such a cylinder must be π/2 for otherwise, repeating the argument of the beginning of this proof, Σ ∞ would not be in the closure of the Teichmüller orbit of Σ 0 . 7.4. Proof of Proposition 9. We will need the following lemma. The modulus of a cylinder is exactly the ratio length/height of the rectangle R inscribed in the trapezoid. Consider two cylinders C 1 , C 2 whose corresponding rectangles have respective heights h 1 , h 2 and lengths l 1 , l 2 . If C 1 and C 2 intersect (see Figure 21) we see that l 1 ≥ h 2 and l 2 ≥ h 1 . Let M i = l i h i be the modulus of C i . We see that M 1 M 2 ≤ 1. In particular at least either M 1 or M 2 is less than 1.

We can now prove Proposition 9. Assume that there are cylinders of arbitrary large moduli. Since two different cylinders always define two different free homotopy class, we can always find arbitrary cylinders of arbitrarily large moduli which intersect. This contradicts Lemma 15.

Figure 7 .

 7 Figure 7. The three first polygons of a degenerating sequence of type 1 whose vertices all converge toward either s 1 ∞ or s 2 ∞ . The terminology long side is explained below.

Figure 8 .

 8 Figure 8. On the left, a Delaunay admissible configuration of two polygons of type 1: none of the singularities lies inside the 2 Delaunay circles. As the polygons shrink, the Delaunay circle tend to cover half a plane. On the right a Forbidden configuration: the red dot lies in inside a large Delaunay circle (becoming half a plane).

Lemma 15 .RFigure 20 .

 1520 Figure 20. The modulus of a cylinder is the modulus of a rectangle inscribed in it.

A. Boulanger, Institut mathématique de Marseille, Aix-Marseille Université, Technopôle Château-Gombert 39, rue Frédéric Joliot-Curie, Marseille Cedex 13 E-mail address: adrien.boulanger@univ-amu.fr S. Ghazouani, Imperial College, London, U.K. E-mail address: s.ghazouani@ic.ac.uk G. Tahar, Weizmann Institute of Science, Rehovot, Israel E-mail address: tahar.guillaume@weizmann.ac.il


Mohamed Niang
email: mohamed.niang@etudiant.univ-reims.fr

Alexandre Philippot
email: alexandre.philippot@univ-reims.fr

François Gellot
email: francois.gellot@univ-reims.fr

Raphaël Coupat
email: raphael.coupat@reseau.sncf.fr

Bernard Riera
email: bernard.riera@univ-reims.fr

Sébastien Lefebvre
email: s.lefebvre@reseau.sncf.fr

Formal Verification for Validation of PSEEL's PLC Program

Keywords: Model-checking, recipe book, factory tests, systems engineers, railways, safety

In order to keep its leadership in French rail market and to improve work conditions of its systems engineers during automation projects, the SNCF (French acronym for National Society of French Railways) wants to develop solutions increasing the productivity. One of these improvements focuses on the current methodology used by systems engineers to verify and validate PLC programs of electrical installations. This task remains one of the most important during an automation project because it is supposed to ensure installations safety, but it must be optimized. Through an industrial thesis financed by SNCF, the aim of this research project is to improve this method and reduce time validation of programs by providing a tool which will help systems engineers to verify and validate quickly and automatically PLC programs during any automation project, not necessarily during factory tests but directly from their office.

INTRODUCTION

In automated systems, most of accidents that occur in industry have been discovered to be the result of Programming errors [START_REF] Mokadem | Verification of a timed multitask system with UPPAAL[END_REF]. Therefore, verification of PLC program before its implementation remains a very important task during an automation project. This verification must concern both functional and safety parts. The first one ensures that the PLC programs meet the functional specifications, and the second one consists in verifying if the controlled system can be or not exposed to dangerous states leading to human and equipment damage. Nowadays, some verification and validation techniques like tests and simulation are available.

At SNCF, the system engineers apply currently these methods to validate the control command (programs and electrical cabinets' wiring) of PSEEL (Power Supply Equipment of the Electric Lines) by using a recipe book which contains a set of scenarios or sequential instructions. According to their knowhow and experience during these last decades about their systems, they consider that a PSEEL's control command is valid once it satisfies the whole test.

The verification consists in executing manually each instruction contained in the recipe book during factory tests, and then comparing the obtained results with the expected ones. This verification is therefore not automatic, and requires too much time because of the length of tests (almost 100 pages of instructions). Moreover, although it was used to validate PLC programs for several decades, this method is not efficient to check formally safety part of PLC programs insofar as it verifies only if PLC programs meet the requirements specifications.

Our first task in this work is to optimize this current methodology of verification by making it faster and automatic with the use of a modelchecker. Then we propose an exhaustive method which will be used to verify the safety part of PLC programs.

After a presentation of general context in section 2, we detail the principle of our methodology and illustrate it through an application in section 3. Exhaustiveness of recipe book is studied in section 4, and section 5 introduces a solution for automatic generation of models used for programs verification. We conclude finally this paper and propose some work prospects in section 6.

GENERAL CONTEXT

The PSEEL are the electrical supply points of the electrified lines, called catenaries. Their role is to transform, to supply, and to rectifier in the case of DC supply, the tension of the High-Voltage (HV) network into compatible tension with traction units (1500 V DC or 25kV AC). They are composed of sub-systems (sSys) like Transformer Group, Track feeder, and common, and each of these sub-systems is composed of elements of sub-Systems (ElSys) like switch, circuit breaker, and so on (Figure 1). These electrical systems are subject to strict standards of railway safety (EN 50126, 2012) (IEC 60870-4, 2013). The PSEEL are distributed automated systems whose control command can be done either locally or remotely in a centralized control station named Central Sub-Stations (CSS).

The recipe book represents for SNCF the main reference for validation of PSEEL's control command systems since many years. It contains several scenarios that systems engineers execute on PSEEL and analyze its behavior in order to validate or not its control command. An example of a test scenario is presented in Table 1. During an automation project, the recipe book and the PLC programs are automatically generated with software named Odil [START_REF] Coupat | Automatic generation of safe PLC program for PSEEL[END_REF]. For this, the systems engineers enter all inputs data of the system (like single line diagram of PSEEL, equipment configuration, inputs/outputs ...) and then, Odil generates automatically programs and recipe book. After a proofreading of these latter, they verify online the correctness of whole control command (PLC program and electrical cabinets) during factory tests, by executing all the scenarios of the recipe book on system. Moreover during factory tests, they need to connect devices simulators to cabinets (like switches and circuit breakers) in order to make tests possible. One major difficulty they can encounter during tests is that in case of an unsatisfied instruction in factory, they must analyze the problem and determine its cause (programming error or wiring error of electrical cabinets). For example in the test scenario described in Table 1, when the circuit breaker does not open after overcurrent (instruction N°1), there are two possible explanations: o The information "Imax" is not received by the PLC (because the input is not wired for example); o

The information is received but the SFC program of the circuit breaker does not evolve (bad program). Despite their experience, this diagnosis may remain long and complex in some cases. The main approach of our methodology consists in dividing the validation step into two parts: offline validation of PLC programs with model-checker Uppaal [START_REF] Behrmann | Uppaal implementation secrets. 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems[END_REF], and then online validation of electrical cabinets during factory tests with virtual commissioning. Thus, PLC programs can be validated earlier with Uppaal and before factory tests. Moreover, this validation step does not require physical devices simulators because they are now included in Uppaal models. From a model of PSEEL, PLC programs, and recipe book, Uppaal is able to check automatically during the simulation if the PLC programs satisfy the recipe book. For this, the model-checker executes all scenarios of recipe book on the system, and verifies if there exists at least one instruction in the recipe book whose effect on the PSEEL does not correspond to the expected one. Then, simulation results will help to diagnose easily the problem if it exists, or otherwise to validate the PLC programs. The validation of electrical cabinets will be done online and also automatically, with the use of virtual commissioning connected to electrical cabinets (not presented in this paper). The advantage of this methodology is as follows: not only the validation of programs will be faster and automatic, but it will also facilitate the validation of electrical cabinets. In fact, once we implement valid PLC programs in the system, any encountered problem during factory tests would necessarily result from wiring errors of electrical cabinets. Another objective in this work is to propose with model-checking an exhaustive method which verifies the safety part of PLC programs. System modeling is the first step of our approach.

SYSTEM MODELING

In this section, we present and illustrate our methodology through its application on a transformer group (PSEEL's sub-system). System modeling requires careful structural analysis of PSEEL and PLC programs because the models must have the same behavior as real system. The transformer group is controlled by one PLC, and is basically composed of circuit breakers, switches, and transformer. Its program's outputs correspond to the orders sent to devices, and inputs are the observed faults on operative part and the devices' states (opened or closed). The programs are designed in STRATON (www.copalp.com) using some of the standardized languages (IEC 61131-3, 2003) such as Ladder Diagram (LD), Sequential Function Chart (SFC) and Structured Text (ST). But in our Uppaal models, the whole program needs to be translated into ST because the model-checker cannot interpret the other languages. Whatever the programming language would be, each scan cycle includes three main phases: input reading, program execution and output updating. The variables "so" and "sf" (Figure 2) represent respectively the information "switch opened" and "switch closed", and "close" (respectively "open") represents closing order (respectively opening order) sent by the programs. The switch can reach three possible states: opened (so=true and sf=false), moving (so=false and sf=false), and closed (so=false and sf=true). Initially opened, it starts moving once it receives closing order from the program. Then, after a certain duration (x==time) it becomes fully closed if the order was still maintained, or otherwise returns to the initial state if closing order was released or if opening order was activated. The switch's behaviour is practically the same when it receives opening order from closed state. We recall here that the order sent by operator is not directly received by the device, but rather by its SFC program which will apply it or not, if the program allows this action. Note that although the transformer has continuous behaviour (magnetic, thermal…), we do not take it into account in its model. So we represent it as a structure of variables (observers, parameters, and observed faults) because these are the only information we need for this model: struct {bool defBLQ, blocDef, defTemp, defBLQR, blocDefRed, defTempRed, wdMicom, TcMC, temp2TR, AMR, fuFuRC, AvDiode, imaxGT, OoAbsUHT, OoDjAbsUHT, deblocGT, absUBarre, presenceSGT, pres_Hexa; int tmpReencGT;} GT1; To reduce states space, most of states are declared as committed so that time can elapse only during program execution. Therefore the duration of input acquisition and output emission is negligible. The control program contains timing operations, described by functional blocks called TON (Timer On-delay). Its behaviour is explained in IEC 61131-3 standard. This TON block has two input variables (boolean variable in to start or stop counting time, and time parameter PT which indicates the timing delay) and two output variables (boolean variable Q which equals 1 if the delay has expired, and time variable x which gives the time elapsed from the last rising edge of in). Initially idle, its location becomes running when the timer has been switched on, and timeout when the fixed delay (PT) has been reached. The model in Figure 5 has been inspired in [START_REF] Mokadem | Verification of a timed multitask system with UPPAAL[END_REF].

Transformer Group Modeling

Control Program Modeling

Any SFC program can use more than two TON block in its different steps. So instead of using a TON block for any step, we declare only one TON block per SFC program. In fact, after a structural analysis of these SFC programs, we noticed that we can never have more than one step simultaneously activated. Thus, a single TON block can be used by all steps of one SFC program without any conflict. However, for two successive steps using the same TON, we must make sure that between the two steps' activation, the TON's output changes from 1 to 0. For this, we must define correctly the inputs in and PT of the TON block used by the SFC program.

In the example described in Figure 6, both steps x1 and x2 use the same TON. When x1 is activated, time starts elapsing until it reaches 500ms. Then, output Q and transition ft1 change from 0 to 1, leading to x2's activation and x1's deactivation. Therefore, the input in (whose expression is shown in Figure 6) moves from 1 to 0 and resets the timer (thus output Q changes from 1 to 0 and input PT changes from 500ms to 1000ms). During the next PLC cycle, the value of ft1 will be updated because the step x1 is no more activated, so the input in will move again from 0 to 1 and time will start again elapsing for x2. But with these operations, we noticed a delay of one PLC scan time from x2's activation to timer's restart. To compensate this delay, we subtract it to the pre-set time of x2. This optimization will reduce the number of TON used, and consequently the space of reachable states.

The whole program is not represented in our model because some lines of code are only dedicated to send information to other PLC through network (Factory Instrumentation Protocol). LD programs: where devices' states are read and all observed faults are collected and used to compute observers. The SFC programs will be translated into Structured Text language (ST), using the classical algebraic representation of SFC [START_REF] Machado | Logic controllers dependability verification using a plant model[END_REF]. The LD programs will also be translated into ST language (Figure 7).

Recipe Book Modeling

After a structural analysis of recipe book, we realized that it could be translated into SFC programs (one per scenario) because it is composed of actions and transitions. In Figure 8 we present the translation of scenario described in Table 1. The variable "start elapsing" is dedicated to trigger a timer which counts the elapsed time in one step of the scenario (x1, x2, or x3 in this example). So if there is a step on which the elapsed time exceeds a certain value (which is not supposed to be reached if the program is valid), it will mean that program presents errors because the transition associated to that step cannot be satisfied. This translation will be applied for all scenarios of transformer group's recipe book. Then, the model described in Figure 9 will call and execute sequentially all scenarios. The recipe book's evolution state will be updated during any PLC scan time. Each state automaton of this model (except the initial and last ones) corresponds to one scenario. During simulation, one scenario can be executed only if the previous one (if it exists) was satisfied. Therefore the program is valid only if the final state automaton (named valides in Figure 9) is reachable, or if it does not exist a blocking instruction in recipe book.

Simulation Results

To validate the PLC program, all scenarios must be executed and satisfied during simulation. For this, we can verify if the final state automaton is reachable by using the query:

E <> recipe_book.valides (1)
However the model checker does not return any trace if (1) is not satisfied. Thus (1) is only useful to determine if programs are valid or not, but not sufficient for diagnosis. So instead of this property, we verify if there exists a blocking step of a scenario where the corresponding condition is not satisfied by using the query:

E<>time_step.timeout (2)
Time step is a timer which counts the elapsed time for any step of the recipe book. If (2) is satisfied, the model checker will return directly the scenario and blocking step on which simulation stopped. Moreover, by analysing the current state of programs, it will help for diagnosis. After a first simulation (see results in Table 2), we realized that (1) is satisfied and ( 2) is not: this is far from being a surprise because the program we used here has already been validated during factory tests.

In the following example, we used a modified program to verify if problems can be diagnosed during simulation. Table 2 presents simulation results, and gives the time and memory used for verification (on a windows machine with 4Gb RAM, Core i5). As expected, (1) is not satisfied for the modified program, but to diagnose the problem, it is not sufficient. So when we verify by using (2), the model-checker has shown that the instruction N°1 of overcurrent test is blocking (step x1 of Figure 8) because the circuit breaker did not open after overcurrent. Moreover, when we analyse the current state of circuit breaker SFC program in simulation results (see in Figure 10), we notice that its evolution stopped in that moment on a step where it was waiting for opening order (step x5 of SFC program grafCtrCmdeDJGT1 in variables column of Figure 10). Thus, we conclude that the transition following that step is not correct because it did not take into account the overcurrent information. This result was expected because the expression "or Imax" was initially deleted from that transition. After correction and second simulation, the instruction N°2 of overcurrent test (transition ft2 of Figure 8) is not satisfied because the circuit breaker started closing when it received that order whereas it should not. In fact, the circuit breaker must stay opened while overcurrent does not disappear. This result was also expected because the expression "and not Imax" was also deleted from SFC program's transition. In that way, we can diagnose quickly and correct the whole program by referring to the expected results of recipe book, and simulation does not require too much memory. Its efficiency has already been validated with some examples of wrong programs.

SAFETY PART VERIFICATION

Although recipe book has served to validate PSEEL's programs for many decades, it is not sufficient to verify formally installations safety. In fact, the previous method does not study all the reachable states of system (meaning all the 2 Ne possible states, with Ne = number PSEEL's sensors + number of received orders). Moreover, it has also been proved in [START_REF] Coupat | Automatic generation of safe PLC program for PSEEL[END_REF] with a specific PSEEL, that there exists one scenario (with low occurrence) not included in recipe book, but which can expose that PSEEL in dangerous state, meaning that the method is not exhaustive. So supposing that events like sending orders by operator or faults apparition can occur whenever on system, the principle is to check with Uppaal if each of these states is not dangerous (meaning does not violate a set of safety properties). Therefore recipe book will no more represent a reference of verification. We delete its model and we add two others ones that generate randomly faults (left side on Figure 11) and sending order (right side of Figure 11). With the first model, fault can take two possible boolean values (true or false), and with the second one a device's SFC program can receive opening order from operator (co=true and cf=false), closing order (co=false and cf= true), or no order (co=false and cf=false). During a PLC cycle, an order sent by an operator would not have any effect on system if the SFC program of the targeted device was not in a step waiting for that order. Thus, to avoid ineffective orders and reduce states space, we added some guards in these models.

This method is more efficient than the first one because all the reachable states of system are browsed and studied, unlike the first method. And it can verify not only the safety part but also the functional correctness of PLC programs, according to the set of properties we verify. With a program already validated by recipe book, we have to verify with this second method if there exists at least a path which leads system to a dangerous state. In that case, it would mean that the recipe book does not contain all required tests, and is therefore insufficient to guarantee safety. Currently, the SNCF experts help us to determine all the dangerous states of PSEEL in order to define all safety properties and complete the verification. We can already verify its efficiency by applying it to the previous modified program. An example of dangerous state is that a blocking fault appears during 300ms without the circuit breaker opens:

E<>cycle.fin and TON_fault.timeout and DG1.sf

(3)

TON_fault is a timer which counts the elapsed time since fault's apparition while circuit breaker stays closed. After simulation, we noticed that this state is reachable only if overcurrent fault appears for 300ms: that is obvious because the variable "Imax" was deleted from that SFC program. This simulation requires more memory time (20.56s and 140Mb with (3)) because of states space increase, but this method is more efficient than the first one. All the errors detectable by recipe book are also detectable by this second method, meaning that the latter is also more exhaustive.

AUTOMATIC GENERATION OF UPPAAL MODELS

The methodology of formal verification must be applied for any new automation project. Because of heterogeneity of PSEEL and programs, systems engineers would be obliged to adapt Uppaal models according to installation's structure, recipe book and program's content. This additional task goes against our principle in this work because it increases time project. As for programs and recipe book, we propose to generate automatically with Odil the Uppaal file (*.xml) which contains all required inputs data (PSEEL models, programs, and recipe book). The methodology used to generate this xml file is not detailed in this paper, but presented in [START_REF] Coupat | Automatic generation of safe PLC program for PSEEL[END_REF]. The xml file contains exactly the same information as for program and recipe book, but in a different language. After automatic generation, the systems engineers have just to import from Uppaal the generated xml file (for any subsystem of PSEEL), and execute it in order to analyse results and validate automatically programs, directly from their office and not necessarily in factory. Some examples of xml files has been generated and used for simulation.

CONCLUSION

The [START_REF] Coupat | Standardization and Safety Control Generation for SNCF Systems Engineer[END_REF]. The proposed solution in this work aims to solve these problems insofar as programs validation is faster and automatic (recipe book of transformer group is browsed in a few tens of milliseconds, see in Table 2), and can be done earlier without any use of physical device simulator compared to the previous method. Another objective in this work was to develop a method which verifies the safety of PLC programs. With model-checker Uppaal, we verify formally for each reachable state of system, if the set of dangerous states (representing the property to verify) is not violated. We proposed also in this work to generate automatically the Uppaal models of verification for any new project, so that systems engineers will not lose time in designing it themselves.

The method of automatic verification has been presented to SNCF's systems engineers, and was judged interesting insofar as it allows to verify quickly and automatically the correctness of any PLC programs. Moreover, it has been used to verify a program newly developed by systems engineers and not tested yet during factory tests. For this we implemented the program in our tool, and we corrected all the problems detected in the new program. The obtained results was presented to systems engineers, then they were approved.

In addition to reduce time project and human error during verification, these results will facilitate validation step of electrical cabinets' wiring. In fact, systems engineers use recipe book to validate both programs and cabinets. When they encounter an instruction not satisfied in recipe book, they must analyze it and determine if it is due to programming error, or wiring error. With our method, they can now exclude the first hypothesis during factory tests because programs are validated earlier.

Our future work will focus on the improvement of validation step of electrical cabinets' wiring. As for program validation, we will try to make it faster and automatic in order to reduce at most time validation during any automation project.

Figure 1 :

 1 Figure 1: Decomposition of PSEEL.

Figure 2 :

 2 Figure 2: UPPAAL model of switch.

Figure 3 :

 3 Figure 3: UPPAAL model of circuit breaker. The model of a circuit breaker presented in Figure 3 has some particularities compared to switch model: o To close the circuit breaker, the two orders (open and close) must be maintained simultaneously for a certain duration (x==tmpEnclDJGT); o To open it, just release the opening order; o Contrary to the switch, opening time (timeOP) is different from closing time (timeCL).

Figure 4 :o

 4 Figure 4: UPPAAL model of PLC cycle. The model in Figure 4 synchronizes all the other models of the system thanks to broadcast channels. PLC cycle structured as a loop includes a clock x which measures the cycle time (equal to 20 time units here). Initialisation of SFC programs and parameters is required during the first PLC cycle. Then, the cycle is composed of 6 steps: o Input reading (faults and devices' states) o Command reading (sent by operators) o Timers evolution (synchronised with TON! channel) o Execution of main program (SFC programs update) followed by output writing; o Evolution of operative part (channel PO!) o End of cycle (channel end!)

Figure 5 :

 5 Figure 5: UPPAAL model of a TON block.

Figure 6 :

 6 Figure 6: Example of TON's use in a SFC program. So the control program is basically composed of: o SFC block programs: which command the equipment like switches and circuits breakers. The structure of the SFC program depends on the kind of equipment. oLD programs: where devices' states are read and all observed faults are collected and used to compute observers. The SFC programs will be translated into Structured Text language (ST), using the classical algebraic representation of SFC[START_REF] Machado | Logic controllers dependability verification using a plant model[END_REF]. The LD programs will also be translated into ST language (Figure7).

Figure 7 :

 7 Figure 7: Example of LD programs translation into ST.

Figure 8 :

 8 Figure 8: Translation of scenario into SFC program.

Figure 9 :

 9 Figure 9: Uppal model of recipe book.

Figure 10 :

 10 Figure 10: simulation view.

Figure 11 :

 11 Figure 11: Uppaal models of fault and sending order.

Table 1 :

 1 Example of one test scenario in recipe book.

Table 2 :

 2 Simulation results.