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/04/05 17:07] 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 ====== | ====== Versions ====== | ||
| - | Pour l'instant nous n'avons implémenté {{ :fr:research:fssp-coq12.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, voici la dernière version du {{ :fr:research:fssp-report12.pdf |rapport technique}}. | + | 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 19: | 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')$$ | + | |