Algebras of relations: from algorithms to formal proofs

My advisor is Damien Pous. I started my PhD in October 2013.

Manuscript :

Last modification: Wednesday September 20th, 2017 (10:10:10).


Tuesday October 4th, 2016 at 2pm.
ENS de Lyon, site Monod, Amphi B (third floor).
  • Carton Olivier, Professeur, Université Paris Diderot (President)
  • Struth Georg, Professeur, University of Sheffield (Examiner)
  • Muscholl Anca, Professeur, Université de Bordeaux (Examiner)
  • Schnoebelen Philippe, Directeur de recherche CNRS, LSV – ENS de Cachan (Examiner)
  • Silva Alexandra, Senior Lecturer, University College London (Examiner)
  • Petrisan Daniela, Docteur, IRIF (Examiner)
  • Malbos Philippe, Maître de Conférences, Université Claude Bernard Lyon (Examiner)
  • Pous Damien, Chargé de recherche CNRS, LIP – ENS de Lyon (PhD advisor)
  • Struth Georg, Professeur, University of Sheffield
  • Kozen Dexter, Professeur, Cornell University
  • Weil Pascal, Directeur de recherche CNRS, LaBRI


Algebras of relations appear naturally in many contexts, in computer science as well as in mathematics. They constitute a framework well suited to the semantics of imperative programs. Kleene algebras are a starting point: these algebras enjoy very strong decidability properties, and a complete axiomatisation. The goal of this thesis was to export known results from Kleene algebra to some of its extensions.

We first considered a known extension: Kleene algebras with converse. Decidability of these algebras was already known, but the algorithm witnessing this result was too complicated to be practical. We proposed a simpler algorithm, which is more efficient, and whose correctness is easier to establish. It allowed us to prove that this problem lies in the complexity class PSpace-complete.

Then we studied Kleene allegories. Few results were known about this extension. Following results about closely related algebras, we established the equivalence between equality in Kleene allegories and the equality of certain sets of graphs. We then developed a new automaton model (so-called Petri automata), based on Petri nets. We proved the equivalence between the original problem and comparing these automata. In the restricted setting of identity-free Kleene lattices, we also provided an algorithm performing this comparison. This algorithm uses exponential space. However, we proved that the problem of comparing Petri automata lies in the class ExpSpace- complete.

Finally, we studied Nominal Kleene algebras. We realised that existing descriptions of these algebra were not suited to relational semantics of programming languages. We thus modified them accordingly, and doing so uncovered several natural variations of this model. We then studied formally the bridges one could build between these variations, and between the existing model and our new version of it. This study was conducted using the proof assistant Coq.