The setting
Modern cyber-physical systems (CPS) are often made of many networked components and agents that interact and communicate. In spatially distributed CPS, these connections can change with the spatial configuration of the agents. Robust monitoring of the distributed components is essential to make sure complex behaviours are achieved and safety properties hold.
The contribution
The paper defines an automaton semantics for the Spatio-Temporal Reach and Escape Logic (STREL), a formal logic for expressing and monitoring spatio-temporal requirements over mobile, spatially distributed CPS, reasoning on dynamic weighted graphs.
STREL already has well-defined qualitative and quantitative semantics; this work proposes a new construction based on alternating finite automata to monitor it.