We consider infinite graphs that are generated by ground tree (or
term) rewriting systems. The vertices of these graphs are trees. Thus,
with a finite tree automaton one can represent a regular set of
vertices. It is shown that for a regular set T of vertices the set
of vertices from where one can reach (respectively, infinitely often
reach) the set T is again regular. Furthermore it is shown that the
problems, given a tree t and a regular set T, whether all paths
starting in t eventually (respectively, infinitely often) reach T,
are undecidable. We then define a logic which is in some sense a
maximal fragment of temporal logic with a decidable model-checking
problem for the class of ground tree rewriting graphs.
