Definability and model checking : the role of orders and compositionality

Ganzow, Tobias; Grädel, Erich

doi:31517

Definability and model checking : the role of orders and compositionality = Definierbarkeit und Model Checking : die Rolle von Ordnungen und Kompositionalität

Ganzow, Tobias (Author)

2011 & 2012

Verantwortlichkeitsangabevorgelegt von Tobias Ganzow

ImpressumAachen : Publikationsserver der RWTH Aachen University 2011

UmfangVIII, 127 S. : graph. Darst.

Aachen, Techn. Hochsch., Diss., 2011

Zsfassung in dt. und engl. Sprache. - Prüfungsjahr: 2011. - Publikationsjahr: 2012

Genehmigende Fakultät
Fak01

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

Tag der mündlichen Prüfung/Habilitation
2011-02-22

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

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Mathematische Logik (Genormte SW) ; Endliche Modelltheorie (Genormte SW) ; Definierbarkeit (Genormte SW) ; Model Checking (Genormte SW) ; Kompositionalität (Genormte SW) ; Informatik (frei) ; Ordnungsinvarianz (frei) ; Deskriptive Komplexitätstheorie (frei) ; finite model theory (frei) ; descriptive complexity theory (frei) ; order invariance (frei) ; counting quantifier (frei)

Thematische Einordnung (Klassifikation)
DDC: 004
ccs: F.4.1

Kurzfassung
Die Grenzen der Audrucksstärke von Logiken auszuloten und Zusammenhänge zwischen den für die Definition bestimmter Eigenschaften von Strukturen benötigten deskriptiven Mitteln und der Komplexität der entsprechenden Entscheidungsprobleme zu finden, sind zentrale Aspekte der Endlichen Modelltheorie und Deskriptiven Komplexitätstheorie. Vor allem in den letzten Jahren ist zunehmend auch die Modelltheorie und die algorithmische Handhabbarkeit von endlich repräsentierbaren unendlichen Strukturen in den Fokus der Forschung gerückt. Im ersten Teil der Dissertation wird untersucht, wie sich das Vorhandensein von Ordnungen in einer Struktur auf die Ausdrucksstärke von Logiken auswirkt, und zunächst das Konzept der sogenannten ordnungsinvarianten Definierbarkeit motiviert. Hierbei darf in einer Formel eine Ordnungsrelation verwendet werden, die nicht Bestandteil der Struktur ist, allerdings darf das Auswertungsergebnis der Formel innerhalb einer Struktur nicht von einer bestimmten (linearen) Ordnung der Elemente abhängen. Wir können zeigen, dass ordnungsinvariante monadische Logik zweiter Stufe (MSO) echt ausdrucksstärker ist als die Erweiterung von MSO um Modulo-Zählquantoren. Anschließend untersuchen wir schwächere Arten von Ordnungen am Beispiel von lokal geordneten ungerichteten Graphen, in denen nur die Nachbarschaften von Knoten linear geordnet sind. Für diese Klasse können wir unter Ausnutzung eines vor wenigen Jahren von Reingold präsentierten Erreichbarkeitsalgorithmus zeigen, dass die transitive Hülle der Kantenrelation durch eine DTC-Formel definierbar ist, wenn die Graphen als zweisortige Struktur vorliegen. Aus diesem Resultat folgt schließlich, dass die Ausdrucksstärke von DTC mit Zählquantoren genau mit der Platzkomplexitätsklasse LogSpace zusammenfällt. Der zweite Teil der Arbeit widmet sich dem Auswertungsproblem von WMSO auf einer Klasse von unendlichen Strukturen, den induktiven Strukturen, die durch endliche Gleichungssysteme repräsentiert werden können und somit häufig bei Verifikationsproblemen anzutreffende Strukturen wie z.B. den unendlichen Binärbaum oder unendliche Listen umfassen. Im Gegensatz zu automatentheoretischen Methoden, die mit gewissen Nachteilen verbunden sind, wird ein Algorithmus entwickelt, der auf der Dekompositionsmethode beruht und damit direkt auf Formelebene arbeitet. Weiterhin wird gezeigt, wie sich der Ansatz erweitern lässt, um einen Algorithmus für das Auswertungsproblem von WMSO mit dem Unbeschränktheitsquantor auf induktiven Strukturen zu erhalten und somit dessen Entscheidbarkeit zu zeigen.

Finite model theory and descriptive complexity theory are concerned with assessing the expressive power of logics over finite models and with relating the descriptive resources needed for defining a class of structures to the computational complexity of the corresponding decision problem. In recent years, also the model theory and computational handling (e.g. of the model checking problem) of finitely representable infinite structures have gained much interest. In the first part of this thesis we study how the expressive power of logics over finite structures is affected by the presence of orders. We will first review the concept of order-invariant definability where we allow formulae to use an additional order-relation that is not present in a given structure in such a way that the truth of the formula in the structure does not depend on the actual interpretation of the order relation, and show that, in the context of monadic second-order logic, order-invariance yields more expressive power than adding modulo-counting quantifiers. Second, we investigate structures with weaker forms of orderings, namely locally ordered graphs, in which only the neighbourhoods of the vertices are linearly ordered. Using recent results on reachability algorithms by Reingold, we are able to show that the transitive closure of the edge relation in such graphs is definable in deterministic transitive closure logic (DTC) in a two-sorted setting, and this observation is the key to linking the descriptive power of DTC with counting to the computational power of logspace-bounded Turing machines. The second part of the thesis is concerned with techniques for model checking weak monadic second-order logic (WMSO) on the class of so-called inductive structures that allow for a finite representation via systems of equations, and which includes structures relevant for verification purposes such as the infinite binary tree, infinite lists, etc. Our new approach presents an algorithmic alternative to automata-theoretic methods, which exhibit certain drawbacks, and is based on a purely logical decomposition technique using the defining equations. Further, the deployed techniques can be extended to obtain a model checking algorithm for the extension of WMSO by an unbounding quantifier, and thus establish the decidability of its model checking problem on the class of inductive structures.

Fulltext:
PDF