用一阶逻辑分离正则语言
Separating Regular Languages with First-Order Logic
摘要：
给定两种语言，分隔符是包含第一种语言且与第二种语言不相交的第三种语言。本文研究了如下判定问题：给定两种有限字的正则输入语言，判定是否存在一阶可定义分隔符。我们证明，为了回答这个问题，可以从识别输入语言的半群中提取足够的信息，使用不动点计算。这就产生了一个EXPTIME算法来检查一阶可分性。此外，该算法的正确性证明产生了一个更强的结果，即一个可能的分离器的描述。最后，我们推广这种技术来回答同样的问题的正则语言的无限词。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
