Separation for dot-depth two
Thomas Place, Marc Zeitoun · Logic in Computer Science · 2017
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.