David Monniaux

Martin Bodin

Modular Abstractions of Reactive Nodes using Disjunctive Invariants *

We wish to abstract nodes in a reactive programming language, such as Lustre, into nodes with a simpler control structure, with a bound on the number of control states. In order to do so, we compute disjunctive invariants in predicate abstraction, with a bounded number of disjuncts, then we abstract the node, each disjunct representing an abstract state. The computation of the disjunctive invariant is performed by a form of quantifier elimination expressed using SMT-solving.

The same method can also be used to obtain disjunctive loop invariants.

Introduction

Our goal is to be able to compute sound abstractions of reactive nodes, with tunable precision. A reactive node in a language such as Lustre, 1 or Scade, 2 Sao, 3 or even Simulink, 4 has input streams, output streams, and an (optional) internal state: at each clock cycle, the value on each output is a function of the values on the inputs and the state; and so is the next value of the state.

If the state consists in a finite vector of Booleans, or other finite values, then the node is a finite automaton, with transitions guarded according to the current values of the inputs, and for each state a relation between the current values of the inputs and the current values of the outputs. This is often referred to as the control structure of the reactive program. The problem with that representation, which exposes the full internal state, is that the number of states 1 grows exponentially with the number of state variables, making it unwieldy for analysis. The problem is even more severe if the control conditions are not directly exposed as Boolean state variables, but as predicates over, say, integer or real variables (see example in Sec. 4).

The main contribution of this article is a method for constructing a more abstract automaton, with a bounded number of states (≤ n), whose behaviors still over-approximate the behaviors of the node. In order to do so:

1. We compute an over-approximation of the set of reachable states of the node, in an unspecified context, as a union of at most n "abstract states", each defined by a conjunction of constraints (these abstract states need not be disjoint).

2. We compute the most precise transition relation between these abstract states.

This automatic abstraction maps a reactive node into another, more abstract (and, in general, nondeterministic) reactive node. This enables modular and compositional analysis: if a node is composed of several nodes, then one can replace each of these nodes by its abstraction, and then analyze the compound node.

As a secondary contribution, the analysis method at step 1 can also be used to obtain disjunctive loop invariants for imperative programs (or, more generally, invariants for arbitrary control flow graphs), given a precondition and an optional postcondition. We describe this algorithm for obtaining invariants in disjunctive normal form, but it in fact also works for other templates.

Our algorithms use satisfiability modulo theory (SMT) solving as an essential subroutine; see e.g. [START_REF] Cimatti | Beyond Boolean SAT: Satisfiability modulo theories[END_REF] for an introduction.

Invariants by Predicate Abstraction

Predicate abstraction abstracts program states using the truth value of a given finite set of predicates {π 1 , . . . , π m }: each state σ is abstracted by a m-tuple of Booleans(π 1 (σ), . . . , π m (σ)). The most precise abstract transition relation between such vectors of Booleans is (B 1 , . . . , B m )

→ π (B ′ 1 , . . . , B ′ m ) if and only if there exist σ |= (π i = B i ), σ ′ |= (π i = B ′ i )
, and σ → σ ′ where → is the transition relation of the program. Then, given an abstract initial state, the set of reachable states of the abstract transition relation can be computed within finite time (in general, exponential in m) by Kleene iterations (equivalently, by computing the transitive closure of → π ).

Such an approach is, however, unworkable in general because of the exponential number of states generated, and thus all current predicate abstraction schemes use some stronger form of abstraction [START_REF] Graf | Construction of abstract state graphs with PVS[END_REF]; for instance, they may simply compute a conjunction of the π i that holds inductively at a given program point. Conjunctive invariants are however fairly restrictive; in this article, we consider the problem of obtaining invariants as disjunctions of a fixed number of conjunctions of the chosen predicates.

The set of reachable states of a reactive node, in an unspecified environment, is the strongest invariant of an infinite loop: while ( true ) { i = i n p u t s ( ) ; o = o u t p u t s ( s t a t e , i ) ; s t a t e = n e x t s t a t e ( s t a t e , i ) ; } We shall therefore investigate the problem of automatically finding disjunctive inductive loop invariants (or, more generally, invariants for predicate abstraction following a fixed template), using predicate abstraction, given a precondition and an optional postcondition. These invariants shall be minimal with respect to the inclusion ordering: there shall be no stronger inductive invariant definable by the same template.

Solution of a Universally Quantified Formula

Let us assume a finite set Π = {π 1 , . . . , π m } of predicates over the state space of the variables of the program. Let n ≥ 1 be an integer. We are looking for invariants of the form C 1 ∨ • • • ∨ C n where the C i are conjunctions of predicates from Π (most of our techniques are not specific to this template form, see Sec. 2.5 for extensions).

Any such invariant can be obtained by instantiating the Booleans b i,j in the following template:

T △ = i b i,j ⇒ π j Ci (1)
Setting b i,j to true(respectively, false) in that template means that predicate π j appears (respectively, does not appear) in the i-th

disjunct C i . For instance, if Π = {x > 0, x < 1, y > 0} and n = 2, then b 1,1 = true, b 1,2 = true, b 1,3 = false, b 2,1 = false, b 2,2 = false, b 2,3 = true correspond to (x > 0 ∧ x < 1) ∨ y > 0.
The problem of finding an invariant reduces to finding suitable values for these Booleans. There is therefore a search space for invariant candidates of a priori size 2 mn . We impose that the invariant I obtained be minimal within that search space with respect to the inclusion ordering; that is, there is no I ′ expressive using the template such that I ′ I.

Our algorithm can in fact apply to any control-flow graph. For the sake of simplicity, we shall describe it on a single loop.

In Hoare logic, the conditions for proving that a postcondition P holds after a while loop whose condition is C, whose transition relation is T and whose precondition is S using loop invariant I are:

• I must contain the precondition, otherwise said ∀σ S ⇒ I.

• I must be inductive, otherwise said ∀σ, σ ′ I ∧ C ∧ T ⇒ I ′ , with I ′ denoting I where all state variables have been primed.

• I ∧ ¬C must imply the postcondition, otherwise said ∀σ I ∧ ¬C ⇒ P .

If we impose I to be an invariant of the required form, that is, an instantiation T [B/b] of T obtained by setting the b i,j variables to certain values B i,j , these conditions boil down to the values B i,j of the b i,j variables must satisfy certain formulas universally quantified over the state σ or on the couple of states σ, σ ′ .

We now make an additional assumption: the states σ or σ ′ comprise a fixed, finite number of variables5 expressible in a theory T for which there exists a satisfiability testing algorithm, in which the predicates π 1 , . . . , π m can be expressed, and which allows propositional variables. Thus, the problem boils down to finding a solution to a conjunction of universally quantified formulas of that theory such that the only free variables are the b i,j Booleans.

In the following sections, lowercase σ and σ ′ stand for states (thus stand for a finite number of variables in the theory T), uppercase Σ and Σ ′ stand for values of these state variables. Similarly, lowercase b stands for the matrix of propositional variables (b i,j ) 1≤i≤m,1≤j≤n , and uppercase B stands for the matrix of Booleans (B i,j ) 1≤i≤m,1≤j≤n . F [B/b] thus stands for the formula F where the propositional values b have been replaced by the corresponding Booleans in B, and F [Σ/σ] stands for the formula F where the state variable σ has been replaced by the state value Σ.

Naive Algorithm for a Given Postcondition

In this section, we shall explain how to compute an invariant suitable for proving the Hoare triple of a loop, given a precondition, a postcondition (which may be true), a loop condition and a transition relation.

Let us first give an intuition of the algorithm. A universally quantified formula ∀σF with free Boolean variables b can be understood as specifying a potentially infinite number of constraints F [Σ/σ] over b, where Σ ranges all possible values for σ (in this section, we will lump together σ and σ ′ as a single σ). The idea is to "discover" such constraints one at a time, when they are violated.

Let us now examine the algorithm in more detail; see Sec. 3 for a complete algorithm run. The H k sequence of propositional formulas over the b variables will express successive refinements of the constraints during the search of a suitable assignment. Initially, we do not know anything about possible solutions, so we set H 1 △ = true. We start by taking any initial assignment B (1) (since any will satisfy H 1 ) and check whether ¬F [B (1) /b] is satisfiable, that is, whether one can find suitable values for σ. If it is not, then B (1)

|= ∀σ F . If it is satisfiable, with example value Σ 1 , we add F [Σ 1 /σ] as a constraint -that is, we take H 2 △ = H 1 ∧F [Σ 1 /σ];
note that this constraint excludes B (1) and possibly other values for b. Now find an assignment (1) and B (2) . The process continues until a suitable assignment is found or the constraints exclude all assignments. Note that one Boolean assignment at least is excluded at each iteration, and that the number of Boolean assignments is finite (exponential in the number of propositional variables in b).

B (2) satisfying H 2 , check whether ¬F [B (2) /b] is satisfiable. If it is not, then B (2) |= ∀σ F . If it is satisfiable, with example value Σ 2 , we take H 3 = H 2 ∧F [Σ 2 /σ]; note that H 3 excludes B
More formally: recall that we have reduced our problem of finding an invariant to finding Boolean values B i,j such that (B i,j ) 1≤i≤m,1≤j≤n |= ∀σ F for a certain quantifier-free formula F whose free variables are (b i,j ) 1≤i≤m,1≤j≤n . Let us now assume we have a SMT-solver for theory T, a function SMT(G) which given a formula G answers sat(M ) when G is satisfiable, where M is a model, that is, a suitable instantiation of the free variables in G, or unsat otherwise. We shall also assume a SAT-solver SAT with similar notations, for purely propositional formulas. We run the following algorithm, expressed in pseudo-ML:

H := true loop match SAT (H) with | unsat → return "no solution" | sat((B i,j ) 1≤i≤m,1≤j≤n ) → match SMT(¬F [B/b]) with | unsat → return "solution B" | sat(Σ) → H := H ∧ F [Σ/σ].
This algorithm always terminates, since the main loop iterates over a finite set of size 2 |b| where |b| = mn is the size of the matrix b of propositional variables: the number of models of the propositional formula H decreases by at least one at each iteration, since model B is excluded by the

F [Σ/σ] condition. The loop invariant is ∀σ F =⇒ H. This invariant is maintained: whatever we choose for Σ, if ∀σ F =⇒ H, ∀σ F =⇒ H ∧ F [Σ/σ].
If the algorithm answers "no solution" for H, because of the invariant, there is no solution for ∀σ F . If the solution answers "solution B", the "unsat" answer for SMT(¬F [B/b]) guarantees that B |= ∀σ F .

Note the use of two solvers: one SAT for the propositional variables b, and one SMT for the state variables σ (or σ, σ ′ ). The SAT solver is used incrementally: one only adds new constraints. The SMT solver is always used with the same set of predicates, enabling it to cache theory lemmas.

Performance Improvements

The algorithm in the preceding subsection is sound, complete and terminating. Yet, experiments have shown that it tends to generate useless iterations. One reason is that the system may iterate across instances B that yield the same formula T [B/b] up to a permutation of the C i disjuncts. Another is that the system may generate empty disjuncts C i , or more generally disjuncts that are subsumed by the other disjuncts (and are thus useless). We shall explain how to deal with those issues.

Removal of Permutations

We impose that the disjunction C 1 ∨• • •∨C n follows a unique canonical ordering. For this, we impose that the vectors of m Booleans (B 1,j ) 1≤j≤m , . . . , (B n,j ) 1≤j≤m are in strict increasing order with respect to the lexicographic ordering ≺ L induced by false < true. This corresponds to n -1 constraints (b i,j ) 1≤j≤m ≺ L (b i+1,j ) 1≤j≤m , each of which can be encoded over the propositional variables (b i,j ) as formula L i,1 defined as follows:

• L i,j0 is a formula whose meaning is that (b i,j ) j0≤j≤m ≺ L (b i+1,j ) j0≤j≤m • L i,m+1 is false • L i,j0 for 1 ≤ j 0 ≤ m is defined using L i,j0+1 as follows: (¬b i,j0 ∧ b i+1,j0 ) ∨ ((b i,j0 ⇒ b i+1,j0 ) ∧ L i,j0+1
).

All such constraints can be conjoined to the initial value of H.

Removal of Subsumed Disjuncts

We can replace the SAT-solver used to find solutions for (b i,j ) by a SMT-solver for theory T, in charge of finding solutions for (b i,j ) and for some auxiliary variables σ 1 , . . . , σ n (we actually shall not care about the actual values of σ 1 , . . . , σ n ).

The following constraint expresses that the disjunct C i0 is not subsumed by the disjuncts (C i ) 1≤i≤n,i =i0 :

∃σ i0 C i0 [σ i0 /σ] ∧ 1≤i≤n,i =i0 ¬C i [σ i /σ] (2)
It therefore suffices to conjoin to the initial value of H the following constraints, for 1

≤ i 0 ≤ n: C i0 [σ i0 /σ] ∧ 1≤i≤n,i =i0 ¬C i [σ i /σ].
A variant consists in simply imposing that each of the C i is satisfiable, thus eliminating useless false disjuncts. For this, one imposes 1

≤ i 0 ≤ n, the constraint C i0 [σ i0 /σ].
Equivalently, one can pre-compute the "blocking clauses" over the b i0,j propositional variable that constrain these variables so that C i0 is satisfiable, and add them as purely propositional constraint. This is the method that we used for the example in Sec. 3 (we wanted to keep to propositional constraints for the sake of simplicity of exposition).

Iterative Refinement of Invariants

We have so far explained how to compute any invariant, with or without imposing a postcondition. If we do not impose a postcondition, the formula true, for instance, can denote a wholly uninteresting invariant; clearly we would like a smaller one. In this section, we shall explain how to obtain minimal invariants within the search space.

For a Fixed Disjunction Size

Let us now assume we have the postcondition P (if we do not have it, then set P to true). A natural question is whether one can get a minimal inductive invariant of the prescribed form for the inclusion ordering; that is, an invariant

T [B 0 /b] such that there exists no B such that T [B/b] ⊆ T [B 0 /b], by which we denote ∀σ T [B/b] ⇒ T [B 0 /b].
We shall now describe an iterative algorithm that first obtains any inductive invariant of the prescribed form, and then performs a downwards iteration sequence for the inclusion ordering, until a minimal element is found.

Let us first note that it is in general hopeless to find a global minimum B 0 , that is, one such that ∀B T [B 0 /b] ⊆ T [B/b], for there may exist incomparable minimal elements. For instance, consider the program:

f l o a t i = 0 ; while ( random ( ) ) { i = i +1; i f ( i > 2 ) i = 0 ; }
The least inductive invariant of this loop, for variable i, is the set of floatingpoint numbers {0, 1, 2}. Now assume our set of predicates is {i ≤ 0, i ≥ 0, i ≥ 1, i ≤ 1, i ≤ 2, i ≥ 2}, and take n = 2; we thus look for disjunctions of two intervals. Two minimal incomparable invariants are (i

≥ 0 ∧ i ≤ 1) ∨ (i ≥ 2 ∧ i ≤ 2), that is, [0, 1] ∪ {2}, and (i ≥ 1 ∧ i ≤ 2) ∨ (i ≤ 0 ∧ i ≥ 0), that is, [1, 2] ∪ {0}.
Let us now assume we have already obtained an invariant T [B ′ /b] and we wish to obtain a better invariant

T [B/b] T [B ′ /b].
This last constraint can be written as the conjunction of:

1. T [B/b] ⊆ T [B ′ /b], otherwise said ∀σ T [B/b] ⇒ T [B ′ /b];
T [B ′ /b] ∧ ¬T [B/b]. When an invariant T [B/b] is found, the value Σ of σ is a witness that this invariant is strictly included in T [B ′ /b].
It is possible to compute a downward iteration sequence until a minimal element is reached: compute any initial invariant B (0) , then B (1) B (0) etc. until the system fails to provide a new invariant satisfying the constraints; one then takes the last element of the sequence. The termination condition is necessarily reached, for the (B (k) i,j ) 1≤i≤m,1≤j≤n Boolean matrices can never be twice the same within the sequence (because of the strict descending property). Furthermore, one can stop at any point B (k) within the sequence and get a (possibly non minimal) inductive invariant.

One can replace point 2 above by a weaker strategy, but with the advantage of operating only on propositional formulas. Note that B (k+1) has at least one component higher than B (k) for the standard ordering false < true on the Booleans, for if all components are lower or equal, then B (k+1) ⊇ B (k) , which is the opposite direction of what we wish. The strategy is to enforce this condition using i,j (b i,j ∧ ¬b ′ i,j ). This is what we used in Sec. 3.

For Varying Disjunction Sizes

The algorithms described above work for a given disjunction size n. The method for preventing subsumed disjuncts of part Sec. 2.3.2 imposes that all n disjuncts are truly needed: it is thus possible that no solution should be found for n = n 0 while solutions exist for n = n 0 -1. We therefore suggest that, once a minimal invariant I n0 is obtained for n = n 0 fixed, one looks for an invariant strictly included in I n0 for n = n 0 + 1. One can choose to stop such iterations when no solutions are found for a given n, or when a limit on n or a timeout is reached.

Extensions

Prohibition of Overlapping Modes Our algorithms produce disjunctions that cover all reachable states, but that do not define partitions: distinct abstract states may be overlapping. This may be somewhat surprising and counterintuitive.

It is possible to impose that disjuncts should be pairwise disjoint. For any i and j, one can impose that C i and C j are disjoint by the universally quantified formula ∀σ¬C i ∨ ¬C j . We have explained in the preceding sections how to deal with such universally quantified formulas.

Other Template Forms We have described our algorithm for templates of the form C 1 ∨• • •∨C m where the C i are conjunctions constructed from the chosen predicates, but the algorithm is not specific to this template shape. Instead of disjunctive normal form, one could choose conjunctive normal form, for instance, or actually any form [START_REF] Srivastava | Program verification using templates over predicate abstraction[END_REF], though reductions of the search space such as those from Sec. 2.3.1 or 2.3.2 may be more difficult to define.

Predicate Choice Our method is based on predicate abstraction; so far we have not discussed methods for obtaining the predicates, beyond the obvious syntactic detection. In many systems based on predicate abstraction, one uses counterexample-based abstraction refinement (CEGAR): from an abstract trace violating the specification, but not corresponding to a concrete trace violating the specification, one derives additional predicates for refining the system. Because we did not implement such refinement, we shall only give a rough description of our CEGAR method.

If there is no inductive invariant built from the requested template that can prove the desired postcondition, the algorithm from Sec. 2.2 will end up with an unsatisfiable constraint system. This system is unsatisfiable because of the postcondition constraints (otherwise, in the worst case, one would obtain a solution yielding the true formula); relevant postcondition constraints can be obtained from an unsatisfiable core of the constraint system. One can then try removing such constraints one by one until the constraint system becomes satisfiable again. Any solution of this relaxed constraint system defines an inductive invariant, but one that does not satisfy the postcondition. As with the usual CEGAR approach, one could try generating test traces leading from the initial states to the complement of the postcondition and staying within the invariant; if the postcondition holds, such searches are unsuccessful and yield interpolants from which predicates may be mined.

Step-by-step Example of Invariant Inference

For the sake of simplicity of exposition, in this section we have restricted ourselves to pure propositional constraints on the b i,j , and satisfiability modulo the theory of linear integer arithmetic for the combination of the b i,j and the state variables. We consider the following simple program.

i nt b , i =0 , a ; / * p r e c o n d i t i o n a > 0 * / while ( i < a ) { b = random ( ) ; i f ( b ) i = i + 1 ; }
The predicates are {π 1 , . . . , π 8 } △ = {i = 0, i < 0, i > 0, i = a, i < a, i > a, b, ¬b}. The state variable σ stands for (i, a, b). For the sake of simplicity, we model i and a as integers in Z, and b as a Boolean. We assume the loop precondition

S △ = i = 0 ∧ a ≥ 1. The loop condition is C △ = i < a, and the transition relation is T △ = (b ′ ∧ i ′ = i + 1) ∨ (¬b ′ ∧ i ′ = i). We choose n = 2.
We shall now run the algorithm described in Sec. 2.2 with the iterative refinement of Sec. 2.4.1. For the sake of simplicity, we shall use none of the improvements described in the preceding sections that need the H i to contain non propositional variables: no removal of subsumed disjuncts as described in Sec. 2.3.2 and no strict inclusion enforcement as described in Sec. 2.4.1.

We initialize H as follows: H 1 contains Boolean constraints on (b i,j ) 1≤i≤2,1≤j≤8

• That prevent C 1 and C 2 from being unsatisfiable, using blocking clauses as explained in Sec. 2.3.2: one cannot have both i = 0 and i > 0, and so on.

• That force (b 1,j ) 1≤j≤8 ≺ L (b 2,j ) 1≤j≤8 for the lexicographic ordering ≺ L on Boolean vectors (this avoids getting the same disjunction twice with the disjuncts swapped).

Let us now see the constraint solving and minimization steps.

1. We perform SAT-solving on H 1 and obtain a satisfying assignment B

(1)

1,1 = true, B

2,8 = true. This corresponds to the invariant-candidate T [B (1) /b], that is, (i = 0∧i = a∧b)∨(i = 0∧i = a∧¬b). Now is this invariant-candidate truly an inductive invariant? It is not, because it does not contain the whole of the set of initial states. SMTsolving on S ∧ ¬T [B (1) /b] gives a solution Σ 1

△ = (i = 0, a = 1, b = false).
We therefore take

H 2 △ = H 1 ∧ F [Σ 1 /σ]. 2. A satisfying assignment B (2) of H 2 yields the invariant candidate (i = 0 ∧ i = a ∧ b) ∨ (i = 0 ∧ i < a ∧ b).
Again, SMT-solving shows this is not an invariant because it does not contain the initial state Σ 2

△ = (i = 0, a = -1, b = false). We therefore take H 3 △ = H 2 ∧ F [Σ 2 /σ]. 3. A satisfying assignment B (3) of H 3 yields the invariant candidate (i = 0 ∧ i = a ∧ b) ∨ (i = 0 ∧ i < a)
. SMT-solving shows this is not inductive, since it is not stable by the transition Σ 3

△ = (i = 0, a = 1, b = false, i ′ = 1, b ′ = true). We therefore take H 4 △ = H 3 ∧ F [Σ 3 /σ].
4. A satisfying assignment B (4) of H 4 yields the invariant candidate (i = 0 ∧ i < a ∧ ¬b) ∨ b. SMT-solving shows this is not inductive, since it is not stable by the transition Σ 4

△ = (i = 1, a = 3, b = true, i ′ = 1, b ′ = false). We therefore take H 5 △ = H 4 ∧ F [Σ 4 /σ].
5. A satisfying assignment B (5) of H 5 yields the invariant candidate (i = 0 ∧ i < a) ∨ (i > 0 ∧ i = a ∧ b). SMT-solving shows this is not inductive, since it is not stable by the transition Σ 5

△ = (i = 0, a = 2, b = false, i ′ = 1, b ′ = false). We therefore take H 6 △ = H 5 ∧ F [Σ 5 /σ].
6. A satisfying assignment B (6) of H 6 yields the invariant candidate

I 1 △ = (i = 0 ∧ i < a) ∨ i > 0.
SMT-solving shows this is an inductive invariant, which we retain. We however would like a minimal inductive invariant within our search space. As described at the end in Sec. 2.4.1, we take H 7 the conjunction of H 6 and a propositional formula forcing at least one of the b i,j to be true while B (6) i,j is false. Furthermore, as described in point 1 of Sec. 2.4.1, we now consider F 2 △ = F ∧ (T ⇒ I 1 ), which ensures that we shall from now on only consider invariants included in I 1 .

7. A satisfying assignment B (7) of H 7 yields the invariant candidate (i > 0 ∧ i = a ∧ b) ∨ i < a. SMT-solving shows this is not included in I 1 , using

Σ 7 △ = (i = -47, a = 181, b = true). We therefore take H 8 △ = H 7 ∧ F 2 [Σ 7 /σ].
8. H 8 has no solution. I 1 is thus minimal and the algorithm terminates.

A postcondition for this loop is thus I 1 ∧ ¬(i < a), thus i > 0 ∧ i = a. Note that the method did not have to know this postcondition in advance in order to prove it.

Construction of the Abstract Automaton

We can now assume that the set of reachable states is defined by a formula

I = I 1 ∨ • • • ∨ I n ,
with each formula I i meant to define a state q i of the abstract automaton.

To each couple of states (q i , q j ) we wish to attach an input-output relation expressed as a formula τ i,j with variables I, ranging over the set of possible current values of the inputs and O over the set of possible current values of the outputs.

Recall that T is a formula expressing the transition relation of the reactive node, over variables I (inputs), σ (preceding state), σ ′ (next state) and O (outputs). Then the most precise transition relation is:

τ i,j △ = ∃σ, σ ′ I i ∧ I j [σ ′ /σ] ∧ T (3)
Any over-approximation of this relation is a sound transition relation for the abstract automaton. If we have a quantifier elimination procedure for the theory in which T and the I i are expressed, then we can compute the most precise τ i,j as a quantifier-free formula; but we can also, if needed, use an approximate quantifier elimination that yields an over-approximation.

Let us consider, as an example, the following Lustre node. It has a single integer input dir and a single integer output out. If dir is nonzero, then it is copied to out; else out decays to zero by one unit per clock cycle:

T △ = (d = 0 ∧ o ′ = d) ∨ (d = 0 ∧ o ≥ 1 ∧ o ′ = o -1) ∨(d = 0 ∧ o ≤ -1 ∧ o ′ = o + 1) ∨ (d = 0 ∧ o ′ = o = 0) (4)
Suitable predicates are {o ≤ -1, o = 0, o ≥ 1}, thus defining the set of reachable states as a partition I -1 ∨ I 0 ∨ I 1 where

I -1 △ = o ≤ -1, I 0 △ = o = 0, I 1 △ = o ≥ 1.
Let us compute τ 0,1

△ = ∃o, o ′ I 0 ∧ I 1 [o ′ /o] ∧ T , that is, ∃o, o ′ o = 0 ∧ o ′ ≥ 1 ∧ T : we obtain d > 0.
More generally, by computing τ i,j for all i, j ∈ {-1, 0, 1}, we obtain the automaton below; the initializers (left hand side of the Lustre operator →) define the initial state q 0 .

q 0 q -1 q 1 d ≥ 0 d ≤ 0 d > 0 d < 0 d = 0 d = 0 d < 0 d > 0
Note that the resulting automaton is nondeterministic: in state q 1 (respectively, q -1 ), representing o > 0 (resp. o < 0), if d = 0, then one can either remain in the same state or return to the initial state q 0 .

Related Work

There have been many approaches proposed for finding invariants and proving properties on transition systems. [START_REF] Shankar | Symbolic analysis of transition systems[END_REF] surveys earlier ones.

The problem of finding the control structure of reactive nodes written in e.g. Lustre has been studied previously, most notably by B. Jeannet [START_REF] Jeannet | Partitionnement dynamique dans l'analyse de relations linéaires et application à la vérification de programmes synchrones[END_REF][START_REF] Jeannet | Dynamic partitioning in linear relation analysis: Application to the verification of reactive systems[END_REF][START_REF] Jeannet | Dynamic partitioning in analyses of numerical properties[END_REF], but with respect to a property to prove: the control structure is gradually refined until the property becomes provable. This supposes that we know the desired property in advance, which is not always the case in a modular setting: the property may pertain to another module, and may not be easy to propagate back to the current module. The NBac tool performs such an analysis using convex polyhedra as an abstract domain. More recent methods for refining the control structure of reactive nodes include [START_REF] Balakrishnan | Refining the control structure of loops using static analysis[END_REF]. We have already proposed some modular abstractions for reactive nodes, but these targeted specific filters with no control structure [START_REF] Monniaux | Compositional analysis of floating-point linear numerical filters[END_REF] or needed some precomputation of the control structure [START_REF] Monniaux | Automatic modular abstractions for template numerical constraints[END_REF].

The problem of finding disjunctive invariants has been much studied especially in the context of convex numerical domains, such as polyhedra: if the property to prove is not convex, or relies on a non-convex weakest precondition, then any analysis inferring convex invariants will fail. A number of methods have been proposed to infer invariants consisting in finite disjunctions of elements of an abstract domain: some distinguish states according to the history of the computation, as in trace partitioning [START_REF] Rival | The trace partitioning abstract domain[END_REF], some recombine elements according to some affinity heuristics [START_REF] Sriram Sankaranarayanan | Static analysis in disjunctive numerical domains[END_REF][START_REF] Popeea | Inferring disjunctive postconditions[END_REF], or decompose the transition relation according to some "convexity witness" [START_REF] Gulwani | The reachability-bound problem[END_REF]. Other methods select predicates with which to split the control state [START_REF] Sharma | Simplifying loop invariant generation using splitter predicates[END_REF]. Some recent methods leverage the power of modern SMT-solvers to impose convex invariants only at a limited subset of program points, and distinguish all execution paths between them, therefore acting as applying a complete trace partitioning between the points in the distinguished subset [START_REF] Monniaux | Automatic modular abstractions for template numerical constraints[END_REF][START_REF] Gawlitza | Improving strategies via SMT solving[END_REF]; the method in the present article also considers a limited subset of program points (e.g. loop heads), but can infer disjunctive invariants at these points too.

Both polyhedral abstraction and predicate abstraction search for an inductive invariant I; then, in order to prove that a certain property P always holds, one shows that I is included in P . In all static analyzers by abstract interpretation known to the authors, some form of forward analysis is used: the set of initial states influences the invariant I obtained by the system. In contrast, with k-induction, as in the Kind tool [START_REF] Hagen | Scaling up the formal verification of Lustre programs with SMT-based techniques[END_REF] the initial states play a very limited role (essentially, they invalidate P if there exists a trace of k states starting in an initial state such that one of them does not satisfy P ). A known weakness of pure k-induction is that it may fail to prove a property because it bothers about bad, but unreachable, states. If one has obtained an invariant I by other methods, one can use it to constrain the system and get rid of these bad, unreachable states. Thus, abstraction-based methods and k-induction based methods nicely combine.

The algorithms presented in this article can be seen as a form of minimization constrained by a universally quantified formula ∀σ F , achieved by maintaining a formula H such that ∀σ F ⇒ H, H being a conjunction of an increasingly large number of constraints generated from F "on demand": a constraint is added only if it is violated by the current candidate solution. This resembles quantifier elimination algorithms we have proposed for linear real arithmetic [START_REF] Monniaux | Quantifier elimination by lazy model enumeration[END_REF]; one difference is that the termination argument is simpler: with a finite number n of Booleans as free variables, a new added constraint suppresses at least one of the 2 n models, thus there can be at most 2 n iterations; in comparison the termination arguments for arithmetic involve counting projections of polyhedra.

Reductions from invariant inferences to quantifier elimination, or to minimization constrained by a universally quantified formula, have already been proposed for numerical constraints, where the unknowns are numerical quanti-ties, in contrast to the present work where they are Booleans [START_REF] Monniaux | Automatic modular abstractions for template numerical constraints[END_REF].

Reductions from loop invariant inference in predicate abstraction to Boolean constraint solving were introduced in [START_REF] Gulwani | Constraint-based invariant inference over predicate abstraction[END_REF], but that work assumed a postcondition to prove, as opposed to minimizing the result. The problem we solve is the same as the one from the later work [START_REF] Srivastava | Program verification using templates over predicate abstraction[END_REF]Sec. 5], but instead of concretely enumerating the (potentially exponential) set of paths inside the program (corresponding to all disjuncts in a disjunctive normal form of the transition relation), each path corresponding to one constraint, we lazily enumerate witnesses for such paths. Unfortunately, we do not have an implementation of the algorithm from [START_REF] Srivastava | Program verification using templates over predicate abstraction[END_REF] at our disposal for performance comparisons.

More generally, a number of approaches for invariant inference based on constraint solving have been proposed in the last years, especially for reducing numerical invariant inference to numerical constraint solving [START_REF] Gulwani | Program analysis as constraint solving[END_REF][START_REF] Michael Colón | Linear invariant generation using non-linear constraint solving[END_REF] or mathematical programming [START_REF] Goubault | Static analysis by abstract interpretation: A mathematical programming approach[END_REF]. One difference between these constraint approaches and ours, except that our variable are Boolean and theirs are real, is that we use a lazy constraint generation scheme: we generate constraints only when a candidate solution violates them, a method long known in mathematical programming when applying cuts. We applied a similar technique for quantifier elimination for linear real arithmetic, using lazy conversions to conjunctive normal form [START_REF] Monniaux | Quantifier elimination by lazy model enumeration[END_REF]. A recent max-policy iteration considers each path through the loop as a constraint, and lazily selects a combination of paths, using SMTsolving to point the next relevant path [START_REF] Gawlitza | Improving strategies via SMT solving[END_REF].

Conclusion

We have given algorithms for finding loop invariants, or, equivalently, invariants for reactive nodes, given as templates with Boolean parameters. Using disjunctive invariants for reactive nodes, one obtains an abstraction of the reactive node as a finite automaton with transitions labeled with guards over node inputs.

If a system consists of a number of nodes, then some of these nodes may be replaced by their abstract automaton, resulting in a more abstract system whose behaviors include all behaviors of the original system. This new system can in turn be analyzed by the same method. Thus, our method supports modular and compositional analysis.

We provide the Candle tool, built using the Yices SMT-solver and the Mjollnir quantifier elimination procedure, which computes abstractions of Lustre nodes.

7 =

 7 false, B

  node c l i c k e r ( d i r : i n t ) returns ( o u t : i n t ) ; l e t o u t = i f d i r ≥ 1 then d i r e l s e i f d i r ≤ -1 then d i r e l s e 0 → i f pre o u t ≤ -1 then ( pre o u t ) + 1 e l s e i f pre o u t ≥ 1 then ( pre o u t ) -1 e l s e 0 ; t e l . In mathematical notation, let us denote dir by d, pre out by o and out by o ′ . The state consists in a single variable o, thus σ is the same as o. The transition relation then becomes

  such a universally quantified constraint can be handled as explained in Sec. 2.2.

2. ∃σ T [B ′ /b] ∧ ¬T [B/b]. Again, as explained in Sec. 2.3.2, one can treat such an existentially quantified constraint by using a SMT-solver instead of a SAT-solver and adding to H an extra variable σ and the constraint

These variables are not necessarily scalar variables. It is for instance possible to consider uninterpreted functions from the integers to the integers, which stand for a countably infinite number of integers.

This work was partially supported by ANR project "ASOPT". † CNRS / VERIMAG


Maxime Crochemore

Pattern Matching in Strings

Introduction

The present chapter describes a few standard algorithms used for processing texts. They apply, for example, to the manipulation of texts (text editors), to the storage of textual data (text compression), and to data retrieval systems. The algorithms of the chapter are interesting in di erent respects. First, they are basic components used in the implementations of practical software. Second, they introduce programming methods that serve as paradigms in other elds of computer science (system or software design). Third, they play an important role in theoretical computer science by providing challenging problems.

Although data are stored variously, text remains the main form of exchanging information. This is particularly evident in literature or linguistics where data are composed of huge corpora and dictionaries. This applies as well to computer science where a large amount of data are stored in linear les. And this is also the case in molecular biology where biological molecules can often be approximated as sequences of nucleotides or amino-acids. Moreover, the quantity of available data in these elds tends to double every eighteen months. This is the reason why algorithms should be e cient even if the speed of computers increases regularly.

The manipulation of texts involves several problems among which are: pattern matching, approximate pattern matching, comparing strings, and text compression. The rst problem is partially treated in the present chapter, in that we consider only one-dimensional objects. Extensions of the methods to higher dimensional objects and solutions to the second problem appear in the chapter headed \Generalized Pattern Matching". The third problem includes the comparison of molecular sequences, and is developed in the corresponding chapter. Finally, an entire chapter is devoted to text compression.

Pattern matching is the problem of locating a collection of objects (the pattern) inside raw text. In this chapter, texts and elements of patterns are strings, which are nite sequences of symbols over a nite alphabet. Methods for searching patterns described by general regular expressions derive from standard parsing techniques (see the chapter on formal grammars and languages). We focus our attention to the case where the pattern represents a nite set of strings. Although the latter case is a specialization of the former case, it can be solved with more e cient algorithms.

Solutions to pattern matching in strings divide in two families. In the rst one, the pattern is xed. This situation occurs for example in text editors for the \search" and \substitute" commands, and in telecommunications for checking tokens. In the second family of solutions, the text is considered as xed while the pattern is variable. This applies to dictionaries and to full-text data bases, for example.

The e ciency of algorithms is evaluated by their worst-case running times and the amount of memory space they require.

The alphabet, the nite set of symbols, is denoted by , and the whole set of strings over by . The length of a string u is denoted by juj; it is the length of the underlying nite sequence of symbols. The concatenation of two strings u and v is denoted by uv. A string v is said to be a factor (or a segment) of a string u if u can be written in the from u 0 vu 00 where u 0 ; u 00 2 ; if i = ju 0 j and j = ju 0 vj 1, we say that the factor v starts at position i and ends 1 at position j in u; the factor v is also denoted by u i : :j]. The symbol at position i in u, that is the i + 1-th symbol of u, is denoted by u i].

Matching Fixed Patterns

We consider in this section the two cases where the pattern represents a xed string or a xed dictionary (a nite set of strings). Algorithms search for and locate all the occurrences of the pattern in any text.

In the string-matching problem, the rst case, it is convenient to consider that the text is examined through a window. The window delimits a factor of the text and has usually the length of the pattern. It slides along the text from left to right. During the search, it is periodically shifted according to rules that are speci c to each algorithm. When the window is at a certain position on the text, the algorithm checks whether the pattern occurs there or not, by comparing some symbols in the window with the corresponding aligned symbols of the pattern; if there is a whole match, the position is reported. During this scan operation, the algorithm acquires from the text information which are often used to determine the length of the next shift of the window. Some part of the gathered information can also be memorized in order to save time during the next scan operation.

In the dictionary-matching problem, the second case, methods are based on the use of automata, or related data structures.

The Brute Force Algorithm

The simplest implementation of the sliding window mechanism is the brute force algorithm. The strategy consists here in sliding uniformly the window one position to the right after each scan operation. As far as scans are correctly implemented, this obviously leads to a correct algorithm.

We give below the pseudocode of the corresponding procedure. The inputs are a nonempty string x, its length m (thus m > 1), a string y, and its length n. The variable p in the procedure corresponds to the current left position of the window on the text. It is understood that the string-to-string comparison in line 2 has to be processed symbol per symbol according to a given order.

Brute-Force-Matcher(x; m; y; n) 1 for p from 0 up to n m 2 loop if y p : :p + m 1] = x 3 then report p The time complexity of the brute force algorithm is O(m n) in the worst case (for instance when a m 1 b is searched in a n for any two symbol a; b 2 satisfying a 6 = b if we assume that the rightmost symbol in the window is compared last). But its behavior is linear in n when searching in random texts.

The Karp-Rabin Algorithm

Hashing provides a simple method for avoiding a quadratic number of symbol comparisons in most practical situations. Instead of checking at each position p of the window on the text whether the pattern occurs here or not, it seems to be more e cient to check only if the factor of the text delimited by the window, namely y p : :p + m 1], \looks like" x. In order to check the resemblance between the two strings, a hash function is used. But, to be helpful for the string-matching problem, the hash function should be highly discriminating for strings. According to the running times of the algorithms, the function should also have the following properties:

to be e ciently computable; to provide an easy computation of the value associated with the next factor from the value associated with the current factor. The last point is met when symbols of alphabet are assimilated with integers and when the hash function, say h, is de ned for each string u 2 by

h(u) = 0 @ juj 1 X i=0 u i] d juj 1 i 1 A mod q;
where q and d are two constants. Then, for each string v 2 , for each symbols a 0 ; a 00 2 , h(va 00 ) is computed from h(a 0 v) by the formula h(va 00 ) = ((h(a 0 v) a 0 d jvj ) d + a 00 ) mod q: During the search for pattern x, it is enough to compare the value h(x) with the hash value associated with each factor of length m of text y. If the two values are equal, that is, in case of collision, it is still necessary to check whether the factor is equal to x or not by symbol comparisons.

The underlying string-matching algorithm, which is denoted as the Karp-Rabin algorithm, is implemented below as the procedure Karp-Rabin-Matcher. In the procedure, the values d m 1 mod q, h(x), and h(y 0 : :m 2]) are rst precomputed, and stored respectively in the variables r, s, and t (lines 1{7). The value of t is then recomputed at each step of the search phase (lines 8{12). It is assumed that the value of symbols ranges from 0 to c 1; the quantity (c 1) q is added in line 8 to provide correct computations on positive integers. Karp-Rabin-Matcher(x; m; y; n) 1 r 1 2 s x 0] mod q 3 t 0 4 for i from 1 up to m 1 5 loop r (r d) mod q 6 s (s d + x i]) mod q 7 t (t d + y i 1]) mod q 8 for p from 0 up to n m 9 loop t (t d + y p + m 1]) mod q 10 if t = s and y p : :p + m 1] = x 11 then report p 12 t ((c 1) q + t y p] r) mod q Convenient values for d are powers of 2; in this case, all the products by d can be computed as shifts on integers. The value of q is generally a large prime (such that the quantities (q 1) d + c 1 and c q 1 do not cause over ows), but it can also be the value of the implicit modulus supported by integer operations. An illustration of the behavior of the algorithm is given in Figure 1. The worst case complexity of the above string-matching algorithm is quadratic, as it is for the brute force algorithm, but its expected running time is O(m + n) if parameters q and d are adequate.

The Knuth-Morris-Pratt Algorithm

This section presents the rst discovered linear-time string-matching algorithm. Its design follows a tight analysis of a version of the brute force algorithm in which the string-to-string comparison proceeds from left to right. The brute force algorithm wastes the information gathered during the scan of the text. On the contrary, the Knuth-Morris-Pratt algorithm stores the information with two purposes. First, it is used to improve the length of shifts. Second, there is no backward scan of the text.

Consider a given position p of the window on the text. Assume that a mismatch occurs between symbols y p + i] and x i] for some i, 0 6 i < m (an illustration is given in Figure 2). Thus, we have y p : :p + i 1] = x 0 : :i 1] and y p + i] 6 = x i]. With regard to the information given by x 0 : :i 1], interesting shifts are necessarily connected with the borders of x 0 : :i 1]. (A border of a string u is a factor of u that is both a pre x and a su x of u). Among the borders of x 0 : :i 1], the longest proper border followed by a symbol di erent from x i] is the best possible candidate, subject to the existence of such of a border. (A factor v of a string u is said to be a proper factor of u if u and v are not identical, that is, if jvj < juj.) This introduces the function de ned for each i 2 f0; 1; : : :; m 1g by i] = maxfk j (0 6 k < i; x i k : :i 1] = x 0 : :k 1]; x k] 6 = x i]) or (k = 1)g: Then, after a shift of length i i], the symbol comparisons can resume with y p + i] against x i]] in the case where i] > 0, and y p + i + 1] against x 0] otherwise. Doing so, we miss no occurrence of x in y, and avoid a backtrack on the text. The previous statement is still valid when no mismatch occurs, that is when i = m, if we consider for a moment the string x$ instead of x, where $ is a symbol of alphabet occurring nowhere in x. This amounts to completing the de nition of function by setting m] = maxfk j 0 6 k < m; x m k : :m 1] = x 0 : :k 1]g:

The Knuth-Morris-Pratt string-matching algorithm is given in pseudocode below as the procedure Knuth-Morris-Pratt-Matcher. The values of function are rst computed by the function Better-Prefix-Function given after. The value of the variable j is equal to p + i in the remainder of the code (the search phase of the algorithm strictly speaking); this simpli es the code, and points out the sequential processing of the text. Observe that the preprocessing phase applies a similar method to the pattern itself, as if y = x 1 : :m 1]. The current shift is the consequence of an analysis of the list of the proper borders of x 0 : :9] and of the symbol which follow them in x. The pre xes of x that are borders of x 0 : :9] = abcabacbab are right-aligned along the discontinuous vertical line. String x 0 : :4] = abcab is a border of x 0 : :9], but is followed by symbol a which is identical to x 10]. String x 0 : :1] is the expected border, since it is followed by symbol c. (c) The values of the function for pattern x.

Knuth-Morris-Pratt-Matcher(x; m; y; n) 1 Better-Prefix-Function(x; m) 2 i 0 3 for j from 0 up to n 1 4 loop while i > 0 and y j] 6 = x i]

5 loop i i] 6 i i + 1 7 if i = m 8 then report j + 1 m 9 i m]
Better-Prefix-Function(x; m)

1 0] 1 2 i 0 3 for j from 1 up to m 1 4 loop if x j] = x i] 5 then j] i] 6 else j] i 7 loop i i]
8 while i > 0 and x j] 6 = x i]

9 i i + 1 10 m] i 11 return
The algorithm has a worst-case running time in O(m + n), and requires O(m) extra-space to store function . The linear running time results from the fact that the number of symbol comparisons performed during the preprocessing phase and the search phase is less than 2m and 2n respectively. All the previous bounds are independent of the size of the alphabet.

The Boyer-Moore Algorithm

The Boyer-Moore algorithm is considered as the most e cient string-matching algorithm in usual applications. A simpli ed version of it, or the entire algorithm, is often implemented in text editors for the \search" and \substitute" commands.

The scan operation proceeds from right to left in the window on the text, instead of left to right as in the Knuth-Morris-Pratt algorithm. In case of a mismatch, the algorithm uses two functions to shift the window. These two shift functions are called the better-factor shift function and the bad-symbol shift function. In the two next paragraphs, we explain the goal of the two functions and we give procedures to precompute their values.

We rst explain the aim of the better-factor shift function. Let p be the current (left) position of the window on the text. Assume that a mismatch occurs between symbols y p + i] and x i] for some i, 0 6 i < m (an illustration is given in Figure 3). Then, we have y p+i] 6 = x i] and y p + i + 1 : :p + m 1] = x i + 1 : :m 1]. The better-factor shift consists in aligning the factor y p+i+1 : :p+m 1] with its rightmost occurrence x k +1 : :m 1 i+k] in x preceded by a symbol x k] di erent from x i] to avoid an immediate mismatch. If no such factor exists, the shift consists in aligning the longest su x of y p + i + 1 : :p + m 1] with a matching pre x of x. The better-factor shift function is de ned by i] = minfi k j (0 6 k < i; x k + 1 : : Better-Factor-Function(x; m) 1 for j from 0 up to m 1 2 loop j] 0 3 i m 4 for j from m 1 down to 0 5 loop f j] i + 1 6 while i < m and x j] 6 = x i]

m 1 i + k] = x i + 1 : :m 1]; x k] 6 = x i]) or (i m 6 k < 0; x = x i k : : m 1]x m i + k : : m 1])g
7 loop if i] = 0 8 then i] i j 9 i f i] 1 10 i i 1 11 for j from 0 up to m 1 12 loop if j] = 0 13 then j] i + 1 14 if j = i 15 then i f i] 1 16 return
We now come to the aim of the bad-symbol shift function (Figure 4 shows an illustration).

Consider again the text symbol y p + i] that causes a mismatch. Assume rst that this symbol occurs in x 0 : :m 2]. Then, let k be the position of the rightmost occurrence of y p + i] in x 0 : :m 2]. The window can be shifted i k positions to the right if k < i, and only one position otherwise, without missing an occurrence of x in y. Assume now that symbol y p + i] does not occur in x. Then, no occurrence of x in y can overlap the position p + i on the text, and thus, the window can be shifted i + 1 positions to the right. Let ! be the table indexed on alphabet , and de ned for each symbol a 2 by ! a] = minfmg fm 1 j j 0 6 j < m 1; x j] = ag:

According to the above discussion, the bad-symbol shift for the unexpected text symbol a aligned with the symbol at position i on the pattern is the value a; i] = maxf! a] + i m + 1; 1g; which de nes the bad-symbol shift function on f0; 1; : : :; m 1g. We give now the code of the function Last-Occurrence-Function that computes table !. Its running time is O(m + card ).

Last-Occurrence-Function(x; m) 1 for each a 2 2 loop ! a] m 3 for j from 0 up to m 2 4 loop ! x j]] m 1 j 5 return !

The shift applied in the Boyer-Moore algorithm in case of a mismatch is the maximum between the better-factor shift and the bad-symbol shift. In case of a whole match, the shift applied to the window is m minus the length of the longest proper border of x, that is also the value 0] (this value is indeed what is called \the period" of the pattern). The code of the entire algorithm is given below. The worst-case running time of the algorithm is quadratic. It is surprising however that, when used to search only for the rst occurrence of the pattern, the algorithm runs in linear time. Slight modi cations of the strategy yield linear-time algorithms. When searching for a m 1 b in a n with a; b 2 and a 6 = b, the algorithm considers only bn=mc symbols of the text. This bound is the absolute minimum for any string-matching algorithm in the model where the pattern only is preprocessed. Indeed, the algorithm is expected to be extremely fast on large alphabets (relative to the length of the pattern).

Practical String-Matching Algorithms

The bad-symbol shift function introduced in the Boyer-Moore algorithm is not very e cient for small alphabets, but when the alphabet is large compared with the length of the pattern (as it is often the case with the ASCII table and ordinary searches made under a text editor), it becomes very useful. Using only the corresponding table produces some e cient algorithms for practical searches. We describe one of these algorithms below.

Consider a position p of the window on the text, and assume that the symbols y p + m 1] and x m 1] are identical. If x m 1] does not occur in the pre x x 0 : :m 2] of x, the window can be shifted m positions to the right after the string-to-string comparison between y p : :p+m 2] and x 0 : :m 2] is performed. Otherwise, let k be the position of the rightmost occurrence of x m 1] in x 0 : :m 2]; the window can be shifted m 1 k positions to the right. This shows that ! y p + m 1]] is also a valid shift in the case where y p + m 1] = x m 1].

The underlying algorithm is the Horspool algorithm.

The pseudocode of the Horspool algorithm is given below. To prevent two references to the rightmost symbol in the window at each scan and shift operation, table ! is slightly modi ed: ! x m 1]] contains the sentinel value 0, after its previous value is saved in variable t. The value of the variable j is the value of the expression p + m 1 in the discussion above.

Horspool-Matcher(x; m; y Just like the brute force algorithm, the Horspool algorithm has a quadratic worst-case time complexity. But its behavior in practice is at least as good as the behavior of the Boyer-Moore algorithm is. An example showing the behavior of both algorithms is given in Figure 5.

; n) 1 ! Last-Occurrence-Function(x; m) 2 t ! x m 1]] 3 ! x m 1]] 0 4 j m 1 5 while j < n 6 loop s ! y j]]

The Aho-Corasick Algorithm

The UNIX operating system provides standard text-le facilities. Among them is the series of grep commands that locate patterns in les. We describe in this section the Aho-Corasick algorithm underlying an implementation of the fgrep command of UNIX. It searches les for a nite and xed set of strings (the dictionary), and can for instance output lines containing at least one of the strings.

If we are interested in searching for all occurrences of all strings of a dictionary, a rst solution consists in repeating some string-matching algorithm for each string. Considering a dictionary X containing k strings and a text y, the search runs in that case in time O(m+n k), where m is the sum of the length of the strings in X, and n the length of y. But this solution is not e cient, since text y has to be read k times. The solution described in this section provides both a sequential read of the text and a total running time which is O(m + n) on a xed alphabet. The algorithm can be viewed as a direct extension of weaker version of the Knuth-Morris-Pratt algorithm.

The search is done with the help of an automaton that stores the situations encountered during the process. At a given position on the text, the current state is identi ed with the set of pattern pre xes ending here. The state represents all the factors of the pattern that can possibly lead to occurrences. Among the factors, the longest contains all the information necessary to continue the search. So, the search is realized with an automaton, denoted by The rst and second shifts result from the better-shift function, the third and fourth from the bad-symbol function, and the fth from a shift of the length of x minus the length of its longest proper border (the period of x). (b) Behavior of the Horspool algorithm. We assume here that the four leftmost symbols in the window are compared with the symbols of x 0 : : 3] from left to right. D(X), of which states are in one-to-one correspondence with the pre xes of X. Implementing completely the transition function of D(X) would required a size O(m card ). Instead of that, the Aho-Corasick algorithm requires only O(m) space. To get this space complexity, a part of the transition function is made explicit in the data, and the other part is computed with the help of a failure function. For the rst part, we assume that for any input (p; a), the function denoted by Target returns some state q if the triple (p; a; q) is an edge in the data, and the value nil otherwise. The second part uses the failure function fail, which is an analogue of the function used in the Knuth-Morris-Pratt algorithm. But this time, the function is de ned on the set of states, and for each state p di erent from the initial state, fail p] = the state identi ed with the longest proper su x of the pre x identi ed with p that is also a pre x of a string of X:

The aim the failure function is to defer the computation of a transition from the current state, say p, to the computation of the transition from the state fail p] with the same input symbol, say a, when no edge from p labeled by symbol a is in the data; the initial state, which is identi ed with the empty string, is the default state for the statement. We give below the pseudocode of the function Next-State that computes the transitions in the representation.

The initial state is denoted by i. Figure 6 The trie-like automaton of the pattern X = face; as; easeg. The initial state is distinguished by a thick ingoing arrow, each terminal state by a thick outgoing arrow. The states are numbered from 0 to 8, according to the order in which they are created by the construction statement described in the present section. State 0 is identi ed with the empty string, state 1 with a, state 2 with ac, state 3 with ace, and so on. The automaton accepts the language X .

Next-State(p; a; i)

1 while p 6 = nil and Target(p; a) = nil 2 loop p fail p] 3 if p 6 = nil 4 then q Target(p; a) 5 else q i 6 return q The preprocessing phase of the Aho-Corasick algorithm builds the explicit part of D(X) including function fail. It is divided itself into two phases.

The rst phase of the preprocessing phase consists in building a sub-automaton of D(X). It is the trie of X (the digital tree in which branches spell the strings of X and edges are labeled by symbols) having as initial state the root of the trie and as terminal states the nodes corresponding to strings of X (an example is given in Figure 6). It di ers from D(X) in two points:

it contains only the forward edges; it accepts only the set X . (An edge (p; a; q) in the automaton is said to be forward if the pre x identi ed with q is in the form ua where u is the pre x corresponding to p.) The function given below as the function Trie-Like-Automaton computes the automaton corresponding to the trie of X by returning its initial state. The terminal mark of each state r is managed through the attribute terminal r]; the mark is either true or false depending on whether state r is terminal or not. We assume that the function New-State creates and returns a new state, and that the procedure Make-Edge adds a given new edge to the data. to store the data and to implement the queue used during the breadth-rst traversal executed in procedure Make-Failure-Function.

Let us discuss the question of reporting occurrences of pattern X (line 7 of procedure Aho-Corasick-Matcher). The simplest way of doing it is to report the ending positions of occurrences. This remains to output the value of the position of the current symbol in the text.

A second possibility is to report the whole set of strings in X ending at the current position.

To do so, the attribute terminal has to be transformed. First, for a state r, terminal r] is the set of the string of X that are su xes of the string corresponding to r. Second, to avoid a quadratic behavior, sets are manipulated by their identi ers only.

Indexing Texts

This section deals with the pattern-matching problem applied to xed texts. Solutions consist in building an index on the text that speeds up further searches. The indexes that we consider here are data structures that contain all the su xes and therefore all the factors of the text. Two types of structures are presented: su x trees and su x automata. They are both compact representations of su xes in the sense that their sizes are linear in the length of the text, although the sum of lengths of su xes of a string is quadratic. Moreover, their constructions take linear time on xed alphabets. On an arbitrary nite alphabet , assumed to be ordered, a log card factor has to be added to almost all running times given in the following. This corresponds to the branching operation involved in the respective data structures. Indexes are powerful tools that have many applications. Here is a non-exhaustive list of them, assuming an index on the text y.

Membership: testing if a string x occurs in y.

Occurrence number: producing the number of occurrences of a string x in y. The su x tree T (y) of the string y = aabbabb$. The nodes are numbered from 0 to 12, according to the order in which they are created by the construction algorithm described in the present section. Each of the eight external nodes of the trie is marked by the position of the occurrence of the corresponding su x in y. Hence, the branch (0; 5; 9; 4), running from the root to an external node, spells the string bbabb$, which is the su x of y starting at position 2.

List of positions: analogue of the string-matching problem of Section 2.

Longest repeated factor: locating the longest factor of y occurring at least twice in y.

Longest common factor: nding a longest string that occurs both in a string x and in y.

Solutions to some of these problems are rst considered with su x trees, then with su x automata.

Su x Trees

The su x tree T (y) of a nonempty string y of length n is a data structure containing all the su xes of y. In order to simplify the statement, it is assumed that y ends with a special symbol of the alphabet occurring nowhere else in y (this special symbol is denoted by $ in the examples). The su x tree of y is a trie which satis es the following properties: the branches from the root to the external nodes spell the nonempty su xes of y, and each external node is marked by the position of the occurrence of the corresponding su x in y; the internal nodes have at least two successors, except if y is a one-length string;

the edges outgoing an internal node are labeled by factors starting with di erent symbols; any string that labels an edge is represented by the couple of integers corresponding to its position in y and its length. (An example of su x tree is displayed in Figure 8.) The special symbol at the end of y avoids marking nodes, and implies that T (y) has exactly n external nodes. The other properties then imply that the total size of T (y) is O(n), which makes it possible to design a linear-time construction of the data structure. The algorithm described in the following and implemented by the procedure Suffix-Tree given further has this time complexity.

The construction algorithm works as follows. It inserts the nonempty su xes y i : : n 1], 0 6 i < n, of y in the data structure from the longest to the shortest su x. In order to explain how this is performed, we introduce the two notations h i = the longest pre x of y i : : n 1] that is a pre x of some stricly longest su x of y; and t i = the string w such that y i : : n 1] is identical with h i w, de ned for each i 2 f1; : : : ; n 1g. The strategy to insert the su xes is precisely based on these de nitions. Initially, the data structure contains only the string y. Then, the insertion of the string y i : : n 1], 1 6 i < n, proceeds in two steps: rst, the \head" in the data structure, that is, the node h corresponding to string h i , is located, possibly breaking an edge; second, a node called the \tail", say t, is created, added as successor of node h, and the edge from h to t is labeled with string t i . The second step of the insertion is clearly performed in constant time. Thus, nding the head is critical for the overall performance of the construction algorithm. A brute-force method to nd the head consists in spelling the current su x y i : : n 1] from the root of the trie, giving an O(jh i j) time complexity for the insertion at step i, and an O(n 2 ) running time to build the su x tree T (y). Adding \short-circuit" links leads to an overall O(n) time complexity, although there is no guarantee that the insertion at any step i is realized in constant time.

Observe that in any su x tree, if the string corresponding to a given internal node p in the data structure is in the form au with a 2 and u 2 , then there exists an unique internal node corresponding to the string u. From this remark are de ned the su x links by link p] = the node q corresponding to the string u when p corresponds to the string au for some symbol a 2

for each internal node p that is di erent from the root. The links are useful when computing h i from h i 1 because of the property: if h i 1 is in the form aw for some symbol a 2 and some string w 2 , then w is a pre x of h i .

We explain in three following paragraphs how the su x links help to nd the successive heads e ciently. We consider a step i in the algorithm assuming that i > 1. We denote by g the node that corresponds to the string h i 1 . The aim is both to insert y i : : n 1] and to nd the node h corresponding to the string h i . We rst study the most general case of the insertion of the su x y i : : n 1]. Particular cases are studied after. We assume in the present case that the predecessor of g in the data structure, say g 0 , is both de ned and di erent from the root. Then h i 1 is in the form auv where a 2 , u; v 2 , au corresponds to the node g 0 , and v labels the edge from g 0 to g. Since the string uv is a pre x of h i , it can be fully spelled from the root. Moreover, the spelling operation of uv from the root can be short-circuited by spelling only the string v from the node link g 0 ]. The node q reached at the end of the spelling operation (possibly breaking the last partially taken down edge) is then exactly the node link g]. It remains to spell the string t i 1 from q for completely inserting the string y i : : n 1]. The spelling stops on the expected node h (possibly breaking again an edge) which becomes the new head in the data structure. The su x of t i 1 that has not been spelled so far, is exactly the string t i . (An example for the whole previous statement is given in Figure 9.) Figure 9 During the construction of the su x tree T (y) of the string y = aabbabb$, the step 5, that is, the insertion of the su x bb$. The de ned su x link are depicted with discontinuous non-labeled directed edges. (a) Initially, the head in the data structure is node 7, and its su x link is not yet de ned. The predecessor of node 7, node 2, is di erent from the root, and the factor of y that is spelled from the root to node 7, namely h 4 = abb, is in the form auv, where a 2 , u 2 , and v is the string of labeling the edge from node 2 to node 7. Here, a = a, u is the empty string, and v = bb. Then, the string uv = bb is spelled from the node linked with node 2, that is, from node 0; the spelling operation stops on the edge from node 5 to node 4; this edge is broken, which creates node 9. Node 9 is linked to node 7. The string t 4 = $ is spelled from node 9; the spelling operation stops on node 9, which becomes the new head in the data structure. (b) Node 10 is created, added as successor of node 9, and the edge from node 9 to node 10 is labeled by the string $, remainder of the last spelling operation.

The second case is when g is a (direct) successor of the root. The string h i 1 is then in the form au where a 2 and u 2 . Similarly to the above case, the string u can be fully spelled from the root. The spelling of u gives a node q, which is then linked with g. Afterwards, the string t i 1 is spelled from q.

The last case is when g is the root itself. The string t i 1 minus its rst symbol has to be spelled from the root. Which ends the study of all the possible cases that can arise.

The important aspect of the algorithm is the use of two di erent implementations for the two spelling operations pointed out above. The rst one, given in the pseudocode below as the function Fast-Find, deals with the situation where we know in advance that a given factor y j : : j + k 1] of y can be fully spelled from a given node p of the trie. It is then su cient to scan only the rst symbols of the labels of the encountered nodes, which justi es the name of the function. The second implementation of the spelling operation spells a factor y j : : j +k 1] of y from a given node p too, but, this time, the spelling is performed symbol by symbol. The corresponding function is implemented after as the function Slow-Find. Before giving the pseudocode of the functions, we precise the notations used in the following.

For any input (y; p; j ), the function Successor-By-One-Symbol returns the node q such that q is a successor of the node p and the rst symbol of the label of the edge from p to q is y j ]; if such a node q does not exist, it returns nil.

For any input (p; q), the function Label returns the two integers that represents the label of the edge from the node p to the node q.

The function New-Node creates and returns a new node.

For any input (p; j; k; q; `), the function New-Breaking-Node creates and returns the node r breaking the edge (p; y j : : j +k 1]; q) at the position `in the label y j : : j +k 1].

(Which gives the two edges (p; y j : : j + ` 1]; r) and (r; y j + `: : j + k 1]; q).) Function Fast-Find returns a couple of nodes such that the second one is the node reached by the spelling, and the rst one is its predecessor.

Fast-Find(y; p; j; k) 1 p 0 nil 2 while k > 0 3 loop p 0 p 4 q Successor-By-One-Symbol(y; p; j ) 5 (r; s) Label(p; q) 6 if s 6 k 7 then p q 8 j j + s 9 k k s 10 else p New-Breaking-Node(p; r; s; q; k) 11 k 0 12 return (p 0 ; p) Compared to function Fast-Find, function Slow-Find considers an extra-input that is the predecessor of node p (denoted by p 0 ). It considers in addition two extra-outputs that are the position and the length of the factor that remains to be spelled.

Slow-Find(y; p 0 ; p; j; k) 1 b false 2 loop q Successor-By-One-Symbol(y; p; j ) 3 if q = nil 4 then b true 5 else (r; s) Label(p; q) 6 ` 1 7 while `< s and y j + `] = y r + `] 8 loop ` `+ 1 9 The complete construction algorithm is implemented as the function Suffix-Tree given below. The function returns the root of the constructed su x-tree. Memorizing systematically the predecessors h 0 and q 0 of the nodes h and q avoids considering doubly linked tries. The name of the attribute which marks the positions of the external nodes is made explicit. The su x automaton S(y) of the string y = aabbabb. The states are numbered from 0 to 10, according to the order in which they are created by the construction algorithm described in the present section. The initial state is state 0, terminal states are states 0, 5, 9, and 10. This automaton is the minimal deterministic automaton accepting the language of the su xes of y.

automata recognizing the same language, which implies that it is not necessarily complete. An example is given in Figure 10.

The main point about su x automata is that their size is asymptotically linear in the length of the string. More precisely, given a string y of length n, the number of states of S(y) is equal to n + 1 when n 6 2, and is bounded by n + 1 and 2n 1 otherwise; as to the number of edges, it is equal to n + 1 when n 6 1, it is 2 or 3 when n = 2, and it bounded by n and 3n 4

otherwise.

The construction of the su x automaton of a string y of length n can be performed in time O(n), or, more precisely, in time O(n log card ) on an arbitrary alphabet . It makes use of a failure function fail de nes on the states of S(y). The set of states of S(y) identi es with the quotient sets u 1 Su (y) = fv 2 j uv 2 Su (y)g for the strings u in the whole set of factors of y. One may observe that two sets in the form u 1 Su (y) are either disjoint or comparable. This allows to set fail p] = the smallest quotient set stricly containing the quotient set identi ed with p; for each state p of the automaton di erent from the initial state of the automaton. The function given below as the function Suffix-Automaton builds the su x automaton of y, and returns the initial state, say i, of the automaton. The construction is on-line, which means that at each step of the construction, just after processing a pre x y 0 of y, the su x automaton S(y 0 ) is build. Denoting by t the state without outgoing edge in the automaton S(y 0 ), terminal states of S(y 0 ) are implicitly known by the \su x path" of t, that is, the list of the states t; fail t]; fail fail t]]; : : : ; i:

The algorithm uses the function length de ned for each state p of S(y) by length p] = the length of the longest string spelled from i to p. 12 if length q] = length p] + 1 13 then fail t] q The state denoted by t 0 is state 10, and the su x path of t 0 is the list of the states 10, 3, 2, 1, and 0.

During the execution of the rst loop of the function, state p runs through a part of the su x path of t 0 . At the same time, edges labeled by a are created from p the newly created state t = 11, unless such an edge already exists in which case the loop stops. (b) If a = c, the execution stops with an unde ned value for p. The edges labeled by c start at terminal states, and the failure of t is the initial state.

(c) If a = b, the loop stops on state p = 3, because an edge labeled by b is de ned on it. The condition at line 12 of function Suffix-Automaton-Extension is satis ed, which means that the edge labeled by a from p is not a short-circuit. In this case, the state ending the previous edge is the failure of t.

(d) Finally, when a = a, the loop stops on state p = 3 for the same reason, but the edge labeled by a from p is a short-circuit. The string bbba is a su x of the (newly considered) string bbbbaabbba, but bbbba is not. Since these two strings reach state 5, this state is duplicated into a new state r = 12 that becomes terminal. Su xes bba and ba are re-directed to this new state. The failure of t is r. Computing the number k of occurrences of x in y (assuming that x is a factor of y) starts similarly. Let p be the state reached after the spelling of x from the initial state. Then k is exactly the number of terminal states accessible from p. The number k associated with each state p can be precomputing in time O(n) (independently of the alphabet) by a depth-rst traversal of the graph underlying the automaton. The query for x is then performed in time O(m), whatever is k.

The base of an algorithm for computing a longest factor common to x and y is implemented

Figure 2

 2 Figure2An illustration of the shift in the Knuth-Morris-Pratt algorithm when searching for the pattern x = abcababcababa. (a) The window on the text y is at position 3. A mismatch occurs at position 10 on x. The matching symbols are shown darkly shaded, and the current analyzed symbols lightly shaded. Avoiding both a backtrack on the text and an immediate mismatch leads to shift the window 8 positions to the right. The string-to-string comparison resumes at position 2 on the pattern. (b) The current shift is the consequence of an analysis of the list of the proper borders of x 0 : :9] and of the symbol which follow them in x. The pre xes of x that are borders of x 0 : :9] = abcabacbab are right-aligned along the discontinuous vertical line. String x 0 : :4] = abcab is a border of x 0 : :9], but is followed by symbol a which is identical to x 10]. String x 0 : :1] is the expected border, since it is followed by symbol c. (c) The values of the function for pattern x.

Figure 3 Figure 4

 34 Figure3An illustration of the better-factor shift in the Boyer-Moore algorithm when searching for the pattern x = babacbababa. (a) The window on the text is at position 4. The string-to-string comparison, which proceeds from right to left, stops with a mismatch at position 7 on x. The window is shifted 9 positions to the right to avoid an immediate mismatch. (b) Indeed, the string x 8 : : 10] = aba is repeated three times in x, but is preceded each time by symbol x 7] = b. The expected matching factor in x is then the pre x ba of x. The factors of x identical with aba and the pre xes of x ending with a su x of aba are right-aligned along the rightmost discontinuous vertical line. (c) The values of the shift function for pattern x.

Figure 5

 5 Figure5An illustration of the behavior of two fast string-matching algorithms when searching for the pattern x = sense in the text y = no defense for sense. The successive positions of the window on the text are suggested by the alignments of x with the corresponding factors of y. The symbols of x considered during each scan operation are shown hachured. (a) Behavior of the Boyer-Moore algorithm. The rst and second shifts result from the better-shift function, the third and fourth from the bad-symbol function, and the fth from a shift of the length of x minus the length of its longest proper border (the period of x). (b) Behavior of the Horspool algorithm. We assume here that the four leftmost symbols in the window are compared with the symbols of x 0 : : 3] from left to right.

Figure 7

 7 Figure 7 The explicit part of the automaton D(X) of the pattern X = face; as; easeg. Compared to the trie-like automaton of X displayed in Figure6, state 7 has been made terminal; this is because the corresponding pre x, namely eas, ends with the string as that is in X . The failure function fail is depicted with discontinuous non-labeled directed edges.

  abbabb$ bb

  abbabb$ bb

  Figure10The su x automaton S(y) of the string y = aabbabb. The states are numbered from 0 to 10, according to the order in which they are created by the construction algorithm described in the present section. The initial state is state 0, terminal states are states 0, 5, 9, and 10. This automaton is the minimal deterministic automaton accepting the language of the su xes of y.

  behavior of function Suffix-Automaton-Extension in Figure11.With the su x automaton S(y) of y, several operations can be solved e ciently. We describe three of them. Let x be a string of length m.

Figure 11

 11 Figure11An illustration of the behavior of function Suffix-Automaton-Extension. The function transforms the su x automaton S(y 0 ) of a string y 0 in the su x automaton S(y 0 a) for any given symbol a (the terminal states being implicitly known). Let us consider that y 0 = bbbbaabbb, and let us examine three possible cases according to a, namely a = c, a = b, and a = a. (a) The automaton S(bbbbaabbb). The state denoted by t 0 is state 10, and the su x path of t 0 is the list of the states 10, 3, 2, 1, and 0. During the execution of the rst loop of the function, state p runs through a part of the su x path of t 0 . At the same time, edges labeled by a are created from p the newly created state t = 11, unless such an edge already exists in which case the loop stops. (b) If a = c, the execution stops with an unde ned value for p. The edges labeled by c start at terminal states, and the failure of t is the initial state. (c) If a = b, the loop stops on state p = 3, because an edge labeled by b is de ned on it. The condition at line 12 of function Suffix-Automaton-Extension is satis ed, which means that the edge labeled by a from p is not a short-circuit. In this case, the state ending the previous edge is the failure of t. (d) Finally, when a = a, the loop stops on state p = 3 for the same reason, but the edge labeled by a from p is a short-circuit. The string bbba is a su x of the (newly considered) string bbbbaabbba, but bbbba is not. Since these two strings reach state 5, this state is duplicated into a new state r = 12 that becomes terminal. Su xes bba and ba are re-directed to this new state. The failure of t is r.

  in time O(m) by spelling x from the initial state of the automaton. If the entire string is spelled, x occurs in y. Otherwise we get the longest pre x of x occurring in y.

  in the procedure Ending-Factors-Matcher given below. This procedure reports at each position in y the length of the longest factor of x ending here. It can obviously be used for string matching. It works as the procedure Aho-Corasick-Matcher in the use of the failure function. The running time of the search phase of the procedure is O(m).

  table ! for pattern x when alphabet is reduced to fa; b; c; dg.for each i 2 f0; 1; : : :; m 1g. The value i] is then exactly the length of the shift induced by the better-factor shift. The values of function are computed by the function given below as the function Better-Factor-Function. An auxiliary table, namely f, is used; it is an analogue of the function used in the Knuth-Morris-Pratt algorithm, but de ned this time for the reverse pattern; it is indexed from 0 to m 1. The running time of the function

Better-Factor-Function is O(m).

Trie-Like-Automaton(X) 1 i New-State 2 terminal i] false 3 for string x from rst to last string of X 4 loop p i 5

for symbol a from rst to last symbol of x 6 loop q Target(p; a) [START_REF]Further Information Problems and algorithms presented in the chapter are just a sample of questions related to pattern matching. They share the formal methods used to design e cient algorithms. A wider panorama of algorithms on texts may be found in a few books such[END_REF] if q = nil 8 then q New-State 9

terminal q] false 10 Make-Edge(p; a; q) 11 p q 12 terminal p] true 13 return i

The second step of the preprocessing phase consists mainly in precomputing the failure function. This is done by a breadth-rst traversal of the trie-like automaton. The corresponding pseudocode is given below as the procedure Make-Failure-Function.

Make-Failure-Function(i)

Empty-Queue 3 Enqueue( ; i) 4 while not Queue-Is-Empty( ) 5 loop p Dequeue( ) 6

for each symbol a such that Target(p; a) 6 = nil 7 loop q Target(p; a) 8

fail q] Next-State(fail p]; a; i) 9 if terminal fail q]] 10 then terminal q] true 11 Enqueue( ; q) During the computation, some states can be made terminal. This occurs when the state is identi ed with a pre x that ends with a string of X (an illustration is given in Figure 7).

The complete dictionary-matching algorithm, implemented in the pseudocode below as the procedure Aho-Corasick-Matcher, starts with the two steps of the preprocessing; the search follows, which simulates automaton D(X). It is understood that the empty string does not belong to X. Aho-Corasick-Matcher(X; y) 1 i Trie-Like-Automaton(X) 2 Make-Failure-Function(i) 3 p i 4 for symbol a from rst to last symbol of y 5 loop p Next-State(p; a; i) 6 if terminal p] 7

then report an occurrence The total number of tests \Target(p; a) = nil" performed by function Next-State during its calls by procedure Make-Failure-Function and during its calls by the search phase of Suffix-Tree(y; n) 1 p New-Node 2 h 0 nil 3 h p 4 r 1 5 s n + 1 6 for i from 0 up to n 1 7 loop if h 0 = nil 8 then (h 0 ; h; r; s) Slow-Find(y; nil; p; r + 1; s 1) 9 else (j; k) Label(h 0 ; h) 10 if h 0 = p 11 then (q 0 ; q) Fast-Find(y; p; j + 1; k 1) 12 else (q 0 ; q) Fast-Find(y; link h 0 ]; j; k) 13 link h] q 14 (h 0 ; h; r; s) Slow-Find(y; q 0 ; q; r; s) Once the su x tree of y is build, some operations can be performed rapidly. We describe four applications in the following. Let x be a string of length m.

Testing whether x occurs in y or not can be solved in time O(m) by spelling x from the root of the trie symbol by symbol. If the operation succeeds, x occurs in y. Otherwise, we get the longest pre x of x occurring in y.

Producing the number of occurrences of x in y starts identically by spelling x. Assume that x occurs actually in y. Let p be the node at the extremity of the last taken down edge, or be the root itself if x is empty. The expected number, say k, is then exactly the number of external nodes of the sub-trie of root p. This number can be computed by traversing the sub-trie. Since each internal node of the sub-trie has at least two successors, the total size of the sub-trie is O(k), and the traversal of the sub-trie is performed in time O(k) (independently of ). The method can be improved by precomputing in time O(n) (independently of ) all the values associated with each internal node; the whole operation is then performed in time O(m), whatever is the number of occurrences of x.

The method for reporting the list of positions of x in y proceeds in the same way. The running time needed by the operation is O(m) to locate x in the trie, plus O(k) to report each of the positions associated with the k external nodes.

Finding the longest repeated factor of y remains to compute the \deepest" internal node of the trie, that is, the internal node corresponding to a longest possible factor in y. This is performed in time O(n).

Su x Automata

The su x automaton S(y) of a string y is the minimal deterministic automaton recognizing Su (y), that is, the set of su xes of y. This automaton is minimal among all the deterministic Suffix-Automaton(y) 1 i New-State 2 terminal i] false 3 length i] 0 4 fail i] nil 5 t i 6 for symbol a from rst to last symbol of y 7 loop t Suffix-Automaton-Extension(i; t; a) 8 p t 9 loop terminal p] true 10 p fail p] 11 while p 6 = nil 12 return i The on-line construction is based on the function Suffix-Automaton-Extension that is implemented below. The latter function processes the next symbol, say a, of the string y. If y 0 is the pre x of y preceding a, it transforms the su x automaton S(y 0 ) already build into the su x automaton S(y 0 a).

Research Issues and Summary

String searching by hashing was introduced by Harrison (1971), and later fully analyzed in [START_REF] Karp | E cient randomized pattern-matching algorithms[END_REF].

The rst linear-time string-matching algorithm is due to Knuth, Morris, and Pratt [START_REF] Knuth | Fast pattern matching in strings[END_REF]). It can be proved that, during the search, the delay, that is, the number of times a symbol of the text is compared to symbols of the pattern, is less than blog (m + 1)c, where is the golden ratio (1 + p 5)=2. [START_REF] Simon | String matching algorithms and automata[END_REF] gives a similar algorithm but with a delay bounded by the size of the alphabet (of the pattern). [START_REF] Hancart | On Simon's string searching algorithm[END_REF] proves that the delay of Simon's algorithm is less than 1+blog 2 mc. This paper also proves that this is optimal among algorithms processing the text with a one-symbol bu er. The bound becomes O(log minf1+blog 2 mc; card g) using an ordering on the alphabet , which is not a restriction in practice. [START_REF] Galil | String matching in real time[END_REF] gives a general criterion to transform string-matching algorithms that work sequentially on the text into real-time algorithms.

The Boyer-Moore algorithm was designed in [START_REF] Boyer | A fast string searching algorithm[END_REF]. The version given in this chapter follows [START_REF] Knuth | Fast pattern matching in strings[END_REF]. This paper contains the rst proof on the linearity of the algorithm when restricted to the search of the rst occurrence of the pattern. [START_REF] Cole | Tight bounds on the complexity of the Boyer-Moore pattern matching algorithm[END_REF] proves that the maximum number of symbol comparisons is bounded by 3n for non periodic patterns, and that this bound is tight. [START_REF] Knuth | Fast pattern matching in strings[END_REF] considers a variant of the Boyer-Moore algorithm in which all previous matches inside the current window are memorized. Each window con guration becomes the state of what is called the Boyer-Moore automaton. It is still unknown whether the maximum number of states of the automaton is polynomial or not.

Several variants of the Boyer-Moore algorithm avoid the quadratic behavior when searching for all occurrences of the pattern. Among the most e cient in terms of the number of symbol comparisons are the algorithm of Apostolico and Giancarlo (1986), Turbo-BM algorithm by Crochemore et alii (1992) (the two previous algorithms are analyzed [START_REF] Lecroq | Experimental results on string-matching algorithms[END_REF]), and the algorithm of Colussi [START_REF] Colussi | Fastest pattern matching in strings[END_REF]).

The Horspool algorithm is from [START_REF] Horspool | Practical fast searching in strings[END_REF]. The paper contains practical aspects of string matching that are developed in Hume and Sunday, 1993].

The optimal bound on the expected time complexity of string matching is O( log m m n) (see [START_REF] Knuth | Fast pattern matching in strings[END_REF] and the paper of Yao ( 1980)).

String matching can be solved by linear-time algorithms requiring only a constant amount of memory in addition to the pattern and the (window on the) text. This can be proved by di erent techniques presented in [START_REF] Crochemore | Text Algorithms[END_REF]. The most recent solution is by G asieniec, Plandowski, and Rytter (1995). Cole et alii, 1995] shows that, in the worst case, any string-matching algorithm working with symbol comparisons makes at least n + 9 4m (n m) comparisons during its search phase.

Some string-matching algorithms make less than 2n comparisons. The presently-known upper bound on the problem is n + 8 3(m+1) (n m), but with a quadratic-time preprocessing phase (see Cole et alii, 1995]). With a linear-time preprocessing phase, the current upper bounds are 4 3 n 1 3 m and n + 4 log m+2 m (n m) (see respectively [START_REF] Galil | On the exact complexity of string matching: upper bounds[END_REF] and [START_REF] Breslauer | E cient comparison based string matching[END_REF]). Except in a few cases (patterns of length 3 for example), lower and upper bounds do not meet. So, the problem of the exact complexity of string matching is open. The Aho-Corasick algorithm is from [START_REF] Aho | E cient string matching: an aid to bibliographic search[END_REF]. Commentz-Walter (1979) has designed an extension of the Boyer-Moore algorithm that solves the dictionary-matching problem. It is fully described in [START_REF] Aho | Algorithms for nding patterns in strings[END_REF].

The su x-tree construction of Section 3 is from [START_REF] Mccreight | A space-economical su x tree construction algorithm[END_REF]]. An on-line version is by Ukkonen (1992). A previous algorithm by Weiner (1973) relates su x trees to a data structure close to su x automata.

The construction of su x automata, also described as direct acyclic word graphs and often denoted by the acronym DAWG, is from Blumer et alii, 1985] and from [START_REF] Crochemore | Transducers and repetitions[END_REF]].

An alternative data structure that implements e ciently indexes is the notion of su x arrays introduced in [START_REF] Manber | Su x arrays: a new method for on-line string searches[END_REF].

De ning Terms

Border: A string v is a border of a string u if v is both a pre x and a su x of u. String v is said to be the border of u if it is the longest proper border of u.

Factor: A string v is a factor of a string u if u = u 0 vu 00 for some strings u 0 and u 00 . Occurrence: A string v occurs in a string u if v is a factor of u. Pattern: A nite number of strings that are searched for in texts. Pre x: A string v is a pre x of a string u if u = vu 00 for some string u 00 . Proper: Quali es a factor of a string that is not equal to the string itself. Segment: Equivalent to factor. Su x: A string v is a su x of a string u if u = u 0 v for some string u 0 . Su x tree: Trie containing all the su xes of a string. Su x automaton: Smallest automaton accepting the su xes of a string. Text: A stream of symbols that is searched for occurrences of patterns. Trie: Digital tree, tree in which edges are labeled by symbols or strings.