| Summary: | 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.
|
|---|