  Cyber-Physical Systems~(CPS) consist of collaborative, networked and tightly
intertwined computational (logical) and physical components, each operating at
different spatial and temporal scales. Hence, the spatial and temporal
requirements play an essential role for their correct and safe execution.
Furthermore, the local interactions among the system components result in
global spatio-temporal emergent behaviors often impossible to predict at the
design time. In this work, we pursue a complementary approach by introducing
STREL a novel spatio-temporal logic that enables the specification of
spatio-temporal requirements and their monitoring over the execution of mobile
and spatially distributed CPS. Our logic extends the Signal Temporal Logic with
two novel spatial operators reach and escape from which is possible to derive
other spatial modalities such as everywhere, somewhere and surround. These
operators enable a monitoring procedure where the satisfaction of the property
at each location depends only on the satisfaction of its neighbours, opening
the way to future distributed online monitoring algorithms. We propose both a
qualitative and quantitative semantics based on constraint semirings, an
algebraic structure suitable for constraint satisfaction and optimisation. We
prove that, for a subclass of models, all the spatial properties expressed with
reach and escape, using euclidean distance, satisfy all the model
transformations using rotation, reflection and translation. Finally, we provide
an offline monitoring algorithm for STREL and, to demonstrate the feasibility
of our approach, we show its application using the monitoring of a simulated
mobile ad-hoc sensor network as running example.
