Time-critical systems must satisfy temporal constraints whose correctness depends not only on event ordering but also on precise timing. Metric Interval Temporal Logic (MITL) provides a formalism to express such requirements. Although robustness has been widely studied under signal-based interpretations, it remains largely unexplored for point-based semantics, where executions are sequences of timestamped facts. In this setting, small timing variations may arbitrarily change Boolean satisfaction, revealing the instability of temporal truth under uncertainty. We introduce a notion of time robustness for MITL over point-based semantics, interpreting robustness as a margin of validity of temporal interpretations. We define a quantitative semantics and prove soundness with respect to Boolean satisfaction together with a Lipschitz stability property with respect to timestamp perturbations, which induces a metric notion of proximity between interpretations. The semantics admits a polynomial-time evaluation procedure and is illustrated on two case studies (drone surveillance and smart hospital), where robustness empirically correlates with tolerance to temporal noise.

Modern cyber-physical systems (CPS) can consist of various networked components and agents interacting and communicating with each other. In the context of spatially distributed CPS, these connections can be dynamically dependent on the spatial configuration of the various components and agents. In these settings, robust monitoring of the distributed components is vital to ensuring complex behaviors are achieved, and safety properties are maintained. To this end, we look at defining the automaton semantics for the Spatio-Temporal Reach and Escape Logic (STREL), a formal logic designed to express and monitor spatio-temporal requirements over mobile, spatially distributed CPS. Specifically, STREL reasons about spatio-temporal behavior over dynamic weighted graphs. While STREL is endowed with well defined qualitative and quantitative semantics, in this paper, we propose a novel construction of (weighted) alternating finite automata from STREL specifications that efficiently encodes these semantics. Moreover, we demonstrate how this automaton semantics can be used to perform both, offline and online monitoring for STREL specifications using a simulated drone swarm environment.

Abstract We present MoonLight, a tool for monitoring temporal and spatio-temporal properties of mobile, spatially distributed, and interacting entities such as biological and cyber-physical systems. In MoonLight the space is represented as a weighted graph describing the topological configuration in which the single entities are arranged. Both nodes and edges have attributes modeling physical quantities and logical states of the system evolving in time. MoonLight is implemented in Java and supports the monitoring of Spatio-Temporal Reach and Escape Logic (STREL). MoonLight can be used as a standalone command line tool, such as Java API, or via Matlab™ and Python interfaces. We provide here the description of the tool, its interfaces, and its scripting language using a sensor network and a bike sharing example. We evaluate the tool performances both by comparing it with other tools specialized in monitoring only temporal properties and by monitoring spatio-temporal requirements considering different sizes of dynamical and spatial graphs.