Specifying and Verifying Properties of Space

DOI10.1007/978-3-662-44602-7_18MaRDI QIDQ3190163zbMATH OpenOpenAlexWikidataFDO

Authors Vincenzo Ciancia, Michele Loreti, Diego Latella, Mieke Massink

Publication date 15 September 2014

Published in Advanced Information Systems Engineering (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1406.6393

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

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 define an efficient model checking procedure, implemented in a proof-of-concept tool.

Recommendations

• Proofs of space
• Specification property for topological spaces
• Specification properties on uniform spaces
• Noetherian Spaces in Verification
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Spatial logic and spatial model checking for closure spaces
• Axiomatizing discrete spatial relations

Cited in

(16)

• Spatial logic and spatial model checking for closure spaces
• Model checking spatial logics for closure spaces
• scientific article; zbMATH DE number 4060071 (Why is no real title available?)
• Qualitative and quantitative monitoring of spatio-temporal properties with SSTL
• A logic for monitoring dynamic networks of spatially-distributed cyber-physical systems
• Geometric Model Checking of Continuous Space
• Conditional bigraphs
• 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}
• A spatial logic with time and quantifiers
• Analysis of spatio-temporal properties of stochastic systems using TSTL
• Weak simplicial bisimilarity and minimisation for polyhedral model checking
• Programming distributed collective processes in the exchange calculus
• On bisimilarity for quasi-discrete closure spaces

This page was built for publication: Specifying and Verifying Properties of Space

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3190163)