Local First Order Logic with Data: Toward Specification of Distributed Algorithms
Jeudi, 14 décembre 2023, 14h00
Université Paris CIté, Bâtiment Sophie Germain, salle 3052
Résumé :
Ce manuscrit s'inscrit dans le domaine de la vérification formelle, une discipline informatique visant à garantir l'absence d'erreurs dans les programmes. Dans ce contexte, la spécification en est une facette, et consiste à énoncer formellement les propriétés que le programme doit satisfaire. Notre focus se porte sur les algorithmes distribués, qui sont particulièrement difficile à conceptualiser. Pour aborder cette problématique, nous explorons les logiques avec données, adaptées à cet usage. Dans notre cadre, une donnée est un élément d'un ensemble dénombrable, les éléments des structures ont une ou plusieurs données et la logique peut seulement tester si deux données sont égales ou non. La manière dont nous analysons les logiques est au travers du problème de la satisfaisabilité. Cette étude débute par un état de l'art des résultats concernant différentes logiques sur diverses structures telle que les mots, les multi-ensembles, les mots avec données, les multi-ensembles avec données et les graphes. Nous comblons quelques lacunes identifiées dans la littérature, notamment des preuves manquantes et des cas non étudiés. Nous exposons également deux outils classiques pour aider à l'analyse du problème de la satisfaisabilité, à savoir les jeux d'Ehrenfeucht-Fraïssé et les problèmes de dominos. Ensuite, commence l'apport principale de ce travail qui réside dans la définition et l'étude d'une nouvelle logique avec données, que nous appelons le fragment local, introduisant à cet effet la modalité locale. Inspirée par la notion de localité et de graphe de Gaifman, notre approche se distingue par l'intégration de la localité dans la définition de notre logique, au niveau de la syntaxe. Nous définissons également un sous-fragment appelé le fragment existentiel. Nous démontrons que notre logique constitue effectivement un fragment de la logique du premier ordre, en cela que la modalité local peut s'exprimer dans la logique du premier ordre. Par la suite, nous analysons notre nouvelle logique sous l'angle du problème de la satisfaisabilité. Nous identifions des critères pour lesquels la logique est décidable et d'autres pour lesquels elle ne l'est pas. De plus, dans les cas où la logique est décidable, nous nous efforçons d'analyser la complexité du problème de la satisfaisabilité.
Membres du jury :
- Nathalie BERTRAND, Rapportrice
- Radu IOSIF, Rapporteur
- Nathalie SZNAJDER, Examinatrice
- Thomas ZEUME, Examinateur
- Arnaud SANGNIER, Directeur de thèse
- Benedikt BOLLIG, Co-encadrant de thèse