关于 PDL 的非上下文无关扩展
计算机科学中的逻辑
2007-07-18 v2
摘要
在过去的 25 年里，人们做了大量工作以寻求命题动态逻辑 (PDL) 的可判定非正则扩展。直到最近，才引入了一种 PDL 的表达性扩展，允许使用可见下推自动机 (VPAs) 作为描述程序的形式体系，并证明其可满足性问题对于确定性双指数时间是完全的。最近，VPA 形式体系被扩展为所谓的 k 阶段多栈可见下推自动机 (k-MVPAs)。与 VPAs 类似，已证明 k-MVPAs 的语言具有理想的 Effective closure properties，且空性问题是可判定的。在引入 k-MVPAs 时，有人提出疑问：用 k-MVPAs 扩展 PDL 是否仍会导致可判定的逻辑。本文对此给出了否定回答。我们证明，即使是对于具有两个栈的 2 阶段 MVPAs 扩展 PDL，其可满足性也变为 \Sigma_1^1-完全。
引用
@article{arxiv.0707.0562,
title = {On a Non-Context-Free Extension of PDL},
author = {Stefan Göller and Dirk Nowotka},
journal= {arXiv preprint arXiv:0707.0562},
year = {2007}
}