关于PDL的非上下文无关扩展
摘要：可见下推自动机是一种用于描述程序的形式主义。最近，可见下推自动机被扩展为所谓的k相位多栈可见下推自动机（k-MVPAs）。类似于可见下推自动机，已经证明了k-MVPAs的语言具有良好的有效闭包性质并且空集问题是可判定的。在介绍k-MVPAs的时候，曾经提出了一个问题，即用k-MVPAs扩展PDL是否仍然是可判定的逻辑。这里给出了否定的答案。我们证明，仅仅将PDL扩展为具有两个栈的2相位MVPAs时，可满足性问题就变成了Sigma 1 1完备问题。
作者：Stefan G"oller and Dirk Nowotka
论文ID：0707.0562
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-07-18