TU Darmstadt / ULB / TUbiblio

Cayley Structures and the Expressiveness of Common Knowledge Logic

Canavoi, Felix (2018)
Cayley Structures and the Expressiveness of Common Knowledge Logic.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung

Kurzbeschreibung (Abstract)

Van Benthem's theorem states that basic modal logic \ML is expressively equivalent to the bisimulation-invariant fragment of first-order logic $\FO/{\sim}$; we write $\ML\equiv\FO/{\sim}$ for short. Hence, \ML can express every bisimulation-invariant first-order property and, moreover, \ML can be considered an effective syntax for the undecidable fragment $\FO/{\sim}$. Over the years, many variations of this theorem have been established. Rosen proved that $\ML\equiv\FO/{\sim}$ is still true when restricted to finite transition systems. Going beyond first-order logic, Janin and Walukiewicz showed that the bisimulation-invariant fragment of monadic second-order logic \MSO is precisely as expressive as the modal $\mu$-calculus~\Lmu, and several important fragments of~\Lmu have been characterised classically in a similar vein. However, whether $\Lmu\equiv\MSO/{\sim}$ is true over finite transition systems, remains an open problem.

This thesis is concerned with modal common knowledge logic \MLCK, another fragment of~\Lmu that is more expressive than \ML. The main result is a characterisation of \MLCK over \Sfive structures, both classically and also in the sense of finite model theory. We achieved this result by showing that $\ML\equiv\FO/{\sim}$ over the non-elementary classes of (finite or arbitrary) common knowledge Kripke structures (\CK Structures).

The fixpoint character of the derived accessibility relations of \CK structures poses a novel challenge for the analysis of model-theoretic games. The technical core of this thesis deals with the development of a specific structure theory for specially adapted \ca graphs, which we call \ca structures. We show that questions regarding \CK structures can be reduced, up to bisimulation, to \ca structures. Specific acyclicity properties of \ca structures make it possible to adapt and expand known locality-based methods, which leads to new techniques for playing first-order \EF games over these non-elementary structures.

Typ des Eintrags: Dissertation
Erschienen: 2018
Autor(en): Canavoi, Felix
Art des Eintrags: Erstveröffentlichung
Titel: Cayley Structures and the Expressiveness of Common Knowledge Logic
Sprache: Englisch
Referenten: Otto, Prof. Dr. Martin ; Dawar, Prof. Dr. Anuj ; Blumensath, Prof. Dr. Achim
Publikationsjahr: 2018
Ort: Darmstadt
Datum der mündlichen Prüfung: 22 November 2018
URL / URN: https://tuprints.ulb.tu-darmstadt.de/8269
Kurzbeschreibung (Abstract):

Van Benthem's theorem states that basic modal logic \ML is expressively equivalent to the bisimulation-invariant fragment of first-order logic $\FO/{\sim}$; we write $\ML\equiv\FO/{\sim}$ for short. Hence, \ML can express every bisimulation-invariant first-order property and, moreover, \ML can be considered an effective syntax for the undecidable fragment $\FO/{\sim}$. Over the years, many variations of this theorem have been established. Rosen proved that $\ML\equiv\FO/{\sim}$ is still true when restricted to finite transition systems. Going beyond first-order logic, Janin and Walukiewicz showed that the bisimulation-invariant fragment of monadic second-order logic \MSO is precisely as expressive as the modal $\mu$-calculus~\Lmu, and several important fragments of~\Lmu have been characterised classically in a similar vein. However, whether $\Lmu\equiv\MSO/{\sim}$ is true over finite transition systems, remains an open problem.

This thesis is concerned with modal common knowledge logic \MLCK, another fragment of~\Lmu that is more expressive than \ML. The main result is a characterisation of \MLCK over \Sfive structures, both classically and also in the sense of finite model theory. We achieved this result by showing that $\ML\equiv\FO/{\sim}$ over the non-elementary classes of (finite or arbitrary) common knowledge Kripke structures (\CK Structures).

The fixpoint character of the derived accessibility relations of \CK structures poses a novel challenge for the analysis of model-theoretic games. The technical core of this thesis deals with the development of a specific structure theory for specially adapted \ca graphs, which we call \ca structures. We show that questions regarding \CK structures can be reduced, up to bisimulation, to \ca structures. Specific acyclicity properties of \ca structures make it possible to adapt and expand known locality-based methods, which leads to new techniques for playing first-order \EF games over these non-elementary structures.

Alternatives oder übersetztes Abstract:
Alternatives AbstractSprache

Nach dem Satz von van Benthem ist Modallogik \ML genauso ausdrucksstark wie das bisimulationsinvariante Fragment der Logik erster Stufe $\FO/{\sim}$; abgek\"urzt schreiben wir $\ML\equiv\FO/{\sim}$. Damit kann \ML alle bisimulationsinvarianten Aussagen der Logik erster Stufe ausdr\"ucken und \ML kann als eine effektive Syntax f\"ur das unentscheidbare Fragment $\FO/{\sim}$ betrachtet werden. Eine Reihe von Varianten dieses Satzes wurde im Laufe der Jahre bewiesen. Rosen hat gezeigt, dass $\ML\equiv\FO/{\sim}$ auch unter Einschr\"ankung auf endliche Transitionssysteme gilt. \"Uber die Ausdrucksst\"arke der ersten Stufe hinausgehend haben Janin und Walukiewicz gezeigt, dass das bisimulationsinvariante Fragment der monadischen Logik zweiter Stufe \MSO \"aquivalent zum modalen $\mu$-Kalk\"ul~\Lmu ist. Weitere wichtige Fragmente von~\Lmu wurden klassisch auf \"ahnliche Weise charakterisiert. Ob $\Lmu\equiv\MSO/{\sim}$ auch \"uber endlichen Transitionssystemen gilt, bleibt jedoch weiterhin ein offenes Problem.

Diese Dissertation besch\"aftigt sich mit modaler Common Knowledge Logik \MLCK, einem weiteren Fragment von~\Lmu, das ausdrucksst\"arker als \ML ist. Das Hauptresultat ist eine Charakterisierung von \MLCK \"uber \Sfive-Strukturen, sowohl klassisch als auch im Sinne der endlichen Modelltheorie. Dieses Resultat wurde bewiesen, indem wir gezeigt haben, dass $\ML\equiv\FO/{\sim}$ \"uber den nicht-elementaren Klassen der endlichen und beliebigen Common-Knowledge-Kripke-Strukturen (\CK-Strukturen) gilt.

Der Fixpunkt-Charakter der abgeleiteten Kantenrelationen der \CK-Strukuren bereitet eine neuartige Herausforderung f\"ur die Analyse modelltheoretischer Spiele. Der technische Kern dieser Dissertation befasst sich mit der Entwicklung einer spezifischen Strukturtheorie f\"ur speziell adaptierte Cayleygraphen, die wir als Cayleystrukturen bezeichnen. Wir zeigen, dass sich Fragen \"uber \CK-Strukuren bis auf Bisimulation auf Cayleystrukturen reduzieren lassen. Spezifische Azyklizit\"atseigenschaften von Cayleystrukturen erm\"oglichen es, bekannte lokalit\"atsbasierte Methoden anzupassen und zu erweitern, was zu neuen Techniken f\"ur \EF-Spiele \"uber diesen nicht-elementaren Strukturen f\"uhrt.

Deutsch
URN: urn:nbn:de:tuda-tuprints-82696
Sachgruppe der Dewey Dezimalklassifikatin (DDC): 500 Naturwissenschaften und Mathematik > 510 Mathematik
Fachbereich(e)/-gebiet(e): 04 Fachbereich Mathematik
04 Fachbereich Mathematik > Logik
04 Fachbereich Mathematik > Logik > Algorithmic Model Theory
04 Fachbereich Mathematik > Logik > Algorithmic Model Theory > Model Constructions and Model-Theoretic Games in Special Classes of Structures
04 Fachbereich Mathematik > Logik > Algorithmic Model Theory > Model Constructions and Model-Theoretic Games in Special Classes of Structures > Model Theory of Modal Logics over Special Frames
Hinterlegungsdatum: 16 Dez 2018 20:55
Letzte Änderung: 16 Dez 2018 20:55
PPN:
Referenten: Otto, Prof. Dr. Martin ; Dawar, Prof. Dr. Anuj ; Blumensath, Prof. Dr. Achim
Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: 22 November 2018
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen