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

Diego Figueira; Santiago Figueira

arxiv: 2501.11641 · v2 · submitted 2025-01-20 · 💻 cs.LO · cs.DB

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

Diego Figueira , Santiago Figueira This is my paper

Pith reviewed 2026-05-23 05:12 UTC · model grok-4.3

classification 💻 cs.LO cs.DB

keywords UCPDL+UNFO*expressive powertree-widthpebble bisimulationsatisfiabilitymodel checkingPDL

0 comments

The pith

UCPDL+ equates to UNFO* and strictly contains ICPDL, CQ, CRPQ, and Regular Queries while remaining 2ExpTime decidable for satisfiability.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines UCPDL+ as an extension of CPDL that adds a universal modality and studies its relation to other formalisms. It establishes that UCPDL+ coincides exactly with UNFO extended by unary transitive closure and properly contains several well-known query and modal languages. Subclasses of formulas are organized by the tree-width of their underlying graphs, with tree-width 1 and 2 both equivalent to ICPDL and higher widths strictly increasing expressive power. These fixed-width classes are characterized by pebble bisimulation games, which also yield a tree-like model property and PTime model checking. Satisfiability for the full logic stays in 2ExpTime, matching the complexity of ICPDL.

Core claim

UCPDL+ is equivalent to UNFO* and therefore strictly contains ICPDL, CQ, CRPQ, Regular Queries and CQPDL. The satisfiability problem for UCPDL+ (and thus for UNFO*) is 2ExpTime-complete. For each fixed tree-width k the expressive power of CPDL+ formulas of tree-width k is captured by a k-pebble bisimulation game; formulas of tree-width at most 2 coincide with ICPDL while each increment beyond 2 yields a strict increase. The logic admits a tree-like model property, and model checking for any fixed tree-width fragment lies in PTime.

What carries the argument

UCPDL+ (PDL with converse and universal modality) together with its tree-width stratification and the corresponding pebble bisimulation games that characterize indistinguishability at each fixed width.

If this is right

Satisfiability for UNFO* is 2ExpTime-complete.
Model checking for any fixed tree-width fragment of CPDL+ is in PTime.
Expressive power of CPDL+ formulas grows strictly with tree-width once the width exceeds 2.
The tree-like model property holds for the full UCPDL+ logic.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The pebble-game characterization may transfer decidability or complexity results to other fragments of first-order logic that admit similar width measures.
Because UCPDL+ sits above both modal and query languages, algorithms developed for one side could be reused on the other via the common syntax.
The coincidence of tree-width 1 and 2 with ICPDL suggests that further width increases are the only route to greater power inside this family.

Load-bearing premise

Pebble bisimulation games with a fixed number of pebbles correctly capture which structures are indistinguishable by CPDL+ formulas of each fixed tree-width.

What would settle it

Two finite structures that agree on every CPDL+ sentence of tree-width 3 yet are distinguished by a 3-pebble bisimulation game, or vice versa, would refute the characterization.

read the original 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+.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

UCPDL+ unifies PDL variants, CQs and UNFO* with tree-width fragments for CPDL+ and 2ExpTime satisfiability, but the pebble-game characterization needs checking for the strict-increase claims.

read the letter

The main thing this paper does is introduce UCPDL+ as equivalent to UNFO* (UNFO plus unary transitive closure) while strictly containing ICPDL, CQ, CRPQ, regular queries and UNFO^reg. For CPDL+ they define tree-width on the formula graph, show that widths 1 and 2 coincide with ICPDL, and claim that each higher fixed width adds expressive power, characterized by a k-pebble bisimulation game. From the games they derive a tree-like model property, 2ExpTime satisfiability for the full logic (matching ICPDL), and PTime model checking when tree-width is fixed. The unification and the tree-width parameterization are the concrete new pieces; the complexity results line up with what was already known for the smaller fragments. The pebble-game characterization is the load-bearing step for both the strict increases and the model-checking bound. The abstract states the equivalence but supplies no sketch, so the paper must show clearly that a game win implies the two formulas agree on every model (and vice versa). If that direction is tight, the separations and the PTime result follow; any gap there would affect the main claims. The rest of the argument uses standard techniques once the characterization is in place. This is for people working on modal logics, description logics or database query languages who care about expressive power hierarchies and decidability. Someone extending UNFO or PDL would get direct use from the new fragments and the tree-width cut. It is worth sending to peer review; the results are specific enough that referees can check the game equivalence and the containments in detail.

Referee Report

2 major / 2 minor

Summary. The paper introduces UCPDL+ (CPDL extended with universal modality and additional constructs) and proves it equivalent to UNFO* (UNFO extended with unary transitive closure). It shows UCPDL+ strictly contains ICPDL, CQ, CRPQ, Regular Queries, CQPDL and UNFO^reg; defines natural tree-width subclasses of CPDL+ formulas; proves that tree-width 1 and 2 coincide with ICPDL while higher fixed tree-width strictly increases expressive power; characterizes each fixed tree-width class via k-pebble bisimulation games; establishes a tree-like model property; proves 2ExpTime-completeness of satisfiability for UCPDL+ (hence for UNFO*) and ExpTime for some subclasses; and shows PTime model checking for each fixed tree-width fragment.

Significance. If the central claims hold, the work supplies a unifying logic that sits above several well-studied modal and query languages, supplies matching complexity upper bounds, and introduces a tree-width parameterization together with pebble-game characterizations that yield both separation results and tractable model checking. The equivalence to UNFO* and the tree-like model property are particularly useful for transferring results between modal and first-order fragments.

major comments (2)

[expressive-power / pebble-bisimulation section] The pebble-bisimulation characterization of CPDL+ formulas of each fixed tree-width k (stated in the abstract and developed in the section on expressive power and bisimulations) is load-bearing for both the strict-increase claim beyond tree-width 2 and the PTime model-checking result. The manuscript must supply explicit proofs (or detailed sketches) for both directions of the equivalence, especially the direction “a k-pebble game win implies that the two structures satisfy exactly the same CPDL+ formulas of tree-width k”; any gap here would undermine the separation and complexity statements.
[equivalence section] § on equivalence between UCPDL+ and UNFO*: the two-directional translation must be spelled out in sufficient detail to verify that unary transitive closure is faithfully captured by the UCPDL+ constructs and conversely; the current abstract statement alone does not allow verification that the equivalence preserves the tree-width parameterization used later.

minor comments (2)

[abstract / introduction] The abstract refers to “some known extensions thereof (Regular Queries and CQPDL)” without citations; add explicit references or definitions in the introduction or related-work section.
A diagram summarizing the containment hierarchy (UCPDL+ vs. ICPDL, CQ, UNFO*, etc.) would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive report. We address the two major comments below and will incorporate the requested expansions into the revised manuscript.

read point-by-point responses

Referee: [expressive-power / pebble-bisimulation section] The pebble-bisimulation characterization of CPDL+ formulas of each fixed tree-width k (stated in the abstract and developed in the section on expressive power and bisimulations) is load-bearing for both the strict-increase claim beyond tree-width 2 and the PTime model-checking result. The manuscript must supply explicit proofs (or detailed sketches) for both directions of the equivalence, especially the direction “a k-pebble game win implies that the two structures satisfy exactly the same CPDL+ formulas of tree-width k”; any gap here would undermine the separation and complexity statements.

Authors: We agree that the current presentation of the pebble-bisimulation characterizations provides only high-level outlines rather than fully explicit proofs for both directions. In particular, the direction establishing that a win for the duplicator in the k-pebble game implies agreement on all CPDL+ formulas of tree-width k requires additional detail. The revised manuscript will include complete proofs (or self-contained detailed sketches) for both directions of each fixed-k equivalence. revision: yes
Referee: [equivalence section] § on equivalence between UCPDL+ and UNFO*: the two-directional translation must be spelled out in sufficient detail to verify that unary transitive closure is faithfully captured by the UCPDL+ constructs and conversely; the current abstract statement alone does not allow verification that the equivalence preserves the tree-width parameterization used later.

Authors: We acknowledge that the equivalence between UCPDL+ and UNFO* is currently stated at the level of the abstract and high-level claims without the full two-directional translations. The revised version will spell out the translations in detail, explicitly showing how unary transitive closure is captured by the UCPDL+ constructs (and vice versa) while preserving the tree-width measure on formulas. revision: yes

Circularity Check

0 steps flagged

No circularity; all claims rest on independent definitions and proofs

full rationale

The paper defines UCPDL+ and CPDL+ from standard PDL primitives, then proves (rather than assumes) the tree-width equivalences, the pebble-bisimulation characterization, the tree-like model property, and the 2ExpTime bound. No equation or central claim reduces by construction to a fitted parameter, a self-citation, or a renamed input; the bisimulation-game equivalence is stated as a theorem derived from the semantics, not presupposed to justify itself. The derivation chain therefore remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The claims rest on the semantic definitions of the new logics, the standard model theory of modal and first-order logics, and the well-definedness of tree-width on formula graphs; no numerical parameters are fitted.

axioms (2)

standard math Standard Kripke semantics and bisimulation invariance for modal logics
Invoked throughout the expressive-power and model-checking arguments.
domain assumption Tree-width of the underlying graph of a formula is a well-defined integer
Used to partition CPDL+ into subclasses whose expressive power is characterized.

invented entities (1)

UCPDL+ no independent evidence
purpose: New logic family that unifies the listed formalisms
Introduced by extending CPDL with intersection, universal modality and additional constructs; no independent evidence outside the paper.

pith-pipeline@v0.9.0 · 5909 in / 1412 out tokens · 43761 ms · 2026-05-23T05:12:07.198677+00:00 · methodology

discussion (0)

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

Guarded Negation Transitive Closure Logic
cs.LO 2025-01 unverdicted novelty 7.0

GNTC satisfiability is 2ExpTime-complete and model checking is P^NP[O(log² n)]-complete via polynomial and exponential reductions to UNTC and 2-way alternating parity tree automata.