DL-PA 与 DCL-PC：模型检测与可满足性问题确实属于 PSPACE
计算机科学中的逻辑
2014-12-01 v1
摘要
我们证明了命题赋值动态逻辑 (DL-PA) 和命题控制与委托联盟逻辑 (DCL-PC) 的模型检测问题和可满足性问题均属于 PSPACE。我们解释了为何 (Balbiani, Herzig, Troquard, 2013) 中提出的关于 DL-PA 模型检测问题具有 EXPTIME 难度的证明是错误的。我们还解释了为何 (van der Hoek, Walther, Wooldridge, 2010) 中给出的关于 DCL-PC 模型检测问题属于 PSPACE 的证明是不正确的。
引用
@article{arxiv.1411.7825,
title = {DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE},
author = {Philippe Balbiani and Andreas Herzig and François Schwarzentruber and Nicolas Troquard},
journal= {arXiv preprint arXiv:1411.7825},
year = {2014}
}