强化版 PDL：关于具有交与逆的 PDL 的表达性扩展
计算机科学中的逻辑
2023-04-21 v1 人工智能
数据库
摘要
我们引入 CPDL+，一个根植于命题动态逻辑(PDL)的表达性逻辑族。在表达力上，CPDL+ 严格包含扩展了交与逆的 PDL(亦称 ICPDL)以及合取查询(CQ)、合取正则路径查询(CRPQ)或其某些已知扩展(正则查询与 CQPDL)。我们研究了 CPDL+ 的表达力、互模拟刻画、可满足性与模型检测。我们认为 CPDL+ 的自然子类可根据公式底层图的树宽来定义。我们证明树宽为 2 的 CPDL+ 公式类等价于 ICPDL，且也与树宽为 1 的 CPDL+ 公式类重合。然而，超过树宽 2 后，增大树宽会严格提升表达力。我们根据带鹅卵石的互模拟博弈刻画了每个固定树宽公式类的表达力。基于该刻画，我们证明 CPDL+ 具有类树模型性质。我们证明可满足性问题在固定树宽公式上是 2ExpTime 可判定的，与 ICPDL 的复杂度一致。我们也给出了可满足性可归约为 ExpTime 的类。最后，我们确立固定树宽公式的模型检测问题在 \ptime 内，而与完整类 CPDL+ 相反。
引用
@article{arxiv.2304.10381,
title = {PDL on Steroids: on Expressive Extensions of PDL with Intersection and Converse},
author = {Diego Figueira and Santiago Figueira and Edwin Pin},
journal= {arXiv preprint arXiv:2304.10381},
year = {2023}
}