Kleene algebra with converse
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.
Related talks  
The Equational Theory of Positive Relation Algebra
MOVE
in Marseille,
March 2017
.

More  
The Equational Theory of Positive Relation Algebra
PACE
in Shanghai,
November 2016
.

More  
A Kleene Theorem for Petri automata
Highlights
in Brussels,
September 2016
.

More  
Une introduction aux algèbres de Kleene
Inter'Actions
in Lyon,
May 2016
(in French)
.

More  
Petri automata for Kleene Allegories
LiCS
in Kyoto,
July 2015
.

More  
Petri automata for Kleene allegories
Rapido
in Paris,
June 2015
.

More  
Petri automata for Kleene allegories
Midlands Graduate School
in Sheffield,
April 2015
.

More  
Décidabilité des Treillis de Kleene sans identité
JFLA
in Val d'Ajol,
January 2015
(in French)
.

More  
Decidability of Identityfree Kleene Lattices
LAC
in Chambéry,
November 2014
.

More  
Kleene Algebra with Converse
RAMiCS
in Marienstatt,
April 2014
.

More  
Deciding Kleene Algebra with converse is PSpacecomplete
GeoCal
in Bordeaux,
March 2014
.

More  
Deciding Kleene Algebra with converse is PSpacecomplete
PACE
in Lyon,
February 2014
.

More  
Algèbres de Relations, Étude des algèbres de Kleene avec converse
Internship defence
in Paris,
September 2013
(Internship defence, in French)
.

More  
Equivalence of regular expressions with converse on relations
PiCoq
in Lyon,
June 2013
.

More  
Related papers  
Petri automata
(in LMCS 2017)
with Damien Pous. 
More  
Algebras of relations: from algorithms to formal proofs (in Université de Lyon 2016)  More  
Cardinalities of finite relations in Coq
(in ITP 2016)
with Insa Stucke and Damien Pous. 
More  
Algorithms for Kleene algebra with converse
(in JLAMP 2016)
with Damien Pous. 
More  
Petri automata for Kleene allegories
(in LICS 2015)
with Damien Pous. 
More  
Decidability of identityfree relational Kleene lattices
(in JFLA 2015)
with Damien Pous. 
More 