Existential Calculi of Relations with Transitive Closure: Complexity and Edge Saturations
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2023
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909630592974848 |
|---|---|
| author | Nakamura, Yoshiki |
| author_facet | Nakamura, Yoshiki |
| contents | 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) $Π_{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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2304_12079 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Existential Calculi of Relations with Transitive Closure: Complexity and Edge Saturations Nakamura, Yoshiki Logic in Computer Science 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) $Π_{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. |
| title | Existential Calculi of Relations with Transitive Closure: Complexity and Edge Saturations |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2304.12079 |