有界次逼近
Bounded Underapproximations
摘要：
本文给出了以下语言理论结果的一个新的构造性证明：对于任何上下文无关语言L，存在包含在L中的有界上下文无关语言L'，它与L具有相同的Parikh（交换）象。有界语言是由Ginsburg和Spanier提出的，是w1*w2*.形式的正则语言的子集。wk* 对于一些有限字w1，...，wk.特别是上下文无关语言的有界子集具有良好的结构和可判定性。我们的证明分两部分进行。首先，利用语言半环上的牛顿迭代，我们构造了L的上下文无关子集Ls，它可以表示为线性语言上的替换序列，并且与L具有相同的Parikh像。其次，我们归纳地构造了Ls的Parikh等价的有界上下文无关子集。我们展示了这个结果在模型检验中的两个应用：欠近似多线程过程程序的可达状态空间和欠近似递归计数器程序的可达状态空间。上面构造的有界语言为原问题提供了一个可判定的欠近似。通过迭代构造，我们得到了原问题的半算法，该算法构造了一个欠近似序列，使得该序列中没有两个欠近似可以比较。这提供了一个进度保证：L中的每个字w都在序列的某种欠近似中。此外，我们表明，我们的方法包括上下文有界的可达性多线程程序。
英文摘要：
We show a new and constructive proof of the following language-theoretic result: for every context-free language L, there is a bounded context-free language L' included in L which has the same Parikh (commutative) image as L. Bounded languages, introduced by Ginsburg and Spanier, are subsets of regular languages of the form w1*w2*...wk* for some finite words w1,...,wk. In particular bounded subsets of context-free languages have nice structural and decidability properties. Our proof proceeds in two parts. First, using Newton's iterations on the language semiring, we construct a context-free subset Ls of L that can be represented as a sequence of substitutions on a linear language and has the same Parikh image as L. Second, we inductively construct a Parikh-equivalent bounded context-free subset of Ls. We show two applications of this result in model checking: to underapproximate the reachable state space of multithreaded procedural programs and to underapproximate the reachable state space of recursive counter programs. The bounded language constructed above provides a decidable underapproximation for the original problems. By iterating the construction, we get a semi-algorithm for the original problems that constructs a sequence of underapproximations such that no two underapproximations of the sequence can be compared. This provides a progress guarantee: every word w in L is in some underapproximation of the sequence. In addition, we show that our approach subsumes context-bounded reachability for multithreaded programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
