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

2023/04/24 by Yoshiki Nakamura, Nakamura, Yoshiki · 1 citation
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.2304.12079

openalex publication_date 2023/04/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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) Π₁⁰-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.

Cited by

• Undecidability of the Emptiness Problem of Deterministic Propositional While Programs with Graph Loop: Hypothesis Elimination Using Loops

Related

• Derivatives on Graphs for the Positive Calculus of Relations with Transitive Closure
• PTIME Computation of Transitive Closures of Octagonal Relations
• Undecidability of the Emptiness Problem of Deterministic Propositional While Programs with Graph Loop: Hypothesis Elimination Using Loops
• The Existential Theory of Equations with Rational Constraints in Free Groups is PSPACE-Complete
• On the satisfiability problem for fragments of the two-variable logic with one transitive relation