Separating Regular Languages with Two Quantifiers Alternations

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 Σ₃ (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 Σ₄ formula (formulas having at most 3 alternations beginning with an existential block).