Online Monitoring of Spatio-Temporal Properties for Imprecise Signals

From biological systems to cyber-physical systems, monitoring the behavior of such dynamical systems often requires to reason about complex spatio-temporal properties of physical and/or computational entities that are dynamically interconnected and arranged in a particular spatial configuration. Spatio-Temporal Reach and Escape Logic (STREL) is a recent logic-based formal language designed to specify and to reason about spatio-temporal properties. STREL considers each system's entity as a node of a dynamic weighted graph representing their spatial arrangement. Each node generates a set of mixed-analog signals describing the evolution over time of computational and physical quantities characterising the node's behavior. While there are offline algorithms available for monitoring STREL specifications over logged simulation traces, here we investigate for the first time an online algorithm enabling the runtime verification during the system's execution or simulation. Our approach extends the original framework by considering imprecise signals and by enhancing the logics' semantics with the possibility to express partial guarantees about the conformance of the system's behavior with its specification. Finally, we demonstrate our approach in a real-world environmental monitoring case study.


INTRODUCTION
Complex emergent spatio-temporal patterns such as traffic congestion or travelling waves are central in the understanding of networked dynamical systems where locally interacting entities are operating at different time and spatial scales. We can observe these patterns both in biological systems [3,5,11] as well as human engineered artefacts such as Collective Adaptive Systems [22] (CAS) and Cyber-Physical Systems [31] (CPS). CAS and CPS consist of a large number of heterogeneous (physical and computational in CPS) and spatially distributed entities featuring complex interactions among themselves, with humans and other systems. Example include biking sharing systems, the internet of things, contact tracing devices preventing the epidemic spread, vehicular networks and smart cities. Many of these systems are also safety-critical [31], meaning that a failure could result in loss of life or in catastrophic consequences for the environment.
The complex interaction with the physical environment in which these systems are embedded prevents them from being exhaustively verified at design time. A common alternative is testing [4]: traces generated during their execution/simulation are stored and monitored offline with respect to a formal specification used as an oracle. However, testing may provide a limited coverage and does not take into account physical failures that may happen during the execution. Online monitoring is instead a preferable solution when the monitoring verdict requires the immediate action of a policy maker during the system's execution or when it is very computationally expensive [32] generating and storing the system's execution traces to be monitored offline. Motivating example. As a case study we consider a sensor network for environmental monitoring. Air pollution is the primary cause of the loss of biodiversity, of the reduction of agricultural productivity and of many diseases for humans' lungs and cardiovascular system. Policy makers are constantly monitoring the amount of 2 , an air pollutant that forms from the combustion of fossil fuels, to activate special policies that mitigate its release when levels grow too significantly for the public concern. For example, in the Italian region of Lombardy, there are over 80 stations distributed throughout the region monitoring the level of 2 in the air.  [20] in terms of / 3 . Red crosses and dotted line represent missing values. Data from the open data initiative of ARPA Lombardia [21].
the location of these stations, and the value reported in the town of Rezzato, for the first quarter of 2021. The measurements happen regularly every hour, but sometimes the sensors fail to communicate the measurements, because of meteorological issues, or temporary faults, and the actual values are provided later on. Furthermore, the values measured by the sensors are noisy and they have a certain degree of uncertainty. Another way to deal with the missing values, could be to check that nearby locations (e.g. within 10 Km) do not register alarming values of particles in the air and this is possible only if we consider spatio-temporal properties.
In this paper we address the problem of online monitoring of spatio-temporal properties over systems from which we can observe noisy signals with possible missing data or out-of-order samples. Spatio-temporal monitoring. In the last decade there has been a great effort to develop logic-based specification languages and monitoring frameworks for spatio-temporal properties. Examples include SpaTeL [12], SSTL [29], (SaSTL) [23,24] and STREL [1]. For more details on the underlying spatial models and the language expressiveness we refer the reader to [28]. In this paper, we consider STREL [1] a spatio-temporal logic operating over a dynamic weighted graph representing the spatial arrangement of spatially distributed entities. Each node generates a set of mixed-analog signals describing the evolution over time of computational and physical quantities characterising the node's behavior. STREL extends the Signal Temporal Logic (STL) [25] with the reach and escape operators that generalizes the somewhere, everywhere and surronded spatial modalities, simplifying the monitoring that can be computed locally with respect to each node. However, the original work on STREL [1,2] provides only an offline monitoring algorithm. In contrast we present here the first online monitoring algorithm for STREL and in general for spatio-temporal monitoring.
Online Monitoring. To the best of our knowledge, the only online monitoring techniques [7,8,14,15,26,27,30] that are available in the literature can handle temporal specification languages such as STL [25] and Metric Temporal Logic [17] (MTL). One of the main challenges for online monitoring is how and when to decide the satisfaction/violation of a formula with temporal operators reasoning about future and not yet observed events. In [8] the authors provides, for the first time, a dynamic programming algorithm for the online monitoring of the robustness metric of MTL formulas with bounded future and unbounded past. The past formula is used to reason about the robustness of the actual system observations, while for evaluating the future formula they use a predictor to estimate the likely robustness. However, the value forecasted by the predictor needs to be trusted because it is not the real value that the system will provide. Other approaches [14,15,30] address the problem of deciding about the future using a technique called pastification that rewrites the future operators as past ones and delays the verdict. Similarly the works of Mamouras et al [26,27] delay the output verdict until some part of the future input is seen. In [7] the authors present an efficient online algorithm to compute the robust interval semantics for bounded horizon formulas. All these approaches assume that the data and the events to be observed come synchronously and in-order. Our contribution In contrast to these works, we present a novel approach to monitor online imprecise spatio-temporal signals (signals are defined on intervals, not just the robustness) where the samples can be processed also out-of-order. The notion of an interval is instrumental when representing partial knowledge about a value that is at least known to be within some boundaries. This might be because of errors in the measurement, or maybe because of some other sources of uncertainty throughout the process of acquiring and processing them. We define both a Boolean and a quantitative interval semantics for STREL and we prove the soundness and the correctness of the robust interval semantics. We design and implement, as extensions to the Moonlight tool 1 , the first online monitoring algorithm for not-in-order sampled signals, and the first online spatio-temporal monitoring tool. Our experiments demonstrate also convincing performances comparing with the state-of-the-art tool BREACH [9] for the online monitoring of temporal properties over in-order sampled signals.
Paper organization The rest of this paper is structured as follows. We provide the important aspects of interval algebra and our notion of imprecise signals in Section 2. In Section 3 we introduce the interval extension of the STREL logic, and its primary results, while in Section 4 we present our approach for the online monitoring of imprecise signals. Lastly, we present a realistic use case in Section 5 and we share our concluding remarks in Section 6.

INTERVAL ALGEBRA, SIGNALS AND SPATIAL MODEL
In this section, we define the key elements of interval algebra, signal and spatial model, which will be useful to characterize samples of the kind depicted in Figure 1. In addition to the classical notion of interval, it is useful to recall some basic operations that can be performed.
Definition 2.4 (Hausdorff Distance). Let , be two non-empty subsets of a metric space ⟨ , ⟩, we will call (Hausdorff) distance the function : P ( ) × P ( ) → R ≥0 defined as In practice, in our context, we can just consider the metric space defined by the euclidean distance over the real numbers, and thus reduces to computing max(| 1 − 2 |, | 1 − 2 |) for any two 1 , 2 ∈ I (R ∞ ), although for doing that we say, by definition, that if both 1 , 2 (or both 1 , 2 ) are infinite, then their Hausdorff distance is 0.
Now we have all the tools to introduce the concept of imprecise signals.
Definition 2.5 (Imprecise Temporal Signal). Let T ≡ [0, ∞] be a set representing the time domain, and let F (T, ), with ⊆ I (R) for a fixed ∈ N, be the family of functions over Cartesian products of real intervals; we call imprecise time signal, any ∈ F (T, ), i.e. any function : T → It is convenient, in some cases, to slice the signals based on the domain of interest, for that reason, we recall the concept of (signal) projection.
To represent a set of signals distributed in the space, we introduce the following definition. . We can naturally describe the distance between spatio-temporal signals by considering the Hausdorff distance from Definition 2.4 over all possible locations of the space, and time instants. Definition 2.8 (Spatio-Temporal Signal Distance). Let s 1 , s 2 ∈ F (L, T, ), we will call signal distance the largest Hausdorff distance over space and time, defined as: To describe the interplay of signals in different locations, we need to encompass the information related to the spatial distribution of the locations. Definition 2.9 (Spatial model). We call spatial model the tuple S = ⟨L, ⟩ 3 , where L is a set of locations and ⊆ L × R ∞ ≥0 × L is a proximity function associating at most one label ∈ R ∞ ≥0 to each distinct pair ℓ 1 , ℓ 2 ∈ L An obvious spatial model for the region of Figure 1 is a graph where every location is connected to all the others, and the proximity function is defined by labels corresponding to the minimal aerial distance between each pair of locations. Finally to consider distance on paths of locations we introduce the notion of routes over the spatial model. Definition 2.10 (Routes). A route on S is a (potentially infinite) sequence ℓ 0 , ℓ 1 , . . . ℓ . . . , such that for any ℓ , ℓ +1 ∈ , there is a label (ℓ , , ℓ +1 ) ∈ . We indicate by Λ(ℓ) the set of routes on S starting at ℓ. Moreover, we will use [ ] to denote the -th node of the route, [ . . . ] to denote the subroute starting at the -th node, and (ℓ ) to denote the first occurrence of ℓ in . Lastly, we will indicate by ℓ 1 < (ℓ 2 ) the fact that ℓ 1 precedes ℓ 2 in the route .
Routes have the same intuitive meaning as they have in the physical world, and, similarly to the real world, we can define the concept of route (or travel) distance, as the aggregated sum of all the labels traversed by the route.
Lastly, routes allow us to conveniently define the distance between any two locations ℓ 1 , ℓ 2 ∈ L, whichever the spatial model being considered. In fact, from the location ℓ 1 to ℓ 2 , one can consider the minimal distance among all the routes starting at ℓ 1 and ending in ℓ 2 :

STREL WITH INTERVAL SEMANTICS
We present in this section an interval semantics that allows for a conservative analysis that considers both the minimum and the maximum values of intervals. This way, a plethora of use scenarios can fit into this specification language, spanning from traditional offline monitoring of a given specification over imprecise signals to online monitoring with out-of-order updates. All the proofs of theorems and lemmas are reported in appendix.
Definition 3.1 (STREL Syntax). We consider logical formulae belonging to the language L generated by the following BNF grammar: where • ∈ {>, <}, ∈ R, is associated to a projection function of Definition 2.6, i.e. • are inequalities on the variables of the systems. U is the until temporal operator, with real interval, while R ≤ and E ≥ are the spatial operators reach and escape , with ∈ R >0 . In addition, we have the derived Boolean operators as and (∧) and implies (→), temporal operators eventually (F ) and globally (G ), and spatial operators somewhere ( ≤ ) and everywhere ( ≤ ).
Considering again the air pollution case study, current regulation in Lombardy requires to take action when the level of nitrogen dioxide ( 2 ) exceeds the threshold of 400 / 3 for more than three hours. Let 2 < 400 denote the atomic proposition that states that the level of nitrogen dioxide is lower than 400 / 3 . A requirement as the previous one could be expressed like in (1): Temporal operators like F specify properties on the dynamic evolution of the system. In fact, when (1) is violated, the alerting procedure could be triggered, to inform the citizens about the danger. However, since it is known that noise and local faults frequently happen, one could consider of alerting the population also when the close neighbourhood (e.g. within 10 Km) exhibits a similar phenomenon. For this aim, a property like (2) can be monitored.
Spatial operators like instead specify properties related to the spatial configuration, and in this context, the exact meaning is that at least a location in a range of less than 10 km must have a level of nitrogen dioxide lower than 400 / 3 . We will see other examples of the logic language in the next sections. For a more detailed description of the logic, we refer the reader to [1]. We present now the Boolean and quantitative interval semantics for STREL.
This is a three-valued semantics, which is equal to 1 if the interval signal (s, ℓ, , ) satisfies , −1 if the formula is not satisfied, and 0 if we cannot answer. The semantics is directly derived from the standard Boolean semantics and the interval algebra described in the previous section. For atomic proposition (s, ℓ, , • ) = 1 iff the inequality (s(ℓ, )) • is true. This means, e.g., (s, ℓ, , 2 > 400) = 1 iff 2 , the left extreme of the projected signal 2 , is greater than 400. (s, ℓ, , 2 > 400) = −1 if the right extreme is less than 400, and (s, ℓ, , 2 > 400) = 0 otherwise, so if 400 ∈ 2 interval value. Similar calculation can be done for the other combination of • and .
The three-valued Boolean semantics can be sufficient in applications where the interest is only whether or not the specification is satisfied. However, in many complex cases, one might be interested in getting some insights about the degree by which a property is satisfied or violated. In the following, we introduce an extension of the quantitative semantics that provides numerical bounds to the robustness degree of a specification.
We will indicate with : L × T → I (R ∞ ) the robustness signal, i.e. the signal generated by the partial application of the function to a given formula and a given signal s, so that (ℓ, ) ≡ (s, ℓ, , ).
Note that without the interval semantics we have defined, missing values should be substituted by some values that approximate the actual value (e.g. by linear interpolation), and therefore only approximate the actual value of satisfaction or robustness of a given property at that specific time point. Conversely, by exploiting the interval semantics, one could actually get upper/lower bounds at those points, which can actually be sufficient in real-world applications. To provide the correctness of the interval semantics over imprecise signals, we introduce the following lemma: . For any ∈ T, for any ℓ ∈ L, for any ∈ L, for any > 0, we have: PROOF. See the extended version of this article for the proof. □

ONLINE MONITORING
In this section a novel online (out-of-order) monitoring algorithm for STREL is presented. Differently from the standard offline approach, where all the data is available at the beginning of the execution, online monitoring is performed incrementally, when a new piece of data is available. In this case, the uncertainty related to the absence of information must be taken into account. For that aim, the machinery of imprecise signals can be exploited to represent the uncertainty, where the result of the monitoring process, whether it is a satisfaction or a robustness signal, is refined as soon as new updates of the input arrive.
The semantics for STREL is defined for arbitrary signals, but algorithms, for computational reason, are provided for piecewise constant ones, along the lines of [1,7]. This class of signals is convenient, and frequently chosen as the class of reference for a number of reasons: (i) it naturally describes digital signals, (ii) it can be stored in memory very efficiently, and processed fast enough to be considered for real-time applications, (iii) it allows to express the vast majority of real-valued signals of practical use with a limited loss of information. Since the presented signals are Lipschitz-continuous (we consider only inequalities on the variables of the system), we can always bound our error, considering the minimum time step and the maximum of their individual Lipschitz constants. An imprecise piecewise-constant signal : T → I (R ∞ ), can be characterized in the following way: , for ≤ < ∞ and graphically represented as in Figure 2. Note that frequently when monitoring real-time application the last part of the signal will be characterized by the widest interval possible, as this denotes the fact that the knowledge collected so far is insufficient for providing any insight about the monitored specification for future values of the signal. Similar infinite interval can be considered for missed values.
We consider space-synchronized (s.s.) signals, i.e. signals defined on the same time intervals for any location of the space model. More precisely, a p.c. s.s. signal : L × T → is a signal that can be represented as a sequence of pairs {( , V )} ∈N , where each pair ( , V ) of the sequence represents a piece of the signal, such that it maps any time-instant between and +1 in T, to the |L| × matrix V that represents the values of the dimensions of the signal at each location ℓ in L. The space-synchronization restriction might appear to be a severe limitation, but this shows one of the conceptual differences between online and offline monitoring: in an offline setting, the space-synchronization hypothesis would likely have detrimental effects on the performances, as it would force all the processing to happen at a temporal granularity that is the union of the temporal granularities of the signals at the different locations.
In an online setting, on the other hand, the temporal granularity is determined by the time when new information is available, and the space-synchronization hypothesis makes it possible to exploit in future work the Single-Instruction Multiple-Data (SIMD) capabilities of modern processors (see [13,18]), resulting in execution times that are virtually independent from the number of locations, when appropriate hardware is available. In this context, we call signal update u the triplet ( , , V), representing a mapping to the value matrix V for any time instant between (included) and (excluded). Signal updates can be seen as some special kinds of signals that we use to represent upcoming partial information from the online behavior of the monitored system. In the context of our analysis, we always assume updates to provide truthful information (the case of hard faults, i.e. where updates provide wrong information, will be explored in future work), and, for that reason, we can always assume updates to be well-formed, meaning that the interval V they provide is always included in the previous interval of the signal we stored for that time and location. To express the online nature of the computation we want to pursue, we need some way of describing the incremental evaluation of new information.
The refinement relation expresses the fact that s 1 and s 2 represent the same information, except that s 2 has a smaller degree of uncertainty. By the notions of signal update and signal refinement, we can easily represent the online evolution of a signal as a chain of signal refinements s 0 ≻ · · · ≻ s ≻ . . . , where the signal s +1 at the step + 1 can be computed from s and update u like in Algorithm 1. The REFINE( ) procedure takes a signal s as a sequence of ordered pairs, and an update as the triplet ( , , V). In practice, it removes all the pieces of the signal that start within the interval [ , ), and adds a piece with value V in the case and/or lay in between of and +1 . Clearly, for efficiency reasons, the algorithm can jump to the next pair each time +1 < , and can terminate as end for 14: end procedure soon as > . The updated signal at the end of the execution is the next element of the refinement chain, i.e. s +1 . The Monitoring Problem. When monitoring online a given specification , let s 0 be the signal representing the starting information on which the atoms of the formula are defined. Let also (u ) ∈N denote a (finite or infinite) sequence of signal updates. The online monitoring problem can be framed as computing the robustness signal s +1 , given s (or, alternatively, the satisfaction signal s +1 given s ), with s ≻ s +1 , starting from s 0 . A naïve implementation of an online monitor could just ignore the information coming from previous monitoring steps and restart the computation over the whole signal each time new information is available. As already noted in [7,8], such an implementation would result in huge amounts of wasted resources when monitoring time signals, and it would therefore be even more costly when monitoring space-time signals. To properly scope the effect that an out-of-order update of the input signal generates for the evaluation of a formula, it is convenient to think of updates as starting from the atoms of the monitored formula, and then propagating their effects up through the syntactic tree, generating a ripple effect where the impacted time span widens based on the operators of the subformulae. Figure 3 shows the ripple effect resulting from the propagation of update information through the syntactic tree. From this intuition we can define the update ripple function, to scope the resulting update's time span, based on the provided update, and on the operator being computed in the following way: otherwise Being able to assess the time boundaries of the effect of an update, we can therefore define an online monitoring procedure that updates the robustness (or satisfaction) signal when needed and that keeps the valid parts otherwise. In general, we have that at the step + 1, t t t t Figure 3: The ripple effect generated from the propagation of an update of the signal , over the formula the monitoring function can be evaluated as: Note that in all the cases where the updates overlap, they must be processed sequentially in order to generate correct results. Monitoring Procedure. To compute the monitoring result signal online, it is crucial to be able to exploit the knowledge from the past each time new information is available. The most natural way for doing so is to develop a stateful algorithm that stores the relevant information from previous computations. We will represent by M the persistent memory (i.e. the state) that we keep throughout the various iterations of the monitoring process, and by M [ ] the access to the item from memory. The memory M is organized around a data structure that represents the set of robustness signals of all the subformulae of the monitored formula , as computed in the last iterations. This set can be encoded as an array indexed on some ordering of the subformulae. We represent as M [ ] the access to the respective robustness signal for some formula . This data structure is extremely important to maximize the time performance of the monitoring process, as next iterations will re-compute only the differing fragments based on the update ripple. Before starting the monitoring process, the memory is initialized by storing an undefined signal for any subformula in the set of the subformulae of the formula being monitored. We call undefined signal the special signal : L × T → [−∞, +∞], which represents the total absence of knowledge about the value, at any possible time instant.
Once the memory is initialized, the monitoring can start. We assume that the signal is always received as a sequence of signal updates u , starting from = 0, where the input signal is considered to be undefined. Algorithm 2 represents the base routine triggered when receiving an update u of the input signal. The recursive procedure MONITOR(M, , u) is responsible for propagating the input signal update to the subformulae and then fetching the corresponding updates of the robustness signal. We indicate by ⟨M, { }⟩ the return value of the algorithm, to mean that it returns an updated version of the memory, and a list of robustness updates of the formula that might either be used by the caller or discarded. The general procedure of Algorithm 2 calls the specific procedures of Algorithms 3-6 depending on the operators encountered while traversing the tree of the formula. Note that all of the above exploit the REFINE( ) primitive operation from Algorithm 1. Online Monitoring Of Non-temporal Operators When monitoring formulae containing Boolean or Spatial operators, the online evaluation can be performed very efficiently by simply updating the robustness signal at the times corresponding to the received update. Algorithm 3 shows the algorithm for monitoring atomic formulae, Algorithm 4 presents the one for monitoring unary operators (i.e. ¬ and E ), and Algorithm 5 shows the one for binary operators (i.e. ∨ and R ). We represent by COMPUTE_OP(OP, V) (and COM-PUTE_OP(OP, V 1 , V 2 )) the execution of the semantic operation corresponding to the operator OP, along the lines of Definitions 3.2,3.3, i.e.
[max]/[min] direct computation for Booleans, and the classical reach/escape routines [1] for spatial operators. A key difference from the offline version of the spatial algorithms, however, is that in our online version the COMPUTE_OP implementation has been crafted to enable spatial-parallelization, i.e. monitors' users with appropriate hardware and the need to speed-up for large spaces, can opt-in for the multi-threaded version of the algorithm, where COMPUTE_OP is executed in parallel for any location of the spatial model. The algorithm for monitoring binary operators is slightly more complex, as it requires to take into account the corresponding value  return ⟨M, {u 1 OP 2 }⟩ 12: end function Online Monitoring Of Temporal Operators To execute temporal operators quickly enough for online needs, on the other hand, we need to store some extra information throughout the process. Firstly, it is useful to recollect that, in general, every temporal operator can be decomposed [10] in the conjunction of two (efficiently computable) operators: • the bounded eventually F (or equivalently the bounded globally G ) • the unbounded until U We propose here an enhanced algorithm for monitoring bounded globally/eventually operators with out-of-order updates. For that aim, we slightly adapted the classical sliding window algorithm from Lemire [19] so that it is constrained on the function and that it can deal seamlessly with numerical and interval values. Algorithm 6 presents primary routine of the sliding window for computing updates of bounded unary temporal operators OP . The algorithm exploits an additional data structure W that is a deque, such that new elements of the window are added at the end, and such that when the window is saturated (i.e. the elements inside denote a time span bigger than the definition interval of the operator), they are removed from left and propagated as updates. The logic of the algorithm is essentially the following: for each update received in input, the sliding window is initialized on the fragment of the robustness signal of the subformula defined by the update ripple function . For each piece of the fragment, the sliding window is updated (line 10), and each time the new piece makes the data in the window exceed the maximum size, the sliding window slides to the right, removing from the window some elements that can be safely propagated as updates (line 8); some edge cases are not covered to keep the algorithm concise (e.g. the case when the current piece is by itself wider than the window size). The precise behaviour of SLIDE and ADD, that control the mutation of W can be examined in the extended version of the paper or in the Moonlight implementation. The second fundamental temporal algorithm is the one for computing the unbounded until. Unfortunately, being unbounded, any update might require to recompute, in the worst case, the whole robustness/satisfaction signal. In our implementation, we consider the algorithm in [7]. Note that it requires to keep the minimum value of preceding computations of 1 and the maximum value of preceding computations of the whole formula as secondary data structures. A last remark about the implementation must be made: while the algorithms have been developed with the goal to enable out-of-order execution, all of them have been implemented also in an in-order variant, so that the execution time penalty from not assuming that updates are at the end, does not affect the users of the tool, when the use case of interest allows to.

EXPERIMENTAL EVALUATION
The interval semantics we presented in Section 3 and the online (in-order and out-of-order) monitoring strategies of Section 4 have been implemented as extensions to the Moonlight tool. To showcase the kind of applications where they can be exploited, and to compare the performances with other state-of-the-art approaches, we propose here three different examples: (i) we present and discuss the results of the properties previously introduced, in the context of air quality monitoring; (ii) we compare the performances of our approach for the evaluation of a temporal property on the Abstract Fuel Control Simulink model from the Breach [9] tool; (iii) we compare the performances of the online approach versus the offline version of Moonlight on a simulated sensor network adopting the ZigBee protocol. All the computations have been executed on an Intel ® Core ™ i7-5820K CPU @ 3.30GHz, 15M cache, 6 cores (12 threads), with 32GB RAM, running Ubuntu ® 20.04.2 LTS, and Matlab ™ R2021a.

Use case: Air pollution monitoring
Recalling Properties 1, 2 from Section 3, we can see in Figure 4 the results of the monitoring. Note that when both the upper and lower bounds are below the 0 threshold, the property is certainly violated, while when only the lower bound is below 0, then the property is potentially violated. Property 1 gives some important insights on the faults observed in Figure 1. In fact, we can see that of the six observed failures for the ten-days span of interest, only three happen for a time that is long enough to potentially trigger public concern, which correspond to the spikes to minus infinity in the lower bound of Figure 4 (left). In essence, with the interval semantics we learn that the property could potentially be violated in those timespans, while it is certainly not for the other missing values. However, Property 2 tells us something more about the neighbourhood: in fact, by combining the observations registered from close location, it is apparent that just one of the failures (the one happening during March 20th) likely corresponds to a violation of the property, since there is no close location exhibiting low levels of nitrogen dioxide in Figure 4 (right).

Online comparison: Abstract Fuel Control
Consider a Simulink ® model that describes a black-box representation of an engine's air-fuel ratio controller aimed at complying to emission targets of a vehicle, where the user has direct control over the engine speed and pedal angle. Each input and output is represented as a signal that is sampled regularly, the outputs being the actual air-to-fuel ratio (AF), and the mean air-to-fuel ratio value for the given input parameters (AF ref ) at a sampling period = 0.1 . For a full description of the model, the reader can see [16], while [7] provides the reference implementation for online monitoring in Breach.
In our experiments, we monitored the following STL property (note that STREL is an extension of STL, and therefore each STL formula is also a STREL formula) = G [10,30] for different sample sizes, considering both updates as an order chain and by shuffling them at random to simulate out-of-order retrieval and processing. The result of | − | from the model has been stored in a file and loaded before starting the stopwatch for both monitors, to eliminate the simulation and loading time from the performance evaluation. Breach monitor has been measured via the reference implementation as a Simulink model, while Moonlight is implemented as a Java program. Table 1  The interesting insight of the comparison is the fact that, while our in-order implementation provides reliably faster performances (note that the offline version of Moonlight had already shown better performance than Breach in [2]), the penalty that comes from not assuming ordered inputs grows substantially with the increase of the input size, as this requires longer searches in the output signal, to find the spot where the update should be applied. Nevertheless, the biggest sample size we considered is quite extreme (ten thousand randomly-shuffled samples), yet the execution time (4.489 ms/sample on average) is way smaller than the sampling time (0.1 s), which therefore makes it reasonable for most real-time scenarios.

Moonlight comparison: ZigBee Protocol
Consider a collection of moving devices communicating via the ZigBee (IEEE 802.15.4) protocol. From the protocol description we know that the devices can have three roles: they can either be coordinators, routers or sensor-node. Each device is equipped with an humidity sensor ℎ( ) that reports at each time instant the observed value of the humidity at the current location. The humidity observed can be described as an MA(0) process, i.e.
where the observed value comes from the real value 0 , with some perturbation from the zero-mean white noise of variance 2 . Each device can communicate with the ones that are close enough directly, but they can also communicate with furthest ones, as long as there is some router between them that can bridges the communication. Let denote the true value of humidity for a given device at a given time, let denote the role of a given sensor, and some time threshold to warn the observers. We monitored the following properties on the system: 2 = <10 ( = coordinator) Property 1 denotes an alert condition: if the humidity measured by a device goes beyond 60%, then it must fall down at 30% afterwords, within the time threshold . Property 2 , on the other hand, defines a reachability criterion between the sensors: it checks whether it is true that from any location, it is possible to reach a coordinator ( = coordinator) in less than 10 hops. Similarly to previous versions of this model [1,6], we can consider the spatial model as a graph where all the devices are the nodes, and the edges between the nodes are all labeled by = 1 to denote the networking hop from one device to another. Table 2 shows the difference in monitoring 1 and 2 both online and offline. It is interesting to see how the different algorithms behave on same formula and data: in fact, the online temporal algorithms are penalized by the complexity added by the fact that some values must be recomputed. Conversely, the online spatial ones benefit from the hypothesis of spatial synchronization of the locations, resulting in a slightly more efficient computations in the case we explored. Lastly, it can be seen that the benefit of parallelization is particularly evident when the number of nodes is strictly smaller than the number of cores of the CPU (10 in our case), while the benefit practically vanishes (actually resulting in more overhead) as the number of parallel threads grows significantly more than the cores available.

CONCLUSIONS & FUTURE WORK
We extended the traditional definition of signals to also consider imprecise signals defined by intervals of values. We presented an interval semantics for STREL, we proved its soundness and correctness, and we introduced an online monitoring algorithm for STREL that exploits imprecise signals that can be refined by updates arriving in any order, and that can monitor updates on different locations in parallel. We implemented the proposed methodology in the Moonlight monitoring tool. We motivated our framework from an air pollution control specification with real data from the region of Lombardy, Italy. Lastly, we compared the new methodology with other state-of-the art tools, and discussed the differences. Many directions of future work can be followed, for example, the space-synchronization hypothesis helped us simplifying the implementation of the algorithms, but is not needed from a theoretical point of view. It will be interesting in the future to clearly assess the computational advantages and disadvantages of that hypothesis, and to which extent it can be relaxed. Another intriguing topic for future development concerns spatial models representing (and interacting as) distributed systems. In that context, multiple directions could be pursued, like considering an ownership model for the atomic formulae, or by reasoning on an actor-based communication model among locations. Another interesting idea could be to expand the kind of failures we can monitor, for example, we could consider some form of error correction in case some received updates later prove to have provided wrong information (maybe because of some broken sensors). Lastly, different form of computational optimization could be explored, like stopping when some bounds on the satisfiability/robustness have been reached, as well as intensive parallelization and hardware acceleration of the main algorithms.