PSPACE-Completeness of the Equational Theory of Relational Kleene Algebra with Graph Loop

In this paper, we show that the equational theory of relational Kleene algebra with \emph{graph loop} 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 with top, tests, converse, and nominals. Notably, we also obtain that for Kleene algebra with tests (KAT), the equational theory of relational KAT with domain is PSpace-complete, whereas the equational theory of relational KAT with antidomain is ExpTime-complete. To this end, we introduce a novel automaton model on relational structures, named \emph{loop-automata}. Loop-automata are obtained from non-deterministic finite string automata (NFA) by adding a transition type that tests whether the current vertex has a loop. Using this model, we give a polynomial-time reduction from the above equational theories to the language inclusion problem for 2-way alternating string automata.