Decidability of Identity-free Relational Kleene Lattices

Paul Brunet 1, 2 Damien Pous 1, 2
2 PLUME - Preuves et Langages
LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : Families of binary relations are important interpretations of regular expressions, and the equivalence of two regular expressions with respect to their relational interpretations is decidable: the problem reduces to the equality of the denoted regular languages. Putting together a few results from the literature, we first make explicit a generalisation of this reduction, for regular expressions extended with converse and intersection: instead of considering sets of words (i.e., formal languages), one has to consider sets of directed and labelled graphs. We then focus on identity-free regular expressions with intersection—a setting where the above graphs are acyclic—and we show that the corresponding equational theory is decidable. We achieve this by defining an automaton model, based on Petri Nets, to recognise these sets of acyclic graphs, and by providing an algorithm to compare such automata.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [16 references]  Display  Hide  Download
Contributor : David Baelde <>
Submitted on : Wednesday, December 31, 2014 - 3:42:46 PM
Last modification on : Wednesday, November 21, 2018 - 1:13:55 AM
Document(s) archivé(s) le : Wednesday, April 1, 2015 - 10:26:17 AM


Files produced by the author(s)


  • HAL Id : hal-01099137, version 1



Paul Brunet, Damien Pous. Decidability of Identity-free Relational Kleene Lattices. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. ⟨hal-01099137⟩



Record views


Files downloads