Abstract
The equational theory generated by all algebras of binary relations with operations of union, composition, converse and reflexive transitive closure was studied by Bernátsky, Bloom, Ésik, and Stefanescu in 1995. We reformulate some of their proofs in syntactic and elementary terms, and we provide a new algorithm to decide the corresponding theory. This algorithm is both simpler and more efficient; it relies on an alternative automata construction, that allows us to prove that the considered equational theory lies in the complexity class PSpace. Specific regular languages appear at various places in the proofs. Those proofs were made tractable by considering appropriate automata recognising those languages, and exploiting symmetries in those automata. © 2014 Springer International Publishing.
Cite
CITATION STYLE
Brunet, P., & Pous, D. (2014). Kleene algebra with converse. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8428 LNCS, pp. 101–118). Springer Verlag. https://doi.org/10.1007/978-3-319-06251-8_7
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
