高阶上下文无关过程的符号可达性分析
计算机科学中的逻辑
2007-05-29 v1
摘要
我们考虑高阶上下文无关过程的符号可达性分析问题。这些模型是上下文无关过程（也称为 BPA 过程）的推广，其中每个过程操作的数据结构可视为嵌套的栈堆栈。我们的主要结果是：对于任意高阶上下文无关过程，给定正则配置集的所有前驱集也是正则的且可有效构造。该结果推广了已知的一阶上下文无关过程的类似结果。我们表明，在对配置施加正则约束的情况下，该结果在向后可达性分析中同样成立。作为推论，我们获得了一种针对具有正则原子谓词的时序逻辑 E(U,X)（即仅限于 EU 和 EX 模态的 CTL 片段）的符号模型检测算法。
引用
@article{arxiv.0705.3888,
title = {Symbolic Reachability Analysis of Higher-Order Context-Free Processes},
author = {Ahmed Bouajjani and Antoine Meyer},
journal= {arXiv preprint arXiv:0705.3888},
year = {2007}
}