Specifying and Verifying Properties of Space - Extended Version
Vincenzo Ciancia, Diego Latella, Michele Loreti, Mieke Massink

TL;DR
This paper introduces a new logical framework and model checking approach for verifying properties of systems that depend on physical space, addressing a gap in traditional temporal verification methods.
Contribution
It develops a topologically-inspired logic for spatial properties, extending to discrete structures and including a novel spatial until operator, with an implemented model checking tool.
Findings
The logic effectively captures spatial properties in various structures.
The model checking procedure is efficient and practically implementable.
The framework broadens verification techniques to include spatial aspects.
Abstract
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, more generally, when dealing with systems distributed in physical space. Traditional verification techniques are well suited to analyse the temporal evolution of programs; properties of space are typically not explicitly taken into account. We propose a methodology to verify 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 a more general setting, also encompassing discrete, graph-based structures. We further extend the framework with a spatial until operator, and…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDigital Image Processing Techniques · Parallel Computing and Optimization Techniques
