| Summary: | 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.
|
|---|