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

TL;DR

This paper proves that the equational theory of relational Kleene algebra with the graph loop operator is PSPACE-complete, extending to various models and resolving open problems in algebraic logic.

Contribution

It establishes the PSPACE-completeness of the equational theory with the graph loop and related operators, introducing loop-automata for reductions.

Findings

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

Relational KAT with domain has PSPACE-complete theory, resolving previous open problems.

Introduces loop-automata, a new automaton model for relational structures.

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.