Eugene Asarin

Nicolas Basset

Aldric Degorre

Entropy of regular timed languages

Keywords: timed automata, timed languages, entropy Contents

published or not. The documents may come

Introduction

Our main problem: size of timed languages

Since early 90s, timed automata and timed languages are extensively used for modelling and verification of real-time systems, and thoroughly explored from a theoretical standpoint. However, two important, and closely linked, aspects have never been addressed before our first related papers: quantitative analysis of the size of these languages and of the information content of timed words. In this paper, we formalize and solve these problems for deterministic timed automata.

Recall that a timed word describes a behavior of a system, taking into account delays between events. For example, 2a3.11b means that an event a happened 2 time units after the system start, and b happened 3.11 time units later. A timed language, which is just a set of timed words, may represent all such potential behaviors. Our aim is to measure the size of such a language. For a fixed number n of events, we can consider the language as a subset of Σ n × R n (that is of finitely many copies of the space R n ). A natural measure in this case is just Euclidean volume V n of this subset. When the number of events is not fixed, we can still consider for each n all the timed words with n events belonging to the language and their volume V n . It turns out that in most cases V n asymptotically behaves as 2 nH for some constant H that we call entropy of the language.

We believe that exploration of entropy of timed languages is theoretically and practically appealing for several reasons.

• Symbolic dynamics approach (including the entropy-based analysis) to finite automata has made its proofs in theory of languages, theory of codes etc. Porting it to an important new class of infinite-state automata: timed ones, is a natural research problem.

• The information-theoretic meaning of H can be stated as follows: for a small ε, if the delays are measured with a finite precision ε, then using the words of the language L with entropy H one can transmit H + log(1/ε) bits of information per event.

In [START_REF] Asarin | Volume and entropy of regular timed languages: Discretization approach[END_REF] we formalize this idea in terms of Kolmogorov complexity. In [START_REF] Asarin | Toward timed theory of channel coding[END_REF] we relate H to the capacity estimation of a time-based information transmission channel.

• In model-checking of timed systems, it is often interesting to know the size of the set of all behaviors violating a property or of a subset of those presented as a counter-example by a verification tool. In the same context of verification, when one overapproximates a timed language L 1 by a simpler timed language L 2 (using, for example, some abstractions as in [START_REF] Ben Salah | On timed components and their abstraction[END_REF]), it is important to assess the quality of the approximation. Comparison of entropies of L 1 and L 2 provides such an assessment.

• Entropy analysis provides new insights into traditional topics of the theory of timed automata: Zeno behaviors, pumping lemmata, discretization etc. These insights, developed below, were also recently used by some authors in [START_REF] Stainer | Frequencies in forgetful timed automata[END_REF][START_REF] Sankur | Robust controller synthesis in timed automata[END_REF].

• Last but not least, the main technical tool in entropy analysis, a positive integral operator associated to a timed automaton, seems to be an important and useful characteristic of the automaton. We have already successfully applied it to several problems: computing generating functions of timed languages [START_REF] Asarin | Generating functions of timed languages[END_REF], finding a natural probability distribution on a given timed automaton [START_REF] Basset | A maximal entropy stochastic process for a timed automaton[END_REF], and, more surprisingly, counting sets of permutations defined by regular expressions and randomly generating their elements [START_REF] Basset | Counting and generating permutations using timed languages[END_REF].

In this paper, we explore and solve the following problem: given a timed language accepted by a deterministic timed automaton, find the volume V n of the set of accepted words of a given length n and the entropy H of the whole language.

Classical works: entropy of regular languages

Our problems and techniques are inspired by works concerning the entropy of finite-alphabet languages (cf. [START_REF] Lind | An Introduction to Symbolic Dynamics and Coding[END_REF][START_REF] Chomsky | Finite state languages[END_REF]). There the cardinality of the set L n of all elements of length n of a prefix-closed regular language also behaves as 2 nH for some entropy H. The characterization of the entropy is based on the Perron-Frobenius theory for positive matrices.

Let us sketch how it works. Given a finite deterministic automaton with state set Q, let L n (q) be the language of n-letter words recognized from state q. Consider the |Q|-dimensional vector x n whose coordinates are cardinalities of L n (q), q ∈ Q. It is easy to see that:

x n = A n x 0 , (1)
where A is the adjacency matrix of the automaton. Under some additional hypotheses (strong connectedness, aperiodicity), by Perron-Frobenius theorem for positive matrices, all the components of x n grow as ρ n where ρ = ρ(A) is the spectral radius of the matrix A (which coincides with its maximum eigenvalue). Hence, the entropy can be computed as follows (all the logarithms in this paper are base 2):

H = log ρ(A).
(2)

On techniques used

In this paper, we extend the technique sketched above to timed automata. For a deterministic timed automaton A, we define a timed language L n (q, x) of all the timed words (with n events) accepted from the state (q, x). We denote by v n (q, x) the volume of this language (now it is a function on Q × R n ), and we generalize Eq. ( 1) as follows

v n = Ψ n v 0 , (3)
but now the role of the adjacency matrix is played by some positive matrix integral operator Ψ associated to the timed automaton.

The analog of Perron-Frobenius theory for such operators is much more involved than for matrices, and we have to use some advanced functional analysis from [START_REF] Krasnosel'skij | Positive Linear Systems: The Method of Positive Operators[END_REF][START_REF] Katō | Perturbation Theory for Linear Operators[END_REF] to explore properties of Ψ useful for study of the entropy; the most important of them being a spectral gap.

1.4. Our main results on entropy of timed languages.

First, we show that volumes V n of a language of a deterministic timed automaton are rational numbers, which can be computed using [START_REF] Asarin | Two size measures for timed languages[END_REF]. Next, in Thm 5, we characterize entropy of such a language by an analog of Eq. ( 2): H = log ρ(Ψ).

Third, using spectral properties of the operator, we devise an iterative numerical procedure (cf. Table 1) for entropy computing for all deterministic timed automata, and prove its exponential convergence (Thm 8).

Finally, for a subclass of those automata (so-called "1 1 ⁄2-clock" automata) we give a symbolic algorithm (cf. Table 3) representing the entropy via explicit equations involving trigonometric functions and exponents, and prove its correctness.

1.5. Our second problem: ruling out pathologies in timed automata An amazing theoretical application of the entropy of timed languages is related to a well-known, but not yet sufficiently understood issue of pathological and "normal" behaviors of timed automata. Indeed, timed automata 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 research on timed automata, 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. Such 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 a pioneering paper [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 condition). This kind of conditions appears in most of the cited literature -and will be replaced in this article by a somewhat subtler condition of existence of a forgetful cycle, that is a cyclic path allowing forgetting the clock values.

We propose a unifying approach to most of these issues for deterministic timed automata. We classify each automaton either as thin or as thick : it is thin when the entropy of its language equals -∞ (that is the volume V n decays faster than any exponent), and thick otherwise. It turns out that:

In thin automata all the infinite trajectories are, in some weak sense Zeno; the digitization of long trajectories is difficult, since it requires very a small discretization step.

In thick automata most of trajectories are non-Zeno and behave well under digitization; such automata have a forgetful cycle, and most trajectories visit such a cycle (this can be seen as a sort of pumping lemma).

This dichotomy between thin and thick automata is stated in Thms 2 and 4. The proof of these results 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's theory, namely Simon's factorization forests theory [START_REF] Simon | Factorization forests of finite height[END_REF].

Related work

This work builds on previous research and ideas concerning timed automata, information theory, entropy of regular languages, functional analysis, monoid theory etc. However, as far as we know, the only previous work considering volume of timed languages is [START_REF] Braberman | Hypervolume approximation in timed automata model checking[END_REF], where heuristic estimations of volume are used to guide the state-space exploration in model-checking.

In [START_REF] Bucci | Introducing probability within state class analysis of dense-time-dependent systems[END_REF][START_REF] Sassoli | Close form derivation of state-density functions over DBM domains in the analysis of non-Markovian models[END_REF], probabilities of some timed languages and densities in the clock space are computed. Our formulae for fixed-length volumes can be seen as specialization of these results to uniform measures. As for languages of unbounded length, they use stringent condition of full simultaneous reset of all the clocks at most every k steps, and under such a condition, they provide a finite stochastic class graph that allows computing various interesting probabilities. Here we use a much weaker hypothesis (thickness or existence of a forgetful cycle), and obtain only the entropy. Integral formulas for densities in probabilistic timed automata, similar to ours for volumes, are presented in [START_REF] Maler | On zone-based analysis of duration probabilistic automata[END_REF][START_REF] Bertrand | Quantitative model-checking of one-clock timed automata under probabilistic semantics[END_REF]. In [START_REF] Bertrand | Quantitative model-checking of one-clock timed automata under probabilistic semantics[END_REF] probabilities of LTL properties of one-clock timed automata (over infinite timed words) are computed using Markov chains techniques. We expect that our techniques based on positive operators will be useful for the analysis of timed probabilistic Petri nets and automata, as in articles cited above.

Paper organization

This paper is organized as follows. In Sect. 2 we define volumes of fixed-length timed languages and entropy of unbounded-length timed languages and explore their basic properties. In Sect. 3 we present the dichotomy between thin and thick timed automata. In Sect. 4 we associate to a timed automaton a functional space and a positive operator Ψ. Next, we characterize the volume and the entropy in terms of this operator. On a more technical side, we explore spectral properties of Ψ. The latter properties play a central role in Sect. 5, where we give two procedures for computing the entropy of a timed regular language based on the spectral radius of Ψ. We conclude the paper by some final remarks in Sect. 6.

Problem statement

Geometry, volume and entropy of timed languages

A convex polytope in R n is the set defined by finitely many linear inequalities; a polytope is a finite union of convex ones. For a measurable P ⊂ R n , we denote its volume (i.e. its finite or infinite Lebesgue measure) by Vol P ; of course all the polytopes are measurable.

A timed word of length n over an alphabet Σ is a sequence w = t 1 a 1 . . . t n a n , with a i ∈ Σ, t i ∈ R and 0 ≤ t i . Here t i represents the delay between the events a i-1 and a i (this definition rules out timed words ending by a time delay).

A timed language L is a set of timed words. For every timed language L and word w = w 1 . . . w n ∈ Σ n , we define

P L w = {(t 1 , . . . , t n ) | t 1 w 1 . . . t n w n ∈ L}.
The language L is called measurable whenever all the P L w are measurable. In this case, for a fixed n, we define the n-volume of L as follows:

V n (L) = w∈Σ n Vol P L w .
In other words, we sum up, over all the possible words w of n discrete events, the volumes of the corresponding sets of delays in R n . We just associated with every measurable timed language a sequence of n-volumes V n . We will show in Sect. 2.5 that, for languages of deterministic timed automata, V n is a computable sequence of rational numbers. However, we would like to find a unique real number characterizing the asymptotic behavior of V n as n → ∞. Typically, V n depends approximately exponentially on n. We define the entropy of a language as the rate of this dependence. Formally, for a measurable timed language L we define its (volumetric) entropy as follows:

H(L) = lim sup n→∞ log V n n .
Remark 1. Many authors consider a slightly different kind of timed words: sequences (a 1 , d 1 ), . . . , (a n , d n ), where

a i ∈ Σ, d i ∈ R and 0 ≤ d 1 ≤ • • • ≤ d n ,
with d i representing the date of the event a i . This definition is in fact isomorphic to ours by a change of variables:

t 1 = d 1 and t i = d i -d i-1 for i = 2.
.n. It is important for us that this change of variables preserves the n-volume, since it is linear and its matrix has determinant 1. Therefore, choosing date (d i ) or delay (t i ) representation has no influence on language volumes (and entropy). Due to the authors' preferences (justified in [START_REF] Asarin | Timed regular expressions[END_REF]), delays will be used in the sequel.

Bounded deterministic timed automata

We assume that the reader is acquainted with timed automata; otherwise, we refer her or him to [START_REF] Alur | A theory of timed automata[END_REF] for details. Here we only fix notations and briefly recall the definitions. We fix a natural constant M , which upper bounds all the constants in the automaton.

A clock is a variable ranging over R ≥0 (non-negative reals). A clock constraint g ∈ G C over a set of clocks C is a conjunction of finitely many inequalities of the form x ∼ c or x ∼ y, where x and y are clocks, ∼∈ {<, ≤, =, ≥, >} and c ∈ 0..M . A clock reset r ∈ R C is determined by a subset of clocks B ⊂ C, it resets to 0 all the clocks in B and does not modify the values of the others.

A timed automaton (TA) is a tuple A = (Q, Σ, C, ∆, q 0 , F ). Its elements are respectively the finite set of locations, the finite alphabet, the finite set of clocks (let its cardinality be d), the transition relation, the initial location, and the final condition. A state of A is a pair (q, x) of a control location q ∈ Q and a vector of clock values x ∈ R d . Elements of ∆ are transitions, i.e. tuples (q, a, g, r,

q ′ ) ∈ Q × Σ × G C × R C × Q
denoting the possibility, at location q when the clock vector satisfies the guard g, to read the label a, apply the clock reset r and then go to location q ′ . An element of F has a form (q, g) ∈ Q × G C meaning that an accepting run can terminate by a transition to q with clocks respecting the clock constraint g.

A run of A along a path π = δ 1 . . . δ n ∈ ∆ n has the form (q i0 , x 0 ) t1a1 ---→ (q i1 , x i1 ) t2a2 ---→ • • • tnan ---→ (q in , x n ),
where, for all j ∈ 1..n, δ j = (q ij-1 , a j , g, r, q ij ) ∈ ∆,

• x j-1 + t j 1 |= g with 1 denoting the vector (1, . . . , 1),

• and x j = r(x j-1 + t j 1).

In this case, we use the notation x 1 t1...tn,π -----→ x n to say that such a run exists. When q i0 = q 0 is the initial state, x 0 is 0 and F contains a couple (q, g) with q in = q and x n satisfying g, then the timed word t 1 a 1 . . . t n a n is said to be accepted by A. The set of all such words is the language L(A) accepted by A. For such a timed regular language, the sets P L w are polytopes, and hence any timed regular language is measurable and its volumes and entropy are well-defined; we will write V n (A) (or even

V n ) instead of V n (L(A)).
Several convex polytopes are naturally associated with a path in a timed automaton. Given a path and two clock vectors, a polytope of all the timings of the path can be defined:

P π (x, x ′ ) = {t | x t,π --→ x ′ }.
If we are not interested in clock values at the end of the path (resp. any clock value), we get a polytope depending only on the path and clock values at the beginning of the path (resp. depending only on the path):

P π (x) = {t | ∃x ′ , x t,π --→ x ′ } (resp. P π = {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 ′ }. All these polytopes are cross-sections or projections of the universal polytope of the path:

Ω π = {(x, t, x ′ ) | x t,π --→ x ′ }.
A TA is deterministic if for any two transitions with the same source and the same label, the guards are disjoint. It is bounded whenever every guard upper bounds at least one clock.

In the rest of the paper, we compute volumes and entropy for regular timed languages recognized by deterministic timed automata. Moreover, if some guards in the automaton were unbounded, the volume would be infinite, which is beyond the reach of our approach. Thus we concentrate on Bounded Deterministic Timed Automata (BDTA).

Remark 2. Most of known techniques to compute entropy of untimed regular languages work on deterministic automata. In fact, these techniques count paths in the automaton, and only in the deterministic case their number coincides with the number of accepted words. The same is true for volumes in timed automata.

Three examples

To illustrate the problem consider the languages recognized by BDTA A 1 , A 2 , A 3 on the first line of Fig. 1 (the three others will be considered later). Two of them can be analyzed directly, using definitions and common sense. The third one resists naive analysis, it will be used to illustrate more advanced methods throughout the paper.

Rectangles

Consider the timed language recognized by A 1 of Fig. 1 For a given untiming w ∈ {a, b} n containing k letters a and nk letters b, the set of possible timings is a rectangle in R n of a volume 2 k 7 n-k (notice that there are C k n such untimings). Summing up all the volumes, we obtain

V n (A 1 ) = n k=0 C k n 2 k 7 n-k = (2 + 7) n = 9 n ,
and the entropy H(L 1 ) = log 9 ≈ 3.17.

A product of trapezia

Consider the language defined by the automaton A 2 on Fig. 1, that is containing words of the form t 1 as 1 bt 2 as 2 b . . . t 2k as 2k b such that 2 ≤ t i + s i ≤ 4. For an even n = 2k, the only possible untiming is (ab) k . The set of timings in R 2k is a Cartesian product of k trapezia 2 ≤ t i + s i ≤ 4. The surface of each trapezium equals S = 4 2 /2 -2 2 /2 = 6, and the volume V 2k (A 2 ) = 6 k . For an odd n = 2k + 1, the language is empty and V 2k+1 (A 2 ) = 0. Thus the entropy H(A 2 ) = log 6/2 ≈ 1.29.

Our favorite example

The language recognized by the automaton A 3 on Fig. 1 contains the words of the form t 1 at 2 bt 3 at 4 b . . . with t i +t i+1 ∈ [0, 1]. Notice that the automaton has two clocks that are never reset together. The geometric form of possible timings in R n is defined by overlapping constraints

t i + t i+1 ∈ [0, 1].
It is not so evident how to compute the volume of this polytope. A systematic method is described below in Sect. 2.5. An ad hoc solution would be to integrate 1 over the polytope, and to rewrite this multiple integral as an iterated one. The resulting formula for the volume is

V n (A 3 ) = 1 0 dt 1 1-t1 0 dt 2 1-t2 0 dt 3 . . . 1-tn-1 0 dt n .
This gives the sequence of volumes: In the sequel, we will also compute the entropy of this language. We should remark here, that this sequence of polytopes, their volumes and growth rate were considered in a different (combinatorial) context in [START_REF] Stanley | Enumerative Combinatorics, volume 1 of Cambridge studies in advanced mathematics[END_REF].

Preprocessing timed automata

In order to compute volumes V n and entropy H of the language of a BDTA, we first transform this automaton into a normal form, which can be considered as a (timed) variant of the region graph defined in [START_REF] Alur | A theory of timed automata[END_REF]. We recall that a subset of R d defined by a clock constraint is called a zone. Smallest (by inclusion) zones are called regions.

We say that a BDTA A = (Q, Σ, C, δ, q 0 , F ) is in a region-split form if the following properties hold:

B1. Each location and each transition of A is visited by some accepting run.

B2. For every location q ∈ Q, a unique clock region r q (called entry region of q, its dimension is denoted by d q ) exists, such that the set of clock values with which q is entered is exactly r q . For the initial location q 0 , its entry region is the singleton {0}. B3. The guard g of every transition δ = (q, a, g, r, q ′ ) ∈ ∆ is just one clock region. All the clock values satisfying g are time-reachable from r q .

Notice, that B2 and B3 imply that r(g) = r q ′ for every δ.

Proposition 1. Given a deterministic BDTA A, a region-split TA A ′ accepting the same language can be constructed 2 .

Proof (sketch). Let A = (Q, Σ, C, ∆, q 0 ) be a TA and let Reg be the set of its regions. The region-split automaton A ′ = (Q ′ , Σ, C, ∆ ′ , q ′ 0 ) can be constructed as follows: 1. Split every location q into sublocations corresponding to all possible entry regions. Formally, just take

Q ′ = Q × Reg. 2.
Split every transition from q to q ′ according to two clock regions: one for the clock values when q is left, another for clock values when q ′ is entered. Formally, for every δ = (q, a, g, r, q ′ ) of A, and every two clock regions r and r ′ such that r ′ is reachable from r by time progress, and r ′ ⊂ g, we define a new transition of A ′ δ ′ rr ′ = ((q, r), a, x ∈ r ′ , r, (q ′ , r(r ′ ))) . 3. Take as initial state q ′ 0 = (q 0 , {0}). 4. Remove all the locations and transitions not reachable from the initial state or not co-reachable from the final set of states.

We could work with the region-split automaton, but it has too many useless (degenerate) states and transitions, which do not contribute to the volume and the entropy of the language. This justifies the following definition: we say that a region-split TA is fleshy if the following holds (and punctual otherwise): B4. For every transition δ, its guard g has no constraints of the form x = c in its definition.

Proposition 2. Given a region-split TA A accepting a language L, a fleshy region-split TA A ′ accepting a language L ′ ⊂ L with V n (L ′ ) = V n (L) and H(L ′ ) = H(L) can be constructed.

Proof (sketch). The construction is straightforward:

1. Remove all punctual transitions. 2. Remove all the locations and transitions that became unreachable (or not co-reachable).

Inclusion L ′ ⊂ L is immediate. Every path in A (of length n) involving a punctual transition corresponds to the set of timings in R n which is degenerate (its dimension is smaller than n), hence it does not contribute to V n .

From now on, we suppose w.l.o.g. that the automaton A is in a fleshy region-split form (see Fig. 3).

p x = 0 q x ∈ (0, 1) (0, 1) q x ∈ (1, 2) q x ∈ (2, 3) q x ∈ (3, 4) (1, 2) (2, 3) a, x ∈ (3, 4) b, x ∈ (2, 3)/x := 0 b, x ∈ (3, 0)/x := 0 p x ∈ (0, 1) y = 0 q x = 0 y ∈ (0, 1)
a, x ∈ (0, 1)/x := 0 b, y ∈ (0, 1)/y := 0 p x = 0 y = 0 a, x ∈ (0, 1)/x := 0

Recurrent equations on volume functions

Given a BDTA A, we want to compute its entropy based on its n-volumes V n . In order to obtain recurrent equations on these volumes, we need to take into account all possible initial locations and clock configurations. For every state (q, x), let L(q, x) be the set of all the timed words corresponding to the runs of the automaton starting at this state, let L n (q, x) be its sublanguage consisting of its words of length n, and v n (q, x) the volume of this sublanguage. Similarly we define for a path π starting in a region r,

v π (x) = Vol(P π (x)).
By definition of runs of a timed automaton, we obtain the following language equations:

L 0 (q, x) = ε if q is final; L 0 (q, x) = ∅ otherwise; L k+1 (q, x) = (q,a,g,r,q ′ )∈∆ τ :x+τ ∈g τ aL k (q ′ , r(x + τ )).
Since the automaton is deterministic, the union over transitions (the first in the formula) is disjoint. Hence, it is easy to pass to volumes:

v 0 (q, x) = 1 F (q, x); v k+1 (q, x) = (q,a,g,r,q ′ )∈∆ τ :x+τ ∈g v k (q ′ , r(x + τ )) dτ, (4)
where 1 F is the indicator function of the final states F . We remark that for a fixed location q, and within every clock region, as defined in [START_REF] Alur | A theory of timed automata[END_REF], the integral over τ : x + τ ∈ g can be decomposed into several u l with bounds l and u either constants or of the form cx i with c an integer and x i a clock variable. These equations hold for any state (q, x), but we will consider volume functions and Eqs (4) restricted to the set S = q∈Q {q} × r q of entry states. These formulas lead to the following structural description of v n (q, x), which can be proved by a straightforward induction. Lemma 3. The function v n (q, x) restricted to a location q and a clock region can be expressed as a polynomial of degree n in coordinates of x, with rational coefficients.

Hence, one should obtain, by symbolic integration, for k = 0..n, polynomial functions v k : S → R; and finally compute v n (q 0 , 0). Theorem 1. For a BDTA A, the volume V n is a rational number, computable from A and n by iterating Eq. (4).

Other volumes, same entropy

In the following, we will need two alternative volumes yielding equivalent characterizations of the entropy, which do not depend on initial nor final states of the timed automaton.

• The first one is in terms of volumes V π of polytopes P π associated to paths π ∈ ∆ * : V π def = Vol(P π ). By summing over all paths π of length n we obtain a new sequence of volumes:

Vn def = π∈∆ n V π .
• The second one is in terms of volume functions taking into account the initial clock vector: vn (q, x) def = π∈∆ n , starting in q v π (x) (here the clock vector x belongs to r q ). The norm of such a function is defined as its supremum over all x and q. Proposition 4. Sequences of volumes V n , of volumes Vn and of norms of volume functions vn have the same growth rate (coinciding with the entropy):

H(L(A)) = lim sup n→∞ (log V n )/n = lim n→∞ (log Vn )/n = lim n→∞ (log vn )/n,
in particular the limits (finite or infinite) always exist.

The proof can be found in Appendix A.

The thin-thick alternative and its consequences

In this section we study the dichotomy, we mentionned in Subsect. 1.5, between thin automata, with entropy -∞, and thick automata, with entropy > -∞. To that purpose, we introduce the key notion of forgetful cycle, the existence of which is, as we will show, a necessary and sufficient condition for thickness.

Ruling out pathological (i.e. thin) automata is crucial, not only in the subsequent sections of this paper (Thms 6-7, Lem. [START_REF] Wulf | Robust safety of timed automata[END_REF][START_REF] Abdulla | Sampled semantics of timed automata[END_REF][START_REF] Simon | Factorization forests of finite height[END_REF], but also in other works by us and by other authors. For instance, we can mention papers about frequency analysis [START_REF] Stainer | Frequencies in forgetful timed automata[END_REF], robustness [START_REF] Sankur | Robust controller synthesis in timed automata[END_REF] and quantitative discretization of timed languages (problem defined and motivated in [START_REF] Asarin | Volume and entropy of regular timed languages: Discretization approach[END_REF], and solved in [START_REF] Basset | Thin and thick timed regular languages[END_REF]). In the latter, thickness turns out to be a necessary and sufficient condition for discretizability.

Our "pathological" behaviors can be seen, in some weak sense, as Zeno runs: clock constraints along a pathological infinite path become narrower and narrower, so that there is no fixed radius such that a ball of that radius could be included in the polytope of each of its prefixes. For this paper, the most important consequence is that the volumes of the prefixes have a subexponential growth (hence H = -∞).

In "well behaving" automata, on the contrary, most paths ("most", in the sense of contribution to volume) tend to "forget" old clock constraints, thanks to visiting these forgetful cycles often enough. In particular it is possible, for some fixed radius, to include a ball of that radius in the polytope of each prefix of such a path. Consequently the volume of prefixes has exponential growth.

This section goes as follows: first we make simple observations on pathological behaviors and relate their volumes to those of simplices. Then, inspired by Puri [START_REF] Puri | Dynamical properties of timed automata[END_REF], we characterize reachability in algebraic terms, introducing the monoid of orbit graphs. This eventually leads us to the definition of a forgetful path. After this, we exhibit a Lyapunov function which decreases along all pathological runs. Next comes our pumping lemma (Thm 2), where it is shown that sufficiently long paths with not too small volume (e.g. containing a ball of radius η) necessarily contain a forgetful cycle. 3 This result builds on a deep theorem from Simon [START_REF] Simon | Factorization forests of finite height[END_REF] (Thm 3), about factorization forests. Finally we conclude by stating the equivalences of Thm 4, which justify that the rough dichotomy thin vs. thick is in fact a precise way to distinguish between "ill behaving" and "well behaving" TA.

Thinness, simplices and examples

Our analysis of thin automata will start with a simple observation that the volume of k-dimensional simplices tends to 0 faster than any exponent: Proposition 5. We call simplices of "type 1" and of "type 2", the sets of points t ∈ R k respectively satisfying the sets of inequalities 0

≤ t 1 + • • • + t k ≤ 1, t i ≥ 0 and 0 ≤ t 1 ≤ • • • ≤ t k ≤ 1.

Simplices of both types have volume 1

k! . The automata on Fig. 1 illustrate the concepts of thinness and thickness. On one hand, A 5 and A 6 are examples of automata having thin languages. The case of A 5 is straightforward: its set of timings {t 1 , . . . , t n | i≤n t i ≤ 1} is a simplex of type 1, thus L(A 5 ) is thin. That of A 6 is slightly more involved, as its timing polytope is {t 1 , . . . , t n | ∀i, t 2i + t 2i+1 ≤ 1 ∧ t 2i+1 + t 2i+2 ≥ 1}. But we can make the following change of variables: u 2i+1 = 1t 2i+1 and u 2i = t 2i , mapping the language polytope into the simplex 0

≤ u 1 ≤ • • • u n ≤ 1. This transformation preserves volumes, thus V n (A 6 ) = 1
n! . This is an example of automaton that is thin although it satisfies the progress cycle condition (i.e. resetting all clocks along each cycle, see below).

On the other hand, examples A 3 and A 4 are thick. Indeed their entropies can be computed symbolically using techniques of 5.2 below, which give us respectively log 2 π and log log e. Note that A 4 does not satisfy the progress cycle condition.

Point to point reachability: algebraic characterization

In this subsection, we characterize the reachability relation of a BDTA in terms of an algebraic structure: the monoid of orbit graphs. The key notion of forgetful cycle is then formulated as a reachability property. 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].

In this analysis, it is more convenient to work with closed sets of delays. Hence we also consider the closed version Ā of a region-split automaton A, which is constructed by replacing every region and every guard appearing in the definition of A by its topological closure. Seen as labeled graphs A and Ā are isomorphic, and thus both automata have exactly the same discrete paths. For a path π of A, we denote by π its isomorphic image in Ā. Then the following holds: Proposition 6. For a region-split BDTA A,

1. for all n ∈ N, V n (A) = V n ( Ā) and 2. for any path π of A, Reach(π) = Reach(π).

Monoid of orbit graphs

For a location q ∈ Q, let us denote by V (q) = {s 1 , . . . , s p } the vertices of the closed region rq . 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 q, q ′ ∈ Q, we call orbit graph a tuple (G, q, q ′ ) where G is, if q = q ′ , a directed graph on V (q) or, else, if q = q ′ , a directed graph on V (q) V (q ′ ) with edges in V (q) × V (q ′ ). An edge from s to s ′ symbolizes the fact that the state (q ′ , s ′ ) can be reached from the state (q, s).

Orbit graphs compose in the natural way: given (G 1 , q 1 , q ′ 1 ), and (G 2 , q 2 , q ′ 2 ) their product (G,

q 1 , q ′ 2 ) = (G 1 , q 1 , q ′ 1 ) • (G 2 , q 2 , q ′ 2 ) is defined if q ′ 1 = q 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 q ′ 1 = q 2 , we define (G 1 , q 1 , q ′ 1 ) • (G 2 , q 2 , q ′
2 ) as 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, q, q ′ ) can be represented by its adjacency matrix M of size |V (q)| × |V (q ′ )|. The matrix of a product of orbit graphs is then equal to the product of their matrices in the max-min algebra:

M (G 1 G 2 ) = M (G 1 ) ⊗ M (G 2 )
, where ⊗ is defined by

(A ⊗ B) ij = max k min(A ik , B kj ).
There exists a natural morphism γ : ∆ * → G from paths to orbit graphs defined as follows. For a transition δ between q and q ′ in Ā, we define the orbit graph γ(δ) = (G, q, q ′ ) with edges V (q) × V (q ′ ) ∩ Reach(δ). For a (closed) path π = δ 1 . . . δ n , we define γ(π) = γ(δ 1 ) • • • γ(δ 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. 4.

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 in G × P(C) and, as before, the two special elements 0, 1. The product on M is defined as follows:

(O 1 , X) • (O 2 , Y ) = (O 1 • O 2 , X ∩ Y ), if O 1 • O 2 = 0 0, otherwise.
For each π ∈ ∆ * , we denote by ν(π) the set of clocks not reset along the path π. We define the morphism µ : ∆ * → M as follows: µ(π) = (γ(π), ν(π)).

Orbit graphs and reachability

The orbit graph of a path γ(π) remarkably determines its reachability relation.

Lemma 7 (Puri [START_REF] Puri | Dynamical properties of timed automata[END_REF]). 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 = λ λ λ ′ . 4Here the matrix "inequality" A B means that for all i, j,

(B ij = 0) ⇒ (A ij = 0).
The following particular case is of interest to us:

Proposition 8. γ(π) is complete iff Reach(π) = rq × rq ′ , or equivalently iff Reach(π) = r q × r q ′ .
In this case, we say that π is forgetful. The intuition is that the clock values reached after reading π are independent of the clock values before reading it. We remark that the orbit graph of a forgetful cycle always is an idempotent of the monoid of orbit graphs. Such elements of this monoid (and corresponding elements of M) will be referred to as forgetful idempotents.

Proof (of Prop. 8). We use Lem. 7 to show that γ(π) is complete iff Reach(π) = rq × rq ′ . Suppose that γ(π) is complete. For all x, x ′ , we denote by λ λ λ, λ λ λ ′ the vectors with corresponding barycentric coordinates. We define P as the matrix with rows equal to λ λ λ ′ , we have λ λ λP = λ λ λ ′ and then (x, x ′ ) ∈ Reach(π). We conclude that γ(π) being complete implies that Reach(π) = rq × rq ′ . The converse is trivial.

The second equivalent characterization is a consequence of Prop. 6.

Other particular cycles

Two other kinds of cycles are often considered in the literature: in a progress cycle [START_REF] Puri | Dynamical properties of timed automata[END_REF] (already mentioned above), every clock is reset at some edge; in a regenerating cycle [START_REF] Sassoli | Close form derivation of state-density functions over DBM domains in the analysis of non-Markovian models[END_REF], there is an edge where all the clocks are reset.

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 of the cycle (see Lem. 11 below). Nevertheless the orbit graph of a progress cycle is not always strongly connected (e.g. cycle ab of A 2 depicted in Fig. 4); in that case, clock values in starting states and ending states are still dependent. More precisely, we have the following strict inclusions: Proposition 9. progress cycles forgetful cycles regenerating cycles.

Proof. First inclusion: if a cycle π is not progressing, then there is one clock x, which is not reset along that cycle. It is direct from the semantics of timed automata that the value of x cannot decrease along the transitions of this cycle. Moreover, necessarily this clock is one of the non-zero clocks of the entry region r of the starting location of π. Runs realizing π must start with clock x = x 0 > ⌊x 0 ⌋ and must end with

x = x 1 ≥ x 0 . Thus Reach(π) = r × r.
Second inclusion: a regenerating cycle π necessarily traverses, after the full reset, a location q having singleton {0} as its entry region. Let us call p the location where π starts. We define π 1 and π 2 such that π = π 1 • π 2 , where π 1 goes from p to q and π 2 goes from q to p. Necessarily Reach(π 1 ) = r p × {0} and Reach(π 2 ) = {0} × r p (due to the fundamental reachability property of the region abstraction, cf. [START_REF] Alur | A theory of timed automata[END_REF]). The accessibility relation of π is the composition of that of π 1 and π 2 , i.e. r p × r q , thus π is forgetful.

In order to prove that the inclusions are strict, consider, in Fig. 1, the forgetful cycle labeled ab in A 3 , which is not regenerating, and the progress cycle labeled ab in A 6 , which is not forgetful.

A remark is in order: in most works using progress or regenerating cycles, all the cycles are required to satisfy the considered property. In our work, existence of one forgetful cycle is sufficient to characterize "non-degenerate" (i.e. thick) automata.

Linear Lyapunov functions and sub-exponential volume

The aim of this section is to prove Lemma 13 below. Informally, it states that the iteration of a nonforgetful cycle yields a fast decreasing volume (and thus entropy equal to -∞). The proof of this lemma involves Lyapunov functions and affine expansive functions defined as follows.

Given a cycle π, we say that f (x) ≥ 0 is a Lyapunov function for this cycle if for any (x,

x ′ ) ∈ Reach(π) it holds that f (x ′ ) ≤ f (x) (that is f decreases after every cycle π). An affine function g : R n → R is expansive if it is of the form (t 1 , . . . , t m ) → C + m j=1 α j t j with |α j | ≥ 1 for some j ≤ m.
We need three lemmata to prove Lemma 13. Indeed the core of its proof will be in three steps: 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: 5Lemma 10. For a cycle π, if γ(π) is not strongly connected then there exists a non-empty I 1..p such that f I (x) def = i∈I λ i is a Lyapunov function for π, where λ λ λ stands for barycentric coordinates of x.

Proof. Let (x, x ′ ) ∈ Reach(π) and λ λ λ, λ λ λ ′ the corresponding barycentric coordinates. We must show that j∈I λ ′ j ≤ i∈I λ i . Let P be the matrix such that λ λ λP = λ λ λ ′ (it exists by virtue of Lemma 7). There exists a strongly connected component (SCC) I of γ(π) without incoming edges from other SCCs. After a change of indices putting those of I before those of its complement J, the matrix P takes the following form:

P = P I→I P I→J 0 P J→J .
If we decompose λ λ λ in (λ λ λ I , λ λ λ J ) and λ λ λ ′ in (λ λ λ ′ I , λ λ λ ′ J ) we get λ λ λ I P I→I = λ λ λ ′ I , and we are done since

j∈I λ ′ j = j∈I i∈I λ i P ij = i∈I λ i j∈I P ij ≤ i∈I λ i .
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 of the orbit graph, i.e. an SCC without incoming edges from other SCCs. According to the lemma, the state moves from the facet spanned by I towards other vertices of the region and cannot come back (see Fig. 4).

The next lemma describes the same Lyapunov function f I (x) in terms of the timed word read along a progress cycle π. Lemma 11. If π is a progress path terminating in some p-dimensional region r, then the clock vector x obtained after reading a timed word t × π (from any initial clock vector) is a function of t. Moreover, for any non-empty I 1..p, there exists an expansive affine function g such that f I (x) = g(t).

λ 1 λ 2 λ 1 λ 3 0.6 1 0.3 λ 2 0.2 0.8 0.1
Proof. Let m = |π|. We show that there exist coefficients α 1 , . . . , α m ∈ -p..p not all null and an integer constant c such that i∈I λ i = c + m j=1 α j t j . Up to a reordering of the clocks and a fusion of equal clocks we can suppose that the region r is

⌊x⌋ + {({x 1 }, . . . , {x p }) | 0 ≤ {x 1 } ≤ • • • {x p } ≤ 1} , where ⌊x⌋ = (⌊x 1 ⌋, . . . , ⌊x p ⌋).
Vertices of the region are s 1 = ⌊x⌋ + (0, . . . , 0), s 2 = ⌊x⌋ + (0, . . . , 1), s p+1 = ⌊x⌋ + (1, . . . , 1). Therefore x = 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-ix p+1-i . This last quantity is, in absolute value, the sum of all delays between resets of clocks x p+2-i and x p+1-i . Therefore every λ i (i ∈ 2..p) is of the form C i ± t j with C i ∈ Z. If 1 ∈ I then i∈I λ i is of the expected form. Otherwise, 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 non-zero coefficient because i∈I λ i is not constant (otherwise dimension of the region would be less than p).

Lemma 12. Let P ⊂ [0, M ] n . If there exist k indices 0 = i 1 < • • • < i k ≤ n
and k expansive affine functions g 1 , . . . , g k such that for all (t 1 , . . . , t n ) ∈ P :

1 ≥ g 1 (t 1 , . . . , t i1 ) ≥ g 2 (t i1+1 , . . . , t i2 ) ≥ • • • ≥ g k (t i k-1 +1 , . . . , t i k ) ≥ 0 then Vol(P ) ≤ M n-k k! .
Proof. We describe an affine change of coordinates φ : (t 1 , . . . , t n ) → (u 1 , . . . , u n ) with Jacobian determinant modulus |J(φ)| ≥ 1 and such that Vol(φ(P )) ≤ M n-k k! . Then the conclusion follows immediately:

Vol(P ) = |J(φ)| -1 Vol(φ(P )) ≤ Vol(φ(P )) ≤ M n-k k! . For l ∈ 1.
.k, the function g l has the following form

g l (t i l-1 +1 , . . . , t i l ) = c l + i l -i l-1 j=1 α j,l t i l-1 +j with |α j l ,l | ≥ 1 for some j l .
We can assume up to a permutation of coordinates (it does not change the volume) that j l = i l . The change of coordinates φ is defined as follows u i l ← g l (t i l-1 +1 , . . . , t i l ) for l ∈ {1, . . . , k} and the other coordinates remain unchanged:

u i ← t i . Every vector (u 1 , . . . , u n ) ∈ φ(P ) satisfies 0 ≤ u i1 ≤ • • • ≤ u i k ≤ 1 and u i ∈ [0, M ] for the other coordinates. Therefore Vol(φ(P )) ≤ M n-k k! .
It remains to prove that |J(φ)| ≥ 1. The Jacobian matrix is lower triangular thus the Jacobian determinant is the product of the entries in the diagonal. These entries are 1 (nk times) and the α i l ,l for l ∈ 1..k. We are done:

|J(φ)| = k l=1 |α i l ,l | ≥ 1.
Now we can state the key technical lemma of this section.

Lemma 13. Let π 1 , . . . , π k be k cycles of ∆ * such that µ(π 1 ), . . . , µ(π k ) are all equal to a same non-forgetful idempotent of M, then

V π1•••π k ≤ M n-k k! where n = |π 1 | + • • • + |π k |.
Proof. We remark that an idempotent orbit graph (thus equal to its transitive closure) is complete if and only if it is strongly connected. 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 some clock is not reset all along the path

π 1 • • • π k , thus P π1•••π k is in a simplex
of type 1 and the volume satisfies the inequality to prove. In the latter case, π 1 , . . . , π k are progress cycles with γ(π 1 ) = • • • = γ(π k ) a non strongly connected orbit graph. For l ∈ 1..k we denote by i l the index of the last transition of the l th cycle. By virtue of Lemma 10 there exists a set of indices I such that

1 ≥ f I (x 0 ) ≥ f I (x i1 ) ≥ • • • ≥ f I (x i k ) ≥ 0.
Moreover, by Lemma 11 there exist expansive affine functions g 1 , . . . , g k (each one corresponding to a cycle) such that f I (x i l ) = g 1 (t i l +1 , . . . , t i l ) for every l ∈ 1..k. Hence

1 ≥ g 1 (t 1 , . . . , t i1 ) ≥ g 2 (t i1+1 , . . . , t i2 ) ≥ • • • ≥ g k (t i k-1 +1 , . . . , t i k ) ≥ 0.
Hypotheses of Lemma 12 are satisfied, the conclusion follows.

Pumping lemma for long thick paths

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

Theorem 2 (pumping lemma). 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. We use Simon's theorem on factorization forests to factorize paths and find some repeated idempotent. Then, absence of forgetful cycles yields repetition of a non-forgetful idempotent along every path, which by Lemma 13 implies thinness.

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:

• a binary node labeled by a word π 1 • π 2 with two children labeled by the words π 1 and π 2 ;

• an 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 3 (Simon [START_REF] Simon | Factorization forests of finite height[END_REF]). If µ is a morphism from ∆ * 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. 13, thus their volume is very small, which implies that V π is also small. Lem. 14 below quantifies this "smallness" of V π as function of the length of π and height of its factorization forest, and Thm 2 follows immediately thereof.

Let LVol be the function defined on paths by LVol(π) = log V π -|π| log M . This function is subadditive 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. Lemma 14. For any height h, for any B > 0, there exists N h,B ∈ N such that for all n ≥ N h,B the inequality L(n, h) ≤ -nB holds.

Proof. We will define N h,B by induction on the height h. Let a be a factorization forest of height h with n leaves and π 1 , . . . , π k the children of the root. Let K = n 2N h-1,2B . We distinguish two disjoint cases: 1. There are more than K subtrees having less than N h-1,2B leaves. 2. There are less than K subtrees with less than N h-1,2B leaves. Here the juicy part (sons with enough leaves to satisfy induction hypothesis) has more than n 2 leaves.

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

LVol(π) ≤ log M n-k k! -n log M = -k log M -log k! ≤ -K log M -log K!,
which is upper bounded by -nB for n large enough.

• In the second case, for i ≤ k, we denote by n i the length of the path π i and by h i ≤ h -1 the height of its corresponding subtree. We can conclude using properties of LVol and the inductive hypothesis:

LVol(π) ≤ k i=1 LVol(π i ) ≤ k i=1 L(n i , h i -1) ≤ ni≥N h-1,2B L(n i , h i -1) ≤ -2B ni≥N h-1,2b n i ≤ -2B n 2 = -nB.
To conclude the proof of Thm 2, given η > 0, let C = log(η/M ) and h = h(M) the bound on height of factorization forest. Using Lem. 14, we obtain that a path longer than N h,C without forgetful idempotents cannot be η-thick.

Characterizing thick automata

In the theorem below we characterize thick automata with forgetfulness and give two other equivalent characterizations of thickness. We say that there is a limit cycle along π if there exists a clock vector x and a time sequence t such that x t,π --→ x. Given ε > 0, in ε-discrete limit cycles all the components of x and t should be multiple of ε.

Theorem 4 (characterizations of thickness). For a deterministic timed automaton in region split form, the following conditions are equivalent and define thick automata:

1. H > -∞; 2. there exists a forgetful cycle; 3. there exists a limit cycle; 4. there exists an ε-discrete 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 , x 0 )

(u1,w1) -----→ (q 1 , x 1 ) • • • (u d ,w d )
-----→ (q 0 , x 0 ) along some π ∈ ∆ d with u 1 , . . . , u d ∈ {ε, 2ε, . . . , M -ε} and such that all the x i are not on the frontier of regions and have discrete coordinates. First we can see that every clock has been reset at least once because any non-reset clock would augment during the run, which contradicts its cyclicity. Then for each n > 0 the polytope P π n is described by a set of in equations of the form A < k i=j t i < B (with ji ≤ d). Extending u periodically permits to have a word in

P π n such that A + ε ≤ k i=j u i ≤ B -ε for each of those inequations. Taking t i ∈ (u i -ε d , u i + ε d
) defines a hypercube included in P π n with the volume greater than ( 2ε d ) nd . Then

H(A) ≥ log 2ε d > -∞.
Proof (of 1 ⇒ 2). We notice first that a thick automaton has long thick paths.

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

Proof. We use the characterization of the entropy in terms of Vn = π∈∆ n V π given in Prop. 4. Let β = 2 H-1 . For n large enough, Vn ≥ β n . Let π be one of the paths of ∆ n of maximal volume, then Vn ≤ V π |∆| n and so if we pose η = β |∆| we have V π ≥ η n . Combining Lem. 15 with Thm 2 we find a required forgetful cycle.

Sankur et al. [START_REF] Sankur | Robust controller synthesis in timed automata[END_REF] established that given a BDTA, existence of a reachable forgetful cycle in its fleshy region-split form is PSPACE-complete. Hence, thickness of a BDTA is also a PSPACE-complete problem.

Operator approach

In this section, we develop an approach to volumes and entropy of languages of timed automata based on functional analysis. First, in 4.1, we recall the analogue in the case of finite automata, their adjacency matrices, their spectral properties and consequences on the size of their languages and their entropies. Then we adapt this approach to timed automata: in 2.5 we have characterized volume functions v n : S → R + by a recurrent equation. Below, in 4.2.1 we identify a functional space C( S) containing these functions. Next, we show that these volume functions can be seen as iterates of some positive integral operator Ψ on this space, applied to the unit function (Sect. 4.2.2). This makes it possible to deduce in 4.2.3 the second main theorem of this paper stating that the entropy equals the logarithm of the spectral radius of Ψ. Finally, we explore the properties of Ψ and establish that this operator has a spectral gap, which is crucial for numerical algorithms of Sect. 5.

Linear operators and finite automata

Here we recall a typical application of linear operators to finite automata and regular languages. More details can be found in [START_REF] Lind | An Introduction to Symbolic Dynamics and Coding[END_REF][START_REF] Seneta | Non-Negative Matrices and Markov Chains[END_REF].

Consider a deterministic finite automaton A = (Q, Σ, δ, q 1 , F ), with states q 1 , q 2 , . . . , q s such that every state is reachable from q 1 and F is reachable from any state. Let L be the language accepted, and L n its sublanguage containing all its words of length n. In most cases, its cardinality |L n | depends on n exponentially, and the entropy of L (or of A) is defined as the growth rate of this cardinality: H(L) = lim sup n→∞ log |Ln| n

. We recall how this entropy (which is an important size, information and compressibility measure) is related to linear operators.

Let L i,n be the set of all n-letter words accepted by A when starting at the state q i , and x i,n its cardinality. From usual language equations

L i,0 = {ε}, if q i ∈ F ∅, otherwise; L i,n+1 = (qi,a,qj )∈δ aL j,n
one passes to equations on cardinalities

x i,0 = 1, if q i ∈ F 0, otherwise; x i,n+1 = (qi,a,qj )∈δ x j,n ,
or, in vector notation, x 0 = 1 F and x n+1 = Ax n , with the vector x n = (x 1,n , . . . , x s,n ) ∈ R s and the s × s adjacency matrix A = (a i,j ) such that a i,j is the number of transitions in A leading from q i to q j . We conclude with the explicit formula for cardinalities: x n = A n 1 F . Thus size analysis of the automaton A is phrased as iteration of the linear operator A on R s . In particular, the entropy is the growth rate of the first coordinate x 1,n . Exploration of the matrix A is simplified by non-negativity of its elements. Using Perron-Frobenius theory, the entropy can be characterized as follows: Proposition 16. It holds that H(A) = log ρ(A), where ρ(A) stands for the spectral radius, i.e. the maximal modulus of eigenvalues of A.

Two decompositions

To insure that the iterations of A on any initial vector all have the same growth rate and converge to the same direction, the automaton must be decomposed, first, into strongly connected components, then into aperiodic components.

Examples: why to decompose. Consider first an example of the non-strongly connected automaton in Fig. 5, left. It has three strongly connected components. The matrix is A =   3 1 0 0 2 2 0 0 3   with two positive eigenvalues (3, which is double, and 2), and three positive eigenvectors (those of the standard basis). When we iterate the operator (i.e. compute A n x for some initial non-negative vector x), the growth rate can be 3 n (e.g. if we start with x = (1, 1, 1)), which corresponds to the spectral radius, but it can also be 2 n (if we start with x = (0, 1, 0)).

The second automaton, on the right of Fig. 5, is strongly connected but periodic. It has four eigenvalues with maximal modulus: 2; 2i; -2; -2i. Iterating the operator leads to a fast rotating sequence of vectors:

(1, 0, 0, 0) ⊤ , (0, 2, 0, 0) ⊤ , (0, 0, 4, 0) ⊤ , (0, 0, 0, 8) ⊤ , . . .

SCC decomposition.

The automaton A, considered as a graph, can be decomposed into strongly connected components. We will distinguish non-trivial components A c (containing a cycle) from transient states (i.e. single-state components without self-loops). For every A c , we consider the corresponding matrix A c (which is a submatrix of A, i.e. the matrix is obtained by selecting rows, then columns corresponding to states in A c ). Computation of the entropy of A reduces to those of A c thanks to the following result. Proposition 17. ρ(A) = max c ρ(A c ) and thus H(A) = max c H(A c ). Thus, we can restrict ourselves to the study of operators of strongly connected automata, which constitutes our first decomposition.

Periodic decomposition. Given a strongly connected automaton A, we define its period p as the greatest common divisor of the lengths of its cycles. Then the following decomposition is possible (see e.g. [START_REF] Denardo | Periods of connected networks and powers of nonnegative matrices[END_REF]). Proposition 18. The set Q can be split into p periodic components Q 0 , . . . , Q p-1 satisfying the following properties:

1. any path visits cyclically in turn all the components Q 0 , . . . , Q p-1 ; 2. hence, any path of length p starts and ends in the same component; 3. there exists a natural b such that any two states within the same Q i are connected by some path of length bp.

The space R s is naturally split into a direct sum of subspaces E i for i ∈ 0..p -1 corresponding to periodic components. Each E i consists of vectors in R s with coordinates vanishing outside of Q i . Operator A maps each E i to E i-1 mod p ; hence each E i is invariant under A p . We denote the restriction of A p to E i by A p i (which is a submatrix of A p ).

Re

Im λ ρ

Figure 6: Spectrum of an operator having a gap: the maximal eigenvalue ρ and a subset of the grey circle.

Proposition 19. For all i ∈ 0..p -1, ρ(A p i ) = ρ(A p ). We conclude that for a strongly connected automaton ρ(A) = ρ(A p ) 1/p = ρ(A p i ) 1/p for any i ∈ 0..p -1. Thus we can concentrate our effort on the operator restricted to one periodic component: A p i .

Spectral gap and its consequences

Consider now the operator for one periodic component B = A p i . It has particular properties. In terms of Perron-Frobenius theory it is irreducible. All its powers B n with n ≥ b (with b as in Prop. 18) are matrices with all positive elements. It follows from Perron-Frobenius theory that the operator B has a spectral gap β ∈ (0, 1), in the following sense (see Fig. Proposition 20. For any positive vector x:

• the vector B n x converges in direction to v;

• the ratio |B n+1 x|/|B n x| converges to ρ(B);

• the error in both cases converges in O((1β) n ).

The operator associated to a TA

Now we examine the case of BDTA, where we can define an operator similar to the adjacency matrix of a finite automaton.

The functional space of a TA

Here, the analogue to language cardinalities is the volume. Thus, in order to use the operator approach we first identify the appropriate functional space containing the volume functions v n . We already know from Lem. 3 that volumes are functions of S → R that are polynomial on each {q} × r q . This allows us to prolong them by continuity to the set S = q∈Q {q} × rq , so they can be considered as elements of the space C( S). We recall that C( S), endowed with the uniform norm u = sup ξ∈ S |u(ξ)|, is a Banach space.

We can compare two functions in C( S) pointwise, thus we write u ≤ v if ∀ξ ∈ S : u(ξ) ≤ v(ξ). For a function f ∈ C( S), we sometimes denote f (p, x) by f p (x). Thus, any function f ∈ C( S) can be seen as a finite collection of functions f p defined on entry regions rp of locations of A.

Defining the operator Ψ

Let us consider again the recurrent formula (4). It has the form v k+1 = Ψv k , where Ψ is the operator on C( S) defined by the equation: Ψf (q, x) = (q,a,g,r,q ′ )∈∆ x+τ ∈g f (q ′ , r(x + τ )) dτ.

(

) 5
We have also

v 0 = 1 F . Hence v n = Ψ n 1 F .
Proposition 21. The operator Ψ is a linear bounded positive operator on the Banach space C( S).

The problem of computing volumes and entropy is now phrased as studying iterations of the operator Ψ on the functional space C( S). The theory of positive operators guarantees, that under some hypotheses, v n is close in direction to a positive eigenvector v * of Ψ, corresponding to its leading eigenvalue ρ. Moreover, the values of v n will grow/decay exponentially like ρ n . The eigenvalue ρ and the corresponding eigenvector can be computed using natural iterative procedures. In the sequel we apply this general scheme to the operator Ψ, referring to the book [START_REF] Krasnosel'skij | Positive Linear Systems: The Method of Positive Operators[END_REF] when a result concerning positive operators is needed.

Characterization of the entropy of a TA

We can now relate the entropy of a timed automaton to its operator.

Theorem 5 (entropy and spectral radius). For a BDTA, H = log ρ(Ψ), where ρ(Ψ) stands for the spectral radius of Ψ.

Proof. By Prop. 4 we have:

H = lim n→∞ (log Vn )/n = lim n→∞ (log vn )/n.
Then we remark that vn = Ψ n (1): indeed, the function 1 (constant, equal to 1 everywhere) is the maximal function of norm 1 (we recall that f = 1 ⇔ sup (q,x)∈S |f (q, x)| = 1). Therefore for all n ∈ N, Ψ n = sup f : f =1 Ψ n (f ) = Ψ n (1) = vn . Using Gelfand's formula ρ = lim n→∞ Ψ n 1/n , we conclude that log ρ = lim n→∞ (log vn )/n = H.

Exploring the operator

Before establishing the existence of a spectral gap, we need to know a few more structural properties of the operator.

Path operators and their kernel form

Equation ( 5) can be rewritten as:

(Ψf ) q (x) = δ=(q,...,q ′ )∈∆ (ψ δ f q ′ )(x). ( 6
)
where for δ = (q, a, g, r, q ′ ) the operator ψ δ acts from the space C(r q ′ ) of continuous functions on the target region to the space C(r q ) on the source region. It is defined by the integral:

ψ δ f (x) = x+τ ∈g f (r(x + τ )) dτ.
Iterating [START_REF] Asarin | Toward timed theory of channel coding[END_REF], we obtain a formula for powers of operator Ψ

(Ψ k f ) q (x) = δ1...δ k from q to q ′ (ψ δ1 . . . ψ δ k f q ′ )(x). ( 7
)
For a path π = δ 1 . . . δ k ∈ ∆ k starting in a state q and leading to a state q ′ , we define ψ π = ψ δ1 . . . ψ δ k . This operator acts from C(r q ′ ) to C(r q ). Let D be the dimension of r q . When the path π satisfies the progress condition, for (x, x ′ ) ∈ r p × r q the polytope P (π, x, x ′ ), is either empty or of dimension (n -D), and we denote by v π (x, x ′ ) its (n -D)dimensional volume. We have the following representation of ψ π .

Theorem 6 (kernel form). When π is a progress path, the function v π is a kernel for ψ π :

ψ π (f )(x) = rq v π (x, x ′ )f (x ′ )dµ q (x ′ ).
The kernel v π is piecewise polynomial, strictly positive and continuous on Reach(π); it is zero outside of Reach(π).

The measure µ q (x ′ ) in the theorem is the d q -dimensional Lebesgue measure on r q , see Appendix B for more details and the proof of the theorem.

Example 1. Let us apply the theorem to the cycle of label ab of the automaton A 3 in Fig. 1. We have

x t1at2b ----→ x ′ if and only if (x, t 1 , t 2 , x ′ ) satisfies the set of inequations (I) = {0 < x < 1, 0 < t 1 , 0 < t 2 , x + t 1 < 1, t 1 + t 2 < 1} and x ′ = t 1 + t 2 .
We instantiate (I) with t 1 = x ′t 2 , and obtain the set of inequations

(I ′ ) = {t 2 < x ′ , 0 < t 2 , x + x ′ -1 < t 2 }. The kernel of ψ ab is v ab (x, x ′ ) = Vol{t 2 | (x, t 2 , x ′ ) |= (I ′ )} = min(x ′ , 1 -x). Thus ψ ab (f )(x) = 1 0 min(x ′ , 1 -x)f (x ′ )dx ′ = (1 -x) 1 1-x f (x ′ )dx ′ + 1-x 0 x ′ f (x ′ )dx ′ .
Remark that this theorem ensures that for a forgetful path π, like the cycle in the above example, v π (x, x ′ ) > 0 for all (x, x ′ ) in r p × r q .

Two decompositions again

Like in the discrete case (4.1.1), we decompose the automaton and the operator.

SCC decomposition. Given a region-split timed automaton A, it can be split into (non-trivial) strongly connected components A i and acyclic pathways between them. The entropy of a TA depends in a very natural way on the entropies of its SCCs. The following result mimics Prop. 17.

Proposition 22. The entropy of the language of A equals the maximal entropy of the languages of its non-trivial SCCs.

Proof. Let us denote by H max the maximal entropy of the SCCs and let it be reached on A i . As all paths of A i are paths of A, we have V Ai n ≤ V A n , and thus, according to Prop. 4, H max = H Ai ≤ H(A). For the converse inequality, let us fix some σ > 0. By definition of entropy, there exists an A > 0 such that in each subautomaton A i we have for all n:

Vn (A i ) ≤ A • 2 n(HA i +σ) ≤ A • 2 n(Hmax+σ) .
Realizable paths of A are all included in the following finite union of path languages:

m≤|SCC|; m k=0 l k ≤|∆|; ∀k,i k :SCC W m,ℓ ℓ ℓ,i with W m,ℓ ℓ ℓ,i = n1,••• ,nm∈N ∆ l0 ∆ n1 i1 ∆ l1 ∆ n2 i2 • • • ∆ nm im ∆ lm .
Sets ∆ i are subsets of ∆ used by corresponding A i . For any m, any ℓ ℓ ℓ and any i,

assuming k l k = l: V n (W m,ℓ ℓ ℓ,i ) ≤ |∆| l j nj =n-l Vnj (A ij ) ≤ |∆| l A • 2 (n-l)(Hmax+σ) .
Since there is a finite number of choices of m, ℓ ℓ ℓ and i, there is thus another constant A ′ > 0 such that Vn ≤ A ′ 2 n(Hmax+σ) . As σ is arbitrary, this means H(A) ≤ H max .

Thus, we can restrict ourselves to the study of operators of strongly connected automata, which constitutes our first decomposition. Since the entropy of thin SCCs is -∞, we will only consider thick components.

Periodic decomposition. Given a strongly connected (region-split fleshy) timed automaton A, we define its period p as the greatest common divisor of the lengths of its cycles. Then the location set Q can be split into p periodic components Q 0 , . . . , Q p-1 as in Prop. [START_REF] Gómez | Efficient detection of Zeno runs in timed automata[END_REF].

The set of entry states S is naturally split into components Si = q∈Qi {q} × rq and the Banach space C( S) becomes a direct sum of subspaces F i for i ∈ 0..p -1 corresponding to periodic components. Each F i consists of functions in C( S) vanishing outside of Si . Operator Ψ maps each F i to F i-1 mod p ; hence each F i is invariant under Ψ p . We denote the restriction of Ψ p to F i by Ψ p i .

Proposition 23. For a strongly connected timed automaton, the spectral radius of Ψ p coincides with spectral radii of each Ψ p i .

Proof. We denote by 1 i ∈ F i the function equal to 1 within Q i and 0 outside. By Gelfand's formula:

ρ(Ψ p i ) = lim k→∞ (Ψ p i ) k 1/k = lim k→∞ (Ψ p i ) k 1 i 1/k = lim k→∞ Ψ pk 1 i 1/k .
For any two i and j let d = ij + p. We have that Ψ d 1 i ∈ F j , and Ψ d 1 i ≤ Ψ d . Hence, it holds that Ψ d 1 i ≤ Ψ d 1 j . Thus, we obtain that

Ψ pk 1 i = Ψ 2p-d Ψ p(k-2) Ψ d 1 i ≤ Ψ 2p-d Ψ d Ψ p(k-2) 1 j = Ψ 2p Ψ p(k-2) 1 j .
Applying lim k→∞ (•) 1/k to both sides of the inequality we get that ρ(Ψ p i ) ≤ ρ(Ψ p j ). Since the latter holds for any i and j, the spectral radii for all the components ρ(Ψ p i ) should be equal to each other. As for the radius of Ψ p , on one hand Ψ p ≥ Ψ p 0 and thus ρ(Ψ p ) ≥ ρ(Ψ p 0 ). On the other hand, using again Gelfand's formula we obtain:

ρ(Ψ p ) = lim k→∞ (Ψ p ) k 1/k = lim k→∞ (Ψ p ) k 1 1/k = lim k→∞ max i Ψ pk 1 i 1/k = max i lim k→∞ ( Ψ pk 1 i ) 1/k = ρ(Ψ p 0 ).
We conclude that for a strongly connected timed automaton ρ(Ψ) = ρ(Ψ p ) 1/p = ρ(Ψ p i ) 1/p for any i ∈ 0..p-1. Thus we can concentrate our effort on the operator restricted to one periodic component: Θ = Ψ p i .

Spectral gap

It is well-known that computation of the spectral radius of an operator (as well as other convergence properties) is substantially simplified by the existence of spectral gap in the operator, as defined in 4.1.2. Here we show that every periodic component of the operator Θ = Ψ p i with p the period of the automaton has such a gap. This result will be used in the next section to ensure convergence of a numerical algorithm for entropy computation.

Theorem 7 (spectral gap). For any region-split strongly connected thick timed automaton A, the operator Θ has a spectral gap.

The proof of this result is quite technical, uses Perron-Frobenius theory for so-called acute operators as in [START_REF] Krasnosel'skij | Positive Linear Systems: The Method of Positive Operators[END_REF], and is based on the series of lemmata below, proved in Appendix C.

The idea of acuteness can be explained as follows. Let v be a non-zero vector in the functional space C( S), and let h be a non-zero covector (a functional) in the dual space C * ( S). The angle α between them can be naturally defined as follows:

cos α = h, v h • v with 0 ≤ α ≤ π
(for h and v two vectors in Euclidean R n this is the usual angle). For non-negative h and v, the angle is always between 0 and π/2.

A linear positive operator A : C( S) → C( S) is called acute if applying it to any non-negative non-zero h and v yields A * h and Av forming an angle smaller than some fixed acute φ. Formally, we say that A is acute with a cosine cos φ where φ ∈ (0, π/2) whenever

∀ non-zero h, v ≥ 0 : cos φ ≤ A * h, Av A * h • Av . ( 8
)
We are interested in acuity since it is a sufficient condition for existence of a spectral gap:

Lemma 24 ([15], Thm 12.3). A positive acute operator A with cosine cos φ has a gap of at least β = 1tan φ/2 (i.e. β = Ω(cos φ) whenever cos φ is small).

In order to prove that the operator Θ has a spectral gap we will first concentrate on two adjacent forgetful paths π 1 and π 2 , and prove that the angle between ψ * π1 h and ψ π2 v is acute, and its cosine admits an exponential lower bound.

Lemma 25 (angle between two forgetful paths). Let π 1 and π 2 be forgetful paths of length n from p to q and from q to r respectively. Let h ∈ C * (r p ) and v ∈ C(r r ) be both non-negative and non-zero. Then, for some α > 0 depending only on the automaton, the following inequality holds:

ψ * π1 h, ψ π2 v ψ * π1 h • ψ π2 v ≥ α n . ( 9
)
The full proof of this lemma can be found in Appendix C.1, but now we give a very rough idea of it. First we use the kernel form given by Thm 6 and obtain the following sufficient condition for [START_REF] Sankur | Robust controller synthesis in timed automata[END_REF]:

∀x ∈ r p , ∀z ∈ r r , rq v π1 (x, y)v π2 (y, z)dy rq v π1 (x, y)dy sup y∈rq v π2 (y, z) ≥ α n .
Then, for each timed run following the path π 1 π 2 from x ∈ r p to z ∈ r q , we consider separately its first part, over path π 1 , and its second part, over π 2 . We transform the first part so that it reaches a point inside some shrunk version r - q of the clock region at the end of π 1 , closer to its barycenter (it is important that this transformation does not change too much the volumes). Then we change its second part, making it start from the point of the shrunk region that would minimize path volumes over π 2 . After this transformation, the integral corresponding to the numerator splits into a product of two factors r - q v π1 (x, y)dy and min y∈r - q v π2 (y, z) proportional to the two factors of the denominator. Thus the fraction simplifies and we get the required estimate.

Next we need a simple consequence of our decomposition into periodic components:

Lemma 26. In any periodic component of a strongly connected and thick automaton, there exists a natural ℓ (multiple of the period), such that for every states p and q in this component there exists a forgetful path θ pq of length exactly ℓ.

Proof. Let σ be a forgetful cycle (its length is multiple of the period p), and let r be a state on this cycle within the aperiodic component considered. By Prop. 18, 3, for some natural b, every two states in the component are connected by a path of length bp. Thus we can go from p to r in bp steps, take the forgetful cycle σ, and go from r to q in bp steps. Thus we obtain a forgetful path of length 2bp + |σ| from p to q. This terminates the proof (with ℓ = 2bp + |σ|).

We call a path π of length n good if its last nℓ transitions form a forgetful path (where ℓ comes from the previous lemma). Of course, a good path is forgetful.

As we know from Eq. ( 7), restricted to one periodic component, the operator Θ n admits the following matrix representation:

(Θ n f ) p = ((Ψ p i ) n f ) p = p π -→q,|π|=np ψ π f q ,
where locations p and q belong to the periodic component Q i and f ∈ F i . We will split it into two operators: Θ n = Φ n + Ξ n where Φ n corresponds to good paths and Ξ n to bad ones.

The following lemma states that the huge majority of paths are good.

Lemma 27 (size of good and bad paths). The volume of bad paths is smaller than any exponent, while that of good ones is at least exponential:

• for every ι > 0 there exists N such that for all n > N it holds that Ξ n < ι n ;

• there exists ν > 0 and N such that for all n > N it holds that ρ(Φ n ) > ν n .

Proof. The first item is an immediate corollary of Thm 2. For the second item, we notice that, by Gelfand's formula, ρ(Φ n ) = lim k→∞ Φ k n 1/k , and thus we have to find an exponential lower bound for Φ k n . Let π be a forgetful cyclic path (which exists due to thickness), and let cp be its length. By Thm 4, there exists an ε-discrete limit cycle along this path, let t be the corresponding time sequence. We notice that for n large enough and arbitrary k any segment of length np in π nk will be good. Thus, π nk is a concatenation of ck good paths of length np. On the other hand, operator Φ ck n corresponds to all concatenations of ck good paths of length np. Hence,

Φ ck n ≥ ψ π nk = ψ π nk 1 = Vol P π nk .
The latter polytope contains the ε/d-ball centered at t nk (i.e. the time sequence t repeated nk times), and thus its volume is at least (2ε/d) cpnk . We conclude that

ρ(Φ n ) = lim k→∞ Φ ck n 1/ck ≥ (Vol P π nk ) 1/ck = (2ε/d) np .
We know from Lem. 25 that operators corresponding to two adjacent forgetful paths form an acute angle. It is possible to deduce that operator Φ n (which is a sum of many operators of forgetful paths) is also acute: Lemma 28 (good part is acute). The operator Φ n is acute, and its cosine admits an exponential lower bound: cos φ = Ω(γ n ) with some γ > 0.

We have thus decomposed the operator Θ n into an acute operator Φ n and a small operator Ξ n . By Lemma 24, Φ n has a spectral gap. We need a result from perturbation theory to establish that the influence of Ξ n on the spectrum is negligible and thus Ψ n A also has a gap. For an operator A having a gap β and spectral radius ρ, consider a ring on the complex plane: Γ = {ζ|(1 -3β/4)ρ ≤ |ζ| ≤ (1β/4)ρ} (see Fig. 7, right). By definition of the gap, all ζ in this ring do not belong to the spectrum of A, thus the resolvent operator (Aζ) -1 is well defined. Let δ be the maximal norm of this resolvent:

δ = sup ζ∈Γ (A -ζ) -1 .
Lemma 29 (small perturbation preserves spectral gap). Let A be a linear operator with gap β. Let B satisfy B < δ -1 . Then A + B also has a gap β/2. This is a well-known fact of perturbation theory (see e.g. [START_REF] Katō | Perturbation Theory for Linear Operators[END_REF]). It turns out that for an acute operator the parameter δ can be estimated.

Lemma 30 (resolvent norm for acute operators). Let A be a linear positive acute operator with cosine cos φ and spectral radius ρ. Then the parameter δ defined above satisfies δ = O((cos φ) -6 ρ -1 ).

Putting the previous lemmata together we obtain almost the required result.

Lemma 31. For a thick strongly connected BDTA A, there exists N such that for all n ≥ N the operator Θ n has a spectral gap. Proof. Indeed, the operator Θ n is decomposed as Φ n + Ξ n . Its forgetful part Φ n is acute with c = O(α n ) by Lem. 28, and thus has a spectral gap β = Ω(α n ) by Lem. 24. Thus, by Lem. 30, the parameter δ of Φ n satisfies δ -1 = Ω(α 6n ρ(Φ n )), and thus, using Lem. 27, δ -1 = Ω(α 6n ν n ). Using Lem. 27, for n large enough we can guarantee that Ξ n < δ -1 ; and by Lem. 29, Θ n = Φ n + Ξ n has a spectral gap β/2 = Ω(α n ).

Re

We have proved the gap property for the automaton operator in high powers: Θ n for n ≥ N . Based on the following lemma, we can deduce the same property for Θ. Lemma 32. Let A be a positive operator. If both operators A N and A N +1 have gaps then operator A also has a gap.

The statement of Thm 7 is now immediate.

Corollary 33. The spectral radius ρ(Ψ) is an isolated eigenvalue of Ψ.

Computing the entropy

The characterization of H in Thm 5 solves the main problem explored in this paper, but its concrete application requires computing the spectral radius of an integral operator Ψ, and this is not straightforward. In 5.1 we give an iterative procedure, which approximates the spectral radius and the entropy with a guaranteed precision; in 5.2 we find an exact solution of this problem for a subclass of automata by reduction to differential equations.

Iterative procedure

Let A be a positive aperiodic linear operator on C( S) with a gap larger than β. Our aim is to compute its spectral radius. For this we iterate the operator:

g 0 = 1; g n+1 = Ag n
(whenever A is the operator of a BDTA, g n = v n ). An approximation of the spectral radius can be computed as ρ n = g n+1 / g n . As stated in [15, (15.16)], for some constant C, the exponential error estimate |ρ nρ(A)| < C(1β) n holds. Combining with the results of Sect. 4 we obtain the algorithm to compute the entropy of a timed automaton presented in Table 1. We summarize with the following result: Theorem 8 (convergence). The algorithm in Table 1 computes the entropy of a BDTA with an exponentially small error (w.r.t. the number of iterations n).

1. Transform A into the fleshy region-split form. 2. Decompose it into strongly connected components A c . 3. For every thick A c , find its operator Ψ c and period p c . 4. Compute the sequence of functions g c,0 = 1; g c,n+1 = Ψ pc c g c,n . 5. Compute the approximations ρ c,n = g c,n+1 / g c,n . 6. Compute H = max c {log ρ c /p c } ≈ max c {log ρ c,n /p c }.

n gn(x) = v (ab) n (x) gn ρn-1 (log ρn-1)/2 0 1 1 1 1 -x -(1 -x) 2 /2 1/2 0.5 -0.5 2 (1 -x)/3 + (1 -x) 4 /24 -(1 -x) 3 /6
5/24 0.41667 -0.6315 3 Example 2. Applying the method to the running example, we first restrict the study to the cycle ab, which is the only non-trivial strongly connected component. Its period is 2 and thus we must compute Ψ 2n (1) for n = 0, 1, 2, . . . restricted to one periodic component p (or q). Table 2 contains the four first iterations of Ψ 2 .

2 15 (1 -x) -(1 -x) 6 /720 + (1 -x) 5 /120 -(1 -x) 3 /18 61/720 0.40667 -0.6490 4 17 315 (1 -x) + (1 -x) 8 /40320 -(1 -x) 7 /5040+ (1 -x) 5 /360 -(1 -x) 3 /
In this table we present

g n (x) = Ψ 2n (1)(p, x) = ψ (ab) n (1)(x) = v (ab) n (x), its norm and ρ n-1 = g n / g n-1
(which is an approximation of ρ(Ψ 2 ) = ρ(Ψ) 2 . This yields the following approximation of the entropy H ≈ (log ρ 3 )/2 ≈ -0.6512, which is close to the true value (see 5.2.1 below) H = log(2/π) ≈ -0.6515.

Case of "1 1 ⁄2-clock" automata

We consider now the class of 1 1 ⁄2-clock automata which are defined as (fleshy region-split) timed automata where the entry regions of all the locations have dimension at most 1 (a simple sufficient condition for being 1 1 ⁄2-clock is that in every transition, at most one clock is not reset). Volume functions of such automata only have one scalar variable, which makes them easier to analyze by symbolic methods. In [START_REF] Ehrenborg | Descent pattern avoidance[END_REF] a similar approach is applied to a spectral analysis of a (slightly simpler) operator related to a combinatorial problem.

Computing the entropy of the running example symbolically

To get some intuition on computing the entropy of 1 1 ⁄2-clock automata, we consider first A 3 of Fig. 1. As before, we work on its fleshy region-split form, as presented on Fig. 3. By symmetry, the volume of a path of length n ∈ N is the same function v n in both non-initial states. Thus v n is characterized by:

v 0 (x) = 1 v n+1 (x) = (Ψv n )(x) = 1-x 0 v n (t)dt.
According to Thm 5, the entropy can be found as log ρ(Ψ), and by Cor. 33 ρ(Ψ) is the maximal eigenvalue of Ψ. Let us write the eigenvalue equation:

λv(x) = 1-x 0 v(t)dt. (10)
Differentiating it twice w.r.t. x we get:

λv ′ (x) = -v(1 -x); (11)
λ 2 v ′′ (x) = -v(x).
The solutions of the latter have the form v(x) = α sin(x/λ) + β cos(x/λ). Using [START_REF] Asarin | Generating functions of timed languages[END_REF] with x = 1 we find v(1) = 0. We inject this in [START_REF] Basset | A maximal entropy stochastic process for a timed automaton[END_REF] for x = 0 and deduce α = 0. Thus v(x) = β cos(x/λ) and cos(1/λ) = 0. Non-zero eigenfunctions of Ψ exist if and only if the differential equation has non-zero solutions, i.e. if and only if λ = 2/((2k + 1)π) with k ∈ Z. The λ with highest modulus is 2/π and we can verify that indeed v : x → cos(xπ/2) satisfies (2/π)v = Ψv. Therefore ρ(Ψ) = 2/π, and the entropy of this automaton is log(2/π).

5.2.2. The theory of 1 1 ⁄2-clock BDTA As we will see below, the method hinted by the example can be generalized to all 1 1 ⁄2-clock BDTA: an integral equation on eigenvalues can be transformed into a differential one and solved.

Theorem 9 (symbolic method for 1 1 ⁄2-clock BDTA). The algorithm in Table 3 yields a symbolic characterization of the entropy of a 1 1 ⁄2-clock BDTA as the logarithm of the maximal root of a transcendental equation.

Notice first that the set of entry states S is now a disjoint union of intervals and singleton points (regions of dimension 1 and 0). Thus we split the set of locations Q into Q 0 and Q 1 , with Q i the set of locations q such that r q has dimension i.

It is convenient to choose as a scalar coordinate (ranging in (0, 1)) in each of the one-dimensional regions r q the fractional part of a non-zero coordinate of x (which is the same for all non-zero coordinates of x ∈ r q ). In regions r q of dimension zero, we introduce a fictitious coordinate ranging in (0, 1). This change of variables transforms any function f ∈ C( S) into a |Q|-dimensional vector of functions f q ∈ C(0, 1) such that f q (x) = f (q, x), where x ∈ r q and x is the scalar coordinate of x as described above (by convention, f q is a constant function for q ∈ Q 0 ). We denote then by F = (f q ) q∈Q the vectorial form thus obtained for f . Using such a notation with scalar coordinates, we can give a more explicit form to the operator Ψ.

Lemma 34 (explicit form of Ψ for a 1 1 ⁄2-clock BDTA). There exist four integer square matrices, (D ij ) (i,j)∈{a,b}×{1,2} , such that Ψ (in scalar coordinates) has the following form:

(ΨF )(x) = D a1 1-x 0 F (t)dt + D b1 1 1-x F (t)dt +D a2 1-x 0 F (x + t)dt + D b2 0 -x F (x + t)dt. (12)
Elements of matrices D are the numbers of transitions of various types in the BDTA, as briefly described in Fig. 8. More explanations can be found in Appendix D.1.

Computing the entropy of the language of the automaton using Thm 5 involves finding the leading eigenvalue of Ψ, that is the greatest λ ∈ R such that for some non-zero function f ∈ C( S), Ψf = λf . Equivalently we seek the greatest λ ∈ R such that some non-zero function F ∈ C(0, 1) Q satisfies ΨF = λF.

The first step toward solving this equation is to reformulate it as an equivalent integral equation on F and its mirror function F (the mirror of a function f , defined on (0, 1), is the function f , also defined on (0, 1), such that f (x) = f (1x)), where only x (and no more 1x) appears as upper bound of an integration interval.

Lemma 35. F = 0 is an eigenfunction of Ψ if and only if Y = F F is a solution of:

λY (x) = A x 0 Y (u)du + B 1 0 Y (u)du ( 14
)
with A = D b2 -D a2 D b1 -D a1 D a1 -D b1 D a2 -D b2 and B = D a2 D a1 D b1 D b2 . C 0 q C + q 1 2 1 2 r q a a b b
C 0 q : clocks null in r q C + q : clocks positive in r q Figure 8: Classifying transitions in 1 1 ⁄2-clock automata. For guards of type a clocks in C + q have a higher fractional part than clocks in C 0 q ; and for type b the opposite is true. Resets of type 1 reset all clocks in C 0 q ; and those of type 2 reset all clocks in C + q . The coefficient (p, q) of matrix D ij is the number of transitions from p to q with guard of type i and reset of type j.

Proof. We start from characterization [START_REF] Lind | An Introduction to Symbolic Dynamics and Coding[END_REF], use formula [START_REF] Basset | Counting and generating permutations using timed languages[END_REF], and make a simple change of variables:

λF (x) = (ΨF )(x) = D a1 1-x 0 F (t)dt + D b1 1 1-x F (t)dt + D a2 1 x F (t)dt + D b2 x 0 F (t)dt = D a1 1 x F (t)dt + D b1 x 0 F (t)dt + D a2 1 x F (t)dt + D b2 x 0 F (t)dt.
Splitting the integrals To prove that (12) also implies the |Q| last lines of ( 14) it suffices to replace x by 1x in the reasoning above, this changes index a into b and 1 into 0.

The next lemma, proved in Appendix D.2, states that integral equation ( 14) can be rewritten as a differential one with a couple of special additional conditions, involving a |Q| × |Q|-matrix defined as

M λ = D a1 + D b2 D a2 + D b1 0 -1 2 exp u λ A du I I -λI. ( 15
)
Lemma 36. The solutions Y of the integral equation ( 14) of the form F F are exactly the solutions of the

differential equation λY ′ = AY satisfying Y (1/2) = X X with X ∈ ker M λ .
We conclude with the characterization of the point spectrum of Ψ.

Corollary 37. The eigenvalues and eigenvectors of Ψ for a 1 1 ⁄2-clock BDTA are as follows:

• λ is an eigenvalue if and only if det M λ = 0;

• F is an eigenfunction if and only if

F (x) = I 0 exp (x-1/2)A λ X X with nonzero X ∈ ker M λ .
This gives a characterization for the entropy.

Corollary 38. The entropy of a 1 1 ⁄2-clock BDTA is the logarithm of the solution of det M λ = 0 with the highest modulus (such a solution is always a real number).

Proof (of Thm 9). det M λ = 0 is a transcendental equation on λ that we know to have an isolated maximal real solution ρ(Ψ) (due to Cor. 33), to be computed numerically. We can thus devise the algorithm for computing H = log ρ(Ψ) depicted in Table 3.

1. Transform A into the fleshy region-split form and check that it has 1 1 ⁄2clocks.

2. Compute the matrices A and B as in Lemma 35.

3. Compute exp ((x/λ)A), its integral, and build the matrix M λ defined by [START_REF] Krasnosel'skij | Positive Linear Systems: The Method of Positive Operators[END_REF]. 4. Find the greatest root ρ (w.r.t. the unknown λ) of det(M λ ) = 0. 5. Return H(L(A)) = log ρ.

Conclusions and further work

In this paper, we have defined size characteristics of timed languages: volume and entropy. The entropy has been characterized as logarithm of the leading eigenvalue of a positive operator on the space of continuous functions on a part of the state space. Properties of the operator have been analyzed, and based on these properties two procedures have been suggested to compute the entropy.

Research in this direction is recent; nonetheless, based on the concepts presented in this paper, we have obtained several other results. In [START_REF] Basset | Dynamique Symbolique des Langages Temporisés Réguliers[END_REF][START_REF] Basset | Volumetry of Timed Languages and Applications[END_REF], dynamical systems are associated to timed languages, and their entropy-like characteristics are related to the entropy of timed languages; in [START_REF] Asarin | Volume and entropy of regular timed languages: Discretization approach[END_REF] the entropy of timed languages is related to Kolmogorov complexity of timed words. These works suggest that this entropy is a relevant information measure, which is confirmed in [START_REF] Asarin | Toward timed theory of channel coding[END_REF] where we sketch an application of entropy of timed languages to transmission of timed data over a constrained channel. In [START_REF] Asarin | Generating functions of timed languages[END_REF] we adapted our methods to a more precise size analysis of timed languages: characterization and computation of generating functions of volumes.

Many questions still need to be studied. We are planning to explore practical feasibility of the procedures described here and compare them to each other. We believe that, as usual for timed automata, they should be transposed from regions to zones. Applications to information transmission and compression of timed data will follow. Practical estimation of entropy remains a challenge. On the theoretical side, it would be interesting to find the amount of information per time unit (in this paper, we measure information per event). We believe that operator methods will be extensively used in research on timed and data automata, and their probabilistic versions. The second lemma permits to upper bound the volume of any polytope associated to a path π ′ by the volume of the polytope corresponding to its two-sided extension ππ ′ π ′′ . Lemma 40. Let ππ ′ π ′′ be a path of length n and k

r p Vol(r p ) = 1 dp! x x t V π P π = ∪ x∈rp P π (x) P π (x) v π (x) Z π
= |π| + |π ′′ | then n! (n+k)! V π ′ ≤ V ππ ′ π ′′ .
Proof. The proof is based on the following "folklore" result: for any path π the set of date vectors

P date π = {(d 1 , . . . , d n ) | (d 1 , d 2 -d 1 , . . . , d n -d n-1 ) ∈ P π }, (A.1)
corresponding to delay vectors in P π , is a zone (with the same volume P π ). The zone P date π ′ is a projection of P date ππ ′ π ′′ and the statement follows from Lem. 39.

Next we compare different volumes associated to a path in the lemma below, where µ p (x) stands for the Lebesgue measure on the region r p adapted to its dimensionality, see the following example. Example 3. Let r q be defined by the clock constraint 0 = x 1 < x 2 -1 = x 3 -1 < x 4 -2 < 1, then natural coordinates in r q are x 2 and x 4 ; Lebesgue measure satisfies dµ q (x) = dx 2 dx 4 and thus rq f (x)dµ q (x) =

2 1 3 x2+1 f (0, x 2 , x 2 , x 4 )dx 4 dx 2 . Lemma 41. If π is a path of length n starting in a region r p then n! (n + d p )! V π (1)
≤ rp v π (x)dµ p (x) (2)
≤ 1 d p ! sup x∈rp v π (x) (3) ≤ 1 d p ! V π .
Proof. Let us associate to any path π the polytope Z π = ∪ x∈rp {x} × P π (x) (see Fig.

A.9). The inequality to prove compares several volumes related to this polytope: V π is the volume of P π -projection of Z π on t; the function v π (x) corresponds to the volume of P π (x) -the cross-section of Z π for a fixed value of x; and the integral of v π is the volume of Z π itself. The inequality (3) comes from language inclusion: for all x ∈ r p , P π (x) ⊂ P π and thus, for their volumes v π (x) ≤ V π . The inequality (2) holds since 1 dp! = rp 1dµ p (x) is the volume of r p .

The inequality (1) follows from Lem. 39 applied to the n-dimensional zone P date π (defined by (A.1)) and the n + d p -dimensional Z date π , which is obtained from the polytope Z π by changing coordinates to d -dp , . . . , d -1 , d 1 , . . . , d n linked to π as follows. The d i for positive i are the dates of the zone P date π . We denote by x 1 > x 2 > • • • > x dp the d p affinely independent clock values in r p . For i ∈ 1..d p we define d -i = -x i < 0 (informally, d -i records the last date in the past when the clock x i was reset).

Example 4. The polytope Z π associated to the cycle ab of the running example is Z ab defined by 0 < x < 1, 0 < t 1 , t 2 , x + t 1 < 1 and t 1 + t 2 < 1. In that case d

-1 = -x, d 1 = t 1 and d 2 = t 1 + t 2 . Thus, (d -1 , d 1 , d 2 ) ∈ Z date ab iff -1 < d -1 < 0 < d 1 < d 2 < 1, and d 1 -d -1 < 1.
Proof (of Prop. 4). The sequence log Vn is sub-additive since for all n, m ≥ 0, Vn+m ≤ Vn Vm . By Fekete's Lemma on sub-additive sequences [START_REF] Fekete | Über die Verteilung der Wurzeln bei gewissen algebraischen Gleichungen mit ganzzahligen Koeffizienten[END_REF] we deduce that (log Vn )/n admits a limit in R = [-∞, +∞] and the first item is proved. It remains to prove two equalities:

lim sup n→∞ (log V n )/n (1) = lim n→∞ (log Vn )/n (2) = lim n→∞ (log vn )/n. The inequality (1,≤) follows from V n = q0 π -→F V π ≤ π∈∆ n V π = Vn .
In order to show the converse inequality we choose for each location p ∈ Q a path π →p leading there from the initial state (q 0 , 0) and a path π p→ that leads from p to a final location (the length of such paths can be bounded by |Q|). For every path π (from p to q, of length n), the path π = π →p ππ q→ is accepting and, by Lem. 40, satisfies

n! (n+2|Q|)! V π ≤ V π .
Summing over all the paths π of length n we obtain the inequality n! (n+2|Q|)! Vn ≤ π∈∆ n V π . On the other hand, for fixed p and q, and for all π from p to q of length n, paths π are accepting and distinct; thus To prove the other equality, we sum in Lem. 41 over all paths π of length n and obtain:

π∈∆ n ;p π -→q V π ≤ V n+i with i = |π →p | + |π q→ | ≤ 2|Q|. Summing over all p and q we get π∈∆ n V π ≤ |Q| 2 max i≤2|Q| V n+i . Thus n! (n+2|Q|)! Vn ≤ |Q| 2 max i≤2|Q| V n+i
n! (n+d)! Vn ≤ |Q| vn ≤ |Q| Vn (we recall that d = |C| is the number of clocks). Finally, taking lim n→∞ log(•)/n of each term, we get, by the "squeeze theorem", the required equality (2). ∀x ∈ r p ∀z ∈ r r y∈rq,σ v π1 (x, y)dy min y∈rq,σ v π2 (y, z) y∈rq v π1 (x, y)dy max y∈rq v π2 (y, z) ≥ α n , this new sufficient condition can, at last, be split in the following way:

∀x ∈ r p ∀z ∈ r r v π1 (x, r q,σ ) v π1 (x, r q ) min y∈rq,σ v π2 (y, z) max y∈rq v π2 (y, z) ≥ α n .
First we look at the variations of the volume function of π 2 :

Proposition 44. min y∈rq,σ v π2 (y, z) ≥ σ n max y∈rq v π2 (y, z).

Proof. We choose y min ∈ r q,σ and y max ∈ rq such that min y∈rq,σ v π2 (y, z) = v π2 (y min , z) and max y∈rq v π2 (y, z) = v π2 (y max , z). Let y 0 ∈ R dq be such that (1σ)y 0 + σy max = y min . Observe that, because y min ∈ r q,σ , the barycentric coordinates λ 0 i of y 0 satisfy λ 0 i =

λ min i -σλ max i 1-σ
> 0 and therefore y 0 actually lies in r q . We can thus choose t 0 ∈ P π2 (y 0 , z) and define the homothety h 2 : t → (1σ)t 0 + σt.

Notice that if t ∈ P π2 (y max , z), then h 2 (t) is necessarily a time vector going from y min to z (the origin of the convex combination of time vectors is the convex combination of the origins with same coefficients). In other words, h 2 [P π2 (y max , z)] ⊂ P π2 (y min , z) and thus, by Lem. 43, we obtain: σ n-dr v π2 (y max , z) ≤ v π2 (y min , z) and a fortiori the sought inequality.

We just showed that restricting the region r q to a smaller subset r q,σ ensures that variations of the volume function on this set are small enough. Now we need to verify that the restriction to r q,σ does not make v π1 (x, r q,σ ) too small in comparison to v π1 (x, r q ). Proposition 45. v π1 (x, r q ) ≤ (1 -(1 + d)σ) n v π1 (x, r q,σ ).

Proof. Let c be the center of r q : c = 1 1+dq dq i=0 s i (it is in r q,σ for all σ such that r q,σ = ∅). We choose t 0 in the interior of P π1 (x 0 , c) for some x 0 ∈ r p (such a t 0 exists because of forgetfulness) and define the homothety h 1 : t → (1γ)t + γt 0 , for some γ. It follows that h 1 [P π1 (x)] ⊂ (1γ)P π1 (x) + γP π1 (x, c).

We define the polytope P σ π (x)

def = {t ∈ R | x t,π1
--→ r q,σ } and remark that Vol(P σ π (x)) = v π1 (x, r q,σ ). Remark that P π1 (x) is the set of time vectors starting from x and going into r q = int(r q,0 )

= { dq i=0 λ i s i | ∀iλ i > 0 ∧ dq i=0 λ i = 1}. It follows that h 1 [P π1 (x)] is a set of time vectors starting from x and going into { dq i=0 ((1 -γ)λ i + γ 1 1+dq )s i | ∀i λ i > 0 ∧ dq i=0 λ i = 1}, which, provided that ∀i, (1 -γ)λ i + γ 1+dq ≥ σ (in particular, for γ = (1 + d)σ), is included in { dq i=0 λ i s i | ∀i λ i ≥ σ ∧ dq i=0 λ i = 1} = r q,σ . Then h 1 [P π1 (x)]
becomes a set of time vectors starting from x going into r q,σ , which means h 1 [P π (x)] ⊂ P σ π (x), and by Lem. 43:

(1 -(1 + d)σ) n v π1 (x, r q ) ≤ v π1 (x, r q,σ ).
Proof (of Lem. 25). Combining the inequalities established in Prop. 44 and 45, we find that the result announced in Lem. 25 holds for α

= σ -(1 + d)σ 2 .
As this is true for all σ in [0, 1 1+d ), this is in particular true for the σ that maximizes α, i.e. 1 2(1+d) . Thus the best lower bound we can guarantee, under our approximations, for the cosine of the angle between ψ * π1 and ψ π2 is

C.2. Proof of Lemma 28

We first need to prove that the norm of Φ n v in different locations does not change too much from location to location. Lemma 46. There exists β > 0 and N such that for all n > N and any non-negative and non-zero v ∈ C( S) the following inequality holds:

min p (Φ n v) p / max p (Φ n v) p > β n .
Proof. First we find an upper bound for (Φ n v) p . Let ℓ be the constant from Lem. 26. Every good path from p of length np can be decomposed into a prefix of length ℓ and a forgetful suffix of length npℓ. This yields the following decomposition (here π ranges over paths of length ℓ from p to s, and ̟ over forgetful paths of length npℓ from s):

(Φ n v) p = s,π ψ π w s , where w s = ̟ ψ ̟ v.
The sum over s contains |Q| terms, let s 0 be the index of the maximal one. Then

(Φ n v) p ≤ |Q| π ψ π w s0 ≤ |Q| ℓ M ℓ w s0 = C 1 w s0 ,
with some constant C 1 (here we used the facts that there are at most |Q| ℓ-1 possible π and that always ψ π ≤ M ℓ ). We conclude that for any p ∈ Q there exists

s 0 ∈ Q such that (Φ n v) p ≤ C 1 w s0 . (C.1)
Next we find a lower bound for (Φ n v) p . Let θ = θ p1s0 be as in Lem. 26. For any choice of s 0 , we have that (Φ n v) p = s,π ψ π w s ≥ ψ θ w s0 (a sum is greater than one term). Let now R be the region of s 0 , and R σ the shrunk region as in the proof of Lem. For y in R σ , the first minimum is bounded from below by some positive constant c 1 . Indeed, all the |Q| 2 paths θ pq given by Lem. 26 are forgetful, thus their operators have kernels strictly positive on R σ , and we can take c 1 = min p,q,y∈Rσ v θpq (x 0 , y) > 0 By Prop. 44, the second minimum admits the lower bound: min y∈Rσ w s0 (y) ≥ σ np-ℓ w s0 . Finally the volume of the shrunk region is Vol(R σ ) ≥ σ |Q| /|Q|! = c 2 . Thus we can conclude that (for any s 0 )

(Φ n v) p ≥ c 1 • σ np-ℓ • c 2 ≥ cσ np w s0
for some positive c. Comparing this lower bound on (Φ n v) p with the upper bound (C.1) we get the required result.

Proof (of Lemma 28). In the following chain of inequalities, π 1 ranges over good paths of length n from p to q, and π 2 over good paths of length n from q to r:

Φ * n h, Φ n v = p,q,r π1 ψ * π1 h p , π2 ψ π2 v r = p,q,r π1,π2 ψ * π1 h p , ψ π2 v r (1)
≥ α n p,q,r π1,π2

( ψ * π1 h p ψ π2 v r ) = α n q p,π1 ψ * π1 h p r,π2

ψ π2 v r (2)
≥ α n q p,π1 ψ * π1 h p r,π2

ψ π2 v r = α n q ( (Φ * n h) q (Φ n v) q ) (3)
≥ α n min q (Φ n v) q q (Φ * n h) q = α n min q (Φ n v) q Φ * n h

≥ α n β n max q (Φ n v) q Φ * n h = (αβ) n Φ * n h Φ n v .

Proof (of Lem. 30). Let β be 1tan φ/2 as in Lem. 24. Take ζ ∈ Γ, by Lem. 24 it does not belong to the spectrum of A, the resolvent (Aζ) -1 is thus a bounded linear operator and we have to estimate its norm. Let x and y be such that x = (Aζ) -1 y, i.e. Axζx = y, we must estimate x knowing y . We project the last inequality to spaces F 0 and F 1 by applying projectors Q and P : where the constant c is as defined in (C.4). We can rephrase (C.8) for all even powers:

A 2m y 0 ≤ K even ρ 2m (1β) 2m y 0 , with K even = (1 + (cos φ) -1 )(cos φ) -2 (tan(φ/2)) -2 . Using the bound (C.3) on A we propagate this bound to odd powers:

A 2m+1 y 0 ≤ A A 2m y 0 ≤ ρ(cos φ) -1 K even ρ 2m (1β) 2m y 0 = K odd ρ 2m+1 (1β) 2m+1 y 0 , with K odd = K even (cos φ) -1 (tan(φ/2)) -1 . We conclude with an estimate for all powers:

A n y 0 ≤ Kρ n (1β) n y 0 , (C.9)

with K = max(K even , K odd ). When cos φ is small, K = O(β -4 ). From (C.5) it follows that x 0 = (Aζ) -1 y 0 = -ζ -1 ∞ n=0 ζ -n A n y 0 , which yields, using (C.9), Let, as on Fig. 8, C + q be the set of clocks that were initially positive in the entry region reg q and C 0 q the others (initially null). Concerning [r], we remark that transitions of a 1 1 ⁄2-clock BDTA going from a state q can be of two types: either all clocks in C + q (type 1 ), or all clocks in C 0 q are reset (type 2 ). Then, for transitions of type 1, [r](x, t) = t and, for transitions of type 2, [r](x, t) = x + t. Note that transitions resetting all clocks could be considered as either type and actually, in this case, the target entry region has dimension 0 thus f is a constant and the form of [r] is irrelevant. To fix our terminology, we choose the convention that transitions resetting all clocks are of type 1.

Concerning [g], we observe that after entering a location q ∈ Q 1 , as time elapses (i.e. as τ progresses), non-degenerated regions of two types are visited alternately: regions where clocks in C + q have greater fractional part than initially null clocks (type a) and regions where it is the opposite (type b). We recall that in region-split BDTA, guards correspond to regions. So here g is either of type a or b. If g is of type a, then x + τ ∈ g is equivalent to τ ∈ (k, k + 1 -{x}), for some k ∈ N, i.e. [g](x) = (0, 1x). Otherwise, if g is of type b, then this constraint is equivalent to τ ∈ (k + 1 -{x}, k + 1), i.e. [g](x) = (-x, 0) or [g](x) = (1x, 1) (we choose the one which makes [r](x, t) stay in (0, 1)).

When coming from a state q ∈ Q 0 , this alternation does not exist and x + τ ∈ g is always equivalent to τ ∈ (k, k + 1). We could thus define a type c for transitions from Q 0 , but it is easy to see that a guard of type c would be the union of two adjacent guards of type a and b (where the value of x does not matter). This is why we do not use type c explicitly in the formulas below but, instead, count transitions from Q 0 twice: once as type a and once as type b.

The two criteria (type 1 vs type 2 and type a vs type b) can be combined in four different ways, covering the set of transitions starting from q into as many subsets: ∆ = (i,j)∈{a,b}×{1,2} ∆ ij (this union is almost disjoint: only transitions of type c appear in two subsets). Hence [Ψ] qq ′ can now be written the following way (with the change of variable t = τk):

([Ψ] qq ′ f )(x) =
(q,a,g,r,q ′ )∈∆a1 1-x 0 f (t)dt + (q,a,g,r,q ′ )∈∆ b1 1 1-x f (t)dt + (q,a,g,r,q ′ )∈∆a2

1-x 0 f (x + t)dt + (q,a,g,r,q ′ )∈∆ b2 0 -x f (x + t)dt.

Finally we define the square matrices D ij as (|{(q, a, g, r, q ′ ) ∈ ∆ ij }|) (q,q ′ )∈Q×Q and we obtain the required form for the matricial operator Ψ.

D.2. Proof of Lemma 36

As a preliminary we define the matrix S = 0 (iii) assuming λY ′ = AY and Y (1/2) = X X , Eq. ( 14) is equivalent to X ∈ ker M λ .

I
Proof. (i) Just differentiate [START_REF] Chomsky | Finite state languages[END_REF] with respect to x.

(ii) The general solution of λY ′ = AY can be written in the following form:

Y (x) = exp (x -1/2)A λ Y (1/2).
Using properties of S (equality (1) below) and Y (1/2) = SY (1/2) (equality (2)) we obtain

SY (x) = S exp (x -1/2)A λ Y (1/2) (1)
= exp (1/2x)A λ SY (1/2)

(2)

= Y (x).

(iii) Eq. ( 14) holds if and only if A

x 0 Y (t)dt + B 1 0 Y (t)dt -λY (x) = 0. We will rewrite the left-hand side using our two constraints on Y . First we integrate λY ′ = AY , developing at the point 1/2: λY (x) = λY (1/2) + A

1 10 3

 110 Our main problem: size of timed languages . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Classical works: entropy of regular languages . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 On techniques used . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.4 Our main results on entropy of timed languages. . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.5 Our second problem: ruling out pathologies in timed automata . . . . . . . . . . . . . . . . . 4 1.6 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.7 Paper organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2 Problem statement 5 2.1 Geometry, volume and entropy of timed languages . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Bounded deterministic timed automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.3 Three examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.3.1 Rectangles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.3.2 A product of trapezia . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.3.3 Our favorite example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.4 Preprocessing timed automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.5 Recurrent equations on volume functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.6 Other volumes, same entropy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . The thin-thick alternative and its consequences 3.1 Thinness, simplices and examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2 Point to point reachability: algebraic characterization . . . . . . . . . . . . . . . . . . . . . . 3.2.1 Monoid of orbit graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2.2 Adding clock resets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2.3 Orbit graphs and reachability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2.4 Other particular cycles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.3 Linear Lyapunov functions and sub-exponential volume . . . . . . . . . . . . . . . . . . . . . 3.4 Pumping lemma for long thick paths . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.5 Characterizing thick automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  ∈ [0, 1]/x := 0 b, y ∈ [1, 2]/y := 0

Figure 1 :

 1 Figure 1: Six simple timed automata: first line -A 1 , A 2 , A 3 , second line -A 4 , A 5 , A 6

Figure 3 :

 3 Figure 3: Fleshy region-split forms of automata A 2 and A 3 from Fig. 1. An entry region is drawn at each location.

step 1 :

 1 Lyapunov functions exist for non-forgetful cycles (Lemma 10); step 2: such a Lyapunov function can be expressed at each cycle as an expansive affine function of the delays read along the cycle (Lemma 11); step 3: inequalities involving expansive affine functions yield a fast decreasing volume (Lemma 12).

Figure 4 :

 4 Figure 4: Two non strongly connected orbit graphs, the first one is that of the cycle of A 1 , of the cycle ab of A 2 and of the cycles a and b of A 4 . States move from the initial SCC I to the 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.

Figure 5 :

 5 Figure 5: Left: non-strongly connected automaton. Right: periodic automaton.

6 ): 1 .

 61 ρ(B) is a positive simple 6 eigenvalue of B; 2. the rest of the spectrum of B belongs to the disk {z | |z| ≤ (1β)ρ(B)};Due to this gap, iterations of B on any positive vector behave in a very regular way, and numerical computation of ρ(B) and of the eigenvector v becomes particularly easy.

Figure 7 :

 7 Figure 7: Finding δ; spectrum of the perturbed operator cannot cross the ring Γ.

0 0 F 0 F 1 0F 1 0F

 0011 permits to conclude that (13) is equivalent to the first |Q| lines of[START_REF] Chomsky | Finite state languages[END_REF]:λF (x) = (ΨF )(x) = (D b2 -D a2 ) x (t)dt + (D b1 -D a1 )x (t)dt + D a2 (t)dt + D a1 (t)dt.

Figure A. 9 :

 9 Figure A.9: Three polytopes associated to a path.

  Proof. We denote by Reg(Z) the set of regions of maximal dimension included in a zone Z. We haveVol(Z) = r∈Reg(Z) Vol(r) = 1 dim(Z)! |Reg(Z)|.Every region of A is a projection of several regions of B, thus |RegA| ≤ |RegB|, and the statement is now immediate.

and taking lim sup n→∞ 1 n

 1 log(•) in both sides gives the expected result (1,≥).

  [START_REF] Wulf | Robust safety of timed automata[END_REF]. Let x 0 be the barycenter of the region of p. Then:(Φ n v) p ≥ (Φ n v) p1 (x 0 ) ≥ ψ θ w s0 (x 0 ) = R v θ (x 0 , y)w s0 (y) dy ≥ Rσ v θ (x 0 , y)w s0 (y) dy ≥ min y∈Rσ v θ (x 0 , y) • min y∈Rσ w s0 (y) • Vol(R σ ).

Ax 0 -. 5 ) 1 -

 051 ζx 0 = y 0 ; (CAx ζx 1 = y 1 .(C.6)Since x 1 is an eigenvector of A, Equation (C.6) is easy to solve:ρx 1ζx 1 = y 1 ,and thus x 1 = (ρζ) -1 y 1 , and, since ζ ∈ Γ,x 1 = |(ρζ) -1 | y 1 ≤ (|ρ| -|ζ|) -1 | y 1 ≤ (βρ/4) -1 y 1 ,and we conclude with the estimatex 1 ≤ 4(βρ) -1 y 1 . (C.7)Estimation of x 0 from (C.5) is more involved and is based on the fact that A on F 0 is almost bounded by (1ρ)β. More precisely, as shown in [15, proof of lemma 12.5] for any y 0 ∈ F 0 :A 2m+2 y 0 ≤ c(cos φ) -2 ρ 2m+2 (tan(φ/2)) 2m y 0 , (C.8)

x 0 ≤ |ζ| - 1 ∞

 1 n=0 |ζ| -n Kρ n (1β) n y 0 = K|ζ| -1 y 0 1ρ(1β)|ζ| -1 ≤ Kρ -1 /(1 -3β/4) y 0 1 -(1β)/(1 -3β/4) = 4K y 0 βρ . (C.10)Combining estimates (C.10) of x 0 and (C.7) of x 1 we getx = x 0 + x 1 ≤ x 0 + x 1 ≤Recalling that x = (Aζ) -1 y, we have obtained the required estimate for the norm of resolvent:δ = (Aζ) -1 ≤ 4K Q + 4 P βρ ,and using the bounds (C.3) on norms of projectors P and Q we obtainδ ≤ 4K(1 + (cos φ) -1 ) + 4(cos φ) -1 βρ = O(β -6 ρ -1 ),which concludes the proof.

  |Q| I |Q| 0 . This matrix permutes the |Q| first lines with the |Q| last lines of any matrix it multiplies from the left, and permutes the |Q| first columns with the |Q| last columns of any matrix it multiplies from the right. It is clear that Y = F F if and only if SY = Y . For any natural k, it holds that SA k = (-A) k S, and the same is true for the infinite series: S exp(A) = exp(-A)S. Proposition 48. The following statements hold: (i) Eq. (14) implies λY ′ = AY ; (ii) assuming λY ′ = AY , the condition Y (1/2) = SY (1/2) implies SY = Y (the converse is always true);

YH 1 / 2 0Y

 12 (t)dt, and finally we put everything together and obtain the following equation which is equivalent to (14): (B(I + S) + A) observe that (B(I + S) + A) = H H where H = D a1 + D b2 D a2 + D b1 , hence the |Q| upper lines of this equation are equal to the |Q| lower lines, so the equation is equivalent to its upper half: (t)dt -λX = 0, or again M λ X = H Lemma 36). Let Y be a solution of the integral equation (14) of the required form F F .Then, by (i) of the previous Proposition it satisfies the differential equation λY ′ = AY . By (ii, converse)Y (1/2) = SY (1/2), hence Y (1/2) = X Xfor some X. Finally, by (iii) Eq. (14) becomes equivalent toX∈ ker M λ . For the converse direction, let X ∈ ker M λ . Then the unique solution Y of Cauchy problem λY ′ = AY with the initial condition Y (1/2) = X X by (ii) satisfies Y (x) = SY (x). Thus function Y has the required form F F for F constituted by the first |Q| components of Y . Finally, by (iii) Y satisfies the integral equation.

Table 1 :

 1 Iterative algorithm: approximating H

Table 2 :

 2 45 277/8064 0.40544 -0.6512 Iterating the operator Ψ 2 for A 3 (H = log(2/π) ≈ -0.6515)

Table 3 :

 3 Symbolic algorithm: computing H for 1 1 ⁄2clocks

The guards of original automaton are bounded w.r.t. some clock. Hence, the same holds for smaller (one-region) guards of A ′ , that is infinite-size regions never occur as a guard.

Such a cycle can be iterated indefinitely, as in usual pumping lemma.

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.

The reader acquainted with Lyapunov functions will remark that, in contradiction to the custom, our Lyapunov functions are linear. Nevertheless, they still serve to characterize a stability property: the tendency of a cyclic path to bring the clock vector closer to some facet of a region. In our case, we consider it as a "bad" property.

An eigenvalue λ is simple if its generalized eigenspace has dimension 1.

Function v(a) is referred to as Radon transform of (the indicator function of) the polytope Ω and plays a central role in tomography.

⋆ The support of Agence Nationale de la Recherche under the project EQINOCS (ANR-11-BS02-004) is gratefully acknowledged.

⋆⋆ This article is partially based on conference papers [1][2][3][4][5].

Appendix A. Proof of Proposition 4

We start with two technical lemmata, the first compares volumes of zones.

Lemma 39. If an n-dimensional zone A is a projection of an m-dimensional zone B then n! m! Vol(A) ≤ Vol(B).

Appendix B. Sketch of proof of Theorem 6

We will use a well-known result about (convex) polytopes.

Lemma 42. For any polytope Ω (in variables y, z), the volume v(a) of its cross-section by the family of affine spaces y = a is a piecewise polynomial function of a continuous on its support 7 .

Proof (of Thm. 6, sketch). Let us fix a progress path π (i.e. a path resetting every clock) from p to q of length n. We start with the following observation: whenever x t,π --→ x ′ , each component x ′ of x ′ depends on t in the following way: x ′ = t lr(x ′ ) + • • • + t n where lr(x ′ ) is the index of the last reset of x ′ .

We can write ψ π (f )(x) as an integral over P π (x):

where x ′ is the clock vector obtained after reading (t, π) from x (i.e. such that x t,π --→ x ′ ). To express ψ π in a kernel form we will proceed to a change of variables in this integral making dx ′ explicit. The new set of variables consists is (x ′ , t) with x′ = (x ′ 1 , . . . , x ′ dq ) the vector of d q affinely independent clocks of the region r q ; as for t, it is formed by all t i except those coming immediately after last resets of clocks on π (i.e. except t lr(x ′ j ) for j = 1..d q ). It is easy to see that (x ′ , t) = tJ for some matrix J with determinant 1. We notice that x′ is a natural system of independent coordinates for r q ; and t is a natural system of independent coordinates for Ω π (x, x ′ ) (in particular, within r q the vector x′ determines the whole x ′ , and within Ω π (x, x ′ ) the vector t determines the whole t).

Equation (B.1) can be rewritten using new variables as

In other words, v π (x, x ′ ) is the nd q -dimensional volume of the polytope P π (x, x ′ ); and we obtain the required kernel form of ψ π (indeed dx ′ = dµ q ). Given (x 0 , x ′ 0 ) ∈ r p × r q , the set P π (x 0 , x ′ 0 ) is the cross-section of Ω π by the affine space of equations x ′ = x ′ 0 and x = x 0 . This set is an open polytope which is non-empty if and only if (x 0 , x ′ 0 ) ∈ Reach(π). Thus v π (x 0 , x ′ 0 ) > 0 on Reach(π) and is null outside of Reach(π). Moreover, due to Lem. 42, v π is piecewise polynomial and continuous on its support Reach(π).

Appendix C. Proof details for Theorem 7

C.1. Proof of Lemma 25

In this proof, we will compare volumes using the following argument:

Below, we will obtain such homotheties using properties of runs of timed automata.

Whenever hypotheses of Lem. 25 satisfied, as π 1 and π 2 are forgetful, Thm 6 applies: the operators ψ πi , i ∈ {1, 2}, admit kernels v πi , which are strictly positive on Reach(π i ).

Because of this, the following inequality is a sufficient condition (see [START_REF] Krasnosel'skij | Positive Linear Systems: The Method of Positive Operators[END_REF]):

We want to split this fraction into its left part (dealing with π 1 , handled in Prop. 45) and its right part (dealing with π 2 , handled in Prop. 44) and then find a lower bound that directly stems from the properties of volumes over π 1 and π 2 . For this, we restrict the integration domain of the numerator to some "shrunk region" r q,σ , and replace v π2 by its minimum over y, yielding the following lower bound for the numerator:

More precisely, using notation {s i | i = 0..d q } for the set of vertices of r q , we define, for σ > 0,

. Thus in both propositions below, we assume we already chose a fixed σ ≤ 1 1+d ensuring non-emptiness of r q,σ for all regions r q of the automaton.

Note that v π2 may vanish on the borders of Reach(π 2 ), but the restriction of y to r q,σ ensures that min y∈rq,σ v π2 (y, z) exists and is positive by virtue of Thm 6. Now it suffices to show the following:

Here the inequality (1) follows from Lem. 25, (2) is triangle inequality, (3) is trivial, and inequality (4) follows from Lem. 46.

C.3. Proof of Lemma 30

Unfortunately, we did not find this result in the literature and were obliged to prove it by adapting techniques from [START_REF] Krasnosel'skij | Positive Linear Systems: The Method of Positive Operators[END_REF]. We first need some "infrastructure".

Let A be an acute operator on Banach space F and ρ its spectral radius. By Lem. 24, A and A * have non-negative eigenvectors e and f corresponding to eigenvalue ρ. By definition of acuteness A * f, Ae > 0, thus ρf, ρe > 0 and f, e > 0.

So e and f can be chosen such that e = 1 and f, e = 1. Let

, and F 1 = {λe|λ ∈ R}. The space F is a direct sum of unidimensional eigenspace F 1 and complementary space F 0 , each vector admits a decomposition v = v 0 + v 1 with

(in this proof, we will systematically use notation v 0 , v 1 for projections Qv and P v). The projectors P and Q commute with A. Let also the constant c be defined by:

The acuteness condition (8) provides useful estimates on several norms:

Proposition 47. For an acute operator A with cosine cos φ, vector e, functional f , operators P, Q and constant c described above, the following bounds hold:

Proof. First, applying (8) to f and e (they are positive) we get

and thus f ≤ 1/ cos φ. On the other hand,

To estimate A , we remark that for any z ∈ F there exists a positive functional h ∈ F * of norm 1 such that Az = | h, Az | (indeed Az = |Az(x * )| for some point x * and we can take the functional h of norm 1 mapping each function to its value at x * ). Applying [START_REF] Stainer | Frequencies in forgetful timed automata[END_REF] to h and e we get that:

Last, to estimate the constant c we remark that for z ∈ F 0 it holds that f, z = 0 and

The supremum in definition (C.2) of c can be represented as maximum of two suprema: c 1 for |λ| ≤ a z , and c 2 for |λ| > a z (we will chose a a couple of lines later). Clearly, c 1 ≤ 1/(1a), and from (C.2) it follows that c 2 ≤ 1/(a cos φ). Choosing a = 1/(1 + cosφ) makes both estimates (for c 1 and c 2 ) equal to 1 + (cos φ) -1 . We conclude that c ≤ 1 + (cos φ) -1 .

C.4. Proof of Lemma 32 and Corollary 33

Proof (of Lemma 32). Let σ ⊂ C be the spectrum of A, then the spectrum σ N of A N has the required form: one simple eigenvalue ρ and a subset of the circle of a lesser radius λ. Hence σ contains some points of maximum modulus ρ 1/N e (with e roots of unity of degree N ) and a subset of the circle of radius λ 1/N . The same is true with respect to N + 1: all the spectral points in σ of maximum modulus have the form ρ ′ 1/N +1 e ′ (with e ′ roots of unity of degree N + 1). Since the only complex number that is a root of unity of both degrees N and N + 1 is 1, we conclude that σ contains one real number ρ = ρ 1/N = ρ ′ 1/N +1 and a subset of the circle of a lesser radius λ = λ 1/N . We have obtained that ρ is the unique spectral value of A of the maximal modulus (thus its spectral radius).

In order to show that it is an eigenvalue of A, consider a positive eigenvector v of A N corresponding to eigenvalue ρ, and build the vector w = N -1 k=0 ρ -k/N A k v. This vector is positive, and it is an eigenvector of A, indeed:

This eigenvalue is simple. Indeed, all corresponding eigenvectors are also eigenvectors of A N for eigenvalue ρ, but there is only one such eigenvector. Let us prove that A has no other generalized eigenvectors. Suppose the contrary, for some x = 0 that is not an eigenvector and natural k, it holds that (A -ρI) k x = 0. We fix such an x and suppose that k is the smallest possible for this x (clearly k ≥ 2). Denote y = (A -ρI) k-2 x and z = (A -ρI) k-1 x; this implies that (A -ρI)y = z, and z is an eigenvector. By induction on n we will prove that A n y = ρ n y + nρ n-1 z. Indeed the equality holds for n = 1. To pass from n to n + 1 we compute

This contradicts the simplicity of the eigenvalue ρ N for the operator A N and concludes the proof.

Proof (of Cor. 33, sketch). According to Thm 7, ρ(Θ) is an eigenvalue of Θ = Ψ pc c,i (for some SCC c) with a positive eigenvector, and thus an eigenvalue of Ψ p c . Using the same argument as in the proof of Lem. 32, we can construct an eigenvector for Ψ c with eigenvalue ρ(Ψ). Finally, this eigenvector can be extended from one SCC to the whole automaton.

On the other hand, it is not difficult to show that every eigenvalue of Ψ is an eigenvalue of some Ψ pc c,i ; and since each of the latter operators has a spectral gap, ρ(Ψ) is an isolated (but possibly multiple) eigenvalue of Ψ.

Appendix D. Proof details for Theorem 9 D.1. Proof sketch of Lemma 34 Proof. First let us denote by [Ψ] the matricial form of Ψ (the operator on C(0, 1) Q such that the vectorial form of Ψf is [Ψ]F ). We recall, from [START_REF] Asarin | Toward timed theory of channel coding[END_REF], that Ψ can be decomposed as (Ψf ) q (x) = δ=(q,...,q ′ )∈∆ (ψ δ f q ′ )(x), with, for f ∈ C(r q ): ψ δ f (x) = x+τ ∈g f (r(x + τ )) dτ. Thus we can explicit the matricial coefficients of [Ψ] as operators [Ψ] qq ′ ∈ C(0, 1) → C(0, 1):

δ=(q,a,g,r,q ′ )∈∆ (ψ δ f )(x) = (q,a,g,r,q ′ )∈∆ x+τ ∈g f (r(x+τ )) dτ = (q,a,g,r,q ′ )∈∆ t∈[g](x) f ([r](x, t)) dτ, where, in the last expression (obtained after the change of coordinates), the reset function [r] and interval [g](x) take forms that depend on the situation.