Kartzow, Alexander (2011)
First-Order Model Checking on Generalisations of Pushdown Graphs.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung
Kurzbeschreibung (Abstract)
We study the first-order model checking problem on two generalisations of pushdown graphs. The first class is the class of nested pushdown trees. The other is the class of collapsible pushdown graphs. Our main results are the following. First-order logic with reachability is uniformly decidable on nested pushdown trees. Considering first-order logic without reachability, we prove decidability in doubly exponential alternating time with linearly many alternations. First-order logic with regular reachability predicates is uniformly decidable on level 2 collapsible pushdown graphs. Moreover, nested pushdown trees are first-order interpretable in collapsible pushdown graphs of level 2. This interpretation can be extended to an interpretation of the class of higher-order nested pushdown trees in the collapsible pushdown graph hierarchy. We prove that the second level of this new hierarchy of nested trees has decidable first-order model checking. Our decidability result for collapsible pushdown graph relies on the fact that level 2 collapsible pushdown graphs are uniform tree-automatic. Our last result concerns tree-automatic structures in general. We prove that first-order logic extended by Ramsey quantifiers is decidable on all tree-automatic structures.
| Typ des Eintrags: |
Dissertation
|
| Erschienen: |
2011 |
| Autor(en): |
Kartzow, Alexander |
| Art des Eintrags: |
Erstveröffentlichung |
| Titel: |
First-Order Model Checking on Generalisations of Pushdown Graphs |
| Sprache: |
Englisch |
| Referenten: |
Otto, Prof. Dr. Martin ; Damian, Prof. Niwinski ; Stephan, Prof. Dr. Kreutzer |
| Publikationsjahr: |
18 Juli 2011 |
|
Datum der mündlichen Prüfung: |
2011 |
| URL / URN: |
urn:nbn:de:tuda-tuprints-26815 |
| Kurzbeschreibung (Abstract): |
We study the first-order model checking problem on two generalisations of pushdown graphs. The first class is the class of nested pushdown trees. The other is the class of collapsible pushdown graphs. Our main results are the following. First-order logic with reachability is uniformly decidable on nested pushdown trees. Considering first-order logic without reachability, we prove decidability in doubly exponential alternating time with linearly many alternations. First-order logic with regular reachability predicates is uniformly decidable on level 2 collapsible pushdown graphs. Moreover, nested pushdown trees are first-order interpretable in collapsible pushdown graphs of level 2. This interpretation can be extended to an interpretation of the class of higher-order nested pushdown trees in the collapsible pushdown graph hierarchy. We prove that the second level of this new hierarchy of nested trees has decidable first-order model checking. Our decidability result for collapsible pushdown graph relies on the fact that level 2 collapsible pushdown graphs are uniform tree-automatic. Our last result concerns tree-automatic structures in general. We prove that first-order logic extended by Ramsey quantifiers is decidable on all tree-automatic structures. |
|
Alternatives oder übersetztes Abstract: |
|
Alternatives Abstract | Sprache |
|---|
Diese Arbeit behandelt das Model-Checking-Problem für die Logik erster Stufe (FO) auf zwei verallgemeinerungen von Kellerautomaten: einerseits auf Nested-Pushdown-Trees und andererseits auf Level 2 Collapsible-Pushdown-Graphen. Unserer Hauptresultate sind, dass FO erweitert um das die Erreichbarkeitsrelation Reach auf beiden Klassen entscheidbar ist. Betrachten wir nur FO auf Nested-Pushdown-Trees ist das Model-Checking-Problem sogar in doppelt exponentiell alterierender Zeit mit linear vielen Alternationen lösbar. Auf Level 2 Collapsible-Pushdown-Graphen ist sogar FO erweiterte um reguläre Erreichbarkeit entscheidbar. Dies zeigen wir, indem wir eine uniforme Repräsentation durch Baumautomaten nachweisen. Schliesslich untersuchen wir allgemein Strukturen mit baumautomatischer Repräsentation. Wir zeigen, dass FO erweitert um Ramsey-Quantoren auf baumautomatisch repräsentierten Strukturen entscheidbar ist. | Deutsch |
|
| Schlagworte: |
| Einzelne Schlagworte | Sprache |
|---|
| first-order logic, reachability, collapsible pushdown graphs, nested pushdown trees, decidability, model checking | Englisch |
|
| Sachgruppe der Dewey Dezimalklassifikatin (DDC): |
000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
500 Naturwissenschaften und Mathematik > 510 Mathematik |
| Fachbereich(e)/-gebiet(e): |
04 Fachbereich Mathematik
04 Fachbereich Mathematik > Logik |
| Hinterlegungsdatum: |
05 Sep 2011 09:07 |
| Letzte Änderung: |
05 Mär 2013 09:54 |
| PPN: |
|
| Referenten: |
Otto, Prof. Dr. Martin ; Damian, Prof. Niwinski ; Stephan, Prof. Dr. Kreutzer |
|
Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: |
2011 |
| Schlagworte: |
| Einzelne Schlagworte | Sprache |
|---|
| first-order logic, reachability, collapsible pushdown graphs, nested pushdown trees, decidability, model checking | Englisch |
|
| Export: |
|
| Suche nach Titel in: |
TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum