key: cord-0733457-xaqecx9m
authors: Nenzi, L.; Bartocci, E.; Bortolussi, L.; Loreti, M.
title: A Logic for Monitoring Dynamic Networks of Spatially-distributed Cyber-Physical Systems
date: 2021-05-24
journal: Logical Methods in Computer Science
DOI: 10.46298/lmcs-18(1:4)2022
sha: 1c850af52ac16c97c75f7572e77c1be0fedf26a0
doc_id: 733457
cord_uid: xaqecx9m

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.

From contact tracing devices preventing the epidemic spread to vehicular networks and smart cities, Cyber-Physical Systems (CPS) are pervasive information and communication technologies augmenting the human perception and control over the physical world. CPS consist of engineering, physical and biological systems that are tightly interacting with computational entities through sensors and actuators. CPS are networked at every scale and they are connected to the Internet (Internet of Things) enabling humans and other software systems to inter-operate with them through the World Wide Web.

A prominent example of CPS is present in the modern automotive systems where the substantial embedding of sensors, actuators, and computational units has facilitated the development of various driving assistance features such as the adaptive cruise control or the collision avoidance system. Furthermore, the upcoming 5G networks will empower soon vehicles also with the possibility to access real-time information about each other (position and speed of vehicles) and the condition of the other roads (accidents or traffic jams). Thus, this dynamic network infrastructure promises to enhance further autonomous driving applications, reduce traffic congestion and improve safety.

The benefits brought by this increasingly pervasive technology have also a price: unexpected failures can potentially manifest causing fatal accidents. Due to their safety-critical nature [RKG + 19], engineers must verify that their behavior is correct with respect to rigorously defined requirements. However, given the uncertainty of the environment in which these systems operate, detecting all the failures at design time is usually unfeasible. Exhaustive verification techniques such as model checking are limited to very small instances due to state-space explosion. An alternative approach is to simulate a digital replica of the CPS (its digital twin) and to test the behavior under different scenarios. Requirements are generally expressed in a formal specification language that can be monitored online (during the simulation) or offline over the simulation traces. Most of the available specification languages [MN13, Mal16 , BDG + 20, ACM02] can specify only temporal properties. However, spatio-temporal patterns play a key role in the understanding of how emergent behaviors can arise from local interactions in such complex systems of systems. Thus, an important problem is then how to specify in a formal language spatio-temporal requirements, and how to efficiently monitor them on the actual CPS or on the simulation of its digital twin.

In this paper, we propose the Spatio-Temporal Reach and Escape Logic (STREL), a spatio-temporal specification language originally introduced in [BBLN17] and that we further revisit and extend in this manuscript. STREL allows to specify spatio-temporal requirements and their monitoring over the execution of mobile and spatially distributed entities and it is supported by the MoonLight [BBL + 20] monitoring tool.

STREL considers the space, where the single components are spatially arranged, as a weighted graph representing the dynamical topological configuration. Both nodes and edges include attributes modeling the physical and logical quantities that can evolve in time. STREL combines the Signal Temporal Logic [MN04] with two spatial operators reach and escape. Other spatial operators such as everywhere, somewhere and surround can be derived from them. The use of reach and escape opens the possibility to monitor the STREL property locally at each node by observing the value of satisfaction of its neighbors. The verdict of a STREL monitor can be evaluated using different semantics (Boolean, real-valued) based on the constraint semirings algebraic structures.

The use of STREL is by no means restricted to CPS as an application domain, but it is capable of capturing many interesting notions in other spatio-temporal systems, including biological systems (e.g. Turing patterns [BBM + 15, BAGHB16, NBC + 18]), epidemic spreading scenarios (in real space or on networks) [PSCVMV15] , or ecological systems. In these cases, monitoring algorithms typically act as key subroutines in statistical model checking [BBM + 15] .

This paper extends our preliminary work [BBLN17] as follows:

• we guide the reader through the all paper using a running example to facilitate the comprehension of our framework in each step; • we simplify the definition of dynamical spatial model and of the spatio-temporal semantics;

• we extend spatial STREL operators to support interval constraints on distances;

• we propose new monitoring algorithms, more efficient and able to work with interval constraints. We also provide correctness proofs and discuss in detail its algorithmic complexity; • we consider a second case study where we monitor spatio-temporal requirements in STREL on a simulated epidemic spreading model for COVID19; The rest of the paper is organized as follows. We discuss the related work in Section 2. In Section 3 we introduce the reader with a running example while in Section 4 we present the considered model of space and the type of signals. The STREL specification language is presented in Section 5 and the offline monitoring algorithms are discussed in Section 6. In Section 7 and 8 we discuss the two case studies: the ZigBee protocol and the COVID-19 epidemic spreading. Finally, Section 9 presents the conclusions.

The study of spatial logics dates back to at least twenty years ago. A first systematic study of spatial logics was proposed in a dedicated handbook [APHvB07] . These works discuss several important theoretical problems such as expressivity and decidability. However, the lack of verification procedures and available tools made these specification languages less practical to use. More recently, Ciancia and others proposed spatial [CLLM14] and spatial-temporal [CGG + 18] model checking algorithms to verify the Spatial Logic for Closure Spaces [CLLM14] (SLCS) and its later extension [CGG + 18] with the temporal modality of the Computation Tree Logic [EH83] . SLCS considers a discrete and topological notion of space that is based on closure spaces [Gal99] . Another example of the spatial model checker is VoxLogicA [BCLM19, BBC + 20], a specialized tool designed for image analysis. VoxLogicA does not consider time and due to its specialization to image analysis, it cannot be employed to verify spatio-temporal properties over cyber-physical systems. Spatialtemporal model checking algorithms are also very computationally expensive due to the state-space explosion that is further exacerbated by the spatial domain. Here, we consider instead a more lightweight verification technique that consists in monitoring spatial properties over a single execution trace of the system. This approach can be applied both on a simulated model of the system or on the system itself by properly instrumenting it and collecting its execution traces.

In the field of runtime verification several logical frameworks for monitoring spatialtemporal properties [NBB + 20] are recently gaining momentum: Spatial-Temporal Logic (SpaTeL) [HJK + 15], Signal Spatio-Temporal Logic (SSTL) [NBC + 15] , Spatial Aggregation Signal Temporal Logic (SaSTL) [MBL + 20, MBL + 21] and Spatio-Temporal Reach and Escape Logic (STREL) [BBLN17] . SpaTeL combines the Signal Temporal Logic [MN04] (STL) with the Tree Spatial Superposition Logic [AGBB14] (TSSL). Spatial patterns in TSSL are specified in terms of properties over quad trees [FB74] spatial data structures. Specifications in this logic can capture even complex fractal spatial patterns. However, finding the right formulation manually can be extremely cumbersome.

SSTL [NBC + 15, NBC + 18] extends the STL temporal logic with two spatial modalities somewhere and surrounded that operate over a weighted graph where nodes represent spatial locations while edges their topological relations. The somewhere operator specifies that a property is true in at least one of the nodes nearby, while the surround operator specifies the property of being surrounded by a region of nodes satisfying its nested formula. SSTL can be interpreted using both Boolean and real-valued semantics. One limitation of SSTL is that the topological relation of the nodes is fixed: the nodes cannot change their position. STREL [BBLN17] overcomes this limitation by operating over a dynamic topological space. STREL introduces also two new spatial operators (reach and escape) that generalize and substitute the SSTL operators and it simplifies the monitoring procedure that is now computed locally in each node.

SaSTL [MBL + 20, MBL + 21] is yet another spatio-temporal monitoring language recently developed to monitor the internet of things of smart cities. SaSTL is equipped with new logical spatial operators to express spatial aggregation and spatial counting and similarly to SSTL the monitoring procedure is limited to only a static topological space.

Another important key characteristic of STREL with respect to all the aforementioned spatio-temporal specification languages is the possibility to define the semantics using constraint semirings algebraic structures. This provides the possibility to elegantly define a unified monitoring framework for both the qualitative and quantitative semantics (similarly to [JBGN18] for the STL case). Finally, it is also worth mentioning several recent applications of STREL ranging from mining spatio-temporal requirements from data [MDN21] to synthesizing neural network-based controllers for multi-agent systems [AMBB21] .

A mobile ad-hoc sensor network (MANET) can consist of up ten thousand mobile devices connected wirelessly, usually deployed to monitor environmental changes such as pollution, humidity, light, and temperature. Each sensor node is equipped with a sensing transducer, data processor, radio transceiver, and an embedded battery. A node can move independently in any direction and indeed can change its links to other devices frequently. Two nodes can communicate with each other if their Euclidean distance is at most their communication range as depicted in Figure 1 (right). Moreover, the nodes can be of different type and their behavior and communication can depend on their types. In the next section, we consider the simplest MANET with all nodes of the same type, while in Section 5 we will differentiate them to describe more complex behaviors.

In this section, we introduce the model of space we consider, and the type of signals that the logic specifies. 4.1. Constraint Semirings. An elegant and general way to represent the result of monitoring is based on constraint semiring [BMR97] . This is an algebraic structure that consists of a domain and two operations named choose and combine. Constraint semirings are a subclass of semirings that have been shown to be very flexible, expressive, and convenient for a wide range of problems, in particular for optimization and solving problems with soft constraints and multiple criteria [BMR97] , and in model checking [LM05] . Definition 4.1 (Semiring). A semiring is a tuple ⟨A, ⊕, ⊗, , ⊺⟩ composed by a set A, two operators ⊕, ⊗ and two constants , ⊺ ∈ A such that: • ⊕ ∶ A × A → A is an associative, commutative operator to "choose" among values 1 , with as unit element ( ⊕ a = a, ∀a ∈ A). • ⊗ ∶ A × A → A is an associative operator to "combine" values with ⊺ as unit element ( ⊺ ⊗ a = a, ∀a ∈ A) and as absorbing element ( ⊗ a = , ∀a ∈ A ) • ⊗ distributes over ⊕;

Definition 4.2 (c-semiring). A constraint semiring (c-semiring) is a semiring ⟨A, ⊕, ⊗, , ⊺⟩ such that: • ⊕ is defined over 2 A , idempotent ( a ∈ A a ⊕ a = a ⊗ a = a) and has ⊺ as absorbing element ( ⊺ ⊕ a = ⊺) • ⊗ is commutative • ⊑, which is defined as a ⊑ b iff a ⊕ b = b, provides a complete lattice ⟨A, ⊑, , ⊺⟩. We say that a semiring A is total when ⊑ is a total order .

With abuse of notation, we sometimes refer to a semiring ⟨A, ⊕, ⊗, , ⊺⟩ with the carrier A and to its components by subscribing them with the carrier, i.e., ⊕ A , ⊗ A , A and ⊺ A . For the sake of a lighter notation, we drop the subscripts when clear from the context. • the tropical semiring ⟨R ∞ ≥0 , min, +, +∞, 0⟩; • the max/min semiring: ⟨R ∞ , max, min, −∞, +∞⟩ ; • the integer semiring: ⟨N ∞ , max, min, 0, +∞⟩. All the above semirings are total.

One of the advantages of semirings is that these can be easily composed. For instance, if A and B are two semirings, one can consider the cartesian product ⟨A×B, ( A , B ), (⊺ A , ⊺ B ), ⊕, ⊗⟩ where operations are applied elementwise. 4.2. Spatial model. Space is represented via a graph with edges having a weight from a set A. We consider directed graphs (undirected graphs can consider symmetric relation).

Definition 4.4 (A−spatial model). An A−spatial model S is a pair ⟨L, W⟩ where: • L is a set of locations, also named space universe; • W ⊆ L × A × L is a proximity function associating at most one label w ∈ A with each distinct pair 1 , 2 ∈ L.

We will use S A to denote the set of A-spatial models, while S L A indicates the set of A-spatial models having L as a set of locations. In the following, we will equivalently write ( 1 , w, 2 ) ∈ W as W( 1 , 2 ) = w or 1 w ↦ 2 , saying that 1 is next to 2 with weight w ∈ A.

Example 4.5. R ∞ ≥0 -spatial model can be used to represent standard weighed graphs as Figure 2 . L is the set of nodes and the proximity function W defines the weight of the edges, e.g. W( 2 , 7 ) = W( 7 , 2 ) = 5. A special class of spatial models is the ones based on Euclidean spaces.

Definition 4.6 (Euclidean spatial model). Let L be a set of locations, R ⊆ L × L a (reflexive) relation and λ ∶ L → R 2 a function mapping each location to a point in R 2 , we let E(L, R, λ) be the R ∞ × R ∞ -spatial model 3 ⟨L, W λ,R ⟩ such that:

Note that we label edges with a 2-dimensional vector w describing how to reach 2 from 1 , i.e., λ( 1 ) − w = λ( 2 ). This obviously allows us to compute the Euclidean distance between 1 and 2 as w 2 , but, as we will see, allows us to compute the Euclidean distance of any pair of locations connected by any path, not necessarily by a line in the plane. Note that, in the general case, a Euclidean spatial model is not a planar graph. A planar graph is obtained when, for instance, one considers the proximity graph of Figure 1 .

Example 4.7. When considering a MANET, we can easily define different proximity functions for the same set of locations, where each location represents a mobile device. Given a set of n reference points in a two-dimensional Euclidean plane, a Voronoi diagram [Aur91] partitions the plane into a set of n regions, one per reference point, assigning each point of the plane to the region corresponding to the closest reference point. The dual of the Voronoi diagram is the proximity graph or Delaunay triangulation [Del34] . In Figure 1 (left) we can see an example of the Voronoi diagram (in blue) and proximity graph (in red).

The proximity function can then be defined with respect to the Cartesian coordinates, as in Definition 4.6:

The proximity function can be also equal to a value that depends on other specific characteristics or behaviors of our nodes. For instance, Figure 1 (right) represents the connectivity graph of MANET. In this case, a location i is next to a location j if and only if they are within their communication range.

Given an A-spatial model we can define routes. Let τ = 0 1 ⋯ k ⋯ be a route, i ∈ N and i ∈ L, we use:

.] to indicate the suffix route i i+1 ⋯; • ∈ τ when there exists an index i such that τ [i] = , while we use ∈ τ if this index does not exist; • τ ( ) to denote the first occurrence of in τ :

We also use Routes(S) to denote the set of routes in S, while Routes(S, ) denotes the set of routes starting from ∈ L. We can use routes to define the distance among two locations in a spatial model. This distance is computed via an appropriate function f that combines all the weights in a route into a value taken from an appropriate total ordered monoid B. 

Given a locations ∈ L, the distance over τ up-to is then d f

Example 4.11. Considering again a MANET, one could be interested in different types of distances, e.g., counting the number of hop, or distances induced by the weights of the Euclidean space structure. It is easy to see that for any route τ and for any location ∈ L in τ , the function d ∆ τ ( ) yields the sum of lengths of the edges in R 2 connecting to τ (0).

Given a distance function f ∶ A → B, the distance between two locations 1 and 2 in a A-spatial model is obtained by choosing the minimum distance along all possible routes starting from 1 and ending in 2 : -

In this paper, we consider two signal domains: • Boolean signal domain ⟨{⊺, }, ∨, ∧, ¬, , , ⊺, ⟩ for qualitative monitoring;

• Max/min signal domain ⟨R ∞ , max, min, −, , ⊺, ⟩ for quantitative monitoring.

For signal domains, we use the same notation and notational conventions introduced for semirings.

such that for ∀i, t i ∈ T, t i < t i+1 and d i ∈ D. We letν denote a piecewise constant temporal

Given a piecewise constant temporal signalν = [(t 0 , d 0 ), . . . , (t n , d n )] we use T (ν) to denote the set {t 0 , . . . , t n } of time steps inν; start(ν) to denote t 0 ; while we say thatν is minimal if and only if for any i, d i = d i+1 . We also letν[t = d] denote the signal obtained fromν by adding the element (t, d). Finally, if ν 1 and ν 2 are two D-temporal signals, and op ∶ D × D → D, ν 1 op ν 2 denotes the signal associating with each time t the value 

such that σ( ) = ν is a temporal signal that returns a value ν(t) ∈ D for each time t ∈ T. We say that σ is piecewise constant when for any , σ( ) is a piecewise constant temporal signal. Piecewise constants signal are denoted byσ. Moreover, we use T (σ) to denote ⋃ T (σ( )). Finally, we letσ@t denote the spatial signal associating each location withσ( , t).

Given a spatio-temporal signal σ, we use σ@t to denote the spatial signal at time t, i.e. the signal s such that s( ) = σ( )(t), for any ∈ L. Different kinds of signals can be considered while the signal domain D is changed. Signals with D = {true, f alse} are called Boolean signals; with D = R ∞ are called real-valued or quantitative signals.

Definition 4.17 (D-Trace). Let L be a space universe, a spatio-temporal D-trace is a function ⃗

x ∶ L → T → D 1 × ⋯ × D n such that for any ∈ L yields a vector of temporal signals ⃗ x( ) = (ν 1 , . . . , ν n ). In the rest of the paper, we use ⃗ x( , t) to denote ⃗ x( )(t).

Example 4.18. We can consider a (R × R)-spatio-temporal trace of our sensor network as ⃗ x ∶ L → T → R × R that associates a set of temporal signals ⃗ x( ) = (ν B , ν T ) at each location, where ν B and ν T respectively correspond to the temporal signals of the battery and the temperature in location , and each signal has domain ⟨R, max, min, −, , ⊺, ⟩.

We plan to work with spatial models that can dynamically change their configurations. For this reason, we need to define a function that returns the spatial configuration at each time.

Definition 4.19 (Dynamical A-Spatial Model). Let L be a spatial universe, a dynamical A-spatial model is a function S ∶ T → S L A associating each element in the time domain T with A-spatial model S(t) = ⟨L, W⟩ that describes the spatial configuration of locations.

With an abuse of notation, we use S for both a dynamical spatial model and a static spatial model, where, for any t, S = S(t).

Example 4.20. Let us consider a MANET with a proximity graph. Figure 3 shows two different snapshots, S(t 1 ) = ⟨L, W 1 ⟩ and S(t 2 ) = ⟨L, W 2 ⟩, of the the dynamical spatial model S for time t 1 and t 2 . We can see that locations 1 and 2 change their position, this changed also the Voronoi diagram and the proximity graph. Vol. 18:1 Figure 3 : Two snapshots of a spatial model with 7 locations 1 , . . . , 7 that move in a 2D Euclidean space. The plane is partitioned using a Voronoi Diagram (blue). In red we have the proximity graph.

In this section, we present the Spatio-Temporal Reach and Escape Logic (STREL), an extension of the Signal Temporal Logic. We define the syntax and the semantics of STREL, describing in detail the spatial operators and their expressiveness. The syntax of STREL is given by

where µ is an atomic predicate (AP ), negation ¬ and conjunction ∧ are the standard Boolean connectives, U [t 1 ,t 2 ] and S [t 1 ,t 2 ] are the Until and the Since temporal modalities, with [t 1 , t 2 ] a real positive closed interval. For more details about the temporal operators, we refer the reader to [MN13, MN04, DFM13] . The spatial modalities are the reachability

In what follows, we omit the type info about function f when it is clear from the context or where it does not play any role.

The reachability operator φ 1 R f [d 1 ,d 2 ] φ 2 describes the behavior of reaching a location satisfying property φ 2 , through a path with all locations that satisfy φ 1 , and with a distance that belongs to

instead, describes the possibility of escaping from a certain region via a route passing only through locations that satisfy φ, with the distance between the starting location of the path and the last that belongs to the interval [d 1 , d 2 ]. Note that the main difference between these two operators is that the distance of the reach operator is with respect to the path, instead, the distance of the escape operator is between the locations, so it considers the shortest path distance between the starting location and the last. As customary, we can derive the disjunction operator ∨ and the future eventually F [t 1 ,t 2 ] and always G [t 1 ,t 2 ] operators from the until temporal modality, and the corresponding past variants from the since temporal modality, see [MN13] for details. We can define also other three derived spatial operators: the somewhere f ∶A→B ≤d φ and the everywhere f ∶A→B ≤d φ that describe behaviors of some or of all locations at a certain distance from a specific point, and the surround that expresses the topological notion of being surrounded by a φ 2 -region, while being in a φ 1 -region, with additional metric constraints. A more thorough discussion of the spatial operators will be given after introducing the semantics. 5.1. Semantics. The semantics of STREL is evaluated point-wise at each time and at each location. We stress that each STREL formula ϕ abstracts from the specific domain used to express the satisfaction value of ϕ. These, of course, are needed to define the semantics. In the following, we assume that D 1 is the domain of the spatio-temporal traces, D 2 is the semiring where the logic is evaluated and B is a distance domain as defined in Definition 4.9.

Definition 5.1 (Semantics). Let S be a dynamical A-spatial model with L the space universe, D 1 and D 2 be two signal domains, and ⃗

x be a spatio-temporal D 1 -trace for L. The D 2 -monitoring function m of ⃗

x is recursively defined in Table 1 . Given a formula φ, the function m(S, ⃗ x, φ, t, ) corresponds to the evaluation of the formula at time t in the location . The procedure is exactly the same for different choices of the formula evaluation domain, just operators have to be interpreted according to the chosen semirings and signal domains. In particular, the choice of the signal domain D 2 produces different types of semantics. In this paper, we consider two signal domains: B and R ∞ , giving rise to qualitative and quantitative monitoring, corresponding respectively to a Boolean answer and a real satisfaction value. For the Boolean signal domain (D 2 = ⟨{⊺, }, ∨, ∧, ¬⟩ ), we say that (S, ⃗

x( , t)) satisfies a formula φ iff m(S, ⃗ x, φ, t, ) = ⊺. For max/min signal domain ⟨R ∞ , max, min, −, , ⊺, ⟩ we say that (S, ⃗

x( , t)) satisfies a formula φ iff m(S, ⃗ x, φ, t, ) > 0. In the following, we useσ S,⃗ x φ to denote the spatio-temporal D 2 -signal such that for any t and m(S, ⃗

x, φ, t, ) =σ S,⃗ x φ ( , t). We describe now in detail the semantics through the sensor network example as the system on which we specify our properties, in particular, we use the graph in Figure 4 to describe the spatial operators. Example 5.2 (ZigBee protocol). In Figure 4 , the graph represents a MANET. In particular, we consider the nodes with three different roles such as the ones implemented in the ZigBee protocol: coordinator, router and EndDevice. The Coordinator node (coord), represented in green color in the graph, is unique in each network and is responsible to initialize the network. After the initialization of the network has started, the coordinator behaves as a router. The Router node (router), represented in red color in the graph, acts as an intermediate router, passing on data from other devices. The EndDevice node (end dev), represented in blue, can communicate only with a parent node (either the Coordinator or a Router) and it is unable to relay data from other devices. Nodes move in space and the figure corresponds to the spatial configuration at a fixed time t. As spatio-temporal trace, let us consider a

if is a router, and ⃗

x( , t) = (end dev, b) if is an end node, where b is the level of the battery.

Atomic Proposition. The function ι ∶ AP × D n 1 → D 2 is the signal interpretation function and permits to translate the input trace in a different D 2 -spatio temporal signal for each atomic proposition in AP , which will be the input of the monitoring procedure. Different types of atomic propositions and signal interpretations are admissible. E.g., we can simply consider a finite set {p 1 , . . . , p n } = AP and an interpretation function ι(p i , ⃗

x( , t)) = ⊺ iff x i ( , t) = ⊺. In Figure 4 , we can consider atomic propositions describing the type of node, i.e., the Boolean propositions {coord, router, end dev} are true if the node is of the corresponding type. In case of real valued signals and of a quantitative interpretation of the logic (D 2 being in this case the real valued max/min semiring), we can consider inequalities µ = (g(⃗ x) ≥ 0) for some real function g and define ι(µ, ⃗

x( , t)) = g(⃗ x( , t)), e.g. b > 0.5, that means "the level of the battery is greater than 50% Negation. The negation operator is interpreted with the negation function ⊙ D 2 of the chosen signal domain; e.g. m(S, ⃗

x, ¬ϕ, t, ) = ¬m(S, ⃗ x, ϕ, t, ) for the Boolean signal domain and m(S, ⃗

x, ¬ϕ, t, ) = −m(S, ⃗ x, ϕ, t, ) for the quantitative ones. Conjunction and Disjunction The conjunction operator ϕ 1 ∧ ϕ 2 is interpreted with the combine operator ⊗ D 2 , i.e. m(S, ⃗

x, ϕ 1 ∧ ϕ 2 , t, ) = m(S, ⃗ x, ϕ 1 , t, ) ⊗ D 2 m(S, ⃗ x, ϕ 2 , t, ), which corresponds to wedge ∧ operator for the Boolean semantics. This means that m(S, ⃗

x, ϕ 1 ∧ ϕ 2 , t, ) = 1 iff both m(S, ⃗ x, ϕ 1 ) and m(S, ⃗ x, ϕ 2 ) are equal to 1. For the quantitative semantics ⊗ D 2 is interpreted ad the minimum operator, so, m(S, ⃗

x, ϕ 1 ∧ ϕ 2 , t, ) = min(m(S, ⃗

x, ϕ 1 , t, ), m(S, ⃗ x, ϕ 2 , t, )). Similarly the disjunction ϕ 1 ∨ ϕ 2 is interpreted through the choose operator ⊕ D 2 , i.e. m(S, ⃗

x, ϕ 1 ∨ ϕ 2 , t, ) = m(S, ⃗ x, ϕ 1 , t, ) ⊕ D 2 m(S, ⃗

x, ϕ 2 , t, ), which corresponds to the ∨ for the Boolean semantics and to the max for the quantitative one.

In the rest of the description, we focus on the Boolean semantics, i.e. D 2 = ⟨{⊺, }, ∨, ∧, ¬⟩, the Quantitative semantics can be derived substituting ∨, ∧ with min, max, as seen for conjunction and disjunction. Until.

As customary, (S, ⃗ x( , t)) satisfies ϕ 1 U [t 1 ,t 2 ] ϕ 2 iff it satisfies ϕ 1 from t until, in a time between t 1 and t 2 time units in the future, ϕ 2 becomes true. Note how the temporal operators are evaluated in each location separately.

Since.

x( , t)) satisfies ϕ 1 S [t 1 ,t 2 ] ϕ 2 iff it satisfies ϕ 1 from now since, in a time between t 1 and t 2 time units in the past, ϕ 2 was true.

Except for the interpretation function, the semantics of the Boolean and the temporal operators is directly derived from and coincident with that of STL (qualitative for Boolean signal domain and quantitative for an R ∞ signal domain), see [MN04, DFM13] for details.

Reachability.

, and such that τ [0] = and all its elements with index less than τ ( ′ ) satisfy ϕ 1 . In Figure 4 , we report an example of reachability property, considering f as the hop function described in Example 4.11. In the graph, the location 6 (meaning the trajectory ⃗ x (it is a coordinator) .

x( , t)) iff all the locations reachable from via a path, with length belonging to the interval [0, d], satisfy ϕ. In Figure 4 , there are no locations that satisfy the property hop [0,2] router because for all the locations i there is a path τ = i j such that j does not satisfy the red property (it is not a router). here it is a derived one. The idea is that one cannot escape from a ϕ 1 -region without passing from a location that satisfies ϕ 2 and, in any case, one has to reach a ϕ 2 -location via a path with a length less or equal to d. In Figure 4 , the location 10 satisfies the property (coord ∨ router) ⊚ hop [0,3] end dev. In fact, it satisfies the green property, it cannot reach a location that does not satisfy the blue or the red property via a path with length lesser or equal to 3 and it cannot escape through a path satisfying the green or red properties at a distance more than 3.

The operators can be arbitrarily composed to specify complex properties as we will see in Section 7 and 8.

Invariance properties of the Euclidean spatial model. The properties we consider with respect to the Euclidean spatial model are typically local and depend on the relative distance and position among nodes in the plane. As such, they should be invariant with respect to the change of coordinates, i.e. with respect to the isometric transformations of the plane. This class of transformations include translations, rotations, and reflections, and can be described by matrix multiplications of the form

where β, γ are the stretching, α the rotation, and t x , t y the translation factor respectively. Invariance of satisfaction of spatial properties holds in STREL logic, for the Euclidean space model of Definition 4.6. Consider an Euclidean space model E(L, µ, R) = ⟨L, W µ,R ⟩ and E(L, µ ′ , R) = ⟨L, W µ ′ ,R ⟩, obtained by applying an isometric transformation A: µ ′ ( ) = A(µ( )), for invariance to hold, we need to further require that distance predicates used in spatial operators are invariant for isometric transformations. More specifically, for any isometry A, we require a distance predicate d on the semiring R ∞ × R ∞ to satisfy d((x, y)) = d (A((x, y) )). This is the case for the norm-based predicates used in the examples, of the form d((x, y)) = (x, y) 2 ≤ r.

Notice that, the path structure is preserved (the edges given by R is the same), and the truth of isometry-invariant distance predicates along paths in E(L, µ, R) and E(L, µ ′ , R) is also the same. This straightforwardly implies that the truth value of spatial operators will be unchanged by isometry.

Proposition 5.3 (Equisatisfiability under isometry). Let E(L, µ, R) = ⟨L, W µ,R ⟩ be an Euclidean spatial model and E(L, µ ′ , R) = ⟨L, W µ ′ ,R ⟩ an isometric transformation of the former. Consider a spatial formula ϕ 1 R f d ϕ 2 or E f d ϕ 1 , where d is an isometry preserving predicate. Assume m(S, ⃗

x, ϕ j , t, ) = m ′ (S, ⃗ x, ϕ j , t, ), j = 1, 2, where m and m ′ are the monitoring functions for the two spatial models. Then it holds that m(S, ⃗

x,

, for all and t.

In this section, we present a monitoring algorithm that can be used to check if a given signal satisfies or not a STREL property. The proposed algorithm follows an offline approach. Indeed, the proposed algorithm takes as input the complete spatio-temporal signal together with the property we want to monitor.

6.1. Offline monitor. Offline monitoring is performed via a function monitor that takes as inputs a dynamical spatial model S, a trace ⃗ x and a formula φ and returns the piecewise constant spatio-temporal signalσ representing the monitoring of φ. The function monitor is defined by induction on the syntax of the formula (Algorithm 6.1). The spatio-temporal signal resulting from the monitoring of atomic proposition µ is just obtained by applying function ι(µ) to the trace x. The spatio-temporal signals associated with ¬ϕ and ϕ 1 ∧ ϕ 2 are obtained by applying operators ⊙ D 2 and ⊗ D 2 to the signals resulting from the monitoring of ϕ and from the monitoring of ϕ 1 and ϕ 2 where ⊕ D 2 , ⊗ D 2 and ⊙ D 2 depend the signal domain used to represent satisfaction values.

Monitoring of temporal properties, namely ϕ 1 U [t 1 ,t 2 ] ϕ 2 and ϕ 1 S [t 1 ,t 2 ] ϕ 2 , relies on functions Until and Since. These are defined by using the same approach of [DFM13] and [MN13] . However, while their monitoring relies on classical Boolean and arithmetic operators, here the procedure is parametrised with respect to operators ⊕ D 2 and ⊗ D 2 of the considered semiring.

To monitor ϕ 1 R f ∶A→B [d 1 ,d 2 ] ϕ 2 we first compute the signals s 1 and s 2 , resulting from the monitoring of ϕ 1 and ϕ 2 . After that, the final result is obtained by aggregating the spatial signals s 1 @t and s 2 @t at each time t ∈ T (s 1 ) ∪ T (s 2 ) by using function Reach defined in Algorithm 2. In this function two cases are distinguished: d 2 = ⊺ B or d 2 = ⊺ B . In the first case, the resulting monitoring value is calculated via function BoundedReach defined in Algorithm 3. Conversely, when d 2 = ⊺ B monitoring is performed by relying on function UnboundedReach defined in Algorithm 4. 

for all t ∈ T (σ 1 ) ∪ T (σ 2 ) do 50:σ@t = Reach(S(t), f, d 1 , d 2 ,σ 1 @t,σ 2 @t) while Q = ∅ do 5:

else 17: 

if the sum of the current distance plus the distance between and ′ is still less than d 2 . When d ′ ∈ [d 1 , d 2 ], s( ′ ) is updated to take into account the new computed value. We recal that s stores the value of the semantics of the reach operator.

UnboundedReach. Function UnboundedReach defined in Algorithm 4 is used when the interval in the reach formula is unbounded. In this case the function takes as parameters the spatial model ⟨L, W⟩ at time t, the function f ∶ A → B, used to compute the distances over paths, and the lower bound d 1 , and returns a spatial signal s. If d 1 = B , i.e. when we are considering a totally unbound reach with no constraints, we initialize s = s 2 . Otherwise, when d 1 = , we have first to call function boundedReach by passing as upper bound d 1 + d max , where d max is the max value that function f can associate to a single edge in W. while T = ∅ do 10:

for all ∈ T do 12:

14:

if v ′ = s[ ′ ] then 15: for all ( 1 , 2 ) ∈ T do 10:

if v = e[ ′ 1 , 2 ] then 13: 

Proof. Let us denote by s i and Q i the value of variables s and Q respectively in Algorithm 3 after i iterations of the while-loop at line (4). Considering that, since f (w) > 0 for any w ∈ A, the algorithm terminates after a finite number of iterations, the statement follows directly from the following properties: Property P 3 can be proved by induction on i by observing that the property is satisfied by Q 0 and that for any i:

From the above, and from inductive hypothesis, we have that:

That is the statement of P 3. Finally, we can probe P 4 by induction on i by using P 3 and by observing that:

, and two spatial signals s 1 ∶ L → D 2 , s 2 ∶ L → D 2 such that UnboundedReach((L, W), f, d 1 , s 1 , s 2 ) = s, for any ∈ L, we have that:

Proof. Directly from the pseudo code in Algorithm 4 and from Lemma 6.2, we can observe that the value s computed by function UnboundedReach is the limit (s = lim i→∞ s i ) of the sequence of signals s i such that for any ∈ L:

The initial spatial signal is s 0 = s 2 , if d 1 = B , while it is:

In both the cases, the statement follows by applying standard algebra and the properties of ⊕ and ⊗. Lemma 6.3 (Escape correctness). Given an A-spatial model (L, W) , a function f ∶ A → B, an interval [d 1 , d 2 ] (with d 1 , d 2 ∈ B, d 1 ≤ B d 2 and) d 2 = ⊺ B ), and a spatial signal s 1 ∶ L → D 2 such that Escape((L, W), f, d 1 , d 2 , s 1 ) = s, for any ∈ L, we have that:

Proof. Let us denote by e i the content of data structures e after i iterations of the loop at line (6) of Algorithm 5. We have only to prove the following properties: 

Property P 1 follows directly from definition of d f (L,W) [ , ′ ] and from the fact that MinDistance(L, W, f) computes the matrix of min distances computed in ⟨L, W⟩ via f . Property P 2 can be proved by induction on i and follows directly from the code of Algorithm 5. Finally, P 3 is a consequence of the fact that after at most L iterations a fix point is reached since all the locations have been taken into account. We can conclude that the statement of the lemma follows directly from properties P 1, P 2 and P 3 above by observing that:

) Theorem 6.4. Given a dynamical spatial model S, a trace ⃗

x and a formula φ, we have that:

Proof. The proof easily follows by induction on φ by using Lemma 6.1, Lemma 6.2, and Lemma 6.3.

6.3. Complexity. In this subsection, we discuss the complexity of each algorithm. 

Note that, at the first iteration Q 0 , d = B . At each iteration, we add a value greater or equal to d min , this means that after k iterations d ′ ≥ k * d min but k * d min > d 2 for definition. Q can have at most β d 2 ⋅ L elements and, at each iteration of the while loop, for each elements in Q, we consider their connected ones. This implies that function BoundedReach terminates after O(k ⋅ β d 2 ⋅ L ⋅ m) steps. Proof. We have already observed in Proposition 6.5 that the first part of Algorithm 4 terminates after O(k ⋅ β d 2 ⋅ L ⋅ m). We can here observe that the second part of the algorithm (lines (9) − (21)) needs at most L ⋅ m steps. This is because the for-loop at lines (12) − (18) consists of at most O(m) steps (indeed each edge is considered at most two times). Moreover, a location can be inserted in T at most L times. Concluding, the algorithm terminates We can conclude this section by observing that the number of steps needed to evaluate function Monitor in Algorithm 6.1 is linear in the size of φ, in the length of the signal, and in the number of edges in the spatial model and it is quadratic in the number of locations.

In this section, we consider the running example used in the previous sections. We discuss some properties to show the expressivity and potentiality of STREL.

Given a MANET with a ZigBee protocol (Example 5.2), we consider as spatial models both its proximity and connectivity graphs computed with respect to the Cartesian coordinates (Example 4.7). Nodes have three kind of roles: coordinator, router and EndDevice, as described in Example 5.2. Moreover, each device is also equipped with a sensor to monitor its battery level (b), the humidity (h) and the pollution (p) in its position. The semiring is the union between the max/min semiring R ∞ (for the proximity graph) and the integer semiring N ∞ (for the connectivity graph). We will use also two types of distances: hop and the ∆ distances described in Example 4.11. Atomic propositions {coord, router, end dev} describe the type of nodes. We also consider inequalities on the values that are read from sensors, plus special propositions @ which encode the address of a specific location, i.e. they are true only in the location .

In the following, we describe several properties of these ZigBee MANET networks that are easily captured by STREL logic, to exemplify its expressive power.

A class of properties naturally encoded in STREL is related to the connectivity of the network. First, we can be interested to know if a node is properly connected, meaning that it can reach the coordinator through a path of routers:

The meaning of this property is that one end node reaches in a step a node which is a router and that is connected to the coordinator via a path of routers. We may also want to know if there is a path to the router which is reliable in terms of battery levels, for instance such that all routers have a battery level, b, above 50%:

The properties focus on spatial connectivity at a fixed time. We can add also temporal requirements, for instance asking that a broken connection is restored within h time units:

3) Another class of properties of interest is the acyclicity of transmissions. To this end, we need to force the connectivity graph to be directed, with edges pointing in the direction of the coordinator (i.e. transmission reduces the distance from the coordinator). With STREL, we can easily detect the absence of a cycle for a fixed location . This is captured by φ acyclic = ¬φ cycle , where

In order to characterize the whole network as acyclic, we need to take the conjunction of the previous formulae for all locations (or at least for routers, enforcing end devices to be connected only with routers). This is necessary as STREL is interpreted locally, on each location, and this forbids us to express properties of the whole network with location unaware formulae. This is a price for efficient monitoring, as global properties of networks require more expressive and computationally expensive logic. However, we can use the parametrization of STREL and the property of a Voronoi diagram to specify the global connection or the acyclicity of the graph. Indeed, the proximity graph connects always all the locations of the system, then the property ∆ φ, verified on the proximity graph, holds iff φ holds in all the locations of the system. Up to now, we have presented qualitative properties, depending on the type of node. If we express properties of sensor measurements, we can also consider quantitative semantics, returning a measure of the robustness of (dis)satisfaction. As an example, we can monitor (7.5) if in each location a high value of pollution eventually implies, within T time units, an high value of humidity, or (7.6) in which locations it is possible to find a 'safe' route, where both the humidity and the pollution are below a certain threshold. We can also check (7.7) if a location is at least at distance at most d from a location that is safe. In this section, we investigate a case study based on an epidemic spreading model in a population of a disease-transmitting via direct contact, like flu or COVID19. The simplest models of epidemic spreading are based on a mean-field assumption and treat the population as a homogeneous entity, assuming equal probability that two individuals can enter into contact [BCCF19] . A more accurate description, instead, models potential contacts in a more explicit way, hence the population is represented as a network of interacting agents [PSCVMV15] , in which nodes are the agents and links are the potential contacts. Such a network can be static (links are fixed) or dynamic (links change during the simulation) and possibly adaptive [PSCVMV15] . These kinds of models are particularly useful when dealing with scenarios in which the number of potentially infective contacts, and thus of secondary infections, can vary a lot between individuals, the so-called super-spreading scenario [LSSKG05] , which seems to be the relevant one also to capture the spreading of COVID19 disease [LWD + 20]. In our case study, we consider a discrete-time model composed of two contact networks, one static, describing contacts within work colleagues, family, closed relatives, and friends, and another one dynamic, modeling less frequent interaction events, like going to the restaurant, the cinema, or the disco. The static network is defined by a degree distribution, assumed to be the same for each node, and modeled as a lognormal distribution with cutoff (mean 10, 99 percentile 50, cut off at 200). 6 To generate the network, we sample a degree for each node and then sample the network relying on the expected degree graph method of networkX Python library [HSS08] . This network is sampled once and not modified during simulations. The dynamic event network, instead, is resampled at every simulation step (essentially corresponding to a day). Here, we additionally choose a subset of nodes that will be affected by the events. Each node has assigned a random probability of taking part in the event (chosen uniformly among the following frequency: once every month, once every two weeks, once every week, twice per week) and at each step, the node is included in the event network with such a probability. Then, each active node receives a degree sampled from a different degree distribution with a longer tail (lognormal with mean 10 and 99 percentile 100, cut off at 1000), to model super-spreading effects. 7 In order to simulate our discrete-time model, with step corresponding to one day, we further give each agent one of four different states (Susceptible, Exposed but not infective, Infective, Recovered), and sample the duration in days of the transitions from E to I and from I to R according to a gamma distribution taken from COVID19 literature [CTR + 20] . Infection of a Susceptible node can happen if it is in contact with an Infective node, with a probability p which is edge dependent and sampled for each edge according to a Beta distribution with a mean 0.05 (which roughly gives an R0 close to 2, as observed in the second phase of the COVID epidemics, in Lombardia, Italy). We assume independence among different edges when modeling the spreading of infection.

At each time step, the spatial model of the epidemic network is designed by the pair ⟨L, W⟩, where the set of locations L corresponds to the set of agents and the proximity function W is such that ( i , w, j ) ∈ W if and only there is a probability greater than 6 Contact distributions are constructed to resemble contact data collected by a regional government in Italy, which is not publicly available.

7 Note that, as we rely on distributions with cut-off, there is no practical difference in using a lognormal or a heavier tail distribution like a power law.

zero that i and j are in contact. The value of the weight w corresponds to the sampled probability described above, both for the static and the dynamic one. More specifically, w = − ln(p i , j (t)), where p i , j (t) is the infection probability at time t. Hence, the higher is w, the lower is the probability that agent i is infected by agent j . We consider two types of distances here, the hop distance, counting the number of hops, and the weight distance, summing the value of edges w.

The spatio-temporal trace of our epidemic network is x ∶ L → T → Z with only one signal ⃗

x( ) = ν associating with each agent and at each time t, the state x( , t) ∈ S = {Susceptible, Exposed, Infected, Recovered} = {S, E, I, R}. To give an idea of the behavior of this model we plot in Figure 5 the number of nodes in each state at each time for a random simulation. time Figure 5 : The number of nodes in each state at each time for a random simulation.

The first property that we consider is:

φ dangerous days is satisfied in a location when it is always true (at each time step) that if a susceptible individual is directly connected with an individual that will be eventually infected in the next 2 days then it will eventually be infected within the next 7 days. If we consider only the static network, this property is satisfied on 447 ± 12.5 nodes of the network, considering 500 experiments, instead, considering only the dynamic network the property is satisfied by 350 ± 70.5 nodes. As expected the daily contacts are more dangerous than casual contact, and the dynamic network has more variability than the static one.

The second property that we consider is:

φ saf e = G( weight [0,r] (¬Infected) => G [0,T ] (¬Infected)) (8.2) φ saf e holds in a location if it is always true that, when all the connected locations at a weight distance less than r (i.e. with infection probability ≤ 10 −r ) are not infected, implies that this location will remain not infected for the next T days. With this property, we can study the relationship between the probability of being infected from connected nodes and being actually an infected individual after a number of days. If a location satisfies the property, it means that being in a radius r of not infected individuals prevents infection. If a location does not satisfy the property it means that there is some infected node at a distance of more than r, connected with it that causes its infection within the next T days. Setting T = 7 days, we study the variation of r versus the number of nodes that satisfy the property (in a network with 500 nodes). Figure 6 shows the results. We report also a second scale with the corresponding probability value. We can see that with r = 3 which corresponds to a connection probability equal to 0.05 (the mean of our Beta distribution), only half of the nodes satisfy the property, and to have almost all nodes that satisfy the property we need to consider a very large radius. This means that having in the network edges with very large values of r will not prevent the spread of the disease. Figure 6 : Number of nodes that satisfy property φ saf e versus parameter r.

We presented STREL, a formal specification language to express and to monitor spatiotemporal requirements over a dynamic network of spatially-distributed CPS. Our monitoring framework considers the CPS topological configuration as a weighted graph with the nodes modeling the CPS entities while the edges representing their arrangement according to predefined spatial relations (e.g. proximity relation, connectivity, Euclidean distance, etc.).

Both nodes and edges contain attributes that model physical and logical quantities that can change over time. STREL combines the Signal Temporal Logic [MN04] with two spatial operators reach and escape that are interpreted over the weighted graph. Other spatial modalities such as everywhere, somewhere and surround can also be derived from them. We demonstrated how STREL can be interpreted according to different semantics (Boolean, realvalued), defining a unified framework capturing all of them, based on constraint semirings. We provided a generic offline monitoring algorithm based on such semiring formulation, providing also correctness proofs and discussing in detail its algorithmic complexity. We showed several examples of requirements that we can monitor in our framework, considering two different case studies. As future works, first, we aim to design a distributed and online monitoring procedure where the spatio-temporal signal is not known at the beginning, and it is discovered while data are collected from the system; some preliminary results on this line can be found [VBLN21] . Second, we aim to extend our framework with new features such as the possibility to synthesize automatically spatio-temporal controllers from the STREL specification or to provide automatically an explanation of the failure, enabling us to detect the responsible components when a STREL requirement is violated.

Timed regular expressions

A formal methods approach to pattern synthesis in reaction diffusion systems

Neural network-based control for multi-agent systems from spatio-temporal specifications

Handbook of Spatial Logics

Voronoi diagrams&mdash;a survey of a fundamental geometric data structure

A formal methods approach to pattern recognition and synthesis in reaction diffusion networks

Spatial logics and model checking for medical imaging

MoonLight: A lightweight tool for monitoring spatio-temporal properties

Monitoring mobile and spatially distributed cyber-physical systems

Studying emergent behaviours in morphogenesis using signal spatio-temporal logic

Mathematical Models in Epidemiology

Cristinel Mateis, Dejan Nickovic, and Xin Qin. Mining shape expressions from positive examples

Semiring-based constraint satisfaction and optimization

Spatio-temporal model checking of vehicular movement in public transport systems

Specifying and verifying properties of space

Spatial logic and spatial model checking for closure spaces

The early phase of the COVID-19 outbreak in

Sur la sphère vide. a la mémoire de georges voronoï

Efficient robust monitoring for STL

sometimes" and "not never" revisited: On branching versus linear time

Quad trees: A data structure for retrieval on composite keys

The mereotopology of discrete space

SpaTeL: a novel spatial-temporal logic and its applications to networked systems

Exploring network structure, dynamics, and function using networkx

An algebraic framework for runtime verification

Quantitative mu-calculus and CTL defined over constraint semirings

Epidemiology and transmission dynamics of COVID-19 in two Indian states. preprint, Epidemiology

Some thoughts on runtime verification

SaSTL: Spatial aggregation signal temporal logic for runtime monitoring in smart cities

A novel spatialtemporal specification-based monitoring system for smart cities

Mining interpretable spatio-temporal logic properties for spatially distributed systems

Monitoring temporal properties of continuous signals

Monitoring properties of analog and mixed-signal circuits

Monitoring spatio-temporal properties (invited tutorial)

Qualitative and quantitative monitoring of spatio-temporal properties

Qualitative and quantitative monitoring of spatio-temporal properties with SSTL

Epidemic processes in complex networks

A roadmap toward the resilient internet of things for cyber-physical systems

Online monitoring of spatiotemporal properties for imprecise signals

This research has been partially supported by the Austrian FWF projects ZK-35 and W1255-N23, by the Italian PRIN project "SEDUCE" n. 2017TWRCNB, by the Italian PRIN project "IT-MaTTerS" n. 2017FTXR7S, and by POR MARCHE FESR 2014-2020, project "MIRACLE", CUP B28I19000330007.