Différences

Ci-dessous, les différences entre deux révisions de la page.

Lien vers cette vue comparative

Prochaine révision 		Révision précédente
fr:research:fssp [2017/03/20 14:24]
apeiron créée 		fr:research:fssp [2021/04/05 17:25]
apeiron effacer FSSP
Ligne 1: Ligne 1:
-[[https://en.wikipedia.org/​wiki/​Firing_squad_synchronization_problem|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 ​>>.
  
-Depuis fin 2015 je fais un postdoc((Financé par l'ANR TARMAC 12 BS02 007 01.)) avec Jean-Baptiste Yunès et Luidnel Maignan à l'​Université Paris-Diderot sur le problème de la synchronisation dans les automates cellulaires. Je veux prouver que leur approche basée sur la modularité et des champs récursifs produit bien le résultat attendu, puis implémenter cette approche en utilisant l'​assistant de preuve Coq.+====== Versions ======
  
-L'intérêt est double pour mon projet de recherche. D'une part, mon travail précédent s'est fait essentiellement sur la complexité ​en temps et la taille des éléments, alors que nous examinons aujourd'​hui ​les problèmes de voisinage et de transmission de l'​information dans l'​espace. D'​autre part, il s'est avéré que mon style de preuve <<​~mécanique~>>​ est idéal pour travailler avec un assistant de preuve, qui répond ​à mon intérêt ​pour la constructivité et notamment la relation ​preuve/programme, ainsi qu'à mon intérêt pour la quête ​des fondements cette fois vue dans un cadre computationnel ​et plus seulement logique.+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]].
  
-Le rapport technique ​est encore en rédaction, voici {{ :fr:research:​rapport11.pdf |la version actuelle}}+====== 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 [[http://​dl.acm.org/​citation.cfm?​id=2570381|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 [[http://web.a.ebscohost.com/​abstract?​direct=true&​profile=ehost&​scope=site&​authtype=crawler&​jrnl=15575969&​AN=117653073&​h=q0DsSB07qQtTr4ExSbZ4utEFNt8pqrv1Ls9objyAD1h3DtaCaiZGkx%2bFy27SIic6ojlW71wBvftuB1UaubpLzA%3d%3d&​crl=c&​resultNs=AdminWebAuth&​resultLocal=ErrCrlNotAuth&​crlhashurl=login.aspx%3fdirect%3dtrue%26profile%3dehost%26scope%3dsite%26authtype%3dcrawler%26jrnl%3d15575969%26AN%3d117653073|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.