  In a recent paper Sutner proved that the first-order theory of the
phase-space $\mathcal{S}_\mathcal{A}=(Q^\mathbb{Z}, \longrightarrow)$ of a
one-dimensional cellular automaton $\mathcal{A}$ whose configurations are
elements of $Q^\mathbb{Z}$, for a finite set of states $Q$, and where
$\longrightarrow$ is the "next configuration relation", is decidable. He asked
whether this result could be extended to a more expressive logic. We prove in
this paper that this is actuallly the case. We first show that, for each
one-dimensional cellular automaton $\mathcal{A}$, the phase-space
$\mathcal{S}_\mathcal{A}$ is an omega-automatic structure. Then, applying
recent results of Kuske and Lohrey on omega-automatic structures, it follows
that the first-order theory, extended with some counting and cardinality
quantifiers, of the structure $\mathcal{S}_\mathcal{A}$, is decidable. We give
some examples of new decidable properties for one-dimensional cellular
automata. In the case of surjective cellular automata, some more efficient
algorithms can be deduced from results of Kuske and Lohrey on structures of
bounded degree. On the other hand we show that the case of cellular automata
give new results on automatic graphs.
