Outils

Agenda de l'ENS de Lyon

From automata to cyclic proofs: equivalence algorithms and descriptive complexity

Date
ven 23 juil 2021
Horaires

10h30

Lieu(x)

Amphi B

Intervenant(s)

Soutenance de thèse de Mme Laureline PINAULT sous la Direction de M. Damien POUS

Organisateur(s)
Langue(s) des interventions
Description générale

Les modèles de calcul permettent d'abstraire le fonctionnement des programmes afin de raisonner sur ceux-ci. 
Selon le problème étudié il est important de choisir un modèle approprié en terme d'expressivité mais aussi de propriétés. Cette thèse étudie différents modèles de calcul afin de développer des outils pour la conception et l'analyse de programmes. Dans un premier temps nous nous intéressons au problème d'équivalence d'automates, qui a de nombreuses applications notamment dans le domaine de la vérification de programmes. 

Le point de départ est un algorithme coinductif exploitant les techniques up-to développé par Bonchi et Pous pour comparer des automates finis. Nous redonnons cet algorithme dans un cadre légèrement plus général afin de l'étendre aux automates de Büchi. Nous donnons aussi une version linéaire d'une sous-routine de l'algorithme initial et présentons un cadre de test utilisant de l'apprentissage d'automates pour comparer de tels algorithmes d'équivalence.

Dans un deuxième temps nous explorons le contenu calculatoire d'un système de preuves cycliques en le comparant à des modèles de calculs préexistants (automates à plusieurs têtes de lecture et système T de Gödel). Ce système de preuve correspond à un système de type cyclique pour des programmes fonctionnels. Nous montrons que si on se restreint aux fonctions des mots dans les booléens on obtient les langages réguliers pour le système affine et LogSpace en présence de la contraction. Sans cette restriction, le système coïncide avec système T sur les fonctions d'entiers naturels : les fonctions primitives récursives dans le cas affine et les fonctions Peano définissables en présence de la contraction.

Gratuit

Mots clés

Disciplines