Games for Topological Fixpoint Logic

TL;DR

This paper introduces a game-theoretic semantics for a topological fixpoint logic based on Stone spaces, demonstrating bisimulation invariance and providing a novel way to interpret fixpoints in topological models.

Contribution

It develops a game semantics for topological fixpoint logic on Stone spaces, establishing bisimulation invariance and characterizing fixpoints via clopen sets.

Findings

Game semantics characterizes fixpoints on Stone spaces.

Bisimulation invariance of the logic is proven.

Adequacy of the game semantics is established.

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.