一个通用的多项式时间方法：无量化器替代的一阶逻辑分离
摘要：关于B{Sigma}1一阶逻辑片段相应的语言类别，我们研究了不允许量词交替的情况下的各种类别。每个类别是通过选择可使用的位置上的谓词集合来定义的。两个关键的片段是带有线性排序和可能的后继关系的片段。已知这两个变体在成员资格上是可判定的：“一个输入正则语言是否属于该类别？”我们依赖于B{Sigma}1的一个操作符BPol的表征，给定一个输入类别C，它输出一个与C相关的B{Sigma}1变体类别BPol(C)，其中包含与C相关的特殊谓词。我们以两个正交方向扩展了这些结果。首先，我们使用两种输入：组语言类别G（即由一个DFA识别，其中每个字母引起状态的置换）以及它们的扩展，写作G+。类别BPol(G)和BPol(G+)包括许多使用线性排序、后继、模运算谓词或字母模运算谓词的B{Sigma}1变体。其次，我们研究了比成员资格更一般的分离问题：判断两个正则语言是否可以被所研究的类别中的一种语言分离。我们证明当G的情况成立时，对于BPol(G)和BPol(G+)来说这是可判定的。这对于BPol(G)和两个特定类别BPol(G+)是已知的。然而，这些算法是间接的，并依赖于复杂的框架，导致上界复杂度较差。我们的方法是直接的，使用基本概念（主要是有限自动机）。我们的主要贡献是从BPol(G)-和BPol(G+)-分离到G-分离的多项式时间图灵归约。这为B{Sigma}1的关键变体提供了多项式算法，包括那些带有线性排序，可能的后继和/或模运算谓词的变体。
作者：Thomas Place and Marc Zeitoun
论文ID：2210.00946
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2022-10-04