PDL on Steroids: on Expressive Extensions of PDL with Intersection and Converse

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 + . This pdf contains internal links: clicking on a notion leads to its definition. 1