Thomas Place
email: tplace@labri.fr

Lorijn Van Rooijen

Marc Zeitoun

Separating regular languages by piecewise testable and unambiguous languages

Separation is a classical problem asking whether, given two sets belonging to some class, it is possible to separate them by a set from a smaller class. We discuss the separation problem for regular languages. We give a Ptime algorithm to check whether two given regular languages are separable by a piecewise testable language, that is, whether a BΣ1(<) sentence can witness that the languages are disjoint. The proof refines an algebraic argument from Almeida and the third author. When separation is possible, we also express a separator by saturating one of the original languages by a suitable congruence. Following the same line, we show that one can as well decide whether two regular languages can be separated by an unambiguous language, albeit with a higher complexity.

Introduction

Separation is a classical notion in mathematics and computer science. In general, one says that two structures L 1 , L 2 from a class C are separable by a set L if L 1 ⊆ L and L 2 ∩ L = ∅. In this case, L is called a separator.

In separation problems, the separator L is required to belong to a given subclass Sep of C. The problem asks whether two disjoint elements L 1 , L 2 of C can always be separated by an element of the subclass Sep.

In the case that disjoint elements of C cannot always be separated by an element of Sep, several natural questions arise: [START_REF] Almeida | Some algorithmic problems for pseudovarieties[END_REF] given elements L 1 , L 2 in C, can we decide whether a separator exists in Sep? [START_REF] Almeida | Pointlike sets with respect to R and J[END_REF] if so, what is the complexity of this decision problem? (3) can we, in addition, compute a separator, and what is the complexity? In this context, it is known for example that separation of two context-free languages by a regular one is undecidable [START_REF] Hunt | III. Decidability of grammar problems[END_REF].

Separating regular languages. In this paper, we look at separation problems for the class C of regular languages. These separation problems generalize the task of finding decidable characterizations for subclasses Sep of C which are closed under complement: a separation algorithm for a subclass Sep entails an algorithm for deciding membership in Sep (i.e., membership reduces to separability). Indeed, membership in Sep can be checked by testing whether the input language is Sep-separable from its complement.

While finding a decidable characterization for Sep already requires a deep understanding of the subclass, the search for separation algorithms is intrinsically more difficult. Indeed, powerful tools are already available to decide membership in Sep: one normally makes use of a recognizing device of the input language, viz. its syntactic monoid. A famous result along these lines is Schützenberger's Theorem [START_REF] Schützenberger | On finite monoids having only trivial subgroups[END_REF], which states that a language is definable in first-order logic if and only if its syntactic monoid is aperiodic, which is easily decidable. Now for a separation algorithm, the question is whether the input languages are sufficiently different, from the point of view of the subclass Sep, to allow this to be witnessed by an element of Sep. Note that we cannot use standard methods on the recognizing devices, as was the case for the membership problem. We now have to decide whether there exists a recognition device of the given type that separates the input: we do not have it in hand, nor its syntactic monoid. An even harder question then is to actually construct the so-called separator in Sep.

Contributions.

In this paper, we study this problem for two subclasses of the regular languages: piecewise testable languages and unambiguous languages.

Piecewise testable languages are languages that can be described by the presence or absence of scattered subwords up to a certain size within the words. Equivalently, these are the languages definable using BΣ 1 (<) formulas, that is, first-order logic formulas that are boolean combinations of Σ 1 (<) formulas. A Σ 1 (<) formula is a first-order formula with a quantifier prefix ∃ * . A well-known result about piecewise testable languages is Simon's Theorem [START_REF] Simon | Piecewise testable events[END_REF] that states that a regular language is piecewise testable if and only if its syntactic monoid is J-trivial. This property yields a decision procedure to check whether a language is piecewise testable. Stern has refined this procedure into a polynomial time algorithm [START_REF] Stern | Complexity of some problems from the theory of automata[END_REF], of which the complexity has been improved by Trahtman [START_REF] Trahtman | Piecewise and local threshold testability of DFA[END_REF].

The second class that we consider is the class of unambiguous languages, i.e., languages defined by unambiguous products. This class has been given many equivalent characterizations [START_REF] Tesson | Diamonds are forever: The variety DA[END_REF]. For example, these are the FO 2 (<)-definable languages, i.e., languages that can be defined in first-order logic using only two variables. Equivalently, this is the class ∆ 2 (<) of languages that are definable by a first-order formula with a quantifier prefix ∃ * ∀ * and simultaneously by a first-order formula with a quantifier prefix ∀ * ∃ * . Note that consequently, all piecewise testable languages are FO 2 (<)-definable. It has been shown in [START_REF] Pin | Polynomial closure and unambiguous product[END_REF] for ∆ 2 (<), and in [START_REF] Thérien | Over words, two variables are as powerful as one quantifier alternation[END_REF] for FO 2 (<) that these are exactly the languages whose syntactic monoid belongs to the decidable class DA.

There is a common difficulty in the separation problems for these two classes. A priori, it is not known up to which level one should proceed in refining the candidate separators to be able to answer the question of separability. For piecewise testable languages, this refinement basically means increasing the size of the considered subwords. For unambiguous languages this means increasing the size of the unambiguous products. For both of these classes, we are able to compute, from the two input languages, a number that suffices for this purpose. This entails decidability of the separability problem for both classes.

A rough analysis yields a 3-Nexptime upper bound for separation by unambiguous languages. For separability by piecewise testable languages, we obtain a better bound starting from NFAs: we show that two languages are separable if and only if the corresponding automata do not contain certain forbidden patterns of the same type, and we prove that the presence of such patterns can be decided in polynomial time wrt. the size of the automata and of the alphabet. This yields a Ptime algorithm for deciding separation by a piecewise testable language.

Related work. The classes of piecewise testable and unambiguous languages are varieties of regular languages. For such varieties, there is a generic connection found by Almeida [START_REF] Almeida | Some algorithmic problems for pseudovarieties[END_REF] between profinite semigroup theory and the separation problem: Almeida has shown that two regular languages over A are separable by a language of a variety A * V if and only if the topological closures of these two languages inside a profinite semigroup, depending only on A * V, intersect. Note that this theory does not give any information about how to actually construct the separator, in case two languages are separable. To turn Almeida's result into an algorithm deciding separability, we should compute representations of these topological closures, and test for emptiness of intersections of such closures.

So far, these problems have no generic answer and have been studied in an algebraic context for a small number of specific varieties. Deciding whether the closures of two regular languages intersect is equivalent to computing the so-called 2-pointlike sets of a finite semigroup wrt. the considered variety, see [START_REF] Almeida | Some algorithmic problems for pseudovarieties[END_REF]. This question has been answered positively for the varieties of finite group languages [START_REF] Ash | Inevitable graphs: a proof of the type II conjecture and some related decision procedures[END_REF][START_REF] Ribes | On the profinite topology on a free group[END_REF], piecewise testable languages [START_REF] Almeida | The pseudovariety J is hyperdecidable[END_REF][START_REF] Almeida | Pointlike sets with respect to R and J[END_REF], star-free languages [START_REF] Henckell | Aperiodic pointlikes and beyond[END_REF][START_REF] Henckell | Pointlike sets: the finest aperiodic cover of a finite semigroup[END_REF], and a few other varieties, but it was left open for unambiguous languages.

A general issue is that the topological closures may not be describable by a finite device. However, for piecewise testable languages, the approach of [START_REF] Almeida | The pseudovariety J is hyperdecidable[END_REF] builds an automaton over an extended alphabet, which recognizes the closure of the original language. This can be performed in polynomial time wrt. the size of the original automaton. Since these automata admit the usual construction for intersection and can be checked for emptiness in Nlogspace, this gives a polynomial time algorithm wrt. the size of the original automata. The construction was presented for deterministic automata but also works for nondeterministic ones. One should mention that the extended alphabet is 2 A (where A is the original alphabet). Therefore, these results give an algorithm which, from two NFAs, decides separability by piecewise testable languages in time polynomial in the number of states of the NFAs and exponential in the size of the original alphabet.

Our proof for separability by piecewise testable languages follows the same pattern as the method described above, but a significant improvement is that we show that non-separability is witnessed by both automata admitting a path of the same shape. This allows us to present an algorithm that provides better complexity as it runs in polynomial time in both the size of the automata, and in the size of the alphabet. Also, we do not make use of the theory of profinite semigroups: we work only with elementary concepts. We have described this algorithm in [START_REF] Van Rooijen | The separation problem for regular languages by piecewise testable languages[END_REF]. Furthermore, we show how to compute from the input languages, an index that suffices to separate them. Recently, Martens et. al. [START_REF] Czerwinski | Efficient separability of regular languages by subsequences and suffixes[END_REF] also provided a Ptime algorithm for deciding separability by piecewise testable languages, using different proofs but do not provide the computation of such an index.

Finally, for separation by unambiguous languages, the positive decidability result of this paper is new, up to the authors' knowledge. It is equivalent to the decidability of computing the 2-pointlike sets for the class DA.

Preliminaries

We fix a finite alphabet A = {a 1 , . . . , a m }. We denote by A * the free monoid over A. The empty word is denoted by ε. For a word u ∈ A * , the smallest B ⊆ A such that u ∈ B * is called the alphabet of u and is denoted by alph(u).

Separability. Given languages L, L 1 , L 2 , we say that L separates L 1 from L 2 if L 1 ⊆ L and L 2 ∩ L = ∅.
Given a class Sep of languages, we say that the pair (L 1 , L 2 ) is Sep-separable if some language L ∈ Sep separates L 1 from L 2 . Since all classes we consider are closed under complement, (L 1 , L 2 ) is Sep-separable if and only if (L 2 , L 1 ) is, in which case we simply say that L 1 and L 2 are Sep-separable.

We are interested in two classes Sep of separators: the class of piecewise testable languages, and the class of unambiguous languages.

Piecewise Testable Languages. We say that a word u is a piece of v, if

u = b 1 • • • b k , where b 1 , . . . , b k ∈ A, and v ∈ A * b 1 A * • • • A * b k A * .
For instance, ab is a piece of bbaccba. The size of a piece is its number of letters. A language L ⊆ A * is piecewise testable if there exists a κ ∈ N such that membership of w in L only depends on the pieces of size up to κ occurring in w. We write w ∼ κ w ′ when w and w ′ have the same pieces of size up to κ. Clearly, ∼ κ is an equivalence relation, and it has finite index (since there are finitely many pieces of size κ or less). Therefore, a language is piecewise testable if and only if it is a union of ∼ κ -classes for some κ ∈ N. In this case, the language is said to be of index κ. It is easy to see that a language is piecewise testable if and only if it is a finite boolean combination of languages of the form

A * b 1 A * • • • A * b k A * .
Piecewise testable languages are those definable by BΣ 1 (<) formulas. BΣ 1 (<) formulas are boolean combinations of first-order formulas of the form:

∃x 1 . . . ∃x n ϕ(x 1 , . . . , x n ),
where ϕ is quantifier-free. For instance,

A * b 1 A * • • • A * b k A * is defined by the formula ∃x 1 . . . ∃x k i<k (x i < x i+1 )∧ i k b i (x i )
, where the first-order variables x 1 , . . . , x k are interpreted as positions, and where b(x) is the predicate testing that position x carries letter b.

We denote by PT[κ] the class of all piecewise testable languages of index κ or less, and by PT = κ PT[κ] the class of all piecewise testable languages.

Given L ⊆ A * and κ ∈ N, the smallest PT[κ]-language containing L is [L] ∼κ = {w ∈ A * | ∃u ∈ L and u ∼ κ w}.
In general however, there is no smallest PT-language containing a given language, because removing one word from a PT-language yields again a PT-language.

Unambiguous Languages. A product L = B * 0 a 1 B * 1 • • • B * k-1 a k B *
k is called unambiguous if every word of L admits exactly one factorization witnessing its membership in L. The integer k is called the size of the product. An unambiguous language is a finite disjoint union of unambiguous products. Observe that unambiguous languages are connected to piecewise testable languages. Indeed, it was proved in [START_REF] Schützenberger | Sur le produit de concaténation non ambigu[END_REF] that the class of unambiguous languages is closed under boolean operations. Moreover, languages of the form

A * b 1 A * • • • A * b k A * are unambiguous, witnessed by the product (A \ {b 1 }) * b 1 (A \ {b 2 }) * • • • (A \ {b k }) * b k A * .
Therefore, piecewise testable languages form a subclass of the class of unambiguous ones.

Many equivalent characterizations for unambiguous languages have been found [START_REF] Tesson | Diamonds are forever: The variety DA[END_REF]. From a logical point of view, unambiguous languages are exactly the languages definable by an FO 2 (<) formula [START_REF] Thérien | Over words, two variables are as powerful as one quantifier alternation[END_REF]. FO 2 (<) is the two-variable restriction of first-order logic. Another logical characterization which further illustrates the link with piecewise testable languages (i.e. BΣ 1 (<)-definable languages) is ∆ 2 (<). A Σ 2 (<) formula is a first-order formula of the form:

∃x 1 . . . ∃x n ∀y 1 . . . ∀y m ϕ(x 1 , . . . , x n , y 1 , . . . , y m ),
where ϕ is quantifier-free. A language is ∆ 2 (<)-definable if it can be defined both by a Σ 2 (<) formula and the negation of a Σ 2 (<) formula. It has been proven in [START_REF] Pin | Polynomial closure and unambiguous product[END_REF] that a language is unambiguous if and only if it is ∆ 2 (<)-definable.

For two words w, w ′ , we write, w ∼ =κ w ′ if w, w ′ satisfy the same unambiguous products of size κ or less. We denote by UL[κ] the class of all languages that are unions of equivalence classes of ∼ =κ, and we let UL = κ UL[κ]. Observe that because unambiguous languages are closed under boolean operations, UL is the class of all unambiguous languages.

Given L ⊆ A * and κ ∈ N, the smallest UL[κ]-language containing L is

[L]∼ =κ = {w ∈ A * | ∃u ∈ L and u ∼ =κ w}.
In general again, there is no smallest UL-language containing a given language.

Automata. A nondeterministic finite automaton (NFA) over A is denoted by

a tuple A = (Q, A, I, F, δ), where Q is the set of states, I ⊆ Q the set of initial states, F ⊆ Q the set of final states and δ ⊆ Q × A × Q the transition relation.
The size of an automaton is its number of states plus its number of transitions. We denote by L(A) the language of words accepted by A. Given a word u ∈ A * , a subset B of A and two states p, q of A, we denote -by p u --→ q a path from state p to state q labeled u. -by p ⊆B --→ q a path from p to q of which all transitions are labeled over B.

by p =B --→ q a path from p to q of which all transitions are labeled over B, with the additional demand that every letter of B occurs at least once along it.

Given a state p, we denote by scc(p, A) the strongly connected component of p in A (that is, the set of states that are reachable from p and from which p can be reached), and by alph scc(p, A) the set of labels of all transitions occurring in this strongly connected component. Finally, we define the restriction of

A to a subalphabet B ⊆ A by A ↾ B def = (Q, B, I, F, δ ∩ (Q × B × Q)).
Monoids. Let L be a language and M be a monoid. We say that L is recognized by M if there exists a monoid morphism α : A * → M together with a subset F ⊆ M such that L = α -1 (F ). It is well known that a language is accepted by an NFA if and only if it can be recognized by a finite monoid. Further, one can compute from any NFA a finite monoid recognizing its accepted language.

Separation by piecewise testable languages

Since PT[κ] ⊂ PT, PT[κ]-separability implies PT-separability. Further, for a fixed κ, it is obviously decidable whether two languages L 1 and L 2 are PT[κ]separable: there is a finite number of P T [κ] languages over A, and for each of them, one can test whether it separates L 1 and L 2 . The difficulty for deciding whether L 1 and L 2 are PT-separable is to effectively compute a witness κ = κ(L 1 , L 2 ), i.e., such that L 1 and L 2 are PT-separable if and only if they are P T [κ]-separable. Actually, we show that PT-separability is decidable, by different arguments: (2) We compute κ ∈ N from L 1 , L 2 , such that PT-separability and P T [κ]separability are equivalent for L 1 and L 2 . Hence, if the Ptime algorithm answers that L 1 and L 2 are PT-separable, then [L 1 ] ∼κ is a valid PT-separator. Let us first introduce some terminology to explain the necessary and sufficient condition on NFAs. Let A be an NFA over A. For u 0 , . . . , u p ∈ A * and nonempty subalphabets B 1 , . . . , B p ⊆ A, let u = (u 0 , . . . , u p ) and B = (B 1 , . . . , B p ). We call (u, B) a factorization pair. A (u, B)-path in A is a successful path (leading from the initial state to a final state of A), of the form shown in Fig. 1.

u0 ⊆ B1 ⊆ B1 u1 up-1 ⊆ Bp ⊆ Bp up = B1 = Bp Fig. 1. A (u, B)-path
Recall that edges denote sequences of transitions (see section Automata, p. 5). Therefore, if A has a (u, B)-path, then L(A) contains a language of the form

u 0 (x 1 y * 1 z 1 )u 1 • • • u p-1 (x p y * p z p )u p , where alph(x i ) ∪ alph(z i ) ⊆ alph(y i ) = B i .
Given NFAs A 1 and A 2 , we say that a factorization pair (u, B) is a witness of non PT-separability for (A 1 , A 2 ) if there is a (u, B)-path in both A 1 and A 2 . For instance, A 1 and A 2 pictured in Fig. 2 We are now ready to state our main result regarding PT-separability.

Theorem 1. Let A 1 and A 2 be two NFAs over A. p|A|+1) . Then the following conditions are equivalent:

Let L 1 = L(A 1 ) and L 2 = L(A 2 ). Let k 1 , k 2 be the number of states of A 1 resp. A 2 . Define p = max(k 1 , k 2 )+1 and κ = p|A|2 2 |A| |A|(
(1) L 1 and L 2 are PT-separable.

(2) L 1 and L 2 are PT[κ]-separable.

(

) The language [L 1 ] ∼κ separates L 1 from L 2 . ( 3
) 4
There is no witness of non PT-separability in (A 1 , A 2 ).

Condition (2) yields an algorithm to test PT-separability of regular languages. Indeed, one can effectively compute all piecewise testable languages of index κ (of which there are finitely many), and for each of them, one can test whether it separates L 1 and L 2 . Before proving Theorem 1, we show that Condition (4) can be tested in polynomial time (and hence, PT-separability is Ptime decidable).

Proposition 2. Given two NFAs A 1 and A 2 , one can determine whether there exists a witness of non PT-separability in (A 1 , A 2 ) in polynomial time wrt. the sizes of A 1 and A 2 , and the size of the alphabet.

Proof. Let us first show that the following problem is in Ptime: given states p 1 , q 1 , r 1 of A 1 and p 2 , q 2 , r 2 of A 2 , determine whether there exists a nonempty

B ⊆ A and paths p i ⊆B --→ q i (=B) ---→ q i ⊆B --→ r i in A i for both i = 1, 2.
To do so, we compute a decreasing sequence (C i ) i of alphabets overapproximating the greatest alphabet B that can be chosen for labeling the loops. Note that if there exists such an alphabet B, it should be contained in

C 1 def = alph scc(q 1 , A 1 ) ∩ alph scc(q 2 , A 2 ).
Using Tarjan's algorithm to compute strongly connected components in linear time, one can compute C 1 in linear time as well. Then, we restrict the automata to alphabet C 1 , and we repeat the process to obtain the sequence (C i ) i :

C i+1 def = alph scc(q 1 , A 1 ↾ Ci ) ∩ alph scc(q 2 , A 2 ↾ Ci ).
After a finite number n of iterations, we obtain

C n = C n+1 . Note that n |alph(A 1 ) ∩ alph(A 2 )|
|A|. If C n = ∅, then there exists no nonempty B for which there is an (= B)-loop around both p 1 and p 2 . If C n = ∅, then it is the maximal nonempty alphabet B such that there are (= B)-loops around q 1 in A 1 and q 2 in A 2 . It then remains to determine whether there exist paths

p 1 ⊆B --→ q 1 ⊆B --→ r 1 and p 2 ⊆B --→ q 2 ⊆B --→ r 2 ,
which can be performed in linear time.

To sum up, since the number n of iterations to get C n = C n+1 is bounded by |A|, and since each computation is linear wrt. the size of A 1 and A 2 , one can decide in Ptime wrt. to both |A| and these sizes whether such pair of paths occurs. Now we build from A 1 and A 2 two new automata Ã1 and Ã2 as follows. The procedure first initializes Ãi as a copy of A i . Denote by Q i the state set of A i . For each 4-uple τ = (p 1 , r 1 , p 2 , r 2 ) ∈ Q 2 1 × Q 2 2 such that there exist B = ∅, two states q 1 ∈ Q 1 , q 2 ∈ Q 2 and paths p i ⊆B --→ q i =B --→ q i ⊆B --→ r i both for i = 1 and i = 2, we add in both Ã1 and Ã2 a new letter a τ to the alphabet, and "summary" transitions p 1 aτ -→ r 1 and p 2 aτ -→ r 2 . Since there is a polynomial number of tuples (p 1 , q 1 , r 1 , p 2 , q 2 , r 2 ), the above shows that computing these new transitions can be performed in Ptime. So, computing Ã1 and Ã2 can be done in Ptime.

By construction, there exists some factorization pair (u, B) such that A 1 and A 2 both have a (u, B)-path if and only if L( Ã1 ) ∩ L( Ã2 ) = ∅. Since both Ã1 and Ã2 can be built in Ptime, this can be decided in polynomial time as well.

⊓ ⊔

The following is an immediate consequence of Theorem 1 and Proposition 2.

Corollary 3. Given two NFAs, one can determine in polynomial time, with respect to the number of states and the size of the alphabet, whether the languages recognized by these NFAs are PT-separable.

⊓ ⊔

In the rest of the section, we sketch the proof of Theorem 1. The implications ℓ-templates. An ℓ-template is a sequence of length ℓ, T = t 1 , . . . , t ℓ , such that every t i is either a letter a or a subset B of the alphabet A. The main idea behind ℓ-templates is that they yield decompositions of words that can be detected using pieces and provide a suitable decomposition for pumping. Unfortunately, not all ℓ-templates are actually detectable. Because of this we restrict ourselves to a special case of ℓ-templates. An ℓ-template is said to be unambiguous if all pairs t i , t i+1 are either two letters, two incomparable sets or a set and a letter that is not included in the set. For example, T = a, {b, c}, d, {a} is unambiguous, while We now use p-implementations to prove (1) =⇒ ( 2). The proof is divided in two steps. First, we prove that there exists p such that if two words are pimplementations of the same ℓ-template for some ℓ, then they can be pumped into words containing the same pieces of size k for any k, while keeping membership in the regular languages. We will then prove that if two words contain the same pieces for a large enough size, they are both p-implementations of a common unambiguous ℓ-template. We begin with the first step in the following lemma. Lemma 4. Let w 1 ∈ L 1 and w 2 ∈ L 2 . From L 1 , L 2 , we can compute p ∈ N such that whenever w 1 , w 2 are both p-implementations of an ℓ-template T for some ℓ, then for every κ ∈ N, there exist w

T ′ = b,
′ 1 ∈ L 1 and w ′ 2 ∈ L 2 such that w ′ 1 ∼ κ w ′ 2 .
Proof. This is a pumping argument. Let k 1 , k 2 be the number of states of automata recognizing L 1 and L 2 and set p = max(k 1 , k 2 ). Set w 1 , w 2 and T = t 1 , . . . , t ℓ as in the statement of the lemma. Fix κ ∈ N. Whenever t i is a set B, the corresponding factors in w 1 , w 2 are (p, B)-patterns. By choice of p, it follows from a pumping argument that these factors can be pumped into (κ, B)-patterns in L 1 and L 2 . It is then easy to check that the resulting words have the same pieces of size κ.

⊓ ⊔

We now move to our second step. We prove that there exists a number κ such that two words having the same pieces of size up to κ must both be pimplementations of a common unambiguous ℓ-template (where p is the number introduced in Lemma 4). Again, we split the proof in two parts. We begin by proving that it is enough to look for ℓ-templates for a bounded ℓ. Lemma 5. Let p ∈ N. Every word is the p-implementation of some unambiguous

N A -template, for N A = 2 2 |A| |A|(p|A|+1) .
Proof. We first get rid of the unambiguity condition. Any ambiguous ℓ-template T can be reduced to an unambiguous ℓ ′ -template T ′ with ℓ ′ < ℓ by merging the ambiguities. It is then straightforward to reduce any p-implementation of T into a p-implementation of T ′ . Therefore, it suffices to prove that every word is the p-implementation of some (possibly ambiguous) N A -template.

The choice of N A comes from Erdös-Szekeres' upper bound of Ramsey numbers. Indeed, for this value of N A , from every complete graph of size N A with edges labeled over 2 |A| colors, there must be some complete monochromatic subgraph of size p|A| + 1 (see [START_REF] Bacher | An easy upper bound for Ramsey numbers[END_REF] for a short proof that this bound suffices).

Observe that a word is always the p-implementation of the ℓ-template which is just the sequence of its letters. Therefore, in order to complete our proof, it suffices to prove that if a word is the p-implementation of some ℓ-template T with ℓ > N A , then it is also the p-implementation of an ℓ ′ -template with ℓ ′ < ℓ.

Fix a word w, and assume that w is the p-implementation of some ℓ-template T = t 1 , . . . , t ℓ with ℓ > N A . By definition, we get a decomposition w = w 1 • • • w ℓ . We construct a complete graph Γ with vertices {0, . . . , ℓ} and edges labeled by subsets of A. For all i < j, we set alph(w i+1 • • • w j ) as the label of the edge (i, j). Since Γ has more than ℓ > N A vertices, by definition N A there exists a complete monochromatic subgraph with p|A| + 1 vertices {i 1 , . . . , i p|A|+1 }. Let B be the color of the edges of this monochromatic subgraph. Let w ′ = w i1+1 • • • w i p|A|+1 , which is the concatenation of the p|A| words, w ij +1 • • • w ij+1 , for j < p|A|. By construction, these words have alphabet exactly B, hence w ′ is a (p, B)-pattern. It follows that w is a p-implementation of the ℓ ′ -template t 1 , . . . , t i1 , B, t i p|A|+2 , . . . , t ℓ with ℓ ′ = ℓ -p|A| + 1. Hence ℓ ′ < ℓ (except for the trivial case p = |A| = 1).

⊓ ⊔

The next lemma shown in App. A proves that once ℓ and p are fixed, given w it is possible to describe by pieces the unambiguous ℓ-templates that w p-implements.

Lemma 6. Let ℓ, p ∈ N. From p and ℓ, we can compute κ such that for every pair of words w ∼ κ w ′ and every unambiguous ℓ-template T , w ′ is a p-implementation of T whenever w is a (p + 1)-implementation of T .

We finish the proof of the implication (1) =⇒ ( 2) by assembling the results. Assume that L i is recognized by an NFA with k i states. Let p = max(k 1 , k 2 ) be as introduced in Lemma 4, N A as introduced in Lemma 5 for p + 1, and κ = |A|(p + 1)N A be as introduced in Lemma 6. Fix κ ′ > κ and assume that we have w 1 ∈ L 1 and w 2 ∈ L 2 such that w 1 ∼ κ w 2 . By Lemma 5, w 1 is the (p + 1)-implementation of some unambiguous N A -template T . Moreover, it follows from Lemma 6 that w 2 is a p-implementation of T . By Lemma 4, we finally get that there exists w

′ 1 ∈ L 1 and w ′ 2 ∈ L 2 such that w ′ 1 ∼ κ ′ w ′ 2 .
The implication (1) =⇒ (4) of Theorem 1 is easy and shown by contraposition, see [START_REF] Van Rooijen | The separation problem for regular languages by piecewise testable languages[END_REF]Lemma 2] and Appendix. The remaining implication ( 4) =⇒ (1) can be shown using Lemma 6 (see Appendix). For a direct proof, see [START_REF] Van Rooijen | The separation problem for regular languages by piecewise testable languages[END_REF]Lemma 3], where the key for getting a forbidden pattern out of two non-separable languages is to extract a suitable p-implementation using Simon's factorization forests [START_REF] Simon | Factorization forests of finite height[END_REF].

Separation by unambiguous languages

This section is devoted to proving that UL-separability is a decidable property. We use an argument that is analogous to property (2) of Theorem 1 in Section 3. We prove that if L 1 , L 2 are languages, it is possible to compute a number κ such that L 1 , L 2 are UL-separable iff they are UL[κ]-separable. It is then possible to test separability by using a brute-force approach that tests all languages in UL[κ].

In this case, we were not able to prove equivalence between UL-separability and the existence of some common witness inside the automata of both input languages. Because of this, we have a much higher complexity. A rough analysis of the problem, which can be found in the Appendix, gives an algorithm that runs in nondeterministic 3-exponential time in κ. It is likely that this can be improved. We now state the main theorem of this section.

Theorem 7. Let M 1 and M 2 be monoids recognizing L 1 , L 2 ⊆ A * . Let κ = (2|M 1 ||M 2 | + 1)(|A| + 1) 2 .
Then the following conditions are equivalent:

(1) L 1 and L 2 are UL-separable.

(2) L 1 and L 2 are UL[κ]-separable.

(

) The language [L 1 ]∼ =κ separates L 1 from L 2 . 3
As in the previous section, Condition [START_REF] Almeida | Pointlike sets with respect to R and J[END_REF] yields an algorithm for testing whether two languages are separable. Indeed, the algorithm simply computes all languages in UL[κ] and checks for each of them whether it is a separator. Corollary 8. It is decidable whether two regular languages can be separated by a unambiguous language.

Observe that in contrast to Theorem 1, the bound κ of Theorem 7 is stated in terms of monoids rather than in terms of automata which means an exponential blow-up. This is necessary for our proof technique to work.

Another remark, is that by definition of UL[κ], the bound κ is defined in terms of unambiguous products. A rephrasing of the theorem would be: there exists a separator iff there exists one defined by a boolean combination of unambiguous products of size κ. It turns out that κ also works for FO 2 (<), i.e., there exists a separator iff there exists one defined by an FO 2 (<)-formula of quantifier rank κ. This can be proved by making minor adjustements to the proof of Theorem 7.

The proof of Theorem 7 is inspired from techniques used in [START_REF] Place | Deciding definability in FO2(< h , <v) on trees[END_REF] and relies heavily on the notion of (B, p)-patterns. The full proof, which works by induction on the size of the alphabet, can be found in the Appendix. We actually prove a proposition that is basically a rephrasing of Theorem 7 as a pumping-like property. In the remainder of this section, we state this proposition and explain why it implies Theorem 7.

Fix two regular languages L 1 , L 2 over A, as well as their syntactic monoids M 1 , M 2 , and the corresponding morphisms α 1 , α 2 . 2 . For all pairs of words w 1 ∼ =κ w 2 and all κ ′ > κ, there exists w

Proposition 9. Let κ = (2|M 1 ||M 2 | + 1)(|A| + 1)
′ 1 ∼ =κ′ w ′ 2 such that α 1 (w 1 ) = α 1 (w ′ 1 ) and α 2 (w 2 ) = α 2 (w ′ 2 ).
Let us briefly explain why Proposition 9 implies Theorem 7. We explain why the direction (1) =⇒ (3) holds, since (3) =⇒ ( 2) and ( 2) =⇒ (1) are trivial. We prove the contrapositive: assume that [L 1 ]∼ =κ is not a separator. Hence, by definition of [L 1 ]∼ =κ , there exist w 1 ∈ L 1 and w 2 ∈ L 2 such that w 1 ∼ =κ w 2 . Now, let κ ′ > κ. From Proposition 9, it follows that there exist w ′ 1 ∈ L 1 and w ′ 2 ∈ L 2 such that w ′ 1 ∼ =κ′ w ′ 2 . This means that L 1 and L 2 cannot be separated by a language of UL[κ ′ ]. Since this holds for all κ ′ > κ, it follows that L 1 and L 2 are not UL-separable.

Conclusion

We proved separation results for both piecewise testable and unambiguous languages. Both results provide a way to decide separability. In the PT case, we even prove that this can be done in Ptime. Moreover, in both cases we give an insight on the actual separator by providing a bound on its size should it exist.

There remain several interesting questions in this field. First, one could consider other subclasses of regular languages, the most interesting one being full first-order logic. Separability by first-order logic has already been proven to be decidable using semigroup theory [START_REF] Henckell | Pointlike sets: the finest aperiodic cover of a finite semigroup[END_REF]. However, this approach is difficult to understand, it yields a costly algorithm, it only provides a yes/no answer, and no insight about a possible separator. Another question is to get tight complexity bounds. For unambiguous languages for instance, one can show a 3Nexptime bound using translation to automata, but in this case, and even for piecewise testable languages, we do not know any tight bounds on the size of separators.

Another observation is that right now, we have no general approach and are bound to use ad-hoc techniques for each subclass. An interesting direction would be to invent a general framework that is suitable for this problem in the same way that monoids are a suitable framework for decidable characterizations.

w ′ 1 • • • w ′ ℓ = w ′
inductively as follows: assume that the factors are defined up to w ′ i and let u be such that w

′ = w 1 • • • w ′ i • u. If t i+1
is a letter then w i+1 is just the first letter of u, otherwise t i+1 = B ⊆ A, and in that case w i+1 is the largest prefix of u which contains only letters of B. We will prove that w ′ 1 • • • w ′ ℓ witnesses that w ′ is a p-implementation of T . The proof relies on a subresult that we state and prove below.

To every unambiguous ℓ-template T = {t 1 , t 2 , . . . , t ℓ } and p ∈ N, we associate a piece v T,p = v 1 • • • v ℓ , such that for all i:

v i = a if t i = a ∈ A (b 1 • • • b n ) p if t i = {b 1 , . . . , b n } ⊆ A By definition, if w is a p-implementation of T then v T,p is a piece of w. Consider v T,1 = v 1 • • • v ℓ . A piece v is incompatible with T when v is of the following form: v = v 1 • • • v i • u • v i+1 • • • v ℓ such that if t i (resp. t i+1 ) is a set the first letter (resp. last letter) of u is not in t i (resp. t i+1 ).
Claim 1 If w is a 1-implementation of some unambiguous ℓ-template T , then there is no piece of w that is incompatible with T .

Proof. This is a consequence of the fact that T is unambiguous.

⊓ ⊔

We now prove that for all i, w ′ i = a if t i is the letter a or w ′ i is a word over some B ⊆ A containing a (p, B)-pattern if t i = B. We proceed by induction, assume that this is true up to w ′ i and consider w

′ i+1 . Set v T,1 = v 1 • • • v ℓ and v T,p+1 = v 1 • • • v ℓ .
By induction hypothesis and by choice of κ, we know that

v i+1 • • • v ℓ and v i+1 • • • v ℓ are pieces of w i+1 • • • w ℓ .
We distinguish two cases depending on the nature of t i+1 .

Case 1: t i+1 is some letter a. We have to prove that w ′ i+1 = a. Assume that

w ′ i+1 = b = a. Then v 1 • • • v i • b • v i+1 • • • v ℓ must
be a piece of w ′ and therefore a piece of w (w ∼ κ w ′ ). We prove that this piece is incompatible with T , which contradicts Claim 1. Observe that by definition of w i , if t i is a set then b ∈ t i (otherwise it would have been included in t

i ). Therefore v 1 • • • v i • b • v i+1 • • • v ℓ is
incompatible with T and we are done for this case.

Case 2: t i+1 is a set B = {b 1 , . . . , b n }. By construction, w i+1 contains only letters in B. Therefore, we have to prove that it contains a (p, B)-pattern. Assume that it does not. By contruction, the first letter of w i+2 is some letter c

∈ B. If w i+1 = ε, then v 1 • • • v i • c • v i+1 • • • v ℓ must
be a piece of w ′ Using a similar argument to the one of the previous case, we can prove that this piece is incompatible with T , which contradicts Claim 1.

Otherwise, let b be the first letter of w i+1 . Recall that by definition, r i+1 contains a (p+1, B)-pattern and that r i+1 • • • r ℓ is a piece of w i+1 • • • w ℓ . Therefore, since w i+1 does not contain a (p, B)-pattern, the last suffix of r i+1 containing a (1, B)-pattern must fall in w i+2 and consequently, v i+1 • • • v ℓ must be a piece of

w i+2 • • • w ℓ . It follows that v 1 • • • v i • b • c • v i+1 • • • v ℓ
is a piece of w ′ and of w (w ∼ κ w ′ ). By definition, c ∈ t i+1 . Moreover, by construction, if t i is a set, then b ∈ t i . Therefore,

v 1 • • • v i • b • c • v i+1 • • • v ℓ is
incompatible with T which contradicts Claim 1 since it is also a piece of w.

⊓ ⊔ B: Proofs of Section 4

Complexity Analysis

We briefly explain how UL-separability can be checked in 3Nexptime. This is a very rough analysis and it is likely that this can be improved. We use the connection between UL and FO 2 (<) to prove that any language in UL[κ] is recognized by a deterministic automaton that is 3-exponential in κ. In order to check separability it is then enough to non-deterministically guess an automaton of size 3-exponential in κ, check if the automata recognizes an unambiguous language and check if it is a separator. This can be done in non-deterministic 3-exponential time.

It is straightforward to see that any unambiguous product can be described by an FO 2 (<) formula whose nesting depth of quantifiers is polynomial in the size κ of the product. One can then construct an equivalent unary temporal logic (UTL) formula that is exponential in size [START_REF] Etessami | First-order logic with two variables and unary temporal logic[END_REF]. From this UTL formula, it is then possible to construct an equivalent deterministic automaton that is double exponential in size [START_REF] Gastin | LTL with past and two-way very-weak alternating automata[END_REF]. This automaton is 3-exponential in κ.

Proof of Theorem 7

We prove Proposition 9. As we explained, our proof relies heavily on the notion of (B, p)-patterns. However, in this case we will only need to use (B, p)-patterns where B is the whole alphabet A. For this reason, we simply write p-pattern for (A, p)-pattern. We begin by giving a brief outline of the proof. We fix a large enough l, intuitively l needs to be large enough so that we can apply our pumping arguments to words of length l. Then, we show that κ is large enough in order to ensure that w 1 , w 2 are both a 2l-pattern or neither of them are. In both cases, we are then able to decompose w 1 , w 2 into sequences of factors that are pairwise equivalent and use a smaller alphabet. We then apply induction on these factors. In the second case, it then suffices to reconcatenate the factors to obtain the desired result. In the first case, a pumping argument depending on l will also be needed. Before providing the lemmas involved in the construction, we first give some additional definitions concerning k-patterns that will come in conveniently.

Decompositions for k-patterns. Recall that by definition, a word w is a kpattern iff w ∈ (A * a 1 • • • A * a n A * ) k . This means that w can be decomposed into a sequence of factors witnessing its membership in (A * a 1

• • • A * a n A * ) k : w = kn i=1 (w i • a i mod n ) • w kn+1 .
To each word w we associate a unique such decomposition for the largest integer k such that w is a k-pattern. Let w ∈ A * , we say that w admits a k-decomposition iff w is a k-pattern but not a k+1-pattern. It is straightforward to see that if w admits

  (1.a) We give a necessary and sufficient condition on NFAs recognizing L 1 and L 2 , in terms of forbidden patterns, to test whether L 1 and L 2 are PT-separable.(1.b) We give a polynomial time algorithm to check this condition.

Fig. 2 .

 2 Fig. 2. A witness of non PT-separability for (A1, A2): u = (ε, c, ε), B = ({a, b}, {a})

( 3 )

 3 ⇐⇒(2) =⇒ (1) are obvious. To show (1) =⇒ (2), we introduce some terminology. Let us fix an arbitrary order a 1 < • • • < a m on A. (p, B)-patterns. Let B = {b 1 , . . . , b r } ⊆ A with b 1 < • • • < b r , and let p ∈ N. We say that a word w ∈ A * is a (p, B)-pattern if w ∈ (B * b 1 B * • • • B * b r B * ) p . The number p is called the power of w. For example, set B = {a, b, c} with a < b < c. The word bbaababccacbabaca is a (2, B)-pattern but not a (3, B)-pattern.

We prove Condition [START_REF] Ash | Inevitable graphs: a proof of the type II conjecture and some related decision procedures[END_REF]. We prove (4) =⇒ ( 1) and ( 3) =⇒ [START_REF] Ash | Inevitable graphs: a proof of the type II conjecture and some related decision procedures[END_REF]. ( 4) =⇒ [START_REF] Almeida | Some algorithmic problems for pseudovarieties[END_REF]. We proceed by contraposition. Assume that L 1 , L 2 are not PTseparable. Recall that A 1 and A 2 are NFAs for L 1 , L 2 and that k 1 , k 2 are their sizes. Set p = max(k 1 , k 2 ) + 1 and ℓ = 2 2 |A| |A|(p|A|+1) . We prove that L 1 , L 2 both contain p-implementations of some N A -template T and use T to construct a witness of non PT-separability in (A 1 , A 2 ).

Let κ be as defined in Lemma 6 from ℓ and p. Because L 1 , L 2 are not PTseparable, there exist w 1 ∈ L 1 and w 2 ∈ L 2 such that w 1 ∼ κ w 2 . By choice of ℓ, p and Lemma 5, w 1 must be the p-implementation of some unambiguous ℓ-template T . Applying Lemma 6, we obtain that w 1 , w 2 are both (max(k 1 , k 2 ))implementations of T .

Let B = (B 1 , . . . , B n ) be the subsequence of elements T that are sets. Let u = (u 0 , . . . , u n ), where u i is the word obtained by concatenating the letters that are between B i and B i+1 in T . By definition (u, B) is a factorization pair.

Because w 1 is a (max(k 1 , k 2 ))-implementation, the path used to read w 1 in A 1 must traverse loops labeled by each of the B i , and clearly this is a (u, B)-path. Using the same argument we get that the path of w 2 in A 2 is also a (u, B)-path. Therefore (u, B) is a witness of non PT-separability.

(3) =⇒ [START_REF] Ash | Inevitable graphs: a proof of the type II conjecture and some related decision procedures[END_REF]. Again, we proceed by contraposition. Set κ as in Theorem 1 and assume that there exists a factorization pair (u, B) that is a witness of non PT-separabilty. We prove that [L 1 ] ∼κ is not a separator.

Set B = (B 1 , . . . , B n ) and u = (u 0 , . . . , u n ). By definition, this means that there exists w 1 ∈ L 1 and w 2 ∈ L 2 of the form

where the words such that alph(v i ) = B i and v i contains a (B i , κ)pattern. It is straightforward to see that w 1 ∼ κ w 2 . Therefore,

Proof of Lemma 6 Lemma 6. Let ℓ, p ∈ N. From p and ℓ, we can compute κ such that for every pair of words w ∼ κ w ′ and every unambiguous ℓ-template T , w ′ is a p-implementation of T whenever w is a (p + 1)-implementation of T .

Proof. We prove that the lemma holds for κ = |A|pℓ. Let w ∼ κ w ′ and let T = {t 1 , t 2 , . . . , t ℓ } be an unambiguous ℓ-template such that w is a p + 1implementation of T . We begin by giving a decomposition of w ′ and prove that it indeed witnesses the fact that w ′ is a p-implementation of T . We define a k-decomposition then there exists an integer l such that kn < l < (k + 1)n, and

such that for all i, a i mod m ∈ w i . The integer l is called the length of the decomposition. We give an example of a word that admits a 1-decomposition (of length 5) in Figure [START_REF] Almeida | The pseudovariety J is hyperdecidable[END_REF]. We now state two lemmas that are needed for our construction. Both lemmas link k-decompositions to unambiguous languages. The first one states that kdecompositions can be detected using an unambiguous product with large enough size. Moreover, using products of the same size, one can also describe the products that are satisfied by the factors in the k-decomposition.

Then for every pair of words u ∼ =κ v and all h k, u admits an h-decomposition iff v admits an h-decomposition. Moreover, the associated decompositions, as described in (1), are of the same length l:

and for all i, u i ∼ =κ v i .

Proof. For the sake of readability, for all a ∈ A we will write A a for the alphabet A \ {a} and for all number i, we will write b i for a i mod m . Assume that u admits an h-decomposition and consider the associated decomposition:

Consider the following unambiguous product:

By construction, P is of size l k(|A| + 1) < κ and u ∈ P . Therefore, v ∈ P and v admits an h-decomposition together with the associated decomposition:

It remains to prove that for all i, u i ∼ =κ v i . Assume that u i belongs to some unambiguous product P ′ of size κ. This means that u is in the unambiguous product:

Because P ′′ is of size at most κ + k(|A| + 1), we have v ∈ P ′′ . By assumption on the decomposition of v, this means that v i ∈ P ′ and we are done.

⊓ ⊔

Our second lemma states that if a word has both a prefix and a suffix that are large enough k-patterns, then the middle part has no influence on membership in an unambiguous product.

Lemma 8. Let κ ′ ∈ N, and let u, v be two words that are both κ ′ -patterns. Then for all words w 1 , w 2 , the following equivalence holds:

Proof. We begin by observing a simple property of unambiguous products.

κ ′ be an unambiguous product. There can be at most one set B i such that B i = A.

an unambiguous product of size κ ′ and assume that uw 1 v ∈ P . We prove that uw 2 v ∈ P . Since uw 1 v ∈ P , there exists some decomposition

that is a witness. If no set B i is the whole alphabet A, then uw 1 v is at most a κ ′ -pattern, which is impossible since it is by definition a 2κ ′ -pattern. Therefore, by Remark 1 there is exactly one set B i such that B i = A. It follows that the words

patterns. Therefore, they are respectively a prefix of u and a suffix of v (which are κ ′ -patterns). It follows that there exists some word y i such that

Such a decomposition for uw 2 v is witness for membership in P . We conclude that uw 2 v ∈ P .

⊓ ⊔

We can now finish our construction by using Lemma 7 and Lemma 8 and prove Proposition 9. The proof goes by induction on the size of the alphabet.

We begin by fixing the size of the patterns we are going to look for in w 1 , w 2 . Set k = |M 1 ||M 2 |. A pigeonhole principle argument proves that for s 0 , . . . , s k ∈ M 1 and r 0 , . . . , r k ∈ M 2 , there exist i < j such that both

We will look for k-patterns.

Observe that κ = (2k+1)(m+1) 2 (recall that m = |A|). We prove Proposition 9 by induction on m. Let κ ′ > κ, w 1 ∼ =κ w 2 and set κ = (2k + 1)m 2 . By Lemma 7, either both w 1 , w 2 admit h-decompositions for some h < 2k or both w 1 , w 2 do not admit h-decomposition for h 2l. We treat these cases separately.

Case 1: both w 1 and w 2 admit h-decompositions for h < 2k. Observe that κ = (2k + 1)m 2 implies that κ > κ + 2k(m + 1). Therefore, we can apply the second part of Lemma 7 to w 1 and w 2 . This yields the following decompositions:

such that for all i, u i ∼ =κ v i . Also observe that by definition of these decompositions u i , v i use a strict subalphabet of A. Therefore, the induction hypothesis can be used and for all i we get words

. Now, consider the words:

By construction, we have w

2 ) and we are done.

Case 2: both w 1 and w 2 do not admit h-decompositions for h 2k. This means that w 1 , w 2 are both 2k-patterns. A simple argument as in the proof of Lemma 7 shows that w 1 , w 2 can be decomposed into three factors:

r are all κ ′ -patterns. We only give the proof for u ′ l , v ′ l , as the proof for u ′ r , v ′ r is identical. Observe that κk(m + 1) > κ + k(m + 1). Therefore, we can apply Lemma 7 to u l and v l . This yields the following decompositions:

such that for all i, u i ∼ =κ v i . Moreover the length l of the decompositions is l > km. Also observe that by definition of these decompositions, u i , v i use a strict subalphabet of A. Therefore, the induction hypothesis can be used and for all i we get words u

. We now use the fact that our choice of k allows us to pump the sequences of factors into large sequences: there exist numbers 0 j 1 < j 2 k such that

Observe that by construction u ′ l ∼ =κ′ v l (they are products of pairwise equivalent factors). Moreover, by construction of e 1 , e 2 , we have α 1 (u l ) = α 1 (u ′ l ) and α 2 (v l ) = α 1 (v ′ l ). Finally, since e 1 , e 2 are 1-patterns, u ′ l , v ′ l are κ ′ -patterns. Using the same construction for u r , v r , we obtain u ′ r , v ′ r . We can now finish our construction by giving w ′ 1 , w ′ 2 :

By construction it is clear that α 1 (w 1 ) = α 1 (w ′ 1 ) and α 2 (w 2 ) = α 2 (w ′ 2 ). Moreover, because u ′ l , u ′ r are κ ′ -patterns it follows from Lemma 8 that

Combining the two equivalences we obtain w ′ 1 ∼ =κ′ w ′ 2 , which concludes the proof.


Thomas Place

Lorijn Van Rooijen

Marc Zeitoun

Separating Regular Languages by Locally Testable and Locally Threshold Testable Languages

Keywords: Automata, Logics, Monoids, Locally testable, Separation, Context-free. 1

A separator for two languages is a third language containing the first one and disjoint from the second one. We investigate the following decision problem: given two regular input languages, decide whether there exists a locally testable (resp. a locally threshold testable) separator. In both cases, we design a decision procedure based on the occurrence of special patterns in automata accepting the input languages. We prove that the problem is computationally harder than deciding membership. The correctness proof of the algorithm yields a stronger result, namely a description of a possible separator. Finally, we discuss the same problem for context-free input languages.

Introduction

Context. The strong connection between finite state devices and descriptive formalisms, such as first-order or monadic second-order logic, has been a guideline in computer science since the seminal work of Büchi, Elgot and Trakhtenbrot. This bridge has continuously been fruitful, disseminating tools and bringing a number of applications outside of its original research area. For instance, compiling logical specifications into various forms of automata has become one of the most successful methods in automatic program verification [START_REF] Vardi | An automata-theoretic approach to automatic program verification[END_REF].

One of the challenging issues when dealing with a logical formalism is to precisely understand its expressiveness and its limitations. While solutions to decide such logics often use a compilation procedure from formulas to automata, capturing the expressive power amounts to the opposite translation: given a language, one wants to know whether one can reconstruct a formula that describes it. In other words, we want to solve an instance of the membership problem, which asks whether an input language belongs to some given class.

For regular languages of finite words, the main tool developed to capture this expressive power is the syntactic monoid [START_REF] Pin | Syntactic semigroups[END_REF]: this is a finite, computable, algebraic abstraction of the language, whose properties make it possible to decide membership. An emblematic example is the membership problem for the class of first-order definable languages, solved by Schützenberger [START_REF] Schützenberger | On finite monoids having only trivial subgroups[END_REF] and McNaughton and Papert [START_REF] Mcnaughton | Counter-free automata[END_REF], which has led to the development of algebraic methods for obtaining decidable characterizations of logical or combinatorial properties.

The separation problem and its motivations. We consider here the separation problem as a generalization of the membership problem. Assume we are given two classes of languages C and S. The question is, given two input languages from C, whether we can separate them by a language from S. Here, we say that a language separates K from L if it contains K and is disjoint from L. An obvious necessary condition for separability is that the input languages K, L be disjoint. A separator language witnesses this condition.

One strong motivation for this problem is to understand the limits of logics over finite words. Notice that membership reduces to separation when C is closed under complement, because checking that a language belongs to S amounts to testing that it is S-separable from its complement. Deciding S-separation is also more difficult than deciding membership in S, as one cannot rely on algebraic tools tailored to the membership problem. It may also be computationally harder, as we shall see in this paper. Thus, solving the separation problem requires a deeper understanding of S than what is sufficient to check membership: one not only wants to decide whether S is powerful enough to describe a language, but also to decide whether it can discriminate between two input languages. This discriminating power provides more accurate information than the expressive power.

While our main concern is theoretical, let us mention some motivating applications. In model checking, reachable configurations of a system can be represented by a language. Separating this from the language representing bad configurations proves to be effective for verifying safety of a system. Craig interpolation is a form of separation used in this context [START_REF] Mcmillan | Applications of Craig interpolants in model checking[END_REF][START_REF] Henzinger | Abstractions from proofs[END_REF]. In this line of work, Leroux [START_REF] Leroux | Vector addition systems reachability problem (a simpler solution)[END_REF] simplified the proof that reachability in vector addition systems is decidable [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF]: he proved that a recursively enumerable set of separators witnesses non-reachability. Finally, questions in database theory also motivated separation questions [START_REF] Czerwinski | Efficient separability of regular languages by subsequences and suffixes[END_REF].

Although the separation problem frequently occurs, it has not been systematically studied, even in the restricted, yet still challenging case of regular languages.

Contributions.

In general, elements of C cannot always be separated by an element of S and there is no minimal separator wrt. inclusion. We are interested in the following questions:

can we decide whether one can separate two given languages of C by a language of S? what is the complexity of this decision problem? if separation is possible, can we compute a separator, and at which cost? A motivating but difficult objective is to understand separation by first-order definable languages, whose decidability follows from involved algebraic methods [START_REF] Henckell | Pointlike sets: the finest aperiodic cover of a finite semigroup[END_REF][START_REF] Henckell | Aperiodic pointlikes and beyond[END_REF]. A first step is to look at easier subclasses. Indeed, the question was raised and solved for separation by piecewise-testable languages [START_REF] Czerwinski | Efficient separability of regular languages by subsequences and suffixes[END_REF][START_REF] Place | Separating regular languages by piecewise testable and unambiguous languages[END_REF], and unambiguous languages [START_REF] Place | Separating regular languages by piecewise testable and unambiguous languages[END_REF], which sit in the lower levels of the quantifier-alternation hierarchy of first-order logic. In this paper, we look at yet another widely studied class, whose properties are orthogonal to those of the above classes.

We investigate the separation problem by locally and locally threshold testable languages. A language is locally testable (LT) if membership of a word can be tested by inspecting its prefixes, suffixes and infixes up to some length (which depends on the language). The membership problem for this class was raised by McNaughton and Papert [START_REF] Mcnaughton | Counter-free automata[END_REF], and solved independently by McNaughton and Zalcstein [START_REF] Zalcstein | Locally testable languages[END_REF][START_REF] Mcnaughton | Algebraic decision procedures for local testability[END_REF] and by Brzozowski and Simon [4]. This class has several generalizations. The most studied one is that of locally threshold testable languages (LTT), where counting infixes is allowed up to some threshold. These are the languages definable in FO(+1), i.e., first-order logic with the successor relation (but without the order). Again, membership is decidable [START_REF] Thérien | Graph congruences and wreath products[END_REF], and can actually be tested in Ptime [START_REF] Pin | Expressive power of existential first-order sentences of Büchi's sequential calculus[END_REF].

Our results are as follows: we show that separability of regular languages by LT and LTT languages is decidable, first for a fixed threshold, by reduction to fixed parameters: we provide a bound on the length of infixes that define a possible separator. This reduces the problem to a finite number of candidate separators, and hence entails decidability. For LTT-separability, we also provide a bound for the threshold. We further get an equivalent formulation on automata in terms of forbidden patterns for the languages to be separable, which yields an Nexptime algorithm. We also obtain lower complexity bounds: even starting from DFAs, the problem is Np-hard for LT and LTT (while membership to LTT is in Ptime). Finally, we discuss the separation problem starting from context-free input languages rather than regular ones. Due to lack of space, several proofs only appear in the journal version of the paper.

The main arguments rely on pumping in monoids or automata. The core of our proof is generic: we show that if one can find two words, one in each input language, that are close enough wrt. the class of separators, then the languages are not separable. Here, "close enough" is defined in terms of parameters of the input languages, such as the size of input NFAs.

Related work.

In the context of semigroup theory, it has been proven [START_REF] Almeida | Some algorithmic problems for pseudovarieties[END_REF] that the separation problem can be rephrased in purely algebraic terms. Solving the separation problem for a class S amounts to computing the so-called pointlike sets for the algebraic variety corresponding to S. While it has been shown that the varieties corresponding to both LT and LTT have computable pointlike sets [START_REF] Beauquier | Languages and scanners[END_REF][START_REF] Steinberg | On pointlike sets and joins of pseudovarieties[END_REF][START_REF] Steinberg | A delay theorem for pointlikes[END_REF], this approach suffers two drawbacks. First, being purely algebraic, the proofs provide no insight on the underlying class S. In particular, they provide only yes/no answers without giving any description of what an actual separator might be.

Finally, the separation problem for the class of piecewise-testable languages has recently been shown Ptime-decidable, independently and with different techniques in [START_REF] Czerwinski | Efficient separability of regular languages by subsequences and suffixes[END_REF] and [START_REF] Place | Separating regular languages by piecewise testable and unambiguous languages[END_REF].

Preliminaries

Words and Languages. We fix a finite alphabet A. We denote by A * the free monoid over A. The empty word is denoted by ε. If w is a word, we set |w| as the length, or size of w. When w is nonempty, we view w as a sequence of |w| positions labeled over A. We number positions from 0 (for the leftmost one) to |w| -1 (for the rightmost one).

Infixes, Prefixes, Suffixes. An infix of a word w is a word Profiles. For k ∈ N, let k ℓ = ⌊k/2⌋ and k r = kk ℓ . A k-profile is a pair of words (w ℓ , w r ) of lengths at most k ℓ and k r , respectively. Given w ∈ A * and x a position of w, the k-profile of x is the pair (w ℓ , w r ) defined as follows: w ℓ = w[max(0, xk ℓ ), x] and w r = w[x, min(x + k r , |w|)] (see Figure 1). A k-profile (w ℓ , w r ) occurs in a word w if there exists some position x within w whose k-profile is (w ℓ , w r ). Similarly, if n ∈ N, we say that (w ℓ , w r ) occurs n times in w if there are n distinct positions in w where (w ℓ , w r ) occurs. Intuitively, the k-profile is the description of the infix of w that is centered at position x. Observe in particular that the k-profiles that occur in a word determine the prefixes and suffixes of length k -1 of this word. This is convenient, since we only have to consider one object instead of three in the usual presentations of the classes LT and LTT.

w ′ such that w = u • w ′ • v for some u, v ∈ A * . Moreover, if u = ε (resp. v = ε) we say that w ′ is a prefix (resp.
We denote by A k the set of k-profiles over the alphabet A. It is of size exponential in k.

Separability. Given languages

L, L 1 , L 2 over A * , we say that L separates L 1 from L 2 if L 1 ⊆ L and L 2 ∩ L = ∅.
Given a class S of languages, we say that the pair (

L 1 , L 2 ) is S-separable if some language L ∈ S separates L 1 from L 2 . When S is closed under complement, (L 1 , L 2 ) is S-separable if and only if (L 2 , L 1 )
is, in which case we simply say that L 1 and L 2 are S-separable.

Automata.

A nondeterministic finite automaton (NFA) over A is denoted by a tuple A = (Q, A, I, F, δ), where Q is the set of states, I ⊆ Q the set of initial states, F ⊆ Q the set of final states and δ ⊆ Q × A × Q the transition relation. The size of an automaton is its number of states plus its number of transitions. If δ is a function, then A is a deterministic finite automaton (DFA). We denote by L(A) the language of words accepted by A.

Monoids.

Let L be a language and M be a monoid. We say that L is recognized by M if there exists a monoid morphism α :

A * → M together with a subset F ⊆ M such that L = α -1 (F ).
It is well known that a language is accepted by an NFA if and only if it can be recognized by a finite monoid. Further, one can compute from any NFA a finite monoid recognizing its accepted language.

Locally Testable and Locally Threshold Testable Languages

In this paper, we investigate two classes of languages. Intuitively, a language is locally testable if membership of a word in the language only depends on the set of infixes, prefixes and suffixes up to some fixed length that occur in the word. For a locally threshold testable language, membership may also depend on the number of occurrences of such infixes, which may thus be counted up to some fixed threshold.

In this section we provide specific definitions for both classes. We start with the larger class of locally threshold testable languages. In the following, we say that two numbers are equal up to threshold d if either both numbers are equal, or both are greater than or equal to d.

Locally Threshold Testable Languages. Let L be a language, we say that L is locally threshold testable (LTT) if it is a boolean combination of languages of the form: LTT languages can actually be defined in terms of first-order logic. A language is LTT if and only if it can be defined by an FO(+1) formula [START_REF] Beauquier | Languages and scanners[END_REF][START_REF] Thomas | Classifying regular events in symbolic logic[END_REF], i.e., a first-order logic formula using predicates for the equality and next position relations, but not for the linear order.

1. uA * = {w | u is a prefix of w}, for some u ∈ A * . 2. A * u = {w | u is
We also define an index on LTT languages. Usually, this index is defined as the smallest size of infixes, prefixes and suffixes needed to define the language. However, since we only work with k-profiles, we directly define an index based on the size of k-profiles. Given words w, w ′ and natural numbers k, d, we write w ≡ d k w ′ if for every k-profile (w ℓ , w r ), the number of positions x such that (w ℓ , w r ) is the k-profile of x is equal up to threshold d in w and w ′ . One can verify that for all k, d ∈ N, ≡ d k is an equivalence relation of finite index. For k, d ∈ N we denote by LTT[k, d] the set of the finitely many languages that are unions of

≡ d k -classes. We have LTT = k,d LTT[k, d]. Given L ⊆ A * , the smallest LTT[k, d]- language containing L is [L] ≡ d k = {w ∈ A * | ∃u ∈ L such that u ≡ d k w}.
As it is often the case, there is no smallest LTT language containing a given regular language.

Locally Testable Languages. The class of locally testable languages is the restriction of LTT languages in which infixes cannot be counted. A language L is locally testable (LT) if it is a boolean combination of languages of the form 1, 2 and the following restriction of 3: No simple description of LT in terms of first-order logic is known. However, there is a simple definition in terms of temporal logic. A language is LT if and only if it can be defined by a temporal logic formula using operators X (next), Y (yesterday), and G (globally).

Given two words w, w ′ and a number k, we write w ≡ k w ′ for w ≡ 1 k w ′ . For all k ∈ N, we denote by LT[k] the set of languages that are unions of ≡ k -classes, and

LT = k LT[k]. Given L ⊆ A * and k ∈ N, the smallest LT[k]-language containing L is [L] ≡ k = {w ∈ A * | ∃u ∈ L such that u ≡ k w}.

Separation for a Fixed Threshold

In this section, we prove that if the counting threshold d is fixed, it is decidable whether two languages can be separated by an LTT language of counting threshold d (i.e., by an LTT[k, d] language for some k). In particular, this covers the case of LT, which corresponds to d = 1. All results in this section are for an arbitrary d. Our result is twofold.

First, we establish a bound on the size of profiles that need to be considered in order to separate the languages. This bound only depends on the size of monoids recognizing the languages, and it can be computed. One can then use a brute-force algorithm that tests separability by all the finitely many LTT[k, d] languages, where k denotes this bound.

The second contribution is a criterion on the input languages to check separability by an LTT[k, d] language for some k. This criterion can be defined equivalently on automata or monoids recognizing the input languages, in terms of the absence of common patterns.

The section is organized into three subsections: our criterion is stated in the first one, and the second and last ones are devoted to the statement and proof of the theorem.

Patterns

In this section we define our criterion that two languages must satisfy in order to be separable. The criterion can be defined equivalently on automata or monoids recognizing the languages. Block Patterns. A block is a triple of words b = (v ℓ , u, v r ) where v ℓ , v r are nonempty. Similarly, a prefix block is a pair of words p = (u, v r ) with v r nonempty, and a suffix block is a pair of words s = (v ℓ , u) with v ℓ nonempty. Let d ∈ N. A d-pattern P is either a word w, or a triple (p, f, s) where p and s are respectively a prefix and a suffix block, and f is a function mapping blocks to the set {0, . . . , d}, such that all but finitely many blocks are mapped to 0.

Decompositions. Let w be a word and let P be a d-pattern. We say that w admits a P-decomposition if w admits a decomposition w = u 0 v 1 u 1 v 2 • • • v n u n with n 0 and such that either n = 0 and P = u 0 = w, or P = (p, f, s) and the following conditions are verified:

1. p = (u 0 , v 1 ) and s = (v n , u n ). 2. for all blocks b, if f (b) < d, then there are exactly f (b) indices i such that (v i , u i , v i+1 ) = b. 3. for all blocks b, if f (b) = d, then there are at least d indices i such that (v i , u i , v i+1 ) = b.
Sometimes, we just say P-decomposition to mean P-decomposition of some word. Let α : A * → M be a morphism into a monoid M , and let s ∈

M . A P-decomposition is (α, s)-compatible if α(w) = s and α(u 0 • • • v i ) = α(u 0 • • • v i ) • α(v i ), for 1 i n.
Similarly, if A is an automaton, we say that a P-decomposition is A-compatible if there is an accepting . . . . . .

u 0 u 1 u i-1 u i+1 u n-1 u i u n v 1 v i v i+1 v n Figure 2 An A-compatible P-decomposition u0v1u1v2 • • • vnun
run for w and each infix v i labels a loop in the run, for 1 i n, as pictured in Figure 2 (where edges denote sequences of transitions). 2 with the same set of triples (v i , u i , v i+1 ).

A useful property about common patterns is that whether such a pattern exists only depends on the recognized languages, and not on the choice of

A 1 , A 2 , M 1 , M 2 . ◮ Proposition 1. Fix d ∈ N. Let L 1 ,

Separation Theorem for a Fixed Threshold

We can now state our main theorem for this section.

The language [L

1 ] ≡ d k separates L 1 from L 2 . 4. M 1 , M 2 do not have a common d-pattern. 5. A 1 , A 2 do not have a common d-pattern.
Observe that Item 2 is essentially a delay theorem [START_REF] Straubing | Finite semigroup varieties of the form V * D[END_REF] for separation restricted to the case of LTT: we prove that the size of profiles (i.e., infixes) that a potential separator needs to consider can be bounded by a function of the size of the monoids recognizing the languages. By restricting Theorem 2 to the case d = 1, we get the following separation theorem for LT. ◮ Theorem 3. Let L 1 , L 2 be regular languages and let M 1 , M 2 , A 1 , A 2 be arbitrary monoids and automata recognizing L 1 , L 2 respectively. Let k = 4(|M 1 ||M 2 | + 1). Then the following conditions are equivalent: 1. L 1 and L 2 are LT-separable.

L 1 and L

2 are LT[k]-separable. 3. The language [L 1 ] ≡ k separates L 1 from L 2 . 4. M 1 , M 2 do not have a common 1-pattern. 5. A 1 , A 2 do not have a common 1-pattern.
Theorem 2 and Theorem 3 yield algorithms for deciding LT-and LTT-separability for a fixed threshold. Indeed, the algorithm just tests all the finitely many LTT[k, d] languages as potential separators. This brute-force approach yields a very costly procedure. It turns out that a better algorithm can be obtained from Items 4 and 5 (the proof is available in the full version of the paper). This yields the following corollary.

◮ Corollary 4. Let d ∈ N. It is decidable whether two given regular languages are LTT[l, d]separable for some l ∈ N. In particular, it is decidable whether they are LT-separable.

More precisely, given NFAs A 1 , A 2 , deciding whether L(A 1 ) and L(A 2 ) are LT-separable is in co-Nexptime. It is co-Np-hard, even starting from DFAs.

It remains to prove Theorem 2. The implications (3) ⇒ (2) ⇒ (1) are immediate by definition. We now prove (1) ⇒ (5) ⇒ (4) ⇒ (3). The implication (5) ⇒ (4) is immediate from Proposition 1. The implication (1) ⇒ ( 5) is a consequence of the following proposition.

◮ Proposition 5. Let d ∈ N and let A 1 , A 2 be NFAs. If A 1 , A 2 have a common d-pattern, then, for all k ∈ N, there exist w 1 , w 2 accepted respectively by A 1 , A 2 such that w 1 ≡ d k w 2 .
An immediate consequence of Proposition 5 is that as soon as A 1 , A 2 have a common d-pattern, the recognized languages cannot be separated by an LTT[k, d] language for any k. This is exactly the contrapositive of (1) ⇒ (5). We now prove Proposition 5.

Proof of Prop. 5. Let P be a common d-pattern

of A 1 , A 2 . If P = w ∈ A * , then by definition, w ∈ L(A 1 ) ∩ L(A 2 )
, so it suffices to choose w 1 = w 2 = w. Otherwise, P = (p, f, s) and there are w 1 , w 2 having an A 1 -, respectively A 2 -compatible P-decomposition. Let

w 1 = u 0 v 1 u 1 v 2 • • • v n u n and w 2 = u ′ 0 v ′ 1 u ′ 1 v ′ 2 • • • v ′ m u ′ m be these decompositions. For k ∈ N, set w 1 = u 0 (v 1 ) k(d+1) u 1 (v 2 ) k(d+1) • • • (v n ) k(d+1) u n w 2 = u ′ 0 (v ′ 1 ) k(d+1) u ′ 1 (v ′ 2 ) k(d+1) • • • (v ′ m ) k(d+1) u ′ m
By definition of compatibility, w 1 ∈ L(A 1 ) and w 2 ∈ L(A 2 ). From the fact that (p, f, s) is a d-pattern, it then follows that w 1 ≡ d k w 2 . ◭

The remaining and most difficult direction, (4) ⇒ (3) is a consequence of the next proposition whose proof is outlined in the next subsection.

◮ Proposition 6. Let α 1 : A * → M 1 and α 2 : A * → M 2 be morphisms, and k = 4(|M 1 ||M 2 | + 1). Let d ∈ N and let w 1 , w 2 be words such that w 1 ≡ d k w 2 . Then there exists a d-pattern P, an (α 1 , α 1 (w 1 ))-compatible P-decomposition, and an (α 2 , α 2 (w 2 ))-compatible P-decomposition.

Before explaining how to show Proposition 6, let us explain how to conclude the proof of Theorem 2. We prove the contrapositive of ( 4) ⇒ (3). If Item 3 does not hold, then by definition there must exist

w 1 ∈ L 1 and w 2 ∈ L 2 such that w 1 ≡ d k w 2 . If w 1 = w 2 , L 1 ∩ L 2 = ∅, therefore, M 1 , M 2 have a common d-pattern.
Otherwise, by Proposition 6 we get a d-pattern (p, f, s). Since w 1 ∈ L 1 and w 2 ∈ L 2 , the d-pattern (p, f, s) is common to both M 1 and M 2 , which ends the proof.

Proof of Proposition 6

We set w 1 , w 2 , k and d as in the statement of the proposition. Observe first that if w 1 = w 2 = w, then it suffices to take P = w. Therefore, we suppose for the remainder of the proof that w 1 = w 2 . We proceed as follows: we construct two new words w ′ 1 , w ′ 2 from w 1 , w 2 admitting respectively a (α 1 , α 1 (w 1 ))-compatible P-decomposition and a (α 2 , α 2 (w 2 ))compatible P-decomposition, for some d-pattern P = (p, f, s). In this outline, we only provide the construction, the proof of correctness is available in the full version of the paper. The construction of w ′ 1 , w ′ 2 , amounts to duplicating infixes in w 1 , w 2 verifying special properties. We first define these special infixes that we will call k-loops. k-loops. Let w ∈ A * , x be a position in w, and (w ℓ , w r ) be the ⌊k/2⌋-profile of x. We say that x admits a k-loop if there exists a nonempty prefix u of w r such that α 1 (w ℓ ) = α 1 (w ℓ • u) and α 2 (w ℓ ) = α 2 (w ℓ • u). In this case, we call the smallest such u the k-loop of x. See Figure 3.

b aa c b c ba a x ⌊k/2⌋-profile of x k-profile of x w ℓ w r u for i = 1, 2, α i (w ℓ ) = α i (w ℓ ) • α i (u) Figure 3 A position x admitting a k-loop u: αi(w ℓ ) = αi(w ℓ • u), for i = 1, 2
For our construction to work, we need k-loops to have three properties that we state now. The first two are simple facts that are immediate from the definition: k-loops are determined by profiles and can be duplicated without modifying the image of the word under α. ◮ Fact 7. Let x be a position. Whether x admits a k-loop, and if so, which k-loop x admits, only depends on the ⌊k/2⌋-profile of x.

◮ Fact 8. Let w be a word and let x be a position within w such that x admits a k-loop u.

Then for i = 1, 2, α i (w[0, x]) = α i (w[0, x]) • α i (u).
The last property we need is that k-loops occur frequently in words, i.e., at least one of ⌊k/4⌋ consecutive positions must admit a k-loop. This follows from pumping arguments: ◮ Lemma 9. Let w be a word and let x 1 , . . . , x ⌊k/4⌋ be ⌊k/4⌋ consecutive positions in w. Then, there exists at least one position x i with i < ⌊k/4⌋ that admits a k-loop.

Construction of w ′

1 , w ′ 2 . We can now construct w ′ 1 and w ′ 2 . If w, u are words and x is a position of w, the word constructed by inserting u at position x is the word w

[0, x] • u • w[x, |w|].
From w 1 (resp. w 2 ), we construct w ′ 1 (resp. w ′ 2 ) by inserting simultaneously all infixes (u x ) k ′ in w 1 (resp. w 2 ) at any position x that admits a k-loop, and where u x is the k-loop of x. Using Fact 7, Fact 8 and Lemma 9 one can then verify that w ′ 1 admits a (α 1 , α 1 (w 1 ))compatible P-decomposition and w ′ 2 admits a (α 2 , α 2 (w 2 ))-compatible P-decomposition, for some d-pattern P = (p, f, s). The proof is available in the full version of the paper.

Separation by LTT Languages

This section is devoted to LTT. Again, our theorem actually contains several results. In the case of LTT, two parameters are involved: the size k of profiles and the counting threshold d.

The first result in our theorem states that the bound on k of Theorem 2 still holds for full LTT. This means that two languages are LTT-separable if and only if there exists some counting threshold d such that they are LTT[k, d]-separable with the same bound k as in Theorem 2. It turns out that this already yields an algorithm for testing LTT-separability. The algorithm relies on the decidability of Presburger arithmetic and is actually adapted in a straightforward manner from an algorithm of [START_REF] Bojańczyk | A new algorithm for testing if a regular language is locally threshold testable[END_REF] for deciding membership in LTT. While this first result gives an algorithm for testing separability, it gives no insight about an actual separator. Indeed, the procedure does not produce the actual counting threshold d. This is obtained in the second part of our theorem: we prove that two languages are LTTseparable if and only if they are LTT[k, d]-separable, where k is as defined in Theorem 2, and d is bounded by a function of the size of the monoids (or automata) recognizing the input languages. Note that this result also gives another (brute-force) algorithm for testing LTT-separability. We now state our theorem. Recall that A k denotes the set of k-profiles. ◮ Theorem 10. Let L 1 , L 2 be regular languages and let M 1 , M 2 , A 1 , A 2 be arbitrary monoids and automata recognizing

L 1 , L 2 . Set n to be either max(|M 1 |, |M 2 |)+1 or max(|A 1 |, |A 2 |)+1. Let k = 4(|M 1 ||M 2 | + 1) and d = (|A k |n) |A k | .
Then, the following conditions are equivalent: 1. L 1 and L 2 are LTT-separable.

There exists

d ′ ∈ N such that L 1 and L 2 are LTT[k, d ′ ]-separable. 3. There exists d ′ ∈ N such that M 1 , M 2 do not have a common d ′ -pattern. 4. There exists d ′ ∈ N such that A 1 , A 2 do not have a common d ′ -pattern. 5. L 1 and L 2 are LTT[k, d]-separable. 6. The language [L 1 ] ≡ d k separates L 1 from L 2 .
Observe that decidability of LTT-separability is immediate from Item 5 by using the usual brute-force algorithm. As it was the case for a fixed counting threshold, this algorithm is slow. In the full version of the paper, we obtain a faster algorithm by using Items 3 and 4.

◮ Corollary 11. It is decidable whether two given regular languages are LTT-separable. More precisely, given NFAs A 1 , A 2 , deciding whether L(A 1 ) and L(A 2 ) are LTT-separable is in 2-Expspace. It is co-Np-hard, even starting from DFAs.

By definition, a language is LTT if it is LTT [k, d] for some natural numbers k, d. Hence, the equivalence between Items 1, 2, 3 and 4 is an immediate consequence of Theorem 2. Therefore, we only need to prove Items 5 and 6, i.e., the bound on the threshold d. Unfortunately, these are exactly the items we need for Corollary 11. However, we will prove that by reusing an algorithm of [START_REF] Bojańczyk | A new algorithm for testing if a regular language is locally threshold testable[END_REF], Corollary 11 can also be derived directly from Item 2.

We now explain how to derive the first part of Corollary 11 from Item 2 without relying on the actual bound on the counting threshold. The bound itself is proved in the full version.

Decidability of LTT-separability as a consequence of Theorem 2

As we explained, the equivalence of Item 2 to LTT-separability is immediate from Theorem 2. We explain how to combine this fact with an algorithm of [START_REF] Bojańczyk | A new algorithm for testing if a regular language is locally threshold testable[END_REF] to obtain decidability directly.

In [START_REF] Bojańczyk | A new algorithm for testing if a regular language is locally threshold testable[END_REF], it is proved that once k is fixed, Parikh's Theorem [START_REF] Parikh | On context-free languages[END_REF] can be used to prove that whether a language is LTT[k, d] for some d can be rephrased as a computable Presburger formula. Decidability of membership in LTT can then be reduced to decidability of Presburger Arithmetic. For achieving this, two ingredients were needed: a) a bound on k, and b) the translation to Presburger arithmetic. It turns out that in [START_REF] Bojańczyk | A new algorithm for testing if a regular language is locally threshold testable[END_REF], only the proof of a) was specific to membership. On the other hand, separation was already taken care of in b), because the intuition behind the Presburger formula was testing separability between the input language and its complement. In our setting, we have already replaced a), i.e., bounding k, by Item 2. Therefore, the argument can be generalized. We explain in the remainder of this subsection how to construct the Presburger formula. The argument makes use of the notion of commutative image, which we now recall.

The commutative image of a word w ∈ A * , denoted π(w), is a vector of length |A| of natural numbers counting, for all a ∈ A, how many occurrences of a there are in w. This notion can be easily generalized in order to count profiles rather than just letters. Let k ∈ N. The k-image of w, π k (w), is a vector of length |A k | of numbers counting for every k-profile (w ℓ , w r ) the number of positions in w with k-profile (w ℓ , w r ). If L is a language, the k-image of L, π k (L) is the set A well-known result about commutative images is Parikh's Theorem [START_REF] Parikh | On context-free languages[END_REF], which states that if L is context-free (so in particular if L is regular), then π(L) is semilinear, i.e., Presburger definable [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF]. As explained in [START_REF] Bojańczyk | A new algorithm for testing if a regular language is locally threshold testable[END_REF], Parikh's Theorem extends without difficulty to k-images. ◮ Theorem 13. Let L be a context-free language and let k ∈ N. Then π k (L) is semilinear. Moreover, a Presburger formula for this semilinear set can be computed.

{π k (w) | w ∈ L} ⊆ N A k
Proof. For k = 1, this is Parikh's Theorem. When k > 1, let L ′ ⊆ A *
k such that w ′ ∈ L ′ if there exists w ∈ L of the same length, and such that a position in w ′ is labeled by the k-profile of the same position in w. One can verify that L ′ is (effectively) context-free, and that the k-image of L is the commutative image of L ′ , which is semilinear by Parikh's Theorem. ◭

We can now explain how to decide LTT-separability. By Item 2 in Theorem 10, L 1 , L 2 are LTT-separable if and only if they are LTT[k, d]-separable for k = 4(|M 1 ||M 2 | + 1) (where M 1 , M 2 are monoids recognizing L 1 , L 2 ) and some natural number d. Therefore, whether L 1 , L 2 are LTT-separable can be rephrased as follows: does there exist some threshold d such that there exist no words w 1 ∈ L 1 , w 2 ∈ L 2 such that w ≡ d k w ′ ? By Fact 12, this can be expressed in terms of k-images: does there exist a threshold d such that there exist no vectors of natural numbers x1 ∈ π k (L 1 ), x2 ∈ π k (L 2 ) that are equal up to threshold d? It follows from Theorem 13 that the above question can be expressed as a computable Presburger formula. Decidability of LTT-separability then follows from decidability of Presburger Arithmetic.

6

The Case of Context-Free Languages

In order to prove decidability of LTT-separability for regular languages, we needed three ingredients: Parikh's Theorem, decidability of Presburger Arithmetic and Item 2 in Theorem 10. Since Parikh's Theorem holds not only for regular languages but also for context-free languages, we retain at least two of the ingredients in the context-free setting.

In particular, we can reuse the argument of Section 5 to prove that once the size k of the profiles is fixed, separability by LTT is decidable for context-free languages. For any fixed k ∈ N, we write LTT

[k] = d∈N LTT[k, d]. ◮ Theorem 14. Let L 1 , L 2 be context-free languages and k ∈ N. It is decidable whether L 1 , L 2 are LTT[k]-separable.
An interesting consequence of Theorem 14 is that LTT [START_REF] Almeida | Some algorithmic problems for pseudovarieties[END_REF]-separability of context-free languages is decidable. A language is LTT [START_REF] Almeida | Some algorithmic problems for pseudovarieties[END_REF] if and only if it can be defined by a first-order logic formula that can only test equality between positions, but not ordering. This result is surprising since membership of a context-free language in this class is undecidable. We give a proof of this fact below, which is a simple adaptation of the proof of Greibach's Theorem (which is in particular used to prove that regularity of a context-free language is undecidable). ◮ Theorem 15. Let L be a context-free language. It is undecidable to test whether L ∈ LTT [START_REF] Almeida | Some algorithmic problems for pseudovarieties[END_REF].

Proof. We reduce universality of context-free languages to this membership problem. Fix L a context-free language over A and let # ∈ A. Let K ∈ LTT [START_REF] Almeida | Some algorithmic problems for pseudovarieties[END_REF] be some context-free language and set L

1 = (K • # • A * ) ∪ (A * • # • L).
Clearly, a context-free grammar for L 1 can be computed from a context-free grammar for L. We show that L = A * iff L 1 ∈ LTT [START_REF] Almeida | Some algorithmic problems for pseudovarieties[END_REF].

If L = A * , then L 1 = A * • # • A * ∈ LTT[1]
. Conversely, assume that L 1 ∈ LTT [START_REF] Almeida | Some algorithmic problems for pseudovarieties[END_REF], and suppose by contradiction that L = A * . Pick w ∈ A * such that w ∈ L. By definition, K = {u | u#w ∈ L 1 }. One can verify that LTT [START_REF] Almeida | Some algorithmic problems for pseudovarieties[END_REF] is closed under right residual. Therefore, K = L 1 (#w) -1 ∈ LTT [START_REF] Almeida | Some algorithmic problems for pseudovarieties[END_REF] which is a contradiction by definition of K. ◭ Theorems 14 and 15 may seem contradictory. Indeed in the setting of regular languages, membership can be reduced to separability (a language belongs to a class if the class can separate it from its complement). However, context-free languages are not closed under complement, which makes the reduction false in this larger setting.

An interesting question is whether decidability extends to full LT and LTT-separability of context-free languages. This would also be surprising since membership of a context-free language in LT or LTT is undecidable. Such a result would require to generalize our third ingredient, Item 2 in Theorem 10, to context-free languages. This means that we would need a method for computing a bound on the size of the infixes that a potential separator has to consider. It turns out that this is not possible. ◮ Theorem 16. Let L 1 , L 2 be context-free languages. It is undecidable to test whether L 1 , L 2 are LT-separable. It is undecidable to test whether L 1 , L 2 are LTT-separable.

It was already known [START_REF] Szymanski | Noncanonical extensions of bottom-up parsing techniques[END_REF] that separability by a regular language is undecidable for context-free languages. The proof of Theorem 16 is essentially the same since the reduction provided in [START_REF] Szymanski | Noncanonical extensions of bottom-up parsing techniques[END_REF] actually works for any class of regular separators that contains languages of the form K 1 A * ∪ K 2 where K 1 , K 2 are finite languages. Since this is clearly the case for both LT and LTT, Theorem 16 follows.

Conclusion

We proved separation theorems for both LT and LTT. In both cases, algorithms to test separability, in co-Nexptime and 2-Expspace respectively, are derived from these theorems. Another contribution is a description of possible separators, given by bounds defining them.

Several questions remain open in this line of research. A first one is to obtain tight complexity bounds for both classes. While we have co-Nexptime and 2-Expspace upper bounds for LT and LTT respectively, we have only co-NP lower bounds. The upper bounds rely on a reduction to the case k = 1, i.e., a translation to the special case when the size of infixes is fixed to 1. This translation is exponential wrt. the size of the input automata. Improving the upper bounds would likely require improving this reduction.

Another question is to consider other fragments for separability. A natural generalization of LTT is LTT+MOD, in which infixes can now also be counted modulo constants. The most interesting fragment is of course full first-order logic. While the problem was shown decidable [START_REF] Henckell | Pointlike sets: the finest aperiodic cover of a finite semigroup[END_REF][START_REF] Henckell | Aperiodic pointlikes and beyond[END_REF], the proofs rely on involved algebraic techniques and give an algorithm that provides only a yes/no answer. Furthermore, the techniques bring no insight on the expressive power of first-order logic. It remains a challenging open problem to obtain a combinatorial proof that FO-separability is decidable, as well as a description of a separator.

  suffix) of w. Let 0 x < y |w|. We write w[x, y] for the infix of w starting at position x and ending at position y -1. By convention, we set w[x, x] = ε. Observe that by definition, when x y z, we have w[x, z] = w[x, y] • w[y, z].

  bac) (aab, cba) (aab, ba) 6-profiles of x, y and z:

Figure 1

 1 Figure 1 Illustration of the notion of k-profile for k = 6

  a suffix of w}, for some u ∈ A * . 3. {w | w has u as an infix at least d times} for some u ∈ A * and d ∈ N.

4 .

 4 A * uA * = {w | w has u as an infix} for some u ∈ A * .

◮ Theorem 2 .

 2 Fix d ∈ N. Let L 1 , L 2 be regular languages and let M 1 , M 2 , A 1 , A 2 be arbitrary monoids and automata recognizing L 1 , L 2 respectively. Set k = 4(|M 1 ||M 2 | + 1). Then the following conditions are equivalent: 1. L 1 and L 2 are LTT[l, d]-separable for some l. 2. L 1 and L 2 are LTT[k, d]-separable.

◮ Fact 12 .

 12 . The definition of ≡ d k yields the following fact. Let w, w ′ ∈ A * and k, d ∈ N. Then w ≡ d k w ′ if and only if π k (w) and π k (w ′ ) are equal componentwise up to threshold d.

  Common Patterns. Let d ∈ N and M 1 , M 2 be two monoids together with morphisms α 1 : A * → M 1 and α 2 : A * → M 2 and accepting setsF 1 ⊆ M 1 , F 2 ⊆ M 2 . We say that M 1 , M 2 have a common d-pattern if there exist a d-pattern P, two elements s 1 ∈ F 1 , s 2 ∈ F 2 ,and two P-decompositions of (possibly different) words that are respectively (α 1 , s 1 )-compatible and (α 2 , s 2 )-compatible. Similarly, if A 1 , A 2 are automata, we say that A 1 , A 2 have a common d-pattern if there exist a d-pattern P and two P-decompositions of words that are respectively A 1 -compatible and A 2 -compatible. In particular, by the very definition, A 1 and A 2 have a common 1-pattern if there are successful paths in A 1 , A 2 of the form shown in Figure

  L 2 be regular languages and let M 1 , M 2 , A 1 , A 2 be arbitrary monoids and automata recognizing L 1 , L 2 , respectively. Then M 1 , M 2 have a common d-pattern if and only if A 1 , A 2 have a common d-pattern.

* Work supported by Agence Nationale de la Recherche ANR 2010 BLAN 0202 01 FREC. licensed under Creative Commons