Michael Benedikt

Gabriele Puppis

Cristian Riveros

Bounded Repairability of Word Languages

Keywords: Bounded repair, edit distance, regular languages

What do you do if a computational object (e.g. program trace) fails a specification? An obvious approach is to perform a repair : modify the object minimally to get something that satisfies the constraints. This approach has been investigated in the database community, for integrity constraints, and in the AI community for propositional logics. Here we study how difficult it is to repair a document in the form of a string. Specifically, we consider number of edits that must be applied to an input string in order to satisfy a given target language. This number may be unbounded; our main contribution is to isolate the complexity of the bounded repair problem based on a characterization of the regular languages that admit bounded repairr. We consider the settings where the repair strategy is unconstrained and when the editing must be produced in a streaming way, i.e. by a letter-to-letter transducer.

Introduction

When a computational object does not satisfy a specification, an obvious approach is to repair it -edit it minimally so that it becomes valid. We may want to perform this editing transformation on the object, or we may be merely interested in knowing how difficult it would be to perform -that is, determining how far a given object or collection of objects is from satisfying the specification. In the database community, this has been extensively studied under the notion of constraint repair (see e.g. [START_REF] Arenas | Consistent query answers in inconsistent databases[END_REF][START_REF] Afrati | Repair checking in inconsistent databases: algorithms and complexity[END_REF]): the specifications considered there are relational integrity constraints, such as keys and foreign keys, and the problems considered include determining how much a database needs to be modified in order to satisfy a given constraint.

Here we study repairs of words. In this case, we can simply consider the edit distance between strings, a standard measure of how many basic operations it takes to get from one string to another. Edit distance is lifted in a natural way to give a measure of the distance of a string u to a language (collection of strings) L. It is well known [START_REF] Wagner | Order-n correction for regular languages[END_REF] that the standard dynamic programming approach to edit distance extends to give an efficient algorithm for calculating the minimum distance of u to any string in L, when L is a regular language given as a non-deterministic finite state automaton.

In this work we take the next step and consider a notion of "distance" between languages: given two languages R and T (specified in terms of automata), we aim to calculate how difficult it is to transform a string satisfying R into a string satisfying T . The notion is motivated by considering R to be a restriction -a constraint that the input is guaranteed to satisfy -while T is a target -a constraint that we want to enforce. We consider the worst-case over any string u ∈ R of the number of edit operations needed to move u into T , that is, we look at the worst-case number of edits needed to get from R to T . Of course, this number may be infinite; the core of our results is a procedure for solving the bounded repair problem, namely, to determine whether the supremum above is finite. In order to solve this effectively, we need to restrict the languages R and T . We consider this problem when the restriction and target languages are presented by both deterministic and non-deterministic finite state automata. In these cases we determine the complexity of the bounded repair problem.

Above we considered the use of an edit/correction function that can read the whole string in memory. In this work we consider the impact of limitations on the editing process -what happens when we require the editing to be done by a transducer, reading the input letter-by-letter and producing the corrected output, based only on a finite amount of control state and a fixed amount of lookahead in the word. We refer to this as a streaming repair processor. We isolate the complexity of the streaming repair problem for any lookahead and for any of type of representation of the languages considered in the non-streaming setting.

The above deals with the problem of determining whether the distance between two specifications is finite or infinite. But in the finite case, we may want to compute this distance exactly, and to produce the processor that optimally edits a given specification. Note that in the non-streaming setting, it is easy to describe the optimal processor: it is simply the procedure that given a word u runs a dynamic programming algorithm to compute the edit distance to the target language (e.g. the algorithm from [START_REF] Wagner | Order-n correction for regular languages[END_REF]). However, in the streaming setting it is not clear how to derive the optimal editing algorithm efficiently. We give results on the complexity of computing the exact bound when it is finite in both the streaming and non-streaming settings, and also give procedures for computing the optimal processor in the streaming setting.

The streaming and non-streaming repair problems have very different flavours: the former are closely related to games played on the components of two automata, while the latter require a more global analysis, and exhibit a close relation to distance automata. However, there are connections between the different problems: we show that in the case where there is no restriction, the bounded repair problems are the same for both the streaming and non-streaming setting. We also show that the bounded repair problem in the streaming setting is independent of the lookahead, and is robust under plausible alternative definitions.

In summary our contributions are:

1.

We formalize the bounded repair problem for languages of words and characterize when regular languages have bounded repair, in both the streaming and non-streaming setting.

2.

We show that the bounded repair problem in the streaming setting is independent of the lookahead, and is robust under variants of the cost function.

3.

Using the characterizations above, we give results on the complexity of the bounded repair problem in each setting.

4.

We present results on the complexity of computing the optimal number of edits, and on computing the optimal repair strategy in the streaming setting.

5.

We demonstrate special cases where the streaming and non-streaming bounded repair problems have the same solution.

Organization. Section 2 gives the preliminaries. Section 3 defines the basic problems. Section 4 gives the characterizations of bounded repairability that we will use throughout the remainder. Section 5 analyses the complexity of the bounded repair problem in the non-streaming and streaming settings. Section 6 shows some connections with games and distance automata. Section 7 gives the conclusions.

Acknowledgments.

We thank the anonymous referees of JCSS for many helpful comments. The authors were supported by the Engineering and Physical Sciences Research Council (UK) grant EP/G004021/1, Enforcement of Constraints on XML Streams.

Preliminaries

Given a word w over an alphabet Σ, we denote by w its length. Given two positions 1 ≤ i ≤ j ≤ w , we denote by w[i] (resp., w[i . . . j]) the i-th symbol of w (resp., the infix of w starting at position i and ending at position j).

Automata. A non-deterministic finite state automaton (shortly, NFA) is a tuple of the form A = (Σ, Q, E, I, F), where Σ is a finite alphabet, Q is a finite set of states, E ⊆ Q × Σ × Q is a transition relation, and I, F ⊆ Q are sets of initial and finite states. The notions of run and accepted word are the usual ones [START_REF] Hopcroft | Introduction to Automata Theory, Languages and Computation[END_REF]. L (A) is the language recognized by A. If A is a deterministic finite state automaton (DFA), which never has more than one applicable transition, then we usually denote the unique initial state by q 0 and turn its transition relation E into a partial function δ from Q × Σ * to Q defined by δ(q, ε) = q and δ(q, a u) = δ(q ′ , u) iff (q, a, q ′ ) ∈ E. We naturally extend the transition function δ of a DFA from letters to strings -that is, we let δ(q, ε) = q and δ(q, u ⋅ a) = δ(δ(q, u), a) for all u ∈ Σ * .

For technical reasons, it is convenient to assume that an automaton is trimmed, namely, all its states are reachable from some initial states (i.e., they are accessible) and they can reach some final states (i.e., they are co-accessible). It is worth noticing that, since the decision problems we are going to deal with are at least NLOGSPACE-hard and since states of automata that are not accessible or not co-accessible can be pruned using a simple non-deterministic logarithmic-space reachability analysis, this assumption will have no impact on our complexity results.

Since automata can be viewed as directed labelled graphs, we inherit standard definitions and constructions in graph theory. In particular, given an automaton A = (Σ, Q, E, I, F) and a state q ∈ Q, we denote by C(q) the strongly connected component (SCC, for short) of A that contains all states mutually reachable with q. Given a set C of states of A (e.g., a SCC), we denote by A C the NFA that recognizes the set of all words that can be consumed entirely inside the SCC C: this automaton is obtained by restricting A to the set C and by letting the new initial and final states be all and only the states in C. Note that if C consists of a single state without transitions to itself, then the language L (A C) recognized by the subautomaton A C is equal to { }. Finally, we denote by dag(A) the directed acyclic graph of the SCCs of A and by dag * (A) the graph obtained from the symmetric and transitive closure of the edges of dag(A).

Transducers. A (subsequential) transducer is a tuple S = (Σ, ∆, Q, δ, q 0 , Ω), where Σ is a finite input alphabet, ∆ is a finite output alphabet, Q is a finite set of states, δ is a partial transition function from Q × Σ to ∆ * × Q, q 0 is an initial state, and Ω is a partial function from Q to ∆ * . For every input word u = a 1 . . . a n ∈ Σ * , there is at most one run of S on u of the form

q 0 a1 v1 -→ q 1 a2 v2 -→ . . . an vn -→ q n ε vn+1 -→
where δ(q i , a i ) = (v i , q i+1 ) for all 0 ≤ i < n and Ω(q n ) = v n+1 [START_REF] Schützenberger | Sur une variante des fonctions sequentielles[END_REF]. In such a case, we define the output of S on u to be the word

S(u) = v 1 v 2 . . . v n v n+1 .
We observe that the transducer may append a string v n+1 at the end of the computation: this is precisely the notion of subsequentiality introduced in [START_REF] Schützenberger | Sur une variante des fonctions sequentielles[END_REF].

Transducers as above produce a portion of the output immediately on reading an input character. We will also consider transducers with a bounded amount of "delay". A k-lookahead transducer, with k ∈ N, is defined as above, but the transition function δ now has input in Q × Σ × (Σ ) k , with Σ = Σ ∪ { } and ∉ Σ. Given an input word u and a position 1 ≤ i ≤ u in it, we denote byu i the (k + 1)-character subword of u ⋅ k that starts at position i and ends at position i + k. The output of a k-lookahead transducer S on an input u of length n is the unique word v = v 1 v 2 . . . v n v n+1 for which there exists a sequence of states q 0 , ..., q n satisfying δ(q i ,u i ) = (v i , q i+1 ), for all 1 ≤ i ≤ n, and Ω(q n ) = v n+1 . Clearly, a 0-lookahead transducer is simply a standard (subsequential) transducer.

The bounded repair problem

Given two words u ∈ Σ * and v ∈ ∆ * , we denote by dist(u, v) the Levenshtein distance (henceforth, edit distance) between u and v, which is defined as the length of a shortest sequence s of edit operations (e.g., deleting a single character, modifying a single character, and inserting a single character) that transforms u into v [START_REF] Wagner | Order-n correction for regular languages[END_REF].

We are interested in quantifying how difficult it is to edit a word in one language to obtain a word in another language. That is, we have finite alphabets Σ and ∆ and regular languages R ⊆ Σ * and T ⊆ ∆ * , called the restriction and target languages, respectively. We would like to edit any string that is known to belong to the restriction language R into a string in the target language T . How do we measure the cost of edits needed to get from R to T ? One method is to look at the largest number of edit operations that are needed to get into T from strings in R, that is, the supremum over all u ∈ R of the minimum over all v ∈ T of dist(u, v):

cost(R, T ) = def sup u∈R min v∈T dist(u, v).
Intuitively, having a finite uniform bound to the edit distance of words in R from T , means that the language R is "quite close to being a subset" of T -the gap between strings in R and strings in T is small.

A repair strategy for two languages R and T is any function from R to T . For a repair strategy f and a word u ∈ R, we define the cost of f on u, denoted cost(u, f), as the edit distance between u and f(u). Accordingly, we define the worst-case cost of f as the supremum of the cost of f over all words in R (if the cost of f on u ∈ R is unbounded, then write cost(R, f) = ∞). Note that the value cost(R, T ) introduced in the previous paragraph can be equally described as the minimum over all repair strategies f for R and T of the worst-case cost of f: indeed, the best repair strategy for R and T is just to output on any u ∈ R the word in T that is closest to u with respect to the edit distance. The bounded repair problem is to decide, given two regular languages R and T , whether cost(R, T ) is finite or not, namely, whether all words in R can be edited into T with at most some cost bound that does not depend on the input word. A variant of the bounded repair problem, called threshold repair problem, consists of deciding whether cost(R, T ) ≤ θ for two given regular languages R and T and for a given number θ. This problem is the decision version of the problem of computing the exact value of cost(R, T ).

The regular languages R and T are naturally presented by means of automata. In the following, we will study the complexity of the bounded repair problem for languages specified by (i) deterministic finite state automata (DFA) and (ii) non-deterministic finite state automata (NFA).

Streaming vs non-streaming. The notion of "how much does it cost to edit a word in R to a word in T " assumes that a repair strategy could be any mapping from R to T (in principle, such a mapping could even fail to be computable). However, we know from [START_REF] Wagner | Order-n correction for regular languages[END_REF] that there is a dynamic programming algorithm that, given a word u and a regular target language T specified by means of a finite state automaton T , computes in time O( u ⋅ T ) an optimal edit sequence that transforms u into some word in T . In particular, this shows that optimal repair strategies can be described by functions of fairly low complexity.

Sometimes it is desirable to have repair strategies that are in even more limited classes. Perhaps the ideal case is when we can repair R into T with a one-pass algorithm, that is, using a transducer. Recall that a transducer defines a word-to-word partial function; if this function happens to produce a word in T for every input u ∈ R, then we say that it is a streaming repair strategy for R and T . Similarly, we can consider k-lookahead transducers, with k ∈ N. This type of transducer outputs words on the basis of its current state and an input (k + 1)character window that represents a substring of u of the form u

[i] . . . u[i + k],
where u[i] is either the i-th symbol of w, if i ≤ u , or a dummy symbol , if i > u . Accordingly, we talk about a k-lookahead streaming repair strategy for R and T .

Given a (k-lookahead) streaming edit strategy S for R and T and given a word u ∈ R, we can define the cost of S on u in two ways:

1.

letting q 0 a1 v1

-→ q 1 a2 v2 -→ . . . an vn -→ q n vn+1
-→ be the run of S on u, we define the aggregate cost of S on u, denoted cost aggr S (u), to be the length of the final output v n+1 plus the sum, over all indices 1

≤ i ≤ n, of dist(a i , v i ), where dist(a i , v i ) is 1 if v i is empty, v i -1 if a i occurs in v i , and v i otherwise; 2.
considering the transducer S as a repair strategy, we define the edit cost of S on u, denoted cost edit S (u), to be simply the edit distance between u and the output S(u).

The first notion of cost considers the distortions performed in producing the input from the output -it is equivalent to considering the transducer as producing edit sequences rather than strings and counting the number of edits produced. The second notion of cost is global and it considers only the output and not its production (clearly, the edit cost never exceeds the aggregate cost). These two models of cost can be very different in general. As an example, consider a transducer S on the input alphabet Σ = {a, b} that converts a's to b's, and b's to a's. On the string u n = (ab) n , the aggregate cost is 2n since S changes each letter, but the edit distance between u and S(u) (i.e., the edit cost of S on u in our sense) is only 2.

Similarly, we define the worst-case aggregate/edit cost of the k-lookahead streaming repair strategy S as follows:

cost λ S (R) = def sup u∈R cost λ S (u) for λ ∈ {aggr, edit}.
The k-lookahead streaming aggregate/edit cost cost λ k-lookahead (R, T ) for two languages R and T and for λ ∈ {aggr, edit} is then defined as the minimum of cost λ S (R) taken over all k-lookahead streaming strategies S for R and T .

The following example illustrates the difference between bounded repairability in the streaming and non-streaming settings: In the non-streaming setting, one can get from R to T by only editing the initial letter, and thus cost(R, T ) = 1. In contrast, a k-lookahead streaming edit strategy must decide whether to leave or change the initial letter, and thus it could be forced to repair an unbounded sequence of a's or b's after the sequence of c's. In this case we have

cost aggr k-lookahead (R, T ) = cost edit k-lookahead (R, T ) = ∞.
The bounded repair problem in the k-lookahead streaming setting consists of deciding whether cost λ k-lookahead (R, T ) < ∞ for a given pair of regular languages R and T , a given λ ∈ {aggr, edit}, and a given k ∈ N. To stress the difference between the streaming and the non-streaming settings, we explicitly refer to the original problem as the bounded repair problem in the non-streaming setting. Even though the two models of aggregate and edit cost for streaming repair strategies can be very different, it will turn out that for the bounded repair problem it does not matter which cost model we choose (see Corollary 4.6).

Special cases. We are also interested in a variant of the bounded repair problem where the restriction language is assumed to be universal, i.e., a language of the form Σ * . In this case, the input to the problem consists of a restriction alphabet Σ and a regular target language T . We refer to this variant as the unrestricted case of the bounded repair problem.

Characterizations of bounded repairability

We fix a restriction language R and a target language T and we assume, for the moment, that these languages are recognized by two NFA R and T , respectively. Recall that, given a SCC C of R, we denote by R C the subautomaton of R that is obtained by declaring the states in C to be both initial and final and by discarding all other states. Moreover, dag(R) denotes the directed acyclic graph of the SCCs of R and dag * (T ) denotes the symmetric and transitive closure of dag(T ). Finally, recall that both R and T are trimmed, namely, unreachable and sink states are removed from R and T .

Non-streaming setting

In order to characterize the positive instances of the bounded repair problem, we need to consider the relationships between the paths in dag(R) and the paths in dag * (T ). We say that a path π = C 1 . . . C k of SCCs in dag(R) is covered by a path τ = D 1 . . . D h of SCCs in dag * (T ) if we have k = h and L (R C i ) ⊆ L (T D i ) for all indices 1 ≤ i ≤ k, namely, if the language recognized by the i-th component along π is contained in the language recognized by the i-th component along τ.

The following characterization reduces the bounded repair problem in the non-streaming setting to a path coverability problem between finite directed acyclic graphs. cost(L (R), L (T )) < ∞ (i.e., there is a strategy that repairs L (R) into L (T ) with a uniformly bounded number of edits), 2.

every path in dag(R) is covered by some path in dag * (T ),

3. cost(L (R), L (T )) ≤ (1 + dag(R) ) ⋅ T .
Proof of Theorem 4.1. Let R = (Σ, Q, E, I, F) and T = (∆, Q ′ , E ′ , I ′ , F ′ ) be two NFA. We first prove the implication from 2 to 3; later we will prove the implication from 1 to 2 (the implication from 3 to 1 is trivial). We briefly outline the main ideas underlying the proof of the implication from 2 to 3. In this direction, we assume that the coverability condition is satisfied, and we repair a generic word u ∈ L (R) as follows. We first consider the path π of SCCs of R that is induced by a successful run on u, and we observe that the input word u can be factorized into a bounded number of pieces, each one realizable within a component of the path. For instance, if π = C 1 . . . C k is the considered path inside dag(R), then we can factorize u as u 1 a 1 u 2 . . . a k-1 u k , with u i ∈ L (R C i ) and a j ∈ Σ for all 1 ≤ i ≤ k and all 1 ≤ j < k. We then consider a path inside dag * (T ) that covers π, say τ = D 1 . . . D k , and we observe that each factor u i is also realizable within the component D i of T . In particular, no repair is needed on the factors u 1 , . . . , u k . On the other hand, the characters a 1 , . . . , a k-1 that are interleaved with the factors in u and that induce jumps along the components C 1 , . . . , C k of π can be replaced by small strings inducing analogous jumps along the components D 1 , . . . , D k of τ. This is possible because there exist partial runs connecting arbitrary states in each component D i to arbitrary states in the next component D i+1 . In the end, the repair of u is formed by interleaving the factors u 1 , . . . , u k with the small strings that replace a 1 , . . . , a k-1 , and by appending a final string to reach an accepting state of T .

We now turn to the technical details of this proof. Suppose that every path in dag(R) is covered by some path in dag * (T ). We have to prove the existence of a repair strategy of L (R) into L (T ) with edit cost uniformly bounded by (1 + dag(R) ) ⋅ T . Let us fix a generic word u in the restriction language L (R), and let ρ be an accepting run of R on u. The sequence of SCCs of R that are visited by the run ρ identifies a path inside dag(R), say π = C 1 C 2 . . . C k . Accordingly, we factorize the word u into the sequence of subwords u 1 , a 1 , u 2 , a 2 , . . . , u k , where

u i ∈ L (R C i ) for all 1 ≤ i ≤ k and a i ∈ Σ for all 1 ≤ i ≤ k -1.
From the assumption of coverability of the paths in dag(R), we know that there is a path

τ = D 1 D 2 . . . D k in dag * (T ) that covers π, namely, such that L (R C i ) ⊆ L (T D i ) for all 1 ≤ i ≤ k.
This shows that each subword u i , with 1 ≤ i ≤ k, belongs also to the language L (T D i ).

We can now construct inductively a corresponding word f(u) that has the form v 0 u 1 v 1 u 2 . . . u k v k and that is accepted by T . Recall that τ = D 1 . . . D k is a path in dag * (T ). Because the automaton T is trimmed, we know that all states in D 1 can be reached from some initial state of T and, similarly, all states in D k can reach some final state. In particular, since u 1 ∈ L (T D 1 ), we know that there exist an initial state s 0 of T , two states r 1 and s 1 in D 1 , and a word v 0 ∈ ∆ * such that T admits a run of the form s 0 v0 -→ r 1 u1 -→ s 1 . Moreover, without loss of generality, we can assume that the length of v 0 is bounded by the number of states of T . For the inductive step, we assume that the words v 0 , . . . , v i-1 , with 0 ≤ i ≤ k -1, are defined and that T admits a run on v 0 u 1 . . . v i-1 from the initial state s 0 to a state s i ∈ D i . Since every state in D i+1 is reachable from every state in D i , we know that there is a word v i , with v i ≤ T , and two states r i+1 and s i+1 in D i+1 such that T admits a run of the form

s i v i -→ r i+1 u i+1 -→ s i+1 .
For the final step, we assume that v 0 , . . . , v k-1 are defined and that T admits a run on v 0 u 1 . . . v k-1 u k from the initial state s 0 to a state s k ∈ D k . Using arguments similar to the previous ones and the fact that all states in D k can reach a final state, we derive the existence of a word v k , with v k ≤ T , and a final state r k+1 of T such that T admits a run of the form s k v k -→ r k+1 . Putting everything together, we obtain the existence of a successful run of T of the form

s 0 v0 -→ r 1 u1 -→ s 1 v1 -→ r 2 u2 -→ . . . r k u k -→ s k v k -→ r k+1
and hence the word f(u) = v 0 u 1 v 1 u 2 . . . u k v k is accepted by T . Moreover, since k ≤ dag(R) and v i ≤ T for all 0 ≤ i ≤ k, we have that the edit distance between u and f(u) is at most (1 + dag(R) ) ⋅ T . This proves that there is a repair strategy f for L (R) and L (T ) with edit cost uniformly bounded by (1 + dag(R) ) ⋅ T , and hence

cost(L (R), L (T )) ≤ (1 + dag(R) ) ⋅ T .
We now prove the implication from 1 to 2, namely, we assume that there is a repair strategy f for R and T with bounded cost and we show that every path in dag(R) is covered by a path in dag * (T ). The general idea is to associate with any path π = C 1 , . . . , C k inside dag(R) a suitable word u π ∈ L (R), called witnessing word of π, whose repair according to the strategy f induces a path τ inside dag * (T ) that covers π. Intuitively, the witnessing word u π is obtained from the path π by replacing every component C i with a sufficiently large number of repetitions of a special string in L (R C i ), which we called fingerprint of C i . The number of repetitions of each fingerprint will depend on the worst-case repair cost N = max u∈L (R) {cost(u, f)}, and will be large enough to imply that any repair of the witnessing word u π achieved by at most N edits contains at least one copy of the fingerprint of each component C i of π. Moreover, the order of occurrence of the fingerprints inside the repaired string will be the same as the order of the components in the path π. One finally looks at some run of T that accepts f(u π ): thanks to the occurrence order of the fingerprints of f(u π ), this run must induce a path τ inside dag * (T ) that covers π.

Before constructing the witnessing word, we prove a technical lemma, which defines precisely the concept of fingerprint of a component of R. Intuitively, the lemma shows that, for any given component C of R, one can find a word u that can be arbitrarily "pumped" inside the language L (R C) -namely,

{u} * ⊆ L (R C) -and such that, for all components D of T , u ∈ L (T D) iff L (R C) ⊆ L (T D). Hereafter, we say that a word u is cyclic (in a component C) if there is q ∈ C such that R admits a run of the form q u -→ q. Lemma 4.2. For every component C of R, there is a cyclic word u ∈ L (R C) such that, for every component D of T , u ∈ L (T D) iff L (R C) ⊆ L (T D).
Proof. Let C be a component of R and let D 1 , . . . , D m be all the components of T . We construct the cyclic word u by exploiting an induction over the number of components in T . That is, we prove that for all i, there is a cyclic word u i ∈ L (R C) such that:

∀1 ≤ j ≤ i. L (R C) ⊆ L (T D j ) iff u i ∈ L (T D j ) (⋆)
Clearly, the lemma follows from (⋆) when we let u = u m . The base step i = 0 is vacuously true, so we simply let u 0 = ε. For the inductive step, let i < m and suppose that there exists a word u i satisfying (⋆). We construct a word u i+1 that satisfies (⋆) as well. We distinguish between two cases, depending on whether

L (R C) ⊆ L (T D i+1 ) or not. If L (R C) ⊆ L (T D i+1 ), then we simply let u i+1 = u i , in such a way that (⋆) holds trivially. Otherwise, let v 1 be a word in L (R C) ∖ L (T D i+1 ). Since v 1 ∈ L (R C),
R admits a run of the form q v1 -→ r, for some states q, r ∈ C. Similarly, since u i is cyclic in C, R admits a run of the form s u i -→ s, for some state s ∈ C. Moreover, since q, r, s are mutually reachable inside C, there exist some words

v 0 , v 2 ∈ L (R C) such that R admits runs of the form s v0 -→ q and r v2 -→ s. Now, define u i+1 = v 0 v 1 v 2 u i .
The word u i+1 is cyclic in C, as witnessed by following the run:

s v0 -→ q v1 -→ r v2 -→ s u i -→ s.
It is also easy to see that u i+1 does not belong to

L (T D i+1 ). Indeed, if u i+1 ∈ L (T D i+1
), then the subautomaton T D i+1 would also admit a run on the factor v 1 of u i+1 , which is a contradiction since v 1 ∉ L (T D i+1 ). Finally, we know from the inductive hypothesis that for all 1

≤ j ≤ i, L (R C) ⊆ L (T D j ) iff u i ∈ L (T D j )
, and that the latter holds iff u i+1 ∈ L (T D j ). We conclude that, for every 1

≤ j ≤ i + 1, L (R C) ⊆ L (T D j ) iff u i+1 ∈ L (T D j )
, which proves the inductive step for (⋆). ◻

Consider now any path

π = C 1 . . . C k ∈ dag(R).
We associate with each component C i a word u i that satisfies Lemma 4.2, and we call it the fingerprint of C i . Since each word u i is cyclic for C i and since all states in a component C i can reach all states in the next component C i+1 , we know that there exist states

q 1 ∈ C 1 , . . . , q k ∈ C k and words u ′ 1 , . . . , u ′ k-1 such that R admits a run of the form q 1 u1 -→ q 1 u ′ 1 -→ q 2 u2 -→ q 2 u ′ 2 -→ ⋯ u k-1 -→ q k u k -→ q k .
Furthermore, since R is trimmed, there exist an initial state q 0 , a final state q k+1 , and some words u ′ 0 , u ′ k such that R admits runs of the form q 0

u ′ 0 -→q1 and q k u ′ k -→qk+1.
Putting all together, we have that, for every positive natural number n, the word

u (n) = def u ′ 0 u n 1 u ′ 1 u n 2 . . . u n k u ′ k is accepted by R.
We define the witnessing word of π as u π = u (M) , where M = (N + 1) ⋅ ( dag(R) + 1).

To conclude the proof, we look at the repair f(u π ) of the witnessing word of π, we extract from it a path τ in dag * (T ), and we show that τ covers π. First, recall that f(u π ) is accepted by T and is obtained from u π by a sequence of at most N edits. From this and the definition of u π , it follows that we can write

f(u π ) = v 0 u 1 v 1 u 2 . . . u k v k where = dag(R) + 1.
A simple application of the pigeon-hole principle shows that every run of T on f(u π ) must contain a sub-run of the form r i u i -→ s i , for each 1 ≤ i ≤ k, where the states r i and s i belong to the same component of T . Specifically, this means that f(u π ) can be equally written as

v ′ 0 u 1 v ′ 1 u 2 . . . u k v ′ k ,
and that this word is accepted by a run of T of the form:

s 0 v ′ 0 -→ r 1 u1 -→ s 1 v ′ 1 -→ r 2 u2 -→ s 2 . . . r k u k -→ s k v ′ k -→ r k+1
where r i , s i ∈ D i for all 1 ≤ i ≤ k, and D 1 , . . . , D k are SCCs of T . In particular, for all 1 ≤ i ≤ k, we have u i ∈ L (T D i ), and hence

L (R C i ) ⊆ L (T D i ) since u i is the fingerprint of C i . We have just shown that the path τ = D 1 . . . D k in dag * (T ) covers the arbitrarily chosen path π = C 1 . . . C k . ◻

Streaming setting

We now provide a variant of Theorem 4.1 that characterizes the positive instances of the bounded repair problem in the streaming setting. We do so by adding in a game. For this it is convenient to assume that the restriction and target languages are presented by means of DFA R and T . We associate with R and T a reachability game played by two players, Adam and Eve, on a directed acyclic graph A R,T , which is defined in terms of the SCCs of R and T . The idea underlying the game is as follows: the moves of Adam's construct incrementally a path π in dag(R); Eve has to respond to these moves by constructing of a corresponding path f(π) in dag * (T ) that covers π. In the game setting, moves are played alternatively between Adam and Eve. In particular, the function f that describes Eve's strategy must satisfy the following condition: if π ⋅ C is an extension of the path π in dag(R) by a single component, then either f(π ⋅ C) coincides with f(π) or it is an extension of f(π) by a single component, namely,

f(π ⋅ C) is of the form f(π) ⋅ D.
Formally, the arena A R,T of the game is a directed acyclic graph, in which the nodes owned by Adam (resp., Eve) are the pairs of the form (C, D) (resp., (D, C)), with C SCC of R and D SCC of T . The edges of the arena connect Adam's nodes (C, D) to Eve's nodes (D, C ′ ) whenever (C, C ′ ) is an edge of dag(R); similarly, they connect Eve's nodes (D, C) to Adam's nodes (C, D ′ ) whenever (D, D ′ ) is an edge of dag * (T ) and, in addition,

L (R C) ⊆ L (T D ′ ).
The initial node is owned by Eve and it is of the form (D 0 , C 0 ), where C 0 is the SCC of the initial state of R and D 0 is the SCC of the initial state of T . The last player who moves wins. Intuitively, Adam's objective is to reach a node (C, D) where Eve cannot respond with any move. Conversely, Eve's objective is to reach a node (D, C) where Adam cannot respond with any move. As usual, we say that a player has a winning strategy on the arena A R,T if he/she can win the reachability game on A R,T independently of the choices of the other player.

The following characterization reduces the bounded repair problem in the streaming setting to the problem of determining the winner of a reachability game over a finite arena. Theorem 4.3. Given two DFA R and T , the following two conditions are equivalent:

1.

there exists a streaming strategy with some lookahead that repairs L (R) into L (T ) with uniformly bounded edit cost,

2.

Eve has a winning strategy in the reachability game on A R,T .

The idea underlying the proof of the direction from 2 to 1 is as follows. If we have a winning strategy for Eve, then we can get a streaming repair strategy for L (R) and L (T ) by tracking the current component C reached by the input and by maintaining the invariant that the component D induced by repaired string is such that (C, D) is a position consistent with Eve's winning strategy. When a new letter comes in and changes the component in the restriction from C to C ′ , we respond with a suitable repair that moves from D to the response component D ′ that preserves the invariant.

For the direction from 1 to 2, we assume that there is a streaming klookahead edit strategy that repairs L (R) into L (T ) with uniformly bounded cost and derive a strategy for Eve. The strategy will maintain the invariant that the position (C, D) corresponds to some input string u and repair v consistent with the repair strategy. If, by way of contradiction, we reach a pair (C, D) corresponding to some string u and, moreover, there is a successor SCC C ′ of C corresponding to some extension u u ′ , and (D, C ′ ) is a losing position for Eve, then, for every SCC D ′ of T , we can find a word witnessing the noncontainment L (R C ′ ) ⊈ L (T D ′ ). We can then concatenate multiple copies of such words together in such a way that the resulting string cannot be re-paired by our transducer with a bounded number of edit operations, which is a contradiction.

Before turning to the proof of the above theorem, it is convenient to establish two preliminary lemmas, which will be also reused in other proofs (e.g., in the proof of Proposition 5.4). For the sake of brevity, given an NFA (resp., DFA) A, a SCC C of it, and a state q ∈ C, we denote by A q C the NFA (resp., the DFA) obtained from the subautomaton A C by letting q be the unique initial state (recall that the final states of A C are all the states in C).

Lemma 4.4. Let R be an NFA, let T be a DFA, and let C and D be some SCCs of R and T , respectively. We have that

L (R C) ⊆ L (T D) iff ∃ q ∈ C, r ∈ D. L (R q C) ⊆ L (T r D). Proof. Let R = (Σ, Q, E, I, F) and T = (∆, Q ′ , δ ′ , r 0 , F ′ ).
We first prove the rightto-left implication. Suppose that L (R q C) ⊆ L (T r D) for some states q ∈ C and r ∈ D. Let u be a word in L (R C). Since q ∈ C and C is a SCC, we know that there is a word

u 0 ∈ Σ * such that u 0 u ∈ L (R q C). Since L (R q C) ⊆ L (T r D)
, the same word u 0 u belongs also to the language L (T r D). In particular, this shows that u ∈ L (T D).

We now prove the contrapositive of the left-to-right implication, namely, we assume that L (R q C) ⊈ L (T r D) for all q ∈ C and all r ∈ D and we derive L (R C) ⊈ L (T D). Let D = {r 1 , . . . , r n }. We first prove, by exploiting an induction on i ≤ n, that there is a word u i that belongs to L (R C) but not to L (T r j D) for all indices 1 ≤ j ≤ i. The base case is trivial. For the inductive step, we assume that the claim holds for i < n and we prove it for i + 1. The main idea is to append to the word obtained from the inductive hypothesis a suitable word that witnesses a non-containment of L (R q C) into L (T r i+1 D). Let u i be the word obtained from the inductive hypothesis such that u i ∈ L (R C) ∖ L (T r j D) for all 1 ≤ j ≤ i. Moreover, let s i+1 be the state reached by T from r i+1 after parsing the word u i , that is, s i+1 = δ ′ (r i+1 , u i ) (note that here we use the determinism of T ). If s i+1 ∉ D, then the claim follows trivially. We thus consider the case

s i+1 ∈ D. Recall that u i ∈ L (R C) and let p i , p ′ i be two states in C such that p i u i -→ p ′ i .
From the original assumption and the fact that

p ′ i ∈ C and s i+1 ∈ D, we know that L (R p ′ i C) ⊈ L (T s i+1 D), and hence there is a word v i+1 ∈ L (R p ′ i C) ∖ L (T s i+1 D).
In particular, this shows that the word u i+1 = u i v i+1 belongs to the language L (R C), but not to the language L (T r i+1 D). Finally, since D is a SCC, it follows that u i+1 does not belong to any of the languages L (T r j D) either, for all 1 ≤ j ≤ i, and this concludes the proof. ◻ Lemma 4.5. Let R and T be two DFA and let C and D be some SCCs of R and T , respectively. We have that

L (R C) ⊆ L (T D) implies ∀ q ∈ C. ∃ r ∈ D. L (R q C) ⊆ L (T r D).
Proof. Let R = (Σ, Q, δ, q 0 , F) and T = (∆, Q ′ , δ ′ , r 0 , F ′ ) be two DFA, let C and D be two SCC of R and T , respectively, such that L (R C) ⊆ L (T D), and let q be a state in C. We know from Lemma 4.4 that there exist two states p ∈ C and s ∈ D such that L (R p C) ⊆ L (T s D). Moreover, since the states p, q in C are mutually reachable, there is a word u 0 such that δ(p, u 0 ) = q. Since L (R p C) ⊆ L (T s D) and u 0 ∈ L (R p C), we know that the state r = δ(s, u 0 ) belongs to D as well. Now, let us consider a generic word u in L (R q C).

Clearly, we have

u 0 u ∈ L (R p C). From L (R p C) ⊆ L (T s D) it follows that u 0 u ∈ L (T s D), whence u ∈ L (T r D). This shows that L (R q C) ⊆ L (T r D). ◻
Proof of Theorem 4.3. Let R = (Σ, Q, δ, q 0 , F) and T = (∆, Q ′ , δ ′ , r 0 , F ′ ) be two DFA and let A R,T be the arena obtained from R and T as described above.

Below, we prove first the implication from 2 to 1 and then the implication from 1 to 2.

Suppose that Eve has a winning strategy in the reachability game over A R,T . Since reachability games are positionally determined, Eve's strategy can be described by a partial function 1 g that maps a node of the form (D, C), with C ∈ dag(R) and D ∈ dag * (T ), to a successor g(D, C) = (C, D ′ ) (if there is any) in the arena A R,T . We can use Eve's winning strategy g to construct a subsequential 0-lookahead transducer S that implements a streaming repair strategy for L (R) and L (T ) having uniformly bounded aggregate cost. Intuitively, the transducer S works as follows. While parsing the input word u from the restriction language L (R) and emitting a corresponding word v, the transducer S mimics, at the same time, the transitions of both automata R and T . Each time the restriction automaton R exits the current SCC C and enters a new SCC C ′ , a corresponding move (C, D) Adam -→ (D, C ′ ) for Adam is identified; accordingly, on the basis of Eve's response g(D, C ′ ) = (C ′ , D ′ ) (recall that Eve's strategy was assumed to be winning), the transducer S outputs a suitable word that makes the target automaton T move from the SCC D to the SCC D ′ (the new state in D ′ can be determined using Lemma 4.5 since we have

L (R C ′ ) ⊆ L (R D ′ )).
The formal definition of the transducer S is a bit more technical due to the treatment of some special cases. First of all, we can assume, without loss of generality, that the initial state q 0 of R has no entering transitions (we can always enforce this condition by duplicating states). Then, we let C 0 be the SCC of q 0 in R, D 0 be the SCC of the initial state r 0 of T , g(D 0 , C 0 ) = (C 0 , D 1 ) be target node in the arena A R,T for the first move of the player Eve (recall that g is the winning strategy of Eve). We also let r 1 be some arbitrary state in D 1 such that L (R q0 C 0 ) ⊆ L (T r1 D 1 ) -this states exists thanks to the containment L (R C 0 ) ⊆ L (R D 1 ) and Lemma 4.5. Accordingly, we define v 0 to be the shortest word such that δ ′ (r 0 , v 0 ) = r 1 -note that dag * (T ) contains an edge from D 0 to D 1 and hence the state r 1 must be reachable from r 0 . Intuitively, the word v 0 is the first prefix emitted by the transducer S at the beginning of 1 The reason for the strategy function g to be partial is that some positions in the arena A R,T may have no successors.

the computation (it should be now clear why we assumed that the initial state q 0 of R has no entering transitions). Below we define the various components of the transducer S = (Σ, ∆, Q ′′ , δ ′′ , s 0 , Ω).

The state space of the transducer is

Q ′′ = Q × Q ′ .
For every state s = (q, r) ∈ Q ′′ and every symbol a ∈ Σ, δ ′′ (s, a) = (v, s ′ ), where s ′ = (δ(q, a), δ ′ (r, v)) and v is the word over ∆ defined as follows:

1. if both states q and δ(q, a) belong to the same SCC of R, then we let v be either the input symbol a or the word v 0 ⋅ a, depending on whether q ≠ q 0 or q = q 0 ; 2. otherwise, if the states q and δ(q, a) belong to different SCCs, we denote by C ′ the SCC of the state δ(q, a) in R, by D the SCC of the state r in T , by (C ′ , D ′ ) the response g(D, C ′ ) given by Eve's winning strategy, by r ′ some arbitrary state in

D ′ such that L (R δ(q,a) C ′ ) ⊆ L (T r ′ D ′ ) -the state r ′ exists thanks to the con- tainment L (R C ′ ) ⊆ L (R D ′
) and Lemma 4.5 -and, finally, we denote by v ′ the shortest word such that δ ′ (r, v ′ ) = r ′ -the state r ′ is reachable from r because dag * (T ) contains an edge from D to D ′ . Accordingly, we define the output v be either the word v ′ or the word v 0 v ′ , depending on whether q ≠ q 0 or q = q 0 . The initial state of the transducer is s 0 = (q 0 , r 0 ). For every state s = (q, r) ∈ Q ′′ , the final output Ω(s) is defined to be the shortest word v ∈ ∆ * such that δ(r, v) ∈ F ′ -note that the existence of such a word v is guaranteed by the assumption that every state of T can reach some final state.

Using arguments similar to those used in the proof of Theorem 4.1 (e.g., by associating with each successful run of R a corresponding path π in dag(R) and a covering path τ in dag * (T ) induced by Eve's winning strategy), one can show that the transducer S maps any word u ∈ L (R) to a word S(u) ∈ L (T ). Moreover, by construction, the output produced at each transition of S can be different from the input symbol only if S is at the beginning of the computation, at the end of the computation, or if the current SCC of the automaton R has just changed. In each of these cases, the length of the produced output does not exceed the number of states in T . This shows that the aggregate cost of S on input u ∈ L (R) is at most (1 + dag(R) ) ⋅ T and hence

cost aggr 0-lookahead (L (R), L (T )) ≤ (1 + dag(R) ) ⋅ T .
We now prove the implication from 1 to 2, namely, we assume that S = (Σ, ∆, Q ′′ , δ ′′ , s 0 , Ω) is a transducer with k-lookahead that implements a repair strategy for L (R) and L (T ) with edit cost uniformly bounded by a natural number N, and we derive from this a winning strategy for Eve. More precisely, we will specify Eve's moves g(D, C) on those nodes (D, C) in A R,T , with C ∈ dag(R) and D ∈ dag * (T ), for which there exist some words u

C , u ′ C ∈ Σ * and v D ∈ ∆ * such that i) δ(q 0 , u C u ′ C ) ∈ C, ii) δ ′ (r 0 , v D ) ∈ D, iii) δ ′′ (s 0 , u C ) = (v D , s ′ ) for some s ′ ∈ Q ′′ .
We call these nodes reachable. On the remaining (unreachable) nodes, we let the function g be unspecified. As a preliminary remark, we observe that from the definition of the arena A R,T and from the above properties, the domain of the function g is closed under the ancestor relation, namely, if g(D, C) is defined and

(D ′ , C ′ ) is an ancestor of (D, C) in the arena A R,T , then g(D ′ , C ′ )
is defined as well. Thus, to prove that the defined strategy g is winning for Eve, it will be sufficient to verify that the moves induced at the leaves of g reach nodes that are losing for Adam. Below, we define the moves g(D, C) by exploiting an induction on the distance of the SCC C from the root of dag(R), which is the SCC of the initial state q 0 of R. Consider a reachable node (D, C) in the arena A R,T . Since (D, C) is reachable, we know that there exist some words u

C , u ′ C ∈ Σ * and v D ∈ ∆ * such that (i) δ(q 0 , u C u ′ C ) ∈ C, (ii) δ ′ (r 0 , v D ) ∈ D, and (iii) δ ′′ (s 0 , u C ) = (v D , s ′ ) for some s ′ ∈ Q ′′ .
For the sake of brevity, we let q = δ(q 0 , u C u ′ C ). We claim that there is a SCC D ′ that is a successor of D in dag * (T ) (possibly

D ′ = D) such that L (R C) ⊆ L (T D ′ )
. Indeed, suppose, by way of contradiction, that this is not the case. Let D 1 , . . . , D h be all the the descendants of D, topologically ordered according to their accessibility relation (hence D 1 = D). Using arguments similar to those used in the proof of Theorem 4.1, we can recursively construct a sequence of words u ′ 0 , u 1 , u ′ 1 , . . . , u h , u ′ h over Σ such that, for all 1 ≤ i ≤ h: i) q u i u ′ i -→ q is a run of R that starts and ends in state q, ii)

u i ∉ L (T D i ).
In particular, the first property implies that the word

u C u ′ C (u 1 u ′ 1 ) N+1 . . . (u h u ′ h ) N+1
is a prefix of some word u in the language L (R) (recall the assumption that all states in R can reach some final states). Moreover, since u contains N + 1 occurrences of the subwords u 1 , . . . , u h and since S implements a repair strategy with cost uniformly bounded by N, we have that the words u 1 , . . . , u h must occur at least once, and in this particular order, as subwords of S(u) (observe that having a transducer with k-lookahead does not help here). However, since v D is a prefix of S(u), δ(r 0 , v D ) ∈ D, and u i ∉ L (T D i ) for all 1 ≤ i ≤ h, we have that S(u) cannot belong to the target language L (T ). This is against the assumption that S implements a repair strategy for L (R) and L (T ). We must conclude that there is a SCC D ′ that is a successor of D in dag * (T ) and that satisfies L (R C) ⊆ L (T D ′ ). Accordingly, we define Eve's move on node (D, C) to be g(D, C) = (C, D ′ ) (note that this is a valid move in the arena A R,T ). Turning to the proof of the main theorem, we argue that the above defined strategy g for Eve is winning. This is equivalent to proving that, in every partial play of the form

(D 0 , C 0 ) Eve -→ (C 0 , D 1 ) Adam -→ . . . Adam -→ (D n , C n )
that follows Eve's strategy g, Eve is able to respond with an appropriate move, namely, g is defined on the node (D n , C n ). To prove this property it is sufficient to check that the node (D n , C n ) is reachable: this can be easily verified by exploiting an induction on n and the definition of g given above. We conclude that Eve has a winning strategy for the reachability game over A R,T . ◻

It is interesting to observe that the above proof also shows that the property of bounded repairability in the streaming setting is not sensitive to the notions of transducer with/without lookahead, nor to the models of aggregate/edit cost: Corollary 4.6. For two DFA R, T , the following two conditions are equivalent:

1.

there exist k ∈ N and a streaming strategy with k-lookahead that repairs L (R) into L (T ) with edit cost uniformly bounded by a constant,

2.

there exists a streaming strategy with 0-lookahead that repairs L (R) into L (T ) with aggregate cost uniformly bounded by (1 + dag(R) ) ⋅ T .

Complexity analysis

In this section we analyse the complexity of the bounded repair problem and the threshold problem, distinguishing, in both cases, between the non-streaming and streaming settings and between NFA-and DFA-based specifications of regular languages. We will also consider special cases where the restriction or the target languages are fixed, and when the restriction language is universal (i.e. no restriction).

The bounded repair problem in the non-streaming setting

NFA vs NFA. Theorem 4.1 leads straightforwardly to a polynomial-space algorithm that solves the bounded repair problem between two NFA R and T in the non-streaming setting: the algorithm first guesses universally a path π = C 1 ...C k in dag(R), then it guesses existentially a path τ = D 1 ...D k of the same length in dag * (T ), and finally it checks the containment of the sub-automaton R C i in the sub-automaton T D i for all indices 1 ≤ i ≤ n (these containments can be checked in polynomial space [START_REF] Stockmeyer | Word problems requiring exponential time: preliminary report[END_REF]). Together with the PSPACE lower bound proved later in Corollary 5.10 (which deals with the unrestricted case), we obtain: Corollary 5.1. The bounded repair problem in the non-streaming setting, where both the restriction and target languages are specified by NFA, is PSPACEcomplete.

NFA vs DFA. The same characterization result can be used to solve the bounded repair problem when the restriction language is specified by an NFA and the target language is specified by a DFA. In this case, we can take advantage of the determinism and show that the problem becomes coNP-complete: Theorem 5.2. The bounded repair problem in the non-streaming setting, where the restriction language is specified by an NFA and the target language is specified by a DFA, is in coNP and it is coNP-hard already for languages specified by DFA.

Before turning to the proof of the above theorem, we establish the following complexity result for the coverability problem: Lemma 5.3. Given two NFA R and T and a path π = C 1 . . . C k in dag(R), the problem of deciding whether π is covered by some path in dag * (T ) is in PTIME with an oracle for deciding containment of the languages L (R C i ) inside language of the form L (T D), with D SCC of T .

Proof. The basic idea for checking whether the path π is covered by some path in dag * (T ) is to incrementally process longer and longer prefixes of π while keeping the frontier of the paths in dag * (T ) that cover these prefixes. Algorithm 5.1 below gives the pseudo-code for a procedure that implements this idea:

Algorithm 5.1: PathCoverability(R, T , π) ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ let π = C 1 . . . C k let dag * (T ) = (V ′ , E ′ ) F ← ∅ for all D ∈ V ′ do if CheckContainment(R, T , C 1 , D) then F ← F ∪ {D} for i ← 2 to k do ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ F ′ ← F F ← ∅ for all D ′ ∈ F ′ and (D ′ , D) ∈ E ′ do if CheckContainment(R, T , C i , D) then F ← F ∪ {D} return (F ≠ ∅)
Note that the pseudo-code uses CheckContainment(R, T , C i , D) as an oracle for deciding containment between the languages L (R C i ) and L (T D). The proof of the correctness of the algorithm is based on the following invariant: at each iteration of the loop on i, the set F contains a SCC D of T iff there is a path τ = D 1 . . . D i in dag * (T ), with D i = D, that covers π i = C 1 . . . C i . The described procedure runs in polynomial time with respect to the size of the input NFA R and T . ◻ Proof of Theorem 5.2. We first prove the complexity upper bound. Let R be an NFA and T be a DFA. Thanks to Theorem 4.1, deciding whether cost(L (R), L (T )) < ∞ amounts at first guessing universally a path π in dag(R) (this can be done in coNP) and then checking whether π is covered by some path in dag * (T ). By Lemma 5.3, this can be done efficiently using an oracle for checking containment of languages recognized by SCCs of R and T . What remains to be done is to show that one can decide in polynomial time the containment of any language L (R C) inside any language L (T D), where C (resp., D) is a SCC of the NFA R (resp., DFA T ) -note that, strictly speaking, the sub-automaton T D is not deterministic, since its successful runs can start from arbitrary states in D. To show this we use Lemma 4.4, which reduces the containment problem L (R C) ⊆ L (T D) to a series of containment problems between a non-deterministic sub-automaton of R (i.e., R q C for some q ∈ C) and a deterministic sub-automaton of T (i.e., T r D for some r ∈ D). Since deterministic automata can be easily complemented, the latter instances of the containment problem can be decided in polynomial time by reducing to an emptiness problem involving the intersection of two automata (i.e., R q C and the complement of T r D).

Putting all together, we have that the bounded repair problem in the nonstreaming setting, where the restriction language is given by an NFA and the target language is given by a DFA, is in coNP.

We now prove the lower bound, which follows from a reduction from the validity problem for propositional formulas in disjunctive normal form (i.e., the dual of the SAT problem). The general idea is to encode in the restriction language all the possible valuations for the propositional variables and then restrict the target language to consist only of encodings of valuations that satisfy at least one clause of the formula. We further allow some redundancy in the encodings of the valuations in order to forbid the repair strategy from modifying the encoded valuations.

We consider a set X = {x 1 , . . . , x k } of propositional variables and we denote by L = {x 1 , . . . , x k } ∪ {¬x 1 , . . . , ¬x k } the corresponding set of literals. For the sake of brevity, we identify ¬¬x i with x i . A valuation for the variables in X can be viewed as a subset V of L such that, for every literal l ∈ L, we have l ∈ V iff ¬l ∉ V. Let us consider a formula in disjunctive normal form

ϕ = ⋁ 1≤i≤m ⋀ 1≤j≤h i l i,j
with l i,j ∈ L for every pair of indices 1 ≤ i ≤ m and 1 ≤ j ≤ h i . Below, we describe suitable restriction and target languages R and T such that R can be repaired into T with uniformly bounded cost iff ϕ is valid, namely, if for every valuation V, there is an index 1 ≤ i ≤ m such that l i,1 , . . . , l i,h i ∈ V.

We define the restriction language over the alphabet Σ = L to be

R = def ({x 1 } * ∪ {¬x 1 } * ) ({x 2 } * ∪ {¬x 2 } * ) . . . ({x k } * ∪ {¬x k } * ).
Note that it is easy to construct a DFA R that recognizes R and that has size polynomial in the number of variables used by ϕ. Similarly, we define the target language over the alphabet ∆ = {a 1 , . . . , a m } ∪ L to be

T = def ⋃ 1≤i≤m {a i } (L ∖ {¬l i,1 , . . . , ¬l i,h i }) * .
Again, it is easy to construct a DFA T that recognizes T and that has size linear in the number of clauses of ϕ and in the number of its variables. We verify that R can be repaired into T with uniformly bounded cost iff ϕ is valid. For the right-to-left implication, suppose that ϕ is valid and let u be a word in R. Clearly, u is of the form (l 1 . . . l 1 ) (l 2 . . . l 2 ) . . . (l k . . . l k ), with l i ∈ {x i , ¬x i } for all 1 ≤ i ≤ k. Such a word encodes the valuation V u = {l 1 , l 2 , . . . , l k }. Moreover, since ϕ is valid, there is an index 1 ≤ i ≤ m such that l i,1 , . . . , l i,h i ∈ V. The repair strategy f for R and T could then map the word u to the word f(u) = a i u, which clearly belongs to T . As for the converse implication, we assume that ϕ is not valid. This means that there is a valuation V = {l 1 , l 2 , . . . , l k }, with l i ∈ {x i , ¬x i } for all 1 ≤ i ≤ k, such that for every index 1 ≤ i ≤ m, there is an index 1 ≤ j ≤ h i satisfying l i,j ∉ V. We then consider the family of words u n = (l 1 ) n (l 2 ) n . . . (l k ) n . We know that for every 1 ≤ i ≤ m, there is 1 ≤ j ≤ h i such that the edit distance between the sub-word (¬l i,j ) n of u n and any word in the sub-language T i = {a i } (L ∖ {¬l i,1 , . . . , ¬l i,h i }) * of T is at least n. This shows that all repair strategies of R into T have unbounded cost. ◻

Fixed restriction or target. Here, we briefly outline some parametrized complexity results. Quite surprisingly, the bounded repair problem in the nonstreaming setting becomes tractable when we fix either the restriction language or the target language.

Proposition 5.4. Let R be a fixed restriction language. The problem of deciding, given a DFA T , whether cost(R, L (T )) < ∞ is in PTIME.

Proof. The proof is similar to the part of the proof of Theorem 5.2 related to the coNP upper bound. Let R be a fixed restriction language and let R be a DFA that recognizes R. Moreover, let T be a given DFA recognizing the target language T . From Theorem 4.1, deciding whether cost(R, L (T )) < ∞ amounts at checking that every path π in dag(R) is covered by some path in dag * (T ).

In virtue of Lemma 5.3 and Lemma 4.4, coverability of a given path in dag(R) by paths in dag * (T ) can be decided in polynomial time. Since the number of paths in dag(R) is fixed, this shows that the problem is in PTIME. ◻ Proposition 5.5. Let T be a fixed target language. The problem of deciding, given an NFA R, whether cost(L (R), T ) < ∞ is in PTIME.

Proof. The polynomial-time solution to the bounded repair problem under a fixed target language T = L (T ) uses a dynamic programming approach and the characterization of Theorem 4.1 (hence it is similar to the proof of Theorem 5.2). However, instead of guessing a path π in dag(R) and then checking whether π is covered by some path τ in dag * (T ), we compute a succinct representation of all instances of the coverability relation. More precisely, we aim at representing the set P of all pairs (π, Π), where π is any path in dag(R) and Π is the set of all and only the paths in dag * (T ) that cover π. Note that this set P can be constructed inductively starting from the paths of length 1 and considering, at each step, the possible prolongations by single components. Because the set P might have size exponential in the number of components of R, we need to succinctly represent it by abstracting all paths in it with their shallowest components. Formally, we replace any pair (π, {τ 1 , . . . , τ }) in P, where π = C 1 . . . C k and τ i = D i,1 . . . D i,k for all 1 ≤ i ≤ , with the corresponding pair (C k , F), where F = {D 1,k , . . . , D ,k }. This abstraction is correct because paths ending in the same component behave similarly with respect to the coverability properties of their prolongations. Algorithm 5.2 below implements such an idea.

Algorithm 5.2: AllPathsCoverability(R, T )

⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ let dag(R) = (V, E) let dag * (T ) = (V ′ , E ′ ) P ← ∅ for all C ∈ V do ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ F ← ∅ for all D ∈ V ′ do if CheckContainment(R, T , C, D) then F ← F ∪ {D} P ← P ∪ {(C, F)} for k ← 2 to V do ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ for all (C, F) ∈ P and (C, C ′ ) ∈ E do ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ F ′ ← ∅ for all D ∈ F and (D, D ′ ) ∈ E ′ do if CheckContainment(R, T , C ′ , D ′ ) then F ′ ← F ′ ∪ {D ′ } P ← P ∪ {(C ′ , F ′ )} return (∀ (C, F) ∈ P. F ≠ ∅)
The proof that the algorithm is correct, namely, that it terminates successfully iff every path π in dag(R) is covered by some path in dag * (T ), relies on the following invariant: at each iteration of the loop on k, the set P contains all pairs (C, F) such that (i) there exists a path π ∈ dag(R) that ends in C and has length at most k and (ii) the set F consists of all and only the shallowest components of the paths in dag * (T ) that cover π. Moreover, we observe that every instruction used in the pseudo-code of the algorithm (including the calls to the subroutine CheckContainment(R, T , C, D)) requires time polynomial in the size of the arguments (recall, for instance, Lemma 4.4). Finally, since the set P has size at most R × 2 T and T is fixed, we conclude that the algorithm runs in polynomial time with respect to the size of R. ◻

The bounded repair problem in the streaming setting

DFA vs DFA. The characterization of Theorem 4.3 shows that the problem of deciding the existence of a streaming repair strategy with uniformly bounded (aggregate or edit) cost for two languages specified by DFA R and T amounts at solving a reachability game over a suitable directed acyclic graph A R,T . In particular, we observe that A R,T can be computed from R and T in polynomial time, and that checking containment of languages recognized by SCCs of automata is in PTIME. Moreover, it is known that the problem of deciding the winner of reachability games over directed acyclic graphs is PTIME-complete [START_REF] Papadimitriou | Computational Complexity[END_REF][START_REF]Automata, Logics, and Infinite Games: a guide to current research[END_REF]. This shows that the bounded repair problem for DFA in the streaming setting is PTIME-complete:

Corollary 5.6. The bounded repair problem in the streaming setting, where the restriction and target languages are specified by DFA, is PTIME-complete.

NFA vs NFA. Of course, the problem becomes more difficult when the languages are specified by NFA. In this case we are not able to provide tight complexity bounds, and we only claim that the complexity of the bounded repair problem for NFA in the streaming setting is between PSPACE and EXPTIME.

The lower bound will follow from Corollary 5.10 below and the upper bound from the standard subset construction on NFA:

Corollary 5.7. The bounded repair problem in the streaming setting, where the restriction and target languages are specified by NFA, is in EXPTIME and it is PSPACE-hard.

DFA vs NFA. We analyse here the complexity of the bounded repair problem in the streaming setting where one of the two input automata is a DFA and the other is an NFA. In these cases, we can improve the upper bounds from EXPTIME to PSPACE:

Theorem 5.8. The bounded repair problem in the streaming setting, where the restriction language is specified by a DFA and the target language is specified by an NFA, is PSPACE-complete.

The bounded repair problem in the streaming setting, where the restriction language is specified by an NFA and the target language is specified by a DFA, is in PSPACE.

Proof. For both claims we make use of the characterization given by Theorem 4.3. We first deal with the case where the restriction language is given by a DFA R and the target language is given by an NFA T . As a preliminary remark, observe that, in this case, PSPACE-hardness will follow again from Corollary 5.10 (below). As for the PSPACE upper bound, we denote by det(T ) the DFA obtained from T by applying the standard subset construction, and we recall that, by Theorem 4.3, there is a streaming repair strategy for L (R) and L (T ) (= L (det(T ))) of uniformly bounded aggregate/edit cost iff Eve wins the reachability game over the arena A R,det(T ) . The crucial observation is that the longest collection of moves of Adam in the arena A R,det(T ) is linear in the size of dag(R). This implies that the length of any play is at most dag(R) and hence we can simulate the reachability game over A R,det(T ) by an alternating polynomial-time procedure [START_REF] Papadimitriou | Computational Complexity[END_REF]. Precisely, we can keep track of the configuration of the reachability game by maintaining the current SCC C of R and (a symbolic representation of) the current SCC D of det(T ) (note that a SCC of det(T ) can be specified by a single state of det(T ) or, equivalently, by a set of states of T ). At each round of the reachability game, we need to check a language containment L (R C) ⊆ L (det(T ) D): this can be done using the characterization given in Lemma 4.5 and a polynomial-space subroutine based on symbolic reachability analysis. What we have described is an alternating polynomial-time procedure that simulates the reachability game over A R,det(T ) using a polynomial-space subroutine for language containment. Overall, this shows that, when the restriction language is given by a DFA, the bounded repair problem in the streaming setting is in PSPACE. We now turn to the case where the restriction language is given by an NFA T and the target language is given by a DFA T . As in the previous proof, we have to simulate the reachability game over the arena A det(R),T that results from the main characterization result. However, we cannot obtain a polynomial bound to the length of the plays since dag(R) has potentially exponential height. The idea here is that it is possible to modify the definition of the arena A det(R),T (and thus the resulting reachability game) by allowing Adam to move down the graph dag(det(R)) using shortcuts, namely, by allowing Adam to move from any SCC of det(R) to some descendant of it (rather than simply a successor of it). On the one hand, allowing this freedom in the new reachability game clearly makes it easier for Adam to win. On the other hand, if Adam wins in the modified arena, then he can also win in the original arena via longer plays. We now argue that, if Adam wins the modified reachability game, then he can do so with a polynomial number of moves. Indeed, a winning strategy of Adam consists in pushing Eve towards a sink node; this however can be done in at most n rounds, where n is the height of the DAG of SCCs of T , by properly choosing shortcut moves. The above arguments show that the two versions of the reachability games are equivalent and, furthermore, one can bound the length of the plays to a polynomial in the size of the DFA T . Therefore, the bounded repair problem for L (R) and L (T ) in the streaming setting can be solved by an alternating polynomial-time procedure similar to the one described above. This shows that, when the target language is given by a DFA, the bounded repair problem in the streaming setting is in PSPACE. ◻

The bounded repair problem in the unrestricted case

We now consider the unrestricted case of the bounded repair problem, namely, the case where the restriction language is assumed to be Σ * and the target language T is specified by a finite state automaton.

The following result adapts the characterization theorems presented in Section 4 to give a necessary and sufficient condition for bounded repairability in the unrestricted case. This result, which can be viewed as a special case of both Theorem 4.1 and Theorem 4.3, also shows that there is no difference between the non-streaming and the streaming settings when the restriction language is universal.

Corollary 5.9. Given an alphabet Σ and an NFA T , the following conditions are equivalent:

1. cost(Σ * , L (T )) < ∞, 2. Σ * ⊆ L (T D) for some component D of T , 3.
cost aggr 0-lookahead (Σ * , L (T )) ≤ 2 T . Using the above characterization, one can easily devise a non-deterministic logarithmic-space algorithm that solves the bounded repair problem for DFA in the unrestricted (streaming or non-streaming) setting. Indeed, if the target automaton T is a DFA and D is a component of T , then we have Σ * ⊆ L (T D) iff for every symbol a ∈ Σ and every state r ∈ D, T contains a transition of the form (r, a, r ′ ), with r ′ ∈ D. Checking this property amounts to performing a standard NLOGSPACE reachability analysis over T . Conversely, NLOGSPACE-hardness follows from the fact that the emptiness problem for DFA is reducible to the bounded repair problem: given a DFA A over an alphabet Σ, we have that L (A) ≠ ∅ iff Σ * is repairable into L (A ′ ) with uniformly bounded cost, where A ′ is a DFA that recognizes the language Σ * L (A) and that can be constructed from A in logarithmic space.

In a similar way, one can show that the bounded repair problem for NFA in the unrestricted case is PSPACE-complete. This follows from Corollary 5.9 and from suitable reductions to/from the universality problem for NFA. Indeed, checking whether a target NFA T has a SCC D such that Σ * ⊆ L (T D) is equivalent to the problem of deciding whether Σ * is repairable into L (T ) with uniformly bounded cost, and it is clearly reducible to the universality problem for NFA. As for the PSPACE-hardness, we observe that a given NFA A recognizes the universal language Σ * iff (Σ ∪ {#}) * is repairable into (L (A) ⋅ {#}) * with uniformly bounded cost and # ∉ Σ. Notice that a finite automaton A ′ recognizing the language (L (A) ⋅ {#}) * can be computed in linear time from A.

We thus conclude the following:

Corollary 5.10. The bounded repair problem in the unrestricted case, where the target language is specified by a DFA (resp., NFA) is NLOGSPACE-complete (resp., PSPACE-complete).

Another consequence of Corollary 5.9 is the following. Suppose that a target language T is recognized by a DFA T that is complete over the target alphabet ∆, namely, for every symbol a ∈ ∆ and every state r of T , T contains a transition from r labelled by a (here we no more assume that T is trimmed). Consider a restriction alphabet Σ ⊆ ∆ and suppose that Σ * is not repairable into T with uniformly bounded cost. Let us consider a SCC D of T that is reachable from the initial state and terminal, namely, with no outgoing edges. We know that D does not contain any final state (otherwise, cost(Σ * , L (T )) < ∞ would follow from Corollary 5.9). In this case, however, the same component D in the complement DFA T ∁ would contain final states and hence Σ * would be repairable into L (T ∁ ) with uniformly bounded cost. This shows that: Corollary 5.11. Given an alphabet Σ and a regular language T ⊆ ∆ * , with Σ ⊆ ∆, then either cost(Σ * , T ) < ∞ or cost(Σ * , ∆ * ∖ T ) < ∞.

The threshold problem in the non-streaming setting

We now consider the problem of calculating the exact repair cost in the non-streaming setting. If the restriction and target languages are specified by DFA, then we know from Theorem 5.2 that we can decide in coNP whether the worst-case repair cost is finite or infinite. Furthermore, Theorem 4.1 tells us that if the cost is finite it must be bounded by a polynomial in the input size. Thus, to determine the exact repair cost in the case where it is finite, it suffices to test whether the cost is above or below a given threshold θ ∈ N, since then we can try every number θ below the polynomial bound. Perhaps surprising, this problem is harder than the bounded repair problem, although still within polynomial space: Theorem 5.12. The problem of determining whether cost(R, T ) ≤ θ, given two languages R and T specified by DFA and given a positive number θ, is PSPACEcomplete. The same holds when R and T are specified by NFA.

Proof. We first give the upper bound, assuming that R and T are recognized by some NFA R and T . First, we recall that, by Theorem 4.1, we have either cost(R, T ) ≤ (1+ dag(R) )⋅ T or cost(R, T ) = ∞. Thus, without loss of generality, we can assume that the threshold θ ∈ N is represented in unary notation. We can then construct in polynomial time an NFA R θ that recognizes the language

R θ = def {v ∈ ∆ * ∶ ∃ u ∈ R. dist(u, v) ≤ θ}.
The automaton R θ is defined by a suitable 'juxtaposition' of θ+1 disjoint copies of R:

the states of R θ are the pairs (q, i), where q is a state of R and 0 ≤ i ≤ θ; the transitions of R θ are the triples (q, i), b, (q ′ , j) that satisfy one of the following conditions 1. i = j, b ∈ Σ, and (q, b, q ′ ) is a transition of R, 2. i < j, b ∈ ∆, and q = q ′ , 3. i < j, b ∈ ∆, and there is a transition (q, a, q ′ ) of R, with a ∈ Σ, 4. i < j, b ∈ Σ, and there are two transitions (q, a, q ′′ ) and (q ′′ , a ′ , q ′ ) of R, with a, a ′ ∈ Σ and b ∈ {a, a ′ }; the initial (resp., final) states of R θ are the pairs (q, i), where q is an initial (resp., final) state of R and 0 ≤ i ≤ θ. Note that the automaton R θ can be constructed in polynomial time from R and θ when θ is represented in unary. Moreover, R θ accepts all and only the words that are at distance at most θ from some words in R, and hence L (R θ ) = R θ . Finally, it is easy to see that

cost(R, T ) ≤ θ iff R θ ⊆ T .
This reduces the threshold problem cost(R, T ) ≤ θ to a containment problem between languages recognized by NFA, which is known to be in PSPACE [START_REF] Stockmeyer | Word problems requiring exponential time: preliminary report[END_REF].

We now discuss the PSPACE lower bound, which holds even for languages specified by DFA. It is via reduction from the problem of tiling a corridor of polynomial width (and unbounded height). An instance of the latter problem is given by a number n (i.e., the width of the corridor, represented in unary notation), a set S of available tiles, some sets H, V ⊆ S × S of vertical and horizontal constraints, and two tiles t and t ⊺ for the bottom and top rows. A tiling of height N (for an instance I = (n, S, H, V, t , t ⊺ )) is a mapping g from the pairs (i, j) ∈ [1, N] × [1, n] to the tiles in S such that g(1, j) = t and g(N, j) = t ⊺ for all 1 ≤ j ≤ n. We say that the tiling g satisfies the constraints of I if 1.

g(i, j), g(i, j + 1) ∈ H for all 1 ≤ i ≤ N and all 1 ≤ j < n,

2.

g(i, j), g(i + 1, j) ∈ V for all 1 ≤ i < N and all 1 ≤ j ≤ n.

The corridor tiling problem is the problem of deciding, given a tiling instance I = (n, S, H, V, t , t ⊺ ), whether there is a tiling g of some height N ≥ 1 that satisfies the constraints in I. This problem is known to be PSPACE-complete [START_REF] Van Emde | The convenience of tilings[END_REF]. Hereafter, we fix an instance I = (n, S, H, V, t , t ⊺ ) of the corridor tiling problem and a threshold θ ≥ 1 (note that for θ = 0 the threshold problem becomes a containment problem between DFA, which is clearly solvable in polynomial time). Moreover, we assume that the threshold θ is represented in unary notation (clearly this does not make the threshold problem more difficult). Below, we reduce the corridor tiling problem for the instance I to a threshold problem for two DFA R and T .

We let the restriction alphabet Σ consist of pairs of the form ⟨t, j⟩, where t is a tile from S and j is a number in {1, . . . , n}. The restriction language R contains "(θ + 1)-redundant" encodings of tilings, namely, words of the form

⟨g(1, 1), 1⟩ θ+1 . . . ⟨g(1, n), n⟩ θ+1 . . . . . . ⟨g(N, 1), 1⟩ θ+1 . . . ⟨g(N, n), n⟩ θ+1
where N is a positive natural number and g ∶ [1, N] × [1, n] → S is a tiling of height N that satisfies the horizontal constraints and the constraints on the bottom and top rows (but possibly not the vertical constraints). We claim that the above language is recognized by a DFA R of size polynomial in I and in θ: indeed, the automaton R needs to check that the input word is well-formed, which requires enforcing the horizontal constraints and the initial and final tile requirements (which clearly can be done with a fixed number of states) and counting up to θ + 1 and n (which clearly can be done with a number of states linear in θ and n).

We now turn to the definition of the target language. Its alphabet ∆ contains all symbols of the restriction alphabet Σ plus marked symbols ⟨t, j⟩, with t ∈ S and 1 ≤ j ≤ n. The marked symbols ⟨t, j⟩ are used to highlight a violation of the vertical constraints in such a way that it becomes easy for an automaton to certify it. Intuitively, a violation of a vertical constraint is certified on a word v ∈ ∆ * when v contains a marked symbol of the form ⟨t, j⟩ at some position x and a symbol ⟨t ′ , j⟩, with (t, t ′ ) ∉ V, at position x + (θ + 1) ⋅ n (this would imply that the tile t ′ is adjacent to t along the vertical axis). More precisely, the target language is defined as follows:

T = def ⋃ (t,t ′ )∉V 1≤j≤n Σ * ⟨t, j⟩ ⟨t, j⟩ θ Σ (θ+1)⋅(n-1) ⟨t ′ , j⟩ (θ + 1) ⋅ n positions ⟨t ′ , j⟩ θ Σ * .
It is easy to construct a DFA T of size polynomial in I and θ that recognizes the language T . We now argue that there is a repair strategy for R into T with cost uniformly bounded by θ iff every tiling g ∶ [1, N] × [1, n] → S violates the constraints in I. On the one hand, suppose that every tiling g ∶ [ where g is a tiling of

[1, N] × [1, n] → S.
From the previous assumptions, we know that g violates the vertical constraints in I. This implies that there are 1 ≤ i < N and 1 ≤ j ≤ n such that g(i, j), g(i + 1, j) ∉ V, and hence there are two positions x (= j+(i-1)⋅(θ+1)⋅n) and x+(θ+1)⋅n (= j+(i-1)⋅(θ+1)⋅n+(θ+1)⋅n) in u that contain the symbols ⟨g(i, j), j⟩ and ⟨g(i + 1, j), j⟩, respectively. Marking the first of these two occurrences (i.e., replacing the symbol ⟨g(i, j), j⟩ at position x with the symbol ⟨g(i, j), j⟩) will bring us into the target language T . This shows that there is a repair strategy for R and T with worst-case cost at most 1 (≤ θ).

On the other hand, suppose that there is a tiling g ∶ [1, N] × [1, n] → S that satisfies the constraints in I. Let u be the corresponding word: ⟨g(1, 1), 1⟩ θ+1 . . . ⟨g(1, n), n⟩ θ+1 . . . . . . ⟨g(N, 1), 1⟩ θ+1 . . . ⟨g(N, n), n⟩ θ+1 .

Clearly, u belongs to the restriction language R. We claim that no matter how we repair u by at most θ edits, the resulting sequence will not belong to the target language T . Consider a word v produced by such an edit. If there are no occurrences of marked symbols in v, then v cannot belong to T , and similarly if there are more than one occurrence of a marked symbol. Suppose that v contains exactly one occurrence of a marked symbol, say v[x] = ⟨t, j⟩, and let v[x + (θ + 1) ⋅ n] = ⟨t ′ , j ′ ⟩. We distinguish between the following cases:

1. v[x + i] ≠ ⟨t, j⟩ for some 1 ≤ i ≤ θ, 2. j ′ ≠ j or v[x + (θ + 1) ⋅ n + i] ≠ ⟨t ′ , j ′ ⟩ for some 1 ≤ i ≤ θ, 3. j ′ = j and v[x + i] = ⟨t, j⟩ and v[x + (θ + 1) ⋅ n + i] = ⟨t ′ , j⟩ for all 1 ≤ i ≤ θ.
In the first two cases, v cannot belong to T . In the third case, since v was obtained from u by applying at most θ edit operations, we know that u contains a sub-string of the form ⟨t, j⟩ θ+1 Σ (θ+1)⋅(n-1) ⟨t ′ , j⟩ θ+1 .

Since u is an encoding of a valid tiling g, we have that (t, t ′ ) ∈ V. This shows again that v cannot belong to the target language T . ◻ current state s of S and move from each node (q, r, c, a) to a successor node (q, r ′ , c ′ ) such that r ′ = δ(r, v), c ′ = c + dist(a, v), and δ ′′ (s, a) = (v, s ′ ).

To conclude the proof we need show that, assuming cost aggr 0-lookahead (R, T ) ≤ θ, one can compute in polynomial time a streaming 0-lookahead repair strategy for R and T that has aggregate cost at most θ. However, this follows immediately from the fact that (i) given the arena A θ R,T whose reachability game is won by Eve, one can construct in polynomial time a winning positional strategy f for Eve, and (ii) using Eve's winning strategy f, one can construct in polynomial time a repair strategy S for R and T such that cost aggr S (R, T ) ≤ θ (for this we use again the above arguments). ◻

Note that in the above result we deal with the model of aggregate cost, which is very different the model of edit cost (the main characterization result, however, shows that one is uniformly bounded iff the other is). We do not know if finding the exact edit cost for two languages specified by DFA is even tractable. Similarly, we do not know whether the threshold problem for streaming repair strategies with k-lookahead is tractable, where the parameter k is represented in binary.

Connections to distance automata and games

Both the non-streaming and streaming repair problems correspond to special cases of prior problems studied in automata and games. The non-streaming bounded repair problem corresponds to the limitedness problem for distance automata, while the streaming variant corresponds to energy games. We explain the correspondences in detail now. In each case, however, we find that the results for the more general framework do not give tight complexity bounds.

Non-streaming repairs and distance automata. Intuitively, a distance automaton is a transducer D that receives as input a finite word u and outputs a corresponding cost D(u) in N ∞ = N ∪ {∞}. Formally, a distance automaton is a transducer of the form D = (Σ, Q, E, I, F), where Σ is the input alphabet, Q is a finite set of states, E ⊆ Q × Σ × N ∞ × Q is the transition relation, and I, F ∶ Q → N ∞ are the initial and final cost functions. The cost D(u) on input u = a 1 . . . a n ∈ Σ * is obtained by taking the minimum among the costs of the runs of D on u, where the cost of each run q 0 a1 c1 -→ q 1 a2 c2 -→ . . . an cn -→ q n is defined as I(q 0 ) + ∑ n i=1 c i + F(q n ) -in particular, every transition of the run has a cost, as well as the beginning and the end of the run. We let D(u) = ∞ if D admits no successful run on w.

The main problem that has been studied for distance automata is the limitedness problem, which consists of deciding whether there exists a finite upper bound to the cost D(u) computed by a given distance automaton D for all words u ∈ Σ * such that D(u) < ∞. This problem was shown decidable by Hashigushi [START_REF] Hashiguchi | Improved limitedness theorems on finite automata with distance functions[END_REF]; later in [START_REF] Leung | The limitedness problem on distance automata: Hashiguchi's method revisited[END_REF] it was shown to be PSPACE-complete. Distance automata have been related to edit-distance problems in several prior works -see Section 7 for further discussion of the connections. Here we only provide a simple reduction of the bounded repair problem to the limitedness problem. absolute value. As a matter of fact, the latter complexity result implies that energy games can be solved in polynomial time with respect to the size of the arena, provided that the weights are represented in unary.

One can easily reduce the bounded repair problem in the streaming setting, under the aggregate cost model for languages recognized by DFA, to the finite initial credit problem for energy games. Informally, the choice of the opponent in the energy game corresponds to the letters emitted by the restriction, while the edits correspond to choices of the energy player. More formally, we have a node in the arena for each pair of states of the restriction DFA R and of the target DFA T -call this node a Restriction Player Node. We also have a node for each combination of restriction state, target state, and letter played -call this a Target Player Node. The former represents the pair of states reached by the restriction and target automata after parsing the unedited and edited words, respectively; the latter adds the last letter emitted by the restriction. There is an edge of weight 0 going from a Restriction Player Node (p, p ′ ) to any Target Player Node (q, p ′ , a) whenever (p, a, q) is a valid transition of R. Similarly, there is an edge of weight -c going from a Target Player Node (q, p ′ , a) to a Restriction Player Node (q, q ′ ) whenever there is a word v at distance c from a (i.e. dist(a, v) = c) such that T can move from p ′ to q ′ consuming v. Clearly, the energy player wins the game using some initial credit of energy if and only if the cost of repairing L (R) into L (T ) is uniformly bounded. Note that this reduction provides a PTIME upper bound to the complexity of the bounded streaming repair problem for DFA, given that the size of the resulting arena is polynomial in the size of the restriction and target DFA and, moreover, the weights are bounded by the size of the target DFA.

Our characterization result (see Theorem 4.3) gives analogous (tight) complexity bounds for bounded repairability languages recognized by DFA and, moreover, it proves that the bounded repair problem in the streaming setting is not sensitive to the models of aggregate/edit cost. They also provide tight bounds for special cases of the problem, which cannot naturally be captured in the setting of energy games. It is also worth mentioning that the repair strategy that arises from our characterization result can be seen as a special case of the notion of good-for-energy strategy, which is introduced in [START_REF] Chatterjee | Energy parity games[END_REF] to solve energy parity games.

Despite the connections mentioned above, many concepts and problems concerning repair do not have natural analogs in the game setting, and vice versa. For instance, in the game setting one could allow lookahead for one player, but it is not as natural as in the repair setting. Moreover, while the aggregate cost metric fits the game setting naturally, our usual cost function does not. Conversely, the binary weights that are allowed in the game setting have no natural analog in the context of edits. Our characterization finally allows us to easily isolated special cases of lower complexity that are not easily seen from the embedding into energy games.

Conclusions and Related Work

In this work we have investigated the problem of repairing documents between different specifications. In our basic setting, a document is represented by a string and a specification by a language. Specifically, we gave a characterization of those pairs of regular languages such that one can repair any string in the first language to a string in the second, using a uniformly bounded number of edits and repair processors that either read the entire string offline and then edit, or have the form of sequential real-time transducers. We then used the characterizations to provide complexity bounds for the considered bounded repair problems. These complexity bounds are summarized in Table 1 and Table 2 -in the non-streaming setting all bounds are tight (indicated by a single class), while in the streaming setting we have several gaps (indicated by cells with lower and upper bounds). We omit the corresponding table for computing the exact cost: in the case of non-streaming repair we can derive tight bounds in all cases, and also in the case of streaming repair for aggregate cost. In the latter case we also know the complexity of computing the optimal stream repair processor.

Related Work. The problem of finding the minimal distance of a string to a regular language was first considered by Wagner in [START_REF] Wagner | Order-n correction for regular languages[END_REF], who showed that the problem could be solved by adapting the dynamic programming approach, giving a polynomial time algorithm. Several authors have extended the definition to deal with distances between languages. Mohri [START_REF] Mohri | Edit-distance of weighted automata: general definitions and algorithms[END_REF] defines a distance function between two languages, and more generally between string distributions: in the case of languages, this is the minimum distance between two strings in the two respective languages, which is appropriate for many applications. Konstantinidis [START_REF] Konstantinidis | Computing the edit distance of a regular language[END_REF] focuses on the minimum distance between distinct strings within the same language, giving tractable algorithms for computing it. Our notion of "distance" is quite distinct from this, since it is asymmetric in the two lan-guages, focusing on the maximum of the distance of a string in one language to the other language. As a matter of fact, this notion of distance between languages can be seen as a special case of a more general concept, known as Hausdorff distance. This latter notion has been studied also in [START_REF] Choffrut | Distances between languages and reflexivity of relations[END_REF], but within a more general setting; in particular, with respect to a generalization of the boundedness property called "almost reflexivity".

Grahne and Thomo [START_REF] Grahne | Query answering and containment for regular path queries under distortions[END_REF] consider a related problem of "approximate containment" of regular expressions. Expressions are evaluated with respect to an edge-labelled graph and are given a numerical semantics by a "distortion", a generalization of the notion of edit distance. Approximate containment of T 1 and T 2 means, roughly speaking, that for every input graph R and every word w generated by R, the distance to target T 1 is bounded by the distance to T 2 . Grahne and Thomo also study "k-containment" (distance to T 1 is at most k more than T 2 ) and "approximate containment" (k-containment for some k), relying primarily on a reduction to the limitedness problem for distance automata. Their problem differs in several fundamental respects from ours: they are interested in bounding the difference over all words, not just the worst-case; in addition, they quantify over all restrictions (databases, in their terminology).

An entire line of research in XML data management has dealt with comparisons and matching algorithms between schema languages. Many of these lift edit distance between trees to the level of schemas (i.e. languages) -see, for example, [START_REF] Do | COMA -a system for flexible combination of schema matching approaches[END_REF]. However, in those cases the lifting is done by looking at the syntactic structure of the schema description, rather than at the instance level (distance between documents in each schema).

An extended abstract of this work appeared in [START_REF] Benedikt | Regular repair of specifications[END_REF].

Example 1 .

 1 Consider the regular languages R = a * b * and T = a * c b * . Clearly, any string in R can be converted to a string in T with at most 1 edit operation, namely, cost(R, T ) = 1; a repair strategy that achieves this cost maps any word a n b m ∈ R to the word a n c b m ∈ T .

Example 2 .

 2 Consider the languages R = (a + b) c * (a * + b * ) and T = a c * a * + b c * b * .

Theorem 4 . 1 .

 41 Given two NFA R and T , the following conditions are equivalent 1.

  1, N] × [1, n] → S violates the constraints in I. Let us consider a word u ∈ R of the form

	⟨g(1, 1), 1⟩

θ+1 . . . ⟨g(1, n), n⟩ θ+1 . . . . . . ⟨g(N, 1), 1⟩ θ+1 . . . ⟨g(N, n), n⟩ θ+1

Table 1 :

 1 Bounded repair problem in the non-streaming setting

			fixed	DFA	NFA
	universal LOGSPACE NLOGSPACE PSPACE
		fixed	Const	PTIME	PSPACE
		DFA	PTIME	coNP	PSPACE
		NFA	PTIME	coNP	PSPACE
		fixed		DFA	NFA
	universal	LOGSPACE	NLOGSPACE	PSPACE
	fixed	Const		PTIME	PSPACE
	DFA	PTIME	PTIME	PSPACE
	NFA	PTIME-PSPACE PTIME-PSPACE PSPACE-EXPTIME

Table 2 :

 2 Bounded repair problem in the streaming setting

The threshold problem in the streaming setting

For the streaming setting, if we consider 0-lookahead repair strategies with aggregate cost, the threshold problem becomes solvable in polynomial time (hence it is as difficult as the bounded repair problem). Indeed, one can easily reduce this threshold problem to a reachability game over a suitable arena that is constructed in polynomial time from the restriction and target DFA R and T and from the threshold θ. It follows from this reduction that one can efficiently compute in polynomial time a streaming repair strategy for R and T whose aggregate cost does not exceed the threshold θ.

Theorem 5.13. The problem of determining whether cost aggr 0-lookahead (R, T ) ≤ θ, given two languages R and T specified by DFA and given a numbers θ, is in PTIME. Moreover, if cost aggr 0-lookahead (R, T ) ≤ θ, then one can compute in polynomial time a streaming 0-lookahead repair strategy for R and T that has aggregate cost at most θ.

Proof. Let R = (Σ, Q, δ, q 0 , F) and T = (∆, Q ′ , δ ′ , r 0 , F ′ ) be two DFA, let R and T be the recognized languages, and let θ be the threshold for the aggregate cost. As a preliminary remark, we observe that, without loss of generality, we can assume that θ is represented in unary: indeed, we know from Theorem 4.3 and Corollary 4.6 that either there is a streaming repair strategy for R and T with aggregate cost uniformly bounded by (1+ dag(R) )⋅ T (i.e., a polynomial in the size of R and T ), or all streaming repair strategies for R and T have unbounded aggregate cost.

We define a reachability game over an arena A θ R,T that characterizes the threshold problem for R and T in the streaming setting. The nodes of the arena are the pairs (q, r, c) and (q, r, c, a), with q ∈ Q, r ∈ R, c ∈ {0, . . . , θ}, and a ∈ Σ. The former nodes are owned by Adam (i.e., the player entitled to emit a word in the restriction language) and the latter nodes are owned by Eve (i.e., the player entitled to repair the given word into the target language). The arena A θ R,T has an edge (q, r, c) → (q ′ , r, c, a) if δ(q, a) = q ′ , and it has an edge (q, r, c, a)

Adam plays first, starting from the node (q 0 , r 0 , 0). The player who cannot move loses. Infinite plays, which are feasible in this type of game, are won by Eve. Now, we show that Eve has a winning strategy in A θ R,T iff there is a streaming 0-lookahead repair strategy for R and T with aggregate cost at most θ. Easily, assume that Eve has a strategy f for winning the reachability game over A θ R,T . Without loss of generality, we can assume that the strategy f is positional. It is then easy to construct, using Eve's positional strategy f, a transducer S with at most Q ⋅ Q ′ ⋅ (θ + 1) states that repairs R into T with aggregate cost cost aggr S (R, T ) ≤ θ. For the other direction, suppose that there is a transducer S = (Σ, ∆, Q ′′ , δ ′′ , s 0 , Ω) that repairs every word from R into T with aggregate cost less than or equal to θ. It is straightforward to define a winning strategy for Eve using the transducer S. Indeed, we only need to maintain the Given two NFA R = (Σ, Q, E, I, F) and T = (∆, Q ′ , E ′ , I ′ , F ′ ), one can construct a distance automaton D that computes the optimal cost of repairing any word from L (R) into a word from L (T ). First of all, one associates with each symbol a ∈ Σ a matrix M(a) whose entries M(a)[p, q] are indexed over the pairs of states p, q of T and give the minimum edit-distance between the symbol a and a word v ∈ ∆ * such that T can move from p to q consuming v (if q is not reachable from p, then one simply lets M(a)[p, q] = ∞). One then defines the distance automaton D as the quadruple (Σ,

, where E M is the set of all transitions of the form (p, p ′ ), a, c, (q, q ′ ) , with a ∈ Σ, (p, a, q) ∈ E, and c = M(a)[p ′ , q ′ ]. The initial cost function I M of D is defined by letting I M (p ′ ) be the length of the minimum word that can be parsed by T when moving from an initial state to the state p ′ (if no such word exist, then I M (p ′ ) = ∞). Similarly, F M (p) is defined to be the length of the minimum word that can be parsed by T when moving from the state p to a final state (or ∞ if no such word exists). It is easy to see that the cost function computed by D maps a word u ∈ L (R) to the cost of an optimal non-streaming repair of u into L (T ). Moreover, the distance automaton D has size polynomial in the size of R and T . This reduces the bounded repair problem for NFA in the non-streaming setting to the limitedness problem for distance automata. Combining this reduction with the PSPACE upper bound for the limitedness problem, we see that the bounded repair problem for NFA is in PSPACE.

The same reduction technique can be applied to solve the bounded repair problem for DFA. In this case, however, the resulting complexity bound is not optimal: the bounded repair problem for DFA is in fact in coNP (cf. Theorem 5.2). Roughly speaking, the reason why the bounded repair problem for DFA is easier than the limitedness problem for distance automata is that the distance automata emerging from bounded repair problems have a more restricted structure (specifically, they are deterministic on the 0-cost moves). In addition to not giving tight bounds, approaches via distance automata give less insight into the problems. We invite the reader, for example, to compare the PSPACE upper bound that we derive from our characterization of bounded repairability, Theorem 4.1, with the PSPACE upper bound given in [START_REF] Leung | The limitedness problem on distance automata: Hashiguchi's method revisited[END_REF].

Streaming repairs and energy games.

Just as non-streaming repair problems can be seen within the framework of distance automata, bounded repair problems in the streaming setting are special cases of games on graphs with quantitative objectives. An interesting family of such games is that of energy games studied in [START_REF] Chakrabarti | Resource interfaces[END_REF], which are played on finite weighted arenas. The game is played between an energy player, who wants to keep the running sum of the weights (i.e. the energy) always positive, and her opponent. A variant of energy games allows the parameterization by an initial credit of energy; the higher the credit the more possibility for the energy player to win.

It is well known that the problem of determining whether there is a finite initial credit so that the energy player has a winning strategy is in NP ∩ coNP [START_REF] Chatterjee | Energy parity games[END_REF], but the exact complexity is still unknown. Furthermore, this problem can be solved in time polynomial in the size of the arena and the largest weight in