Infinite graphs generated by tree rewriting
type: CreativeWork
description: 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.
abstract: 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.
author: Löding, Christof
language: eng
keywords: info:eu-repo/classification/ddc/510, Mathematik, unendliche Graphen, Termersetzung, Model Checking
date published: 2003
date modified: 2026-07-30T19:42:31Z
provider: RWTH Aachen University
publisher: Networked Digital Library of Theses and Dissertations
type: WebPage
source organization: Publikationsserver der RWTH Aachen University