Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, decide whether there exists a first-order definable separator. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation. This yields an EXPTIME algorithm for checking first-order separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. Finally, we generalize this technique to answer the same question for regular languages of infinite words.

• 03B25 - Decidability of theories and sets of sentences
• 03D05 - Automata and formal grammars in connection with logical questions
• 20M35 - Semigroups in automata theory, linguistics, etc.
• 68Q45 - Formal languages and automata
• 68Q70 - Algebraic theory of languages and automata