有界下逼近

我们展示了一个新的、构造性的证明，证明以下语言理论结果：对于每个上下文无关语言L，存在一个包含于L的有界上下文无关语言L'，它与L具有相同的Parikh（交换）像。有界语言由Ginsburg和Spanier引入，是形如w1*w2*...wk*的正则语言的子集，其中w1,...,wk是有限单词。特别地，上下文无关语言的有界子集具有良好的结构和可判定性性质。我们的证明分两部分进行。首先，使用语言半环上的牛顿迭代，我们构造了L的一个上下文无关子集Ls，它可以表示为对线性语言的序列替换，并且与L具有相同的Parikh像。其次，我们归纳地构造了Ls的一个Parikh等价的有界上下文无关子集。我们展示了该结果在模型检验中的两个应用：用于下逼近多线程过程化程序的可达状态空间，以及用于下逼近递归计数器程序的可达状态空间。上述构造的有界语言为原始问题提供了可判定的下逼近。通过迭代该构造，我们得到了原始问题的一个半算法，该算法构造一个下逼近序列，使得序列中任意两个下逼近都无法相互比较。这提供了进展保证：L中的每个单词w都在序列的某个下逼近中。此外，我们证明我们的方法包含了多线程程序的上下文有界可达性。