Decision problems over infinite graphs : higher order pushdown systems and synchronized products

Wöhrle, Stefan; Thomas, Wolfgang

doi:urn:nbn:de:hbz:82-opus-11474

Decision problems over infinite graphs : higher order pushdown systems and synchronized products

Wöhrle, Stefan (Author)

2005

Verantwortlichkeitsangabevorgelegt von Stefan Wöhrle

ImpressumAachen : Publikationsserver der RWTH Aachen University 2005

Umfang128 S. : graph. Darst.

Aachen, Techn. Hochsch., Diss., 2005

Zusammenfassung in dt. und engl. Sprache

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Thomas, Wolfgang (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2005-06-30

Online
URN: urn:nbn:de:hbz:82-opus-11474
URL: https://publications.rwth-aachen.de/record/62123/files/Woehrle_Stefan.pdf

Einrichtungen

Fakultät für Mathematik, Informatik und Naturwissenschaften (100000)

Inhaltliche Beschreibung (Schlagwörter)
Unendlicher Graph (Genormte SW) ; Entscheidungsproblem (Genormte SW) ; Mathematik (frei) ; Model Checking (frei) ; Infinite Graphs (frei) ; Higher-order Pushdown Systems (frei)

Thematische Einordnung (Klassifikation)
DDC: 510

Kurzfassung
Die Erweiterung formaler Verifikationsmethoden auf unendliche Systeme erfordert die Untersuchung von endlich darstellbaren Graphklassen, für die das Model Checking Problem entscheidbar ist. Wir betrachten drei Zugänge, um solche Graphklassen zu definieren: interne Darstellungen als Konfigurationsgraphen von Kellerautomaten höherer Ordnung, Darstellungen durch Transformationen, die die Entscheidbarkeit der monadischen Theorie erhalten, und die Komposition von Komponenten mittels synchronisierter Produkte. Im ersten Teil der Dissertation zeigen wir, dass die Hierarchie von Graphen, die durch Kellerautomaten höherer Ordnung erzeugt werden, mit der mittels Transformationen defininierten Caucal Hierarchie übereinstimmt. Wir können somit schließen, dass die monadische Theorie dieser Graphen entscheidbar ist. Im zweiten Teil der Arbeit untersuchen wir synchronisierte Produkte endlich darstellbarer Graphen im Bezug auf das Model Checking Problem. Wir betrachten unter anderem die Logik der ersten Stufe erweitert um Erreichbarkeitsprädikate und zeigen, dass nur die Bildung endlich synchronisierter Produkte die Entscheidbarkeit dieser Logik erhält. Dieses Ergebnis wird durch Unentscheidbarkeitsresultate für Varianten der zulässigen Produktoperationen und der betrachteten Logiken ergänzt.

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.

Fulltext:
PDF
(additional files)