Games for topological fixpoint logic

Nick Bezhanishvili, Clemens Kupke

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

1 Citation (Scopus)

Abstract

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.
LanguageEnglish
Title of host publicationProceedings of the Seventh International Symposium on Games, Automata, Logics, and Formal Verification
EditorsDomenico Cantone, Giorgio Delzanno
Pages1-15
Number of pages15
Publication statusPublished - 13 Sep 2016
EventSeventh International Symposium on Games, Automata, Logics, and Formal Verification - University of Catania, Catania, Italy
Duration: 14 Sep 201616 Sep 2016
Conference number: 7

Conference

ConferenceSeventh International Symposium on Games, Automata, Logics, and Formal Verification
Abbreviated titleGandALF
CountryItaly
CityCatania
Period14/09/1616/09/16

Fingerprint

Fixpoint
Game
Logic
Stone Space
Bisimulation
Game Semantics
Monotone Operator
Topological Structure
Operator
Invariant
Graph in graph theory

Keywords

  • modal logic
  • topology
  • modal fixpoint logic
  • graph games

Cite this

Bezhanishvili, N., & Kupke, C. (2016). Games for topological fixpoint logic. In D. Cantone, & G. Delzanno (Eds.), Proceedings of the Seventh International Symposium on Games, Automata, Logics, and Formal Verification (pp. 1-15)
Bezhanishvili, Nick ; Kupke, Clemens. / Games for topological fixpoint logic. Proceedings of the Seventh International Symposium on Games, Automata, Logics, and Formal Verification. editor / Domenico Cantone ; Giorgio Delzanno. 2016. pp. 1-15
@inproceedings{4c012c378f4649438504b9808371bfe2,
title = "Games for topological fixpoint logic",
abstract = "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.",
keywords = "modal logic, topology, modal fixpoint logic, graph games",
author = "Nick Bezhanishvili and Clemens Kupke",
year = "2016",
month = "9",
day = "13",
language = "English",
pages = "1--15",
editor = "Domenico Cantone and Giorgio Delzanno",
booktitle = "Proceedings of the Seventh International Symposium on Games, Automata, Logics, and Formal Verification",

}

Bezhanishvili, N & Kupke, C 2016, Games for topological fixpoint logic. in D Cantone & G Delzanno (eds), Proceedings of the Seventh International Symposium on Games, Automata, Logics, and Formal Verification. pp. 1-15, Seventh International Symposium on Games, Automata, Logics, and Formal Verification, Catania, Italy, 14/09/16.

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 proceedingConference 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 -

Bezhanishvili N, Kupke C. Games for topological fixpoint logic. In Cantone D, Delzanno G, editors, Proceedings of the Seventh International Symposium on Games, Automata, Logics, and Formal Verification. 2016. p. 1-15