  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.
