Pure and applied fixed point logics [Elektronische Ressource] / vorgelegt von Stephan Kreutzer
239 pages
English

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Pure and applied fixed point logics [Elektronische Ressource] / vorgelegt von Stephan Kreutzer

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
239 pages
English
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Description

Pure and AppliedFixed-Point LogicsVon der Fakult at fur Mathematik, Informatik undNaturwissenschaften der Rheinisch-Westf alischen TechnischenHochschule Aachen zur Erlangung des akademischen Grades einesDoktors der Naturwissenschaften genehmigte Dissertationvorgelegt vonDiplom-InformatikerStephan Kreutzeraus Aachen, DeutschlandBerichter: Universit atsprofessor Dr. Erich Gr adelUniversit Dr. Wolfgang ThomasTag der mundlic hen Prufung: 17.12.2002Diese Dissertation ist auf den Internetseiten der Hochschulbibliothek online verfugbar.23AbstractFixed-point logics are logics with an explicit operator for forming xed pointsof de nable mappings. They are particularly well suited for modelling recur-sion in logical languages and consequently they have found applications invarious areas of theoretical computer science such as database theory, nitemodel theory, and computer-aided veri cation.The topic of this thesis is the study of xed-p oint logics with respect totheir expressive power. Of particular interest are logics based on in ationary xed points and their comparison to least xed-p oint logics.The rst part focuses on xed-p oint extensions of rst-order logic. Inthe main result we show that in ationary and least xe d-point logic { theextensions of rst-order logic by least and in ationary xed points { havethe same expressive power on all structures, i.e. LFP = IFP.In the second part of this thesis, we study xed-p oint extensions of modallogic.

Sujets

Informations

Publié par
Publié le 01 janvier 2002
Nombre de lectures 12
Langue English
Poids de l'ouvrage 1 Mo

Extrait

Pure and Applied
Fixed-Point Logics
Von der Fakult at 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
Stephan Kreutzer
aus Aachen, Deutschland
Berichter: Universit atsprofessor Dr. Erich Gr adel
Universit Dr. Wolfgang Thomas
Tag der mundlic hen Prufung: 17.12.2002
Diese Dissertation ist auf den Internetseiten der Hochschulbibliothek online verfugbar.23
Abstract
Fixed-point logics are logics with an explicit operator for forming xed points
of de nable mappings. They are particularly well suited for modelling recur-
sion in logical languages and consequently they have found applications in
various areas of theoretical computer science such as database theory, nite
model theory, and computer-aided veri cation.
The topic of this thesis is the study of xed-p oint logics with respect to
their expressive power. Of particular interest are logics based on in ationary
xed points and their comparison to least xed-p oint logics.
The rst part focuses on xed-p oint extensions of rst-order logic. In
the main result we show that in ationary and least xe d-point logic { the
extensions of rst-order logic by least and in ationary xed points { have
the same expressive power on all structures, i.e. LFP = IFP.
In the second part of this thesis, we study xed-p oint extensions of modal
logic. Such logics are widely used in the eld of computer-aided veri cation.
Again, the least xed-p oint extension of modal logic, the modal -calculus,
is of particular interest and is among the best studied logics in this area.
The main contribution of the second part is the introduction and study of
the corresponding in ationary xed-p oint logic. Contrary to the case of
rst-order logic mentioned above, where least and in ationary xed points
lead to equivalent logics, it is shown that in the context of modal logic,
in ationary xed points are far more expressive than least xed points. On
the other hand, they are algorithmically far more complex.
Besides the two main results, we study a variety of di eren t xed-p oint
logics and develop methods to compare their expressive power.
Finally, in the third part, we study xed-p oint logics as query languages
for constraint databases. It is shown that already relatively simple logics
such as the transitive closure logic lead to undecidable query languages on
constraint databases. Therefore we consider suitable restrictions of xed-
point logics to obtain tractable query languages, i.e. languages with polyno-
mial time evaluation.
A detailed overview of the results presented in this thesis can be found
in the second part of the introduction.
Zusammenfassung
Die vorliegende Dissertation beschaftigt sich mit der Untersuchung von Fix-
punktlogiken hinsichtlich ihrer Ausdrucksstarke. Der Schwerpunkt liegt da-
bei auf in ation aren Fixpunktlogiken und ihrer Abgrenzung von Logiken,
die auf kleinsten Fixpunkten basieren. Im ersten Teil der Arbeit werden da-
zu die seit langem bekannten Fixpunkterweiterungen der Pradikatenlogik
untersucht. Das Hauptergebnis ist der Beweis, da die Logiken LFP und4
IFP, also die Erweiterung der Pradikatenlogik um kleinste und in ation are
Fixpunkte, die gleiche Ausdrucksstark e haben. Es gilt also LFP = IFP.
Im zweiten Teil der Arbeit stehen dann Fixpunkterweiterungen der Mo-
dallogik im Vordergrund, wie sie intensiv im Bereich der automatischen Ve-
ri k ation studiert werden. Wahrend der modale -Kalkul (L ), die Erwei-
terung der Modallogik um kleinste Fixpunkte, schon seit Anfang der 80er
Jahre eingehend untersucht wird, wird hier zum ersten Mal die entsprechen-
de in ation are Logik, der modale Iterationskalkul (MIC), betrachtet. Es zeigt
sich, da , im Gegensatz zum Fall der Pradikatenlogik, in ation are Fixpunk-
te im modallogischen Kontext eine sehr viel gro ere Ausdrucksstarke bieten
als kleinste. MIC ist also sehr viel ausdrucksstark er als L , allerdings im
Hinblick auf algorithmische Probleme auch erheblich komplexer.
Neben diesen beiden Hauptergebnissen werden in den ersten beiden Tei-
len der Arbeit noch weitere Arten von Fixpunktlogiken studiert und Metho-
den zum Vergleich ihrer Ausdrucksstarke entwickelt.
Im dritten und letzten Teil der Dissertation stehen sogenannte constraint
Datenbanken im Zentrum der Betrachtungen. Hierbei handelt es sich um ein
relativ neues Datenbankmodell, das sich besonders zur Speicherung geome-
trischer Daten eignet. Ahnlich wie bei relationalen Datenbanken konnen
auch hier Fixpunktlogiken als Grundlage von Abfragesprachen dienen. In
Teil III wird gezeigt, da in diesem Bereich allerdings schon relativ einfache
Fixpunktlogiken, wie die transitive Hullenlogik, unentscheidbare Sprachen
liefern. Anhand zweier auf kleinsten Fixpunkten basierenden Logiken wird
jedoch demonstriert, da durch geeignete De nition der Logiken auch im
constraint Datenbankbereich algorithmisch handhabbare Abfragesprachen
mit Hilfe von Fixpunktlogiken de niert werden konnen.
Eine ausfuhrlic here Darstellung der in dieser Dissertation prasen tierten
Ergebnisse ndet sich im zweiten Teil der Einleitung.5
Acknowledgements
I have many people to thank and acknowledge. First of all, I want to thank
my advisor, Erich Gr adel, for all his support and encouragement during the
last four years. I am grateful to Anuj Dawar for the very enjoyable collabo-
ration on several parts of this thesis and in particular for his patience during
the discussions about the equivalence of least and in ationary xed-p oint
logic. Many thanks also to my colleagues, in particular Achim Blumensath
and Dietmar Berwanger. Often enough they had the misfortune of being in
their o ce { Achim mostly before anyone else arrived and Dietmar primarily
after everybody else left { when I needed someone to bother with questions.
Further, I want to thank the database group in Limburg, in particular Jan
Van den Bussche and Floris Geerts for the pleasant discussions we had on
constraint databases. Very special thanks go to Jan Van den Bussche for
attracting my attention to the expressive power of strati ed xed-p oint logic
and transitive-closure logic on constraint databases. Unknowingly, his ques-
tions raised at an AFM-seminar in Aachen gave me the impulse to study
xed-p oint logics on in nite structures and in this sense made the results
reported in the rst part of this thesis possible. Finally, I want to thank all
the other people who contributed to this thesis in some way, in particular
Colin Hirsch and David Richerby for proofreading parts of the manuscript.6Contents
1 Introduction 11
2 Preliminaries 27
I Fixed-Point Extensions of First-Order Logic 29
3 Least and In ationary Fixed-Point Logic 31
3.1 De nitions by Monotone Inductions . . . . . . . . . . . . . . 31
3.2 Elementary Inductive De nitions . . . . . . . . . . . . . . . . 33
3.3 Least and Monotone Fixed-Point Logic . . . . . . . . . . . . . 37
3.3.1 Simultaneous Inductions . . . . . . . . . . . . . . . . . 39
3.3.2 Alternation and Nesting in Least Fixed-Point Logic . 41
3.3.3 Comparing the Stages . . . . . . . . . . . . . . . . . . 43
3.4 In ationary Fixed-Point Logic . . . . . . . . . . . . . . . . . . 44
3.5 Inductive Fixed Points and Second-Order Logic . . . . . . . . 50
4 Other Fixed-Point Logics 53
4.1 Fragments of Least Fixed-Point Logic . . . . . . . . . . . . . 53
4.1.1 Transitive Closure Logics . . . . . . . . . . . . . . . . 53
4.1.2 Existential and Strati ed Fixed-Point Logic . . . . . . 54
4.2 Partial Fixed-Point Logic . . . . . . . . . . . . . . . . . . . . 56
5 Descriptive Complexity 59
5.1 Evaluation Complexity of Fixed-Point Formulae . . . . . . . . 61
5.2 Logics Capturing Complexity Classes . . . . . . . . . . . . . . 62
6 Fixed-Point Logics with Choice 65
6.1 Choice Fixed-Point Logic . . . . . . . . . . . . . . . . . . . . 66
6.1.1 Simplifying the First-Order Quanti er Structure . . . 69
6.1.2 Choice Fixed-Point and Second-Order Logic . . . . . . 71
6.1.3 Arity-Restricted CFP and Transitive-Closure Logic . . 73
6.2 Fixed-Point Logics with Alternating Choice . . . . . . . . . . 75
78 CONTENTS
7 A General Semantics for Partial Fixed-Point Logic 77
7.1 An Alternative Semantics for Partial Fixed-Point Logic . . . 79
7.2 Separating Partial and In ationaryoint Logic . . . . 85
7.2.1 Acceptable Structures, Coding, and Diagonalisation . 85
7.2.2 Separating Partial and In ationary Fixed-Point Logic 87
8 Equivalence of Least and In ationary Fixed-Point Logic 91
8.1 Equivalence on Finite Structures . . . . . . . . . . . . . . . . 91
8.2 Equiv in the General Case . . . . . . . . . . . . . . . . 94
8.3 Open Problems . . . . . . . . . . . . . . . . . . . . . . . . . . 100
II Modal Fixed-Point Logics 101
9 Modal Logics and Bisimulation 103
9.1 Transition Systems . . . . . . . . . . . . . . . . . . . . . . . . 104
9.2 Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
9.3 Modal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
10 The Modal -Calculus 111
11 The Modal Iteration Calculus 115
11.1 The Satis abilit y Problem for MIC . . . . . . . . . . . . . . . 118
11.2 The Model Checking Problem for MIC . . .

  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • Podcasts Podcasts
  • BD BD
  • Documents Documents