Guarded Fragments Meet Dynamic Logic: The Story of Regular Guards

We study the Guarded Fragment with Regular Guards RGF which

combines the expressive power of the Guarded Fragment (GF)

with Propositional Dynamic Logic with Intersection and

Converse (ICPDL).

Our logic generalizes, in a uniform way, many

previously-studied extensions of GF, including

(conjunctions of) transitive or equivalence guards,

transitive or equivalence closure and more.

We prove 2ExpTime-completeness of the satisfiability

problem for RGF, showing that RGF is not harder than ICPDL

or GF.

Shifting to the query entailment problem, we provide

undecidability results that significantly strengthen and

solidify earlier results along those lines.

We conclude by identifying the maximal, in some natural

sense, ExpSpace-complete fragment of RGF.