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, characterization of bisimulation, 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+.

翻译：我们引入 CPDL+，这是一类植根于命题动态逻辑（PDL）的表达性逻辑家族。在表达力方面，CPDL+ 严格包含扩展了交叉与逆的 PDL（即 ICPDL），以及合取查询（CQ）、合取正则路径查询（CRPQ）或其某些已知扩展（正则查询和 CQPDL）。我们研究了 CPDL+ 的表达力、互模拟特征、可满足性和模型检测问题。我们论证，CPDL+ 的自然子类可根据公式底层图的树宽来定义。我们证明，树宽为 2 的 CPDL+ 公式类等价于 ICPDL，且它也与树宽为 1 的 CPDL+ 公式类重合。然而，在树宽 2 之上，增加树宽会严格提升表达力。我们利用带卵石的互模拟博弈，刻画了每个固定树宽公式类的表达力。基于此刻画，我们证明 CPDL+ 具有树状模型性质。我们证明，在固定树宽公式类上，可满足性问题是 2ExpTime 可判定的，这与 ICPDL 的复杂度一致。我们还展示了可满足性可归约为 ExpTime 的类。最后，我们证明，与完整的 CPDL+ 类不同，固定树宽公式的模型检测问题属于 \ptime 复杂度。