Reachability Problems on Regular Ground Tree Rewriting Graphs

We consider the transition graphs of regular ground tree (or term) rewriting systems. The vertex set of such a graph is a (possibly infinite) set of trees. Thus, with a finite tree automaton one can represent a regular set of vertices. It is known that the backward closure of sets of vertices under the rewriting relation preserves regularity, i.e., for a regular set T of vertices the set of vertices from which one can reach T can be accepted by a tree automaton. The main contribution of this paper is to lift this result to the recurrence problem, i.e., we show that the set of vertices from which one can reach infinitely often a regular set T is regular, too. Since this result is effective, it implies that the problem whether, given a tree t and a regular set T, there is a path starting in t that infinitely often reaches T, is decidable. Furthermore, it is shown that the problems whether all paths starting in t eventually (respectively, infinitely often) reach T, are undecidable. Based on the decidability result we define a fragment of temporal logic with a decidable model-checking problem for the class of regular ground tree rewriting graphs.