Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Derivatives on Graphs for the Positive Calculus of Relations with Transitive Closure

Yoshiki Nakamura

TL;DR

<3-5 sentence high-level summary> This paper proves that the equational theory of the positive calculus of relations with transitive closure (PCoR*) is decidable and EXPSPACE-complete, and it further remains EXPSPACE-complete when extended with tests and nominals (hybrid logic). The authors introduce derivatives on graphs, extending Brzozowski/Antimirov derivatives from strings to graph structures, and leverage a linearly bounded pathwidth model property to build a finite automata construction via path decompositions. A central Decomposition Theorem shows derivatives decompose along gluing operations, enabling a reduction to two-way alternating finite automata (2AFA) containment problems, which yields the EXPSPACE upper bound and EXPSPACE-hardness via reductions from regular-expression universality. The work also provides encodings for top, converse, tests, and nominals within this automata framework, and establishes a PSPACE bound for certain intersection-bounded fragments, highlighting the boundary between tractable and intractable cases. Overall, the approach connects graph-language characterizations, automata theory, and structural graph decompositions to achieve a robust decision procedure for a broad relational-calculus setting with transitive closure.

Abstract

We prove that the equational theory of the positive calculus of relations with transitive closure (PCoR*) is EXPSPACE-complete. Here, PCoR* terms consist of the following standard operators on binary relations: identity, empty, universality, union, intersection, composition, converse, and reflexive transitive closure (so, PCoR* terms subsume Kleene algebra and allegory terms as fragments). Additionally, we show that the equational theory of PCoR* extended with tests and nominals (in hybrid logic) is still EXPSPACE-complete; moreover, it is PSPACE-complete for its intersection-free fragment. To this end, we design derivatives on graphs by extending derivatives on words for regular expressions. The derivatives give a finite automata construction on path decompositions, like those on words. Because the equational theory has a linearly bounded pathwidth model property, we can decide the equational theory of PCoR* using these automata.

Derivatives on Graphs for the Positive Calculus of Relations with Transitive Closure

TL;DR

<3-5 sentence high-level summary> This paper proves that the equational theory of the positive calculus of relations with transitive closure (PCoR*) is decidable and EXPSPACE-complete, and it further remains EXPSPACE-complete when extended with tests and nominals (hybrid logic). The authors introduce derivatives on graphs, extending Brzozowski/Antimirov derivatives from strings to graph structures, and leverage a linearly bounded pathwidth model property to build a finite automata construction via path decompositions. A central Decomposition Theorem shows derivatives decompose along gluing operations, enabling a reduction to two-way alternating finite automata (2AFA) containment problems, which yields the EXPSPACE upper bound and EXPSPACE-hardness via reductions from regular-expression universality. The work also provides encodings for top, converse, tests, and nominals within this automata framework, and establishes a PSPACE bound for certain intersection-bounded fragments, highlighting the boundary between tractable and intractable cases. Overall, the approach connects graph-language characterizations, automata theory, and structural graph decompositions to achieve a robust decision procedure for a broad relational-calculus setting with transitive closure.

Abstract

We prove that the equational theory of the positive calculus of relations with transitive closure (PCoR*) is EXPSPACE-complete. Here, PCoR* terms consist of the following standard operators on binary relations: identity, empty, universality, union, intersection, composition, converse, and reflexive transitive closure (so, PCoR* terms subsume Kleene algebra and allegory terms as fragments). Additionally, we show that the equational theory of PCoR* extended with tests and nominals (in hybrid logic) is still EXPSPACE-complete; moreover, it is PSPACE-complete for its intersection-free fragment. To this end, we design derivatives on graphs by extending derivatives on words for regular expressions. The derivatives give a finite automata construction on path decompositions, like those on words. Because the equational theory has a linearly bounded pathwidth model property, we can decide the equational theory of PCoR* using these automata.
Paper Structure (51 sections, 52 theorems, 110 equations)

This paper contains 51 sections, 52 theorems, 110 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. PCoR*: The Positive Calculus of Relations with Transitive Closure
  4. Semantics: relational models
  5. An alternative semantics: graph languages
  6. Comparison to word languages
  7. Kleene lattice terms: a core fragment of PCoR* terms
  8. Second alternative semantics: run (DAG with vertices of one fan-in and one fan-out) languages
  9. Compositions on runs
  10. Left quotients of runs
  11. Runs on structures
  12. Compositions on $\mathfrak A$-runs
  13. Left quotients of $\mathfrak A$-runs
  14. Labeled Kleene Lattice Terms
  15. Semantics: relational models
  16. ...and 36 more sections

Key Result

Proposition 2.3

For all PCoR* terms $t$, we have $\mathop{\mathrm{\mathrm{iw}}}\nolimits( t ) \le \| t \|$.

Theorems & Definitions (129)

  • Definition 2.1
  • Remark 2.2
  • Proposition 2.3
  • proof
  • Proposition 2.4
  • proof : Proof (Corollary of bodlaenderPartialArboretumGraphs1998)
  • Proposition 2.5
  • proof
  • Proposition 2.6: andrekaEquationalTheoryKleene2011 (for PCoR* without $\top$), brunetPetriAutomata2017 (for PCoR*)
  • proof
  • ...and 119 more