We introduce an extension of classical cellular automata (CA) to arbitrary labeled graphs, and show that FO logic on CA orbits is equivalent to MSO logic. We deduce various results from that equivalence, including a characterization of finitely generated groups on which FO model checking for CA orbits is undecidable, and undecidability of satisfiability of a fixed FO property for CA over finite graphs. We also show concrete examples of FO formulas for CA orbits whose model checking problem is equivalent to the domino problem, or its seeded or recurring variants respectively, on any finitely generated group. For the recurring domino problem, we use an extension of the FO signature by a relation found in the well-known Garden of Eden theorem, but we also show a concrete FO formula without the extension and with one quantifier alternation whose model checking problem does not belong to the arithmetical hierarchy on group Z^2.

翻译：我们将经典细胞自动机(CA)推广至任意标记图，并证明CA轨道上的一阶逻辑等价于二阶逻辑。由此等价性推断出多项结论，包括：在有限生成群上CA轨道的FO模型检验不可判定的刻画条件，以及有限图上固定FO性质的CA可满足性不可判定性。我们还展示了CA轨道FO公式的具体实例，其在任意有限生成群上的模型检验问题分别等价于多米诺骨牌问题及其带种子或循环变体。针对循环多米诺骨牌问题，我们通过加入著名"伊甸园定理"中的关系扩展了FO签名，但同时给出了一个不含此扩展且仅含一次量词交替的具体FO公式，其在群Z^2上的模型检验问题不属于算术层级。