Separation and covering for group based concatenation hierarchies

Concatenation hierarchies are classifications of regular languages. All such hierarchies are built through the same construction process: start from an initial class of languages and build new levels using two generic operations. Concatenation hierarchies have gathered a lot of interest since the 70s, thanks to an alternate logical definition: each concatenation hierarchy is the quantification alternation hierarchy within a variant of first-order logic over words. Our goal is to understand such hierarchies. We look at two decision problems: membership and separation. 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 hierarchy: 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 may only contain group languages. An example is the quantifier alternation hierarchy of first-order logic with modular predicates: its basis consists of languages counting 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 for levels up to 3/2. 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.