Separating regular languages with two quantifier alternations

TL;DR

This paper proves that the separation problem is decidable for certain levels of concatenation hierarchies, including the dot-depth hierarchy, advancing understanding of automata theory and logical definability.

Contribution

It establishes the decidability of separation at level 3/2 for any finite basis hierarchy and at level 5/2 for the dot-depth hierarchy, connecting automata and logic.

Findings

Separation is decidable at level 3/2 of any finite basis concatenation hierarchy.

Separation is decidable at level 5/2 in the dot-depth hierarchy.

This solves the separation problem for  in first-order logic.

Abstract

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.