Decision problems over infinite graphs [Elektronische Ressource] : higher-order pushdown systems and synchronized products / vorgelegt von Stefan Wöhrle

"Stefan Wöhrle"

Sujets

• Mathematics

Informations

• Publié par: rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen
• Publié le: 01 janvier 2005
• Nombre de lectures: 9
• Langue: English

Extrait

DECISION PROBLEMS OVER INFINITE GRAPHS
HIGHER-ORDER PUSHDOWN SYSTEMS AND
SYNCHRONIZED PRODUCTS
Von der Fakultat¤ fur¤ Mathematik, Informatik und
Naturwissenschaften der Rheinisch-Westfalischen¤ Technischen
Hochschule Aachen zur Erlangung des akademischen Grades eines
Doktors der Naturwissenschaften genehmigte Dissertation
vorgelegt von
Diplom-Mathematiker
Stefan Wohrle¤
aus Offenburg
Berichter: Univ.-Prof. Dr. Wolfgang Thomas
Dr. habil. Didier Caucal
Tag der mundlichen¤ Prufung:¤ 30. Juni 2005
Diese Dissertation ist auf den Internetseiten der Hochschulbibliothek
online verfugbar¤Abstract
The extension of formal veri cation methods to in nite models requires
classes of graphs which are nitely representable and for which the
model checking problem is decidable. We consider three approaches to
de ne classes of nitely representable graphs: internal representations
as con guration graphs of higher-order pushdown systems, transfor-
mational representations by application of operations which preserve
the decidability of the model checking problem, and by composition
from components using synchronized products.
In the rst 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 push-
down graphs and can conclude that they enjoy a decidable monadic
second-order theory.
In the second part of the thesis investigate synchronized products
of nitely representable in nite graphs and show that the decidabil-
ity of an extension of rst-order logic with reachability predicates is
preserved under the formation of nitely 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.Zusammenfassung
Die Erweiterung formaler Veri kationsmethoden auf unendliche Sys-
teme erfordert die Untersuchung von endlich darstellbaren Graphklas-
sen, fur¤ die das Model Checking Problem entscheidbar ist. Wir be-
trachten drei Zugange,¤ um solche Graphklassen zu de nieren: interne
Darstellungen als Kon gurationsgraphen von Kellerautomaten hoher¤ er
Ordnung, Darstellungen durch Transformationen, die die Entscheid-
barkeit 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 hoher¤ er Ordnung erzeugt wer-
den, mit der mittels Transformationen de ninierten Caucal Hierarchie
uber¤ einstimmt. Wir konnen¤ somit schlie en, dass die monadische The-
orie dieser Graphen entscheidbar ist.
Im zweiten Teil der Arbeit untersuchen wir synchronisierte Produkte
endlich darstellbarer Graphen im Bezug auf das Model Checking Prob-
lem. Wir betrachten unter anderem die Logik der ersten Stufe erweitert
um Erreichbarkeitspradikate¤ und zeigen, dass nur die Bildung endlich
synchronisierter Produkte die Entscheidbarkeit dieser Logik erhalt.¤ Die-
ses Ergebnis wird durch Unentscheidbarkeitsresultate fur¤ Varianten der
zulassigen¤ Produktoperationen und der betrachteten Logiken erganzt.¤Contents
1 Introduction 9
2 Preliminaries and Background Theory 21
2.1 Graph Structures and Speci cation Logics. . . . . . . . . . . . . . . . . . .21
2.1.1 Graph Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .21
2.1.2 Speci cation Logics. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .23
2.1.3 The Model Checking Problem. . . . . . . . . . . . . . . . . . . . . . . . . .25
2.2 Graphs Represented by Finite Systems . . . . . . . . . . . . . . . . . . . . . .26
2.2.1 Pushdown Systems and Pre x Rewriting Graphs. . . . . .26
2.2.2 Pre x Recognizable Graphs and Pushdown Graphs . . .27
2.2.3 Automatic Graphs and Rational Graphs . . . . . . . . . . . . . . .28
2.2.4 Tree Rewriting Graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .29
2.3 Finite Representations via Operations . . . . . . . . . . . . . . . . . . . . . . .31
2.3.1 Inverse Rational Mappings and Transductions. . . . . . . . .31
2.3.2 Iteration of Structures and Unfolding . . . . . . . . . . . . . . . . . .32
2.3.3 Synchronized Products . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .34
2.4 The Caucal Hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .35
3 Graphs of Higher-order Pushdown Systems 39
3.1 Higher-order Pushdown Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . .40
3.2 The Treegraph Operation and Transductions . . . . . . . . . . . . . . . .46
3.2.1 A Deterministic Subhierarchy . . . . . . . . . . . . . . . . . . . . . . . . . .47
3.2.2 Trees Suf ce . . . . . . . . . . . . . . . . . . . . . . . . . . . . .52
3.3 From HOPDG to Caucal Graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . .55
3.4 From Caucal Graphs to HOPDG . . . . . . . . . . . . . . . . . . . . . . . . . . . . .58
3.4.1 HOPDS with Equality Pop . . . . . . . . . . . . . . . . . . . . . . . . . . . . .58
3.4.2 Unfoldings of HOPDGs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .75
3.4.3 Caucal Graphs as HOPDGs . . . . . . . . . . . . . . . . . . . . . . . . . . . .77
3.5 Properties of HOPDGs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .81
78
4 Synchronized Products of Graphs 85
4.1 Transitive Closure Logic over the In nite Grid . . . . . . . . . . . . . .86
24.1.1 Undecidability of FO(TC) . . . . . . . . . . . . . . . . . . . . . . . . . . . .87(1)
14.1.2 Decidability of FO(TC) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .90
(1)
4.2 A Composition Theorem for FO(R) . . . . . . . . . . . . . . . . . . . . . . . . . .95
4.3 Undecidability Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
5 Conclusion 111
Bibliography 117
Index 125Chapter 1
Introduction
Several techniques have been invented to assist developers in assuring
the correctness of computing systems. Among the automatic formal
veri cation methods, see e.g [Pel01] for an overview, the model check-
ing paradigm introduced in [CE81] was most successful.
S ˆ! M(S) ˆ! ’
Figure 1.1: The model checking paradigm
The idea of model checking is depicted in Figure 1.1. Given a com-
puting systemS, a formal modelM(S) is de ned. An expected behav-
ior of the system model is formalized by a formula’ in a certain spec-
i cation logic, and an automatic procedure, i.e. an algorithm, veri es
whether the modelM(S) satis es (j=) the formula’.
Conditions posed on the behavior of a system are often Boolean
combinations of rather simple requirements like
† Guaranty: Eventually something happens.
† Safety: Something never happens.
† Recurrence: Something happens again and again.
† Fairness: If something happens in nitely often, then something
else happens in nitely often.
910 1 INTRODUCTION
Temporal logics like LTL and CTL allow to express such properties.
They play a prominent role as speci cation languages in model check-
ing, see e.g. [CGP99], but also non-temporal logics like the modal „-
calculus or monadic second-order logic (MSO) are considered. The sys-
tem models are usually Kripke structures or transition systems [Arn94].
Both can be seen as edge and/or vertex labeled graphs where vertices
represent internal states of the system, their labels represent certain
properties of these states, and an edge labeled by a symbola between a
vertexv and a vertexw implies that there is some actiona which causes
the system to change its state fromv tow.
Model checking of nite state-based systems is nowadays well un-
derstood, see [CGP99, Pel01] and references therein. It is applied in
practice even for large scale models. However, in nite state spaces nat-
urally arise when modeling real world systems. Real world systems
usually contain potentially in nite structures such as call stacks, coun-
ters, communication queues or channels. Thus the generation of nite
models always requires abstraction techniques which may constrain the
applicability of results obtained by a model checker.
In the last years considerable effort has been spent to transfer the
results known about nite models at least partially to in nite models.
The present thesis is a contribution to this track of research.
The extension of the model checking paradigm to in nite state sys-
tems raises two problems which are not present for nite ones: the sys-
tem must be nitely representable to be handled by an algorithm which
decides whetherM(S) satis es a speci cation’, and such an algorithm
must exist, i.e. the model checking problem ?M(S)j= ’? must be
decidable.
It is quite obvious that for keeping the model checking problem de-
cidable there is a tradeoff between the richness of a class of models and
the expressive power of the logic under consideration. Expressive log-
ics like monadic second-order logic are already undecidable over very
simple system models such as the in nite grid, whereas the quanti er
free fragment of rst-order logic is decidable even for recursive graphs,
i.e. graphs