Derivatives on Graphs for the Positive Calculus of Relations with Transitive Closure
<|reference_start|>Derivatives on Graphs for the Positive Calculus of Relations with Transitive Closure: We prove that the equational theory of the positive calculus of relations with transitive closure (PCoR*) is EXPSPACE-complete. 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 terms 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.<|reference_end|>
@article{nakamura2024derivatives,
    title={Derivatives on Graphs for the Positive Calculus of Relations with
  Transitive Closure},
    author={Yoshiki Nakamura},
    journal={arXiv preprint arXiv:2408.08236},
    year={2024},
    archivePrefix={arXiv},
    eprint={2408.08236},
    primaryClass={cs.LO}
}