Wolfgang Steiner
email: steiner@liafa.jussieu.fr

DIGITAL EXPANSIONS WITH NEGATIVE REAL BASES

Digital expansions with negative real bases

Introduction

Digital expansions in real bases β > 1 were introduced by Rényi [START_REF] Rényi | Representations for real numbers and their ergodic properties[END_REF]: The (greedy) β-expansion of a real number x ∈ [0, 1) is

x = ε 1 (x) β + ε 2 (x) β 2 + • • • with ε n (x) = ⌊β T n-1 β (x)⌋,
where ⌊•⌋ denotes the floor function and T β is the β-transformation T β : [0, 1) → [0, 1), x → βx -⌊βx⌋ .

Rényi suggested representing arbitrary x ∈ R by

x = ⌊x⌋ + ε 1 (⌊x⌋) β + ε 2 (⌊x⌋) β 2 + • • • ,
whereas nowadays it is more usual (for x ≥ 0) to multiply the β-expansion of xβ -k by β k , with k an arbitrary integer satisfying xβ -k ∈ [0, 1). Anyway, the possible expansions can be described by those of x ∈ [0, 1). A sequence b 1 b 2 • • • is called β-admissible if and only if it is (the digit sequence of) the β-expansion of a number x ∈ [0, 1), i.e., b n = ε n (x) for all n ≥ 1. Parry [START_REF] Parry | On the β-expansions of real numbers[END_REF] showed that an integer sequence b

1 b 2 • • • is β-admissible if and only if 00 • • • ≤ lex b k b k+1 • • • < lex a 1 a 2 • • • for all k ≥ 1,
where < lex denotes the lexicographic order and a 1 a 2 • • • is the (quasi-greedy) β-expansion of 1, i.e., a n = lim x→1-ε n (x). Moreover, a sequence of integers a 1 a 2 • • • is the (quasigreedy) β-expansion of 1 for some β > 1 if and only if 00

• • • < lex a k a k+1 • • • ≤ lex a 1 a 2 • • • for all k ≥ 2.
(These results are stated in a slightly different way in [START_REF] Parry | On the β-expansions of real numbers[END_REF].)

Part of this research was conducted while the author was visiting academic at the Department of Computing of the Macquarie University, Sydney.

Following [START_REF] Rényi | Representations for real numbers and their ergodic properties[END_REF] and [START_REF] Parry | On the β-expansions of real numbers[END_REF], a lot of papers were dedicated to the study of β-expansions and β-transformations, but surprisingly little attention was given to digital expansions in negative bases. This changed only in recent years, after Ito and Sadahiro [START_REF] Ito | Beta-expansions with negative bases[END_REF] considered (-β)-expansions, β > 1, defined for x ∈ -β β+1 , 1 β+1 by

(1.1)

x = ε 1 (x) -β + ε 2 (x) (-β) 2 + • • • with ε n (x) = β β+1 -β T n-1 -β (x) ,
where the (-β)-transformation is defined by

T -β : -β β+1 , 1 β+1 → -β β+1 , 1 β+1 , x → -βx -β β+1 -βx . A sequence b 1 b 2 • • • is (-β)-admissible if
and only if it is the (-β)-expansion of some x ∈ -β β+1 , 1 β+1 , i.e., b n = ε n (x) for all n ≥ 1. Since the map x → -βx is order-reversing, the (-β)-admissible sequences are characterized using the alternating lexicographic order.

By [IS09], a sequence b 1 b 2 • • • is (-β)-admissible if and only if (1.2) a 1 a 2 • • • ≥ alt b k b k+1 • • • > alt 0a 1 a 2 • • • for all k ≥ 1,
where

a 1 a 2 • • • is the (-β)-expansion of the left endpoint -β β+1 , i.e., a n = ε n -β β+1 , which is supposed not to be periodic with odd period length. If a 1 a 2 • • • = a 1 a 2 • • • a 2ℓ+1
for some ℓ ≥ 0, and ℓ is minimal with this property, then the condition (1.2) is replaced by

(1.3) a 1 a 2 • • • ≥ alt b k b k+1 • • • > alt 0a 1 • • • a 2ℓ (a 2ℓ+1 -1) for all k ≥ 1.
Recall that the alternating lexicographic order is defined on sequences

x 1 x 2 • • • , y 1 y 2 • • • with x 1 • • • x k-1 = y 1 • • • y k-1 and x k = y k by x 1 x 2 • • • < alt y 1 y 2 • • • if and only if x k < y k when k is odd, y k < x k when k is even.
The main result of this paper is a characterization of the sequences a 1 a 2 • • • that are the (-β)-expansion of -β β+1 for some β > 1. This turns out to be more complicated than the corresponding problem for β-expansions, and we will see that several proofs cannot be directly carried over from positive to negative bases. From (1.2) and (1.3), one deduces that

(1.4) a k a k+1 • • • ≤ alt a 1 a 2 • • • for all k ≥ 2.
The proof of Proposition 3.5 in [LS] (see also Theorem 3 below) shows that

(1.5) a 1 a 2 • • • > alt u 1 u 2 • • • = 100111001001001110011 • • • ,
where u 1 u 2 • • • is the sequence starting with ϕ n (1) for all n ≥ 0, with ϕ being the morphism of words on the alphabet {0, 1} defined by ϕ(1) = 100, ϕ(0) = 1. (See the remarks following Theorem 3 and note that the alphabet is shifted by 1 in [LS].) Our first result states that a sequence satisfying (1.4) and (1.5) is "almost" the (-β)-expansion of -β β+1 for some β > 1.

Theorem 1. Let a 1 a 2 • • • be a sequence of non-negative integers satisfying (1.4) and (1.5).

Then there exists a unique β > 1 such that

(1.6) ∞ j=1 a j (-β) j = -β β + 1 and ∞ j=1 a k+j (-β) j ∈ -β β + 1 , 1 β + 1 for all k ≥ 1.
For a (-β)-expansion of -β β+1 , we have to exclude the possibility that ∞ j=1 a k+j

(-β) j = 1 β+1 for some k ≥ 1. If a 1 • • • a k > alt u 1 u 2 • • • , then out of {a 1 • • • a k , a 1 • • • a k-1 (a k -1)0} ω , which is the set of infinite sequences composed of blocks a 1 • • • a k and a 1 • • • a k-1 (a k -1)0, only the periodic sequence a 1 • • • a k is possibly the (-β)-expansion of -β β+1 for some β > 1, see Section 4. This implies that a 1 a 2 • • • ∈ {a 1 • • • a k , a 1 • • • a k-1 (a k -1)0} ω \ {a 1 • • • a k } (1.7) for all k ≥ 1 with a 1 • • • a k ≻ u 1 u 2 • • • , a 1 a 2 • • • ∈ {a 1 • • • a k 0, a 1 • • • a k-1 (a k +1)} ω (1.8) for all k ≥ 1 with a 1 • • • a k-1 (a k +1) ≻ u 1 u 2 • • • .
The main result states that there are no other conditions on a 1 a 2

• • • . Theorem 2. A sequence of non-negative integers a 1 a 2 • • • is the (-β)-expansion of -β β+1
for some (unique) β > 1 if and only if it satisfies (1.4), (1.5), (1.7), and (1.8).

It is easy to see that the natural order of bases β > 1 is reflected by the lexicographical order of the (quasi-greedy) β-expansions of 1 [START_REF] Parry | On the β-expansions of real numbers[END_REF]. For negative bases, a similar relation with the alternating lexicographic order holds, although it is a bit harder to prove.

Theorem 3. Let a 1 a 2 • • • be the (-β)-expansion of -β β+1 and a ′ 1 a ′ 2 • • • be the (-β ′ )-expansion of -β ′ β ′ +1 , with β, β ′ > 1. Then β < β ′ if and only if a 1 a 2 • • • < alt a ′ 1 a ′ 2 • • • .
It is often convenient to study a slightly different (-β)-transformation,

T -β : (0, 1] → (0, 1], x → -βx + ⌊βx⌋ + 1.
As already noted in [LS], the transformations T -β and T -β are conjugate via the involution

φ(x) = 1 β+1 -x, i.e., T -β • φ(x) = φ • T -β (x) for all x ∈ (0, 1]. Setting εn (x) = β T n-1 -β (x) for x ∈ (0, 1], we have x = -∞ n=1 εn(x)+1 (-β) n = 1 β+1 -∞ n=1 εn(x)
(-β) n , and εn (x) = ε n (φ(x)). Note that T -β (x) = -βx -⌊-βx⌋ except for finitely many points, hence T -β is a natural generalization of the beta-transformation. The map T -β was studied e.g. by Góra [START_REF] Góra | Invariant densities for generalized β-maps[END_REF], where it corresponds to the case E = [1, 1, . . . , 1], and in [LS]. The following corollary is an immediate consequence of Theorems 1 and 2.

Corollary 1. Let a 1 a 2 • • • be a sequence of non-negative integers satisfying (1.4) and (1.5). Then there exists a unique β > 1 such that

(1.9) - ∞ j=1 a j + 1 (-β) j = 1 and - ∞ j=1 a k+j + 1 (-β) j ∈ [0, 1] for all k ≥ 1.
Moreover, ∞ j=1 a k+j +1 (-β) j = 0 for all k ≥ 1 if and only if (1.7) and (1.8) hold. With the notation of [START_REF] Góra | Invariant densities for generalized β-maps[END_REF], this means, for

E = [1, 1, . . . , 1], that a 1 a 2 • • • is the itinerary It β (1)
for some β > 1 if and only if (1.4), (1.5), (1.7), and (1.8) hold. Note that Góra [Gór07, Theorems 25 and 28] claims that already (1.4) is sufficient when a 1 ≥ 2, and he has a less explicit statement for a 1 = 1. However, his proof deals only with the first part of the theorem, i.e., that there exists a unique β > 1 satisfying (1.9). To see that this is not sufficient, consider the sequences a 1 a 2 • • • ∈ {2, 1 0} ω . They all satisfy (1.9) with β = 2, and there are uncountably many of them satisfying (1.4) and a 1 = 2. All these uncountably many sequences would have to be equal to It 2 (1) by [Gór07, Theorem 25], which is of course not true. (See also [START_REF] Dombek | Number representation using generalized (-β)transformation[END_REF].) Moreover, Góra's proof of the existence of a unique β > 1 satisfying (1.9) is incorrect when β is small, see Remark 1. Lemma 1. For any β > 1, we have that lim n→∞

Proof of Theorem 3

Let β > 1. For a sequence of digits b 1 • • • b n , set I b 1 •••bn = x ∈ -β β+1 , 1 β+1 : ε 1 (x) • • • ε n (x) = b 1 • • • b n , with ε j (x) as in (1.1). Let L β,n be the number of different sequences b 1 • • • b n such that I b 1 •••bn = ∅,
1 n log L β,n = lim n→∞ 1 n log L ′ β,n = log β. Proof.
It is well known that the entropy of T -β , which is a piecewise linear map of constant slope -β, is log β. The lemma can be derived from this fact, see [START_REF] Frougny | Negative bases and automata[END_REF], but we prefer giving a short elementary proof, following Faller [START_REF] Faller | Contribution to the ergodic theory of piecewise monotone continuous maps[END_REF]Proposition 3.6

]. As d dx T n -β (x) = β n at all points of continuity of T n -β , the length of any interval I b 1 •••bn is at most β -n . Since the intervals I b 1 •••bn form a partition of an interval of length 1, we obtain that L β,n ≥ L ′ β,n ≥ β n .
To get an upper bound for L ′ β,n , let m be the smallest positive integer such that β m > 2, and let δ be the minimal positive length of an interval

I b 1 •••bm . Consider an interval I b 1 •••bn , n > m, such that b 1 • • • b n is
neither the minimal nor the maximal sequence (with respect to the alternating lexicographic order) starting with b

1 • • • b n-m and satisfying I b 1 •••bn = ∅. Then each prolongation b 1 b 2 • • • satisfies the inequalities in (1.2) and (1.3), respectively, for 1 ≤ k ≤ n -m. Therefore, b 1 b 2 • • • is (-β)-admissible if and only if b n-m+1 b n-m+2 • • • is (-β)-admissible. This implies that T n-m -β (I b 1 •••bn ) = I b n-m+1 •••bm , and the length of I b 1 •••bn is β m-n times the length of I b n-m+1 •••bm , thus at least β m-n δ when the length is positive. There are at least L ′ β,n -2L ′ β,n-m sequences b 1 • • • b n such that I b 1 •••bn has positive length and b 1 • • • b n is neither the minimal nor the maximal sequence starting with b 1 • • • b n-m and satisfying I b 1 •••bn = ∅. This yields that (L ′ β,n -2L ′ β,n-m )β m-n δ ≤ 1 for all n > m, thus L ′ β,n ≤ β n-m δ + 2L ′ β,n-m ≤ β n-m δ + 2β n-2m δ + 4L ′ β,n-2m ≤ • • • ≤ β n-m δ ⌈n/m⌉-2 j=0 2 β m j + 2 ⌈n/m⌉-1 L ′ β,n-⌈n/m⌉m+m < β n δ 1 β m -2 + β n L ′ β,m ≤ β n δ β m -1 β m -2 .
This shows that lim n→∞

1 n log L ′ β,n = β. An interval I b 1 •••bn consists only of one point if and only if I b 1 •••b k = -β β+1 and b k+1 • • • b n = a 1 • • • a n-k for some k ≤ n. (This can happen only in case that a 1 a 2 • • • is periodic with odd period length.) Therefore, we can estimate L β,n -L ′ β,n ≤ L ′ β,0 +L ′ β,1 +• • •+L ′ β,n ≤ Cβ n for some constant C > 0, thus lim n→∞ 1 n log L β,n = lim n→∞ 1 n log L ′ β,n .
For the proof of Theorem 3, let β)-admissible sequences are equal to the (-β ′ )-admissible sequences, thus L β,n = L β ′ ,n for all n ≥ 1, and β = β ′ by Lemma 1. Therefore, the equations β)-admissible sequence. By (1.2) and (1.3) respectively, we have that

a 1 a 2 • • • be the (-β)-expansion of -β β+1 and a ′ 1 a ′ 2 • • • be the (-β ′ )-expansion of -β ′ β ′ +1 , β, β ′ > 1. If β = β ′ , then we clearly have that a 1 a 2 • • • = a ′ 1 a ′ 2 • • • . If a 1 a 2 • • • = a ′ 1 a ′ 2 • • • , then the (-
β = β ′ and a 1 a 2 • • • = a ′ 1 a ′ 2 • • • are equivalent. Hence, it suffices to show that a 1 a 2 • • • < alt a ′ 1 a ′ 2 • • • implies that β < β ′ , as the other direction follows by contraposition. Assume that a 1 a 2 • • • < alt a ′ 1 a ′ 2 • • • , and let b 1 b 2 • • • be a (-
(2.1) b k b k+1 • • • ≤ alt a 1 a 2 • • • < alt a ′ 1 a ′ 2 • • • . Furthermore, as 0a 1 • • • a 2ℓ (a 2ℓ+1 -1) > alt 0a 1 a 2 • • • for all ℓ ≥ 0, we obtain that (2.2) b k b k+1 • • • > alt 0a 1 a 2 • • • > alt 0a ′ 1 a ′ 2 • • • . If a ′ 1 a ′ 2 • • • is not periodic with odd period length, then (2.1) and (2.2) show that b 1 b 2 • • • is (-β ′ )-admissible, thus L β,n ≤ L β ′ ,n for all n ≥ 1, and β ≤ β ′ by Lemma 1. Since a 1 a 2 • • • = a ′ 1 a ′ 2 • • • , this yields that β < β ′ . In case a ′ 1 a ′ 2 • • • = a ′ 1 • • • a ′ 2ℓ ′ +1 , we show that (2.3) a 1 a 2 • • • ≤ alt a ′ 1 • • • a ′ 2ℓ ′ (a ′ 2ℓ ′ +1 -1)0.

This is clearly true when

a 1 • • • a 2ℓ ′ +1 < alt a ′ 1 • • • a ′ 2ℓ ′ (a ′ 2ℓ ′ +1 -1). If a 1 • • • a 2ℓ ′ +1 = a ′ 1 • • • a ′ 2ℓ ′ +1 , then a 2ℓ ′ +2 a 2ℓ ′ +3 • • • > alt a ′ 2ℓ ′ +2 a ′ 2ℓ ′ +3 • • • = a ′ 1 a ′ 2 • • • > alt a 1 a 2 • • • , contradicting (1.4). It remains to consider the case that a 1 • • • a 2ℓ ′ +1 = a ′ 1 • • • a ′ 2ℓ ′ (a ′ 2ℓ ′ +1 -1). If a 2ℓ ′ +1 > 0, then (2.3) holds, otherwise a 1 • • • a 2ℓ ′ +2 = a ′ 1 • • • a ′ 2ℓ ′ (a ′ 2ℓ ′ +1 -1)0. In the latter case, (1.4) implies that a 2ℓ ′ +3 • • • a 4ℓ ′ +4 ≤ alt a 1 • • • a 2ℓ ′ +2 = a ′ 1 • • • a ′ 2ℓ ′ (a ′ 2ℓ ′ +1
-1)0, and we obtain inductively that (2.3) holds. Now, (2.1), (2.2), and (2.3) show that b 1 b 2 • • • is (-β ′ )-admissible, which yields as above that β < β ′ .

Proof of Theorem 1

Let a 1 a 2 • • • be a sequence of non-negative integers satisfying (1.4) and (1.5). We show that there exists a unique β > 1 satisfying (1.9), which is equivalent to (1.6). For n ≥ 1, set

P n (x) = (-x) n + n j=1 (a j + 1) (-x) n-j , J n = x > 1 | P j (x) ∈ [0, 1] for all 1 ≤ j ≤ n . Then J 1 ⊇ J 2 ⊇ J 3 ⊇ • • • , and J n is compact if and only if inf J n = 1.
First note that, for β > 1, (1.9) is equivalent to β ∈ n≥1 J n . Indeed, if (1.9) holds, then

P n (β) = -∞ j=1 a n+j +1 (-β) j ∈ [0, 1] for all n ≥ 1. On the other hand, if P n (β) ∈ [0, 1] for all n ≥ 1, then 1 + ∞ j=1 a j +1 (-β) j = lim n→∞ Pn(β)
(-β) n = 0, thus (1.9) holds. Inductively for n ≥ 1, we show the following statements, where we use the abbreviations

v [j,k] for v j v j+1 • • • v k and v [j,k) for v j v j+1 • • • v k-1 :
(1) J n is a non-empty interval, with inf

J n = 1 if and only if a [1,n] = u [1,n] . If P n (β) = P n (β ′ ) ∈ {0, 1} with β, β ′ ∈ J n , then β = β ′ . (2) If n is even, a [1,n-2m+1] = u [1,n-2m+1] or a [n-2m+2,n] = a [1,2m) for all 1 ≤ m ≤ n/2, and a [1,n] = u [1,n] , then P n (min J n ) = 0. If n is odd and a [n-2m+2,n] = a [1,2m) for all 1 ≤ m ≤ n/2, then P n (max J n ) = 0. (3) If n is even, a [1,n-2m+1] = u [1,n-2m+1] and a [n-2m+2,n] = a [1,2m) for some 1 ≤ m ≤ n/2,
and m is maximal with this property, then P n (min

J n ) = P 2m-1 (min J n ). If n is odd, a [n-2m+2,n] = a [1,2m)
for some 1 ≤ m ≤ n/2, and m is maximal with this property, then P n (max

J n ) = P 2m-1 (max J n ). (4) If n is even and a [n-2m+1,n] = a [1,2m] for all 1 ≤ m < n/2, then P n (max J n ) = 1. If n is odd, a [1,n-2m] = u [1,n-2m] or a [n-2m+1,n] = a [1,2m] for all 1 ≤ m < n/2, and a [1,n] = u [1,n] , then P n (min J n ) = 1. (5) If n is even, a [n-2m+1,n] = a [1,2m]
for some 1 ≤ m < n/2, and m is maximal with this property, then P n (max

J n ) = P 2m (max J n ). If n is odd, a [1,n-2m] = u [1,n-2m] and a [n-2m+1,n] = a [1,2m]
for some 1 ≤ m < n/2, and m is maximal with this property, then P n (min J n ) = P 2m (min J n ). We have that P 1 (x) = a 1 + 1x, and a 1 ≥ 1 by (1.5). If a 1 ≥ 2, then J 1 = [a 1 , a 1 + 1], P 1 (a 1 ) = 1 and P 1 (a 1 + 1) = 0; if a 1 = 1, then J 1 = (1, 2] and P 1 (2) = 0. Therefore, the statements hold for n = 1. Assume that they hold for n -1, and set

B = b ∈ {0, 1, . . . , a 1 } : b + 1 -xP n-1 (x) ∈ [0, 1] for some x ∈ J n-1 , i.e., J n = ∅ if and only if a n ∈ B. Assume first that a [1,n) = u [1,n) , i.e., inf J n-1 = min J n-1 > 1, and that n is even. (i) If a [n-2m+1,n) = a [1,2m) for all 1 ≤ m < n/2, then P n-1 (max J n-1 ) = 0, thus 1 -(max J n-1 ) P n-1 (max J n-1 ) = 1.
This implies that 0 ∈ B, and P n (max J n ) = P n (max J n-1 ) = 1 if a n = 0. Since the map x → xP n-1 (x) is continuous and J n-1 is an interval, we get that P n (max

J n ) = 1
for a n > 0 as well, when J n = ∅. Moreover, we clearly have that a

[n-2m+1,n] = a [1,2m] for all 1 ≤ m < n/2, thus (4) holds when a n ∈ B. (ii) If a [n-2m+1,n) = a [1,2m)
for some 1 ≤ m < n/2, and m is maximal with this property, then P n-1 (max J n-1 ) = P 2m-1 (max J n-1 ), thus

a 2m + 1 -(max J n-1 ) P n-1 (max J n-1 ) = P 2m (max J n-1 ) ∈ [0, 1],
where we have used that J n-1 ⊆ J 2m and P 2m (J 2m ) ⊆ [0, 1]. This gives a 2m ∈ B.

If a n = a 2m , then max J n = max J n-1 and P n (max J n-1 ) = P 2m (max J n-1 ), thus

P n (max J n ) = P 2m (max J n ) and a [n-2m+1,n] = a [1,2m]
. By the maximality of m, we have that a

[n-2ℓ+1,n] = a [1,2ℓ] for all m < ℓ < n/2, thus (5) holds. If a n = a 2m , then the equation a [n-2m+1,n) = a [1,2m) and (1.4) yield that a n > a 2m , thus P n (max J n ) = 1 when J n = ∅, similarly to (i). If a [1,2ℓ) = a [n-2ℓ+1,n) , 1 ≤ ℓ < m, then we also have that a [1,2ℓ) = a [2m-2ℓ+1,2m) , thus a 2ℓ ≤ a 2m < a n . This implies that a [n-2ℓ+1,n] = a [1,2ℓ] for all 1 ≤ ℓ < n/2, thus (4) holds when a n ∈ B. (iii) If a [1,n-2m) = u [1,n-2m) or a [n-2m,n) = a [1,2m] for all 1 ≤ m ≤ n/2 -1, then we have that P n-1 (min J n-1 ) = 1, thus a 1 + 1 -(min J n-1 ) P n-1 (min J n-1 ) = P 1 (min J n-1 ) ∈ [0, 1],
and a 1 ∈ B. If a n = a 1 , then min J n = min J n-1 and P n (min J n-1 ) = P 1 (min J n-1 ), thus P n (min

J n ) = P 1 (min J n ), and a [1,n-2m+1] = u [1,n-2m+1] or a [n-2m+2,n] = a [1,2m) for all 2 ≤ m ≤ n/2. Therefore, (3) holds. If a n < a 1 , then P n (min J n ) = 0 when J n = ∅, a [1,n-2m+1] = u [1,n-2m+1] or a [n-2m+2,n] = a [1,2m) for all 1 ≤ m ≤ n/2, thus (2) holds when a n ∈ B. (iv) If a [1,n-2m) = u [1,n-2m) and a [n-2m,n) = a [1,2m]
for some 1 ≤ m ≤ n/2 -1, and m is maximal with this property, then P n-1 (min J n-1 ) = P 2m (min J n-1 ), thus

a 2m+1 + 1 -(min J n-1 ) P n-1 (min J n-1 ) = P 2m+1 (min J n-1 ) ∈ [0, 1],
hence a 2m+1 ∈ B. If a n = a 2m+1 , then min J n = min J n-1 and P n (min J n-1 ) = P 2m+1 (min J n-1 ), thus P n (min

J n ) = P 2m+1 (min J n ), and a [n-2m,n] = a [1,2m+1] . The maximality of m yields that a [1,n-2ℓ+1] = u [1,n-2ℓ+1] or a [n-2ℓ+2,n] = a [1,2ℓ) for all m + 1 < ℓ ≤ n/2, thus (3) holds. If a n = a 2m+1 , then a n < a 2m+1 by (1.4). If moreover a [1,2ℓ-2] = a [n-2ℓ+2,n) , 1 ≤ ℓ ≤ m, then we have that a [1,2ℓ-2] = a [2m-2ℓ+3,2m] , thus a 2ℓ-1 ≥ a 2m+1 > a n . Then we get that P n (min J n ) = 0 when J n = ∅, a [1,n-2ℓ+1] = u [1,n-2ℓ+1] and a [n-2ℓ+2,n] = a [1,2ℓ) for all 1 ≤ ℓ ≤ n/2, thus (2) holds when a n ∈ B. Since x → xP n-1 (x)
is continuous and J n-1 is an interval, the set B is an interval of integers. The paragraphs (i) and (ii) show that a n is not smaller than the smallest element of B, (iii) and (iv) show that a n is not larger than the largest element of B, thus a n ∈ B. We have therefore proved that J n = ∅ and (2)-(5) hold, when a [1,n) = u [1,n) and n is even. For odd n, the proof runs along the same lines and is left to the reader.

If

a [1,n) = u [1,n) , then inf J n-1 = 1.
From [LS, Proposition 3.5], we know that u n ∈ B, that inf J n = 1 when a n = u n , and that min J n > 1 when u n = a n ∈ B. Let first n be even, thus a n ≤ u n by (1.5). If a [n-2m+1,n) = a [1,2m) for all 1 ≤ m < n/2, then we obtain as in (i) that 0 ∈ B, thus a n ∈ B, and (4) holds. If a [n-2m+1,n) = a [1,2m) for some 1 ≤ m < n/2, and m is maximal with this property, then (ii) yields that a 2m ∈ B and a 2m ≤ a n , thus a n ∈ B. If a n = a 2m , then (5) holds; if a n > a 2m , then (4) holds. Moreover, if a n < u n , then we get that P n (min J n ) = 0, thus (2) holds. Again, if n is odd, then similar arguments apply. Hence, we have proved that J n = ∅ and (2)-(5) hold for the case that a

[1,n) = u [1,n) too.
If J n is not an interval, then the continuity of x → xP n-1 (x) on the interval J n-1 implies that P n meets the lower bound 0 or the upper bound 1 at least twice within J n . Therefore, suppose that P n (β) = P n (β ′ ) ∈ {0, 1} for β, β ′ ∈ J n . If P j (β) ∈ (0, 1] and P j (β ′ ) ∈ (0, 1] for all 1 ≤ j < n, then the (-β)-expansion of -β β+1 and the (-

β ′ )-expansion of -β ′ β ′ +1 are both a [1,n] (if P n (β) = 1) or a [1,n) (a n +1) (if P n (β) = 0), thus β = β ′ by Theorem 3.
Suppose in the following that P j (β ′ ) = 0 for some 1 ≤ j < n, and let ℓ ≥ 1 be minimal such that P ℓ (β ′ ) ∈ {0, 1}. If P ℓ (β ′ ) = 0, then a ℓ+1 = 0 and P ℓ+1 (β ′ ) = 1, hence a [1,n] is a concatenation of blocks a [1,ℓ] 0 and a [1,ℓ) (a ℓ +1), except possibly for the last block, which is a [1,ℓ] when P n (β ′ ) = 0. If P ℓ (β ′ ) = 1, then a [1,n] is a concatenation of blocks a [1,ℓ] and a [1,ℓ) (a ℓ -1)0, ending with a [1,ℓ) (a ℓ -1) when P n (β ′ ) = 0. We obtain that

P n (x) = P n (β ′ ) + P ℓ (x) -P ℓ (β ′ ) Q(x)
for some polynomial Q(x) = n-ℓ j=0 q j (-x) j with coefficients q j ∈ {0, 1}, and q j-1 = q j-2 = • • • = q j-ℓ+1 = 0 whenever q j = 1. If P ℓ (β) = P ℓ (β ′ ), then the induction hypotheses yield that

β = β ′ . If P ℓ (β) = P ℓ (β ′ ), then Q(β) = 0, which implies that 1 < 1 β ℓ+1 + 1 β 2ℓ+1 + • • • = 1 β ℓ+1 -β when ℓ is even, 1 < 1 β ℓ + 1 β 2ℓ+1 + • • • = β β ℓ+1
-1 when ℓ is odd, i.e., β ℓ+1 < β + 1. To exclude the latter case, suppose that P n (β) = P n (β ′ ) ∈ {0, 1} for β, β ′ ∈ J n , β = β ′ , and that β ℓ+1 < β + 1 for the minimal ℓ ≥ 1 such that P ℓ (β ′ ) ∈ {0, 1}. Set g k = ⌊2 k+1 /3⌋, and let, for k ≥ 1, γ k and η k be the real numbers greater than 1 satisfying

γ g k +1 k = γ k + 1, η g k +1 k = η g k-1 +1 k +1 when k is even, η g k k = η g k-1 k
+1 when k is odd, as in [LS]. For the positive integer m satisfying g m ≤ ℓ < g m+1 , we have that β < γ m < η m . By Proposition 3.5 in [LS] and its proof, β < η m implies that the (-β)-expansion of -β β+1 starts with ϕ m (1) and that

T j -β (1) ∈ {0, 1} for all 1 ≤ j ≤ |ϕ m (1)| = g m+1 + 1-(-1) m 2
, where |w| denotes the length of the word w. Since β ∈ J n and P n (β) ∈ {0, 1}, we obtain that a 1 a 2 • • • starts with ϕ m (1) and that n > |ϕ m (1)|. By equation (3.2) in [LS], we have that P 2 m (x) > 1 for all x > η m (note that 2 m = |ϕ m-1 (10)| < |ϕ m (1)|), thus J 2 m = (1, η m ], and ℓ < g m+1 yields that β ′ = η m , ℓ = 2 m . As β and β ′ are in the interval J n-1 , we also have that γ m ∈ J n-1 . The (-γ m )-expansion of -γm γm+1 is ϕ m-1 (1) ϕ m-1 (0) by [LS, Theorem 2.5]. Since n ≥ 2ℓ by the above block decomposition of a [1,n] , we obtain that a 1 a 2 • • • starts with ϕ m-1 (1000) if m ≥ 2, and with 100 if m = 1. In case m = 1, we get that P [LS] and, using the notation of [LS], the function f γm,ϕ m-1 (0) is order-reversing. Again, this contradicts that η m = β ′ ∈ J n . Therefore, we have shown that β = β ′ whenever P n (β) = P n (β ′ ) ∈ {0, 1}, β, β ′ ∈ J n . Hence, J n is an interval, and (1)-( 5) hold for all n ≥ 1.

3 (2) ∈ J 3 , contradicting that 2 = η 1 = β ′ ∈ J n . For m ≥ 2, we have that P |ϕ m-1 (1000)| (η m ) > P |ϕ m-1 (10)| (η m ) = 1 because P |ϕ m-1 (100)| (η m ) = P |ϕ m (1)| (η m ) < P |ϕ m-1 (1)| (η m ) by equation (3.4) in
As the J n form a sequence of nested non-empty intervals that are compact for sufficiently large n, we have that n≥1 J n = ∅, thus there exists some β > 1 satisfying (1.9), which is equivalent to (1.6). To show that β is unique, suppose that n≥1 J n is not a single point. Then n≥1 J n is an interval of positive length, thus there exist β, β ′ ∈ n≥1 J n , β = β ′ , such that P n (β) ∈ (0, 1] and P n (β ′ ) ∈ (0, 1] for all n ≥ 1. This means that a 1 a 2 • • • is both the (-β)-expansion of -β β+1 and the (-β ′ )-expansion of -β ′ β ′ +1 , which contradicts that β = β ′ by Theorem 3. This concludes the proof of Theorem 1.

Remark 1. Some parts of the proofs of Theorems 1 and 3 can be simplified when one is only interested in β > 1 not too close to 1. Since P n (x) = a n + 1 -xP n-1 (x) for n ≥ 2, and P ′ 1 (x) = -1, the derivative of P n (x) is

P ′ n (x) = (-1) P n-1 (x) + xP ′ n-1 (x) = • • • = (-1) n x n-1 1 + n-1 j=1 P j (x) (-x) j . If x ∈ J n-1 , then 1 + n-1 j=1 P j (x) (-x) j > 1 -1 x -1 x 3 -• • • = x 2 -x-1 x 2 -1 . If moreover x ≥ (1+ √
5)/2, then we get that (-1) n P ′ n (x) > 0, hence P n is a strictly increasing (decreasing) function on

J n-1 ∩ [(1+ √ 5)/2, ∞) when n is even (odd). Moreover, lim n→∞ |P ′ n (x)| = ∞ if x ≥ (1+ √
5)/2 and x ∈ J n for all n ≥ 1. However, it is not true that P n is always increasing (decreasing) on J n-1 when n is even (odd). For instance, if a 1 a 2 • • • starts with 1001, then P 4 (x) = x 4 -2x 3 + x 2x + 2 and J 3 = (1, β] with β 3 = 2β 2β + 1 (β ≈ 1.755). The function P 4 decreases on (1, β ′ ], with β ′ ≈ 1.261, and increases on [β ′ , ∞). Note that this is a major flaw in the proof of Theorem 28 of [START_REF] Góra | Invariant densities for generalized β-maps[END_REF] (besides the fact that the statement is incorrect, as explained in the Introduction). This lack of monotonicity is what makes Theorems 1 and 3 more difficult to prove than the corresponding statements for β-expansions.

Proof of Theorem 2

Let a 1 a 2 • • • be a sequence of non-negative integers satisfying (1.4) and (1.5). We have already seen in the Introduction that these conditions are necessary to be the (-β)-expansion of -β β+1 for some β > 1. Moreover, β can only be the number given by Theorem 1. Then a 1 a 2 • • • is the (-β)-expansion of -β β+1 if and only if ∞ j=1 a k+j (-β) j = 1 β+1 for all k ≥ 1. Suppose first that ∞ j=1 a k+j (-β) j = 1 β+1 for some k ≥ 1, and let ℓ ≥ 1 be minimal such that β+1 , then the (-β)-expansion of -β β+1 is a [1,ℓ) (a ℓ +1), a 1 a 2 • • • is composed of blocks a [1,ℓ] 0 and a [1,ℓ) (a ℓ +1), and we have that a [1,ℓ) (a ℓ +1) > alt u 1 u 2 • • • , thus (1.8) does not hold. Therefore, (1.4), (1.5), (1.7), and (1.8) imply that a 1 a 2 • • • is the (-β)-expansion of -β β+1 for some (unique) β > 1. Suppose now that (1.7) does not hold, i.e., a 1 a 2 • • • ∈ {a [1,k] , a [1,k) (a k -1)0} ω \ {a [1,k] } for some k ≥ 1 with a [1,k] > alt u 1 u 2 • • • . We show that the sequence a [1,k] satisfies (1.4).

  and let L ′ β,n be the number of different sequences b 1 • • • b n such that I b 1 •••bn is an interval of positive length. (The latter is called the lap number of T n -β .)

  ) j = -β β+1 , then the (-β)-expansion of -β β+1 is a [1,ℓ] . Then a 1 a 2 • • • is composed of blocks a [1,ℓ] and a [1,ℓ) (a ℓ -1)0. Since ∞ j=1 a k+j (-β) j = 1 β+1 for some k ≥ 1, we have at least one block a [1,ℓ) (a ℓ -1)0, i.e., a 1 a 2 • • • ∈ {a [1,ℓ] , a [1,ℓ) (a ℓ -1)0} ω \ {a [1,ℓ] }. As a [1,ℓ] is the (-β)-expansion of -β β+1 , we have that a [1,ℓ] > alt u 1 u 2 • • • , thus (1.7) does not hold. If ∞ j=1 a ℓ+j (-β) j = 1

Acknowledgments

The author would like to thank Edita Pelantová for many fruitful discussions.

Suppose on the contrary that a [j,k] a [1,k] > alt a [1,k] for some 2 ≤ j ≤ k. This implies that a

satisfies (1.4) and (1.5), and we can apply Theorem 1 for this sequence. Let β ′ > 1 be the number satisfying (1.6) for the sequence a

β+1 . Suppose finally that (1.8) does not hold, i.e., a

As in the preceding paragraph, the number given by Theorem 1 for the sequence a

β+1 . Therefore, (1.7) and (1.8) are necessary for a 1 a 2 • • • to be the (-β)-expansion of -β β+1 for some β > 1.


Karine Altisen
email: karine.altisen@imag.fr

Matthieu Moy
email: matthieu.moy@imag.fr

Causality Closure for a New Class of Curves in Real-Time Calculus

Keywords: I.1.2 [Computing Methodologies]: Symbolic and Algebraic Manipulation-Algorithms; D.4.8 [Computer Systems Organization]: Performance of Systems-Modeling Techniques Real-Time Calculus, Causality, Algorithms

 is a framework to analyze heterogeneous real-time systems that process event streams of data. The streams are characterized by arrival curves which express upper and lower bounds on the number of events that may arrive over any specified time interval. System properties may then be computed using algebraic techniques in a compositional way.

The property of causality on arrival curves essentially characterizes the absence of deadlock in the corresponding generator. A mathematical operation called causality closure transforms arbitrary curves into causal ones.

In this paper, we extend the existing theory on causality to the class Upac of infinite curves represented by a finite set of points plus piecewise affine functions, where existing algorithms did not apply. We show how to apply the causality closure on this class of curves, prove that this causal representative is still in the class and give algorithms to compute it. This provides the tightest pair of curves among the curves which accept the same sets of streams.

INTRODUCTION

Modern embedded system design must deal with more and more constraints in several domains: an ever increasing Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. WCTT '11 November 29 2011, Vienna, UNK, Austria Copyright 2011 ACM 978-1-4503-1008-6/11/11 ...$10.00. size, deeply interdependent softwares and hardwares, timing constraints, low power constraints with power management mechanisms included. Furthermore, they have to be manufactured at low cost, and with an increasingly short life-cycle. In this context, it is no longer possible to wait for the physical prototypes to validate the decisions on the design of a system: hardware dimensioning (e.g. buffer size) and timing performance should be evaluated at an early stage of the development.

In this work, we focus on the performance evaluation of embedded systems using the Real-Time Calculus framework (RTC) [START_REF] Thiele | Real-time calculus for scheduling hard real-time systems[END_REF]. It uses abstract models to analyze heterogeneous systems in a compositional manner. It allows the characterization of streams of events to be treated by a component with curves called arrival curves: they provide the worst and best cases on the number of events that may arrive in any window of time of a given length. RTC also uses the notion of service curves, which count available resources instead of events in a similar manner. A given component's interface is described with curves for its input stream and available resources, and some other curves for the outputs. The huge advantage of RTC is its ability, for already-modeled components, to give exact bounds (i.e. both conservative and as tight as possible) on the output stream of a component as a function of its input stream. Unfortunately, complex components can not be modeled in RTC. In particular, RTC models cannot handle state-based components such as power managed systems.

Some works proposed RTC extensions using Event Count Automata [START_REF] Phan | Composing functional and state-based performance models for analyzing heterogeneous real-time systems[END_REF], Timed Automata [START_REF] Lampka | Analytic real-time analysis and timed automata: A hybrid method for analyzing embedded real-time systems[END_REF][START_REF] Lampka | Analytic real-time analysis and timed automata: a hybrid methodology for the performance analysis of embedded real-time systems[END_REF][START_REF]Cats tool[END_REF][START_REF] Altisen | Performance evaluation of components using a granularity-based interface between real-time calculus and timed automata[END_REF], and Synchronous Programs [START_REF] Altisen | ac2lus: Bringing SMT-solving and abstract interpretation techniques to real-time calculus through the synchronous language Lustre[END_REF]; all of those approaches perform the analysis using some formal verification tool (model-checking, abstract interpretation) and they all face the causality problem [START_REF] Altisen | Arrival curves for real-time calculus: the causality problem and its solutions[END_REF] in a way or another. They express the input arrival curves as a non-deterministic generator, or an observer of events that encodes the constraints of the curves. Arrival curves are functions of relative time that constrains the number of events that can occur in an interval of time: for any sliding window of time, the functions explicitly express the maximum and minimum number of events. But, arrival curves may also contain implicit constraints deduced from explicit ones. It may happen that the corresponding generator of events deadlocks, due to conflicting implicit constraints. Curves exhibiting such contradictions are called non-causal. They can thus lead to deadlocks in generators, but also to spurious counter-examples in formal verification, or simply to suboptimal results. Conversely, they can also be produced by non-exact computations: e.g. when a curve is computed after abstracting the system [START_REF] Altisen | Performance evaluation of components using a granularity-based interface between real-time calculus and timed automata[END_REF], using abstract interpretation [START_REF] Altisen | ac2lus: Bringing SMT-solving and abstract interpretation techniques to real-time calculus through the synchronous language Lustre[END_REF], or using a non-complete model-checking algorithm [START_REF] Phan | Composing functional and state-based performance models for analyzing heterogeneous real-time systems[END_REF]. It is therefore useful in some cases, mandatory in others, to solve this issue by transforming non-causal curves into causal ones.

This causality problem has been studied theoretically in [START_REF] Altisen | Arrival curves for real-time calculus: the causality problem and its solutions[END_REF]: this work provides an algebraic characterization of a causal pair of curves and defines the causality closure which makes the implicit constraints explicit. This operation, as a free side effect, results in the best pair of curves among the equivalent ones.

The present paper provides algorithms that extend and apply the results in [START_REF] Altisen | Arrival curves for real-time calculus: the causality problem and its solutions[END_REF]; it computes the causality closure on infinite curves with a particular shape. We focus on so-called Upac curves defined by a finite set of points followed by a piecewise convex/concave affine part. This class of curves is interesting since it enables to have a finite and simple computational encoding for the curves whereas curves are infinite. They may include a precise description for short windows of time, description with affine pieces for larger windows and then the long term rate curve. The Upac class includes (but is strictly larger than) the class of curves used in [START_REF] Lampka | Analytic real-time analysis and timed automata: A hybrid method for analyzing embedded real-time systems[END_REF], which cannot express non convex/concave curves. It is the one used in [START_REF] Altisen | ac2lus: Bringing SMT-solving and abstract interpretation techniques to real-time calculus through the synchronous language Lustre[END_REF] which computes the performance (given as arrival curves) of a system modeled as a synchronous program and uses bounded model-checking and abstract interpretation. In [START_REF] Altisen | ac2lus: Bringing SMT-solving and abstract interpretation techniques to real-time calculus through the synchronous language Lustre[END_REF], the causality closure is used to prevent the tool from computing spurious counter-examples in the proofs and to increase the precision of the result, but the actual algorithm and the underlying theory that handles causality for Upac curves were never published. This paper fills this gap with the following contributions:

• We identify a normal form on Upac curves, on which the causality closure can be computed easily; we prove that the causal representatives of such curves are still in the class; • We provide an algorithm that transforms a pair of curves of the class into normal form and then computes the causality closure, i.e. the causal representative of the curves. The algorithms are all in polynomial time (quadratic) and have been implemented in ac2lus.

The results of the paper are all proved (due to space limitations, full proofs only appear in the extended version of this paper [START_REF] Moy | Causality closure for a new class of curves in real-time calculus full version[END_REF], but the intuition is given here). Furthermore, although all along the paper we talk about arrival curves, the reader should be convinced that the results and the algorithms also apply to service curves in Real-Time Calculus, and strict service curves in network calculus [START_REF] Bouillard | Service curves in Network Calculus: dos and don'ts[END_REF], which behave the same.

The outline of this paper is as follows: Section 2 summarizes the Real-Time Calculus background and recalls the notion of causality from [START_REF] Altisen | Arrival curves for real-time calculus: the causality problem and its solutions[END_REF]; Section 3 defines the above class of curves and provides the first contribution of this paper: a normal form and a normalization algorithm. Section 4 gives the second contribution: an algorithm for the causality closure on those curves.

CAUSALITY IN REAL-TIME CALCULUS:

MOTIVATION AND FORMALIZATION

Real-Time Calculus Curves

The Real-Time Calculus focuses on components that process events; it uses curves to characterize the streams of events a component may compute. Event streams are abstracted with cumulative curves that represent the number of events that occurred since the origin of time t = 0. Arrival curves characterize the timing properties of a set of event streams using their cumulative curves. A pair of lower and upper arrival curves defines lower and upper bounds on the number of events allowed in a sliding window of ∆ unit of time. Since the goal of the paper is to define algorithms, we need the curves to be machine-representable. We consider the discrete-time fluid-event model where the time is discrete, but the event counters are rational-numbers. Notice that the definitions and characterization of the causality are nevertheless model-independent.

Formally, the cumulative curves and the arrival curves are functions from N (time) to Q + (number of events) where N is the set of naturals and Q + is the set of non-negative rationals. We note C the set of wide-sense increasing curves c from N to Q + = Q + ∪ {∞} and such that c(0) = 0; C is the set of such curves from N to Q + (no infinity value). The order on curves is point-wise.

Definition 1 (Cumulative Curves, Arrival Curves). Functions R ∈ C are called cumulative curves: R(t) represents the (finite) amount of events that occurred in the interval of time [0, t]. A pair of arrival curves is a pair of functions

(α u , α l ) in C × C, such that α l ≤ α u .
Let R be a cumulative curve and (α u , α l ) be a pair of arrival curves. R is said to satisfy

(α u , α l ) noted R |= (α u , α l ) iff ∀x ∈ N , ∀∆ ∈ N , R(x + ∆) -R(x) ∈ [α l (∆), α u (∆)].
We say that a pair of arrival curves (α u , α l ) is satisfiable iff there exists a cumulative curve R that satisfies (α u , α l ). The fact that arrival curves are defined on relative time (windows of size ∆) involves many implicit constraints. Among those constraints, some may be tighter than the constraints explicitly given by the curves. In [START_REF] Altisen | Arrival curves for real-time calculus: the causality problem and its solutions[END_REF], two kinds of implicit constraints were informally distinguished (see Figure 1). The first ones (as in the above explanation) remove regions called unreachable regions (see Figure 1(a)): no (finite nor infinite) cumulative curve can cross through those regions. The removal is done using the sub and super additive closures of the curves which are briefly recalled here, but this result is well-known and detailed in e.g. [START_REF] Boudec | Network Calculus[END_REF]. For example, splitting a window of size ∆ into two windows of size ∆1 and ∆2 (s.t. ∆1 + ∆2 = ∆) may reveal a greater bound α l (∆1) + α l (∆2) for α l (∆). This removes some regions from the curve and leads to an equivalent but tighter pair of arrival curves.

Definition 2 (Sub and Super Additive Closures).

Let α ∈ C. α is said to be sub-additive (resp. superadditive) iff ∀s, t ∈ N . α(t + s) ≤ α(t) + α(s) (resp α(t + s) ≥ α(t) + α(s)). Among all the sub-additive (resp. super-additive) curves that are smaller (resp. greater) than α there exists an upper (resp. lower) bound called the subadditive (resp. super-additive) closure of α and denoted by α (resp. α).

A pair of arrival curves (α u , α l ) is sub-additive and superadditive (denoted SA-SA for short) iff α u is sub-additive and α l is super-additive. We note (α u , α l ) the SA-SA closure of (α u , α l ).

The SA-SA closure makes explicit the unreachable regions of the curves: they are the regions between α l and its superadditive closure α l in the one side, between α u and its subadditive closure α u on the other.

Causality and the Causality Closure

The second kind of constraints removes the forbidden regions: no execution can cross a forbidden region without being blocked some time latter by some contradiction between lower and upper constraints (for example, being forced to emit more than 2 events but less than 1 which is not possible). In other words, there cannot exist an infinite cumulative curve that crosses through such a region (see Figure 1(b)). It may occur due to the forbidden regions of some implicit constraints that an event stream (represented by a cumulative curve) satisfies a pair of arrival curves up to a certain time T , but then deadlocks since no time can elapse and no event can be emitted without violating the arrival curves. A pair of arrival curves for which this problem cannot happen is called causal.

Issues and Solutions with Non-Causal Curves. The causal-

ity problem has received surprisingly little attention in the Real-Time Calculus community, although many of the existing approaches which connect Real-Time Calculus to other formalisms (e.g. [START_REF] Lampka | Analytic real-time analysis and timed automata: A hybrid method for analyzing embedded real-time systems[END_REF][START_REF] Künzli | Generating event traces based on arrival curves[END_REF][START_REF] Phan | Composing functional and state-based performance models for analyzing heterogeneous real-time systems[END_REF]) did produce, or have problems with non-causal pairs of curves.

Indeed, non-causal curves can be produced by non-exact algorithms, that is, whenever a conservative approximation is performed in a computation. This is the case when using techniques like abstract interpretation, model-checking algorithms with a timeout like in [START_REF] Altisen | ac2lus: Bringing SMT-solving and abstract interpretation techniques to real-time calculus through the synchronous language Lustre[END_REF], or when abstractions are performed on the model before the computation [START_REF] Altisen | Performance evaluation of components using a granularity-based interface between real-time calculus and timed automata[END_REF]. It can also happen when an algorithm computes only part of the points of an arrival curve, like done in [START_REF] Phan | Composing functional and state-based performance models for analyzing heterogeneous real-time systems[END_REF].

When an algorithm produces non-causal curves, the causality closure provides another pair of curve which is equivalent and tighter, somehow increasing the precision of the result. See [START_REF] Altisen | Performance evaluation of components using a granularity-based interface between real-time calculus and timed automata[END_REF] for an example where such a post-treatment of the curve leads to a better precision.

In addition to their sub-optimality, non-causal curves can be a real issue if used as input of some algorithms. Most model-checking algorithms may produce spurious counterexamples if fed with non-causal hypothesis. It is possible to solve the non-causality during the state-space exploration either in the tool itself (see for example the -causal option of Lesar [START_REF] Halbwachs | Programming and verifying critical systems by means of the synchronous data-flow programming language lustre[END_REF]) or with an appropriate temporal logic formula as proposed in [START_REF] Lampka | Analytic real-time analysis and timed automata: a hybrid methodology for the performance analysis of embedded real-time systems[END_REF], but this leads to costly algorithms, and is not applicable with any tool (for example, Nbac, used in [START_REF] Altisen | ac2lus: Bringing SMT-solving and abstract interpretation techniques to real-time calculus through the synchronous language Lustre[END_REF] cannot do it). As opposed to this, the causality closure can be applied a priori on the curves regardless of the tool being used for the analysis, and with much cheaper algorithms.

Non-causal curves would also greatly complexify the design of an event generator for simulation-based approaches [START_REF] Künzli | Combining simulation and formal methods for system-level performance analysis[END_REF]: the usual implementations generate event streams that satisfy the constraints up to the current point in time, but doing so may result in deadlocks in the future (contradiction between the upper-bound and the lower-bound). A generator for noncausal curves would therefore have to explore the reachable state-space in the future to make sure a deadlock will not occur. Again, it is much simpler, and cheaper algorithmically, to make the curves causal a priori.

In summary, 1) when computing output curves as functions of input curves, applying the causality closure on inputs allows to get rid of the causality problem and therefore to use any method, even if it is not robust to non-causal inputs. And 2) applying the causality closure on the output may increase the precision of the result, providing the best equivalent output curves.

Characterization of Causality.

The following paragraph recalls the formal definition of causality and the main results from [START_REF] Altisen | Arrival curves for real-time calculus: the causality problem and its solutions[END_REF] which are used in this paper.

Definition 3 (Causal Arrival Curves). Let (α u , α l ) be a pair of arrival curves. (α u , α l ) is said to be causal iff for any T ∈ N , any cumulative curve R that satisfies (α u , α l ) up to T can be extended forever into a cumulative curve R ′ that also satisfies (α u , α l ). In other words,

(α u , α l ) is causal iff ∀T ≥ 0, ∀R, R |= ≤T (α u , α l ) =⇒ ∃R ′ | R ′ |= (α u , α l ) and ∀t ≤ T, R(t) = R ′ (t)
where the fact that R satisfies (α u , α l ) up to T is defined by: R

|= ≤T (α u , α l ) iff ∀t ≤ T, ∀∆ ≤ t, R(t) -R(t -∆) ∈ [α l (∆), α u (∆)].
We now give an algebraic characterization of causality. Intuitively, let us consider some pair of curves (α u , α l ), and a cumulative curve R such that R(T ) = α l (T ). We now look at an extension of R for x units of time after T . The number of events to emit between T and T + x (i.e. R(T + x) -R(T )) has to be lower than α u (x), but the total number of event since the beginning (i.e. R(T + x)) has to be greater than α l (T + x). Since we have chosen R(T ) = α l (T ), this means that the number of events emitted between T and T + x has to be at least α l (T + x)α l (T ). Combining the constraints on α u and α l , we deduce that for (α u , α l ) to be causal, we must have ∀x ≥ 0,

α u (x) ≥ R(T + x) -R(T ) ≥ α l (T + x) -α l (T ), hence α l (T ) ≥ sup x≥0 α l (T + x) -α u (x) = α l ⊘ α u (T )
. This example is far from being a proof, but gives a part of the intuition, and exhibits a formula using the deconvolution operator ⊘. Following this intuition, it was shown in [START_REF] Altisen | Arrival curves for real-time calculus: the causality problem and its solutions[END_REF] a necessary and sufficient condition for the causality, based on this formula: a pair of curves is causal iff its SA-SA closure is stable when applying some deconvolutions on it. We use the classical (min, +) (resp. (max, +)) deconvolution operators [START_REF] Boudec | Network Calculus[END_REF] ⊘ and ⊘ : for c and

d in C, for x ≥ 0, (c ⊘ d)(x) def = sup t≥0 {c(x + t) -d(t)} and (c ⊘ d)(x) def = inf t≥0 {c(x + t) -d(t)}.
Theorem 1 (Characterization of Causality). Let (α u , α l ) be a pair of arrival curves:

(α u , α l ) is causal ⇐⇒ α l = α l ⊘ α u and α u = α u ⊘ α l
Notice that the causality, unlike SA-SA properties, is a property on a pair of curves; it does not make sense to say that α u alone, or α l alone, is causal since the impossibility to extend a cumulative curve can come only from a contradiction between an upper bound and a lower bound.

Given a pair of arrival curves, the removal of its forbidden regions is achieved using deconvolution operators, as a direct consequence of the characterization.

Definition 4 (The C operator). A pair (α u , α l ) of arrival curves has been defined as functions in C × C such that α u ≥ α l (see Definition 1). We note ⊥ AC the set of pairs of functions in C × C such that the former constraint is false; ⊥ AC will be considered as a single element, for simplicity, even if it represents an infinite set of objects. Let AC be the set of all pairs of arrival curves plus ⊥ AC . The operator C, is defined from AC to AC as:

C (⊥ AC ) def = ⊥ AC C α u , α l def = let C u = α u ⊘ α l , C l = α l ⊘ α u if C u ≥ C l then (C u , C l ) else ⊥ AC
The operator C makes explicit some implicit constraints of the curves and removes some forbidden regions. In some cases, it may occur that the lower and the upper curve cross over: this means that the curves were not satisfiable (i.e. no cumulative curve satisfies it); this is denoted with the ⊥ AC value. As opposed to this, when the curves were satisfiable, the operator computes a causal pair of curves equivalent to the original ones.

Theorem 2. For any pair of arrival curves (α u , α l ),

• C(α u , α l ) = ⊥ AC ⇐⇒ (α u , α l ) is non-satisfiable; • C(α u , α l
) is causal, SA-SA and equivalent to (α u , α l ), otherwise. When (α u , α l ) is satisfiable, C(α u , α l ) is the tightest pair of curves equivalent to (α u , α l ). Conversely, if (α u , α l ) is the tightest pair of curves representing a set of cumulative curves, then (α u , α l ) is causal.

By tightest, we mean the smallest (resp. the greatest) curve for the upper (resp. lower) part among the set of equivalent pairs of arrival curves. Given a pair of curves, one can compute the causality closure C(α u , α l ), and get either the information that the curves are not satisfiable, or the tightest causal representative of the original arrival curves.

ULTIMATELY PIECEWISE AFFINE CURVES

We now study the set of Upac curves comprising both a finite prefix given by a set of points and a long-term rate given by a piecewise-affine, convex/concave pairs of curves. This class of curves is the one used in the tool ac2lus [START_REF] Altisen | ac2lus: Bringing SMT-solving and abstract interpretation techniques to real-time calculus through the synchronous language Lustre[END_REF]. It was chosen to be both expressive and adapted to interfacing with other formalisms.

A wider class is the one of ultimately periodic curves, widely used in analytical models (like the MPA-RTC toolbox [START_REF] Wandeler | Modular Performance Analysis and Interface-Based Design for Embedded Real-Time Systems[END_REF]). This class is expressive, but hard to use in the interfacing with state-based formalisms. Most interfacing approaches restrict to a much stricter class. For example, [START_REF] Lampka | Analytic real-time analysis and timed automata: A hybrid method for analyzing embedded real-time systems[END_REF] use convex/concave piecewise affine curves. An extension to non-convex/concave curves is proposed in [START_REF] Lampka | Analytic real-time analysis and timed automata: a hybrid methodology for the performance analysis of embedded real-time systems[END_REF], but involves more complex synchronization of automata, hence a greater algorithmic complexity. [START_REF] Altisen | Performance evaluation of components using a granularity-based interface between real-time calculus and timed automata[END_REF] and [START_REF]Cats tool[END_REF] use discrete, finite curves, which are not able to express precisely the long-term rate of the streams. [START_REF] Phan | Composing functional and state-based performance models for analyzing heterogeneous real-time systems[END_REF] can use any ultimately periodic curve to model the input of a component, but the output computed has a periodic part limited to a single entry (a long term period), hence, the generality of the model is not exploited.

The Upac class is basically a combination of the finite, discrete curves from [START_REF]Cats tool[END_REF], with the convex/concave curves of [START_REF] Lampka | Analytic real-time analysis and timed automata: A hybrid method for analyzing embedded real-time systems[END_REF]. It allows a precise and possibly non-convex/concave description of the initial portion of the curves, as well as a set of constraints on the long-term rate of the event stream; it may be easily machine-representable: the finite portion is basically an array and each affine piece is encoded with its slope and its Y -intercept.

We first define this class of curves. The goal is to obtain an algorithm that computes the causality closure on Upac. In order to do that, we define a normal form and we propose an algorithm to compute for each curve in Upac its normal form. This is the first step for the computation of the causality closure: the normal form is SA-SA and the C operator will be easily (in a computational manner) applicable on the normal form of the curve.

Upac: Formal Definitions

Definition 5 (Upac). We define the class of Upac curves as the set of pairs of curves (α u , α l ) such that there exists

• P (α u ), P (α l ) ∈ N : size of the finite prefix (i.e. abscissa of the last point explicitly given in the representation); • N (α u ), N (α l ) ∈ N : number of pieces of the piecewise affine part of the curves;

• a set of values p u i ∈ N , i ∈ [0, P (α u )]
, and a set of rational values a u j , b u j , j ∈ [1, N (α u )]: representation of the curve α u ; • a set of values p l i ∈ N , i ∈ [0, P (α l )], and a set of rational values a l j , b l j , j ∈ [1, N (α l )]: representation of the curve α l ; such that, ∀∆ ≥ 0:

F u (∆) = if ∆ ∈ [0, P (α u )] then p u ∆ else + ∞; F l (∆) = if ∆ ∈ [0, P (α l )] then p l ∆ else p l P (α l ) ; I u (∆) = if N (α u ) > 0 then min j∈[1,N (α u )] a u j ∆ + b u j else + ∞; I l (∆) =    if N (α l ) > 0 then max j∈[1,N (α l )] a l j ∆ + b l j else 0; with α u (∆) = min {F u (∆), I u (∆)} and α l (∆) = max F l (∆), I l (∆) .
The tuple P (α u ),

P (α l ), N (α u ), N (α l ), {p u i } i∈[0,P (α u )] , {a u j , b u j } j∈[1,N (α u )] , {p l i } i∈[0,P (α l )] , {a l j , b l j } i∈[1,P (α l )]
is called the representation of the pair (α u , α l ). It corresponds to the data-structure to be used in algorithms. We call the set of points p u i and p l i the finite prefix and each line aj∆ + bj the affine pieces of (α u , α l ).

Note that we require the individual points to be integers (this will be necessary to ensure the convergence of the algorithms later), but remain in the fluid-event model. Figure 2 shows an example: the upper part is made of 3 points and two affine pieces; the lower part, 3 points, one affine piece.

Normal form in Upac

To compute the causality closure on Upac curves, the difficulty comes from the points of α u and α l , which can interact together, or with the affine pieces of the other curve. In particular, arbitrary curves with points and affine pieces are not necessarily SA-SA. We will first transform the curves to ones that obey a few well-formedness properties, which we call the normal form.

The causality closure is trivial if the curves have only affine pieces, as expressed later in Theorem 5. Curves comprising only points are not SA-SA, and could not be made so algorithmically (since their SA-SA closure has an infinite number of points). This difficulty can be eliminated thanks to the piecewise affine part of the curves: we can apply the SA-SA closure to the points of the curves, and only a finite number of points will remain under or above the affine pieces. If this is not the case, then it means the affine pieces add no information and can be removed. This transformation is called the normalization, and is presented in Algorithm 1; it leads to a SA-SA curve (Theorem 4) made of points and affine pieces. This allows to apply the C operator on it to get a causal pair of curves. The computation of C is made easier by Theorem 6, which reduces the computation of C to a version where all the operators are bounded.

Properties of SA-SA Closure of Finite Prefix

We first focus on the finite prefix (i.e. the points) of Upac curves, in order to introduce two intermediate results that will be useful in the computation of the normal form and of the causality closure.

We first need to define properly the notion of "finite curves" and the associated operators. We define "finite curves" as restriction of infinite ones: the restriction of (α u , α l ) to [0, T ] is defined as:

∀t ≤ T, α u T (t) def = α u (t) and α l T (t) def = α l (t) ∀t > T, α u T (t) def = +∞ and α l T (t) def = α l (T )
This way, α u T and α l T match the intuition of finite curves, can be easily represented with a finite set of points, but are still infinite objects on which the usual theorems apply. This notion matches the Upac subset of curves with no affine pieces (N (α l ) = N (α u ) = 0). ). The situation is illustrated on Figure 3, representing an upper curve defined explicitly up to ∆ = 3, and its sub-additive closure.

It should be noted that, in this case, (α u , α l ) is no longer a Upac curve, since it has an infinite number of points (as far as ∃t > 0.α u (t) < +∞). However, one can define the property SA-SA up to P and the associated closure (see [START_REF] Altisen | Arrival curves for real-time calculus: the causality problem and its solutions[END_REF] for details): the SA-SA closure up to P and (α u , α l ) will be identical on [0, P ]. Additionally, [START_REF] Bouillard | An algorithmic toolbox for network calculus[END_REF] (page 7), provides an efficient way to compute the sub-additive closure in discrete events. It can easily be adapted to compute the SA-SA closure over [0, P ] leading to a simple, quadratic algorithm. The SA-SA closure up to P (α l ) (resp. P (α u )) can be applied to the finite prefix of any pair of curves in Upac. The finite prefix of α u (resp. α l ) allows us to compute the slope S P (α u ) (resp. S P (α l )) of the curve, the point of maximal influence ∆ P (α u ) (resp. ∆ P (α l )), and the maximal drift d P m (α u ) (resp. d P m (α l )) defined as follows and illustrated in Figure 3. Definition 6. Let (α u , α l ) be a pair of arrival curves, and P > 0. We define the following:

S P (α u ) def = min ∆≤P {α u (∆)/∆} ∆ P (α u ) def = min{∆ ∈ [0, P ] | S P (α u ) × ∆ = α u (∆)} d P m (α u ) def = sup ∆≤∆ P (α u )
{α u (∆) -S P (α u ) × ∆} S P (α l ), ∆ P (α l ) and d P m (α l ) are defined in a symmetrical way.

Since we work here in discrete time, the min and max are over finite sets and are well-defined.

Interesting properties of the definitions are given by the following lemma. The sub-additive closure of the curve remains above the line S P (α u ) × ∆ defined by the slope (Lemma 2). The distance of the curve to this line remains bounded, and the bound d P m (α u ) depends only on the finite prefix (Lemma 3). Also, α u will actually have contact with the line S P (α u ) × ∆ at least periodically, with a period of ∆ P (α u ) which is smaller than the size of the finite prefix (Lemma 1). Lemma 1. Let (α u , α l ) be a pair of arrival curves and T > 0. Then:

∀k ∈ N , α u T (k × ∆ P (α u )) = k × ∆ P (α u ) × S P (α u ) α l T (k × ∆ P (α l )) = k × ∆ P (α l ) × S P (α l )
Lemma 2. Let (α u , α l ) be a pair of arrival curves and T > 0. Then:

∀∆, α u (∆) ≥ α u T (∆) ≥ S P (α u ) × ∆ α l (∆) ≤ α l T (∆) ≤ S P (α l ) × ∆ Lemma 3. Let (α u , α l
) be a pair of arrival curves. Then: #events As a consequence, affine pieces a∆ + b with a slope steeper than S P (α u ) × ∆ do not add information to the curve (provided the explicit points of α u are below the affine piece), and can be removed. Theorem 3. Let (α u , α l ) be a pair of arrival curves in Upac, different from ⊥ AC , and J ∈ [1, N (α u )] such that these two conditions are satisfied:

∀∆ ≥ 0, α u (∆) -S P (α u ) × ∆ ≤ d P m (α u ) S P (α l ) × ∆ -α l (∆) ≤ d P m (α l )
∆ S P (α u ) 2 α u S P (α u ) × ∆ ∆ P (α u ) d P m (α u )
∀i ∈ [0, P (α u )], ∀j ∈ [1, N (α u )], p u i ≤ a u j × i + b u j a u J ≥ S P (α u )
Then, removing the affine piece a u J + b u J from (α u , α l ) yields an equivalent curve. In this case, we say that the affine piece

a u J + b u J is not relevant. Similarly for α l , if ∀i ∈ [0, P (α l )], ∀j ∈ [1, N (α l )], p l i ≤ a l j × i + b l j a l J ≥ S P (α l )
Then, removing the affine piece a l J + b l J from (α u , α l ) yields an equivalent curve.

Normal Form: Definition and Algorithm

We now have the necessary background to introduce the normal form, on which the causality closure will be computed: Definition 7 (Normal form of curves in Upac). A pair of arrival curves (α u , α l ) in U pac is said to be in normal form if P (α u ) = P (α l ) = P and at least one of the following conditions is satisfied:

1. (α u , α l ) = ⊥ AC 2. N (α u ) = N (α l ) = 0 and (α u , α l ) is SA-SA up to P 3. N (α u ) = 0, α u is
sub-additive up to P and α l is superadditive. 4. N (α l ) = 0, α l is super-additive up to P and α u is sub-additive. 5. (α u , α l ) is SA-SA Case 2 corresponds to the case of finite curves [START_REF] Altisen | Arrival curves for real-time calculus: the causality problem and its solutions[END_REF]. In this case, we say that (α u , α l ) has no relevant affine pieces. Cases 3 and 4 correspond to asymmetric cases where only one of α u and α l has relevant affine pieces. In these cases, we consider the SA-SA curves in theory, but the representation is restricted to the SA-SA set of points on the prefix.

Converting an arbitrary pair of curves into a normal-form is straightforward using the properties stated in Section 3.2.1; the algorithm is given below. For the common case where both curves have relevant affine pieces (case 5), the transformation of a pair of curves into normal form is illustrated by Figure 4. It essentially consists in adding explicit points to the curve until one can be sure all the points are above the affine pieces. In the general case, the transformation is as follows.

Algorithm 1 (Normalization of curves in Upac). For any curve in Upac, we apply the steps:

1. Make sure all the explicit points p u i (resp. p l i ) are under (resp. above) all affine pieces; if not, modify p u i (resp. p l i ), keeping integer abscissa; add points on α u or α l until P (α u ) = P (α l ) = P . See Figure 4.(b). 2. Eliminate affine pieces of α u (resp. α l ) which have a slope greater or equal (resp. lower or equal) to S P (α u ) (resp. S P (α l )). It can be proved that this does not change the curve. See Figure 4.(c). Then, multiple cases can occur:

If N (α u ) = N (α l ) = 0 then 3.
Apply the SA-SA closure up to P . If N (α u ) = 0 and N (α l ) = 0 then 3. Compute the abscissa M u j of the intersection between S P (α u ) × ∆ and the affine piece j of α u (and similarly M l for α l ). Set M u = minj{M u j }, M l = minj{M l j }, M = max{M u , M l }. 4. Add explicit points p u and p l to the curves, so that P (α u ) = P (α l ) = M . 5. Apply the SA-SA closure up to M to (α u , α l ). See Figure 4.(d). If N (α u ) = 0 and N (α l ) = 0 then 3. Compute the abscissa M u j of the intersection between S P (α u ) × ∆ and the affine piece j of α u . Set M = minj{M u j }. 4. Add explicit points p u and p l to the curves, so that P (α u ) = P (α l ) = M . 5. Apply the SA-SA closure up to M to (α u , α l ). If N (α u ) = 0 and N (α l ) = 0 then apply the same transformation as above, replacing α l by α u and vice-versa in the text.

The normalization trivially implies SA-SA closure up to M . The SA-SA property is actually true for the whole curve, when it has some relevant affine pieces: Theorem 4. Let (α u , α l ) be a pair of curves obtained by applying the normalization (Algorithm 1) on a pair of curves in Upac. Then (α u , α l ) is in Upac and in normal form. In particular, if α l (resp. α u ) has at least one relevant affine piece, then α l is super-additive (resp. sub-additive).

CAUSALITY CLOSURE IN Upac

First, the algorithm for the causality closure applies the normalization on the curves. Then, the idea is to apply Theorem 2 with the operator C (see Definition 4) on the curves: the theorem states that C α u , α l is the causality closure of (α u , α l ). This step is divided into 2 parts. The part where the curves have no relevant affine pieces at all was treated in [START_REF] Altisen | Arrival curves for real-time calculus: the causality problem and its solutions[END_REF] and is quickly recalled in Section 4.1; it requires a fix-point computation. The other part of the algorithm factorizes the three other cases where curves have at least one affine piece (no affine pieces on α l , no affine pieces on α u , both curves with affine pieces) and is provided in Section 4.2.

Curves With No Affine Pieces

For curves in normal form in Upac with no relevant affine pieces at all (case 2 of the normal form), the algorithm has been proposed in [START_REF] Altisen | Arrival curves for real-time calculus: the causality problem and its solutions[END_REF] and is briefly summarized here. The major difficulty for the curves with only a finite prefix is that their SA-SA closure is not representable with a finite number of points; so we cannot directly use the result of Theorem 2. Instead, we use the fact that any fix-point of C is causal. Therefore, the algorithm iterates the computation of C on the finite prefix of the curves; the termination is ensured by the fact that the points of the prefix are natural numbers. The iteration either reaches the ⊥ AC value (the curves were not satisfiable) or a causal curve equivalent to the original one. Computing the finite SA-SA closure on the resulting curves provides the expected result.

C for Curves With at Least One Affine Piece

As a first remark, let us consider the particular case of convex/concave affine piecewise curves. This is an interesting class of curves in Upac, used for example in [START_REF] Lampka | Analytic real-time analysis and timed automata: A hybrid method for analyzing embedded real-time systems[END_REF][START_REF] Lampka | Analytic real-time analysis and timed automata: a hybrid methodology for the performance analysis of embedded real-time systems[END_REF]. It corresponds to the particular case where the finite prefix uniquely contains (0, 0). An interesting property is that α u (resp α l ) can be expressed as the minimum (resp. maximum) of a set of affine functions. When reasoning about these curves, the minimum and maximum are naturally translated in conjunction of conditions. Those curves are always causal: Theorem 5. Let (α u , α l ) = ⊥ AC be a pair of piecewise affine, concave/convex curves. Then (α u , α l ) is causal.

We now focus on the general case, i.e. curves in normal form in Upac, with either α l , α u or both having affine pieces: N (α u ) > 0 or N (α l ) > 0. We show that we can directly apply the operator C on the curves and that its computation can be done in quadratic time. Theorem 6. Let (α u , α l ) be a pair of curves in Upac, in normal form, such that (α u , α l ) = ⊥ AC , with either α u or α l having relevant affine pieces. Let M = P (α l ) = P (α u ) be the index of the last point of (α u , α l ) given explicitly (as it

was computed in Algorithm 1). Let C M = C M u , C M l be the following operator: ∀∆ ≥ 0, C M u α u , α l (∆) = inf t∈[0,M ] {α u (∆ + t) -α l (t)} and C M l α u , α l (∆) = sup t∈[0,M ] {α l (∆ + t) -α u (t)} 1. ∀∆ ≥ 0, C α u , α l (∆) = C M α u , α l (∆) 2. If N (α u ) = 0 then ∀∆ > M , C u α u , α l (∆) = α u (∆) 3. If N (α l ) = 0 then ∀∆ > M , C l α u , α l (∆) = α l (∆)
We give the intuition of the proof (see [START_REF] Moy | Causality closure for a new class of curves in real-time calculus full version[END_REF] for details) with an affine piece of α l , and consider its interaction with the finite prefix of α u . We consider the slope S P (α u ) of the finite prefix and the slope a of the affine piece. If S P (α u ) ≥ a, then according to the results of Section 3.2.1, the curve α u will remain above S P (α u ) × ∆ and it cannot create any forbidden region with the affine piece. If S P (α u ) is lower than a, then we know that α u will "touch" periodically S P (α u ) × ∆ and will eventually end up below the affine piece. This implies that the curves are not satisfiable.

As a consequence, the C operator can easily be computed algorithmically: for each point to compute, the inf{} and the sup{} can be computed with a simple for loop iterating from 0 to M . The expression of C M α u , α l includes a SA-SA closure. When the curve has affine pieces, it is already SA-SA, hence no SA-SA closure needs to be applied. However, for curve with no affine pieces, since we only use the values of the SA-SA curves for ∆ ≤ 2M , it is sufficient to compute the SA-SA closure up to 2M . Furthermore, when the curve has at least one affine piece, this computation has to be done for the points of abscissa from 0 to M , the other points are given by the original curve itself.

Based on these remarks, the causality closure algorithm for Upac curves with at least one relevant affine piece follows: • In all cases, the affine pieces do not change (this is ensured by cases 2 and 3 of theorem 6):

a u * j = a u j , b u * j = b u j , a l * k = a l k , b l * k = b l k
• To compute the points p * i of the finite prefix, define (α u 2M , α l 2M ), a pair of curves: if N (α u ) = 0 then α u 2M = α u else the finite prefix of α u 2M is the subadditive closure of α u up to 2M and it has no affine pieces (likewise for α l 2M ). Then:

p u * i = C M u (α u 2M , α u 2M ) (i), p l * i = C M l (α u 2M , α u 2M ) (i)

CONCLUSION

This paper provides an algorithm to compute the causality closure on an interesting class of curves, already used in several tools [START_REF] Lampka | Analytic real-time analysis and timed automata: A hybrid method for analyzing embedded real-time systems[END_REF][START_REF] Altisen | ac2lus: Bringing SMT-solving and abstract interpretation techniques to real-time calculus through the synchronous language Lustre[END_REF]: curves with a finite prefix made of points, followed by convex/concave affine pieces. This class enables the precise modeling of the beginning of the curves together with the long term rate information. For this class of curves, the operators which compute the causality closure cannot be straightforwardly deduced from the initial work on causality closure [START_REF] Altisen | Arrival curves for real-time calculus: the causality problem and its solutions[END_REF]. This new algorithm can handle all the cases of curves in the class; it is efficient, quadratic in complexity (with reasonably-sized curves, this means the computation is almost instantaneous).

Furthermore, while the problem appeared to be relatively simple, the algorithm relies on several theorems, whose proofs were indeed non-trivial [START_REF] Moy | Causality closure for a new class of curves in real-time calculus full version[END_REF].

This work completes the theoretical and computational foundations for the connection of Real-Time Calculus to synchronous languages, implemented in the tool ac2lus [START_REF] Altisen | ac2lus: Bringing SMT-solving and abstract interpretation techniques to real-time calculus through the synchronous language Lustre[END_REF]. Further works include to apply it to larger and more realistic case studies. This may involve using other verification tools and may require changes in the abstractions used to represent the set of streams.

Figure 1 :

 1 Figure 1: Implicit constraints on arrival curves

Figure 2 :

 2 Figure 2: Example of a Upac curve

The

Figure 3 :

 3 Figure 3: Point of maximal influence of α u . The curve α u remains in the greyed area and has contact with S P (α u ) × ∆ at least with period ∆ P (α u ).

  After step 1: p u 1 pulled below the affine piece.

Figure 4 :

 4 Figure 4: Step by step transformation into normal form

Algorithm 2 .

 2 Given a pair of curves (α u , α l ) in Upac in normal form represented byp u i , a u j , b u j , p l i , a l k , b l k (i ∈ [0, M ], j ∈ [1, N (α u )], k ∈ [1, N (α l )]), we denote by p u * i , a u * j , b u * j , p l * i , a l * k , b l *k the representation of the causality closure C α u , α l . This representation is computed as follows:

2 Figure 5 :Figure 5

 255 Figure 5: Causality Closure on a Upac Curve With One Affine Piece