Vincenzo Ciancia ; Diego Latella ; Michele Loreti ; Mieke Massink - Model Checking Spatial Logics for Closure Spaces

lmcs:2067 - Logical Methods in Computer Science, April 27, 2017, Volume 12, Issue 4 - https://doi.org/10.2168/LMCS-12(4:2)2016
Model Checking Spatial Logics for Closure Spaces

Authors: Vincenzo Ciancia ; Diego Latella ; Michele Loreti ORCID-iD; Mieke Massink ORCID-iD

    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.


    Volume: Volume 12, Issue 4
    Published on: April 27, 2017
    Accepted on: October 11, 2016
    Submitted on: February 8, 2016
    Keywords: Computer Science - Logic in Computer Science,D.2.4,F.3.1,F.3.2
    Fundings :
      Source : OpenAIRE Research Graph
    • A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours; Funder: European Commission; Code: 600708

    Linked data

    Source : ScholeXplorer IsCitedBy ARXIV 2007.01266
    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.mfcs.2020.66
    Source : ScholeXplorer IsCitedBy DOI 10.48550/arxiv.2007.01266
    • 10.48550/arxiv.2007.01266
    • 10.4230/lipics.mfcs.2020.66
    • 2007.01266
    Analysing Spatial Properties on Neighbourhood Spaces
    Linker, Sven ; Papacchini, Fabio ; Sevegnani, Michele ;

    15 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 1408 times.
    This article's PDF has been downloaded 828 times.