Nicolas Ollinger (LIFO, Univ. Orléans)

Ces travaux réalisés avec O. Carton, JM. Couvreur et M. Delacourt sont motivés par une question issue de l’étude des pavages hiérarchiques du plan par des jeux de tuiles minimaux. Quand est-il possible d’automatiser la démonstration de propriétés sur les motifs apparaissant dans ces pavages en utilisant des outils de vérification de propriétés énoncées au premier ordre, comme Walnut (https://cs.uwaterloo.ca/~shallit/walnut.html) ?

Pour répondre à cette question, nous sommes amenés à considérer le problème de calculer la relation d’addition par un automate fini dans des systèmes de numération abstraits. Nous introduisons les automates de suites, un outil très pratique pour ce type de considérations. Nous montrons que dans le cas Pisot, les résultats de Bruyère/Hansel et Frougny / Solomyak permettent de construire explicitement l’automate de l’addition. On termine l’exposé les mains dans le cambouis avec des bibliothèque Python interfacées avec Walnut.