Model checking spatial logics for closure spaces
From MaRDI portal
Logic in computer science (03B70) Topological spaces and generalizations (closure spaces, etc.) (54A05) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Abstract: 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 space. Traditional formal verification techniques are well suited to analyse the temporal evolution of programs; however, properties of space are typically not taken into account explicitly. We present a topology-based approach to formal verification of spatial properties depending upon physical space. We define an appropriate logic, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. We lift the topological definitions to the more general setting of closure spaces, also encompassing discrete, graph-based structures. We extend the framework with a spatial surrounded operator, a propagation operator and with some collective operators. The latter are interpreted over arbitrary sets of points instead of individual points in space. We define efficient model checking procedures, both for the individual and the collective spatial fragments of the logic and provide a proof-of-concept tool.
Recommendations
Cited in
(13)- Expressing discrete spatial relations under granularity
- Spatial logic and spatial model checking for closure spaces
- Qualitative and quantitative monitoring of spatio-temporal properties with SSTL
- Geometric Model Checking of Continuous Space
- Analysing Spatial Properties on Neighbourhood Spaces
- A Spatial Logic for Simplicial Models
- Back-and-forth in space: on logics and bisimilarity in closure spaces
- Minimisation of spatial models using branching bisimilarity
- On bisimilarity for polyhedral models and \texttt{SLCS}
- Weak simplicial bisimilarity and minimisation for polyhedral model checking
- Programming distributed collective processes in the exchange calculus
- On bisimilarity for quasi-discrete closure spaces
- \textsc{MacroSwarm}: a field-based compositional framework for swarm programming
This page was built for publication: Model checking spatial logics for closure spaces
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2974786)
