{"id":{"repo_id":"aachen","oai_identifier":"oai:publications.rwth-aachen.de:62123"},"canonical_url":"https://search.dev.ndltd.org/etd/aachen/oai:publications.rwth-aachen.de:62123","repository":{"repo_id":"aachen","name":"RWTH Aachen University","base_url":"https://publications.rwth-aachen.de/oai2d"},"display":{"title":"Decision problems over infinite graphs : higher order pushdown systems and synchronized products","abstract":"The extension of formal verification methods to infinite models requires classes of graphs which are finitely representable and for which the model checking problem is decidable. We consider three approaches to define classes of finitely representable graphs: internal representations as configuration graphs of higher-order pushdown systems, transformational representations by application of operations which preserve the decidability of the model checking problem, and by composition from components using synchronized products. In the first part of the thesis we show that the hierarchy of higher-order pushdown graphs coincides with the Caucal hierarchy of graphs. We thus obtain transformational representations of higher-order pushdown graphs and can conclude that they enjoy a decidable monadic second-order theory. In the second part of the thesis investigate synchronized products of finitely representable infinite graphs and show that the decidability of an extension of first-order logic with reachability predicates is preserved under the formation of finitely synchronized products. This result is complemented by undecidability results for extensions of the admissible product operations as well as the expressive power of the logic under consideration.","abstract_html":"The extension of formal verification methods to infinite models requires classes of graphs which are finitely representable and for which the model checking problem is decidable. We consider three approaches to define classes of finitely representable graphs: internal representations as configuration graphs of higher-order pushdown systems, transformational representations by application of operations which preserve the decidability of the model checking problem, and by composition from components using synchronized products. In the first part of the thesis we show that the hierarchy of higher-order pushdown graphs coincides with the Caucal hierarchy of graphs. We thus obtain transformational representations of higher-order pushdown graphs and can conclude that they enjoy a decidable monadic second-order theory. In the second part of the thesis investigate synchronized products of finitely representable infinite graphs and show that the decidability of an extension of first-order logic with reachability predicates is preserved under the formation of finitely synchronized products. This result is complemented by undecidability results for extensions of the admissible product operations as well as the expressive power of the logic under consideration.","abstract_has_math":false,"creators":["Wöhrle, Stefan"],"institution":"Publikationsserver der RWTH Aachen University","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Thomas, Wolfgang"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2005,"date_issued":"2005","date_published":"2005","updated_at":"2026-07-30T19:43:19Z","subjects":["info:eu-repo/classification/ddc/510","Unendlicher Graph","Entscheidungsproblem","Mathematik","Model Checking","Infinite Graphs","Higher-order Pushdown Systems"],"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-123716%22"],"render_values":[{"text":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-123716%22","href":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-123716%22","code":true}]}]},"links":{"outbound_url":"https://publications.rwth-aachen.de/record/62123","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Thomas, Wolfgang"]},{"key":"dc:creator","label":"Author","values":["Wöhrle, Stefan"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:coverage","label":"Dc Coverage","values":["DE"]},{"key":"dc:date","label":"Dc Date","values":["2005"]},{"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-11474"]},{"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","Unendlicher Graph","Entscheidungsproblem","Mathematik","Model Checking","Infinite Graphs","Higher-order Pushdown Systems"]}]},{"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/62123","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-123716%22"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["The extension of formal verification methods to infinite models requires classes of graphs which are finitely representable and for which the model checking problem is decidable. We consider three approaches to define classes of finitely representable graphs: internal representations as configuration graphs of higher-order pushdown systems, transformational representations by application of operations which preserve the decidability of the model checking problem, and by composition from components using synchronized products. In the first part of the thesis we show that the hierarchy of higher-order pushdown graphs coincides with the Caucal hierarchy of graphs. We thus obtain transformational representations of higher-order pushdown graphs and can conclude that they enjoy a decidable monadic second-order theory. In the second part of the thesis investigate synchronized products of finitely representable infinite graphs and show that the decidability of an extension of first-order logic with reachability predicates is preserved under the formation of finitely synchronized products. This result is complemented by undecidability results for extensions of the admissible product operations as well as the expressive power of the logic under consideration."]},{"key":"dc:source","label":"Dc Source","values":["Aachen : Publikationsserver der RWTH Aachen University 128 S. : graph. Darst. (2005). = Aachen, Techn. Hochsch., Diss., 2005"]},{"key":"dc:title","label":"Title","values":["Decision problems over infinite graphs : higher order pushdown systems and synchronized products"]}]}],"canonical_facts":{"dc:contributor":["Thomas, Wolfgang"],"dc:coverage":["DE"],"dc:creator":["Wöhrle, Stefan"],"dc:date":["2005"],"dc:description":["The extension of formal verification methods to infinite models requires classes of graphs which are finitely representable and for which the model checking problem is decidable. We consider three approaches to define classes of finitely representable graphs: internal representations as configuration graphs of higher-order pushdown systems, transformational representations by application of operations which preserve the decidability of the model checking problem, and by composition from components using synchronized products. In the first part of the thesis we show that the hierarchy of higher-order pushdown graphs coincides with the Caucal hierarchy of graphs. We thus obtain transformational representations of higher-order pushdown graphs and can conclude that they enjoy a decidable monadic second-order theory. In the second part of the thesis investigate synchronized products of finitely representable infinite graphs and show that the decidability of an extension of first-order logic with reachability predicates is preserved under the formation of finitely synchronized products. This result is complemented by undecidability results for extensions of the admissible product operations as well as the expressive power of the logic under consideration."],"dc:identifier":["https://publications.rwth-aachen.de/record/62123","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-123716%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-11474"],"dc:rights":["info:eu-repo/semantics/openAccess"],"dc:source":["Aachen : Publikationsserver der RWTH Aachen University 128 S. : graph. Darst. (2005). = Aachen, Techn. Hochsch., Diss., 2005"],"dc:subject":["info:eu-repo/classification/ddc/510","Unendlicher Graph","Entscheidungsproblem","Mathematik","Model Checking","Infinite Graphs","Higher-order Pushdown Systems"],"dc:title":["Decision problems over infinite graphs : higher order pushdown systems and synchronized products"],"dc:type":["info:eu-repo/semantics/doctoralThesis","info:eu-repo/semantics/publishedVersion"]},"updated_at":"2026-07-30T19:43:19Z"}