Décidabilité pour les mots sturmiens

Abstract

Dans ce travail, nous montrons que la théorie du premier ordre de la collection d'extensions de l'arithmétique de Presburger par un mot sturmien interprété comme une fonction unaire est décidable. Pour cela, nous établissons un lien entre décidabilité et ω-régularité. Un élément clef de ce travail est la construction d'un automate de Büchi qui permet de réaliser des additions de codages binaires de représentations d'Ostrowski. C'est pourquoi, nous nous intéressons également aux systèmes de numération d'Ostrowski ainsi qu'aux fractions continues qui permettent de définir ces systèmes. Ensuite, nous présentons le logiciel Pecan, une implémentation de cet algorithme de décision, qui utilise des automates de Büchi afin de représenter des prédicats logiques.