一句话：提出逻辑族 CPDL+，严格包含 ICPDL、CQ/CRPQ 等，并用树宽刻画表达力层次及可满足性/模型检测复杂度。
论文提出 CPDL+，一种以命题动态逻辑 PDL 为基础的高表达力逻辑族。在表达力上，CPDL+ 严格包含带交与逆的 PDL（ICPDL），并包含合取查询（CQ）、合取正则路径查询（CRPQ）及其若干已知扩展。作者研究其表达力、互模拟不可区分性、可满足性与模型检测，并按公式底层图的树宽定义自然子类。关键结果是：树宽 2 的公式等价于 ICPDL，且与树宽 1 相同；树宽超过 2 后表达力严格增加。他们用带卵石的互模拟博弈刻画各固定树宽类，证明 CPDL+ 具有树状模型性质；固定树宽可满足性为 2EXPTIME（与 ICPDL 一致），部分类为 EXPTIME，固定树宽模型检测为 PTIME，完整类则不然。
We introduce CPDL+, a family of expressive logics rooted in Propositional Dynamic Logic (PDL). In terms of expressive power, CPDL+ strictly contains PDL extended with intersection and converse (a.k.a. ICPDL) as well as Conjunctive Queries (CQ), Conjunctive Regular Path Queries (CRPQ), or some known extensions thereof (Regular Queries and CQPDL). We investigate the expressive power, indistinguishability via bisimulations, satisfiability, and model checking for CPDL+.We argue that natural subclasses of CPDL+ can be defined in terms of the tree-width of the underlying graphs of the formulas. We show that the class of CPDL+ formulas of tree-width 2 is equivalent to ICPDL, and that it also coincides with CPDL+ formulas of tree-width 1. However, beyond tree-width 2, incrementing the tree-width strictly increases the expressive power. We characterize the expressive power for every class of fixed tree-width formulas in terms of a bisimulation game with pebbles. Based on this characterization, we show that CPDL+ has a tree-like model property. We prove that the satisfiability problem is decidable in 2EXPTIME on fixed tree-width formulas, coinciding with the complexity of ICPDL. We also exhibit classes for which satisfiability is reduced to EXPTIME. Finally, we establish that the model checking problem for fixed tree-width formulas is in PTIME, contrary to the full class CPDL+.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-2304-10381,
title = {PDL on Steroids: on Expressive Extensions of PDL with Intersection and Converse},
author = {Diego Figueira and Santiago Figueira and Edwin Pin},
booktitle = {LICS},
year = {2023},
doi = {10.1109/lics56636.2023.10175813}
}