高阶上下文无关进程的符号可达性分析
摘要：高阶上下文无关过程的符号可达性分析问题。这些模型是上下文无关过程（也称为BPA过程）的推广，在这些模型中，每个过程操作一个可以被看作是一组堆栈的嵌套堆栈的数据结构。我们的主要结果是，对于任何高阶上下文无关过程，给定正则配置集合的所有前驱集是正则的且可以有效构建。这个结果推广了已知的适用于一级上下文无关过程的类似结果。我们还表明，在配置上施加正则约束的情况下，这个结果也适用于反向可达性分析。作为推论，我们得到了一个针对具有正则原子谓词的时态逻辑E(U,X)的符号模型检验算法，即CTL片段限制为EU和EX模态。
作者：Ahmed Bouajjani (LIAFA), Antoine Meyer (LIAFA)
论文ID：0705.3888
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-29