On Effective Representations of Well Quasi-Orderings / Simon Halfon ; sous la direction de Philippe Schnoebelen

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : anglais / English

Vérification de modèles (informatique)

Logique informatique

Schnoebelen, Philippe (19..-....) (Directeur de thèse / thesis advisor)

Conchon, Sylvain (1972-....) (Président du jury de soutenance / praeses)

Kuske, Dietrich (1965-...) (Rapporteur de la thèse / thesis reporter)

Habermehl, Peter (Rapporteur de la thèse / thesis reporter)

Džamonja, Mirna (19..-....) (Membre du jury / opponent)

Schmitz, Sylvain (1980-....) (Membre du jury / opponent)

Geeraerts, Gilles (1979-....) (Membre du jury / opponent)

Université Paris-Saclay (2015-2019) (Organisme de soutenance / degree-grantor)

École doctorale Sciences et technologies de l'information et de la communication (Orsay, Essonne ; 2015-....) (Ecole doctorale associée à la thèse / doctoral school)

École normale supérieure Paris-Saclay (Gif-sur-Yvette, Essonne) (Autre partenaire associé à la thèse / thesis associated third party)

Laboratoire Spécification et Vérification (Gif-sur-Yvette, Essonne ; 1997-2020) (Laboratoire associé à la thèse / thesis associated laboratory)

Résumé / Abstract : Avec des motivations venant du domaine de la Vérification, nous définissons une notion de WQO effectifs pour lesquels il est possible de représenter les ensembles clos et de calculer les principales opérations ensemblistes sur ces représentations. Dans une première partie, nous montrons que de nombreuses constructions naturelles sur les WQO préservent notre notion d'effectivité, prouvant ainsi que la plupart des WQOs utilisés en pratique sont effectifs. Cette partie est basée sur un article non publié dont Jean Goubault-Larrecq, Narayan Kumar, Prateek Karandikar et Philippe Schnoebelen sont co-auteurs.Dans une seconde partie, nous étudions les conséquences qu'a notre notion sur la logique du première ordre interprété sur un WQO. Bien que le fragment existentiel positif soit décidable pour tous les WQOs effectif, les perspectives de généralisation sont limitées par le résultat suivant: le fragment existentiel de la logique du première ordre sur les mots finis, ordonnés par plongement, est déjà indécidable. Ce résultat a été publié à LICS 2017 avec Philippe Schnoebelen et Georg Zetzsche.

Résumé / Abstract : With motivations coming from Verification, we define a notionof effective WQO for which it is possible to represent closed subsetsand to compute basic set-operations on these representations. In a firstpart, we show that many of the natural constructions that preserve WQOsalso preserve our notion of effectiveness, proving that a large class ofcommonly used WQOs are effective. This part is based on an unpublishedarticle with Jean Goubault-Larrecq, Narayan Kumar, Prateek Karandikarand Philippe Schnoebelen.In a second part, we investigate the consequences of our notion onfirst-order logics over WQOs. Although the positive existential fragmentis decidable for any effective WQO, the perspective of extension tolarger fragments is hopeless since the existential fragment is alreadyundecidable for the first-order logic over words with the subwordordering. This last result has been published in LICS 2017 with PhilippeSchnoebelen and Georg Zetzsche.