Résumé :

Nous introduisons une définition d'automate cellulaire sur des graphes arbitraires, basée sur une notion de règle locale agnostique, et qui coïncide avec la définition classique sur les graphes de Cayley de groupes finiment engendrés. Nous montrons que, dans ce cadre, la logique du premier ordre sur les orbites d'automates cellulaires est équivalente à la logique monadique du second ordre sur les graphes. Nous en déduisons une caractérisation des groupes sur lesquels le problème de vérification de modèle (model checking) des formules du premier ordre sur les orbites d'automates cellulaires est indécidable. Nous montrons également que des formules du premier ordre très simples dans ce formalisme capturent le problème du domino et ses variantes. Nos résultats sont donc à rapprocher de la conjecture de Ballier-Stein qui affirme que le problème du domino sur les groupes finiment engendrés est décidable si et seulement si le groupe est virtuellement libre. Si le temps le permet nous sortirons du cadre des graphes de Cayley et donnerons des exemples de graphes 4-réguliers où le problème du domino est décidable, mais pas ses variantes.