Thèse

Algèbres de relations : des algorithmes aux preuves formelles

Mon directeur de thèse est Damien Pous. J'ai commencé mon doctorat en octobre 2013.

Manuscrit :

[Télécharger]
Dernière modification: mardi 10 octobre 2017 (09:44:31).

Soutenance

Mardi 4 octobre 2016 à 14h.
ENS de Lyon, site Monod, Amphi B (troisième étage).
  • Carton Olivier, Professeur, Université Paris Diderot (Président)
  • Struth Georg, Professeur, University of Sheffield (Examinateur)
  • Muscholl Anca, Professeur, Université de Bordeaux (Examinatrice)
  • Schnoebelen Philippe, Directeur de recherche CNRS, LSV – ENS de Cachan (Examinateur)
  • Silva Alexandra, Senior Lecturer, University College London (Examinatrice)
  • Petrisan Daniela, Docteur, IRIF (Examinatrice)
  • Malbos Philippe, Maître de Conférences, Université Claude Bernard Lyon (Examinateur)
  • Pous Damien, Chargé de recherche CNRS, LIP – ENS de Lyon (Directeur de thèse)
  • Struth Georg, Professeur, University of Sheffield
  • Kozen Dexter, Professeur, Cornell University
  • Weil Pascal, Directeur de recherche CNRS, LaBRI

Résumé

Les algèbres de relations apparaissent naturellement dans de nombreux cadres, en informatique comme en mathématiques. Elles constituent en particulier un formalisme tout à fait adapté à la sémantique des programmes impératifs. Les algèbres de Kleene constituent un point de départ : ces algèbres jouissent de résultats de décidabilité très satisfaisants, et admettent une axiomatisation complète. L'objectif de cette thèse a été d'étendre les résultats connus sur les algèbres de Kleene à des extensions de celles-ci.

Nous nous sommes tout d'abord intéressés à une extension connue : les algèbres de Kleene avec converse. La décidabilité de ces algèbres était déjà connue, mais l'algorithme prouvant ce résultat était trop compliqué pour être utilisé en pratique. Nous avons donné un algorithme plus simple, plus efficace, et dont la correction est plus facile à établir. Ceci nous a permis de placer ce problème dans la classe de complexité PSpace-complete.

Nous avons ensuite étudié les allégories de Kleene. Sur cette extension, peu de résultats étaient connus. En suivant des résultats sur des algèbres proches, nous avons établi l'équivalence du problème d'égalité dans les allégories de Kleene à l'égalité de certains ensembles de graphes. Nous avons ensuite développé un modèle d'automate original (les automates de Petri), basé sur les réseaux de Petri, et avons établi l'équivalence de notre problème original avec le problème de comparaison de ces automates. Nous avons enfin développé un algorithme pour effectuer cette comparaison dans le cadre restreint des treillis de Kleene sans identité. Cet algorithme utilise un espace exponentiel. Néanmoins, nous avons pu établir que la comparaison d'automates de Petri dans ce cas est ExpSpace-complète.

Enfin, nous nous sommes intéressés aux algèbres de Kleene Nominales. Nous avons réalisé que les descriptions existantes de ces algèbres n'étaient pas adaptées à la sémantique relationnelle des programmes. Nous les avons donc modifiées pour nos besoins, et ce faisant avons trouvé diverses variations naturelles de ce modèle. Nous avons donc étudié en détail et en Coq les ponts que l'on peut établir entre ces variantes, et entre le modèle "classique" et notre nouvelle version.