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+,这是一族有表达力的逻辑,根植于Propositional Dynamic Logic(PDL)。在表达力方面,CPDL+严格包含了通过添加交集和逆运算(即ICPDL)扩展的PDL,以及Conjunctive Queries(CQ)、Conjunctive Regular Path Queries(CRPQ)或一些已知扩展(Regular Queries和CQPDL)。我们研究了CPDL+的表达能力、双模拟的表征、可满足性和模型检验。我们认为,可以根据公式的底层图形的树的宽度来定义CPDL+的自然子类。我们证明了基于树宽度2的CPDL+公式与ICPDL等价,它也与树宽度为1的CPDL+公式相同。但是,在树宽度2之外,树宽度的增加会严格增加表达能力。我们基于夹子双模拟游戏的表征,表征了每个固定树宽度公式的表达能力。基于这种表征,我们证明了CPDL+具有树状模型性质。我们证明了在固定树宽度公式上,可满足性问题在2ExpTime上是可判定的,这与ICPDL的复杂度相符。我们还展示了使可满足性简化为ExpTime的类别。最后,我们证明了固定树宽度公式的模型检验问题在\ptime内,与完整类别的CPDL+相反。