We introduce a new kind of pebble games, which capture logical indistinguishability for programs and formulas of 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). The games introduced here are closely related to the "existential k-pebble game" on first-order structures with binary and unary signatures, but in our setting we add an additional rule stating that a pebble cannot be placed too far away from another pebble. This allows us to separate natural fragments of CPDL that can be defined in terms of the "tree-width" of the underlying graphs of the expressions.
This extended abstract is based on the paper "PDL on Steroids: on Expressive Extensions of PDL with Intersection and Converse", accepted at LICS'23.