Definability and model checking : the role of orders and compositionality

• Definierbarkeit und Model Checking : die Rolle von Ordnungen und Kompositionalität

Ganzow, Tobias; Grädel, Erich (Thesis advisor)

Aachen : Publikationsserver der RWTH Aachen University (2011, 2012)
Doktorarbeit

Aachen, Techn. Hochsch., Diss., 2011

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.