Derivatives on Graphs for the Positive Calculus of Relations with Transitive Closure

TL;DR

This paper establishes the computational complexity of the positive calculus of relations with transitive closure, showing it is EXPSPACE-complete, and introduces derivatives on graphs for automata-based decision procedures.

Contribution

It proves the EXPSPACE-completeness of PCoR* and extends derivatives on graphs to facilitate automata construction for relation calculus decision problems.

Findings

PCoR* equational theory is EXPSPACE-complete.

Automata construction on graphs via derivatives is feasible.

Decidability of PCoR* using automata with path decomposition.

Abstract

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.