一句话:为 dot-depth 2 给出分离算法,并证明基有限的拼接层级第一层分离可判定。
dot-depth 层级刻画星自由语言与一阶可定义语言,其各层对应一阶量词交替块数;判定给定正则语言是否属于某一层(membership)是自动机理论著名难题,目前仅低层已知。本文转向更一般的分离问题:给定两个语言,判定是否存在该层语言包含第一个且与第二个不相交。作者为 dot-depth 2 设计了分离算法;更一般地,证明对任意基为有限的拼接层级,第一层分离可判定,再结合已有结果将其提升到 dot-depth 2。
The dot-depth hierarchy of Brzozowski and Cohen classifies the star-free languages of finite words. By a theorem of McNaughton and Papert, these are also the first-order definable languages. The dot-depth rose to prominence following the work of Thomas, who proved an exact correspondence with the quantifier alternation hierarchy of first-order logic: each level in the dot-depth hierarchy consists of all languages that can be defined with a prescribed number of quantifier blocks. One of the most famous open problems in automata theory is to settle whether the membership problem is decidable for each level: is it possible to decide whether an input regular language belongs to this level? Despite a significant research effort, membership by itself has only been solved for low levels. A recent breakthrough was achieved by replacing membership with a more general problem: separation. Given two input languages, one has to decide whether there exists a third language in the investigated level containing the first language and disjoint from the second. The motivation is that: (1) while more difficult, separation is more rewarding (2) it provides a more convenient framework (3) all recent membership algorithms are reductions to separation for lower levels. We present a separation algorithm for dot-depth two. While this is our most prominent application, our result is more general. We consider a family of hierarchies that includes the dot-depth: concatenation hierarchies. They are built via a generic construction process. One first chooses an initial class, the basis, which is the lowest level in the hierarchy. Further levels are built by applying generic operations. Our main theorem states that for any concatenation hierarchy whose basis is finite, separation is decidable for level one. In the special case of the dot-depth, this can be lifted to level two using previously known results.