A Common Ancestor of PDL, Conjunctive Queries, and Unary Negation First-order

TL;DR

This work presents UCPDL+, a unifying framework that extends Propositional Dynamic Logic with Converse and universal modalities to capture both modal recursion and graph-structured queries. It establishes that UCPDL+ is equi-expressive with the unary-negation fragment UNFO* extended by unary transitive closure, and it characterizes the expressive power through a tree-width based hierarchy, bisimulation, and a tree-like model property. Satisfiability for UCPDL+ is 2ExpTime-complete (with ExpTime in fixed tree-width subclasses), while model checking is polynomial for fixed tree-width fragments; UNFO* satisfiability and UNTC are tightly connected to UCPDL+ via polynomial-time translations. The paper also develops a robust framework of simulations, bisimulations, and ω-regular tree automata to analyze satisfiability and model checking, providing deep insights into the relation between modal logics and graph query languages and enabling practical reasoning over complex data structures. Overall, the results offer a natural, well-behaved bridge between modal logics and graph querying, with strong theoretical guarantees and potential applications in verification and database querying.

Abstract

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+.

Figures (10)

• Figure 1: The landscape of expressive power and complexity. The arrow goes in the direction of the more expressive language, and all arrows are witnessed via polynomial time translations, except the red ones, which are exponential. For the query languages "CQ", "UC2RPQ", "Regular Queries", and "UCQPDL" we restrict to queries of arity 1 in order to be able to compare the expressive power. By "UC2RPQ"($\Tw$) we denote "UC2RPQs" whose underlying graph has "tree-width" $\leq k$. $\ICPDL_{\Iwidth\leq\ell}$ for any $\ell$, is the set of all $\ICPDL$ "formulas" $\varphi$ s.t. $\Iwidth(\varphi) \leq \ell$, introduced in DBLP:journals/jsyml/GollerLL09 and defined in \ref{['sec:solving-omega-reg-sat']}. $\CPDLp_{\Cqsizealt \leq \ell}$ for any $\ell$, is the set of all $\CPDLp$ "formulas" $\varphi$ s.t. $\Cqsize{\varphi} \leq \ell$, as defined in \ref{['sec:sat']}. (We assume any fixed $\ell\geq 2$ and $k \geq 2$ for the interpretation of expressiveness arrows.) The complexities correspond to the basic reasoning problem for each formalism: satisfiability for logics closed under negation, and containment for query languages of the "CQ"/"UC2RPQ" family. In blue we highlight the family of logics introduced in the present work.
• Figure 2: A. graphical representation of the "atoms" contained in the set $C=\{ \pi_{13}(x_1,x_3),$$\pi_{12}(x_1,x_2),$$\pi_{14}(x_1,x_4),$$\pi'_{14}(x_1,x_4),$$\pi_{33}(x_3,x_3),$$\pi_{32}(x_3,x_2),$$\pi_{24}(x_2,x_4),$$\pi_{42}(x_4,x_2) \}$; B. $\uGraph{C[x_1,x_2]}$; C. $\uGraph{C[x_3,x_4]}$; D. $\uGraph{C[x_2,x_2]}$. Observe that $\uGraph{C[x_1,x_2]},\uGraph{C[x_2,x_2]}\in\Tw[2]$ but $\uGraph{C[x_3,x_4]}\in\Tw[3]\setminus\Tw[2]$.
• Figure 3: An example of translation of a "conjunctive program" made up of only $\ICPDL$ "atoms" and 3 variables to . The name of the $\ICPDL$-"programs" $\pi_{C[x_3,x_3]}$ and $\pi_{C[x_1,x_2]}$ are the one used in Lemma \ref{['lemita']}.
• Figure 4: A "conjunctive program" $C[x_1,x_2]$ made up of only $\ICPDL$ "programs" and the steps of the algorithm to construct a semantically equivalent $\ICPDL$ formula from a "tree decomposition" of "tree-width" 2 of $\uGraph{C[x_1,x_2]}$. Rounded boxes represent the bags of such "tree decomposition" where variables $x_1,\dots,x_6$ are grouped (additional information such as edges and labels are not part of the "tree decomposition"). See Figure \ref{['fig:lemita']} for the definition of $\pi_{C[x_3,x_3]}$ and $\pi_{C[x_1,x_2]}$.
• Figure 5: Left: Kripke structures $K$ and $K'$. Center: an example of a game $\kSimGame[2]$ over $K$ and $K'$. The order of moves are: (S1), (D1), (S2), (D2). In fact, Duplicator can always answer to any Spoiler's move in $\kSimGame[2]$, and so $K,u_1 \pebblesim{2} K',v_1$. Right: a tree representation of a winning strategy for Spoiler in $\kSimGame[3]$ over $K$ and $K'$. All possible answers by Duplicator are shown. Duplicator cannot answer after (S2) and so $K,u_1 \not\pebblesim{3} K',v_1$. Observe that $K,u_1,u_1\models\pi$ and $K,v_1,v_1\not\models\pi$ for $\pi=\{c(x_s,x_4),a(x_s,x_3),a(x_3,x_4),b(x_s,x_2),b(x_2,x_4)\}[x_s,x_s]$. Graphically the vectors in the positions can be thought as moving color pebbles on the "Kripke structures". Only "Kripke structures" that change pebble positions with respect to the previous move are shown.

Theorems & Definitions (98)

• Remark 1
• Remark 2
• proof
• Proposition 1
• Proposition 2
• Proposition 3
• Theorem 4.1
• Proposition 4
• Lemma 1
• proof