Thomas Place ; Marc Zeitoun - Separating Regular Languages with First-Order Logic

lmcs:1628 - Logical Methods in Computer Science, March 9, 2016, Volume 12, Issue 1 - https://doi.org/10.2168/LMCS-12(1:5)2016
Separating Regular Languages with First-Order LogicArticle

Authors: Thomas Place ; Marc Zeitoun

    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.


    Volume: Volume 12, Issue 1
    Published on: March 9, 2016
    Submitted on: June 4, 2014
    Keywords: Computer Science - Formal Languages and Automata Theory,Computer Science - Logic in Computer Science

    19 Documents citing this article

    Consultation statistics

    This page has been seen 1381 times.
    This article's PDF has been downloaded 441 times.