Ce travail est issu de mon stage postdoctoral1) de fin 2015 à fin 2016. J'ai travaillé avec Jean-Baptiste Yunès et Luidnel Maignan au LIAFA sur le problème de la synchronisation dans les automates cellulaires, le « Firing Squad Synchronization Problem ».

Versions

Pour l'instant nous n'avons implémenté en Coq que les résultats préliminaires, qui nous ont servi à déterminer à quel point les preuves devaient être détaillées pour être ensuite implémentées le plus facilement possible. La preuve de la correction des champs infinis est quasiment terminée et est disponible sur HAL.

Contexte du problème

Le but est de concevoir un automate cellulaire (où chaque cellule ne peut communiquer qu'avec ses voisins) démarrant avec quelques cellules actives (les généraux) tel qu'au bout d'un moment toutes les cellules passent dans le même état simultanément (le peloton d'exécution fait feu). Beaucoup de solutions particulières ont été conçues selon le nombre et le placement des généraux, ou la notion de voisinage utilisée, mais pas de solution suffisamment générale. L'approche de Jean-Baptiste Yunès et Luidnel Maignan consiste à décomposer le problème en champs infinis modulables pouvant être adaptés à différentes variations du problème et composés ensuite pour le résoudre. Ces champs infinis peuvent ensuite être réduits en un nombre fini d'états permettant de définir l'automate cellulaire associé.

Mon objectif était de prouver que cette approche très algorithmique du problème produit bien le résultat attendu, et ce en utilisant l'assistant de preuve Coq. L'intérêt pour mon projet de recherche était double. D'une part, mon travail de thèse a essentiellement consisté à étudier la complexité en temps ainsi que la taille des éléments, approche qui a été complétée durant mon postdoc par l'étude des problèmes de voisinage et de transmission de l'information dans l'espace. D'autre part, mon style de preuve « mécanique » et mon intérêt pour la constructivité (en particulier la relation preuve/programme) étaient adaptés à une implémentation en Coq.

Esquisse de la preuve

L'espace est simplifié pour la preuve : une cellule $c$ est un nombre entre $1$ et $n$. Les champs sont définis récursivement sur le temps $t$. Ainsi le champ Input, indiquant qu'une cellule est réveillée, est donné à $t=0$ par une fonction indiquant quels sont les généraux, puis se propage de proche en proche. Les autres champs (Border, Inside, Stable et Middle) sont de plus définis récursivement par couche, une couche au niveau $\ell$ servant à définir la couche suivante $\ell+1$.

Tout d'abord nous avons prouvé la monotonie des champs, c'est à dire que le champ de distance ne peut qu'augmenter jusqu'à être stable, et pour les autres que quand un champ devient vrai il le reste. Puis nous avons caractérisé le moment où une région délimitée par deux bords $b_1$ et $b_2$ produit le cône de lumière permettant de faire apparaître le milieu de cette région.

Comme le milieu d'une région à une couche $\ell$ devient un bord à la couche $\ell+1$, chaque région se divise en deux jusqu'à ce que toutes les cellules deviennent des bords. Cela définit notre champ Output.

Enfin, nous montrons que les milieux apparaissent en même temps pour chaque couche, ce qui nous permet de conclure qu'il existe une date à laquelle toutes les cellules émettent leur signal de sortie, et pas avant.

1) Financé par l'ANR TARMAC 12 BS02 007 01.