Canavoi, Felix (2018)
Cayley Structures and the Expressiveness of Common Knowledge Logic.
Technische Universität Darmstadt
Ph.D. Thesis, Primary publication
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.
Item Type: | Ph.D. Thesis | ||||
---|---|---|---|---|---|
Erschienen: | 2018 | ||||
Creators: | Canavoi, Felix | ||||
Type of entry: | Primary publication | ||||
Title: | Cayley Structures and the Expressiveness of Common Knowledge Logic | ||||
Language: | English | ||||
Referees: | Otto, Prof. Dr. Martin ; Dawar, Prof. Dr. Anuj ; Blumensath, Prof. Dr. Achim | ||||
Date: | 2018 | ||||
Place of Publication: | Darmstadt | ||||
Refereed: | 22 November 2018 | ||||
URL / URN: | https://tuprints.ulb.tu-darmstadt.de/8269 | ||||
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. |
||||
Alternative Abstract: |
|
||||
URN: | urn:nbn:de:tuda-tuprints-82696 | ||||
Classification DDC: | 500 Science and mathematics > 510 Mathematics | ||||
Divisions: | 04 Department of Mathematics 04 Department of Mathematics > Logic 04 Department of Mathematics > Logic > Algorithmic Model Theory 04 Department of Mathematics > Logic > Algorithmic Model Theory > Model Constructions and Model-Theoretic Games in Special Classes of Structures 04 Department of Mathematics > Logic > Algorithmic Model Theory > Model Constructions and Model-Theoretic Games in Special Classes of Structures > Model Theory of Modal Logics over Special Frames |
||||
Date Deposited: | 16 Dec 2018 20:55 | ||||
Last Modified: | 16 Dec 2018 20:55 | ||||
PPN: | |||||
Referees: | Otto, Prof. Dr. Martin ; Dawar, Prof. Dr. Anuj ; Blumensath, Prof. Dr. Achim | ||||
Refereed / Verteidigung / mdl. Prüfung: | 22 November 2018 | ||||
Export: | |||||
Suche nach Titel in: | TUfind oder in Google |
Send an inquiry |
Options (only for editors)
Show editorial Details |