Différences
Ci-dessous, les différences entre deux révisions de la page.
| Les deux révisions précédentes Révision précédente Prochaine révision | Révision précédente | ||
|
fr:research:fssp [2017/03/23 13:46] apeiron |
fr:research:fssp [2021/04/05 17:25] apeiron effacer FSSP |
||
|---|---|---|---|
| Ligne 1: | Ligne 1: | ||
| - | Mon stage postdoctoral((Financé par l'ANR TARMAC 12 BS02 007 01.)) a commencé fin 2015. J'ai travaillé avec Jean-Baptiste Yunès et Luidnel Maignan à l'Université Paris-Diderot sur le problème de la synchronisation dans les automates cellulaires, le << Firing Squad Synchronization Problem >>. | + | Ce travail est issu de mon stage postdoctoral((Financé par l'ANR TARMAC 12 BS02 007 01.)) de fin 2015 à fin 2016. J'ai travaillé avec Jean-Baptiste Yunès et Luidnel Maignan au [[http://archives.liafa.univ-paris-diderot.fr|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é {{ :fr:research:fssp-coq-13.rar |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 [[https://hal.archives-ouvertes.fr/hal-01739317|HAL]]. | ||
| ====== Contexte du problème ====== | ====== Contexte du problème ====== | ||
| Ligne 10: | Ligne 14: | ||
| 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$. | 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$. | ||
| - | |||
| - | 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, voici {{ :fr:research:rapport11.pdf |la version actuelle}}. | ||
| 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. | 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. | ||
| Ligne 17: | Ligne 19: | ||
| 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. | 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 : | + | 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. |
| - | $$\forall \ell t c, \text{Out}^\ell_t(c) \Rightarrow \forall c', \text{Out}^\ell_t(c')$$ | + | |