Separating Regular Languages with First-Order Logic

2014/02/28 by Thomas Place, Marc Zeitoun · 1 citation
Computer Science · #cs.FL #cs.LO

paper · pdf · doi:10.2168/lmcs-12(1:5)2016

published as Logical Methods in Computer Science, Volume 12, Issue 1 (March 9, 2016) lmcs:1628

arxiv created 2016/03/08 · arxiv updated 2017/01/11

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.

Cited by

• Finite-Horizon First-Order Rank Profiles of Regular Languages

Related

• The separation problem for regular languages by piecewise testable languages
• Separating regular languages by piecewise testable and unambiguous languages
• A Transfer Theorem for the Separation Problem
• Efficient Separability of Regular Languages by Subsequences and Suffixes
• A generic polynomial time approach to separation by first-order logic without quantifier alternation