Finite graphs and algorithms on finite graphs are an important tool for the verification of finite-state systems. To transfer the methods for finite systems, at least partially, to infinite systems a theory of infinite graphs with finite representations is needed. In this thesis the class of the transition graphs of ground tree rewriting systems is studied. To investigate the structure of ground tree rewriting graphs they are analyzed under the aspect of tree-width of graphs and are compared to already well-studied classes of graphs, as the class of pushdown graphs and the class of automatic graphs. Furthermore, the trace languages that are definable by ground tree rewriting graphs are investigated. The algorithmic properties of ground tree rewriting graphs are studied by means of reachability problems that correspond to the semantics of basic temporal operators. The decidability results from this analysis are used to build up a temporal logic such that the model-checking problem for this logic and ground tree rewriting graphs is decidable.
展开▼
