pith. sign in

arxiv: 2512.22930 · v2 · submitted 2025-12-28 · 💻 cs.LO

The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete

Yoshiki Nakamura This is my paper

Pith reviewed 2026-05-16 20:13 UTC · model grok-4.3

classification 💻 cs.LO
keywords equational theoryrelational Kleene algebragraph loopPSPACE-completeloop-automataKleene algebra with testsdomain operatorrelational models
0
0 comments X

The pith

The equational theory of relational Kleene algebra with the graph loop operator is PSPACE-complete.

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

This paper proves that deciding whether two terms denote the same relation is PSPACE-complete when the signature includes the graph loop operator, which restricts a binary relation to the identity on its diagonal. The same PSPACE bound holds after the terms are extended with top, tests, converse, and nominals interpreted over ordinary relational models. The work also resolves an open question for Kleene algebra with tests by showing that the relational version using domain remains PSPACE-complete, while the version using antidomain is already known to be EXPTIME-complete. The proof introduces loop-automata, an automaton model on graphs, and reduces the equational problems to language inclusion for two-way alternating automata in polynomial time.

Core claim

The equational theory of relational Kleene algebra with the graph loop operator is PSPACE-complete. This complexity bound remains unchanged when the signature is enlarged with top, tests, converse, and nominals over relational models. For Kleene algebra with tests the relational version equipped with domain is PSPACE-complete, while the version equipped with antidomain is EXPTIME-complete.

What carries the argument

Loop-automata: an automaton model on graphs that extends ordinary nondeterministic finite automata with an additional transition type that tests whether the current vertex carries a loop edge.

If this is right

  • Validity of equations in the extended relational algebras can be decided by a PSPACE procedure.
  • Adding converse and nominals does not raise the complexity above PSPACE.
  • The choice between domain and antidomain in Kleene algebra with tests produces a genuine complexity gap of PSPACE versus EXPTIME.

Where Pith is reading between the lines

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

  • The loop operator encodes a limited form of fixed-point behavior that stays inside PSPACE rather than pushing the problem into EXPTIME.
  • The loop-automata technique may transfer to other graph-based or relational logics whose models are finite structures.
  • PSPACE-completeness indicates that practical implementations are feasible in principle but will encounter worst-case hardness on some inputs.

Load-bearing premise

The polynomial-time reduction that translates equational problems into language-inclusion questions for two-way alternating automata via the loop-automata construction is correct.

What would settle it

A concrete pair of terms that are equal in every relational model containing the graph loop operator, yet whose associated loop-automata languages are unequal.

read the original abstract

In this paper, we show that the equational theory of relational Kleene algebra with the \emph{graph loop} operator (a.k.a.~\emph{fixset}) is \textsc{PSpace}-complete. Here, the graph loop is the unary operator that restricts a binary relation to the identity relation. We further show that this \textsc{PSpace}-completeness still holds by extending the terms with top, tests, converse, and nominals, over relational models. Notably, for Kleene algebra with tests (KAT), while the equational theory of relational KAT with antidomain is \textsc{ExpTime}-complete, we show that the equational theory of relational KAT with domain is \textsc{PSpace}-complete, thereby resolving a problem left open in previous works. To this end, we introduce a novel automaton model on relational structures (graphs), called \emph{loop-automata}. Loop-automata extend nondeterministic finite automata with a transition type that tests whether the current vertex has a loop. Using this model, we can give a polynomial-time reduction from the equational theories above to the language inclusion problem for 2-way alternating automata.

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.

Referee Report

1 major / 3 minor

Summary. The paper proves that the equational theory of relational Kleene algebra with the graph loop (fixset) operator is PSPACE-complete. The result extends uniformly to terms augmented with top, tests, converse, and nominals interpreted over relational models. It further resolves an open question by showing that the equational theory of relational Kleene algebra with tests (KAT) is PSPACE-complete when using domain but EXPTIME-complete when using antidomain. The proof proceeds by introducing loop-automata (nondeterministic automata on graphs with an explicit loop-test transition) and giving a polynomial-time reduction from equational validity to language inclusion for 2-way alternating automata.

Significance. If the reduction is correct, the result supplies a sharp complexity classification for an important family of Kleene-algebra variants and supplies a reusable automaton model for the fixset operator. The construction handles the domain/antidomain distinction by differing transition types while remaining inside PSPACE, and the uniform extension to converse and nominals is a technical strength. The work therefore advances both the algebraic and automata-theoretic sides of the field.

major comments (1)
  1. [§4.2] §4.2, Definition 4.3 and Lemma 4.5: the semantic equivalence between the loop-automaton transition for the graph-loop operator and the relational fixset semantics must be verified explicitly for the case that includes converse; the current sketch leaves open whether the 2-way alternation correctly simulates the converse without an exponential blow-up in the state space.
minor comments (3)
  1. [§2] The notation for the graph-loop operator alternates between “loop” and “fixset” in the introduction and §2; adopt a single symbol and term throughout.
  2. [Figure 3] Figure 3 (loop-automaton example) would benefit from an explicit legend distinguishing the three transition types.
  3. [Theorem 5.1] Theorem 5.1 claims a linear-size construction; add a sentence confirming that the handling of nominals does not introduce an extra logarithmic factor.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript, positive evaluation of its significance, and recommendation for minor revision. We address the single major comment below.

read point-by-point responses

  1. Referee: §4.2, Definition 4.3 and Lemma 4.5: the semantic equivalence between the loop-automaton transition for the graph-loop operator and the relational fixset semantics must be verified explicitly for the case that includes converse; the current sketch leaves open whether the 2-way alternation correctly simulates the converse without an exponential blow-up in the state space.

    Authors: We agree that an explicit verification for the converse case improves clarity. In the revised manuscript we will expand the proof of Lemma 4.5 with a full inductive case analysis that includes converse. The loop-automaton transition for the graph-loop operator is defined locally at each vertex by testing for the presence of a self-loop; this local test is independent of edge direction. Converse is simulated in the 2-way alternating automaton by allowing the head to traverse edges in the reverse direction on the underlying graph, which is a standard feature of 2-way models and does not require additional states. Because the loop-test remains a constant-time local check and alternation is used only to resolve the nondeterminism already present in the term, the state space of the constructed automaton stays polynomial in the size of the input term. Semantic equivalence follows by structural induction, noting that the fixset operator satisfies fixset(R^op) = fixset(R) for any relation R. revision: yes

Circularity Check

0 steps flagged

Derivation is self-contained via explicit reduction to independent automata problem

full rationale

The paper establishes PSPACE-completeness by defining loop-automata on relational structures and constructing a direct polynomial-time reduction from equational validity (in the extended relational Kleene algebra with graph loop, top, tests, converse, and nominals) to language inclusion for 2-way alternating automata. This construction encodes the graph-loop operator via a new transition type and extends uniformly to the additional operators while preserving relational semantics. Hardness follows from embedding a known PSPACE-complete problem for such algebras, with no fitted parameters, self-definitional equations, or load-bearing self-citations; the domain/antidomain distinction is handled by differing transition types without circularity. The argument is independent of prior fitted results and resolves the open KAT-domain question through this fresh reduction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The claim rests on standard properties of relational models and Kleene algebra plus the known PSPACE-completeness of 2-way alternating automata inclusion; the only new element is the loop-automata construction.

axioms (2)
  • standard math Standard axioms of Kleene algebra and relational models hold
    Invoked throughout the reduction; taken from prior literature on Kleene algebra.
  • standard math Language inclusion for 2-way alternating automata is PSPACE-complete
    Used as the target problem in the reduction; cited as known.
invented entities (1)
  • loop-automata no independent evidence
    purpose: Nondeterministic automata on graphs that test for loops at the current vertex
    New model introduced to encode the graph-loop operator in the reduction.

pith-pipeline@v0.9.0 · 5507 in / 1242 out tokens · 25241 ms · 2026-05-16T20:13:41.049574+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

9 extracted references · 9 canonical work pages · 1 internal anchor

  1. [1]

    Andréka, S

    1 H. Andréka, S. Mikulás, and I. Németi. The equational theory of Kleene lattices.Theoretical Computer Science, 412(52):7099–7108, 2011.doi:10.1016/J.TCS.2011.09.024. 2 C. Areces and B. ten Cate. Hybrid logics. InHandbook of Modal Logic, volume 3 ofStudies in Logic and Practical Reasoning, pages 821–868. Elsevier, 2007.doi:10.1016/S1570-2464(07) 80017-6. ...

    work page doi:10.1016/j.tcs.2011.09.024 2011

  2. [2]

    doi:10.23638/LMCS-13(3:33)2017. 5 D. Calvanese, G. De Giacomo, M. Lenzerini, and M.Y. Vardi. Rewriting of regular expressions and regular path queries. InPODS, page 194–204. ACM, 1999.doi:10.1145/303976.303996. 6 B. Courcelle and J. Engelfriet.Graph Structure and Monadic Second-Order Logic. Number 138 in Encyclopedia of Mathematics and its Applications. C...

    work page doi:10.23638/lmcs-13(3:33)2017 2017

  3. [3]

    doi:10.1017/CBO9780511977619. 7 R. Danecki. Nondeterministic propositional dynamic logic with intersection is decidable. In SCT, volume 208 ofLNCS, pages 34–53. Springer, 1984.doi:10.1007/3-540-16066-3_5. 8 R. Danecki. Propositional dynamic logic with strong loop predicate. InMFCS, volume 176 of LNCS, pages 573–581. Springer, 1984.doi:10.1007/BFb0030342. ...

    work page doi:10.1017/cbo9780511977619 1984

  4. [4]

    doi:10.1007/978-3-662-44522-8_25. 13 S. Göller, M. Lohrey, and C. Lutz. PDL with intersection and converse: satisfiability and infinite-state model checking.The Journal of Symbolic Logic, 74(1):279–314,

    work page doi:10.1007/978-3-662-44522-8_25

  5. [5]

    doi: 10.2178/jsl/1231082313. 14 C. Kapoutsis and M. Zakzok. Alternation in two-way finite automata.Theoretical Computer Science, 870:75–102, 2021.doi:10.1016/j.tcs.2020.12.011. 15 D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. In LICS, pages 214–225. IEEE, 1991.doi:10.1109/LICS.1991.151646. 16 D. Kozen. Kleene alge...

    work page doi:10.2178/jsl/1231082313 2021

  6. [6]

    org/abs/2504.20415v1

    URL:http://arxiv. org/abs/2504.20415v1. 27 P.W. O’Hearn. Incorrectness logic.Proceedings of the ACM on Programming Languages, 4(POPL):10:1–10:32, 2019.doi:10.1145/3371078. 28 D. Pous. On the positive calculus of relations with transitive closure. InSTACS, volume 96 of LIPIcs, pages 3:1–3:16. Schloss Dagstuhl, 2018.doi:10.4230/LIPICS.STACS.2018.3. 29 D. Po...

    work page doi:10.1145/3371078 2019

  7. [7]

    URL:https://arxiv.org/ abs/1304.2637v2. 32 I. Sedlár. On the complexity of Kleene algebra with domain. InRAMICS, volume 13896 of LNCS, pages 208–223. Springer, 2023.doi:10.1007/978-3-031-28083-2_13. 33 I. Sedlár. Kleene algebra with dynamic tests: Completeness and complexity,

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.1007/978-3-031-28083-2_13 2023

  8. [8]

    URL: https://arxiv.org/abs/2311.06937v1. 34 A. Tarski. On the calculus of relations.The Journal of Symbolic Logic, 6(3):73–89,

    work page arXiv

  9. [9]

    On the calculus of relations

    doi:10.2307/2268577. 35 K.Thompson. Programmingtechniques: Regularexpressionsearchalgorithm.Communications of the ACM, 11(6):419–422, 1968.doi:10.1145/363347.363387. 36 L. Verscht and B.L. Kaminski. A taxonomy of hoare-like logics: Towards a holistic view using predicate transformers and Kleene algebras with top and tests.Proc. ACM Program. Lang., 9(POPL)...

    work page doi:10.2307/2268577 1968