L. Nenzi ; E. Bartocci ; L. Bortolussi ; M. Loreti - A Logic for Monitoring Dynamic Networks of Spatially-distributed Cyber-Physical Systems

lmcs:7505 - Logical Methods in Computer Science, January 7, 2022, Volume 18, Issue 1 - https://doi.org/10.46298/lmcs-18(1:4)2022
A Logic for Monitoring Dynamic Networks of Spatially-distributed Cyber-Physical SystemsArticle

Authors: L. Nenzi ; E. Bartocci ; L. Bortolussi ; M. Loreti

    Cyber-Physical Systems (CPS) consist of inter-wined computational (cyber) and physical components interacting through sensors and/or actuators. Computational elements are networked at every scale and can communicate with each other and with humans. Nodes can join and leave the network at any time or they can move to different spatial locations. In this scenario, monitoring spatial and temporal properties plays a key role in the understanding of how complex behaviors can emerge from local and dynamic interactions. We revisit here the Spatio-Temporal Reach and Escape Logic (STREL), a logic-based formal language designed to express and monitor spatio-temporal requirements over the execution of mobile and spatially distributed CPS. STREL considers the physical space in which CPS entities (nodes of the graph) are arranged as a weighted graph representing their dynamic topological configuration. Both nodes and edges include attributes modeling physical and logical quantities that can evolve over time. STREL combines the Signal Temporal Logic with two spatial modalities reach and escape that operate over the weighted graph. From these basic operators, we can derive other important spatial modalities such as everywhere, somewhere and surround. We propose both qualitative and quantitative semantics based on constraint semiring algebraic structure. We provide an offline monitoring algorithm for STREL and we show the feasibility of our approach with the application to two case studies: monitoring spatio-temporal requirements over a simulated mobile ad-hoc sensor network and a simulated epidemic spreading model for COVID19.


    Volume: Volume 18, Issue 1
    Published on: January 7, 2022
    Accepted on: October 2, 2021
    Submitted on: May 25, 2021
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Logical Methods in Computer Science; Code: W 1255

    6 Documents citing this article

    Consultation statistics

    This page has been seen 2133 times.
    This article's PDF has been downloaded 1210 times.