2025/12/28 by Yoshiki Nakamura, Nakamura, Yoshiki
Biochemistry, Genetics and Molecular Biology · Computer Science · #Algebra over a field #Automaton #Binary relation #Countable set #DNA and Biological Computing #Extension (predicate logic) #Formal Methods in Verification #Graph algebra #Kleene algebra #Kleene's recursion theorem #Unary operation #Universal algebra #semigroups and automata theory
paper · pdf · open access · doi:10.48550/arxiv.2512.22930
published in arXiv (Cornell University) (Cornell University)
openalex publication_date 2025/12/28 · openalex created_date 2025/12/31 · openalex updated_date 2026/07/28
In this paper, we show that the equational theory of relational Kleene algebra with the graph loop operator (a.k.a. fixset) is PSpace-complete. Here, the graph loop is the unary operator that restricts a binary relation to the identity relation. We further show that this 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 ExpTime-complete, we show that the equational theory of relational KAT with domain is 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 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.