# Separating Regular Languages with First-Order Logic

arXiv: https://arxiv.org/abs/1402.3277 · HTML: https://mlsanity.com/paper/1402.3277/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Feb 2014.

## Built on by (most cited first, 1 of 1)

- [Reverse Engineering of Temporal Queries Mediated by LTL Ontologies](https://mlsanity.com/paper/2305.01248/) (2023)

## Abstract (arXiv)

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.