Automatic graphs and D0L-sequences of finite graphs

AbstractThe notion of end is a classical mean to understand the behavior of a graph at infinity. In this respect, we show that the problem of deciding whether an infinite automatic graph has more than one end is recursively undecidable. The proof involves the analysis of some global topological properties of the configuration graph of a self-stabilizing Turing machine. This result is applied to the graph transformation system theory: It allows us to set a picture of decidability issues concerning logic of D0L-languages of finite graphs. We first show that the first-order theory of a D0L-sequence of finite graphs is decidable. Secondly, we show that the first-order theory, when it is upgraded with a closure operator, becomes undecidable for D0L-sequences of finite graphs