带图循环的关系Kleene代数的等式理论是PSPACE完全的 (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.

翻译：本文证明了带\emph{图循环}的关系Kleene代数的等式理论是PSPACE完全的。其中，图循环是将二元关系限制为恒等关系的一元运算符。我们进一步证明，即使扩展了顶元素、测试、逆运算和标称，这一PSPACE完全性仍然成立。值得注意的是，我们还得到以下结论：对于带测试的Kleene代数（KAT），带域的关系KAT的等式理论是PSPACE完全的，而带反域的关系KAT的等式理论是ExpTime完全的。为此，我们提出了一种在关系结构上的新型自动机模型，称为\emph{循环自动机}。循环自动机是在非确定性有限字符串自动机（NFA）的基础上，增加了一种测试当前顶点是否具有循环的转移类型。利用该模型，我们给出了从上述等式理论到双向交替字符串自动机语言包含问题的多项式时间归约。