Verification Series

Notions of Bisimulations on Neighbourhood Spaces

3rd March 2020, 11:00 add to calender
Sven Linker

Abstract

The logic SLCS (Spatial Logic on Closure Spaces) is a modal logic, which is defined with a generalisation of topological spaces as its semantics. These spaces, which we will call "neighbourhood spaces" comprise, e.g., all topological spaces. Additionally, graphs can also be treated as neighbourhood spaces. While a model checking algorithm for SLCS exists, the analysis of the logic itself is almost non-existing.

In this talk, I present first results towards a model theory of SLCS. To that end, I define two notions of bisimulations on neighbourhood spaces, and which operators of SLCS they preserve.
Furthermore, I compare these bisimulations with the standard definition of modal and converse bisimulations on graphical models, as well as with topological bisimulation.

The results presented are joint work with Fabio Papacchini and Michele Sevegnani.
add to calender (including abstract)