证明语言接收器有界问题可判定性的技术

文献中已研究了多种类型的自动机和文法模型，对于这些模型，确定某些问题是否可判定是很常见的。在自动机与形式语言理论的历史中，一直难以回答的一个问题是：判定给定系统 $M$ 是否接受有界语言（即是否存在词 $w_1, \ldots,w_k$ 使得 $L(M) \subseteq w_1 \cdots w_k$ 成立？）。对于文献中的大多数自动机/文法模型，该问题的可判定性一直悬而未决。直到最近，有界性才被证明对于正则语言和上下文无关语言是可判定的，并且对于增加了反转有界计数器的有限自动机和下推自动机，以及带状态的向量加法系统也是可判定的。在本文中，我们通过将该问题归约为更简单类别自动机的有界性可判定性，开发了新技术以证明有界问题对于更大类别的单向非确定自动机和文法模型是可判定的。一种技术涉及用多带自动机来刻画这些模型。我们给出了有限回合图灵机、增加了各种存储结构（如下推、多个反转有界计数器、部分盲计数器等）的有限回合图灵机以及简单矩阵文法的新刻画。随后利用这些刻画证明了这些模型的有界问题是可判定的。另一种技术使用了自动机的存储语言概念。这被用于证明其下推可以“翻转”有界次数的下推自动机的有界问题是可判定的，并且即使我们为该设备增加额外的存储，有界性依然是可判定的。