We introduce and study UCPDL+, a family of expressive logics rooted in Propositional Dynamic Logic (PDL) with converse (CPDL) and universal modality (UCPDL). In terms of expressive power, UCPDL+ 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). Further, it is equivalent to the extension of the unary-negation fragment of first-order logic (UNFO) with unary transitive closure, which we denote by UNFO*, which in turn strictly contains a previously studied extension of UNFO with regular expressions known as UNFO^reg. We investigate the expressive power, indistinguishability via bisimulations, satisfiability, and model checking for UCPDL+ and 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 for UCPDL+ is decidable in 2ExpTime, coinciding with the complexity of ICPDL. As a consequence, the satisfiability problem for UNFO* is shown to be 2ExpTime-complete as well. 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+.

翻译：我们引入并研究UCPDL+，这是一类基于命题动态逻辑（PDL）及其逆运算（CPDL）和全域模态（UCPDL）的表达性逻辑族。在表达能力方面，UCPDL+严格包含扩展了交集和逆的PDL（即ICPDL），以及合取查询（CQ）、合取正则路径查询（CRPQ）或其某些已知扩展（正则查询和CQPDL）。此外，它等价于带有一元传递闭包的一元否定一阶逻辑片段（UNFO）的扩展，记为UNFO*，后者严格包含先前研究的带正则表达式的UNFO扩展（UNFO^reg）。我们研究了UCPDL+和CPDL+的表达能力、通过互模拟的不可区分性、可满足性以及模型检测问题。我们认为CPDL+的自然子类可根据公式底层图的树宽来定义。我们证明树宽为2的CPDL+公式类等价于ICPDL，同时也与树宽为1的CPDL+公式类重合。然而，超过树宽2后，增加树宽会严格增强表达能力。我们使用带石子的互模拟博弈刻画了每个固定树宽公式类的表达能力。基于这一刻画，我们证明CPDL+具有树状模型性质。我们证明UCPDL+的可满足性问题可在2ExpTime内判定，与ICPDL的复杂度一致。由此，UNFO*的可满足性问题也被证明为2ExpTime完全的。我们还展示了某些类的可满足性可降至ExpTime。最后，我们证明固定树宽公式类的模型检测问题属于PTime，这与完整的CPDL+类形成对比。