Weak Simplicial Bisimilarity for Polyhedral Models and SLCS_eta -- Extended Version
In the context of spatial logics and spatial model checking for polyhedral models -- mathematical basis for visualisations in continuous space -- we propose a weakening of simplicial bisimilarity....
On Bisimilarity for Quasi-discrete Closure Spaces
Closure spaces, a generalisation of topological spaces, have shown to be a convenient theoretical framework for spatial model checking. The closure operator of closure spaces and quasi-discrete...
Geometric Model Checking of Continuous Space
Topological Spatial Model Checking is a recent paradigm where model checking techniques are developed for the topological interpretation of Modal Logic. The Spatial Logic of Closure Spaces, SLCS,...
Towards Spatial Bisimilarity for Closure Models: Logical and Coalgebraic Characterisations
The topological interpretation of modal logics provides descriptive languages and proof systems for reasoning about points of topological spaces. Recent work has been devoted to model checking of...
On Bisimilarities for Closure Spaces - Preliminary Version
Closure spaces are a generalisation of topological spaces obtained by removing the idempotence requirement on the closure operator. We adapt the standard notion of bisimilarity for topological...
Refined Mean Field Analysis of the Gossip Shuffle Protocol -- extended version --
Gossip protocols form the basis of many smart collective adaptive systems. They are a class of fully decentralised, simple but robust protocols for the distribution of information throughout large...
Using Spatial Logic and Model Checking for Nevus Segmentation
Spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems and signal and image analysis. In the latter domain,...
Model Checking Spatial Logics for Closure Spaces
Spatial aspects of computation are becoming increasingly relevant in Computer Science, especially in the field of collective adaptive systems and when dealing with systems distributed in physical...
VoxLogicA: a Spatial Model Checker for Declarative Image Analysis (Extended Version)
Spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems and signal and image analysis. We explore a new domain,...
Specifying and Verifying Properties of Space - Extended Version
The interplay between process behaviour and spatial aspects of computation has become more and more relevant in Computer Science, especially in the field of collective adaptive systems, but also,...
On-the-fly Fast Mean-Field Model-Checking: Extended Version
A novel, scalable, on-the-fly model-checking procedure is presented to verify bounded PCTL properties of selected individuals in the context of very large systems of independent interacting...