We study a celebrated class of regular languages: star-free languages. A long-standing goal is to classify them by the complexity of their descriptions. The most influential research effort involves concatenation hierarchies, which measure alternations between "complement" and "union plus concatenation".We explore alternative hierarchies that also stratify star-free languages (and extensions thereof). They are built with an operator ${\mathcal{C}} \mapsto {\text{TL}}\left({\mathcal{C}}\right)$. It takes a class of languages ${\mathcal{C}}$ as input, and produces a larger one ${\text{TL}}\left({\mathcal{C}}\right)$, consisting of all languages definable in a variant of unary temporal logic, where the future/past modalities depend on ${\mathcal{C}}$. Level n in the navigational hierarchy of basis ${\mathcal{C}}$ is then constructed by applying this operator n times to ${\mathcal{C}}$.As bases ${\mathcal{G}}$, we focus on group languages and natural extensions thereof, denoted ${{\mathcal{G}}^ + }$. We prove that the navigational hierarchies of bases ${\mathcal{G}}$ and ${{\mathcal{G}}^ + }$ are strictly intertwined and we conduct a thorough investigation of their relationships with their concatenation hierarchy counterparts. We also look at two standard problems on classes of languages: membership (decide if a language is in the class) and separation (decide, for two languages L1,L2, if there is a language K in the class with L1⊆ K and L2∩K = ∅). We prove that if separation is decidable for ${\mathcal{G}}$, then so is membership for level two in the navigational hierarchies of bases ${\mathcal{G}}$ and ${{\mathcal{G}}^ + }$.We take a closer look at the trivial class ST = {∅,A*}. For the bases ST and ST+, the levels one are the standard variants of unary temporal logic. The levels two correspond to variants of two-variable logic, investigated recently by Krebs, Lodaya, Pandya and Straubing. We solve one of their conjectures. We also prove that for these two bases, level two has decidable separation. Combined with earlier results on the operator ${\mathcal{C}} \mapsto {\text{TL}}\left({\mathcal{C}}\right)$, this implies that level three has decidable membership.

We introduce an operator on classes of regular languages, the star-free closure. Our motivation is to generalize standard results of automata theory within a unified framework. Given an arbitrary input class \(\mathscr{C}\) , the star-free closure operator outputs the least class closed under Boolean operations and language concatenation, and containing all languages of \(\mathscr{C}\) as well as all finite languages. We establish several equivalent characterizations of star-free closure: in terms of regular expressions, first-order logic, pure future and future-past temporal logic, and recognition by finite monoids. A key ingredient is that star-free closure coincides with another closure operator, defined in terms of regular operations where Kleene stars are allowed in restricted contexts. A consequence of this first result is that we can decide membership of a regular language in the star-free closure of a class whose separation problem is decidable. Moreover, we prove that separation itself is decidable for the star-free closure of any finite class, and of any class of group languages having itself decidable separation (plus mild additional properties). We actually show decidability of a stronger property, called covering.

We investigate an operator on classes of languages. For each class $C$, it outputs a new class $FO^2(I_C)$ associated with a variant of two-variable first-order logic equipped with a signature$I_C$ built from $C$. For $C = \{\emptyset, A^*\}$, we get the variant $FO^2(<)$ equipped with the linear order. For $C = \{\emptyset, \{\varepsilon\},A^+, A^*\}$, we get the variant $FO^2(<,+1)$, which also includes the successor. If $C$ consists of all Boolean combinations of languages $A^*aA^*$ where $a$ is a letter, we get the variant $FO^2(<,Bet)$, which also includes "between relations". We prove a generic algebraic characterization of the classes $FO^2(I_C)$. It smoothly and elegantly generalizes the known ones for all aforementioned cases. Moreover, it implies that if $C$ has decidable separation (plus mild properties), then $FO^2(I_C)$ has a decidable membership problem. We actually work with an equivalent definition of \fodc in terms of unary temporal logic. For each class $C$, we consider a variant $TL(C)$ of unary temporal logic whose future/past modalities depend on $C$ and such that $TL(C) = FO^2(I_C)$. Finally, we also characterize $FL(C)$ and $PL(C)$, the pure-future and pure-past restrictions of $TL(C)$. These characterizations as well imply that if \Cs is a class with decidable separation, then $FL(C)$ and $PL(C)$ have decidable membership.

We look at concatenation hierarchies of classes of regular languages. Each such hierarchy is determined by a single class, its basis: level n is built by applying the Boolean polynomial closure operator "BPol" n times to the basis. An important and challenging open question in automata theory is deciding if a regular language belongs to a given level. For the historical dot-depth hierarchy, the membership problem is only known to be decidable at levels one and two.

Group languages are regular languages recognized by finite groups, or equivalently by finite automata in which each letter induces a permutation on the set of states. We investigate the separation problem for this class of languages: given two arbitrary regular languages as input, we show how to decide if there exists a group language containing the first one while being disjoint from the second. We prove that covering, a problem generalizing separation, is decidable. A simple covering algorithm was already known: it can be obtained indirectly as a corollary of an algebraic theorem by Ash. Unfortunately, while deducing the algorithm from this algebraic result is straightforward, all proofs of Ash’s result itself require a strong background on algebraic concepts, and a wealth of technical machinery outside of automata theory. Our proof is independent previous ones. It relies exclusively on standard notions from automata theory: we directly deal with separation and work with input languages represented by nondeterministic finite automata.We also investigate two strict subclasses. First, the alphabet modulo testable languages are those defined by counting the occurrences of each letter modulo some fixed integer (equivalently, they are the languages recognized by a commutative group). Secondly, the modulo languages are those defined by counting the length of words modulo some fixed integer. We prove that covering is decidable for both classes, with algorithms that rely on the construction made for group languages.Our proofs lead to tight complexity bounds for separation for all three classes, as well as for covering for both alphabet modulo testable languages and for modulo testable languages.

We look at classes of languages associated to the fragment of first-order logic BΣ1 which disallows quantifier alternations. Each class is defined by choosing the set of predicates on positions that may be used. Two key such fragments are those equipped with the linear ordering and possibly the successor relation. It is known that these two variants have decidable membership: "does an input regular language belong to the class ?". We rely on a characterization of BΣ1 by the operator BPol: given an input class C, it outputs a class BPol(C) that corresponds to a variant of BΣ1 equipped with special predicates associated to C. We extend these results in two orthogonal directions. First, we use two kinds of inputs: classes G of group languages (i.e., recognized by a DFA in which each letter induces a permutation of the states) and extensions thereof, written G+. The classes BPol(G) and BPol(G+) capture many variants of BΣ1 which use predicates such as the linear ordering, the successor, the modular predicates or the alphabetic modular predicates. Second, instead of membership, we explore the more general separation problem: decide if two regular languages can be separated by a language from the class under study. We show it is decidable for BPol(G) and BPol(G+) when this is the case for G. This was known for BPol(G) and for two particular classes BPol(G+). Yet, the algorithms were indirect and relied on involved frameworks, yielding poor upper complexity bounds. Our approach is direct. We work with elementary concepts (mainly, finite automata). Our main contribution consists in polynomial time Turing reductions from both BPol(G)- and BPol(G+)-separation to G-separation. This yields polynomial algorithms for key variants of BΣ1, including those equipped with the linear ordering and possibly the successor and/or the modular predicates.

Polynomial closure is a standard operator which is applied to a class of regular languages. In this paper, we investigate three restrictions called left (LPol), right (RPol) and mixed polynomial closure (MPol). The first two were known while MPol is new. We look at two decision problems that are defined for every class . Membership takes a regular language as input and asks if it belongs to . Separation takes two regular languages as input and asks if there exists a third language in including the first one and disjoint from the second. We prove that LPol, RPol and MPol preserve the decidability of membership under mild hypotheses on the input class, and the decidability of separation under much stronger hypotheses. We apply these results to natural hierarchies.

The dot-depth hierarchy of Brzozowski and Cohen classifies the star-free languages of finite words. By a theorem of McNaughton and Papert, these are also the first-order definable languages. The dot-depth rose to prominence following the work of Thomas, who proved an exact correspondence with the quantifier alternation hierarchy of first-order logic: each level in the dot-depth hierarchy consists of all languages that can be defined with a prescribed number of quantifier blocks. One of the most famous open problems in automata theory is to settle whether the membership problem is decidable for each level: is it possible to decide whether an input regular language belongs to this level? Despite a significant research effort, membership by itself has only been solved for low levels. A recent breakthrough was achieved by replacing membership with a more general problem: separation. Given two input languages, one has to decide whether there exists a third language in the investigated level containing the first language and disjoint from the second. The motivation is that: (1) while more difficult, separation is more rewarding (2) it provides a more convenient framework (3) all recent membership algorithms are reductions to separation for lower levels. We present a separation algorithm for dot-depth two. While this is our most prominent application, our result is more general. We consider a family of hierarchies that includes the dot-depth: concatenation hierarchies. They are built via a generic construction process. One first chooses an initial class, the basis, which is the lowest level in the hierarchy. Further levels are built by applying generic operations. Our main theorem states that for any concatenation hierarchy whose basis is finite, separation is decidable for level one. In the special case of the dot-depth, this can be lifted to level two using previously known results.

Given a class C of word languages, the C -separation problem asks for an algorithm that, given as input two regular languages, decides whether there exists a third language in C containing the first language, while being disjoint from the second. Separation is usually investigated as a means to obtain a deep understanding of the class C . In this article, we are mainly interested in classes defined by logical formalisms. Such classes are often built on top of each other: given some logic, one builds a stronger one by adding new predicates to its signature. A natural construction is to enrich a logic with the successor relation. In this article, we present a transfer result applying to this construction: We show that for suitable logically defined classes, separation for the logic enriched with the successor relation reduces to separation for the original logic. Our theorem also applies to a problem that is stronger than separation: covering. Moreover, we actually present two reductions: one for languages of finite words and the other for languages of infinite words.

Concatenation hierarchies are natural classifications of regular languages. All such hierarchies are built through the same construction process: one starts from an initial, specific class of languages (the basis) and builds new levels using two generic operations. Concatenation hierarchies have gathered a lot of interest since the early 70s, notably thanks to an alternate logical definition: each concatenation hierarchy can be defined as the quantification alternation hierarchy within a variant of first-order logic over words (while the hierarchies differ by their bases, the variants differ by their set of available predicates). Our goal is to understand these hierarchies. A typical approach is to look at two decision problems: membership and separation. In the paper we are interested in the latter, which is more general. For a class of languages C, C-separation takes two regular languages as input and asks whether there exists a third one in C including the first one and disjoint from the second one. Settling whether separation is decidable for the levels within a given concatenation hierarchy is among the most fundamental and challenging questions in formal language theory. In all prominent cases, it is open, or answered positively for low levels only. Recently, a breakthrough was made using a generic approach for a specific kind of hierarchies: those with a finite basis. In this case. separation is always decidable for levels 1/2. 1 and 3/2. Our main theorem is similar but independent: we consider hierarchies with possibly infinite bases, but that contain only group languages. An example is the group hierarchy introduced by Pin and Margolis: its basis consists of all group languages. Another example is the quantifier alternation hierarchy of first-order logic with modular predicates FO( <;, MOD): its basis consists of the languages that count the length of words modulo some number. Using a generic approach, we show that for any such hierarchy, if separation is decidable for the basis, then it is decidable as well for levels 1/2, 1 and 3/2 (we actually solve a more general problem called covering). This complements the aforementioned result nicely: all bases considered in the literature are either finite or made of group languages. Thus, one may handle the lower levels of any prominent hierarchy in a generic way.

We investigate quantifier alternation hierarchies in first-order logic on finite words. Levels in these hierarchies are defined by counting the number of quantifier alternations in formulas. We prove that one can decide membership of a regular language in the levels BΣ 2 (finite Boolean combinations of formulas having only one alternation) and Σ 3 (formulas having only two alternations and beginning with an existential block). Our proofs work by considering a deeper problem, called separation , which, once solved for lower levels, allows us to solve membership for higher levels.

We investigate the complexity of the separation problem associated to classes of regular languages. For a class C, C-separation takes two regular languages as input and asks whether there exists a third language in C which includes the first and is disjoint from the second. First, in contrast with the situation for the classical membership problem, we prove that for most classes C, the complexity of C-separation does not depend on how the input languages are represented: it is the same for nondeterministic finite automata and monoid morphisms. Then, we investigate specific classes belonging to finitely based concatenation hierarchies. It was recently proved that the problem is always decidable for levels 1/2 and 1 of any such hierarchy (with inefficient algorithms). Here, we build on these results to show that when the alphabet is fixed, there are polynomial time algorithms for both levels. Finally, we investigate levels 3/2 and 2 of the famous Straubing-Thérien hierarchy. We show that separation is PSPACE-complete for level 3/2 and between PSPACE-hard and EXPTIME for level 2.

We investigate a famous decision problem in automata theory: separation. Given a class of language C, the separation problem for C takes as input two regular languages and asks whether there exists a third one which belongs to C, includes the first one and is disjoint from the second. Typically, obtaining an algorithm for separation yields a deep understanding of the investigated class C. This explains why a lot of effort has been devoted to finding algorithms for the most prominent classes. Here, we are interested in classes within concatenation hierarchies. Such hierarchies are built using a generic construction process: one starts from an initial class called the basis and builds new levels by applying generic operations. The most famous one, the dot-depth hierarchy of Brzozowski and Cohen, classifies the languages definable in first-order logic. Moreover, it was shown by Thomas that it corresponds to the quantifier alternation hierarchy of first-order logic: each level in the dot-depth corresponds to the languages that can be defined with a prescribed number of quantifier blocks. Finding separation algorithms for all levels in this hierarchy is among the most famous open problems in automata theory. Our main theorem is generic: we show that separation is decidable for the level 3/2 of any concatenation hierarchy whose basis is finite. Furthermore, in the special case of the dot-depth, we push this result to the level 5/2. In logical terms, this solves separation for $\Sigma_3$: first-order sentences having at most three quantifier blocks starting with an existential one.

An important endeavor in computer science is to understand the expressive power of logical formalisms over discrete structures, such as words. Naturally, "understanding" is not a mathematical notion. This investigation requires therefore a concrete objective to capture this understanding. In the literature, the standard choice for this objective is the membership problem, whose aim is to find a procedure deciding whether an input regular language can be defined in the logic under investigation. This approach was cemented as the right one by the seminal work of Sch\"utzenberger, McNaughton and Papert on first-order logic and has been in use since then. However, membership questions are hard: for several important fragments, researchers have failed in this endeavor despite decades of investigation. In view of recent results on one of the most famous open questions, namely the quantifier alternation hierarchy of first-order logic, an explanation may be that membership is too restrictive as a setting. These new results were indeed obtained by considering more general problems than membership, taking advantage of the increased flexibility of the enriched mathematical setting. This opens a promising research avenue and efforts have been devoted at identifying and solving such problems for natural fragments. Until now however, these problems have been ad hoc, most fragments relying on a specific one. A unique new problem replacing membership as the right one is still missing. The main contribution of this paper is a suitable candidate to play this role: the Covering Problem. We motivate this problem with 3 arguments. First, it admits an elementary set theoretic formulation, similar to membership. Second, we are able to reexplain or generalize all known results with this problem. Third, we develop a mathematical framework and a methodology tailored to the investigation of this problem.

The dot-depth hierarchy of Brzozowski and Cohen is a classification of all first-order definable languages. It rose to prominence following the work of Thomas, who established an exact correspondence with the quantifier alternation hierarchy of first-order logic: each level contains languages that can be defined with a prescribed number of quantifier blocks. One of the most famous open problems in automata theory is to obtain membership algorithms for all levels in this hierarchy. For a fixed level, the membership problem asks whether an input regular language belongs to this level. Despite a significant research effort, membership by itself has only been solved for low levels. Recently, a breakthrough was made by replacing membership with a more general problem called separation. This problem asks whether, for two input languages, there exists a third language in the investigated level containing the first language and disjoint from the second. The motivation for looking at separation is threefold: (1) while more difficult, it is more rewarding; (2) being more general, it provides a more convenient framework, and (3) all recent membership algorithms are actually reductions to separation for lower levels. This paper presents a separation algorithm for dot-depth 2. A crucial point is that while dot-depth 2 is our main application, we prove a much more general theorem. Indeed, dot-depth belongs to a family of hierarchies which all share the same generic construction process: starting from an initial class of languages called the basis, one applies generic operations to build new levels. We prove that for any such hierarchy whose basis is a finite class, level 1 has decidable separation. In the special case of dot-depth, this generic result can easily be lifted to level 2.

An important endeavor in computer science is to precisely understand the expressive power of logical formalisms over discrete structures, such as words. Naturally, "understanding" is not a mathematical notion. Therefore, this investigation requires a concrete objective to capture such a notion. In the literature, the standard choice for this objective is the membership problem, whose aim is to find a procedure deciding whether an input regular language can be defined in the logic under study. This approach was cemented as the "right" one by the seminal work of Schuetzenberger, McNaughton and Papert on first-order logic and has been in use since then. However, membership questions are hard: for several important fragments, researchers have failed in this endeavor despite decades of investigation. In view of recent results on one of the most famous open questions, namely the quantifier alternation hierarchy of first-order logic, an explanation may be that membership is too restrictive as a setting. These new results were indeed obtained by considering more general problems than membership, taking advantage of the increased flexibility of the enriched mathematical setting. This opens a promising avenue of research and efforts have been devoted at identifying and solving such problems for natural fragments. However, until now, these problems have been ad hoc, most fragments relying on a specific one. A unique new problem replacing membership as the right one is still missing. The main contribution of this paper is a suitable candidate to play this role: the Covering Problem. We motivate this problem with three arguments. First, it admits an elementary set theoretic formulation, similar to membership. Second, we are able to reexplain or generalize all known results with this problem. Third, we develop a mathematical framework as well as a methodology tailored to the investigation of this problem.

We investigate the quantifier alternation hierarchy of first-order logic over finite words. To do so, we rely on the separation problem. For each level in the hierarchy, this problem takes two regular languages as input and asks whether there exists a formula of the level that accepts all words in the first language and no word in the second one. Usually, obtaining an algorithm that solves this problem requires a deep understanding of the level under investigation. We present such an algorithm for the level Σ3(formulas having at most 2 alternations beginning with an existential block). We also obtain as a corollary that one can decide whether a regular language is definable by a Σ4formula (formulas having at most 3 alternations beginning with an existential block).

We investigate two problems for a class C of regular word languages. The C-membership problem asks for an algorithm to decide whether an input language belongs to C. The C-separation problem asks for an algorithm that, given as input two regular languages, decides whether there exists a third language in C containing the first language, while being disjoint from the second. These problems are considered as means to obtain a deep understanding of the class C. It is usual for such classes to be defined by logical formalisms. Logics are often built on top of each other, by adding new predicates. A natural construction is to enrich a logic with the successor relation. In this paper, we obtain new and simple proofs of two transfer results: we show that for suitable logically defined classes, the membership, resp. the separation problem for a class enriched with the successor relation reduces to the same problem for the original class. Our reductions work both for languages of finite words and infinite words. The proofs are mostly self-contained, and only require a basic background on regular languages. This paper therefore gives simple proofs of results that were considered as difficult, such as the decidability of the membership problem for the levels 1, 3/2, 2 and 5/2 of the dot-depth hierarchy.

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.

We prove that it is decidable whether a regular unranked tree language is definable in FO2(h,v). By FO2(h,v) we refer to the two variable fragment of first order logic built from the descendant and following sibling predicates. In terms of expressive power it corresponds to a fragment of the navigational core of XPath that contains modalities for going up to some ancestor, down to some descendant, left to some preceding sibling, and right to some following sibling. We also investigate definability in some other fragments of XPath.