Pure and applied fixed point logics

Kreutzer, Stephan; Grädel, Erich

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

Pure and applied fixed point logics

Kreutzer, Stephan (Author)

2002 & 2003

Verantwortlichkeitsangabevorgelegt von Stephan Kreutzer

ImpressumAachen : Publikationsserver der RWTH Aachen University 2002

Umfang237 S. : graph. Darst.

Aachen, Techn. Hochsch., Diss., 2002

Prüfungsjahr: 2002. - Publikationsjahr: 2003

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Grädel, Erich (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2002-12-17

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

Einrichtungen

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

Inhaltliche Beschreibung (Schlagwörter)
Fixpunkt-Logik (Genormte SW) ; Mathematik (frei)

Thematische Einordnung (Klassifikation)
DDC: 510

Kurzfassung
Die vorliegende Dissertation beschäftigt sich mit der Untersuchung von Fixpunktlogiken hinsichtlich ihrer Ausdrucksstärke. Der Schwerpunkt liegt dabei auf inflationären Fixpunktlogiken und ihrer Abgrenzung von Logiken, die auf kleinsten Fixpunkten basieren. Im ersten Teil der Arbeit werden dazu die seit langem bekannten Fixpunkterweiterungen der Prädikatenlogik untersucht. Das Hauptergebnis ist der Beweis, daß die Logiken LFP und IFP, also die Erweiterung der Prädikatenlogik um kleinste und inflationäre Fixpunkte, die gleiche Ausdrucksstärke haben. Es gilt also LFP = IFP. Im zweiten Teil der Arbeit stehen dann Fixpunkterweiterungen der Modallogik im Vordergrund, wie sie intensiv im Bereich der automatischen Verifikation studiert werden. Während der modale mu-Kalkül (L_mu), die Erweiterung der Modallogik um kleinste Fixpunkte, schon seit Anfang der 80er Jahre eingehend untersucht wird, wird hier zum ersten Mal die entsprechende inflationäre Logik, der modale Iterationskalkül (MIC), betrachtet. Es zeigt sich, daß, im Gegensatz zum Fall der Prädikatenlogik, inflationäre Fixpunkte im modallogischen Kontext eine sehr viel größere Ausdrucksstärke bieten als kleinste. MIC ist also sehr viel ausdrucksstärker als L_mu, allerdings im Hinblick auf algorithmische Probleme auch erheblich komplexer. Neben diesen beiden Hauptergebnissen werden in den ersten beiden Teilen der Arbeit noch weitere Arten von Fixpunktlogiken studiert und Methoden zum Vergleich ihrer Ausdrucksstärke 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 geometrischer Daten eignet. Ähnlich wie bei relationalen Datenbanken können 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 Hüllenlogik, unentscheidbare Sprachen liefern. Anhand zweier auf kleinsten Fixpunkten basierenden Logiken wird jedoch demonstriert, daß durch geeignete Definition der Logiken auch im constraint Datenbankbereich algorithmisch handhabbare Abfragesprachen mit Hilfe von Fixpunktlogiken definiert werden können. Eine ausführlichere Darstellung der in dieser Dissertation präsentierten Ergebnisse findet sich im zweiten Teil der Einleitung.

Fixed-point logics are logics with an explicit operator for forming fixed points of definable mappings. They are particularly well suited for modelling recursion in logical languages and consequently they have found applications in various areas of theoretical computer science such as database theory, finite model theory, and computer-aided verification. The topic of this thesis is the study of fixed-point logics with respect to their expressive power. Of particular interest are logics based on inflationary fixed points and their comparison to least fixed-point logics. The first part focuses on fixed-point extensions of first-order logic. In the main result we show that inflationary and least fixed-point logic -- the extensions of first-order logic by least and inflationary fixed points -- have the same expressive power on all structures, i.e. LFP = IFP. In the second part of this thesis, we study fixed-point extensions of modal logic. Such logics are widely used in the field of computer-aided verification. Again, the least fixed-point extension of modal logic, the 'modal mu-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 inflationary fixed-point logic. Contrary to the case of first-order logic mentioned above, where least and inflationary fixed points lead to equivalent logics, it is shown that in the context of modal logic, inflationary fixed points are far more expressive than least fixed points. On the other hand, they are algorithmically far more complex. Besides the two main results, we study a variety of different fixed-point logics and develop methods to compare their expressive power. Finally, in the third part, we study fixed-point 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 fixed-point logics to obtain tractable query languages, i.e.~languages with polynomial time evaluation. A detailed overview of the results presented in this thesis can be found in the second part of the introduction.

Fulltext:
PDF
(additional files)