Abstract
| Language | English |
|---|---|
| Title of host publication | Proceedings of the Seventh International Symposium on Games, Automata, Logics, and Formal Verification |
| Editors | Domenico Cantone, Giorgio Delzanno |
| Pages | 1-15 |
| Number of pages | 15 |
| Publication status | Published - 13 Sep 2016 |
| Event | Seventh International Symposium on Games, Automata, Logics, and Formal Verification - University of Catania, Catania, Italy Duration: 14 Sep 2016 → 16 Sep 2016 Conference number: 7 |
Conference
| Conference | Seventh International Symposium on Games, Automata, Logics, and Formal Verification |
|---|---|
| Abbreviated title | GandALF |
| Country | Italy |
| City | Catania |
| Period | 14/09/16 → 16/09/16 |
Fingerprint
Keywords
- modal logic
- topology
- modal fixpoint logic
- graph games
Cite this
}
Games for topological fixpoint logic. / Bezhanishvili, Nick; Kupke, Clemens.
Proceedings of the Seventh International Symposium on Games, Automata, Logics, and Formal Verification. ed. / Domenico Cantone; Giorgio Delzanno. 2016. p. 1-15.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book
TY - GEN
T1 - Games for topological fixpoint logic
AU - Bezhanishvili, Nick
AU - Kupke, Clemens
PY - 2016/9/13
Y1 - 2016/9/13
N2 - Topological fixpoint logics are a family of logics that admits topological models and where the fixpoint operators are defined with respect to the topological interpretations. Here we consider a topological fixpoint logic for relational structures based on Stone spaces, where the fixpoint operators are interpreted via clopen sets. We develop a game-theoretic semantics for this logic. First we introduce games characterising clopen fixpoints of monotone operators on Stone spaces. These fixpoint games allow us to characterise the semantics for our topological fixpoint logic using a two-player graph game. Adequacy of this game is the main result of our paper. Finally, we define bisimulations for the topological structures under consideration and use our game semantics to prove that the truth of a formula of our topological fixpoint logic is bisimulation-invariant.
AB - Topological fixpoint logics are a family of logics that admits topological models and where the fixpoint operators are defined with respect to the topological interpretations. Here we consider a topological fixpoint logic for relational structures based on Stone spaces, where the fixpoint operators are interpreted via clopen sets. We develop a game-theoretic semantics for this logic. First we introduce games characterising clopen fixpoints of monotone operators on Stone spaces. These fixpoint games allow us to characterise the semantics for our topological fixpoint logic using a two-player graph game. Adequacy of this game is the main result of our paper. Finally, we define bisimulations for the topological structures under consideration and use our game semantics to prove that the truth of a formula of our topological fixpoint logic is bisimulation-invariant.
KW - modal logic
KW - topology
KW - modal fixpoint logic
KW - graph games
UR - http://gandalf2016.dmi.unict.it/
M3 - Conference contribution book
SP - 1
EP - 15
BT - Proceedings of the Seventh International Symposium on Games, Automata, Logics, and Formal Verification
A2 - Cantone, Domenico
A2 - Delzanno, Giorgio
ER -