paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Existential Calculi of Relations with Transitive Closure: Complexity and Edge Saturations

带传递闭包的存在关系演算:复杂性与边饱和
LICS 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2023匹配度 2/10 · 本文研究关系演算与传递闭包的等式理论可判定性与复杂度,属于纯逻辑/形式语义与Kleene代数理论,与用户关注的ML/Agentic程序静态分析、LLM改进静态分析/形式化验证、浮点程序分析及贝叶斯程序分析均无直接关联。仅在形式化验证的代数基础层面有非常边缘的联系。引用 8 inbox
Yoshiki Nakamura
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:本文用边饱和刻画 ECoR* 及其片段的等式理论,并确定其可判定性与复杂度。

论文研究带传递闭包的存在关系演算 ECoR* 及其片段的等式理论的可判定性与复杂度。ECoR* 是在带传递闭包的正关系演算上加入项变量和常量的补而成。作者通过“边饱和”这一技术给出这些等式理论的刻画,并据此证明:不带传递闭包的 ECoR* 的等式理论是 coNP 完全的;不带交的 ECoR* 属于 coNEXP,而两个更小片段的等式理论是 PSPACE 完全的;完整 ECoR* 的等式理论是 Π_1^0 完全的。第二个结果还为若干 Kleene 代数扩展给出 PSPACE 上界,包括带 top 的 Kleene 代数在二元关系解释下的情形。

问题
确定 ECoR* 及其片段(带传递闭包、补、交等运算的关系演算)的等式理论是否可判定,并精确刻画其复杂度。
方法
利用边饱和(edge saturations)对相关等式理论进行刻画,并结合归约与复杂度上/下界证明。
评估
通过理论证明建立各片段的复杂度界限,包括 coNP、coNEXP、PSPACE 与 Π_1^0 完全性,并导出若干 Kleene 代数扩展的 PSPACE 上界。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@inproceedings{abs-2304-12079,
  title = {Existential Calculi of Relations with Transitive Closure: Complexity and Edge Saturations},
  author = {Yoshiki Nakamura},
  booktitle = {LICS},
  year = {2023},
  doi = {10.1109/lics56636.2023.10175811}
}