一句话:本文用边饱和刻画 ECoR* 及其片段的等式理论,并确定其可判定性与复杂度。
论文研究带传递闭包的存在关系演算 ECoR* 及其片段的等式理论的可判定性与复杂度。ECoR* 是在带传递闭包的正关系演算上加入项变量和常量的补而成。作者通过“边饱和”这一技术给出这些等式理论的刻画,并据此证明:不带传递闭包的 ECoR* 的等式理论是 coNP 完全的;不带交的 ECoR* 属于 coNEXP,而两个更小片段的等式理论是 PSPACE 完全的;完整 ECoR* 的等式理论是 Π_1^0 完全的。第二个结果还为若干 Kleene 代数扩展给出 PSPACE 上界,包括带 top 的 Kleene 代数在二元关系解释下的情形。
We study the decidability and complexity of equational theories of the existential calculus of relations with transitive closure (ECoR*) and its fragments, where ECoR* is the positive calculus of relations with transitive closure extended with complements of term variables and constants. We give characterizations of these equational theories by using edge saturations and we show that the equational theory is 1) coNP-complete for ECoR* without transitive closure; 2) in coNEXP for ECoR* without intersection and PSPACE-complete for two smaller fragments; 3) $\Pi _1^0$-complete for ECoR*. The second result gives PSPACE-upper bounds for some extensions of Kleene algebra, including Kleene algebra with top w.r.t. binary relations.