Infinite graphs generated by tree rewriting [Elektronische Ressource] / vorgelegt von Christof Löding

Christof Loeding

Sujets

• Mathematics
• Informatik

Informations

• Publié par: rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen
• Publié le: 01 janvier 2002
• Nombre de lectures: 16
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

INFINITE GRAPHS GENERATED BY
TREE REWRITING
Von der Fakultat fur Mathematik, Informatik und˜ ˜
Naturwissenschaften der Rheinisch-Westf˜alischen Technischen
Hochschule Aachen zur Erlangung des akademischen Grades eines
Doktors der Naturwissenschaften genehmigte Dissertation
vorgelegt von
Diplom-Informatiker
Christof Loding˜
aus Neumunster,˜ Schleswig-Holstein
Berichter: Universitatsprofessor Dr. Wolfgang Thomas˜
Universit Dr. Erich Gradel˜ ˜
Tag der mundlichen Prufung: 19. Dezember 2002˜ ˜
Diese Dissertation ist auf den Internetseiten der Hochschulbibliothek
online verfugbar.˜.Abstract
Finite graphs and algorithms on flnite graphs are an important tool for
the veriflcation of flnite-state systems. To transfer the methods for flnite
systems, at least partially, to inflnite systems a theory of inflnite graphs
with flnite representations is needed. In this thesis the class of the transi-
tion 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 deflnable 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.
Zusammenfassung
Endliche Graphen und Graphalgorithmen haben vielfaltige Anwendun-˜
gen in der Informatik, unter anderem in der Veriflkation endlicher, zustands-
basierter Systeme. Um die Methoden und Ergebnisse fur endliche Systeme˜
zumindest teilweise auf unendliche Systeme zu ubertragen, wird eine Theo-˜
rie unendlicher Graphen mit endlicher Darstellung ben˜otigt. In dieser Arbeit
wird die Klasse der Transitionsgraphen von Grundtermersetzungssystemen
behandelt. Um die Struktur von Grundtermersetzungsgraphen zu analysie-
ren, werden diese unter dem Aspekt der Baumweite von Graphen untersucht
und mit bereits intensiv studierten Graphklassen wie der Klasse der Push-
downgraphen und der Klasse der automatischen Graphen verglichen. Wei-
terhin werden die durch deflnierbaren Pfad-
sprachen studiert.
DiealgorithmischenEigenschaftenvonGrundtermersetzungsgraphenwer-
den anhand von Erreichbarkeitsproblemen, die der Semantik grundlegender
temporaler Operatoren entsprechen, untersucht. Die Entscheidbarkeitser-
gebnisse aus dieser Analyse werden benutzt, um eine temporale Logik aufzu-
bauen, fur˜ die das Model-Checking-Problem mit Grundtermersetzungsgra-
phen entscheidbar ist..Contents
1 Introduction 1
2 Tree Rewriting Graphs 11
2.1 Graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2 Ranked Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.3 Ground Tree Rewriting . . . . . . . . . . . . . . . . . . . . . 15
2.4 Tree Automata . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.5 Regular Ground Tree Rewriting . . . . . . . . . . . . . . . . . 24
3 The Structure of GTR Graphs 29
3.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.1.1 Pushdown Automata . . . . . . . . . . . . . . . . . . . 31
3.1.2 Factorizations of Trees . . . . . . . . . . . . . . . . . . 33
3.2 GTR Graphs of Bounded Width . . . . . . . . . . . . . . . . 36
3.2.1 Tree-Width . . . . . . . . . . . . . . . . . . . . . . . . 37
3.2.2 Inflx Pushdown Automata . . . . . . . . . . . . . . . . 41
3.2.3 From GTRS to Inflx Pushdown Automata . . . . . . . 44
3.2.4 From Inflx Pushdown Graphs to Pushdown Graphs . . 48
3.2.5 Clique-Width . . . . . . . . . . . . . . . . . . . . . . . 55
3.2.6 Characterization of GTR Graphs of Bounded Width . 62
3.3 Comparison to Other Classes of . . . . . . . . . . . . 62
3.3.1 Preflx Recognizable and Equational Graphs . . . . . . 63
3.3.2 Automatic Graphs . . . . . . . . . . . . . . . . . . . . 65
3.4 Traces of GTR Graphs . . . . . . . . . . . . . . . . . . . . . . 72
3.4.1 Classiflcation in the Chomsky Hierarchy . . . . . . . . 74
3.4.2 Closure Properties . . . . . . . . . . . . . . . . . . . . 82
4 Model-Checking for RGTR Graphs 85
4.1 Basic Reachability Problems . . . . . . . . . . . . . . . . . . . 86
4.2 Decidable Properties . . . . . . . . . . . . . . . . . . . . . . . 88
vvi CONTENTS
4.2.1 One Step Reachability (EX) . . . . . . . . . . . . . . . 89
4.2.2 Reachability (EF) . . . . . . . . . . . . . . . . . . . . 91
4.2.3 Recurrence (EGF) . . . . . . . . . . . . . . . . . . . . 96
4.3 Undecidable Properties . . . . . . . . . . . . . . . . . . . . . . 113
4.3.1 Simulation of Turing Machines . . . . . . . . . . . . . 114
4.3.2 Universal Reachability (AF) . . . . . . . . . . . . . . . 119
4.3.3 Constrained Reachability (EU) . . . . . . . . . . . . . 120
4.3.4 Universal Recurrence (AGF) . . . . . . . . . . . . . . 120
4.4 A Temporal Logic for Model-Checking . . . . . . . . . . . . . 122
4.5 Reachability Games . . . . . . . . . . . . . . . . . . . . . . . 124
5 Conclusion 133
5.1 Open Problems and Perspectives . . . . . . . . . . . . . . . . 134
Appendix 137
A.1 Computing the Reachable States in Tree Automata . . . . . . 137
A.2 Time Complexity of REACH . . . . . . . . . . . . . . . . . . 140
A.3 Undecidability of \Diverging Conflguration" . . . . . . . . . . 143
Bibliography 147
Index 155Chapter 1
Introduction
Finite graphs constitute one of the most basic data structures used in com-
puter science. In the 1960s and 1970s many e–cient algorithms for the
analysis of flnite graphs were developed. Later, flnite graphs advanced from
a pure data structure to an important tool for modeling and verifying flnite
state-based systems. In the approach of model-checking [Eme81, CE81] al-
gorithms for the automatic veriflcation of systems modeled by flnite graphs
with properties written in certain speciflcation logics are developed. In this
⁄framework temporal logics like LTL, CTL, and CTL (cf. [Eme90]) are
among the most popular speciflcation logics. In the last 20 years many
contributions have been made to this area, and by now the theory of model-
checking flnite systems with temporal speciflcations is well understood (cf.
[BVW94, Var96, Eme96]).
With the motivation to transfer these methods, at least partially, to
inflnite systems the development of a new theory of inflnite graphs started.
Inflnite arise from the use of potentially unbounded data structures
like stacks, counters, or queues. Parametrized systems, which correspond
to inflnite families of systems consisting of several components, the number
of which is determined by the parameter, are another example for inflnite
systems. To represent systems of this kind inflnite graphs are necessary.
For an algorithmic theory of inflnite graphs, classes of inflnite graphs
with flnite representations are needed. Given a formalism for flnite repre-
sentations of graphs from a classK, two natural questions arise:
(i) Which decision problems can be solved for the classK of graphs gen-
erated by this formalism?
(ii) How expressive is the given formalism, i.e., what kind of graphs are in
K, and how isK related to other classes of inflnite graphs?
An example for a problem of type (i) is the reachability problem:
12 CHAPTER 1. INTRODUCTION
Given a flnite representation of a graph G from K and two vertices u;v of
G, is there a path from u to v?
In automatic veriflcation this problem has to be solved to check whether
a system can reach an undesirable state. In contrast to flnite graphs, it
is not clear a priori whether this problem is decidable for a given class of
inflnite graphs. It is easy to deflne classes of inflnite graphs allowing to
use reachability problems to encode undecidable problems like the halting
problem for Turing machines. One task in the development of a theory
of inflnite graphs is to identify classes of inflnite graphs, where elementary
problems like reachability are decidable.
The aim of this thesis is to give a comprehensive analysis of a speciflc
class of inflnite graphs, namely the transition graphs of ground tree rewrit-
1ing systems . The vertices of these graphs are represented by ranked trees
(or terms), and the edges are generated by replacements at the front of the
trees according to a flxed set of rules. We study the structure of ground tree
rewriting graphs (GTR graphs) and their relation to other graph classes,
in particular to pushdown graphs. Furthermore, we analyze several vari-
ants of the above mentioned reachability problem. As some these problems
turn out to be decidable in polynomial time, this analysis shows that GTR
graphsconstitute, fromanalgorithmicpointofview, ausableclassofinflnite
graphs.
Before we give a more detailed explanation of the topics covered in this
thesis we review several classes of graphs that have been considered in the
literature.
Classes of Inflnite Graphs
Pushdown Graphs. In their seminal paper [MS85] Muller and Schupp
analyzed the transition graphs of pushdown automata. The main compo-
nents of a pushdown automaton are a flnite set Q of control states,