Meriem Halimi

Gilles Millérioux

Jamal Daafouz Mode

Mode detection and discernability as a framework for the estimation of time-varying delays

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

Mode detection and discernability as a framework for the estimation of time-varying delays

Mereim Halimi 1,2 and Gilles Millérioux 1,2 and Jamal Daafouz 1,2 Abstract-In this paper, it is shown how the issue of reconstructing time-varying unknown delays for linear systems can be turned into a mode detection one for switched affine systems. The specificities due to this reformulation are highlighted. The property of discernability, that is the ability for a detector to deliver a unique solution, is specifically addressed. An example is given as an illustration of the efficiency of the approach.

Time-delay systems have been the subject of intensive researches over the years. This is due to the fact that time delays are inherent in many real physical systems, such as mechanical systems, chemical processes, biology, transportation or communication systems and econometric models. The estimation of time delays of dynamical systems has received considerable attention in automatic control. Although a review and a comparison of time-varying delays estimation approaches have been proposed in the literature, see [START_REF] Bjorklund | A Review of Time-Delay Estimation Techniques[END_REF] and more recently [START_REF] Belkoura | Parameters estimation of systems with delayed and structured entries[END_REF], most of the available methods are dedicated to continuous systems. The problem of the estimation of the delay for discrete-time systems is rather scarce and motivates the present work. It is shown that such an issue for linear systems can be turned into a special mode detection one for switched affine systems.

An important concept for mode detection purpose is the so-called discernability. Roughly speaking, discernability reflects the ability of discriminating the active sequence from any other ones. In other words, it deals with the matter of uniqueness. A sufficient condition for discernability to hold is the observability [START_REF] Vidal | Observability and Identifiability of Jump Linear Systems[END_REF]. However, less restrictive conditions can be found in the literature like (η, ω)-discernability [START_REF] Alessandri | Receding-Horizon Estimation for Switching Discrete-Time Linear Systems[END_REF], Backward Discernability and Forward Discernability [START_REF] Babaali | Asymptotic Observers for Discrete-Time Switched Linear Systems[END_REF]. For systems with input, discernability deserves a special treatment because it depends on the input sequence. In this respect, the so-called active mode observation has been addressed in [START_REF] Babaali | Observability of Switched Linear Systems[END_REF], [START_REF] Baglietto | Active mode observability of switching linear systems[END_REF] and [START_REF] Baglietto | Active mode observation of switching linear systems based on set-valued estimation on the continuous state[END_REF] where a distinction between discerning control sequences over a finite or an infinite horizon of time is made. In this paper, discernability is tackled in the special context of the estimation of timevarying delays. This paper is organized as follows. Section I is devoted to the problem statement. The reformulation of the estimation of time-varying delays as a mode detection problem for switched affine systems is carried out. In section II, discern-ability is discussed in the general context. It is introduced the notion of (λ)-discernability. In Section III, discernability and mode detection methodologies are particularized for the purpose of time-varying delays estimation. The paper ends up with an illustrative example in Section IV. Notation: N is the set of natural numbers. R n is the ndimensional set of real numbers. 1 is the identity matrix and 0 is the zero matrix, being both of appropriate dimension when unspecified. X T is the transpose of the matrix X. The matrix X † stands for the generalized inverse (Moore-Penrose) of X satisfying X † X symmetric, XX † symmetric, XX † X = X and X † XX † = X † . The kernel (null space) of X is denoted ker(X). R(X) is the column range space of X. The rank of a matrix X is denoted rank(X).

I. PROBLEM STATEMENT

Let us consider the discrete-time affine delayed system given by

X k+1 = AX k + GX k-τ (k) + BU k-τ (k) + E Y k = CX k + DU k ( 1
)
where k is the natural number standing for the discretetime, As a clue to tackle this problem, we can interestingly point out that such an issue can be reformulated as a mode detection problem of an equivalent switched affine system. Indeed, despite a different purpose, the same lines of reasoning than the ones suggested in [START_REF] Hetel | Equivalence Between the Lyapunov-Krasovskii Functional Approach for Discrete Delay Systems and the Stability Conditions for Switched Systems[END_REF] [12] can be followed, that is, a switched system transformation approach can be used. It is detailed below. Let σ be a function σ : N → J which, at any time k, uniquely identify the pair (τ (k), τ (k)) ∈ T × T according to the following one-to-one correspondence:

X k ∈ R N is the state vector, Y k ∈ R M is the output, U k ∈ R P is the input. The matrices A ∈ R N ×N , G ∈ R N ×N , B ∈ R N ×P , C ∈ R M ×N , D ∈ R M ×P and E ∈ R N ×1
(τ (k), τ (k)) = (0, 0) ↔ σ(k) = 1, (τ (k), τ (k)) = (1, 0) ↔ σ(k) = 2, . . . , (τ (k), τ (k)) = (α, 0) ↔ σ(k) = α + 1, (τ (k), τ (k)) = (0, 1) ↔ σ(k) = α + 2, . . . , (τ (k), τ (k)) = (0, α ) ↔ σ(k) = (α + 1) • α + 1, . . . , (τ (k), τ (k)) = (α, α ) ↔ σ(k) = (α + 1) • (α + 1). Then, defining x k =      X k X k-1 . . . X k-α      , u k =      U k U k-1 . . . U k-α      , y k = Y k (2)
The system (1) can be equivalently rewritten as a switching affine system like

x k+1 = A σ(k) x k + B σ(k) u k + E σ(k) y k = C σ(k) x k + D σ(k) u k (3)
where x k ∈ R n is the state vector with n = (α + 1)N , y k ∈ R m is the output with m = M , and u k ∈ R p is the input with p = (α + 1)P . The function σ defined above corresponds for (3) to the switching law σ : N → J = {1, . . . , J} with J = (α +1)(α +1) that assigns, to any discrete-time k ∈ N, the integer σ(k) ∈ J . The matrices

A σ(k) ∈ R n×n , B σ(k) ∈ R n×p , C σ(k) ∈ R m×n , D σ(k) ∈ R m×p and E σ(k) ∈ R n×1
are the state space matrices of the system which belong to the respective sets {A 1 , . . . , A J }, {B 1 , . . . , B J }, {C 1 , . . . , C J }, {D 1 , . . . , D J } and {E 1 , . . . , E J }. The state space matrices obey the following construction

A σ(k) =      A + κ(τ (k))G ψ1(τ (k)) • • • ψα(τ (k)) 1 0 • • • 0 0 1 • • • 0 . . . • • • . . . 0 0 • • • 1 0      B σ(k) = ψ 0 (τ (k)) ψ 1 (τ (k)) • • • ψ α (τ (k)) 0 0 • • • 0 E σ(k) = E 0 , C σ(k) = C 0 , D σ(k) = D 0 ψ i is defined for i = 1, . . . , α as ψ i (τ (k)) = G if τ (k) = i 0 if τ (k) = i , κ(τ (k)) = 1 if τ (k) = 0 0 if τ (k) = 0
Finally, ψ i is defined for i = 0, . . . , α as

ψ i (τ (k)) = B if τ (k) = i 0 if τ (k) = i
This being the case, estimating τ (k) and τ (k) of (1) amounts to estimate the mode σ(k) of (3), being known a sequence of input/output data u k and y k over a finite length receding horizon. As a result, we can write without any confusion a sequence of modes σ s = σ(k)σ(k + 1) . . . σ(k + h) and a sequence of pairs of delays

σ s = (τ (k), τ (k))(τ (k + 1), τ (k + 1)) . . . (τ (k + h), τ (k + h)). Hereafter, σ [k1,k2]
will stand for the finite sequence of modes (also called path)

{σ(k 1 ), • • • , σ(k 2 )} in the interval of time [k 1 , k 2 ].
We denote with S the set of integers s ∈ S that uniquely identify a sequence σ s ∈ J h+1 in the interval of time [k -h, k] and with S the number of admissible sequences in J h+1 . By admissible sequence, it is meant a sequence for which σ(k + 1) is compatible with σ(k) and the transition rule defined by the switching function σ. The active sequence will be denoted with σ * . Hence, we can resort to the mode detection proposed in [START_REF] Domlan | Switching Systems Mode Estimation using a Model-based Diagnosis Method[END_REF] and recalled in the following proposition. Proposition 1: [START_REF] Domlan | Switching Systems Mode Estimation using a Model-based Diagnosis Method[END_REF] Let h be a horizon length. The active sequence σ * in the interval of time [k -h, k] is a sequence σ s ∈ J h+1 such that the corresponding residual fulfills

r h,σs = 0 (4) with r h,σs = Ω σs (y k-h,k -T σs u k-h,k -T σs )
where Ω σs is the solution of Ω σs O σs = 0, with

y k-h,k = O σ [k-h,k] x k-h + T σ [k-h,k] u k-h,k + T σ [k-h,k] (5)
where

O σ [k-h,k] =         C σ(k-h) C σ(k-h+1) A σ(k-h) . . . C σ(k-1) A σ(k-h) σ(k-2) C σ(k) A σ(k-h) σ(k-1)         (6)
T

σ [k-h,k] =         D σ(k-h) 0 0 C σ(k-h+1) B σ(k-h) D σ(k-h+1) 0 . . . . . . . . . C σ(k-1) B σ(k-h) σ(k-2) D σ(k-1) 0 C σ(k) B σ(k-h) σ(k-1) D σ(k)         T σ [k-h,k] =         0 C σ(k-h+1) E σ(k-h) . . . C σ(k-1) E σ(k-h) σ(k-2) C σ(k) E σ(k-h) σ(k-1)         A k2 k1 = A k1 A k1+1 • • • A k2 B k2 k1 = A k2-1 k1 B k2 • • • A k1+1 k1 B k1+2 A k1 B k1+1 B k1 E k2 k1 = A k2-1 k1 E k2 + • • • + A k1+1 k1 E k1+2 + A k1 E k1+1 + E k1 y k1,k2 = y T k1 y T k1+1 • • • y T k2 T u k1,k2 = u T k1 u T k1+1 • • • u T k2 T O σ [k-h,k] is the observability matrix in the finite observation window [k -h, k].
Actually, the horizon length h is defined in [START_REF] Domlan | Switching Systems Mode Estimation using a Model-based Diagnosis Method[END_REF] as the integer which satisfies rank(O σ [k-h,k] ) = n. That supposes the system to be pathwise observable and is restrictive. It has been shown in [START_REF] Halimi | A hybrid approach for the estimation of time-varying delays of discrete-time systems[END_REF] that such a condition can be relaxed and h must obey

rank(O σ [k-h,k] ) = rank(O σ [k-h,k-1] ) (7)
An important issue to be addressed for mode detection purpose is the ability for a detector to deliver a unique solution, that is a unique mode sequence σ s . Let us stress that the detector defined as in Proposition 1 does not exclusively deliver the active mode σ(k) at time k but deliver the whole active sequence σ * in the interval of time [k -h, k]. Addressing the question of uniqueness amounts to checking whether the mode detector is able to discriminate the active sequence σ * from any other sequences σ s ∈ J h+1 . Such a notion is related to the so-called discernability.

First, we recall and provide new results on the question of uniqueness in the general case. Then, we particularize the investigation in the special context of time-varying delays estimation.

II. UNIQUENESS

A. Discernability

Discernability has been thoroughly discussed in [START_REF] Babaali | Asymptotic Observers for Discrete-Time Switched Linear Systems[END_REF] and [START_REF] Domlan | Switching Systems Mode Estimation using a Model-based Diagnosis Method[END_REF]. Let us point out that some authors use the terminology "mode observability" instead of "discernability". Formally, discernability of mode sequences obeys the following definition which is restated here to be in accordance with the notation of the present paper and with the detector defined as in Proposition 1.

Definition 1: For the detector defined as in Proposition 1 based on the residual r h,σs , two modes sequences σ s1 and σ s2 delivered by (3), with (s 1 , s 2 ) ∈ S 2 , are discernible on an observation window of length h + 1, if the corresponding residuals r h,σs 1 et r h,σs 2 are not simultaneously zero when one of the sequence σ s1 or σ s2 is the active sequence σ * .

A necessary and sufficient condition for discernability of two sequences is proved in [START_REF] Domlan | Switching Systems Mode Estimation using a Model-based Diagnosis Method[END_REF] and is recalled below.

Theorem 1: [START_REF] Domlan | Switching Systems Mode Estimation using a Model-based Diagnosis Method[END_REF] For a given input sequence u k-h,k , two mode sequences σ s1 and σ s2 delivered by (3), with (s 1 , s 2 ) ∈ S 2 , are discernible on an observation window of length h + 1, for almost all initial conditions x k-h , iff at least one of the two following conditions is satisfied for all i, j ∈ {s 1 , s 2 } , i = j

Ω σi O σj = 0 (8) Ω σi ((T σj -T σi )u k-h,k + (T σj -T σi )) = 0 (9)
Finally, we can introduce the notion of discernability for (3).

Definition 2: For a given input sequence u k-h,k , system (3) is discernible if, for every pairs of sequences σ s1 , σ s2 ∈ J h+1 with (s 1 , s 2 ) ∈ S 2 , σ s1 is discernible from σ s2 . According to Definition 1, if discernability is not satisfied, this means that several residuals can vanish simultaneously. That causes the estimation of the sequence σ s provided in Proposition 1 to be unsuccessful. In other words, the active sequence of length h + 1 cannot be discriminated from all the other ones and then, cannot be directly estimated. This being the case, an alternative to circumvent the problem has been proposed in the literature through the concept of (η, ω)discernability [START_REF] Alessandri | Receding-Horizon Estimation for Switching Discrete-Time Linear Systems[END_REF]. It is the purpose of next subsection.

B. (η, ω)-Discernability

The property of (η, ω)-discernability has been introduced in [START_REF] Alessandri | Receding-Horizon Estimation for Switching Discrete-Time Linear Systems[END_REF]. It reflects the ability to discriminate, and then to estimate, the active subsequence σ * [k-h+η,k-ω] from all the other ones. The quantities η and ω are positive integers verifying η ∈ {0, . . . , h}, ω ∈ {0, . . . , h} and η + ω ≤ h. Clearly, (η, ω)-discernability coincides with discernability if η = 0 and ω = 0. In the sequel, we shall consider either η > 0 or ω > 0. The integers η and ω shall be chosen as small as possible to get a estimated sequence of maximal length. Letting σ s[k-h+η,k-ω] with s ∈ S as the sequence of modes σ(k -h + η), . . . , σ(k -ω), (η, ω)-discernability obeys the following definition.

Definition 3: [1] σ s1 is (η, ω)-discernible from σ s2 with σ s1 , σ s2 ∈ J h+1 , (s 1 , s 2 ) ∈ S 2 , if σ s1 [k-h+η,k-ω] = σ s2 [k-h+η,k-ω] and σ s1 is discernible from σ s2 .
Based on Theorem 1 of discernability, we can derive conditions for checking (η, ω)-discernability as given in the following proposition.

Proposition 2: For a given input sequence u k-h,k , two modes sequences σ s1 and σ s2 of (3) with (s 1 , s 2 ) ∈ S 2 are (η, ω)-discernible on an observation window of length h + 1, for almost all initial conditions x k-h , iff at least one of the two following conditions is satisfied for all i, j ∈ {s 1 , s 2 } with i = j

Ω σi O σj = 0 (10)
Ω σi ((T σj -T σi )u k-h,k + (T σj -T σi )) = 0 (11) with σ s1 [k-h+η,k-ω] = σ s2 [k-h+η,k-ω] Proof 1:
The proof is a straightforward consequence of the consideration of both Definition 3 of (η, ω)discernability and ( 8)-( 9) of Theorem 1.

Definition 4: [START_REF] Alessandri | Receding-Horizon Estimation for Switching Discrete-Time Linear Systems[END_REF] For a given input sequence u k-h,k , ( 3) is (η, ω)-discernible, if, for every pairs of sequences σ s1 , σ s2 ∈ J h+1 with (s

1 , s 2 ) ∈ S 2 such that σ s1 [k-h+η,k-ω] = σ s2 [k-h+η,k-ω] , σ s1 is discernible from σ s2 .
The estimation of the active subsequence σ * [k-h+η,k-ω] can be performed according to the following proposition.

Proposition 3: Assume that ( 3) is (η, ω)-discernable. Let S ⊂ S be the set of integers s ∈ S such that all the sequences σ s[k-h+η,k-ω] differ one another. The active subsequence σ

* [k-h+η,k-ω] in the interval of time [k -h, k] is the unique subsequence σ s[k-h+η,k-ω]
of the sequences σ s with s ∈ S such that the corresponding residual fulfills

r h,σs = 0 (12) with r h,σs = Ω σs (y k-h,k -T σs u k-h,k -T σs )
where Ω σs is the solution of Ω σs O σs = 0. Proof 2: The proof follows along the same lines of reasoning as in the proof of Proposition 1 except that s ∈ S is replaced by s ∈ S, that is, only the residuals for which the subsequences σ s[k-h+η,k-ω] which differ from all the other ones are considered.

If discernability is satisfied, the first active sequence σ * [0,h] can be obtained. On the other hand, if (η, ω)-discernability is satisfied, at time k = h, the active subsequence σ * [η,h-ω] can be estimated but by a sliding window approach, the initial active sequence can be complemented to obtain a sequence of any prescribed length. On the other hand, the sequence σ * [0,η-1] cannot be estimated. All in all, Proposition 3 allows to achieve the estimation of all the modes σ(k) for k ≥ 0 or k ≥ η accordingly. However, the complexity of the estimation of the mode σ(k) at time k, in terms of required amount of data and number of residuals to be calculated and analyzed, can be reduced. Indeed, the estimation of the mode σ(k) at time k can be performed taking into account that all the modes at times k < k have already been estimated and so are assumed to be known. Such a consideration motivated the introduction of the concept of (λ)-Backward Discernability.

C. (λ)-Backward Discernability and permanent estimation

The property of (λ)-Backward Discernability allows to deliver at time k, the mode σ(k -λ), being the modes σ(k -i) (1 + λ ≤ i ≤ h) already estimated. The quantity λ is an integer such that λ ∈ {1, . . . , h}. (λ)-Backward Discernability stands as an extension of the so-called Backward Discernability introduced in [START_REF] Babaali | Asymptotic Observers for Discrete-Time Switched Linear Systems[END_REF]. Indeed, Backward Discernability corresponds to the case when λ = 0. More formally, (λ)-Backward Discernability obeys the following definition.

Definition 5: A mode i is (λ)-Backward Discernible from another mode j, if there exists an integer λ such that, in an observation window [k -h, k], for every sequence σ h-λ of length h -λ, and for any two sequences σ 1 and σ 2 of length λ, σ h-λ iσ 1 is discernible from σ h-λ jσ 2 .

It is clear that discernability implies (λ)-Backward Discernability. Conditions for guaranteeing (λ)-Backward Discernability are provided in the following proposition.

Proposition 4: For a given input sequence u k-h,k , two modes i and j are (λ)-Backward discernible on an observation window [k -h, k] of length h + 1, for almost all initial conditions x k-h iff, for every sequence σ h-λ of length h-λ and for any two sequences σ 1 and σ 2 of length λ delivered by ( 3), at least one of the following conditions are satisfied for all i, j ∈ J , i = j

Ω σ h-λ iσ 1 O σ h-λ jσ 2 = 0 (13) Ω σ h-λ iσ 1 ((T σ h-λ jσ 2 -T σ h-λ iσ 1 )u k-h,k + (T σ h-λ jσ 2 -T σ h-λ iσ 1 )) = 0 (14) Proof 3:
The proof is a straightforward consequence of the consideration of both Definition 5 of (λ)-Backward Discernability and ( 8)-( 9) of Theorem 1.

Definition 6: For a given input sequence u k-h,k , system (3) is (λ)-Backward Discernible if, for every pairs of modes (i, j) ∈ J 2 , the mode i is (λ)-Backward Discernible from the mode j.

When (λ)-Backward Discernability is satisfied, the estimation of the mode σ(k -λ) at time k can be performed according to the following proposition.

Proposition 5: Assume that ( 3) is (λ)-Backward Discernable. Let σ h-λ be a sequence of length h-λ. Let Sσ h-λ ⊂ S be the set of integers s ∈ S such that σ h-λ iσ differ one another for all for all i ∈ J and for any sequences σ of length λ. The active mode σ * (k -λ) in the interval of time [k -h, k] is the unique mode σ(k -λ) of the sequence σ s with s ∈ Sσ h-λ such that the corresponding residual fulfills

r h,σs = 0 (15)
with

r h,σs = Ω σs (y k-h,k -T σs u k-h,k -T σs ),
where Ω σs is the solution of Ω σs O σs = 0. Proof 4: The proof follows along the same lines of reasoning as in the proof of Proposition 1 except that s ∈ S is replaced by s ∈ Sσ h-λ , that is, for a given subsequence σ h-λ of length h -λ, only the residuals for which the mode σ(k -λ) differs one another are considered, the rest of the sequence of length λ + 1 being disregarded. The relevance of Proposition 5 lies in that only the residuals of the sequences σ h-λ iσ (σ ∈ J λ ) with σ h-λ ∈ J h-λ resulting from the estimation at time k-1 have to be checked by the detectors. That allows to reduce the number of tests: J λ+1 sequences instead of J h+1 sequences. Let us recall that λ ≤ h.

When (λ)-Backward Discernability is considered, a sequence of length respectively equal to h -λ must be known. It has been previously stressed that (η, ω)-discernability allows to estimate with Proposition 5 the active subsequence σ *

[η,h-ω] and can be complemented by shifting in time the procedure until a sequence of length h -λ is known. Then, we can proceed to the permanent estimation based on a receding horizon technique for k > h + ω + η -1.

III. SPECIFICITY FOR TIME-DELAYED SYSTEMS

As previously stressed, because of the restriction due to the specific structure of the state space matrices of (3), it can be suspected that some of the properties of discernability are no longer satisfied. This is precisely shown in what follows. All the proofs are based on the search for particular sequences for which the properties are not satisfied.

1) Preliminary result:

The following lemma is recalled from [START_REF] Babaali | Asymptotic Observers for Discrete-Time Switched Linear Systems[END_REF].

Lemma 1: Given a vector Y and a matrix O, being X unknown, it holds that

Y ∈ R(O) ⇔ ∃X | Y = OX ⇔ (OO † -1)Y = 0 (16) Proposition 6: Condition Ω σs 2 O σs 1 = 0 is equivalent to rank( O σs 1 O σs 2 ) > rank(O σs 2 ) (17)
where 2) Discernability: Proposition 7: For system (1), discernability and (0)-Backward Discernability (that is Backward Discernability) are not fulfilled.

O
Proof 6: Consider the two particular sequences σ s1 = σ s [k-h,k-1] i (i ∈ J ) and σ s2 = σ s [k-h,k-1] j (j ∈ J ). For (3), the matrix C σ(k) does not depend on σ(k). Therefore, the matrices O, T , and T defined as in [START_REF] Baglietto | Active mode observation of switching linear systems based on set-valued estimation on the continuous state[END_REF] only depend on σ s [k-h,k-1] . Consequently, T σs 1 = T σs 2 and T σs 1 = T σs 2 , which implies that ( 9) is not fulfilled. Besides, since (0)-Backward Discernability is a special case of discernability, since Backward Discernability is not fulfilled, discernability is not fulfilled either. That completes the proof. Since neither discernability nor (0)-Backward Discernability are satisfied, the whole sequence σ s[k-h,k] cannot be estimated. Let us focus on the less restrictive property, namely the (η, ω)-discernability. We recall that such a property reflects the ability of discriminating, and so estimating, the subsequences σ * [k-h+η,k-ω] . 3) (η, ω)-Discernability: Proposition 8: System (1) is not (η = 0, ω = 1)discernible.

Proof 7: (0, 1)-discernability is not satisfied if and only if neither [START_REF] Halimi | A hybrid approach for the estimation of time-varying delays of discrete-time systems[END_REF] nor [START_REF] Hetel | Equivalence Between the Lyapunov-Krasovskii Functional Approach for Discrete Delay Systems and the Stability Conditions for Switched Systems[END_REF] in Proposition 2 is satisfied. Let us consider the two particular sequences σ s1 = (0, 0)(0, 0) • • • (0, 0) and

σ s2 = (1, 0)(0, 0) • • • (0, 0) of length h + 1. Let us note that the condition σ s1 [k-h,k-1] = σ s2 [k-h,k-1] ,
O σs 1 =      C CA (0,0)
. . . [START_REF] Alessandri | Receding-Horizon Estimation for Switching Discrete-Time Linear Systems[END_REF]0) . . .

CA (0,0) h      =        C 0 • • • 0 C(A + G) 0 • • • 0 C(A + G) 2 0 • • • 0 . . . . . . . . . C(A + G) h 0 • • • 0        O σs 2 =      C CA
CA (0,0) h-1 A (1,0)      O σs 2 =        C 0 0 • • • 0 CA CG 0 • • • 0 C(A + G)A C(A + G)G 0 • • • 0 . . . . . . . . . . . . C(A + G) h-1 A C(A + G) h-1 G 0 • • • 0       
Denote with V 1 the first column of O σs 1 , and V 2 , V 2 the first and the second column of O σs 2 respectively. It is clear that

V 1 = V 2 + V 2 . As a result, rank([O σs 1 O σs 2 ]) = rank(O σs 2 ) (19)
According to Proposition 6, it is equivalent to

Ω σs 2 O σs 1 = 0 (20)
On the other hand, since D σ(k) , B σ(k) and E σ(k) do not depend on τ (k), it holds that D (0,0) = D (1,0) , B (0,0) = B (1,0) and E (0,0) = E (1,0) . As a result, from the definitions of T and T given in ( 5), we have that T σs 1 = T σs 2 and T σs 1 = T σs 2 which implies that

Ω σs 2 ((T σs 1 -T σs 2 )u k-h,k + (T σs 1 -T σs 2 )) = 0 (21)
As a result, from (20) and ( 21), it holds that Proposition 2 is not satisfied and the sequences σ s1 is not (0,1)-discernible from σ s2 . That completes the proof.

4) (λ)-Backward Discernability: Proposition 9: If U k remains unchanged between two consecutive discrete times k and k + 1, system (1) is not (λ = 1)-Backward Discernible.

Proof 8: Let us consider the sequences σ s3 = σ h-λ i(0, 0) and σ s4 = σ h-λ j(0, 0) of length h + 1 with σ h-λ = (0, 0)(0, 0) • • • (0, 0), i = (0, 0) and j = (0, 1). It suffices to show that conditions (13) and ( 14) of Proposition 4 are not satisfied for σ s3 and σ s4 . For both sequences σ s3 and σ s4 , it holds that τ (k) = 0 for all k. Since the observability matrix O σ [k-h,k] exclusively depends on τ (k), O σs 3 = O σs 4 and then ker(O σs 3 ) = ker(O σs 4 ) which implies that

Ω σs 4 O σs 3 = 0 (22)
On the other hand, it holds that A (0,0) = A (0,1) , D (0,0) = D (0,1) and E (0,0) = E (0,1) since A σ(k) , D σ(k) and E σ(k) do not depend on τ (k). From the definitions of T and T given in (5), we have that T σs 3 = T σs 4 . Thus, [START_REF] Domlan | Switching Systems Mode Estimation using a Model-based Diagnosis Method[END_REF] becomes

Ω σs 4 ((T σs 3 -T σs 4 )u k-h,k ) = 0 (23)
with The delays fulfill τ (k) ∈ {0, 1, 2} (α = 2), τ (k) = 0 for all k (α = 0). This linear delayed discrete-time system is rewritten into the form (3) with

T σs 3 -T σs 4 =      0 0 0 . . . . . . . . . 0 0 0 0 C(B (0,0) -B (0,1) ) 0      =      0 0 0 0 . . . . . . . . . . . . 0 0 0 0 0 CB -CB 0      Substituting T σs 3 -T σs 4 into (23) yields Ω σs 4 0 CBU k-1 -CBU k-2 T = 0 (24) Hence, if U k-1 = U k-2 , from (
x k =   X k X k-1 X k-2   , u k = U k , y k = Y k
and the switching rule σ is defined as σ : k ∈ N → σ(k) ∈ J with J = (α + 1)(α + 1) = 3 as the number of modes. The corresponding state space matrices read where σ(k) = 1 is associated to (τ, τ ) = (0, 0), σ(k) = 2 is associated to (τ, τ ) = (1, 0), and σ(k) = 3 is associated to (τ, τ ) = (2, 0). The smallest detection horizon h which satisfies ( 7) is h = 3.

• Initial estimation The property of (η, ω)-discernability is checked using [START_REF] Halimi | A hybrid approach for the estimation of time-varying delays of discrete-time systems[END_REF] since [START_REF] Hetel | Equivalence Between the Lyapunov-Krasovskii Functional Approach for Discrete Delay Systems and the Stability Conditions for Switched Systems[END_REF] is never verified because B 1 = B 2 and E 1 = E 2 . After having performed the test, it holds that (10) is satisfied for η = 2 and ω = 1 which means that (2, 1)-discernability is fulfilled.

• Permanent estimation Since ( 14) is never verified because B 1 = B 2 , E 1 = E 2 and C 1 = C 2 , conditions (13) are checked to test (λ)-Backward Discernability. It holds that ( 13) is fulfilled for λ = 1. Therefore, the permanent estimation can be performed by the detector which delivers the active mode σ * (k -1) for k > h+ω +η -λ-1 = 4. The detector successfully recovers the unknown delay as depicted on Figure 1 (bottom).

  are constant matrices. The quantities τ (k) and τ (k) are time-varying delays acting respectively on the state vector and on the input. They take values in two respective finite sets T = {0, 1, • • • , α} and T = {0, 1, • • • , α }. The time variation of τ (k) and τ (k) is arbitrary. The case when τ (k) and τ (k) are not directly accessible is considered. Hence, the aim is to estimate τ (k) and τ (k) while the model, the sequences U k and Y k are assumed to be known and available on-line.

  22) and (24), we infer that neither (13) nor (14) of Proposition 4 is satisfied and the sequence σ s3 is not (1)-Backward Discernible from σ s4 . That completes the proof.IV. EXAMPLE Let us consider (1) with the particular setting

  i = C 0 0 , D i = 0 ∀ i ∈ {1, 2, 3}

Fig. 1 .

 1 Fig. 1. Top: active sequences τ * . Middle: reconstructed sequences τ . Bottom: error τ -τ *

  σs 1 O σs 2 denotes the horizontal concatenation of O σs 1 and O σs 2 . Proof 5: If (17) is not satisfied, it is equivalent to rank( O σs 1 O σs 2 ) = rank(O σs 2 ) since it is clear that rank( O σs 1 O σs 2 ) < rank(O σs 2 ) can never occur. This means that O σs 1 ∈ R(O σs 2 ). From (16) of Lemma 1, we get that O σs 1 ∈ R(O σs 2 ) ⇔ (O σs 2 O † σs 2 -1)O σs 1 = 0 (18) And yet, according to Proposition 3.3 in [6], R(O σs 2 O † σs 2 -1) = ker(O σs 2 ). Therefore, since by definition ker(O σs 2 ) = Ω σs 2 , (18) implies that Ω σs 2 O σs 1 = 0. That completes the proof.

  as required in Proposition 2, is well satisfied. The respective observability matrices denoted O σs 1 and O σs 2 read

Acknowledgement

This work was partially supported by Research Grants ANR-13-INSE-0005-01 from the Agence Nationale de la Recherche.


Vivien Maisonneuve
email: vivien.maisonneuve@cri.mines-paristech.fr

Olivier Hermant
email: olivier.hermant@cri.mines-paristech.fr

François Irigoin
email: francois.irigoin@cri.mines-paristech.fr

ALICe: A Framework to Improve Affine Loop Invariant Computation *

A crucial point in program analysis is the computation of loop invariants. Accurate invariants are required to prove properties on a program but they are difficult to compute. Extensive research has been carried out but, to the best of our knowledge, no benchmark has ever been developed to compare algorithms and tools.

We present ALICe, a toolset to compare automatic computation techniques of affine loop scalar invariants. It comes with a benchmark that we built using 102 test cases which we found in the loop invariant bibliography, and interfaces with three analysis programs, that rely on different techniques: Aspic, ISL and PIPS. Conversion tools are provided to handle format heterogeneity of these programs.

Experimental results show the importance of model coding and the poor performances of PIPS on concurrent loops. To tackle these issues, we use two model restructurations techniques whose correctness is proved in Coq, and discuss the improvements realized.

* We thank Laure Gonnord and Sven Verdoolaege who helped us to use their tools Aspic and ISL.

Introduction

The standard state-based model checking problem is to characterize the set of all reachable states of a transition system modeling some program. This information is generally used to check safety properties on the system, ensuring that bad configurations cannot be reached. The accuracy of computed invariants is very important, as it plays an essential role in the success of the program analysis.

Dealing with potentially infinite-state models requires to overapproximate invariants into a mathematical model (or abstract domain) whose representation is finite and that allows to make the required computations. Many such domains exist in the literature, but we focus on the domain of affine invariants, first introduced by N. Halbwachs [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF][START_REF] Halbwachs | Détermination automatique de relations linéaires vérifiées par les variables d'un programme[END_REF], which offers a good trade-off between invariant accuracy and computational complexity.

Most of the usual analysis techniques consist in starting from a set of supposed predicates about a particular control position in the transition system, and then propagating it to other positions by evaluating the effect of each transition on the predicates. This is pretty straightforward, except in the case of loops that needs special treatment. This lead to intensive research, with many approaches based either on abstract interpretation [START_REF] Jeannet | Partitionnement dynamique dans l'Analyse de Relation Linéaire et application à la vérification de programmes synchrones[END_REF][START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF][START_REF] Merchat | Réduction du nombre de variables en analyse de relations linéaires[END_REF], that is, using widening operations, or on direct computation [START_REF] Ancourt | A modular static analysis approach to affine loop invariants detection[END_REF]. The case of concurrent loops, i.e. when there are different possible loops on the same control point, is particularly challenging.

As of today, several tools for linear relation analysis use a vast pattern of algorithms and heuristics to handle loops, aiming to maximum accuracy. We propose a toolset that compares these tools on a common set of small-scale, previously published test cases and to test the sensibility of these tools to different encoding schemes. In Section 2, we introduce our toolset, ALICe, and present the set of test cases and of analysis programs that we use. The different encodings are discussed in Section 3, after which the results of our experiments are shown.

The ALICe Benchmark

The ALICe benchmark project aims to provide tools and a standardized set of test cases to compare as fairly as possible different polyhedral analysis techniques and softwares. ALICe is a free software distributed under GPLv3, and is available at http://alice.cri.mines-paristech. fr/.

There are several motivations behind the ALICe project. First, we want to use it as a tool to compare polyhedral invariant computation tools on a common ground, using a set of published test cases issued from various sources, instead of evaluating their performances on ad hoc examples only, in the spirit of the TPTP library [START_REF] Sutcliffe | The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0[END_REF] and the CASC competition [START_REF] Sutcliffe | The state of CASC[END_REF][START_REF] Pelletier | The development of CASC[END_REF]. ALICe also gives the opportunity to evaluate the benefits of model-to-model restructurations prior to analysis (Section 3).

Program Model

Test cases in ALICe are particular interpreted automata called models, and traditionally represented as graphs. In a nutshell, a model in ALICe is a transition system constituted by a set of control points (nodes), connected by guarded commands acting on integer variables (edges), and comes with initial and error states. An example of model in shown in Figure 1.

k 1 k 2 t 1 : x ≥ 0 ? t 2 : x ≤ 0 ? x++ t 3 : x ≥ 1 ? x-- Error condition: x < 0 in k 2 Figure 1: An example of model
Definitions Let X be a finite set of integer variables (boolean variables, if any, are cast to integers) and K be a finite set, whose elements are called control points. In our example,

X = {x} and K = {k 1 , k 2 }.
• A valuation on X is a function v : X → Z mapping each variable to an integer value. Let

V = Z X be the set of valuations on X. • A (global) state of the model is a pair q = (k, v) ∈ K × V , for instance: (k 2 , 0). The set of global states is noted Q. • A guard is a function g : V → B = { , ⊺},
giving the value of a logic formula on a valuation v. In the example model, the guard in t 2 is:

g 2 : v ↦ v(x) ≤ 0, simply noted x ≤ 0 .
In practice, the guard is assimilated to its truth set {v g(v) = ⊺}. The set of guards is noted G.

• An action a is a binary relation on valuations: a ⊆ V × V and represent possible valuation changes; it is not necessarily a function. In t 2 , the corresponding action is:

a 2 = {(v, v ′ ) ∈ V × V v ′ (x) = v(x) + 1}, simply noted x++ with X = {x}.
The set of actions is noted A.

• A transition t is a quadruplet t = (k, g, a, k ′ ) ∈ K × G × A × K.
Intuitively, when the automaton is at control point k, and if the current valuation v satisfies the guard g (i.e.

g(v) = ⊺), the transition execution moves to the control point k ′ , with a valuation v ′ such that (v, v ′ ) ∈ a. The transition t = (k, g, a, k ′ ) is usually noted:

t : k g ? a → k ′
Transitions are not necessarily deterministic.

In the example model, t 2 is a transition from control point k 2 to control point k 2 with guard g 2 and action a 2 , that is

t 2 : k 2 x≤0 ? x++ → k 2 .
The set of transitions is noted T .

Formalism Using these definitions, a model can now be formally defined as a tuple m = (X, K, T, Q init , Q err ) where

• X is a finite set of variables;

• K is a finite set of control points;

• T is a finite set of transitions on X and K;

• Q init and Q err are subsets of Q, called respectively initial states and error states of m.

In the example model of Figure 1, there is an initial control point k 1 with no valuation constraint so Q init = {k 1 } × V . The error region is at control point k 2 with x < 0, that is:

Q err = {k 2 } × (x < 0).
The set of models is noted M.

Semantics

The semantics of a model is defined in terms of transition systems. The model m = (X, K, T, Q init , Q err ) is associated to the transition system (Q, →, Q init ), which transition relation obeys to:

(k, v) → (k ′ , v ′ ) ⇐⇒ ∃(k, g, a, k ′ ) ∈ T, g(v) = ⊺ ∧ (v, v ′ ) ∈ a. (1)
Accessibility and Verification A safety property expresses that something bad never happens . We consider accessibility properties, a subset of safety properties, expressing that the set of error states Q err -representing something bad -cannot be reached. Their verification involves the computation of accessible states from the initial states Q init .

Let R be a subset of states Q. We note

Post(R) = {q ′ ∈ Q ∃q ∈ R, q → q ′ }
the set of successor states of all states in R, and

Acc(R) = ⋃ n≥0 Post n (R)
the set of all accessible states from some state in R (Acc is the transitive closure of Post). The model m is correct if and only if:

Acc(Q init ) ∩ Q err = ∅. (2)
The test cases available in ALICe are all correct models.

Challenging a Tool

In general, it is not possible to compute exactly the set of accessible states Acc(Q init ). Instead, analysis tools tested by ALICe compute supersets

Q ′ of Acc(Q init ):
if a given Q ′ does not intersect with Q err , then the tool that generated this Q ′ has verified that states in Q err are unreachable (Figure 2), thus the test case is considered a success for that tool. However, if the intersection Q ′ ∩ Q err is not empty, the tool user cannot conclude whether the property is violated or if the overapproximation is too inaccurate: this corresponds to a failure for the tool.

Acc(Q init ) Q ′ Q err Figure 2: Model checking
Note that we could use backward analysis instead: starting from error states Q err , computing iteratively the set of coaccessible states and testing the intersection with Q init . But as all analysis tools used within ALICe rely on forward analysis (see Section 2.3), this is not explored further.

Test Cases

The benchmark itself consists in 102 previously published test cases, including work from L. Gonnord [START_REF] Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF][START_REF] Alias | Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs[END_REF], S. Gulwani [START_REF] Chawdhary | Ranking abstractions[END_REF][START_REF] Gulwani | SPEED: symbolic complexity bound analysis[END_REF][START_REF] Gulwani | Control-flow refinement and progress invariants for bound analysis[END_REF][START_REF] Gulwani | SPEED: precise and efficient static estimation of program computational complexity[END_REF][START_REF] Gulwani | The reachability-bound problem[END_REF], N. Halbwachs [START_REF] Halbwachs | Delay analysis in synchronous programs[END_REF][START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF][START_REF] Halbwachs | Linear relation analysis principles and recent progress[END_REF][START_REF] Halbwachs | Détermination automatique de relations linéaires vérifiées par les variables d'un programme[END_REF], B. Jeannet [START_REF] Jeannet | Partitionnement dynamique dans l'Analyse de Relation Linéaire et application à la vérification de programmes synchrones[END_REF] et al. The comprehensive list of model sources can be found in the bibliography [START_REF] Bardin | Vers un Model Checking avec accélération plate des systèmes hétérogènes[END_REF][START_REF] Soon | Program termination analysis in polynomial time[END_REF][START_REF] Beyer | Path invariants[END_REF][START_REF] Bultan | Symbolic model checking of infinite state systems using presburger arithmetic[END_REF][START_REF] Chawdhary | Ranking abstractions[END_REF][START_REF] Colón | Synthesis of linear ranking functions[END_REF][START_REF] Colón | Practical methods for proving program termination[END_REF][START_REF] Cook | Termination proofs for systems code[END_REF][START_REF] Cousot | Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming[END_REF][START_REF] Gopan | Lookahead widening[END_REF][START_REF] Gopan | Guided static analysis[END_REF][START_REF] Bhargav | SYNERGY: a new algorithm for property checking[END_REF][START_REF] Henry | Static analysis by abstract interpretation, path focusing[END_REF][START_REF] Henzinger | Lazy abstraction[END_REF][START_REF] Katz | Implementing a cache consistency protocol[END_REF][START_REF] Merchat | Réduction du nombre de variables en analyse de relations linéaires[END_REF][START_REF] Podelski | A complete method for the synthesis of linear ranking functions[END_REF][START_REF] Popeea | Inferring disjunctive postconditions[END_REF], as well as on the ALICe website. They come mostly from works on loop invariant computation, loop bound analysis and, to a lesser extent, protocol verification. Test cases are usually relatively small: typically 1 to 10 states and 2 to 15 transitions. Histograms showing distribution of test cases according to their sizes are shown in Figure 3.

These test cases come in many forms and had to be hand-encoded to a common format, described in Section 2.4.

Three Supported Tools

For now, ALICe is interfaced with three invariant computation tools: Aspic, ISL and PIPS.

• Aspic [START_REF] Gonnord | [END_REF], a polyhedral invariant generator developed by L. Gonnord. Aspic relies on classic linear relation analysis, improved with abstract accelerations, identifying classes of loops in the abstract polyhedral domain whose effect can be computed directly instead of using widening operations, thus granting better accuracy. • ISL: the Integer Set Library [START_REF] Verdoolaege | isl -integer set library[END_REF], developed by S. Verdoolaege. ISL is a library for manipulating sets S and relations R on integer tuples bounded by affine constraints in the following form:

S(s) = x ∈ Z d ∃z ∈ Z e : Ax + Bs + Dz ≥ c , R(s) = (x 1 , x 2 ) ∈ Z d1 × Z d2 ∃z ∈ Z e : A 1 x 1 + A 2 x 2 + Bs + Dz ≥ c .
These definitions allow greater expressiveness than polyhedral constraints: in terms of logical expressiveness, they are equivalent to Presburger arithmetic constraints.

• PIPS [7], an interprocedural source-to-source compiler framework for C and Fortran programs, initiated at MINES ParisTech, that relies on a polyhedral abstraction of program behavior. Unlike other tools, PIPS performs a two-step analysis. First, the program is abstracted: each program command instruction is associated to an affine transformer representing its underlying transfer function. This is a bottom-up procedure, starting from elementary instructions, then working on compound statements and up to function definitions. Second, polyhedral invariants are propagated along instructions, using transformers previously computed.

We do not consider the Omega+ [START_REF] Pugh | The omega project[END_REF] library, as it appears to be superseded by ISL [START_REF] Verdoolaege | isl: An integer set library for the polyhedral model[END_REF]. It would be very interesting to be able to use more tools, such as FASTer [START_REF]FAST -fast acceleration of symbolic transition systems[END_REF][START_REF] Bardin | FASTer acceleration of counter automata in practice[END_REF] or NBAC [START_REF] Jeannet | [END_REF][START_REF] Jeannet | Dynamic partitioning in linear relation analysis: Application to the verification of reactive systems[END_REF], but adding support is a time-consuming task, as explained below, and we have not been able to do it up to now.

Heterogeneity of Tools

ALICe test cases are written in the fsm format. This is a simple language that directly represents models, originally used in FAST [START_REF]FAST -fast acceleration of symbolic transition systems[END_REF] and then in Aspic. An example of fsm program for the model in Figure 1 is given in Listing 1.

As we wish to analyze these test cases with different tools and compare results, we have to convert input and output formats. Basically, each tool uses different input and output formats:

• Aspic uses the fsm format both as input and as output;

• ISL uses a custom format to describe both the input model as a relation on states with conditions on variables, and the output invariant, given as a map from states to domains; • PIPS processes a structured C program according to a script written in a custom scripting language, called tpips, while resulting invariants are given as comments surrounding instructions in the output C code.

To check whether an analyzer works successfully on a test cases, we follow these steps:

1. if necessary, convert the model (originally in fsm) into the analyzer's input format;

2. run the analyzer and get the computed model invariant;

3. if necessary, convert the model invariant into ISL format;

4. use ISL to check whether the intersection of the model error region and the invariant computed by the analyzer is empty, i.e. whether the analyzer is able to solve the test case.

Those steps are illustrated in Figure 4. Implementing these steps required to develop several translation programs, from and to Aspic, ISL and PIPS formats. In particular, the tools fsm2c and fsm2isl respectively convert a fsm model into C code or ISL relation. There is also an export tool for fsm in dot format that allows visualization, fsm2dot. They are available within ALICe.

Results for the Raw, Hand-Encoded Test Cases

In this section, we present experimental results obtained with ALICe. Benchmarks were run on a computer with a Quad-Core AMD Opteron Processor 2380 at 2.4 GHz and 16 GB of memory, using the following versions of analyzers (latest versions at the time of writing):

• Aspic version 3.1;

• ISL from Barvinok version 0.36;

• PIPS revision 22 105 (April 2014).

Results obtained by these three tools are displayed in Table 1, along with the corresponding execution times. Aspic stands out as the winner in this comparison, with ISL coming second and PIPS, which is not primarily targeted at invariant analysis, being placed last, both in terms of success rate and of execution time. This ranking is lessened by by the fact that no tool is strictly better than another: for each tool, there is at least one model that is successfully analyzed only by this tool, as shown in Figure 5; and it appears in Table 2 that there is no clear trend as for the quality of generated invariants, in terms of invariant inclusion.

Aspic ISL PIPS

A closer analysis shows that ISL performs comparatively well on test cases encoded with concurrent loops (several loops on a single control point, similar to what is shown Figure 7), unlike PIPS whose results are particularly bad. On the other hand, ISL can be quite slow on test cases that display a large, intricate control structure. Finally, despite its successes, Aspic has greater difficulty to deal with transitions featuring complex formulas, that it is not able to accelerate. This leads us to wonder if the tools are sensitive to the encoding, since a problem can be presented under many guises. This is the topic of the next section, and the other original contribution of this paper. Formally, a sound model restructuration is a function ρ : M → M that maps a model m 1 to a model m 2 such that: if m 2 is correct (i.e., its error region is not reachable), then m 1 is also correct:

∀m 1 , m 2 ∈ M, m 2 = ρ(m 1 ) ∧ correct(m 2 ) ⇒ correct(m 1 ). (3)
Thus, given a model m 1 and a restructuration ρ, it is sufficient to prove the correctness of m 2 = ρ(m 1 ) to deduce that m 1 is also correct. In addition, the restructuration ρ can be equivalent (m 1 is correct if and only if m 2 is correct), although we are not interested in proving such properties in our toolchain. So, for instance, the restructuration that to any model associates the same trivial, inconsistent model is sound (but not very interesting).

For analysis purposes, a model that fails to be checked can be rewritten into another one, hopefully easier to analyze. Within ALICe, we have implemented two restructurations on model states, to test analysis tools on a wider range of models and on specific model schemes, and explore the impact of model encoding. Model restructurations are performed at the very beginning of ALICe execution, just before Step 1., as an additional, preliminary stage to Figure 4. Both these restructurations were proved sound in Coq, using a trace-equivalence scheme: considering an arbitrary, possible state trace with transitions

θ 1 = (k 0 , v 0 ) t1 → (k 1 , v 1 ) t2 → (k 2 , v 2 ) t3 → ⋯
in the original model m 1 , we show that for any corresponding trace θ 2 in the transformed model m 2 (corresponding to the same behavior, once the model has been transformed), then:

(∀q 2 ∈ θ 2 , q 2 / ∈ Q err2 ) ⇒ (∀q 1 ∈ θ 1 , q 1 / ∈ Q err1 ),
thus ensuring (3).

Control-Point Splitting Heuristic

The first restructuration we use is a heuristic to split control nodes that contain several self loops. The global idea is to get rid of such nodes, that are usually the most difficult to automatically analyze, by splitting them with respect to the guards of the transitions, and adjusting the initial and error regions accordingly. This heuristic was initially designed for PIPS and is presented in details in [START_REF] Maisonneuve | Convex invariant refinement by control node splitting: a heuristic approach[END_REF]. In Figure 6, we show the effect of this heuristic applied on the same model as in Figure 1, where the control point k 2 is split into two components with respect to the guards of transitions t 2 and t 3 . The initial state set is unchanged. Proving that the new error state set {k 2 , k ′ 2 } × (x < 0) cannot be reached is easier than in the original model: it is true by construction for the control point k ′ 2 , and can be easily deduced by looking at guards of entering transitions for control point k 2 .

k 1 k 2 (x ≤ 0) k ′ 2 (x ≥ 1) t 1 : x = 0 ? t ′ 1 : x ≥ 1 ? t 2 : x++ t 3 : x = 1 ? x-- t ′ 3 : x ≥ 2 ? x--

Reduction to a Unique Control Point

The other model restructuration reduces the set of controls to a unique control point ℓ, with all transitions turned into loops on ℓ, adding an extra boolean variable x k for each original control point k in both guards and actions (assuming symbols ℓ and {x k } are not bound in the original model), to represent the corresponding control point of the original model. We assure that, in every state of the system, exactly one x k is set to 1. Formally, a transition t between control states k i , k j , with guard g and action a t : k i g ? a → k j is turned into the transition

t ′ : ℓ g∧xi=1∧⋀ k≠i x k =0 ? a∧x ′ j =1∧⋀ k≠j x ′ k =0 → ℓ.
Again, the initial and error set states are adjusted accordingly.

A more direct approach is to encode control information on a unique integer variable instead of several boolean variables, by numbering the control points in the initial model. We did not adopt it because it introduces encoding issues. Indeed, some relations on control points might or might not be expressed in terms of affine constraints, depending on the control-point encoding. For instance, being in k 1 or k ′ 2 in the model of Figure 6 cannot be expressed if the third control point k 2 is encoded with a value between those of k 1 and k ′ 2 . This issue is avoided with our boolean variable scheme.

The resulting model of this restructuration applied on the initial model of Figure 1 is shown in Figure 7. The corresponding initial state set is: This restructuration has three purposes. First, it stresses the tool with more difficult test cases. It also reduces bias factors related to encoding choices. Finally, if used before the control-point splitting heuristic, merging increases the effect of splitting by generating the control-point structure to which it applies.

Q init = {ℓ} × {b 1 = 1 ∧ b 2 = 0}. The error state set is: Q err = {ℓ} × {b 1 = 0 ∧ b 2 = 1 ∧ x < 0}. ℓ t 1 : b 1 = 1, b 2 = 0, x ≥ 0 ? b 1 = 0, b 2 = 1 t 2 : b 1 = 0, b 2 = 1, x ≤ 0 ? x++ t 3 : b 1 = 0, b 2 = 1, x ≥ 1 ? x--

Combining Restructurations

These model restructurations can be used independently or together: first the model is reduced to a unique control point, then this control point is split, widening the scope of the splitting heuristic. Therefore, ALICe works with four version of each model:

• The original version, with no restructuration (noted direct in the tables below);

• With all control points merged into a unique one, as described in Section 3.2 ( merged );

• Using the control-point splitting heuristic presented in Section 3.1 ( split );

• Combining both approaches ( merged-split ).

Impact of Restructurations on Experimental Results

The results obtained using these restructuration schemes are displayed in Table 3.

We notice that the control state splitting heuristic leads to improved results for all tools, as shown by the comparison of Tables 3a and 3c on the one hand, and Tables 3b and 3d on the other. These results also confirm that ISL is significantly better in the treatment of concurrent loops, as previously noticed in Section 2.5: it outperforms the other tools on merged models (Table 3b). Aspic has lower scores than ISL on split models, with or without merging (Tables 3c and3d), because it cannot accelerate transitions that are generated by control node merging. PIPS is the worst performer in all cases, but we managed to increase its success rate by about 3a to Table 3d). The merge-splitting strategy gives the best results for ISL and PIPS.

Once again, detailed results are more contrasted. There is still no inclusion relation between successful test cases for different tools, whatever the restructuration scheme is chosen (Figure 8). The same holds for invariant sharpness.

Conclusion and Future Work

In this paper, we described ALICe, a benchmark for automatic tools that compute affine loop invariants. The benchmark consisted in 102 test cases taken from previously published papers from the relevant literature, and helper tools that allowed to compare three invariant generators, Aspic, ISL and PIPS, handling their different formats. We also presented two model restructurations, splitting and merging, that can be used separately or together to improve results and highlight the differences between tools. Finally, we gave some insight on the benchmark results.

The ALICe toolset provides a framework to improve current results, either by working more deeply on the model restructurations, or improving the loop computation algorithms used in PIPS or other tools to deal with weaknesses in concurrent loop computation.

There are two ways to further pursue this work. The benchmark can be expanded, either by adding more test cases, which is relatively easy but time-consuming, or by integrating other analysis tools, such as FASTer [START_REF]FAST -fast acceleration of symbolic transition systems[END_REF][START_REF] Bardin | FASTer acceleration of counter automata in practice[END_REF] or NBAC [START_REF] Jeannet | [END_REF][START_REF] Jeannet | Dynamic partitioning in linear relation analysis: Application to the verification of reactive systems[END_REF]. Before adding new tools, it may be interesting to equip the models with a minimum invariant , of which computed invariants should be supersets to be considered correct. This would reduce the problems posed by the presence of a buggy or cheating tool, that could generate wrong, too narrow invariants and would apparently pass all test cases. Adding deliberately incorrect models could also address this issue.

Figure 3 :

 3 Figure 3: Distribution of test cases

Listing 1 :

 1 Source code in fsm format

Figure 4 :

 4 Figure 4: Analysis steps within ALICe

Figure 5 :

 5 Figure 5: Venn diagram of successes for each tool

Figure 6 :

 6 Figure 6: Model of Figure 1 transformed by the splitting heuristic

Figure 7 :

 7 Figure 7: Model of Figure 1 reduced to a unique control point

Figure 8 :

 8 Figure 8: Venn diagrams of successes for each tool

Table 1 :

 1 Benchmark results

	Successes Time (s.)	75 10.9	63 35.5 46.2 43

Table 3 :

 3 Benchmark results with different encodings 50 % (from Table

	Successes Time (s.)	Aspic ISL PIPS 75 63 43 10.9 35.5 46.2	Successes Time (s.)	Aspic ISL PIPS 59 70 40 16.7 26.2 50.0
		(a) Direct		(b) Merged
	Successes Time (s.)	Aspic ISL PIPS 79 72 50 12.8 43.0 61.7	Successes Time (s.)	Aspic ISL PIPS 70 83 63 11.3 40.8 59.5
		(c) Split	(d) Merged-split


Sébastien Canard

Julien Devigne

Fabien Laguillaumie

Improving the Security of an Efficient Unidirectional Proxy Re-Encryption Scheme

published or not. The documents may come   L'archive ouverte pluridisciplinaire


Aurélie Lemaitre
email: aurelie.lemaitre@irisa.fr

Jean Camillerapp
email: jean.camillerapp@irisa.fr

Bertrand Coüasnon
email: couasnon@irisa.fr

Handwritten text segmentation using blurred image

Keywords: text line segmentation, handwritten document, structure analysis, blurred image

In this paper, we present our new method for the segmentation of handwritten text pages into lines, which has been submitted to ICDAR'2013 handwritten segmentation competition. This method is based on two levels of perception of the image: a rough perception based on a blurred image, and a precise perception based on the presence of connected components. The combination of those two levels of perception enables to deal with the difficulties of handwritten text segmentation: curvature, irregular slope and overlapping strokes. Thus, the analysis of the blurred image is efficient in images with high density of text, whereas the use of connected components enables to connect the text lines in the pages with low text density. The combination of those two kinds of data is implemented with a grammatical description, which enables to externalize the knowledge linked to the page model. The page model contains a strategy of analysis that can be associated to an applicative goal. Indeed, the text line segmentation is linked to the kind of data that is analysed: homogeneous text pages, separated text blocks or unconstrained text. This method obtained a recognition rate of more than 98% on last ICDAR'2013 competition.

INTRODUCTION

Handwritten text line segmentation is still an open problem, as shown by the recent competitions on this topic, for example in ICDAR'2013. [START_REF] Stamatopoulos | Icdar 2013 handwriting segmention contest[END_REF] Thus, if text line detection in printed document is considered as an easy task, the handwriting brings uncertainty in the recognition. Thus, in handwritten documents, the text lines are not regularly spaced. They often overlap each-other. They may have a global slope or a local curvature, which differs from one writer to another, and even inside a given text, from one line to another. These properties are common for many languages, and many scripts: Latin letters, Greek, Bangla... Thus, in the competitions that are proposed in the community, these languages are often mixed.

In this paper, we present our new method for text line detection that has been submitted for ICDAR'2013 text line segmentation competition. [START_REF] Stamatopoulos | Icdar 2013 handwriting segmention contest[END_REF] This method is based on two levels of analysis: a low level analysis of a blurred image, and a high level description of a page model. This method is able to deal with the difficulties of the handwritten irregular texts, and with various kinds of scripts (figure 11). Moreover, our method is implemented with two levels of analysis: a generic low level of primitive extraction, and a grammatical level that enables to introduce some knowledge about each specific kind of document to analyze. Indeed, we consider that it is necessary to take into account the page model of a collection to set up some sepecific recognition strategies or parameters. Thus, the segmentation process may slightly differ if we work on single text blocs, on unconstrained handwritten notes or even in heterogeneous documents that contains both handwritten and printed text. In particular, it is important to decide how to interpret the white spaces bewteen pieces of text lines.This is the kind of information that we want to express with a grammatical description. Consequently, the low level analysis is generic, whereas the introduction of the necessary knowledge is restricted to the grammatical part.

The paper is organized as follows. Section 2 presents some related work on handwritten text segmentation. Then, the sections 3 and 4 detail the two steps of our method. The section 5 shows our results on some various international competition databases and ends by a discussion.

RELATED WORK

The text line segmentation has been studied in various fields: typewritten documents, historical documents, 2 unconstrained documents, 3 handwritten documents . . . The presented approaches sometimes only detect the presence of text lines in the document, by representing the base line of the text. However, some application fields require a more precise segmentation, at pixel level, for example in the case of a pre-processing for handwriting recognition.

We focus on the methods that address the same problem as our, that is to say the segmentation of single handwritten text pages into text lines, at pixel level. This task is defined in the competitions that have been proposed by Gatos et al. in ICDAR'2009, 4 ICFHR 2010 [START_REF] Gatos | Icfhr 2010 handwriting segmentation contest[END_REF] and ICDAR'2013.

The results of the segmentation competition 5 highlight a few methods that obtained good recognition rates in the previous years. Thus, Louloudis et al. [START_REF] Louloudis | Text line and word segmentation of handwritten documents[END_REF] present an efficient method based on Hough transform mapping. This method requires various post-processing treatments that are based on the presence and the re-segmentation of connected components.

Papavassiliou et al. [START_REF] Papavassiliou | Handwritten document image segmentation into text lines and words[END_REF] apply a smooth version of the projection profile. They base their analysis on an oversegmentation of the document into small regions; those regions are then classified into text and gap regions using a HMM. Their method is convenient to deal with skew and irregular patterns but has limits when the majority of the characters are broken into many fragments.

More recently, another approach has been proposed in. [START_REF] Messaoud | A multilevel text-line segmentation framework for handwritten historical documents[END_REF] It combines several different existing techniques such as vertical projections, grouping connected components, nearest neighbor. This work is applied on ICFHR'2010 database, but it cannot be compared to the other participants as the used metric is different.

All those methods presented for the competition often seems dedicated to the specific database of the competition, that is to say single column handwritten pages.

We ourselves took part to the previous competition with a method based on the perceptive vision. [START_REF] Lemaitre | A perceptive method for handwritten text segmentation[END_REF] In this method, we proposed to combine two points of view of the document. In a low resolution image, we use a line segment extractor based on Kalman filtering to predict the position of the text lines in the document. We verify this prediction by taking into account the presence of connected components in a high resolution level of image. This approach has shown its limits during ICFHR'2010 competition: the extraction of line segments is realized at a very low resolution (image dimensions are divided by 16). Thus, it is sensitive to very small variations of the image, and to quantization noise.

In this paper, we present our new method. We keep thinking that combining two ways of interpreting the image can improve the recognition, as the human brain combines several perceptions for the interpretation of a scene. That is why we propose to combine two levels of analysis: the extraction of significant black regions in a blurred image, and an analysis of connected component.

Our low level analysis is close to the one proposed in. [START_REF] Li | Script-independent text line segmentation in freestyle handwritten documents[END_REF] However, the difference with this method is the way we combine the two perception levels. Thus, we propose to use a grammatical description of the page model, in order to introduce some knowledge on "how to combine the two points of view", depending on the context of application. Thus, we estimate that, in order to have a better recognition of text lines, it is necessary to include knowledge about the page context. Indeed, the thresholds or the parameters may differ when finding text lines on handwritten or printed documents, in single column text (figure 11), in multi column text (figure 5) or in unconstrained documents with erasures or word insertions. [START_REF] Li | Script-independent text line segmentation in freestyle handwritten documents[END_REF] That is why we separate two levels of analysis: a low level analysis that is generic and enables to detect the significant black regions (with high density of black pixels) on any kind of document; and a high level analysis, based on a grammatical description, which enables to introduce the necessary dedicated knowledge, for the recognition of a kind of page model. An overview of our method is proposed on the flowchart of figure 1.

LOW LEVEL IMAGE ANALYSIS

The goal of the low level image analysis is to extract some indications about the position of text lines, called line axes, without introduction of knowledge about the page model. Thus, this part of the work is generic and can be applied for the detection of text lines in various kinds of documents.

The low level image analysis is based on a blurred image. It is composed of two steps: the extraction of significant black regions in the image to build parts of line axes, and the construction of line axes.

Extraction of significant black regions

The analysis is based on a binary image (the image is binarized if necessary). On the first step, the image is blurred. For this purpose, we use a recursive low pass filter with IIR (Infinite Impulse Response). An example of blurred image is shown on figure 2. Then, a double binarization is applied on the blurred image, as presented on figure 3. We first compute the average grey-level of the blurred image, and use this value as a threshold for the first binarization. It gives some rough indication on the zones that contains text (in red on figure 3(a)). As we work after a low pass filter, we use only a sub-sampling of the columns. For the second binarization, we compute a threshold for each run-lentgh in a column of the image that contains some text: the threshold value is 50% of the darkest black pixel of the run-length. We obtain the second binarization (in blue on figure 3(b)). This second binarization corresponds to the presence of significant black regions in the image that will be used to build the line axes. The interest of this method is that we can find the significant black region, and the method is not very sensitive to the size of the characters or of the vertical line spacings.

Construction of line axes

Once the significant black regions have been detected, they are used to build line axes. We study the black regions, column after column, with a criteria of position and thickness to link them. When the black regions have a regular position and thickness among several columns, we produce a line axis. Some example of produced line axes are presented on the figure 4(a). This first step of analysis enables to compute an average thickness of the black regions, and an average slope of the document. Those thickness and slope are then used for the extension of the line axes. We then classify the pieces of line axes depending on their average thickness, relatively to the medium thickness on the page:

• when two line axes have a medium thickness and a regular slope and position, they are grouped into a single line axis,

• a line axis with a too thin thickness is removed, it may not correspond to a significant text line,

• a line axis with a too large thickness is studied to determine if it corresponds to:

an error in the construction of the significant black region: there is a single black region that corresponds to two text lines; a larger text zone in the initial document, such as capital letters, title. . . At the end of this low level treatment, we obtain the line axes as presented on figure 4(b). The line axes are not complete, but at that low level, we cannot determine if the holes between the axes correspond to an incomplete line (like in image 4(b)) or to a real blank in the document, for example between two columns (figure 5). That is why we delegate to the page model the role to combine the line axes into text lines.

GRAMMATICAL DESCRIPTION OF THE PAGE MODEL

This second step aims at building the text lines of the document, using the line axes that have been detected at the low level image analysis. In this second step, it is necessary to express some knowledge about the kind of images that are studied. Thus, the process of text line construction may vary if we study regular single column text pages, isolated text blocks or multi-column text pages, such as mail pages, or even totally unconstrained text pages. Depending on the organization of the document, the aligned or close line axes must be gathered together into a single text line, or must remain separated with two isolated text lines.

In order to externalize the knowledge related to the page model, we propose to express it using a grammatical description of the page. This grammatical description is based on two kinds of primitives: the connected components and the line axes extracted at the previous step (figure 6). The grammatical description of the page model can include two steps for line recognition: the localization of the text lines in the document, and then the assignment of the pixels to the text lines.

In this paper, we present the page model that has been applied for ICDAR'2013 competitions. The images contain single column text. The images do not contain extra information as images or graphics, that is to say all the pixels belong to a text line. Consequently, our grammatical description of the content must join together the line axes that belong to the same text line.

Localization of text lines

The localization of text lines exploits the presence of line axes to compute the global text lines. As we have seen previously, the line axes are not always complete, and the page model must define whether they have to be linked with each other or not.

However, the handwritten nature of the document makes it not so easy: the text lines may contain some slope, some curvature. A brutal concatenation of line axes at a global level is too rough to produce the global segmentation. That is why we propose to locally use the presence of connected components to build the text lines.

Our grammatical description follows the rules below:

• For each line axis look for the connected components at the close extremity of the line axis (figure 7 This description enables to build the text lines that are directly deduced from the line axes. However, sometimes some line axes are not detected at all on text lines, more particularly on short text lines. Thus, when the density level of black pixels is too weak, we cannot detect any significant black region on the blurred image. To deal with that limit, we add a second rule in our grammatical description:

• For each isolated connected component that does not belong to a text line look for the neighbor connected components, build a text line when finding an isolated set of aligned connected components.

This step enables to build some additional text lines (in red on figure 8), that had been forgotten in the blurred image analysis.

Figure 8. Additional line axis (in red) built on isolated sets of aligned connected components

At that step of the analysis, we know the position of each text line in the document. This information can be sufficient, depending on the context of application, mainly for global structure document recognition. However, for certain tasks such as handwriting recognition, it is necessary to know which pixel belongs to each text line. This association is realized in the next step of analysis.

Assignment of pixels to text lines

The assignment of each pixel to a text line is realized using a grammatical description of the document. Thus, this step of analysis requires some specific knowledge, linked to the field of application: do we need a precise assignation of each pixel? is each pixel associated to a given text line or is there some unassigned noise pixels?

In the proposed model, used for ICDAR'2013 competition, each pixel must be assigned to a given text line.

That is what we express in our grammatical description. In order to simplify the assignment of pixels, we use the entity of connected component: each connected component is assigned to a text line. However, when necessary, we can re-segment the conflicting connected components, so that they are associated to several text lines.

Our grammatical description follows the rules below:

• For each connected component look for the upper and lower nearest text lines, identify the connected component as conflicting if it is near at least two text lines, taking into account the base lines of the upper and the lower text lines (figure 9(a)),

re-segment the conflicting connected components, using the medium position between upper and lower baselines (figure 9(b)).

• After the re-segmentation, for each connected component assign the connected component to the nearest text line (figure 10).

EXPERIMENTS

We present the application of our handwritten text line segmentation method on public available databases. We first present the databases and metrics, and our comparative results. We show that we have applied our method on several international databases. We present our results on ICDAR'2013 competition, the comparison with our previous Kalman based method and with the other participants of the competiton. We evaluate the quality of our text-line detection system. We then discuss the interests and the limits of our approach.

Databases and metrics

We apply our method on five different databases, all provided by Gatos, Stamatopoulos and Louloudis for the different international competitions of the past years: ICDAR'2009, 4 ICFHR'2010, [START_REF] Gatos | Icfhr 2010 handwriting segmentation contest[END_REF] and ICDAR'2013. In addition of the three competition databases, we also present our results on the two training databases that were provided to the participants.

The properties of those five databases are presented on table 1: each database is made of 100 or 200 images. The images are handwritten document pages in various scripts and languages: French, English, Latin, Greek, and India Bangla. Some examples of the proposed images are presented on figures 11 and 12 . The metric used is the one proposed by Gatos et al. [START_REF] Gatos | Icdar2009 handwriting segmentation contest[END_REF] For each text line, we compute the rate of pixels that has been correctly labeled. If this rate is bigger than a threshold called Ta, Threshold of acceptance, then the text line is considered as recognized. By default, Ta equals 95%, which means that a text line is recognized if 95% of its pixels have been correctly labeled.

Let N the number of lines present in the ground-truth, M is the number of text lines retrieved in the hypothesis, and o2o is the number of recognized text lines, according to the Ta threshold. Three values are then computed:

• the Detection Rate, DR=o2o/N,

• the Recognition Accuracy, RA=o2o/M,

• the performance metric FM=2*DR*RA/(DR+RA).

Results

We present several comparative results.

Application to various databases

First, we apply our method on the five databases that we have presented above. The table 1 presents the obtained performances. We have mainly trained our method on the two training databases. The results show that the recognition rates are quite stable between 98 and 99%. The slight variations from one database to another come from very small differences of difficulty on the images.

Results on ICDAR'2013 competition

We now present the performances of our method for ICDAR'2013 competition. The method that has been presented for the competition is called Submitted method. However, we must precise that our method was not totally achieved when we had to take part to ICDAR'2013 competition. Thus, we have kept going on improving our method, after the submission for the competition, but before obtaining the competition image database. We call Last version of our method the last obtained method.

When we received the competition database, we could compare three methods:

• our previous method, based on Kalman filtering, 9 that took part to ICFHR'2010 competition,

• the submitted method, that took part to the ICDAR'2013 competition,

• the achieved last version of our method.

The table 2 presents the comparative recognition rates on the competition database. The results shows that our new method based on blurred image significantly improves the results, compared with our Kalman based filtering method: FM rates goes from 94.6% to 98.0%. This is due to the limits of the method based on Kalman filtering. We can also notice that the last version is slightly better than the submitted method.

Database Previous

Comparative results with other participants

In order to evaluate our new method in comparison with the other approaches, we present some results on the ICDAR'2013 competition, on figure 13. The blue items are the methods that were proposed by the other participants of the competition in 2013. [START_REF] Stamatopoulos | Icdar 2013 handwriting segmention contest[END_REF] The red item presents our participation in 2013. Our method is in the best five ones, over 13 proposed methods. The green item presents the rate obtained with our last version of the method: it obtains the third place with a FM rate of 98.06%.

Quality of the text line detection

As presented in the metric section 5.1, the result rates are strongly linked to the threshold of acceptance Ta, which is the rate of pixels correctly affected to recognize one line. By default, this rate is 95%. Thus, sometimes, a text line that is quite well detected, for example with 92% of pixels will be count as 0 in the final rate FM. In order to evaluate the global quality of the detected text line, we propose to study the evolution of our systems, depending on the threshold of acceptance Ta (figure 14). These results show that our new method is able to localize more than 99% of text lines, even if sometimes only 89% of pixels are correctly assigned. This is really much better than the previous Kalman filtering method that reaches a maximum at 97% of text lines.

These results shows that the main limit of our method is the association of pixels to the text lines. We will discuss that point in the following section.

Discussion

The results have really been improved, by comparison with our previous work. The strength of this method comes from the combination of two levels of analysis of the image: the blurred image at a global level and the connected components at a local level. This combination enable to deal with the difficulties met in handwritten documents: irregular slope, curvature and overlapping text lines.

Thus, the construction of line axes on the blurred image is very convenient in high density zones of text (figure 15(a)). On those kinds of images, the analysis of connected components would be difficult because of the overlapping text lines that require a lot of re-segmentation.

On the opposite, in the locally low density images, the analysis of the blurred image is incomplete (figure 15(b)), because some significant black regions are difficult to extract. However, on those images, it is very easy to follow the local presence of connected components to find the presence of a text line, because the connected components are well isolated. We will now discuss the limits of our method. As presented in the results, we are missing about 1% of text line in the segmentation process. The main limit of our method is due to the assignation of the pixels to the text lines.

On the one hand, our method for re-segmenting connected components on overlapping text lines is really rudimentary (figure 16(a)): the connected components are roughly segmented in the middle position between the upper and the lower lines. We should improve this segmentation.

On the other hand, the connected components are associated to the nearest text line, which presents limits with very small and segmented connected components, like on figure 16(b): the upper pixels of the second line are allocated to the first one.

CONCLUSION

In this paper, we have presented the method that took part to the ICDAR'2013 handwritten segmentation competition. This method is based on the cooperation of two levels of analysis of the image: the low level analysis of a blurred image, that gives some indications about the position of line axes, and a local analysis of connected components in order to obtain the precise position of text lines. We have shown in the results that those two levels of analysis are complementary as they enable to address different difficulties, in high density zones of black pixels, such as in low density zones.

Moreover, those two steps of analysis can be reused in other kinds of document processing. Thus, the first step of blurred image analysis is generic and can be applied for searching significant black regions in any kind of document. The second step contains the page model. We choose to use a grammatical description. Thus, for studying a new kind of document, it is only necessary to change the knowledge contained in the page model. For example, we could easily describe the text lines present in a multi-block document such as mail document by only changing the page model (figure 5).

For the future work, we should focus on the assignment of pixels to the text lines, and more particularly the re-segmentation of connected components, which is too rough in the current version. We will also focus on applying our text line segmentation method on other kinds of document. The difficulty for that purpose is to evaluate the text line segmentation as few public databases are available with a ground truth at pixel level.

Figure 1 .

 1 Figure 1. Overview of the steps of the proposed method

Figure 2 .

 2 Figure 2. Construction of the blurred image

Figure 3 .

 3 Figure 3. Double binarization of the blurred image, with a sub-sampling of the columns

Figure 4 .

 4 Figure 4. Construction of line axes

Figure 5 .

 5 Figure 5. Example of extracted line axes on a mail document

Figure 6 .

 6 Figure 6. Input data for the grammatical step: line axes and connected components in red

  (a)), extend the line axis taking into account the presence of connected components (figure 7(b)), when meeting another line axis, merge the two line axes into a single text line (figure 7(c)).

Figure 7 .

 7 Figure 7. Construction of text lines

Figure 9 .

 9 Figure 9. Re-segmentation of connected components

Figure 11 .

 11 Figure 11. Example of obtained line segmentation results, on images with various scripts and languages

Figure 12 .

 12 Figure 12. Example of obtained line segmentation results, on images with difficulties: overlapping text lines, varying slope and curvature

Figure 13 .

 13 Figure 13. Comparative results on ICFHR'2013 competition: results obtained by all the participants, including our latest version, named IRISA-b

Figure 14 .

 14 Figure 14. Comparison results for text line segmentation using various acceptance threshold values on the competition 2013 database.

  Figure 15. Interest of the cooperation between blurred image and connected components analysis

  Figure 16. Main limit of our method: assignation of pixels to lines

Table 1 .

 1 Properties of several competition databases and comparative results obtained by our method

	Database 2008 training ICDAR'2009 ICFHR'2010 2013 training ICDAR'2013
			competition	competition		competition
	Image nb	100	200	100	200	150
	Line nb	2242	4034	1629	3727	2679
	FM	98,10%	99,52%	99,35%	99,26%	98,06%

Table 2 .

 2 Comparative results of our three methods on ICDAR'2013 competition