Sandrine Caruso

A family of pseudo-Anosov braids whose super summit sets grow exponentially

We prove that the size of the super summit set of a braid can grow exponentially with the canonical length of the braid, even for pseudo-Anosov braids.

Introduction

When trying to find a polynomial time solution to the conjugacy problem in braid groups, one strategy is to use Garside theory in order to associate to any given braid a certain finite subset of its conjugacy class. This subset should only depend on the conjugacy class of the given braid, and it should be effectively computable. Among the invariants of this type, the super summit set, introduced by El-Rifai and Morton in [START_REF] Elrifai | Algorithms for positive braids[END_REF], is one of the most famous. More recently, in [START_REF] Gebhardt | The cyclic sliding operation in Garside groups[END_REF], Gebhardt and Gonzalez-Meneses have introduced a new invariant, the set of sliding circuits, which is a subset of the super summit set.

Given two elements of the braid group, the strategy for deciding if they are conjugate is then in two steps: first, for each of the two braids, find one element of the invariant subset of its conjugacy class; then, calculate the complete invariant subset of one of the two in order to check whether it contains the other element.

There does exist a polynomial time algorithm which, given a braid, finds an element of its super summit set [START_REF] Birman | The infimum, supremum, and geodesic length of a braid conjugacy class[END_REF]. However, determining whether two such elements are in the same super summit set seems to be much more difficult to do quickly. Indeed, in general, the size of the super summit set of a braid is not bounded by a polynomial in the length of the braid: in [START_REF] Gonzalez-Meneses | On reduction curves and Garside properties of braids, Topology of algebraic varieties and singularities[END_REF], Gonzalez-Meneses construct a family of reducible braids whose super summit set grows exponentially, both with the length of the braid and with the number of strings. In fact, even the sets of sliding circuits of his braids grow exponentially.

One might have hoped that this bad behavior is specific to reducible braids. However, inspired by his construction, we present here a family of pseudo-Anosov braids with 5 strings whose super summit set grows exponentially in the length of the braids.

β k = (σ 2 σ 1 ) 3k+1 σ 2k+2 4 σ 3 σ 2k-1 4 1
is pseudo-Anosov and has a super summit set whose cardinality is at least 2 2k-2 .

It is interesting to note that, on the other hand, the set of sliding circuits of this family of braids is as small as possible (Lemma 2.4). This is relevant to a conjecture, well known to the specialists of the domain:

Conjecture. For all n, there exists a polynomial P n such that, for every pseudo-Anosov braid x with n strings and with canonical length , the cardinality of the set of sliding circuits of x is at most P n ( ).

Acknowledgments. I would like to thank my PhD advisor Bert Wiest for his help and guidance. The Artin braid group with n strings is isomorphic to the group MCG(D n , ∂D n ). Recall that the classification theorem of Nielsen and Thurston states that a mapping class f ∈ MCG(D n ) is either periodic, or reducible, or pseudo-Anosov. A braid x ∈ MCG(D n , ∂D n ) can be projected on an element of MCG(D n ). We call Nielsen-Thurston type of x the Nielsen-Thurston type of its projection. The definition of periodicity is then transformed as follows: a braid x ∈ B n is periodic if and only if there exist nonzero integers m and l such that x m = ∆ l , where ∆ = (σ

Definitions

Braids and mapping class group of the punctured disk

1 • • • σ n-1 )(σ 1 • • • σ n-2 ) • • • (σ 1 σ 2 )σ 1 .
(Geometrically ∆ corresponds to the half-twist around the boundary of the disk).

Garside structure and invariants of conjugacy classes

A general introduction to Garside theory can be found in [START_REF] Dehornoy | Garside Calculus[END_REF]. We shall only recall some facts which are useful for our purposes.

While the group B n admits the well-known presentation of groups

B n = σ 1 , . . . , σ n-1 ; σ i σ i+1 σ i = σ i+1 σ i σ i+1 and σ i σ j = σ j σ i for |i -j| 2 ,
the monoid of positive braids B + n , which is embedded in B n , is defined by the same presentation, interpreted as a presentation of monoids.

For m n, we denote ∆ m the element of B + n defined by

∆ m = (σ 1 • • • σ m-1 )(σ 1 • • • σ m-2 ) • • • (σ 1 σ 2 )σ 1
and we will denote ∆ = ∆ n ∈ B + n . The pair (B + n , ∆) defines what we call a Garside structure on B n . Without giving the complete definition, here are some properties of such a structure. The group B n is endowed with an order defined by x y ⇔ x -1 y ∈ B + n . If x y, we say that x is a prefix of y. Any two elements x, y of B n have a unique greatest common prefix.

We also define by x y ⇔ xy -1 ∈ B + n . Note that x y is not equivalent to y x. The elements of the set {x ∈ B n , 1 x ∆} are called simple braids. Definition 1.2 (left-weighting). Let s 1 , s 2 be two simple braids in B n . We say that s 1 and s 2 are left-weighted if there does not exist any generator σ i such that s 1 σ i and σ -1 i s 2 are both still simple. Proposition 1.3. Let x ∈ B n . There exists a unique decomposition x = ∆ p x 1 • • • x r such that x 1 , . . . , x r are simple braids, distincts from ∆ and 1, and such that x i and x i+1 are left-weighted for all i = 1, . . . , r -1.

Definition 1.4 (left normal form). In the previous proposition, the writing

x = ∆ p x 1 • • • x r is called the left normal form of x, p
is called the infimum of x and is denoted by inf x, p + r is the supremum of x and is denoted by sup x, and r is called the canonical length of x.

Furthermore, we denote by

ι(x) = ∆ -p x 1 ∆ p the initial factor of x (ι(x) = x 1 if p is even, ι(x) = ∆ -1 x 1 ∆ if p is
odd), and φ(x) = x r its final factor. Definition 1.5 (super summit set). Let x ∈ B n . We call super summit set of x (abbreviated SSS) the set of the conjugates of x with the minimal canonical length.

Obviously, if x and y are conjugate, they have the same super summit set: thus the super summit set is an invariant of the conjugacy class. Definition 1.6 (cycling, decycling). Let x ∈ B n , and let x = ∆ p x 1 • • • x r be its normal form. If r 1, we define

• the cycling of x by ι(x) -1 xι(x) = ∆ p x 2 • • • x r x 1 , • the decycling of x by φ(x)xφ(x) -1 = ∆ p x r x 1 • • • x r-1 ,
where x 1 = ι(x) = x 1 or ∆ -1 x 1 ∆, and x r = φ(x) = x r or ∆ -1 x r ∆, depending on the parity of p. If r = 0, the cycling and the decycling of x are equal to x itself.

An interesting property of the cycling and decycling operations is that they preserve the SSS. Moreover, from any braid, we can obtain an element of its SSS by applying a finite number of cyclings and decyclings [START_REF] Elrifai | Algorithms for positive braids[END_REF].

Another type of conjugation is the cyclic sliding [START_REF] Gebhardt | The cyclic sliding operation in Garside groups[END_REF].

Definition 1.7 (cyclic sliding). We call preferred prefix of x the greatest common prefix of ι(x) and ∂φ(x) = φ(x) -1 ∆. The cyclic sliding is defined as the conjugation by the preferred prefix.

The cyclic sliding also preserves the super summit set. The operation of cyclic sliding is ultimately periodic, because it does not increase the length of the braid. This allows us to define another invariant of conjugacy classes [START_REF] Gebhardt | The cyclic sliding operation in Garside groups[END_REF]: Definition 1.8 (set of sliding circuits). We call set of sliding circuits of a braid x (abbreviated SC) the set of the conjugates of x that are periodic points of the cyclic sliding.

The SC of x is a subset of its SSS [START_REF] Gebhardt | The cyclic sliding operation in Garside groups[END_REF]. Definition 1.9 (rigidity). A braid x is said to be rigid if φ(x) and ι(x) are left-weighted, that is, if the cyclic sliding of x is equal to x.

A rigid braid, by definition, belongs necessarily to its SC, since it is a periodic point of period 1 of the cyclic sliding operation.

A family of pseudo-Anosov braids

Let k 2 be an integer. Let us define the following braid with 5 strings:

β k = δ 3k+1 3 σ 2k+2 4 σ 3 σ 2k-1 4
where δ 3 = σ 2 σ 1 . Recall that we also have ∆ 3 = σ 2 σ 1 σ 2 .

Lemma 2.1. The left normal form of β k is given by the following factorisation

β k = (∆ 3 σ 4 ) 2k (δ 3 σ 4 σ 3 σ 4 )(σ 3 σ 4 )(σ 4 ) 2k-3 .
In particular, inf β k = 0 and sup β k = 4k -1.

Proof. We easily check that this writing is indeed equal to β k (recall that ∆ 2 3 = δ 3 3 ), that each of these factors is a simple braid, and that two successive factors are left-weighted. (See Figure 1.) Let us also consider the braid Indeed, β k has the same canonical length as one of its conjugates that lies in its SC, and thus in its SSS.

βk = (σ 1 σ 3 ) 2k-2 (σ 3 σ 4 ∆ 3 )(∆ 3 σ 4 )[(δ 3 σ 4 )( δ3 σ 4 )] k-1 (δ 3 σ 4 σ 3 σ 4 ),
Proof of Lemma 2.2. The braid βk is obtained by conjugating

β k by τ = (∆ 3 σ 4 ) 2k (δ 3 σ 4 σ 3 σ 4 )(σ 3 σ 4 ∆ 3 )(∆ 3 σ 4 ) 2k-1 (δ 3 σ 4 σ 3 σ 4 ), i.e. βk = τ -1 β k τ . Then, the left normal form of βk is βk = (σ 1 σ 3 ) 2k-2 (σ 3 σ 4 ∆ 3 )(∆ 3 σ 4 )[(δ 3 σ 4 )( δ3 σ 4 )] k-1 (δ 3 σ 4 σ 3 σ 4 ).
We observe that this braid is rigid, and consequently, belongs to the SC of β k . Furthermore, we have inf βk = 0 and sup βk = 4k -1.

The SC has only one orbit under cycling or conjugation by ∆ Lemma 2.4. The SC of β k is reduced to the orbit of βk under the operation of cycling or conjugation by ∆.

We shall denote this orbit under cycling and conjugation by O( βk ). Note that, because of the rigidity of βk , a cycling of βk is just a cyclic permutation of its factors.

The proof is based on the following two lemmas: Lemma 2.6 gathers some results proved in [START_REF] Gebhardt | A new approach to the conjugacy problem in Garside groups[END_REF] or in [START_REF] Birman | Conjugacy in Garside groups. II. Structure of the ultra summit set[END_REF] (Section 3.3), and Lemma 2.7 is stated and proven in [START_REF] Gonzalez-Meneses | Reducible braids and Garside theory[END_REF] (Lemma 6.1).

Definition 2.5 (transport). Let

x ∈ B n be in its super summit set. Let s be a simple braid such that y = s -1 xs is in the super summit set of x. Let x = ι(x) -1 xι(x) and y = ι(y) -1 yι(y) be the braids obtained by cycling from x and y, respectively. We call transport of s the braid s (1) = ι(x) -1 sι(y), that is to say the braid s (1) such that y = (s (1) ) -1 x s (1) . Lemma 2.6. If s is simple, s (1) is simple. Moreover, for s and t simple, s t implies s (1) t (1) , and (ι(x)) (1) = ι(x ). In particular, if s is a prefix of ι(x), then s (1) is a prefix of ι(x ). We also have (∂φ(x)) (1) = ∂φ(x ) and in particular, if s is a prefix of ∂φ(x), then s (1) is a prefix of ∂φ(x ). Lemma 2.7. Given two conjugate elements x and y, both in their SC, there exists a sequence of elements x = α 1 , α 2 , . . . , α r , α r+1 = y, all in the SC, and simple braids s 1 , . . . , s r , such that α i+1 = s -1 i α i s i , i = 1, . . . , r, and such that Lemma 2.4. Let ι = ι( βk ) = σ 1 σ 3 be the initial factor of βk and φ = φ( βk ) = δ 3 σ 4 σ 3 σ 4 its final factor, and ∂φ = σ 2 σ 1 σ 3 σ 2 σ 4 the complement of φ (that is, φ • ∂φ = ∆). Let us show that for each strict prefix p of ι or of ∂φ, the braid p -1 βk p does not belong to the SC of βk .

s i ι(α i ) or s i ι(α -1 i ) = ∂φ(α i ). Proof of
Let us list the strict prefixes of ι and ∂φ. The strict prefixes of ι = σ 1 σ 3 are σ 1 and σ 3 . Those of ∂φ are σ 2 , σ 2 σ 1 , σ 2 σ 3 , σ 2 σ 1 σ 3 , σ 2 σ 3 σ 4 , σ 2 σ 1 σ 3 σ 2 and σ 2 σ 1 σ 3 σ 4 . For each of them, let us calculate the left normal form of p -1 βk p.

• For σ 1 :

σ -1 1 βk σ 1 = σ -1 1 (σ 1 σ 3 ) 2k-2 (σ 3 σ 4 ∆ 3 )(∆ 3 σ 4 )[(δ 3 σ 4 )( δ3 σ 4 )] k-1 (δ 3 σ 4 σ 3 σ 4 )σ 1 = (σ 1 σ 3 ) 2k-2 (σ 3 σ 4 ∆ 3 )( δ3 σ 4 )[(δ 3 σ 4 )( δ3 σ 4 )] k-1 (δ 3 σ 4 σ 3 σ 4 )σ 1 ,
the last line being in left normal form.

• For σ 3 :

σ -1 3 βk σ 3 = (σ 1 σ 3 ) 2k-3 (σ 3 σ 4 ∆ 3 )(∆ 3 σ 4 ) 2 ( δ3 σ 4 )[(δ 3 σ 4 )( δ3 σ 4 )] k-2 (δ 3 σ 4 σ 3 σ 4 )σ 3 .
• For σ 2 :

σ -1 2 βk σ 2 = ∆ -1 (∆ 3 σ 3 σ 2 σ 4 σ 3 δ 3 )(σ 1 σ 3 ) 2k-2 (σ 3 σ 4 ∆ 3 )(∆ 3 σ 4 ) [(δ 3 σ 4 )( δ3 σ 4 )] k-1 (δ 3 σ 4 σ 3 σ 4 σ 2 ).
• For σ 2 σ 1 :

(σ 2 σ 1 ) -1 βk σ 2 σ 1 = ∆ -1 (∆ 3 σ 3 δ 3 σ 4 σ 3 )(σ 1 σ 3 ) 2k-2 (σ 3 σ 4 ∆ 3 )(∆ 3 σ 4 ) [(δ 3 σ 4 )( δ3 σ 4 )] k-1 (δ 3 σ 4 σ 3 σ 4 σ 2 σ 1 ).
• For σ 2 σ 3 :

(σ 2 σ 3 ) -1 βk σ 2 σ 3 = ∆ -1 ( δ3 σ 3 σ 4 σ 2 σ 3 δ 3 )(σ 1 σ 3 ) 2k-2 (σ 3 σ 4 ∆ 3 )(∆ 3 σ 4 ) [(δ 3 σ 4 )( δ3 σ 4 )] k-1 (δ 3 σ 4 σ 3 σ 4 σ 2 σ 3 ). • For σ 2 σ 1 σ 3 : (σ 2 σ 1 σ 3 ) -1 βk σ 2 σ 1 σ 3 = ∆ -1 ( δ3 σ 3 δ 3 σ 4 σ 3 )(σ 1 σ 3 ) 2k-2 (σ 3 σ 4 ∆ 3 )(∆ 3 σ 4 ) [(δ 3 σ 4 )( δ3 σ 4 )] k-1 (δ 3 σ 4 σ 3 σ 4 σ 2 σ 1 σ 3 ). • For σ 2 σ 3 σ 4 : (σ 2 σ 3 σ 4 ) -1 βk σ 2 σ 3 σ 4 = ∆ -1 (σ 2 σ 3 σ 2 σ 4 σ 3 δ 3 )(σ 1 σ 3 ) 2k-2 (σ 3 σ 4 ∆ 3 )(∆ 3 σ 4 ) 2 ( δ3 σ 4 )[(δ 3 σ 4 )( δ3 σ 4 )] k-2 (δ 3 σ 4 σ 3 σ 4 σ 2 σ 3 ). • For σ 2 σ 1 σ 3 σ 2 : (σ 2 σ 1 σ 3 σ 2 ) -1 βk σ 2 σ 1 σ 3 σ 2 = (σ 3 σ 4 σ 3 ∆ 3 )(σ 2 σ 4 ) 2k-2 (δ 3 σ 3 σ 4 σ 3 ) (σ 1 σ 4 σ 3 )[(σ 1 σ 3 σ 4 )(σ 1 σ 4 σ 3 )] k-1 .
• For σ 2 σ 1 σ 3 σ 4 :

(σ 2 σ 1 σ 3 σ 4 ) -1 βk σ 2 σ 1 σ 3 σ 4 = ∆ -1 (σ 2 σ 3 δ 3 σ 4 σ 3 )(σ 1 σ 3 ) 2k-2 (σ 3 σ 4 ∆ 3 )(∆ 3 σ 4 ) [(δ 3 σ 4 )( δ3 σ 4 )] k-1 (δ 3 σ 4 σ 3 σ 4 σ 2 σ 1 σ 3 σ 4 ).
We observe that the canonical length of σ -1

1 βk σ 1 , σ -1 2 βk σ 2 , (σ 2 σ 1 ) -1 βk σ 2 σ 1 , (σ 2 σ 3 ) -1 βk σ 2 σ 3 , (σ 2 σ 1 σ 3 ) -1 βk σ 2 σ 1 σ 3 , (σ 2 σ 3 σ 4 ) -1
βk σ 2 σ 3 σ 4 and (σ 2 σ 1 σ 3 σ 4 ) -1 βk σ 2 σ 1 σ 3 σ 4 is 4k, so that these elements are not in the SSS of βk , and a fortiori not in its SC.

As to σ -1 3 βk σ 3 and (σ 2 σ 1 σ 3 σ 4 ) -1 βk σ 2 σ 1 σ 3 σ 4 , they certainly are in the SSS, but they are not rigid, and so they cannot be in the SC, because if the SC contains one rigid element, then all its elements are rigid (see Corollary 11 in [START_REF] Gebhardt | The cyclic sliding operation in Garside groups[END_REF]). Now, Lemmas 2.6 and 2.7 allow us to conclude. Let us assume that there exists a braid α in the set of sliding circuits of βk which is not in O( βk ). According to Lemma 2.7, there is a sequence βk = α 1 , α 2 , . . . , α r , α r+1 = α of elements in the set of sliding circuits that verify the conclusions of the Lemma 2.7. Let i be the smallest index such that α 1 , . . . , α i are in O( βk ) and α i+1 is not. We denote by s the braid by which α i is conjugated to get α i+1 . According to Lemma 2.7, it is a simple braid which is a prefix of ι(α i ) or ∂φ(α i ).

Let α i = γ 0 , γ 1 , . . . , γ t = βk be the elements of O( βk ) such that γ j+1 is obtained from γ j by cycling (or, if necessary, γ t = ∆ -1 γ t-1 ∆). According to Lemma 2.6, the transport s (1) of s is a simple braid, prefix of ι(γ 1 ) or of ∂φ(γ 1 ). We define by induction s (j+1) = (s (j) ) (1) (or, if necessary, s (t) = ∆ -1 s (t-1) ∆). Still according to Lemma 2.6 (and, if necessary, to the fact that the conjugate by ∆ of a prefix of ι(x) is a prefix of ι(∆ -1 x∆)), for all j, s (j) is a prefix of ι(γ j ) or of ∂φ(γ j ). In particular, s (t) is a prefix of ι( βk ) or of ∂φ( βk ). So βk is sent by conjugation by s (t) to a braid that is not in its orbit O( βk ), since it is in the orbit of α i+1 . But this is impossible: according to the exhaustive case checking above, the conjugate of βk by a strict prefix of ι( βk ) or of ∂φ( βk ) is never an element of the set of sliding circuits, and the conjugates by ι( βk ) and ∂φ( βk ) themselves are elements of O( βk ).

Round reduction curves

We want to prove the following theorem Theorem 2.8. The braid βk (and thus also the braid β k , which is conjugated to it) is pseudo-Anosov.

First of all, it is easy to show the Lemma 2.9. The braid βk is not periodic.

Proof. If βk was periodic, one of its powers would be equal to a power of ∆. But βk is rigid with inf βk = 0, so the left normal form of a power of βk is directly obtained by juxtaposing that of βk the suitable number of times. It is then obvious that it is not a power of ∆.

It remains to prove that βk is not reducible. The following result (Corollary 4.3 in [START_REF] Gonzalez-Meneses | On reduction curves and Garside properties of braids, Topology of algebraic varieties and singularities[END_REF]) allows us to reduce to the case of round curves (i.e. homotopic to a circle): Proposition 2.10. For every reducible, non periodic braid x ∈ B n , there exists a conjugate of x in its SC that sends at least one round curve to a round curve.

Let us also state the following theorem of Bernadete, Gutierrez and Nitecki (Theorem 5.7 in [START_REF] Bernadete | Braids and the Nielson-Thurston classification[END_REF]) as given in [START_REF] Calvez | Dual Garside structure and reducibility of braids[END_REF] A corollary of this last result is that, if an element of the SC sends a round curve to a round curve, then so do the braids obtained by applying cyclings to it (and so do, of course, their conjugates by ∆). Now, according to Lemma 2.4, the SC is reduced to only one orbit under cycling or conjugation by ∆. Hence it suffices to show that βk does not send any round curve to a round curve: this will imply that no element of the SC sends any round curve to a round curve, and then, due to Proposition 2.10, that βk is not reducible.

Figure 3 shows all the essential round curves for a braid with 5 strings. Let us check that none of these curves is sent by βk to a round curve. Let us remark that, still according to Proposition 2.11, it suffices that a braid consisting of the first factors In particular, the canonical length of β k,i 1 ,...,i 2k-2 is 4k -1, and so this braid is in the super summit set. This normal form also allows us to observe that β k,i 1 ,...,i 2k-2 = β k,j 1 ,...,j 2k-2 if and only if i 1 = j 1 , . . . , i 2k-2 = j 2k-2 . The 2 2k-2 possible choices for (i 1 , . . . , i 2k-2 ) lead to 2 2k-2 distinct elements in the super summit set of β k .

a) b) c) d) e) f ) g) h) i)

Theorem 3 . 1 .

 31 Let k 1. The braid

Definition 1 . 1 (

 11 Mapping class group of the punctured disk). Let D n be the closed unit disk in C, with n punctures regularly spaced on the real axis. The mapping class group of D n , denoted MCG(D n ), is the group of the homeomorphisms of D n , modulo the isotopy relation. We also denote MCG(D n , ∂D n ) the group of the homeomorphisms of D n fixing pointwise the boundary ∂D n of D n , modulo the isotopy relation.

Lemma 2 . 2 . 3 Figure 1 :

 2231 Figure 1: Left normal form of the braid β .

2k - 2 2k - 2 Figure 2 : 2 . 3 .

 22223 Figure 2: The braid in normal form

  (Theorem 1):Proposition 2.11. Let x ∈ B n , seen as a mapping class in MCG(D n , ∂D n ), with left normal form x = ∆ p x 1 • • • x r . Let C be a round curve in D n . If x(C) is round, then ∆ p x 1 • • • x m (C)is round for all m = 1, . . . , r.

Figure 3 :

 3 Figure 3: All round curves for 5 strings

of βk transforms the round curve to a curve that is not round, in order to be sure that the final image is not round.

Let us check this explicitly for each of the round curves in Figure 3. After applying the first factor σ 1 σ 3 , only the images of the curves a), c), g) and h) are still round. These four are transformed into themselves, and so remain unchanged after applying (σ 1 σ 3 ) 2k-2 . The factor σ 3 σ 4 ∆ 3 transforms a) into b), whereas the images of c), g) and h) are no longer round. By ∆ 3 σ 4 , b) is again transformed into a), then applying the elements δ 3 σ 4 and δ3 σ 4 alternatively transforms a) into b) and b) into a). Finally, the last factor δ 3 σ 4 σ 3 σ 4 transforms a) into a curve that is no longer round.

After all, none of the round curves is preserved by βk . This concludes the proof of Theorem 2.8.

A lower bound for the cardinality of the super summit set

is pseudo-Anosov, and the cardinality of its super summit set is at least 2 2k-2 .

Proof. We have already seen in Section 2 that the braid is pseudo-Anosov.

Let α 11 = σ 1 , α 12 = σ 1 σ 2 , α 21 = σ 2 σ 1 and α 22 = σ 2 , so that for all i, j ∈ {1, 2}, S(α ij ) = {σ i } and F (α ij ) = {σ j }, where S(x) is the set of the generators σ l such that σ l x, and F (x) is the set of the σ l such that x σ l . If we choose a sequence of elements i 1 , . . . , i 2k-2 ∈ {1, 2}, we denote

On the one hand, the simple braids δ 3 σ 4 σ 3 σ 4 and σ 3 σ 4 α 1i 1 are left-weighted, and this is also the case for σ 3 σ 4 α 1i 1 and σ 4 α i 1 i 2 , for σ 4 α i 1 i 2 and σ 4 α i 2 i 3 , etc. On the other hand, we can calculate the left normal form of (α

, seen as a braid with 3 strings: the left normal form of a braid can be easily expressed in terms of its inverse (see [START_REF] Elrifai | Algorithms for positive braids[END_REF]). That of (α 1i

). Moreover, ∂ -1 (α 1i 1 )σ 4 = ∆ 3 α 1i 1 σ 4 and δ 3 σ 4 σ 3 σ 4 are left-weighted. From this, we deduce the left normal form of β k,i 1 ,...,i 2k-2 :


Nicolas Basset

Eugene Asarin
email: asarin@liafa.jussieu.fr

Thin and thick timed regular languages

.

Introduction

Timed automata [START_REF] Alur | A theory of timed automata[END_REF] using exact continuous clocks, exact guards and resets are a beautiful mathematical object and a useful model of real-time systems. However, from the very beginning of the timed automata research, it was clear that they are in several aspects too precise, which leads sometimes to strange artifacts, mathematical pathologies or unrealistic models. Several lines of research have partially elucidated these issues.

Thus, the state space of a timed automaton being infinite, some long (or infinite) runs never revisit the same state. For this reason, as stated in [START_REF] Beauquier | Pumping lemmas for timed automata[END_REF], usual pumping lemmata do not hold, and should be replaced by rather involved analogues. In a run, infinitely many events can happen during a finite amount of time, or two events can happen again and again with the time interval between them tending to 0. Such a run reminds of Zeno's aporias and is often called a Zeno run, see [START_REF] Gómez | Efficient detection of Zeno runs in timed automata[END_REF] and reference therein. Pathological runs do not support well discretization of clocks, see [START_REF] Henzinger | What good are digital clocks?[END_REF][START_REF] Asarin | On discretization of delays in timed automata and digital circuits[END_REF].

In order to rule out bad behaviors, restricted classes of timed automata and alternative semantics were considered by several authors. Thus, in [START_REF] Gupta | Robust timed automata[END_REF][START_REF] Henzinger | Robust undecidability of timed and hybrid systems[END_REF], a tube language semantics is introduced. In [START_REF] Puri | Dynamical properties of timed automata[END_REF] a robust semantics, based on small imprecisions is considered. It reappears in a different flavor as implementability, see [START_REF] Wulf | Almost ASAP semantics: from timed models to timed implementations[END_REF][START_REF] Wulf | Robust safety of timed automata[END_REF], and in another version in [START_REF] Abdulla | Sampled semantics of timed automata[END_REF].

With the same objective to rule out bad behaviors, restrictions are often put on all the cycles in the automaton, by requiring that each cycle takes at least one time unit (strongly non-Zeno condition), or resets all the clocks (progress cycle condition), or even resets all the clocks at one and the same transition (regeneration or synchronization condition).

In this paper, we propose a unifying approach to most of these issues for deterministic timed automata. We classify each automaton either as thin or as thick (the classification is decidable).

In thin automata all the infinite trajectories, are, in some weak sense Zeno; the digitization of long trajectories is difficult, since it requires very small discretization step. In thick automata most of trajectories are non-Zeno, behave well under digitization and satisfy a sort of pumping lemma.

The main technical tool used to characterize thin and thick timed languages is their (volumetric) entropy introduced in [START_REF] Asarin | Volume and entropy of regular timed languages: Analytic approach[END_REF][START_REF] Asarin | Volume and entropy of regular timed languages: Discretization approach[END_REF]. Let us briefly recall this notion: a timed language L, for a given number of events n, can be seen as several polytopes in IR n , their total volume is denoted by V n . In most cases, for n → ∞ this volume behaves exponentially: V n ≈ 2 nH . The growth rate (i.e. H) is referred to as entropy, and characterizes the size and the information contents of the timed language. With the notion of entropy, the definition of thin and thick languages is simple: a language is thin if its entropy equals -∞ (that is the volume V n decays faster than any exponent), and thick otherwise.

We identify a novel notion of a forgetful cycle, that is a cyclic path allowing forgetting the clock values. We state that any path in a timed automaton which is thick and long (in some precise sense), necessarily contains a forgetful cycle (Thm. 1), which can be seen as a weak version of pumping lemma. Based on this pumping lemma, we obtain our first main result (Thm. 2): thickness of a language is equivalent to many other nice properties briefly described above (good discretization, existence of forgetful cycle etc.).

The proof of Thms. 1-2 is rather technical, and uses together with "timed" techniques inspired by [START_REF] Puri | Dynamical properties of timed automata[END_REF][START_REF] Abdulla | Sampled semantics of timed automata[END_REF], the monoid version of Ramsey theory, namely Simon factorization forests [START_REF] Simon | Factorization forests of finite height[END_REF].

The thin-thick alternative leads to a more precise analysis of a timed automaton when applied to its strongly connected components. In general, a timed automaton can be decomposed into several strongly connected components (some of them are thin, others thick) and acyclic pathways between them. We show that most of the long enough runs spend most of the time in thick components, and only few pathological runs wander in thin components (Thm. 3).

Finally, we apply the thin-thick alternative to the analysis of entropy of timed languages. In [START_REF] Asarin | Volume and entropy of regular timed languages: Discretization approach[END_REF] it was shown that the entropy of a timed language can be lower and upper bounded using entropies of two discrete languages L - ε and L + ε , corresponding to a shrunk and a bloated discretizations of L: h(L - ε ) + log(ε) ≤ H ≤ h(L + ε ) + log(ε).

Here (Thm. 4) we strengthen this result and establish that on a thick component the entropy of a timed language can be approximated with a good precision using the entropy h(L ε ) of the discretized language:

H = h(L ε ) + log(ε) + o(1).
As a corollary we obtain a converging algorithm allowing computation of H for any timed regular language with any precision required. This answers the open question from [START_REF] Asarin | Volume and entropy of regular timed languages: Discretization approach[END_REF]: H is always a computable real number.

Paper organization. In Sect. 2, we recall some basic definitions, define thin and thick languages and give some motivating examples. In Sect. 3 we describe three more involved constructions: polytopes associated to paths in timed automata as in [START_REF] Maler | On recognizable timed languages[END_REF], region split automaton as in [START_REF] Asarin | Volume and entropy of regular timed languages: Analytic approach[END_REF] and monoid of orbit graphs inspired by [START_REF] Puri | Dynamical properties of timed automata[END_REF]. In the central Sect. 4 we state the thin-thick alternative for timed automata and a sort of pumping lemma for thick automata (Thm. 1). In Sect. 5 we apply these results to entropy of timed languages. We conclude with some perspectives in Sect. 6.

Preliminaries

Timed languages and their measures

A timed word α = (t 1 , a 1 ) . . . (t n , a n ) is a word on the alphabet IR + × Σ where Σ is a finite alphabet of events. Times t i represent delays between events a i-1 and a i . Throughout this paper, delays will be bounded3 by an integer constant M . We will sometimes write the same timed word α as (t, w) with t ∈ [0, M ] n and w ∈ Σ n . A timed language L is a set of timed words. We will denote by L n the language L restricted to words of length n.

Volume and volumetric entropy. Let L be a timed language. For each word of events w ∈ Σ n , let L(w) be the set {t ∈ [0, M ] n | (t, w) ∈ L}. This subset of IR n has a volume4 (Lebesgue's measure) denoted by Vol(L(w)). The volume of L n is Vol(L n ) = w∈Σ n Vol(L(w)). Bounding the delays by M leads to a volume bounded by (|Σ| M ) n . In this paper, we will work with factor closed languages5 , i.e. such that if (t 1 , a 1 ) . . . (t n , a n ) ∈ L then for all 1 ≤ i ≤ j ≤ n (t i , a i ) . . . (t j , a j ) ∈ L. For each couple of words w 1 , w 2 ∈ Σ * the language inclusion L(w 1 • w 2 ) ⊆ L(w 1 )L(w 2 ) holds, and then Vol(L(w 1 • w 2 )) ≤ Vol(L(w 1 ))Vol(L(w 2 )). The volumetric entropy of a timed language is a number in [-∞, +∞) defined as

H(L) = lim n→+∞ 1 n log 2 (Vol(L n )).
The limit (finite or -∞) exists due to subadditivity of log 2 Vol(L n ) wrt n and is upper bounded by log 2 (|Σ| M ). A timed language L is called thin if H(L) = -∞ ant thick otherwise.

To deal with finite objects, one can discretize all the previous continuous languages. Given

an ε = 1 N , (N ∈ IN) called discretization step, let us define L ε,n = L n ∩ (εIN × Σ) n , i.e. the set of words in L n with all delays multiple of ε, L ε = n∈IN L ε,n , L ε (w) = L(w) ∩ (εIN) n . The ε-entropy h ε is defined as h ε (L) = lim n→∞ 1 n log 2 (|L ε,n |).
We will relate the discrete entropy h ε to the continuous one H in Sect. 5.

Open, closed and punctual languages. A language is said to be open if for all n, the set L n is an open subset (for the product topology) of IR n × Σ n . In other words, L n should be a finite union of O × {w} where w is a word of events and O an open subset of IR n . Interior and closure of L, denoted int(L) and L are defined in a natural way.

Taking closure or interior of a finite union of polytopes of IR n has no effect on its volume. Nevertheless the number of discrete points can drastically change if punctuality is allowed (see [START_REF] Asarin | Two size measures for timed languages[END_REF]). We call a language to be punctual if int(L) = L.

Timed automata and their languages

Clocks, zones and regions. Let X be a finite set of variables called clocks. Clocks have non negative values bounded by a constant M c . A rectangular constraint is a formula of the form x ∼ c where x ∈ X, c ∈ IN, ∼∈ {≤, <, =, >, ≥}. A diagonal constraint is a formula of the form xy ∼ c where x, y ∈ X. A guard is a finite conjunction of rectangular constraints. We denote by G the set of all guards. A zone is a set of clock vectors x ∈ [0, M c ] X satisfying a finite conjunction of rectangular and diagonal constraints. A region is an inclusionminimal zone. A region (which is always a simplex) is uniquely defined by a point with integer coordinates ⌊x⌋ ∈ {0, . . . , M c } X giving integer part of clocks and an order on the fractional part of clocks 0

∼ 0 {x i1 } ∼ 1 {x i2 } ∼ 2 • • • ∼ |X| 1
where ∼ 0 , . . . , ∼ |X| ∈ {<, =}. The closure of a region (abusively called closed region) can be obtained by replacing < by ≤ and > by ≥ in its definition.

Timed automata. A timed automaton is a tuple (Q, X, Σ, E, L, I, F ) with Q a finite set of locations; X a set of bounded clocks; E ⊆ Q × G × 2 X × Q a finite set of edges; L : E → Σ a labeling function on edges; I ⊆ Q × [0, M c ] X the set of initial states; F ⊆ Q × [0, M c ] X the set of final states.
By default all the states (elements of Q × [0, M c ] X ) are initial and final, otherwise they are given by union of zones.

The clocks grow with the same (unit) speed and some of them are reset to 0 when passing through an edge. More formally, there is a transition

(q, x) (t,a)
---→ (q ′ , x ′ ) if there is an edge e = (q, g, R, q ′ ) ∈ E with L(e) = a such that x + (t, . . . , t) satisfies the guard g and for each clock x ∈ X, its new value x ′ = 0 iff x ∈ R, or x ′ = x + t otherwise. A run on the timed word α = (t 1 , a 1 ) . . . (t n , a n ) is a sequence of consecutive transitions (q 0 , x 0 )

(t1,a1) ----→ (q 1 , x 1 ) • • • (tn,an)
----→ (q n , x n ), where x 0 , . . . , x n ∈ [0, M ] X , q 0 , . . . , q n ∈ Q. A timed word is recognized by the automaton if there exists a run on it from an initial state to a final state. The timed language L(A) consists of all the recognized words. We will be interested in its entropy H(L(A)), that will be abusively denoted H(A).

We call a TA right resolving if any two edges leaving the same location and having the same label have disjoint guards. Adding the condition that there is only one initial state gives the usual definition of determinism. In the rest of the paper, we work with right resolving TA.

Paths and reachability relation. We call a path in an automaton any sequence of edges. The "useful" paths are sequences of consecutive edges (such that the starting location of the (i + 1) th edge is the ending one of the i th ), but we allow arbitrary words of E * and all objects associated to a non-consecutive sequence will be empty.

Given two clock vectors x, x ′ , a path π ∈ E n and a sequence of delays of the same length t = (t 1 , . . . , t n ), we write that x t,π --→ x ′ whenever exists a run in the automaton of the form (q 0 , x)

(t1,a1) ----→ (q 1 , x 1 ) • • • (tn,an)
----→ (q n , x ′ ) following the sequence of edges π.

Several objects are naturally associated with a path. Given a path and two clock vectors, a language (a polytope of all the timings of the path) can be defined:

L(π, x, x ′ ) = {t | x t,π --→ x ′ }. If we are not interested in clock values,
we get a polytope depending only on the path:

L(π) = {t | ∃x, x ′ , x t,π --→ x ′ }.
The other way around, if we do not care about timing, we get the reachability predicate:

Reach(π) = {(x, x ′ ) | ∃t, x t,π --→ x ′ }.
A path π ∈ E n is said to be punctual if L(π) is not empty but has dimension less than n. The closure (resp. interior) of a path π denoted by π (resp. int(π)) is the path obtained from π by taking closure (resp. interior) of all guards of edges in π (i.e. changing strict inequalities in non-strict ones (resp. vice versa)). There is a limit cycle (resp. strong limit cycle) along π if there exists a clock vector x and time sequence t such that x t,π --→ x (resp. x t,int(π) -----→ x). Given ε > 0, in ε-discrete limit cycles all the components of x and t should be multiple of ε.

Thinness, simplices and examples

Our analysis of thin languages will start with a simple observation that the volume of k-dimensional simplices tends to 0 faster than any exponent: Lemma 1. The volume of a simplex of "type 1" described by inequalities 0 ≤

t 1 + • • • + t k ≤ 1, t i ≥ 0 or of a simplex of "type 2" described by inequalities 0 ≤ t 1 ≤ • • • ≤ t k ≤ 1 is 1 k! . x ≤ 1 a, x ∈ [0; 1] p 0 ≤ x ≤ 1 y = 0 q 0 ≤ y ≤ 1 x = 0 a, x ∈ [0; 1]/x := 0 b, y ∈ [1; 2]/y := 0 p 0 ≤ x ≤ 1 y = 0 q 0 ≤ y ≤ 1 x = 0 a, x ∈ [0; 1]/x := 0 b, y ∈ [0; 1]/y := 0 x, y ∈ [0, 1]
a, x ∈ [0; 1], y := 0 a, y ∈ [0; 1], x := 0 Fig. 1. First row: thin automata A1, A2. Second row: thick ones A3, A4. Initial states are given by conditions in nodes By change of coordinates the lemma can be extended to more general polytopes:

Corollary 1. Let P be a subset of {t 1 , . . . , t n | 0 ≤ t i ≤ M }.
If there exists a subsequence of indices s(1), . . . , s(k) of 1, . . . , n and new coordinates u s(i) func-

tions of t s(1) , . . . , t s(i) with 0 ≤ u s(1) ≤ u s(2) ≤ • • • ≤ u s(k) ≤ 1 and ∂u s(i) ∂t s(i) ≥ 1 then Vol(P ) ≤ M n-k
k! . The automata on Fig. 1 illustrate the concepts of thin and thick. L n (A 1 ) = {t 1 , . . . , t n | i≤n t i ≤ 1} is a simplex of type 1, and thus L(A 1 ) is thin. L n (A 2 , q) = {t 1 , . . . , t n | ∀i, t 2i + t 2i+1 ≤ 1 ∧ t 2i+1 + t 2i+2 ≥ 1}, by interchanging even and odd indices we obtain L n (A 2 , p). Posing u 2i+1 = 1t 2i+1 and u 2i = t 2i yields a simplex 0 ≤ u 1 ≤ . . . u n ≤ 1. This change of coordinates preserves volume and so Vol(L n (A 2 , q)) = 1 n! . This is an example of automaton satisfying the progress cycle condition (i.e. resetting all clocks along each cycle) and nevertheless thin.

Third and fourth examples are thick, their entropies can be computed symbolically because they are 1 1 2 clock (see [START_REF] Asarin | Volume and entropy of regular timed languages: Analytic approach[END_REF]), they are respectively log 2 2 π and log 2 log 2 (e). Note that A 4 does not satisfy the progress cycle condition.

3 More on paths and cycles

Region graph and state split automata

Timed variants of the region graph [START_REF] Alur | A theory of timed automata[END_REF] are extensively used in the literature. Here we use so-called region-split automaton given in [START_REF] Asarin | Volume and entropy of regular timed languages: Analytic approach[END_REF], add several new conditions and modify those concerning initial states. A timed automaton is in region-split form if B1. For every location q ∈ Q a unique region r q (called its entry region) exists, such that the set of clock values with which q is entered is exactly r q . B2. The guard g of every transition δ = (q, g, R, q ′ ) ∈ E is just one region. B3. All the states of entry regions (and only these states) are both initial and final. B4. For any location there exists a path leading to some cycle and a path coming from some cycle. B5. For every transition δ its guard g has no constraints of the form x = c in its definition. B6. The labeling function on edges is identity (and so every two distinct edges have different labels).

0 ≤ x ≤ 1 y = 0 0 ≤ y ≤ 1 x = 0 a1, y ∈ [0; 1]/x := 0 b1, x ∈ [0; 1]/y := 0 b2, x ∈ [0; 1], y := 0 a2, y ∈ [0; 1], x := 0
Proposition 1. Given a right resolving TA A with bounded clocks and all states initial and final, one can construct an automaton RS(A) called the region-split automaton of A which satisfies B1 -B6 and such that H(RS(A)) = H(A).

In the following, we replace w.l.o.g. for the computing of H, A by RS(A) obtained from RS(A) by taking non-strict inequalities instead of strict ones.

Proposition 2. For region split automata:

words, paths, and region paths are in natural bijection; -volume of any path is less or equal to 1; -every path of consecutive edges has a non empty and non punctual language.

As for our running examples, A 1 , A 2 , A 3 are already region split automata. RS(A 4 ) is depicted in Fig. 2.

Paths and polytopes

Let us describe languages associated with paths as polytopes in IR n , following [START_REF] Maler | On recognizable timed languages[END_REF].

Contiguous polytopes. Let T n = {t 1 , . . . , t n } be an ordered set of real variables bounded by M. A sum S j..k = k i=j t i is called a contiguous sum (of length k -j + 1). A temporal inequality is a constraint of the form S j..k ∈ [A, B] where A, B ∈ IN, A ≥ 0 and B ≤ M . A contiguous polytope is a bounded subset of
IR n which is composed by all the points satisfying a conjunction of temporal inequalities. We say that the polytope is d-contiguous if the length of all sums in the inequalities is bounded by d.

Proposition 3. For each path π ∈ E * , L(π) is a contiguous polytope.

The inequality

k i=j t i ∈ [A, B] comes from testing the guard x ∈ [A, B]
during the k th transition, provided that the last reset of x took place in the j th transition. The subclass of d-contiguous polytopes corresponds to automata with progress cycle condition, where the number of transitions between two resets is bounded by d.

Given a polytope P, we denote by N P its N -fold dilated copy, i.e. {N t | t ∈ P} and by E(P) = P ∩ Z Z n the set of points with integer coordinates in P. A contiguous polytope is said to be N -fat if there exists an integer point in the interior of N P (called an internal point ): E(int(N P)) = ∅.

Point to point reachability: algebraic characterization

In this section, we characterize the relation Reach(π) in terms of an algebraic object: monoid of orbit graphs. Our analysis is less detailed than those in [START_REF] Comon | Timed automata and the theory of real numbers[END_REF][START_REF] Dima | Computing reachability relations in timed automata[END_REF][START_REF] Krcál | Infinite Structures in Timed Systems[END_REF] and follows the lines of [START_REF] Puri | Dynamical properties of timed automata[END_REF].

For a closed region r, let us denote by V (r) = {S 1 , . . . , S p } its vertices. Any point x in the region is uniquely described by its barycentric coordinates λ 1 , . . . , λ p , i.e. nonnegative numbers such that

p i=1 λ i = 1; x = p i=1 λ i S i .
Given two regions r and r ′ , we call orbit graph any graph G with vertices V (r) V (r ′ ) if r and r ′ are different and V (r) otherwise, and with edges going from V (r) to V (r ′ ). Informally, an edge from S to S ′ means that the clock vector at the vertex S can reach the clock vector at S ′ along some transition or path.

Orbit graphs compose in the natural way: for G 1 on regions r 1 and r ′ 1 , and G 2 on regions r 2 and r ′ 2 , their product

G = G 1 • G 2 is defined if r ′ 1 = r 2 .
In this case, G is an orbit graph on r 1 and r ′ 2 . There is an edge from S to S ′′ in G if and only if there exists S ′ such that (S, S ′ ) and (S ′ , S ′′ ) are edges of G 1 and G 2 . Whenever r ′ 1 = r 2 , we put G 1 • G 2 equal to some special (absorbing) element 0. The set G of orbit graphs, augmented with 0 and a neutral element 1 has a structure of finite monoid.

An orbit graph G can be represented by its adjacency matrix M of size |V (r)| × |V (r ′ )|. Products in the monoid of orbit graphs are easy to compute using matrices:

M (G 1 G 2 ) = M (G 1 ) ⊗ M (G 2 ) where the "product" ⊗ is defined by (A ⊗ B) ij = max k min(A ik , B kj ).
There exists a natural morphism γ : E * → G from paths to orbit graphs defined as follows. For a transition e between r and r ′ , we define the orbit graph γ(e) on r and r ′ with edges {(S,

S ′ ) ∈ V (r) × V (r ′ ) | ∃t, S (e,t)
---→ S ′ }. For a path π = e 1 . . . e n , we define γ(π) = γ(e 1 ) . . . γ(e n ) (it will be called the orbit graph of the path π). For the empty path we have γ(ε) = 1, and for any non-consecutive path γ(π) = 0.

For example, the orbit graphs of cycles ab and ba of A 3 and A 4 are complete, the orbit graphs of the other running examples are given in Fig. 3.

The orbit graph is crucial for reachability analysis.

Proposition 4. The orbit graph of a path γ(π) determines its reachability relation Reach(π). In particular, γ(π)

is complete iff Reach(π) = r × r ′ , or equiv- alently iff Reach(int(π)) = r × r ′ .
The proof of the first criterion is based on the following remarkable characterization of Reach(π) in terms of the orbit graph due to Puri [START_REF] Puri | Dynamical properties of timed automata[END_REF].

Lemma 2. 6 Let x and x ′ be two clock vectors with barycentric coordinates λ and λ ′ . Then (x, x ′ ) ∈ Reach(π) iff there exists a stochastic matrix P M (γ(π)), such that λP = λ ′ .

Here matrix "inequality" A B means that B ij = 0 ⇒ A ij = 0 for all i, j.

Adding clock resets. For future use, we must enrich the monoid of orbit graphs by adding information on clock resets. Elements of the monoid M are couples (orbit graph, subset of clocks) (and also, as before, two special elements 0, 1), the product rule is:

(G 1 , X) • (G 2 , Y ) = (G 1 • G 2 , X ∩ Y ), if G 1 • G 2 = 0 0, otherwise.
For each π ∈ E * we denote by ν(π) the set of clocks not reset along the path π.

We define a morphism µ : E * → M as follows:

µ(π) = (γ(π), ν(π)).
Idempotents. An idempotent of a monoid is an element m such that m • m = m. Every finite monoid contains an idempotent. In our case, an idempotent orbit graph is always associated to a cyclic path, it is a graph G equal to its transitive closure

G + = ∪ n∈IN + G n .
4 The thin-thick alternative and its consequences

In this central section, we characterize thin and thick paths and languages, based on a new notion of a forgetful cycle.

Forgetful cycles, and the others

After reading a timed path π × t from a state s 0 , the reached state s depends only on s 0 and on the delays t. We will say that π is forgetful if s and s 0 are independent, i.e. all the following equivalent conditions hold:

Reach(int(π)) = r × r ′ , Reach(π) = r × r′ , γ(π) is complete.
If a cycle is non-forgetful, and moreover its orbit graph is not strongly connected, then it is possible to find a linear Lyapunov function: Lemma 3. For a cycle π, if γ(π) is not strongly connected then there exists a non empty I {1, . . . , p} such that i∈I λ ′ i ≤ i∈I λ i whenever (x, x ′ ) ∈ Reach(π), where λ and λ ′ stand for barycentric coordinates of x and x ′ .

In this lemma, as before, {1, . . . , p} are indices of the vertices of the region where π starts (and ends).

In fact I corresponds to an initial strongly connected component (SCC) of the orbit graph, i.e. an SCC without incoming edges from other SCC. According to the lemma, the state moves from the facet spanned by I towards other vertices of the region and cannot come back.

Comparing to other types of cycles. Two other kinds of cycles are often considered in the literature: in a progress cycle each clock should be reset at some edge; in a synchronizing cycle all the clocks are reset along one and the same edge of the cycle.

Proposition 5. progress cycles forgetful cycles synchronizing cycles.

A remark is in order, in most works using progress or synchronizing cycles, all the cycles are required to be like that. In our work, existence of a forgetful cycle appears naturally in "non degenerate" (i.e. thick) automaton.

The condition of progress cycle can be seen as a weaker kind of forgetting: the state after such a cycle is exactly determined by the delays (see following lemma). Nevertheless the orbit graph of a progress cycle can be not strongly connected (e.g. cycle ab of A 2 depicted in Fig. 3); in that case starting states and ending states are still dependent. Lemma 4. If all clocks have been reset during reading of π × (t 1 , . . . , t m ) then for all non empty I {1, . . . , p}, there exists α 1 . . . α m ∈ {-p, . . . , p} and an integer constant C such that i∈I λ i = C + m j=1 α j t j . Moreover one of the α j is not zero.

Pumping lemma for long thick paths

For a given real η > 0, we say that a path π is η-thick if Vol(L(π)) ≥ η |π| . The following "pumping lemma" will play the key role in characterization of thick languages below and can be interesting by itself.

Theorem 1. For every timed automaton A and every η > 0, there exists N η such that any η-thick path longer than N η contains a forgetful cycle.

The rest of this section is devoted to the proof of this result.

Elements of the monoid M associated to forgetful cycles will be referred to as forgetful, they are idempotent. We will first see how repeating a non forgetful idempotent induces a subexponential volume (like the simplex example), then we will use Simon's theorem on factorization forests to factorize paths and find some repeated idempotent. Absence of forgetful cycles in a path will then imply thinness. Proposition 6. Let π 1 , . . . , π k be k cycles of E * such that µ(π 1 ), . . . , µ(π k ) are all equal to a same non forgetful idempotent of M, then Vol(L(π

1 . . . π k )) ≤ M n-k k! where n = |π 1 | + • • • + |π k |.
Proof. If G is an idempotent orbit graph (thus equal to its transitive closure), G is complete if and only if G is strongly connected. Thus we will distinguish two disjoint kinds of non forgetful idempotents, those associated to non progress cycles and those associated to progress cycles with non strongly connected orbit graphs. In the former case a clock is not reset all along the path π 1 . . . π k , thus L(π 1 . . . π k ) is in a simplex of type 1 and the volume satisfies the inequality to prove. In the latter case, we use Lem. 3,4, and Cor. 1.

⊓ ⊔

A factorization forest of a word π is an unranked labeled tree with leaves labeled by the letters of π, with root labeled by π and with two types of internal nodes:

binary node labeled by a word π 1 • π 2 with two children labeled by the words π 1 and π 2 ; -idempotent node labeled by a word π 1 . . . π k with all µ(π i ) equal to a same idempotent and with children labeled by the words π 1 , . . . , π k .

Theorem (Simon [20]). If µ is a morphism from E * to a finite monoid M, then every word admits a factorization forest of height at most h(M) = 9|M|.

We suppose that there are no forgetful cycles on a long path π and consider its factorization forest of height at most h(M). When its length n grows up, the number of leaves also grows and since the height is bounded, branching of nodes must get larger and larger. These hugely branched nodes are idempotent and satisfy hypotheses of Lem. 6, thus their volume is very small, which implies that Vol(L(π)) is also small. The Prop. 7 below quantifies this "smallness" of Vol(L(π)) as function of the length of π and height of its factorization forest, and Thm. 1 follows immediately from this proposition.

Let LVol be the function defined on paths by LVol(π) = log 2 Vol(L(π)). This function is subadditive and non-positive, i.e. LVol(π 1 • π 2 ) ≤ LVol(π 1 ) + LVol(π 2 ) ≤ 0. Let L(n, h) be the maximum of LVol(π) over paths π of length n that do not contain forgetful idempotents and admit a factorization forest of height at most h. Proposition 7. For any height h, for any C < 0, there exists N h,C ∈ IN such that for all n > N h,C the inequality L(n, h) ≤ Cn holds.

Proof. We will define N h,C by induction on the height h. Let a be a factorization forest of height h with n leaves. We consider all the children of the root and their subtrees (all these subtrees have heights ≤ h -1), and distinguish two disjoint cases:

1. There are more than k = n 2N h-1,2C subtrees having less than N h-1,2C leaves. 2. There are less than k = n 2N h-1,2C subtrees with less than N h-1,2C leaves. Here the juicy part (sons with enough leaves to satisfy induction hypothesis) has more than n 2 leaves.

In the first case: root is an idempotent node and we can apply Lem. 6:

LVol(π) ≤ (n -k) log 2 (M ) -log 2 (k!) ≤ nC for n large enough.
In the second case:

LVol(π) ≤ k i=1 L(n i , h i ) ≤ ni≥N h-1,2C L(n i , h i ).
We apply the induction hypothesis:

LVol(π) ≤ 2C ni≥N h-1,2C n i ≤ 2C n 2 ≤ nC (recall that C is negative). ⊓ ⊔
To conclude the proof of Thm. 1, given η > 0, let C = log 2 η and h = h(M) the bound on height of factorization forest. Using Prop. 7, we obtain that a path longer than N h,C without forgetful idempotents cannot be η-thick. ⊓ ⊔

Characterizing thick languages

We are ready to describe thick languages now.

Theorem 2. For a right resolving timed automaton in region split form the following conditions are equivalent and define thick languages:

1. H > -∞; 2. there exists a forgetful cycle; 3. there exists a strong limit cycle; 4. there exists an ε-discrete strong limit cycle with ε > 0.

Equivalence between 3 and 4 can be found in [START_REF] Krcál | Infinite Structures in Timed Systems[END_REF]. 2 ⇒ 3 is straightforward.

Proof of 4 ⇒ 1. There exist q 0 , . . . , q d-1 , x 0 , . . . , x d-1 , π ∈ E d , u 1 , . . . , u d ∈ {ε, 2ε, . . . , M -ε} such that (q 0 , x 0 ) (u1,w1)

-----→ (q 1 , x 1 ) . . .

(u d ,w d )
-----→ (q 0 , x 0 ) along π and all the x i are not on the frontier of regions and have discrete coordinates. First we can see that all clocks have been reset at least once because any nonreset clock would augment during the run, which contradicts its cyclicity. Then for each n ∈ IN * the language L(π n ) is a d-contiguous polytope with equation of the form A ≤ k i=j t i ≤ B. Extending u periodically permits to have a word in

L(π n ) such that A + ε ≤ k i=j u i ≤ B -ε. Taking t i ∈ [u i -ε d , u i + ε d ] defines a hypercube included in L(π n ) whose volume is therefore greater than ( 2ε d ) nd . Then H(A) ≥ log 2 2ε d > -∞. ⊓ ⊔ Proof of 1 ⇒ 2.
We notice first that a thick language contains long thick paths.

Lemma 5. If H > -∞, there exists η > 0 such that for all n big enough, there exists an η-thick path of length n.

Proof. Let β = 2

Thin and thick SCC

The theory developed above can be refined using a decomposition of A into strongly connected components (SCC) A 1 , A 2 , . . . , A k .

Proposition 8. Volumetric entropy of A equals the maximal volumetric entropy of its SCC. In particular, A is thin iff so are all the subautomata A i .

It is easy to see that long and thick paths spend most of the time in thick SCC.

Theorem 3. For every timed automaton A and every η, α > 0, there exists N η,α such that for any η-thick path of length n > N η,α at most nα states belong to thin SCC.

Entropies of thick languages

In this section, we apply the results of the previous section to show that in thick automata, volumes and entropies can be computed with a good precision using discretization.

Theorem 4. For a thick strongly connected automaton A in region split form, the discrete and the volumetric entropies are related as follows 7 :

h ε = log 2 1 ε + H + o(1). 7 It can be proved that o(1) is in fact O ε 1/3 log 2 1 ε 2/3 .

Proof (≥ direction).

To bound the volume of L n by the number of discrete points, we will use a beautiful theorem on counting points in polytopes:

Theorem (Ehrhart, see [START_REF] Beck | Computing the continuous discretely: Integer-point enumeration in polyhedra[END_REF]). For integer N and an integer polytope P ⊂ IR n (i.e. whose vertices have integer coordinates), the number of integer points |E(N P)| is a polynomial in N with non negative coefficients of degree n and whose coefficient of the highest degree is the volume.

We deduce directly from this theorem that for each path π of length n and ε = 1) is more involved, and we give only a sketch of proof. We fix several integer parameters: a, b, c, d, e (they have to be adjusted in order to obtain the required estimate). Let π be a path of a length n > a. At every b transitions, we insert in π a forgetful cycle of length c (it exists by virtue of Thm. 2, and can be made of the same fixed length everywhere for an appropriate choice of c). Thus we obtain a slightly longer path π ′ (its length is n ′ ≈ n(1 + c/b)), satisfying two additional conditions:

every clock is reset at least every 2d transitions (and thus L(π ′ ) is 2dcontiguous polytope); -the polytope L(π ′ ) is e-fat.

We have three inequalities:

1. The first one:

|L ε (π)| ≤ |L ε (π ′ )|
can be proved by constructing an injection from the left-hand side discrete language to the right-hand side one. 2. We choose ε ′ slightly smaller than ε (another parameter to adjust) and consider the polytope L -obtained from L(π ′ ) by pushing all its facets inside by the amount δ = ε ′ d8 . Using fatness of L(π ′ ), it is possible to build an injection from its ε-discrete points to ε ′ -discrete points of L -(the latter is a bit smaller but its discrete points are slightly denser).

|L ε (π ′ )| ≤ L - ε ′ .
3. Taking an ε ′ -cube at every ε ′ -discrete point of L -, we get a set included in L(π ′ ) (this requires 2d-contiguity of L(π ′ )). Passing to volumes we conclude that

ε ′ n ′ L - ε ′ ≤ Vol(L(π ′ )).
Combining the three inequalities we get:

|L ε (π)| ≤ ε ′-n ′ Vol(L(π ′ )) ,
and with an appropriate choice of parameters, ε ′ and n ′ can be made very close to ε and n. Summing up over π and taking lim n→∞ 1 n log 2 in the previous inequality, we obtain the required result.

⊓ ⊔ Corollary 2. For right resolving TA with bounded clocks, H(A) is computable as function of A. Consequently, H(A) is a computable real (i.e. one can compute its approximation with any wanted precision).

Proof. First compute RS(A). Then compute by fixpoint method the submonoid of orbit graphs γ(E * ) ⊂ G and see whether there is a complete graph. If there is none, the automaton is thin and H = -∞. Otherwise, the automaton is thick and it just remains to compute the discrete entropy of L ε (RS(A)) for the wanted precision (similarly to [START_REF] Asarin | Volume and entropy of regular timed languages: Discretization approach[END_REF]). ⊓ ⊔

Conclusion and future work

We have identified the class of thick timed automata (those with non-vanishing language volume). Most runs in such automata are thick and exhibit a nice behavior, they spend most of the time in thick strongly connected components (Thm. 3) and visit from time to time forgetful cycles (Thm. 1). Thick runs are captured (both qualitatively and quantitatively) by ε-discretized automata.

We believe that the notions of thick languages and forgetful cycles will be useful in the operator approach to volume and entropy of [START_REF] Asarin | Volume and entropy of regular timed languages: Analytic approach[END_REF] and will imply some good properties of operators associated to these forgetful cycle. Similarly, we believe that thickness hypothesis is exactly what is needed for the analysis of probabilistic timed systems in the spirit of [START_REF] Carnevali | State-density functions over DBM domains in the analysis of non-Markovian models[END_REF] but for an unbounded time horizon. Another direction of future work is to extend the thin-thick dichotomy to the case of punctual paths and to find when the two size measures of [START_REF] Asarin | Two size measures for timed languages[END_REF] are defined. We hope also to relate thinness with the notion of mean topological dimension [START_REF] Lindenstrauss | Mean topological dimension[END_REF]. In the verification context, we believe that when analyzing a thick timed automaton, it suffices to check that the thick paths satisfy the specification, while thin ones can violate it.

A Proofs and minor results

A.1 Region split automaton

We assume w.l.o.g. that there is a special clock T in the automaton A to be split with a trivial behavior: in every transition, guards are of the form 0 ≤ T ≤ M and T is reset at each transition.

The volume of a path in the region split automaton is less or equal to 1. In the region split automaton the special clock T is reset at every transition and verify guards of the form T ∈ (A, A + 1). Thus times t i vary in intervals of length 1. The language of each path is then included in a hypercube of side 1. Volume is therefore less or equal to 1.

Proof of proposition 1. We will construct step by step automata A i such that B 1 to B i is true for A i and such that H(A) = H(A i ). To construct A 2 we refer to the procedure of [START_REF] Asarin | Volume and entropy of regular timed languages: Analytic approach[END_REF] without the two last points (because we want to keep all states initial). A 4 can be constructed from A 2 by removing locations that do not satisfy B 4 and by setting the initial and final states to be the entry regions. We must show that H(A 4 ) = H(A 2 ). First we have that H(A 4 ) ≤ H(A 2 ) as L(A 4 ) ⊆ L(A 2 ). We call internal locations which satisfy B 4 and external the others. Let k be the maximal length of a consecutive path composed exclusively with edges involving external locations (we speak of external path). We factorize every path of A 2 with length greater than 2k as

π (1) π (2) π (3) with π (1) , π (3) ∈ E k . By definition of k, π (2) is a path of A 4 . Moreover we have Vol(L(π)) ≤ Vol(L(π (1) ))Vol(L(π (2) ))Vol(L(π (3) )) ≤ M 2k Vol(L(π (2) )). Then Vol(L n+2k (A 2 )) ≤ Vol(L n (A 4
))M 2k and we are done by taking lim n→∞ 1 n log 2 . A 5 is constructed from A 4 by deleting edges which do not satisfy B 5 (one has also to delete locations which no more satisfy B 3 , B 4 ). By doing this we delete punctual paths, their volumes are null and do not contribute to H.

A 6 is constructed from A 5 by taking identity as labeling function.

For each w we have L(w) = ∪ π∈L -1 (w) L(π) and then

Vol(L n (A 5 )) = w∈Σ n Vol(L(w)) ≤ w∈Σ n π∈L -1 (w) Vol(L(π)) = Vol(L n (A 6 )).
For the converse inequality, everything would be very simple if the above union were disjoint but this is not the case due to freedom on the initial state. However from one state s the languages L(π (2) , s), L(π ′ (2) , s) starting from s and associated with two distinct paths π (2) = π ′

(2) are disjoint (as guards and regions of π (2) and π ′

(2) are disjoint at a moment). Then, if all clocks have been reset during a path π (1) , for every two distinct paths π (2) , π ′

(2) we have

L(π (1) π (2) ) ∩ L(π (1) π ′ (2) ) = ∅.
We divide in two groups the set of paths of a given length l (l is a parameter that we will tune later):

the set R(l) of paths which have reset all its clocks; -the set of other paths which have a volume Vol(L(π))

≤ 1 l! π∈E n Vol(L(π)) = π (1) ∈R(l) π (2) ∈E n-l Vol(L(π (1) π (2) ))+ π (1) ∈R(l) π (2) ∈E n-l Vol(L(π (1) π (2) )).
We will denote by S 1 and S 2 the two sums above. S 2 is upper bounded by |E| n l! . For each w ∈ Σ n we have

L(w) = π (1) ∈R(l) π (2) ∈E n-l π (1) π (2) ∈L -1 (w) L(π (1) π (2) )
and then

Vol(L(w)) ≥ max π (1) ∈R(l) π (2) ∈E n-l π (1) π (2) ∈L -1 (w) Vol(L(π (1) π (2) )) ≥ 1 |E| l π (1) ∈R(l) π (2) ∈E n-l π (1) π (2) ∈L -1 (w) Vol(L(π (1) π (2) ))
We sum over all w and deduce

S 1 ≤ |E| l Vol(L n (A 5 )). Then Vol(L n (A 6 )) ≤ Vol(L n (A 5 ))(|E| l + |E| n l!Vol(Ln(A 5 ))
). We can find l such that l = o(n) and Proof of proposition ??. A part of the previous proof is easy to adapt to show that h ε (A) = h ε (A 4 ).

The following lemma says that L(A 5 ) is the non punctual part of L(A 4 ) and thus h ε (L(A 4 )) = h ε (L(A 5 )) if and only if L(A 4 ) is not punctual i.e. L(A 4 ) = int(L(A 4 )). Lemma 6. L(A 5 ) = int(L(A 4 ))

Proof. Let NPin(w) (resp. Pin(w)) be the set of non punctual (resp. punctual) paths π such that L(π) = w. NPin(w) is exactly the set of paths of L(A 5 ) labeling w. Thus we have to show that for each w, int(L(w)) ⊂ ∪ π∈NPin(w) L(π) (the converse inclusion is straightforward as ∪ π∈NPin(w) L(π) is an open subset of L(w)). Let x be a point in int(L(w)). Suppose by contradiction that x ∈ ∪ π∈NPin(w) L(π), then for ε small enough x is ε far from ∪ π∈NPin(w) L(π). x is less than ε 2 far from a point y in int(L(w)). y is then in the interior of ∪ π∈Pin(w) L(π) which is absurd as this set has empty interior.

⊓ ⊔

As in the proof of the previous proposition, for each w we have

L(w) = ∪ π∈L -1 (w) L(π) and then L n,ε (A 5 ) = w∈Σ n |L n,ε (w)| ≤ w∈Σ n π∈L -1 (w) |L n,ε (π)| = L n,ε (A 6 ) . We deduce that h ε (A 5 ) ≤ h ε (A 6 ) Lemma 7. h ε (A 6 ) ≤ h ε (A 5 )
Proof. For a path π and a vector of delays t, one can show that the set of states from which π × t can be read is a polytope of IR |X| . Let us denote this set by

Start(π, t) = {x | ∃x ′ , x (t1,π1)(t2,π2)...(tn,πn) ---------------→ x ′ }. We denote by S ε the set of ε |X|+1 -discrete and internal states. By lemma 2 of [6] if t is ε-discrete, one can find a state in Start(π, t)∩S ε . We deduce that L n,ε (A 5 ) ≤ |S ε | max x∈Sε |L(π, x)| ≤ |S ε | L n,ε (A 6 ) . As |S ε | ≤ |Q| (|X|+1)Mc ε which is a constant in n, by taking lim n→∞ 1 n log 2 we conclude the proof. ⊓ ⊔
We have the chain

h ε (A 6 ) ≤ h ε (A 5 ) ≤ h ε (A 4 ) ≤ h ε (L(A 4 )) = h ε (L(A 5 )) ≤ h ε (A 6 ).
The remaining inequalities are straightforward due to language inclusion. We close the cycle with the following lemma which is shown using the theory of section 5 (it should be read before the next proof).

Lemma 8. For non punctual automaton

h ε (RS(A)) = h ε (RS(A)) + o(1)
Proof. With the notation of the proof of theorem 4 we have :

|L n,ε | ≤ L - n ′ ,ε ′ ≤ |int(L) n ′ ,ε ′ | ≤ |L n ′ ,ε ′ | .
n ′ and ε ′ are designed in such a way that taking lim n→∞ 1 n log 2 we obtain the result (see computations at the end of the proof of theorem 4).

A.2 Polytope of paths

Proof of proposition 3. We suppose that π 1 , . . . , π n are consecutive and then form a region path, otherwise L(π) is empty and thus a contiguous polytope. We denote by x 1 , . . . , x |X| the clocks and by x l k the value of the clock x l after the k th transition. We call a mixed condition on t 1 , . . . , t n a condition of the form ∃x 1 0 , . . . ∃x |X| 0 ( i I i (x 1 0 , . . . , x |X| 0 )) where I i (x 1 0 , . . . , x |X| 0 ) are inequalities of three types:

inequalities between two clocks without time: x l 0 ≤ B + x p 0 ; -inequality between a clock and a contiguous sum starting from index 1:

x l 0 ≤ B -S 1..j , A -S 1..j ≤ x l 0 ; -inequalities without clocks (which are temporal inequalities): A ≤ S j..k , S j..k ≤ B.

We will proceed in two steps: first we show that L(π) verifies a mixed condition, then we show that any mixed condition describes a contiguous polytope by eliminating (projecting) clock variables with the Fourier-Motzkin procedure:

First step: Starting clock values satisfy the condition of the starting region:

x l 0 ≤ B + x p 0 , A ≤ x l 0 ≤ B.
For all k between 1 and n -1, the guard x l ∈ [A, B] of the k th transition will be translated in

x l k-1 + t k ∈ [A, B].
There are two cases, either x l has not been reset and then x l k-1 + t k = x l 0 + S 1..k , we add the inequality A -S 1..k ≤ x l 0 ≤ B -S 1..k ; or x l has been reset for the last time in the j th transition and then x l k-1 + t k = S j..k , we add the inequality A ≤ S j..k ≤ B.

Second step: Suppose by induction that we have found a mixed condition describing L(π) without clocks x 1 0 , .., x l-1 0 , we will show how to get rid of the clock x l 0 . Let us divide inequalities in five groups: 1. inequality without x l 0 ; 2. inequalities of type: A -S 1..i ≤ x l 0 ; 3. inequalities of type: x l 0 ≤ B -S 1..j ; 4. inequalities of type: x p 0 ≤ C + x l 0 ; 5. inequalities of type: x l 0 ≤ D + x q 0 . We keep inequalities of the first group, we replace others by a conjunction of equivalent inequalities:

-A -S 1..i ≤ B -S 1..j formed with groups 2 and 3; -A -S 1..i ≤ D + x q 0 formed with groups 2 and 5; -x p 0 ≤ C + B -S 1..j formed with groups 3 and 4; -x p 0 ≤ C + D + x q 0 formed with groups 2 and 4. Inequalities are of the expected form(first is equivalent to A -B ≤ S i+1..j or A ≤ B or S j+1..i ≤ B -A whether i < j, i = j or i > j). At the end there is only a conjunction of temporal inequalities i.e. a contiguous polytope.

A.3 Point to point reachability

Proof of proposition 4. We use lemma 2 to show that G(π) is complete iff Reach(π) = r × r ′ . Suppose that G(π) is complete. For all x, x ′ , we denote by Λ, Λ ′ vectors with corresponding convex coordinates. We define P as the matrix with rows equal to Λ ′ , we have ΛP = Λ ′ , then x, x ′ ∈ Reach(π). We conclude that G(π) ⇒ Reach(π) = r × r ′ . The reciprocal is trivial.

Reach(π) and Reach(int(π)) are polytopes obtained by quantifier elimination (projection) in the formula ∃t 1 , . . . t n , x (t1,π1)(t2,π2)...(tn,πn) ---------------→ x ′ . The result is a finite conjunction of exactly the same equalities and inequalities in both cases except that inequalities in π are non-strict and strict in int(π). By flipping the nature of inequalities one can change r × r ′ in r × r ′ and vice versa.

Proof of proposition 5. Synchronizing cycles are by definition particular forget cycles. We do the other inclusion by contrapositive : if a cycle is not progressing then there is a clock x which is not reset and thus in the orbit graph of the cycle there is no edge from vertices in the hyperplane x = A + 1 to vertices in the hyperplane x = A where A is the integer part of x in the region where the cycle starts and ends. The graph is not complete and thus the cycle is not forgetting.

More on synchronization cycle

The stringent condition of synchronization cycle seems too strong for us but is a simpler interesting subcase, in fact if πa is a synchronizing cycle with a the synchronizing edge then Vol(L((πa) n )) = (Vol(L(πa))) n and so H ≥ 1 |πa| Vol(L(πa)) > -∞. This strong condition has been used in [START_REF] Carnevali | State-density functions over DBM domains in the analysis of non-Markovian models[END_REF].

Proof of lemma 4. Modulo a reordering of the clocks and a fusion of equal clocks we can suppose that the ending p-dimensional region r′ is

⌊x⌋ + {({x 1 }, . . . , {x p }) | 0 ≤ {x 1 } ≤ {x 2 } ≤ • • • ≤ 1},
where ⌊x⌋ = (⌊x 1 ⌋, . . . , ⌊x p ⌋). We have the following lemma to pass from cartesian coordinates (x 1 , . . . , x p ) to barycentric coordinates (λ 1 , . . . , λ p+1 ):

Lemma 9. for i ≥ 2, λ i = {x p+2-i } -{x p+1-i }.
Proof. Vertices of the region are S 1 = ⌊x⌋ + (0, . . . , 0), S 2 = ⌊x⌋ + (0, . . . , 1), S p+1 = ⌊x⌋ + (1 . . . 1). Therefore (x 1 , . . . , x p ) = i∈I λ i S i = ⌊x⌋ + (λ p+1 , λ p+1 + λ p , . . . , λ p+1 +λ p +..+λ 2 ) and then for i ≥ 2 we have λ

i +(⌊x p+2-i ⌋-⌊x p+1-i ⌋) = x p+2-i -x p+1-i . For each i ∈ {2, . . . , p}, λ i + (⌊x p+2-i ⌋ -⌊x p+1-i ⌋) = x p+2-i -x p+1-i is the sum of all delays between reset of x p+2-i and x p+1-i with a negative coefficient if x p+2-i < x p+1-i . Therefore every λ i (i ∈ {2, . . . , p}) is of the form -C i ± t j with C i ∈ IN. If 1 ∈ I then
i∈I λ i is of the expected form else as λ 1 = 1 -i≥2 λ i , there exists J ⊆ {2, . . . , p} such that i∈I λ i = 1 + i∈J ±λ i ; the sum is also of the expected form. Moreover, there is one coefficient distinct from 0 because i∈I λ i is not constant (otherwise dimension of the region would be less than p).

Proof of lemma 3. Let P be the matrix such that ΛP = Λ ′ . There exists an SCC I of G(π) without incoming edges from other SCCs. Modulo a change of indices, we can suppose that indices of I are minimal and then matrix P has the following form:

P = P I→I P I→ Ī 0 PĪ → Ī . If we decompose Λ in (Λ I , Λ Ī ) and Λ ′ in (Λ ′ I , Λ ′ Ī ) we have Λ I P I→I = Λ ′ I . j∈I λ ′ j = j∈I i∈I λ i P ij = i∈I λ i j∈I P ij ≤ i∈I λ i .

A.4 Thin and thick SCCs

Proof of proposition 8. First, if all subautomata are thin, as cycle are included in SCC, there is no forgetful cycle in the whole automaton which is therefore thin. Let us denote by H max the maximal volumetric entropy obtained for a subautomaton A imax . As L(A imax ) is a sublanguage of L(A) then H max ≤ H(A). For the converse inequality we use a straightforward consequence of the definition of volumetric entropy: H is the least real such that ∀σ > 0, ∃A > 0, ∀n ≥ 0, Vol(L n ) ≤ A2 n(H+σ) . Therefore, in each subautomaton we have ∀σ > 0, ∃A > 0, ∀n ≥ 0, Vol(L n ) ≤ A2 n(Hmax+σ) . One can decompose L n in a finite disjoint union of languages of the form

L n1 (A i1 ) • L i1→i2 • L n2 (A i2 ) • • • L nm (A im ) where i 1 < • • • < i m , n -c ≤ n 1 + • • • + n m ≤ n (
for some constant c) and L ij →ij+1 are finite languages going from A ij to A ij+1 and thus with bounded volume. Volume V of such a language verifies ∀σ > 0, Hmax+σ) where A ′′ = max(2 -c(Hmax+σ) , 1) (with some constant c). Summing over elements of the finite disjoint union of languages gives the expected result ∀σ > 0, ∃A > 0, ∀n ≥ 0, Vol(L n ) ≤ A2 n(Hmax+σ) and then H max ≥ H(A).

∃A ′ > 0, ∀n ≥ 0, V ≤ A ′ 2 (n1+ dots+nm)(Hmax+σ) ≤ A ′′ 2 n(
Proof of theorem 3. Let λ, α > 0 and π a λ-thick path of length n. Let r be the number of SCC in the automaton. We suppose by contradiction that π wanders more than αn transitions on thin SCCs and thus has a factor π ′ of length greater than αn r in one thin SCC. In thin SCC, for every γ, for m large enough i.e. greater than a constant N γ , every path π ′′ of length m is γ-thin :

Vol(π ′′ ) < γ m . If n is greater than Nγ r α then Vol(π) ≤ Vol(π ′ ) < γ α r
n which contradict the λ-thickness when choosing γ such that γ α r = λ. Proposition 9. In a thick SCC A i , there exists a constant c such that there is a forgetful cycle of length c on each location of A i .

Proof. Let π be some forgetful cycle and r be the region where π starts and ends. Let r ′ be a region in the same SCC as r. There is a path π (1) from r to r ′ and a path π (2) from r ′ to r. We will show that π (1) ππ (2) is a forgetful cycle on r ′ . As Puri stated in [START_REF] Puri | Dynamical properties of timed automata[END_REF], in an orbit graph, there is an outgoing edge from each vertex of the starting region and an incoming edge to each vertex of the ending region. Let S, S ′ be two vertices of r ′ , let S 1 , S 2 be two vertices of r such that (S, S 1 ) and (S 2 , S ′ ) are respectively edges of G(π (1) ) and G(π (2) ). As G(π) is complete there is an edge between S 1 and S 2 and so there is an edge between S and S ′ in G(π (1) ππ (2) ). To sum up there is a forgetful cycle π r ′ on each region r ′ of the strongly connected subautomaton, the least common multiple of all length of π r ′ gives an appropriate constant c.

A.5 Proof of theorem 4, more details for ≤ direction

We begin by some auxiliary results used in the core of the proof.

Remark 1. An e-fat contiguous polytope is eM contiguous.

Proof. Let t 1 , . . . , t n an 1 e discrete and intern point of the polytope. Equations of the polytopes are of the form A ≤ S j..k ≤ B with B ≤ M . As for every i ∈ {1, . . . , n}, t i > 0 and t i is multiple of 1 e then t i ≥ 1 e and k-j+1 e ≤ S j..k ≤ M . We deduce the result: lengths kj + 1 of contiguous sums are bounded by eM .

The following two discretization lemmata are from [START_REF] Asarin | On discretization of delays in timed automata and digital circuits[END_REF]. Lemma 10. If x, x ′ are ε-discrete and L(π, x, x ′ ) = ∅ then L ε (π, x, x ′ ) = ∅. Lemma 11. Every contiguous polytope P of dimension n has an 1 m -discrete internal point for all m > n.

The core of the proof of 4 Let c be a constant such that there is a progress cycle of length c from everywhere in the automaton (see proposition 9 above). Let π be a path of length n = mb, we will insert in π at every b letters a forgetful cycle f i such that polytopes associated to the created word are e-fat with e = (b + 1)(c + 1) (and thus contain more discrete points).

Let π = π (1) π (2) . . . π (m) where π (1) , . . . , π (m) are words of length b. For all i ∈ {1, . . . , m-1}, there exists a forgetful cycle f i of length c on the region r i between π (i) and π (i+1) . We define π ′ = φ(π) by φ(π) = π (1) f 1 π (2) . . . π (m-1) f m-1 π (m) . Function φ is an injection from E n = E mb to E mb+(m-1)c = E n ′ with n ′ defined as n(1 + c b )c . This injection can be extended to ε-discrete words because with lemma 10, for each couple of ε-discrete states of r i we can chose delays labeling f i to join each other. Therefore we have a first inequality

|L ε (π)| ≤ |L ε (π ′ )| .
By lemma 11, for each i one can find a 1 b+1 -discrete and internal run on π (i) starting from a state s i and ending in a state s ′ i . One can also find a 1 e = 1 (b+1)(c+1) -discrete and internal run on f i from s ′ i to s i+1 . We have described a

Third inequality : ε

′ n ′ L - ε ′ (π ′ ) ≤ Vol(L(π ′ )). ∀t = (t 1 , . . . , t n ) ∈ L - ε ′ (π ′ ), ∀v = (v 1 , . . . , v n ) ∈ [-ε ′ 2 , ε ′ 2 ]
, for all equations S j..k ∈ [A, B] defining L(π ′ ), we have

A + dε ′ ≤ k i=j (t i + v i ) ≤ B -dε ′ and | k i=j v i | ≤ ε ′ 2 (k -j + 1) ≤ d, thus A ≤ k i=j (t i + v i ) ≤ B i.e. t + v ∈ L(π ′
). The set of cubes of side ε ′ centered in point of L - ε ′ (π ′ ) has volume ε ′ n ′ L - ε ′ (π ′ ) , it is contained in L(π ′ ), this prove the third inequality.

End of the proof. Combining the three inequalities we get:

|L ε (π)| ≤ ε ′-n ′ Vol(L(π ′ )).
Recall that φ : π → π ′ is an injection and thus

|L n,ε | = π∈E n |L ε (π)| ≤ ε ′-n ′ π ′ ∈E n ′ Vol(L(π ′ )) = ε ′-n ′ Vol(L n ′ ).
If we take lim n→∞ 1 n log 2 in the previous inequality we obtain .

h ε ≤ 1 + c b log 2 1 ε ′ + H .

Fig. 2 .

 2 Fig. 2. The closed region-split version of A4

Fig. 3 .

 3 Fig.3. Two non strongly connected orbit graphs, the first one is the orbit graph of the cycle of A1, of the cycle ab of A2 and of the cycles a and b of A4. States move from initial SCC I to final one. By choosing the convex combination of paths given by the Markov chain on the second orbit graph we pass from state (λ1 = 0.2, λ2 = 0.5, λ3 = 0.3) to state (λ ′ 1 = 0.46, λ ′ 2 = 0.02, λ ′ 3 = 0.52). The sum λ1 + λ2 can only decrease.

1 N 1 n 1 ε 1 ε

 1111 the following holds:Vol(L(π))N n ≤ |E(N L(π))| = |L ε (π)|.Summing over all words of length n and taking lim n→∞ log 2 , we obtain that H+ log 2 ≤ h ε . ⊓ ⊔ Proof (≤ direction of Thm. 4).Upper bounding h ε by H + log 2 + o(

  (Ln(A 5 )) = O(1) (e.g. n = log 2 l! ∼ l log 2 l). With such an l the quantity 1 n log 2 (|E| l + |E| n l!Vol(Ln(A 5 )) ) tends to 0 and then H(A 5 ) ≥ H(A 6 ).

1 e 1 ε

 11 -discrete and internal run on π ′ which is thus e-fat.Moreover an e-fat polytope is eM contiguous by remark 1. We pose 2d = eM and we have that π ′ is 2d contiguous.Let ε ′ = ε α where α = 1 + deε. L -(π ′ ) is defined by shrinking the inequalities defining L(π ′ ) by the amount ε′ d i.e. changing S j..k ∈ [A, B] into S j..k ∈ [A + dε ′ , Bdε ′ ]. Second inequality : |L ε (π ′ )| ≤ L - n ′ ,ε ′ . To simplify we pose N = 1 ε and N ′ = ′ = αN , We give an injection from E(N L(π ′ )) to E(N ′ L -(π ′ )), these two sets are respectively in bijection with L ε (π) and L ε (π ′ ). As L(π ′ ) is e-fat, there exists(u 1 , . . . , u n ) ∈ IN n such that eA + 1 ≤ k i=j u i ≤ eB -1 (where S j..k ∈ [A, B]is one of the equations defining L(π ′ )). We multiply by d and use the fact that de= (α -1)N : (α -1)N A + d ≤ k i=j du i ≤ (α -1)N Bd. If (t 1 , . . . , t n ) verifies N A ≤ k i=j t i ≤ N B then (t 1 + du 1 , . . . , t n + du n ) verifies αN A + d ≤ k i=j (t i + du i ) ≤ αN Bd and thus it is in E(N ′ L -(π ′ )). The translation of vector (du 1 , . . . , du n ) is an injection from E(N L(π ′ )) to E(N ′ L -(π ′ )) and then we are done.

The right hand side is equal to log 2 1 ε 1 ε 1 3 (log 2 1 ε ) 1 3 , then log 2 α and c b log 2 1 ε are O ε 1 3

 1111111 + H + log 2 α + c b O(log 2 ). Let b = ε -

Our approach to timed languages is based on volumes, and does not apply, in its present form, to unbounded delays which lead to infinite volumes.

under the condition that the set is measurable; timed languages considered in this paper are all measurable as unions of polytopes.

This roughly corresponds to automata where all states are both initial and final.

An intuition behind this lemma could be as follows. A clock vector with barycentric coordinates λ in a region can be seen as a probabilistic distribution over vertices of this region (with probabilities λ). The lemma says that this distribution, at each cycle, evolves exactly as in some Markov chain.

i.e. by replacing each constraint S j..k ∈ [A, B] in the definition of L(π ′ ) as a contiguous polytope by S j..k ∈ [A + δ, Bδ] (see[START_REF] Asarin | Volume and entropy of regular timed languages: Discretization approach[END_REF]).

Acknowledgements. The authors are thankful to Thomas Colcombet for a key advise: to use Simon factorization forests, and to Dominique Perrin and Aldric Degorre for inspiring discussions.