Model-Checking Infinite Systems Generated by Ground Tree Rewriting

Christof Löding

To appear at Foundations of Software Science and Computation Structures (FOSSACS02), Grenoble, France, 6-14 April, 2002


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.

Server START Conference Manager
Update Time 14 Dec 2001 at 14:02:38
Start Conference Manager
Conference Systems