Separating Regular Languages with First-Order Logic

Abstract

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.

References in corpus (1)

• Separating regular languages by piecewise testable and unambiguous languages

Cited by in corpus (7)

• A Characterization for Decidable Separability by Piecewise Testable Languages
• Certifying Inexpressibility
• The omega-inequality problem for concatenation hierarchies of star-free languages
• Certifying DFA Bounds for Recognition and Separation
• On Varieties of Automata Enriched with an Algebraic Structure (Extended Abstract)
• Factoriality and the Pin-Reutenauer procedure
• Recognizing pro-R closures of regular languages