Logic and games on automatic structures

Kaiser, Lukasz; Grädel, Erich

doi:2561

Logic and games on automatic structures = Logik und Spiele auf automatischen Strukturen

Kaiser, Lukasz (Author)

2008

Verantwortlichkeitsangabevorgelegt von Lukasz Kaiser

ImpressumAachen : Publikationsserver der RWTH Aachen University 2008

UmfangXIII, 144 S. : graph. Darst.

Aachen, Techn. Hochsch., Diss., 2008

Genehmigende Fakultät
Fak01

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

Tag der mündlichen Prüfung/Habilitation
2008-06-26

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

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Mathematische Logik (Genormte SW) ; Spieltheorie (Genormte SW) ; Automatentheorie (Genormte SW) ; Lindström-Quantor (Genormte SW) ; Informatik (frei) ; Automatischen Strukturen (frei) ; logic (frei) ; games (frei) ; finite model theory (frei) ; automatic structures (frei) ; generalized quantifiers (frei)

Thematische Einordnung (Klassifikation)
DDC: 004
ccs: F.4. * F.1.1

Kurzfassung
Die Auswertung einer logischen Formel kann als ein Spiel betrachtet werden, in dem einer der Spieler versucht, die Formel zu beweisen, und der andere versucht, sie zu wiederlegen. Dieser Zusammenhang kann algorithmisch genutzt werden, um Formeln der Prädikatenlogik erster und zweiter Stufe auf endlichen Strukturen auszuwerten. Wir erweitern diesen spieltheoretischen Ansatz zur Auswertung der Logik erster Stufe auf unendlichen Strukturen, die in der Informatik vorkommen. Da solche Strukturen im Rechner gespeichert und bearbeitet werden sollen, müssen sie endlich darstellbar sein. Wir untersuchen eine grundlegende Klasse von endlich darstellbaren Strukturen, nämlich automatische Strukturen. Die Elemente einer automatischen Struktur werden durch Wörter über einem endlichen Alphabet dargestellt. Relationen solcher Strukturen werden durch synchrone Automaten erkannt, die Tupel von Symbolen des Alphabets Schritt für Schritt bearbeiten. Ein natürliches Beispiel einer automatischen Struktur ist die Presburger Arithmetik. Eine wichtige Eigenschaft automatischer Strukturen ist die Entscheidbarkeit der Logik erster Stufe. Um den Zusammenhang zwischen Logik und Spielen auf automatische Strukturen auszudehnen, suchen wir nach logischen Erweiterungen, die weiterhin entscheidbar bleiben. Wir erweitern den Begriff eines offenen bzw. geschlossenen Spielquantors aus der Modelltheorie infinitärer Logiken zu einem regulären Spielquantor und zeigen, dass dieser Quantor auf automatischen Präsentationen Regularität erhält. Um die Ausdrucksstärke dieses Quantors zu erfassen, bestimmen wir die Klassen von Strukturen, auf denen die Spielquantor-Erweiterung der Logik erster Stufe zur reinen Logik erster Stufe kollabiert. Für Strukturen, die diesen Kollaps nicht aufzeigen, führen wir induktive Automorphismen ein und beweisen, dass sie die durch den Spielquantor definierbaren Relationen enthalten. Model-Checking Spiele für die eingeführte Erweiterung der Logik erster Stufe lassen sich nun auf eine natürliche Weise definieren. Wir erweitern dazu klassische zwei-Spieler Paritätsspiele zu einem Mehrspielermodell, in dem zwei Koalitionen mit einer besonderen Art hierarchischer imperfekter Information gegeneinander spielen. Im Unterschied zum klassischen Fall ist es für hierarchische Spiele wesentlich, dass die Spieler abwechselnd ziehen. Wir zeigen, dass andernfalls die Frage, welche Koalition das Spiel gewinnt, unentscheidbar wird. In einer wichtigen Hinsicht bleibt jedoch die ähnlichkeit zum klassischen Fall erhalten: hierarchische Spiele sind robust unter Veränderungen der Darstellung von Gewinnbedingungen. Ein Grund für diese Robustheit ist, dass ein endlicher Speicher ausreicht, um Spiele mit komplexen Gewinnbedingungen in Spiele mit einfachen Gewinnbedingungen zu übersetzen. Dieses Verfahren war für Spiele mit endlich vielen Prioritäten bereits bekannt, wir erweitern es hier jedoch auf Spiele mit unendlich vielen Prioritäten. Dazu verallgemeinern wir den klassichen Begriff eines Latest Appearance Record zu einer neuen Speicherstruktur, die ausreicht, um Spiele mit endlichen und co-endlichen Mullerbedingungen zu lösen. Gewisse Klassen von Gewinnbedingungen mit unendlich vielen Prioritäten lassen sich durch Zielonka Bäume beschreiben. Wir untersuchen diese Bedingungen und erweitern den klassischen Zusammenhang zwischen der Anzahl der Zweige in einem Zielonka Baum und der Größe des Speichers, die benötigt wird, um ein Spiel zu gewinnen. Verallgemeinerte Lindström Quantoren bilden die Grundlage einer wichtigen Methode die Logik erster Stufe zu erweitern. Wir untersuchen die Frage, welche verallgemeinerten unären Quantoren zur Logik erster Stufe hinzugefügt werden können, ohne die Regulärität definierbarer Relationen zu verletzen. Wir beantworten diese Frage, indem wir diese Quantoren durch Kardinalitäts und Modulo-Zählquantoren charakterisieren. Wir zeigen, dass diese Quantoren auf allen automatischen Strukturen Regularität erhalten, selbst auf nicht-injektiv dargestellten omega-automatischen Strukturen. Damit beantworten wir auch eine offene Frage von Blumensath indem wir zeigen, dass alle abzählbaren omega-automatischen Strukturen auch automatisch sind. Wir untersuchen Kardinalitätsquantoren auch über der Klasse der verallgemeinert-automatischen Stukturen und zeigen anhand der Kompositionsmethode für monadische Logik zweiter Stufe, dass Kardinalitätsquantoren hier zur Logik erster Stufe kollabieren.

The evaluation of a logical formula can be viewed as a game played by two opponents, one trying to show that the formula is true and the other trying to prove it false. This correspondence is exploited algorithmically to evaluate formulas of first and second-order logic on finite structures. We extend the game-based algorithmic approach to first-order logic on infinite structures that arise in computer science. Such structures are stored and manipulated by a computer, thus elements and relations must be represented in a finite way. We study a prominent class of finitely presentable structures, namely automatic structures. Automatic structures consist of elements represented by words over a finite alphabet. Relations within these structures are represented by synchronous automata that perform step-by-step transitions on tuples of symbols from the alphabet. A prominent example of an automatic structure is Presburger arithmetic, for which the natural way of writing numbers as sequences of digits and the standard column addition method constitute an automatic presentation. An important property of automatic structures is that first-order logic is decidable on these structures. To develop the correspondence between games and logic on automatic structures, we first look for suitable extensions of first-order logic that remain decidable. We study the notion of game quantification and extend the notions of open and closed game quantifiers, introduced in the model theory of infinitary logics, to a regular game quantifier. We show that this game quantifier preserves regularity on automatic presentations and investigate its expressive power. We identify the classes of structures on which first-order logic extended with this quantifier collapses to pure first-order logic. For better understanding of the classes where this is not the case, we introduce the notion of inductive automorphisms and show that they preserve relations defined using the game quantifier. Model-checking games for the above extension of first-order logic can be defined in a more natural way than for pure first-order logic. Towards this, we extend the classical two-player parity games to a multiplayer setting where two coalitions play against each other with a particular kind of hierarchical imperfect information about actions of the players. In contrast to the classical case, in hierarchical games it is essential that players alternate. We show that otherwise the problem which coalition wins a hierarchical game is undecidable. Nevertheless, there is an important aspect in which they are similar to classical games: hierarchical games are robust with respect to changes of the representation of winning condition. One reason for this robustness of hierarchical games is that only a finite memory is needed to reduce games with complex winning conditions to games with simpler ones. While this technique has been well-known for games with finitely many priorities, our approach is the first to extend it to games with infinitely many priorities on infinite arenas. We generalize the classical notion of latest appearance record to a new memory structure, which we show to be sufficient for winning Muller games with a finite or co-finite number of sets in the Muller condition, and additionally for a few other classes of games with infinitely many priorities. Certain classes of winning conditions on infinitely many priorities admit descriptions in terms of generalized Zielonka trees. We investigate such conditions and show that the correspondence between the number of branches of a Zielonka tree and the memory needed for strategies generalizes to the case of infinitely many priorities. A basic way of extending first-order logic is by adding generalized Lindström quantifiers. We address the following question: which generalized unary quantifiers can be added to first-order logic without introducing non-regular relations on automatic structures. We answer this question by giving a complete characterization of such quantifiers in terms of definability using cardinality and modulo counting quantifiers. We show that these quantifiers indeed preserve regularity on all automatic structures, including the non-injective omega-automatic ones. As a corollary we answer a question of Blumensath and prove that all countable omega-automatic structures are in fact finite-word automatic. Further, we study cardinality quantifiers on a large class of generalized-automatic structures. We use the composition method for monadic second-order logic to show that on such structures cardinality quantifiers collapse to first-order logic.

Fulltext:
PDF