一句话：证明 PCoR* 及其测试/名义扩展的等式理论复杂度，并用图上导数构造自动机进行判定。
本文研究带传递闭包的正关系演算 PCoR* 的等式理论。PCoR* 项包含恒等、空、全关系、并、交、复合、逆以及自反传递闭包等二元关系算子，可涵盖 Kleene 代数与 allegory 片段。作者证明其等式理论是 EXPSPACE 完全的；将 PCoR* 扩展测试和 hybrid logic 的名义后，等式理论仍为 EXPSPACE 完全，而无交片段降为 PSPACE 完全。方法上，作者把正规表达式的词上导数推广为图上的导数，从而在路径分解上构造有限自动机；结合等式理论具有线性有界 pathwidth 的模型性质，可用这些自动机判定等式理论。
We prove that the equational theory of the positive calculus of relations with transitive closure (PCoR*) is EXPSPACE-complete. Here, PCoR* terms consist of the following standard operators on binary relations: identity, empty, universality, union, intersection, composition, converse, and reflexive transitive closure (so, PCoR* terms subsume Kleene algebra and allegory terms as fragments). Additionally, we show that the equational theory of PCoR* extended with tests and nominals (in hybrid logic) is still EXPSPACE-complete; moreover, it is PSPACE-complete for its intersection-free fragment. To this end, we design derivatives on graphs by extending derivatives on words for regular expressions. The derivatives give a finite automata construction on path decompositions, like those on words. Because the equational theory has a linearly bounded pathwidth model property, we can decide the equational theory of PCoR* using these automata.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Nakamura25,
title = {Derivatives on Graphs for the Positive Calculus of Relations with Transitive Closure},
author = {Yoshiki Nakamura},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 4},
year = {2025},
doi = {10.46298/lmcs-21(4:27)2025}
}