diaporama

Cet exposé présentera des résultats récents obtenus dans la communauté sur les liens entre automates quantitatifs et logiques quantitatives. L'histoire a commencé il y a 10 ans avec l'introduction d'une sémantique quantitative pour la logique MSO sur les mots et un théorème d'équivalence entre des automates quantitatifs et une logique MSO quantitative restreinte. Depuis lors, de nombreuses extensions ont été étudiées : des mots aux arbres, mots infinis, images, etc ; des semi-anneaux à des structures pondérés plus générales. De plus, les techniques de preuve ont évolué, partant de bas niveau, imitant minutieusement les preuves classiques dans le domaine booléen, à un plus haut niveau, utilisant différentes sémantiques plus abstraites. J'illustrerai cette évolution en introduisant une logique quantitative de base (core weighted logic) et sa sémantique abstraite en terme de multi-ensembles de structures de poids. Je présenterai également une direction orthogonale de recherche, qui se propose d'étudier la logique quantitative du premier ordre et les automates quantitatifs à jetons qui lui sont associés. Je démontrerai aussi la versatilité de l'approche par automates quantitatifs en les spécialisant dans le domaine des transducteurs, montrant une direction possible vers la conception d'une logique alternative pour les transductions (relations entre mots finis).