{"id":{"repo_id":"aachen","oai_identifier":"oai:publications.rwth-aachen.de:58868"},"canonical_url":"https://search.dev.ndltd.org/etd/aachen/oai:publications.rwth-aachen.de:58868","repository":{"repo_id":"aachen","name":"RWTH Aachen University","base_url":"https://publications.rwth-aachen.de/oai2d"},"display":{"title":"Infinite graphs generated by tree rewriting","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.","abstract_html":"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_has_math":false,"creators":["Löding, Christof"],"institution":"Publikationsserver der RWTH Aachen University","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Thomas, Wolfgang","Grädel, Erich"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2003,"date_issued":"2003","date_published":"2003","updated_at":"2026-07-30T19:42:31Z","subjects":["info:eu-repo/classification/ddc/510","Mathematik","unendliche Graphen","Termersetzung","Model Checking"],"languages":["eng"],"rights":["info:eu-repo/semantics/openAccess"],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-120696%22"],"render_values":[{"text":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-120696%22","href":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-120696%22","code":true}]}]},"links":{"outbound_url":"https://publications.rwth-aachen.de/record/58868","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Thomas, Wolfgang","Grädel, Erich"]},{"key":"dc:creator","label":"Author","values":["Löding, Christof"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:coverage","label":"Dc Coverage","values":["DE"]},{"key":"dc:date","label":"Dc Date","values":["2003"]},{"key":"dc:publisher","label":"Institution","values":["Publikationsserver der RWTH Aachen University"]},{"key":"dc:relation","label":"Dc Relation","values":["info:eu-repo/semantics/altIdentifier/urn/urn:nbn:de:hbz:82-opus-5547"]},{"key":"dc:type","label":"Dc Type","values":["info:eu-repo/semantics/doctoralThesis","info:eu-repo/semantics/publishedVersion"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["info:eu-repo/classification/ddc/510","Mathematik","unendliche Graphen","Termersetzung","Model Checking"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["info:eu-repo/semantics/openAccess"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://publications.rwth-aachen.de/record/58868","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-120696%22"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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."]},{"key":"dc:source","label":"Dc Source","values":["Aachen : Publikationsserver der RWTH Aachen University VI, 157 S. : graph. Darst. (2003). = Aachen, Techn. Hochsch., Diss., 2002"]},{"key":"dc:title","label":"Title","values":["Infinite graphs generated by tree rewriting"]}]}],"canonical_facts":{"dc:contributor":["Thomas, Wolfgang","Grädel, Erich"],"dc:coverage":["DE"],"dc:creator":["Löding, Christof"],"dc:date":["2003"],"dc: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."],"dc:identifier":["https://publications.rwth-aachen.de/record/58868","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-120696%22"],"dc:language":["eng"],"dc:publisher":["Publikationsserver der RWTH Aachen University"],"dc:relation":["info:eu-repo/semantics/altIdentifier/urn/urn:nbn:de:hbz:82-opus-5547"],"dc:rights":["info:eu-repo/semantics/openAccess"],"dc:source":["Aachen : Publikationsserver der RWTH Aachen University VI, 157 S. : graph. Darst. (2003). = Aachen, Techn. Hochsch., Diss., 2002"],"dc:subject":["info:eu-repo/classification/ddc/510","Mathematik","unendliche Graphen","Termersetzung","Model Checking"],"dc:title":["Infinite graphs generated by tree rewriting"],"dc:type":["info:eu-repo/semantics/doctoralThesis","info:eu-repo/semantics/publishedVersion"]},"updated_at":"2026-07-30T19:42:31Z"}