* This paper is an extended version of the ”Monitoring mobile and spatially distributed cyber-physical systems” manuscript published at MEMOCODE 2017.

# A Logic for Monitoring Dynamic Networks of Spatially-distributed Cyber-
Physical Systems*

Ezio Bartocci  TU Wien, Austria<EMAIL_ADDRESS>,  Luca Bortolussi
University of Trieste, Italy<EMAIL_ADDRESS>,  Laura Nenzi  TU Wien,
Austria and University of Trieste, Italy<EMAIL_ADDRESS>and
Michele Loreti  University of Camerino, Italy<EMAIL_ADDRESS>
###### Abstract.

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 others 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 understanding of how
complex behaviors can emerge from local and dynamic interactions.

We propose here the Spatio-Temporal Reach and Escape Logic, (STREL), a logic-
based formal language designed to express and to 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 have attributes modelling 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 a qualitative and quantitative semantics based on
constraint semirings, an algebraic structure suitable for constraint
satisfaction and optimisation. 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.

###### Key words and phrases:

Spatio-Temporal Logic, Monitoring, Cyber-Physical Systems

##  1\. Introduction

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 the humans and other
software systems to inter-operate with them through the World Wide Web.

A prominent example can be found in the modern automotive systems where the
extensive integration of sensor networks and embedded computational units has
lead to the development of various driving assistance features that facilitate
the driver during repetitive maneuvers and protect the passengers from
hazardous situations. Furthermore, the upcoming 5G networks will empower soon
vehicles also with the possibility to exchange information among each other
and the road infrastructure about position and speed of vehicles, driving
conditions on a particular road, accidents, or traffic jams. Thus, this
dynamic network infrastructure promises to enhance further autonomous driving
applications, to reduce traffic congestion and to improve safety.

The rise of this disrupting and revolutionary technology comes at a price:
these systems are becoming so ubiquitous that unexpected failures can
potentially manifest causing fatal accidents and diminishing the trust of the
public opinion. Their safety-critical nature [RKG+19] requires the engineers
to verify their correct execution with respect to rigorously defined spatial
and temporal requirements. Detecting anomalies and failures at design time is
extremely challenging. Exhaustive verification techniques such as model
checking are limited to very small instances due to state-space explosion. A
more practical approach is to simulate a digital replica of the CPS (its
digital twin) and to test the behaviour 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. This approach, called also _specification-based monitoring_ [BDD+18],
is nowadays the core functionality of several other computer-aided
verification and design techniques for CPS such as statistical model checking
[YS06, BMS16, DLL+11], falsification analysis [SPB17, YF17, SKC+17, AFS+13],
failure explanation/debugging [BFMN18, BMM+19, BMM+20] and parameter synthesis
[DKR09, DCLL09, BMS15, BBNS15].

The majority of specification languages and tools available for CPS supports
only the monitoring of temporal properties. Examples are Metric Temporal Logic
(MTL) [Koy90], Signal Temporal Logic (STL) [MN13b, Mal16], Timed Regular
Expressions (TRE) [ACM02] and Shape Expressions [BDG+20]. However, spatio-
temporal patterns plays 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 [NBB+20], and how to efficiently
detect/monitor them on the actual CPS or on the simulation of its digital
twin.

In this paper, we present the Spatio-Temporal Reach and Escape Logic (STREL),
a spatio-temporal specification language originally introduced in [BBLN17] and
recently supported by the MoonLight [BBL+20] tool. STREL enables the
specification of spatio-temporal requirements and their monitoring over the
execution of mobile and spatially distributed components. In this framework,
space is represented as a weighted graph, describing the topological
configurations in which the single components (nodes of the graph) are
arranged. Both nodes and edges have attributes modelling physical and logical
quantities that can change in time. STREL extends Signal Temporal Logic [MN04]
with two spatial operators _reach_ and _escape_ from which is possible to
derive other spatial modalities such as _everywhere_ , _somewhere_ and
_surround_. These operators enable a monitoring procedure where the
satisfaction of the property at each location depends only on the satisfaction
of its neighbours. Furthermore, we show how STREL can be interpreted according
different semantics (Boolean, real-valued) semantics based on constraint
semirings, an algebraic structure suitable for constraint satisfaction and
optimisation.

The use of STREL is by no means restricted to CPS as 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, GBB14,
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.

##  2\. Related Work

Monitoring spatial-temporal properties over CPS executions was initially
addressed in [Tal08] where Talcott introduced the notion of spatial-temporal
event-based model. In this model, actions (e.g. the exchange of messages, or a
physical changes) are labeled with time and space stamps and they trigger
events that are further processed by a monitor. In [TVG09] the model was
further extended to enable different space representations. Although the
approaches in [Tal08, TVG09] provide a valuable algorithmic framework, they
lack a specification language and the monitors cannot be automatically
generated. In the context of _collective adaptive systems_ [CLLM16], several
mathematical structures such as _topological spaces_ , _closure spaces_ ,
_quasi-discrete closure spaces_ and _finite graphs_ [NBC+15] have been
employed to reason about spatial relations (e.g. _closeness_ and
_neighborhood_) of interacting agents. Another line of research in [GSC+09,
HJK+15, GBB14] proposed the use of _quad-trees_ spatial structures [FB74] in
[GSC+09, HJK+15, GBB14] to reason about fractal-like spatial patterns or
spatial superposition properties in a grid, such as electrical spiral
formation in cardiac tissues [GSC+09] or power management requirements in a
smart grid [HJK+15]. However, quad-trees are spatial data structures that are
not invariant with respect to isometric transformations such as translation,
rotation and reflection: two spatial patterns that are equivalent modulo an
isometric transformation are usually represented by two different quad-trees.
To overcome this limitation, in our approach we have considered weighted
graphs where the edges represent the spatial relations between the involved
entities.

Spatial logics have been the subject of theoretically investigation since at
least almost a couple of decades [APHvB07]. The work in [APHvB07] focuses on
theoretically investigation, expressivity and decidability, often in
continuous space. Less attention has been placed on more practical aspects,
especially in the verification procedures. For example, model checking
techniques for spatial models have been considered more recently. In [CLLM14],
the authors introduce a Spatial Logic for Closure Spaces (SLCS) that leverages
a discrete and topological notion of space, based on closure spaces [Gal99].
An extension of the SLCS with temporal aspects, as “snapshot” models, was
proposed later in [CGG+18]. This extends SLCS with the temporal modality of
the branching logic Computation Tree Logic [EH83]. However, the algorithms to
check snapshot models are very computational expensive and are susceptible to
state-space explosion problems because the spatial formulae need to be
recomputed at every state. It is also worth mentioning VoxLogicA [BCLM19,
BBC+20] a recently developed a spatial model checking tool for image analysis.
However, this tool is not suitable to monitor CPS, because it is specialized
for medical imaging and does not take into consideration time.

Relevant works are also those on spatial logics for process algebra with
locations such as in [CC03, CG00], or spatial logic for rewrite theories
[BM12]. Other logic-based formalisms have been introduced to reason about the
topological [BCWZ02] or directional [BSM+10] aspects of locally interacting
components. In the topological approach [BCWZ02], the entities are sets of
points in the space and the relation between them is preserved under
translation, scaling and rotation. If the relation between objects depends on
their relative position then the spatial model supports the directional
reasoning. These logics are highly computationally complex [BSM+10] or even
undecidable [MR99] and indeed impractical to use.

Monitoring spatial-temporal behaviors has recently started to receive more
attention with several works such as 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 is the unification of Signal Temporal Logic
[MN04] (STL) and Tree Spatial Superposition Logic (TSSL) introduced in [GBB14]
to classify and detect spatial patterns that are expressed using quad trees
[FB74]. This allows one to capture very complex spatial structures, but at the
price of a complex formulation of spatial properties, which are in practice
only learned from some template images. SSTL instead combines STL with two
spatial modalities, one expressing that something is true _somewhere_ nearby
and the other capturing the notion of being _surrounded_ by a region that
satisfies a given spatio-temporal property. SSTL has two possible semantics a
Boolean and a real-valued one. SSTL [NBC+18] operates over a static
topological space while STREL on the contrary can monitor entities over a
dynamic topological space. Furthermore, STREL generalizes SSTL spatial
modalities with the _reach_ and _escape_ operators, simplifying the monitoring
that can be computed locally with respect to each node. SaSTL [MBL+20, MBL+21]
is recently proposed specification language that augment STL with two new
logical operators for expressing spatial aggregation and spatial counting
characteristics that are typical in monitoring spatio-temporal requirements in
a smart city. Similarly to SSTL, also SaSTL operates only on a static
topological space. Finally, 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). Moreover, it opens our framework to
the possibility to define new semantics for STREL by just defining and
plugging-in a new semiring algebraic structure but without the need to
redefine the monitoring algorithm.

##  3\. Running Example: A Mobile ad hoc sensor network

A mobile ad-hoc sensor network (MANET) can consist of up ten thousands of
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, a 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
each other if their Euclidean distance is at most their communication range as
depicted in Fig. 1 (right) . Moreover, the nodes can be of different type and
their behaviour 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 behaviours.

Figure 1. Proximity graph (left) and Connectivity graph (right)

##  4\. Spatial Models, Signals and Traces

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_. This is an algebraic structure that consists of a
domain and two operations named _choose_ and _combine_. Constraint semirings
are subclass of semirings which have been shown to be very flexible,
expressive and convenient for a wide range of problems, in particular for
optimisation and solving problems with soft constraints and multiple criteria
[BMR97], and in model checking [LM05].

######  Definition (semiring).

A _semiring_ is a tuple $\langle A,\oplus,\otimes,\bot,\top\rangle$ composed
by a set $A$, two operators $\oplus$, $\otimes$ and two constants $\bot$,
$\top$ such that:

  * •

$\oplus:A\times A\rightarrow A$ is an associative, commutative operator to
“choose” among values111We let $x\oplus y$ to denote $\oplus(\\{x,y\\})$.,
with $\bot$ as unit element ($\bot\oplus a=a,\forall a\in A$).

  * •

$\otimes:A\times A\rightarrow A$ is an associative operator to “combine”
values with $\top$ as unit element ( $\top\otimes a=a,\forall a\in A$) and
$\bot$ as absorbing element ($\bot\otimes a=\bot,\forall a\in A$ )

  * •

$\otimes$ distributes over $\oplus$;

######  Definition (constraint semiring).

A _constraint semiring_ is a semiring $\langle
A,\oplus,\otimes,\bot,\top\rangle$ such that:

  * •

$\oplus$ is defined over $2^{A}$, idempotent ( $a\in A$ $a\oplus a=a\otimes
a=a$) and has $\top$ as absorbing element ( $\top\oplus a=\top$)

  * •

$\otimes$ is commutative

  * •

$\sqsubseteq$, which is defined as $a\sqsubseteq b$ iff $a\oplus b=b$,
provides a complete lattice $\langle A,\sqsubseteq,\bot,\top\rangle$.

We say that a _constraint semiring_ $A$ is _idempotent_ if and only if also
the combine operator $\otimes$ is idempotent, i.e. $a=a\otimes a=a$. Moreover,
we say that a _semiring_ $A$ is _total_ when $\sqsubseteq$ is a _total order_.

With an abuse of notation we sometimes refer to a semiring $\langle
A,\oplus,\otimes,\bot,\top\rangle$ with the carrier $A$ and to its components
by subscripting them with the carrier, i.e., $\oplus_{A}$, $\otimes_{A}$,
$\bot_{A}$ and $\top_{A}$. For the sake of a lighter notation we drop the
subscripts when clear from the context.

######  Example.

Typical examples of semirings are222We use $\mathbb{R}^{\infty}$ (resp.
$\mathbb{N}^{\infty}$) to denote $\mathbb{R}\cup\\{-\infty,+\infty\\}$ (resp.
$\mathbb{N}\cup\\{\infty\\}$).:

  * •

the Boolean semiring
$\langle\\{\mathit{true},\mathit{false}\\},\vee,\wedge,\mathit{false},\mathit{true}\rangle$;

  * •

the tropical semiring $\langle\mathbb{R}_{\geq
0}^{\infty},\emph{min},+,+\infty,0\rangle$;

  * •

the max/min semiring:
$\langle\mathbb{R}^{\infty},\emph{max},\emph{min},-\infty,+\infty\rangle$ ;

  * •

the integer semiring:
$\langle\mathbb{N}^{\infty},\emph{max},\emph{min},0,+\infty\rangle$.

Boolean, max/min and integer semirings are _idempotent_ while tropical
semiring is not. 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_ $\langle A\times
B,(\bot_{A},\bot_{B}),(\top_{A},\top_{B}),\oplus,\otimes\rangle$ 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 a symmetric
relation).

######  Definition ($A-$spatial model).

An $A-$_spatial model_ $\mathcal{S}$ is a pair $\langle L,\mathbf{W}\rangle$
where:

  * •

$L$ is a set of _locations_ , also named _space universe_ ;

  * •

$\mathbf{W}\subseteq L\times A\times L$ is a _proximity function_ associating
at most one label $w\in A$ with each distinct pair $\ell_{1},\ell_{2}\in L$.

We will use $\mathbb{S}_{A}$ to denote the set of $A$-_spatial models_ , while
$\mathbb{S}^{L}_{A}$ indicates the set of $A$-_spatial models_ having $L$ as a
set of locations. In the following, we will equivalently write
$(\ell_{1},w,\ell_{2})\in\mathbf{W}$ as $\mathbf{W}(\ell_{1},\ell_{2})=w$ or
$\ell_{1}\stackrel{{\scriptstyle w}}{{\mapsto}}\ell_{2}$, saying that
$\ell_{1}$ is _next to_ $\ell_{2}$ with weight $w\in A$.

######  Example.

$\mathbb{R}_{\geq 0}^{\infty}$-spatial model on _tropical semiring_ (see
Example Example) can be used to represent standard weighed graphs as Figure 2.
$L$ is the set of nodes and the proximity function $\mathbf{W}$ defines the
weight of the edges, e.g.
$\mathbf{W}(\ell_{2},\ell_{7})=\mathbf{W}(\ell_{7},\ell_{2})=5$

$\ell_{1}$$\ell_{2}$$\ell_{3}$$\ell_{4}$$\ell_{5}$$\ell_{6}$$\ell_{7}$$\ell_{8}$$\ell_{9}$215143723
Figure 2. Example of a weighted undirected graph; e.g.
$\mathbf{W}(\ell_{2},\ell_{7})=\mathbf{W}(\ell_{7},\ell_{2})=5$

A special class of spatial models are the ones based on _Euclidean spaces_.

######  Definition (Euclidean spatial model).

Let $L$ be a set of locations, $R\subseteq L\times L$ a (reflexive) relation
and $\lambda:L\rightarrow\mathbb{R}^{2}$ a function mapping each location to a
point in $\mathbb{R}^{2}$, we let $\mathcal{E}(L,R,\lambda)$ be the
$\mathbb{R}^{\infty}\times\mathbb{R}^{\infty}$-spatial
model333$\mathbb{R}^{\infty}$ is the _max/min_ semiring considered in Example
Example. $\langle L,\mathbf{W}^{\lambda,R}\rangle$ such that:

$\mathbf{W}^{\lambda,R}=\\{(\ell_{1},\lambda(\ell_{1})-\lambda(\ell_{2}),\ell_{2})|(\ell_{1},\ell_{2})\in
R\\}$

Note that we label edges with a 2-dimensional vector $w$ describing how to
reach $\ell_{2}$ from $\ell_{1}$, i.e.,
$\lambda(\ell_{1})-w=\lambda(\ell_{2})$. This obviously allows us to compute
the euclidean distance between $\ell_{1}$ and $\ell_{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.

######  Example.

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 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 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 Definition:
$\mathbf{W}^{\mu,R}(\ell_{i},\ell_{j})=\mu(\ell_{i})-\mu(\ell_{j})=(x_{i},y_{i})-(x_{j},y_{j})=(x_{i}-x_{j},y_{i}-y_{j})$,
where $(x_{i},y_{i})$ are the plane coordinates of the location $\ell_{i}$.

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

Given an $A$-spatial model we can define _routes_.

######  Definition (route).

Let $\mathcal{S}=\langle L,\mathbf{W}\rangle$, a _route_ $\tau$ is an infinite
sequence $\ell_{0}\ell_{1}\cdots\ell_{k}\cdots$ in $L^{\omega}$ such that for
any $i\geq 0$, $\ell_{i}\stackrel{{\scriptstyle d}}{{\mapsto}}\ell_{i+1}$.

Let $\tau=\ell_{0}\ell_{1}\cdots\ell_{k}\cdots$ be a route, $i\in\mathbb{N}$
and $\ell_{i}\in L$, we use:

  * •

$\tau[i]$ to denote the $i$-th node $\ell_{i}$ in $\tau$;

  * •

$\tau[i..]$ to indicate the suffix route $\ell_{i}\ell_{i+1}\cdots$;

  * •

$\ell\in\tau$ when there exists an index $i$ such that $\tau[i]=\ell$, while
we use $\ell\not\in\tau$ if this index does not exist;

  * •

$\tau(\ell)$ to denote the first occurrence of $\ell$ in $\tau$:

$\tau(\ell)=\left\\{\begin{array}[]{ll}\min\\{i|\tau[i]=\ell\\}&\mbox{if
$\ell\in\tau$}\\\ \infty&\mbox{otherwise}\\\ \end{array}\right.$

We also use $Routes(\mathcal{S})$ to denote the set of routes in
$\mathcal{S}$, while $Routes(\mathcal{S},\ell)$ denotes the set of routes
starting from $\ell\in 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$.

######  Definition (Distance Domain).

We say that _distance domain_ $(B,\bot_{B},\top_{B},+_{B},\leq_{B})$ whenever
$\leq_{B}$ is a total order relation over $B$ where $\bot_{B}$ is the minimum
while $\top_{B}$ is the maximum and $(B,\bot_{B},+_{B})$ is a monoid. Given a
distance domain $B$, we will use $\bot_{B}$, $\top_{B}$, $+_{B}$ and
$\leq_{B}$ to denote its elements.

######  Definition (Distance Function and Distance over paths).

Let $\mathcal{S}=\langle L,\mathbf{W}\rangle$ be an $\mathcal{S}=\langle
L,\mathbf{W}\rangle$ be an $A$-spatial model, $\tau$ a route in $\mathcal{S}$,
$\langle B,\bot_{B},\top_{B},+_{B},\leq_{B}\rangle$ a _distance domain_ , we
call $f:A\rightarrow B$ the _distance function_ , associating elements of $A$
to the distance domain $B$. The distance $d_{\tau}^{f}[i]$ up-to index
$i\in\mathbb{N}^{\infty}$ is defined as follows:

$d_{\tau}^{f}[i]=\begin{cases}\bot_{B}&i=0\\\ \infty&i=\infty\\\
f(w)+_{B}d_{\tau[1..]}^{f}[i-1]&(i>0)\mbox{ and
}\tau[0]\stackrel{{\scriptstyle w}}{{\mapsto}}\tau[1]\end{cases}\\\ $

Given a locations $\ell\in L$, the distance over $\tau$ up-to $\ell$ is then
$d_{\tau}^{f}[\ell]=d_{\tau}^{f}[\tau(\ell)]$ if $\ell\in\tau$, while it is
$\top_{B}$ if $\ell\not\in\rho$.

######  Example.

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.

To count the number of hop, we can simply use the function
$hop:A\rightarrow\mathbb{N}^{\infty}$, taking values in the distance domain
$\langle\mathbb{N}^{\infty},0,\infty,+,\leq\rangle$,:

$hop(w)=1$

and in this case $d^{hop}_{\tau}[i]=i$.

Considering the proximity function $\mathbf{W}^{\mu,R}(\ell_{i},\ell_{j})$
computed from the Cartesian coordinates and the distance domain
$\langle\mathbb{R}^{\infty},0,\infty,+,\leq\rangle$, we can use the Euclidean
distance $\Delta(x,y)=\|(x,y)\|$, where $(x,y)$ are the coordinates of the
vectors returned by $\mathbf{W}^{\mu,R}$.

It is easy to see that for any route $\tau$ and for any location $\ell\in L$
in $\tau$, the function $d_{\tau}^{\Delta}(\ell)$ yields the sum of lengths of
the edges in $\mathbb{R}^{2}$ connecting $\ell$ to $\tau(0)$.

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

$d^{f}_{\mathcal{S}}[\ell_{1},\ell_{2}]=\min\left\\{d^{f}_{\tau}[\ell_{2}]|\tau\in
Routes(\mathcal{S},\ell_{1})\right\\}.$

######  Example.

Consider again the distance functions defined for a MANETS. For _hop_ , we are
taking the minimum hop-length over all paths connecting $\ell_{1}$ and
$\ell_{2}$, resulting in the shortest path distance.

###  4.3. Spatio-Temporal Signals

######  Definition.

A _signal domain_ is a tuple $\langle D,\oplus,\otimes,\odot,\bot,\top\rangle$
where:

  * •

$\langle D,\oplus,\otimes,\bot,\top\rangle$, is an _idempotent semiring_ ;

  * •

$\odot:D\rightarrow D$, is a _negation function_ such that:

    * –

$\odot\top=\bot$;

    * –

$\odot\bot=\top$;

    * –

$\odot(v_{1}\oplus v_{2})=(\odot v_{1})\otimes(\odot v_{2})$

    * –

$\odot(v_{1}\otimes v_{2})=(\odot v_{1})\oplus(\odot v_{2})$

    * –

for any $v\in D$, $\odot(\odot v)=v$.

In this paper we will consider two _signal domains_ :

  * •

Boolean signal domain
$\langle\\{\top,\bot\\},\vee,\wedge,\neg,,\bot,\top,\rangle$ for qualitative
monitoring;

  * •

Max/min signal domain
$\langle\mathbb{R}^{\infty},\max,\min,-,\bot,\top,\rangle$ for quantitative
monitoring.

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

######  Definition.

Let $\mathbb{T}=[0,T]\subseteq\mathbb{R}_{\geq 0}$ a time domain and $\langle
D,\oplus,\otimes,\odot,\bot,\top\rangle$ a _signal domain_ , a _temporal
$D$-signal_ $\nu$ is a function $\nu:\mathbb{T}\rightarrow D$.

Consider a finite sequence:

$\tilde{\nu}=[(t_{0},d_{0}),\ldots,(t_{n},d_{n})]$

such that for $\forall i,t_{i}\in\mathbb{T}$, $t_{i}<t_{i+1}$ and $d_{i}\in
D$. We let $\tilde{\nu}$ denote a _piecewise constant temporal $D$-signal_ in
$\mathbb{T}=[t_{0},T]$, that is

$\tilde{\nu}(t)=\begin{cases}&d_{i}\quad\text{ for }t_{i}\leq t<t_{i+1},\\\
&d_{n}\quad\text{ for }t_{n}\leq t\leq T;\end{cases}\\\ $

Given a _piecewise constant temporal signal_
$\tilde{\nu}=[(t_{0},d_{0}),\ldots,(t_{n},d_{n})]$ we will use
$\mathcal{T}(\tilde{\nu})$ to denote the set $\\{t_{0},\ldots,t_{n}\\}$ of
_time steps_ in $\tilde{\nu}$; $start(\tilde{\nu})$ to denote $t_{0}$; while
we will say that $\tilde{\nu}$ is _minimal_ if and only if for any $i$,
$d_{i}\not=d_{i+1}$. We will also let $\tilde{\nu}[t=d]$ to denote the signal
obtained from $\tilde{\nu}$ by adding the element $(t,d)$. Finally, if
$\nu_{1}$ and $\nu_{2}$ are two $D$-temporal signals, and $op:D\times
D\rightarrow D$, $\nu_{1}~{}op~{}\nu_{2}$ denotes the signal associating with
each time $t$ the value $\nu_{1}(t)~{}op~{}\nu_{2}(t)$. Similarly, if
$op:D_{1}\rightarrow D_{2}$, $op~{}\nu_{1}$ denotes the $D_{2}-$signal
associating with $t$ the value $op~{}\nu_{1}(t)$.

######  Definition (Spatial $D$-signal).

Let $L$ be a _space universe_ , and $\langle
D,\oplus,\otimes,\odot,\bot,\top\rangle$ a signal domain. A _spatial
$D$-signal_ is a function $\mathbf{s}:L\rightarrow D$.

######  Definition (Spatio-temporal $D$-signal).

Let $L$ be a space universe, $\mathbb{T}=[0,T]$ a time domain, and $\langle
D,\oplus,\otimes,\odot,\top,\bot\rangle$ a signal domain, a spatio-temporal
$D$-signal is a function

$\sigma:L\rightarrow\mathbb{T}\rightarrow D$

such that $\sigma(\ell)=\nu$ is a temporal signal that returns a value
$\nu(t)\in{D}$ for each time $t\in\mathbb{T}$. We say that $\sigma$ is
_piecewise constant_ when for any $\ell$, $\sigma(\ell)$ is a _piecewise
constant temporal signal_. _Piecewise constants_ signal are denoted by
$\tilde{\sigma}$. Moreover, we will use $\mathcal{T}(\tilde{\sigma})$ to
denote $\bigcup_{\ell}\mathcal{T}(\tilde{\sigma}(\ell))$. Finally, we let
$\tilde{\sigma}@t$ denote the spatial signal associating each location $\ell$
with $\tilde{\sigma}(\ell,t)$.

Given a spatio-temporal signal $\sigma$, we will use $\sigma@t$ to denote the
_spatial signal_ at time $t$, i.e. the signal $\mathbf{s}$ such that
$\mathbf{s}(\ell)=\sigma(\ell)(t)$, for any $\ell\in L$. Different kinds of
signals can be considered while the signal domain $D$ is changed. Signals with
$D=\\{true,false\\}$ are called _Boolean signals_ ; with
$D=\mathbb{R}^{\infty}$ are called real-valued or _quantitative signals_.

######  Definition ($D$-Trace).

Let $L$ be a space universe, a spatio-temporal $D$-trace is a function
$\vec{x}:L\rightarrow\mathbb{T}\rightarrow D_{1}\times\cdots\times D_{n}$ such
that for any $\ell\in L$ yields a vector of temporal signals
$\vec{x}(\ell)=(\nu_{1},\ldots,\nu_{n})$. In the rest of the paper we will use
$\vec{x}(\ell,t)$ to denote $\vec{x}(\ell)(t)$.

######  Example.

We can consider a $(\mathbb{R}\times\mathbb{R})$-spatio-temporal trace of our
sensor network as
$\vec{x}:L\rightarrow\mathbb{T}\rightarrow\mathbb{R}\times\mathbb{R}$ that
associates a set of temporal signals $\vec{x}(\ell)=(\nu_{B},\nu_{T})$ at each
location, where $\nu_{B}$ and $\nu_{T}$ respectively correspond to the
temporal signals of the battery and the temperature in location $\ell$, and
each signal has domain $\langle\mathbb{R},\max,\min,-,\bot,\top,\rangle$.

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 (Dynamical $A$-Spatial Model).

Let $L$ be a spatial universe, a dynamical $A$-spatial model is a function
$\mathcal{S}:\mathbb{T}\rightarrow\mathbb{S}^{L}_{A}$ associating each element
in the time domain $\mathbb{T}$ with $A$-spatial model $\mathcal{S}(t)=\langle
L,\mathbf{W}\rangle$ that describes the spatial configuration of locations.

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

######  Example.

Let us considering a MANET with a proximity graph. Figure 3 shows two
different snapshots, $\mathcal{S}(t_{1})=\langle L,\mathbf{W}_{1}\rangle$ and
$\mathcal{S}(t_{2})=\langle L,\mathbf{W}_{2}\rangle$, of the the dynamical
spatial model $S$ for time $t_{1}$ and $t_{2}$. We can see that locations
$\ell_{1}$ and $\ell_{2}$ change their position, this changed also the Voronoi
diagram and the proximity graph.

Figure 3. Two snapshots of a spatial model with 7 locations
$\ell_{1},\dots,\ell_{7}$ that move in a 2D Euclidian space. The plane is
partitioned using a Voronoi Diagram ( blue). In  red we have the proximity
graph.

##  5\. Spatio-temporal Reach and Escape Logic

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

$\varphi:=\mu\mid\neg\varphi\mid\varphi_{1}\wedge\varphi_{2}\mid\varphi_{1}\>\mathrm{U}_{[t_{1},t_{2}]}\>\varphi_{2}\mid\varphi_{1}\>\mathrm{S}_{[t_{1},t_{2}]}\>\varphi_{2}\mid\varphi_{1}\>\mathcal{R}_{[d_{1},d_{2}]}^{f:A\rightarrow
B}\>\varphi_{2}\mid\mathcal{E}_{[d_{1},d_{2}]}^{f:A\rightarrow B}\>\varphi$

where $\mu$ is an atomic predicate ($AP$), negation $\neg$ and conjunction
$\wedge$ are the standard Boolean connectives, $\mathrm{U}_{[t_{1},t_{2}]}$
and $\mathrm{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 [MN13a, MN04,
DFM13]. The spatial modalities are the reachability
$\mathcal{R}_{[d_{1},d_{2}]}^{f:A\rightarrow B}$ and the escape
$\mathcal{E}_{[d_{1},d_{2}]}^{f:A\rightarrow B}$ operators, with
$f:A\rightarrow B$ a _distance function_ (see Definition Example), $B$ a
_distance domain_ , and $d_{1},d_{2}\in B$ with $d_{1}\leq_{B}d_{2}$. In what
follows we will 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 $\phi_{1}\mathcal{R}_{[d_{1},d_{2}]}^{f}\phi_{2}$
describes the behaviour of reaching a location satisfying property $\phi_{2}$,
with a distance from the initial location belongs to $[d_{1},d_{2}]$, passing
only through locations that satisfy $\phi_{1}$. The escape operator
$\mathcal{E}_{[d_{1},d_{2}]}^{f}{\phi}$, instead, describes the possibility of
escaping from a certain region via a route passing only through locations that
satisfy $\phi$, with distance between the starting location of the path and
the last that belongs to the interval $[d_{1},d_{2}]$.

As customary, we can derive the disjunction operator $\vee$ and the future
eventually $\mathrm{F}_{[t_{1},t_{2}]}$ and always
$\mathrm{G}_{[t_{1},t_{2}]}$ operators from the until temporal modality, and
the corresponding past variants from the since temporal modality, see [MN13a]
for details. We can define also other three derived spatial operators: the
somewhere $\diamonddiamond_{\leq d}^{f:A\rightarrow B}\phi$ and the everywhere
$\boxbox_{\leq d}^{f:A\rightarrow B}\phi$ 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
$\phi_{2}$-region, while being in a $\phi_{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 each location.
We stress that each STREL formula $\varphi$ abstracts from the specific domain
used to express the satisfaction value of $\varphi$. 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
Definition.

######  Definition (Semantics).

Let $\mathcal{S}$ be a dynamical $A$-spatial model, $D_{1}$ and $D_{2}$ be two
signal domains, $\vec{x}$ be a spatio-temporal $D_{1}$-trace for $L$ and
$\mathcal{S}$ a dynamical spatial model. The $D_{2}$-monitoring function
$\mathbf{m}$ of $\vec{x}$ is recursively defined in Table 1.

$\mathbf{m}(\mathcal{S},\vec{x},\mu,t,\ell)$ | $=$ | $\iota(\mu,\vec{x}(\ell,t))$
---|---|---
$\mathbf{m}(\mathcal{S},\vec{x},\neg\varphi,t,\ell)$ | $=$ | $\odot_{D_{2}}\mathbf{m}(\mathcal{S},\vec{x},\varphi,t,\ell)$
$\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1}\wedge\varphi_{2},t,\ell)$ | $=$ | $\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1},t,\ell)\otimes_{D_{2}}\mathbf{m}(\mathcal{S},\vec{x},\varphi_{2},t,\ell)$
$\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1}\>\mathrm{U}_{[t_{1},t_{2}]}\>\varphi_{2},t,\ell)$ | $=$ | ${\bigoplus_{D_{2}}}_{t^{\prime}\in[t+t_{1},t+t_{2}]}\big{(}\mathbf{m}(\mathcal{S},\vec{x},\varphi_{2},t^{\prime},\ell)\otimes_{D_{2}}{\bigotimes_{D_{2}}}_{t^{\prime\prime}\in[t,t^{\prime}]}\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1},t^{\prime\prime},\ell)\big{)}$
$\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1}\>\mathrm{S}_{[t_{1},t_{2}]}\>\varphi_{2},t,\ell)$ | $=$ | ${\bigoplus_{D_{2}}}_{t^{\prime}\in[t-t_{2},t-t_{1}]}\big{(}\mathbf{m}(\mathcal{S},\vec{x},\varphi_{2},t^{\prime},\ell)\otimes_{D_{2}}{\bigotimes_{D_{2}}}_{t^{\prime\prime}\in[t^{\prime},t]}\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1},t^{\prime\prime},\ell)\big{)}$
$\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1}\>\mathcal{R}_{[d_{1},d_{2}]}^{f:A\rightarrow B}\>\varphi_{2},t,\ell)$ | $=$ |
${\bigoplus_{D_{2}}}_{\tau\in
Routes(\mathcal{S}(t),\ell)}~{}~{}{\bigoplus_{D_{2}}}_{i:\left(d_{\tau}^{f}[i]\in[d_{1},d_{2}]\right)}\left(\mathbf{m}(\mathcal{S},\vec{x},\varphi_{2},t,\tau[i])\otimes_{D_{2}}{\bigotimes_{D_{2}}}_{j<i}\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1},t,\tau[j])\right)$
$\mathbf{m}(\mathcal{S},\vec{x},\mathcal{E}_{[d_{1},d_{2}]}^{f:A\rightarrow B}\>\varphi,t,\ell)$ | $=$ | ${\bigoplus_{D_{2}}}_{\tau\in Routes(\mathcal{S}(t),\ell)}~{}~{}{\bigoplus_{D_{2}}}_{\ell^{\prime}\in\tau:\left(d_{\mathcal{S}(t)}^{f}[\ell,\ell^{\prime}]\in[d_{1},d_{2}]\right)}~{}~{}{\bigotimes_{D_{2}}}_{i\leq\tau(\ell^{\prime})}\mathbf{m}(\mathcal{S},\vec{x},\varphi,t,\tau[i])$
Table 1. Monitoring function.

Given a formula $\phi$, the function
$\mathbf{m}(\mathcal{S},\vec{x},\phi,t,\ell)$ corresponds to the evaluation of
the formula at time $t$ in the location $\ell$. The procedure will be 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:
$\mathbb{B}$ and $\mathbb{R^{\infty}}$, giving rise to qualitative and
quantitative monitoring, corresponding respectively to a Boolean answer value
and real satisfaction value. For the Boolean signal domain
($D_{2}=\langle\\{\top,\bot\\},\vee,\wedge,\neg\rangle$ ), we say that
$(\mathcal{S},\vec{x}(\ell,t))$ satisfies a formula $\phi$ iff
$\mathbf{m}(\mathcal{S},\vec{x},\phi,t,\ell)=\top$. For max/min signal domain
$\langle\mathbb{R}^{\infty},\max,\min,-,\bot,\top,\rangle$ we say that
$(\mathcal{S},\vec{x}(\ell,t))$ satisfies a formula $\phi$ iff
$\mathbf{m}(\mathcal{S},\vec{x},\phi,t,\ell)>0$. In the following, we will use
$\tilde{\sigma}^{\mathcal{S},\vec{x}}_{\phi}$ to denote the spatio-temporal
$D_{2}$-signal such that for any $t$ and $\ell$
$\mathbf{m}(\mathcal{S},\vec{x},\phi,t,\ell)=\tilde{\sigma}^{\mathcal{S},\vec{x}}_{\phi}(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 will use the
graph in Figure 4 to describe the spatial operators.

######  Example (ZigBee protocol).

In Fig. 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
$({\color[rgb]{0.3,0.615,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.615,0.3}coord})$,
represented in green color in the graph, is unique in each network and is
responsible to initialize the network. After the initialisation of the network
has started, the coordinator behaves as a router. The Router node
$({\color[rgb]{0.65,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.65,0.3,0.3}router})$,
represented in red color in the graph, acts as a intermediate router, passing
on data from other devices. The EndDevice node
$({\color[rgb]{0.3,0.3,0.615}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.615}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
$\\{{\color[rgb]{0.3,0.615,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.615,0.3}coord},{\color[rgb]{0.65,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.65,0.3,0.3}router},{\color[rgb]{0.3,0.3,0.615}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.615}end\\_dev}\\}\times\mathbb{R}$-trace
$\vec{x}:L\rightarrow\mathbb{T}\rightarrow\mathbb{Z}\times\mathbb{R}^{\infty}$
denoting the pair: (kind of node, level of battery), i.e.
$\vec{x}(\ell,t)=({\color[rgb]{0.3,0.615,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.615,0.3}coord},b)$
if $\ell$ is a coordinator,
$\vec{x}(\ell,t)=({\color[rgb]{0.65,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.65,0.3,0.3}router},b)$
if $\ell$ is a router, and
$\vec{x}(\ell,t)=({\color[rgb]{0.3,0.3,0.615}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.615}end\\_dev},b)$
if $\ell$ is an end node, where $b$ is the level of the battery.

Atomic Proposition. The function $\iota:AP\times D_{1}^{n}\rightarrow 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},\dots,p_{n}\\}=AP$ and an interpretation function
$\iota(p_{i},\vec{x}(\ell,t))=\top$ iff $x_{i}(\ell,t)=\top$. In Fig. 4, we
can consider atomic propositions describing the type of node, i.e., the
Boolean propositions
$\\{{\color[rgb]{0.3,0.615,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.615,0.3}coord},{\color[rgb]{0.65,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.65,0.3,0.3}router},{\color[rgb]{0.3,0.3,0.615}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.615}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
$\mu=(g(\vec{x})\geq 0)$ for some real function $g$ and define
$\iota(\mu,\vec{t,\ell})=g(\vec{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
$\odot_{D_{2}}$ of the chosen signal domain; e.g.
$\mathbf{m}(\mathcal{S},\vec{x},\neg\varphi,t,\ell)=\neg\mathbf{m}(\mathcal{S},\vec{x},\varphi,t,\ell)$
for the Boolean signal domain and
$\mathbf{m}(\mathcal{S},\vec{x},\neg\varphi,t,\ell)=-\mathbf{m}(\mathcal{S},\vec{x},\varphi,t,\ell)$
for the quantitative ones.

Conjunction and Disjunction The conjunction operator
$\varphi_{1}\wedge\varphi_{2}$ is interpreted with $\otimes_{D_{2}}$,
$\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1}\wedge\varphi_{2},t,\ell)=\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1},t,\ell)\otimes_{D_{2}}\mathbf{m}(\mathcal{S},\vec{x},\varphi_{2},t,\ell)$,
which corresponds to wedge $\wedge$ operator for the Boolean semantics. This
means that
$\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1}\wedge\varphi_{2},t,\ell)=1$ iff
both $\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1})$ and
$\mathbf{m}(\mathcal{S},\vec{x},\varphi_{2})$ are equal to 1. For the
quantitative semantics $\otimes_{D_{2}}$ is interpreted ad the minimum
operator, so $\otimes_{D_{2}}$,
$\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1}\wedge\varphi_{2},t,\ell)=\min(\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1},t,\ell),\mathbf{m}(\mathcal{S},\vec{x},\varphi_{2},t,\ell))$.
Similarly the disjunction $\varphi_{1}\vee\varphi_{2}$ is interpreted through
the $\oplus_{D_{2}}$ operator, i.e. $\otimes_{D_{2}}$,
$\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1}\vee\varphi_{2},t,\ell)=\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1},t,\ell)\oplus_{D_{2}}\mathbf{m}(\mathcal{S},\vec{x},\varphi_{2},t,\ell)$,
which corresponds to the $\vee$ 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}=\langle\\{\top,\bot\\},\vee,\wedge,\neg\rangle$, the Quantitative
semantics can be derived substituting $\vee,\wedge$ with $\min,\max$, as seen
for conjunction and disjunction.

Until.

$\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1}\>\mathrm{U}_{[t_{1},t_{2}]}\>\varphi_{2},t,\ell)=\bigvee_{t^{\prime}\in
t+[t_{1},t_{2}]}\linebreak(\mathbf{m}(\mathcal{S},\vec{x},\varphi_{2},t^{\prime},\ell)\wedge\bigwedge_{t^{\prime\prime}\in[t,t^{\prime}]}\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1},t^{\prime\prime},\ell)\big{)}.$

As customary, $(\mathcal{S},\vec{x}(\ell,t))$ satisfies
$\varphi_{1}\>\mathrm{U}_{[t_{1},t_{2}]}\>\varphi_{2}$ iff it satisfies
$\varphi_{1}$ from $t$ until, in a time between $t_{1}$ and $t_{2}$ time units
in the future, $\varphi_{2}$ becomes true. Note how the temporal operators are
evaluated in each location separately.

Since.

$\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1}\>\mathrm{S}_{[t_{1},t_{2}]}\>\varphi_{2},t,\ell)=\bigvee_{t^{\prime}\in
t-[-t_{2},-t_{1}]}\linebreak\big{(}\mathbf{m}(\mathcal{S},\vec{x},\varphi_{2},t^{\prime},\ell)\wedge\bigwedge_{t^{\prime\prime}\in[t^{\prime},t]}\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1},t^{\prime\prime},\ell)\big{)}$

$(\mathcal{S},\vec{x}(\ell,t)$ satisfies
$\varphi_{1}\>\mathrm{S}_{[t_{1},t_{2}]}\>\varphi_{2}$ iff it satisfies
$\varphi_{1}$ from now since, in a time between $t_{1}$ and $t_{2}$ time units
in the past, $\varphi_{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
$\mathbb{R}^{\infty}$ signal domain), see [MN04, DFM13] for details.

Reachability.

$\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1}\>\mathcal{R}_{[d_{1},d_{2}]}^{f}\>\varphi_{2},t,\ell)=\bigvee_{\tau\in
Routes(\mathcal{S}(t),\ell)}\linebreak\bigvee_{i:\left(d_{\tau}^{f}[i]\in[d_{1},d_{2}]\right)}(\mathbf{m}(\mathcal{S},\vec{x},\varphi_{2},t,\tau[i])\wedge\bigwedge_{j<i}\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1},t,\tau[j]))$

$(\mathcal{S},\vec{x}(\ell,t))$ satisfies
$\varphi_{1}\>\mathcal{R}_{d}^{f}\>\varphi_{2}$ iff it satisfies $\varphi_{2}$
in a location $\ell^{\prime}$ reachable from $\ell$ through a route $\tau$,
with a length $d_{\tau}^{f}[\ell^{\prime}]$ belonging to the interval
$[d_{1},d_{2}]$, and such that $\tau[0]=\ell$ and all its elements with index
less than $\tau(\ell^{\prime})$ satisfy $\varphi_{1}$. In Figure 4, we report
an example of reachability property, considering f as the $hop$ function
described in Example Example. In the graph, the location $\ell_{6}$ (meaning
the trajectory $\vec{x}$ at time t in position $\ell_{6}$) satisfies
${\color[rgb]{0.3,0.3,0.615}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.615}end\\_dev}\>\mathcal{R}_{[0,1]}^{hop}\>{\color[rgb]{0.65,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.65,0.3,0.3}router}$.
Indeed, there exists a route $\tau=\ell_{6}\ell_{5}$ such that
$d_{\tau}^{hop}[1]=1$, where $\tau[0]=\ell_{6}$, $\tau[1]=\ell_{5}$, $\tau[1]$
satisfies the red property (it is a router) and all the other elements of the
route satisfy the blue property (they are end-devices). Instead, for example,
the location $\ell_{8}$ does not satisfy the property because it does not
satisfies the blue (end-device) property.

Escape.

$\mathbf{m}(\mathcal{S},\vec{x},\mathcal{E}_{[d_{1},d_{2}]}^{f}\>\varphi,t,\ell)=\bigvee_{\tau\in
Routes(\mathcal{S}(t),\ell)}\linebreak\bigvee_{\ell^{\prime}\in\tau:\left(d_{\lambda(t)}^{f}[\ell,\ell^{\prime}]\in[d_{1},d_{2}]\right)}~{}\bigwedge_{i\leq\tau(\ell^{\prime})}\mathbf{m}(\mathcal{S},\vec{x},\varphi,t,\tau[i]).$

$(\mathcal{S},\vec{x}(\ell,t))$ satisfies $\mathcal{E}_{d}^{f}\>\varphi$ if
and only if there exists a route $\tau$ and a location $\ell^{\prime}\in\tau$
such that $\tau[0]=\ell$ and $d_{\mathcal{S}}[\tau[0],\ell^{\prime}]$ belongs
to the interval $[d_{1},d_{2}]$, while $\ell^{\prime}$ and all the elements
$\tau[0],...\tau[k-1]$ (with $\tau(\ell^{\prime})=k$) satisfy satisfies
$\varphi$. In Fig 4, we report an example of escape property. In the graph,
the location $\ell_{10}$ satisfies
$\mathcal{E}_{[2,\infty]}^{hop}\>\neg{\color[rgb]{0.3,0.3,0.615}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.615}end\\_dev}$.
Indeed, there exists a route $\tau=\ell_{10}\ell_{7}\ell_{8}$ such that
$\tau[0]=\ell_{10}$, $\tau[2]=\ell_{8}$, $d_{S}^{hop}[\ell_{10},\ell_{1}]=2$
and $\ell_{10}$, $\ell_{7}$ and $\ell_{8}$ do not satisfy the blue property,
i.e. they are not end-devices. Note that the route $\ell_{10}\ell_{9}$ is not
a good route to satisfy the property because the distance
$d_{S}^{hop}[\ell_{10},\ell_{9}]=1$.

12345678910111213141516 Figure 4.  Example of spatial properties.
Reachability:
${\color[rgb]{0.3,0.3,0.615}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.615}end\\_dev}\>\mathcal{R}_{[0,1]}^{hop}\>{\color[rgb]{0.65,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.65,0.3,0.3}router}$.
Escape:
$\mathcal{E}_{[2,\infty]}^{hop}\>\neg{\color[rgb]{0.3,0.3,0.615}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.615}end\\_dev}$.
Somewhere:
$\diamonddiamond_{[0,4]}^{hop}{\color[rgb]{0.3,0.615,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.615,0.3}coord}$.
Everywhere:
$\boxbox_{[0,2]}^{hop}{\color[rgb]{0.65,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.65,0.3,0.3}router}$.
Surround:
$({\color[rgb]{0.3,0.615,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.615,0.3}coord}\vee{\color[rgb]{0.65,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.65,0.3,0.3}router})\circledcirc_{[0,3]}^{hop}\>{\color[rgb]{0.3,0.3,0.615}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.615}end\\_dev}$.

We can also derive other three spatial operators: somewhere, everywhere and
surround.

Somewhere.
$\diamonddiamond_{[0,d]}^{f}\varphi:=true\mathcal{R}_{[0,d]}^{f}\varphi$ is
satisfied by $(\mathcal{S},x(t,\ell))$ iff there exists a location that
satisfies $\varphi$ reachable from $\ell$ via a route $\tau$ with a distance
belonging to the interval $[0,d]$. This length is computed via the function
$f$. In Fig. 4, all the locations satisfy the property
$\diamonddiamond_{[0,4]}^{hop}{\color[rgb]{0.3,0.615,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.615,0.3}coord}$
because, for all $\ell_{i}$, there is always a path
$\tau=\ell_{i}\dots\ell_{10}$ with a length $d_{\tau}^{hop}(k)<4$, where
$\tau[0]=\ell_{i}$, $\tau[k]=\ell_{10}$, and $\ell_{10}$ satisfies the green
property.

Everywhere.
$\boxbox_{[0,d]}^{f}\varphi:=\neg\diamonddiamond_{[0,d]}^{f}\neg\varphi$ is
satisfied by $(\mathcal{S},\vec{x}((\ell,t))$ iff all the locations reachable
from $\ell$ via a path, with length belonging to the interval $[0,d]$, satisfy
$\varphi$. In Fig. 4, there are no locations that satisfy the property
$\boxbox_{[0,2]}^{hop}{\color[rgb]{0.65,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.65,0.3,0.3}router}$
because for all the locations $\ell_{i}$ there is a path
$\tau=\ell_{i}\ell_{j}$ s.t. $\ell_{j}$ does not satisfy the red property.

Surround.
$\varphi_{1}\circledcirc_{[0,d]}^{f}\varphi_{2}:=\varphi_{1}\wedge\neg(\varphi_{1}\mathcal{R}_{[0,d]}^{f}\neg(\varphi_{1}\vee\varphi_{2})\wedge\neg(\mathcal{E}_{\neg[d,\infty]}^{f}\varphi_{1})$
expresses the topological notion of being surrounded by a
$\varphi_{2}$-region, while being in a $\varphi_{1}$-region, with an
additional metric constraint. The operator has been introduced in [CLLM16] as
a basic operator, while here it is a derived one. The idea is that one cannot
escape from a $\varphi_{1}$-region without passing from a location that
satisfies $\varphi_{2}$ and, in any case, one has to reach a
$\varphi_{2}$-location via a path with a length less or equal to $d$. In Fig.
4, the location $\ell_{10}$ satisfies the property
$({\color[rgb]{0.3,0.615,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.615,0.3}coord}\>\vee\>{\color[rgb]{0.65,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.65,0.3,0.3}router})\circledcirc_{[0,3]}^{hop}\>{\color[rgb]{0.3,0.3,0.615}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.615}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 .

###  5.2. 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 change of
coordinates, i.e. with respect to isometric transformations of the plane This
class of transformations include translations, rotations, and reflections, and
can be described by matrix multiplications of the form

$\begin{bmatrix}x^{\prime}_{\ell}\\\ y^{\prime}_{\ell}\\\ 1\\\
\end{bmatrix}=\begin{bmatrix}\beta\cos(\alpha)&-\beta\sin(\alpha)&\beta
t_{x}\\\ \gamma\sin(\alpha)&\gamma\cos(\alpha)&\gamma t_{y}\\\
0&0&1\end{bmatrix}\begin{bmatrix}x_{\ell}\\\ y_{\ell}\\\ 1\\\ \end{bmatrix}$

Invariance of satisfaction of spatial properties holds in STREL logic, for the
Euclidean space model of Definition Definition. Consider more specifically an
Euclidean space model $\mathcal{E}(L,\mu,R)=\langle
L,\mathbf{W}^{\mu,R}\rangle$ and $\mathcal{E}(L,\mu^{\prime},R)=\langle
L,\mathbf{W}^{\mu^{\prime},R}\rangle$, obtained by applying an isometric
transformation $A$: $\mu^{\prime}(\ell)=A(\mu(\ell))$. 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
$\mathbb{R}^{\infty}\times\mathbb{R}^{\infty}$ 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}\leq 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
$\mathcal{E}(L,\mu,R)$ and $\mathcal{E}(L,\mu^{\prime},R)$ is also the same.
This straightforwardly implies that the truth value of spatial operators will
be unchanged by isometry.

######  Proposition (Equisatisfiability under isometry).

Let $\mathcal{E}(L,\mu,R)=\langle L,\mathbf{W}^{\mu,R}\rangle$ be an euclidean
spatial model and $\mathcal{E}(L,\mu^{\prime},R)=\langle
L,\mathbf{W}^{\mu^{\prime},R}\rangle$ an isometric transformation of the
former. Consider a spatial formula
$\varphi_{1}\>\mathcal{R}_{d}^{f}\>\varphi_{2}$ or
$\mathcal{E}_{d}^{f}\>\varphi_{1}$, where $d$ is an isometry preserving
predicate. Assume
$\mathbf{m}(\mathcal{S},\vec{x},\varphi_{j},t,\ell)=\mathbf{m}^{\prime}(\mathcal{S},\vec{x},\varphi_{j},t,\ell)$,
$j=1,2$, where $\mathbf{m}$ and $\mathbf{m}^{\prime}$ are the monitoring
functions for the two spatial models. Then it holds that
$\mathbf{m}(\mathcal{S},\vec{x},\varphi_{1}\>\mathcal{R}_{d}^{f}\>\varphi_{2},t,\ell)=\mathbf{m}^{\prime}(\mathcal{S},\vec{x},\varphi_{1}\>\mathcal{R}_{d}^{f}\>\varphi_{2},t,\ell)$
and
$\mathbf{m}(\mathcal{S},\vec{x},\mathcal{E}_{d}^{f}\>\varphi_{1},t,\ell)=\mathbf{m}^{\prime}(\mathcal{S},\vec{x},\mathcal{E}_{d}^{f}\>\varphi_{1},t,\ell)$,
for all $\ell$ and $t$.

##  6\. Monitoring STREL

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. At the end of this section we will also briefly discuss a possible
alternative approach that can lead to a distributed and _online_ monitoring
procedure. In this case, the spatio-temporal signal is not known at the
beginning, and it is discovered while data are collected from the system while
it is running.

###  6.1. Offline monitor

Offline monitoring is performed via a function $\mathsf{monitor}$ that takes
as inputs a dynamical spatial model $\mathcal{S}$, a trace $\vec{x}$ and a
formula $\phi$ and returns the _piecewise constant spatio-temporal signal_
$\tilde{\sigma}$ representing the monitoring of $\phi$. Function
$\mathsf{monitor}$ is defined by induction on the syntax of the formula
(Algorithm 1). The spatio-temporal signal resulting from the monitoring of
atomic proposition $\mu$ is just obtained by applying function $\iota(\mu)$ to
the trace $\mathbf{x}$. The spatio-temporal signals associated with
$\neg\varphi$ and $\varphi_{1}\wedge\varphi_{2}$ are obtained by applying
operators $\odot_{D_{2}}$ and $\otimes_{D_{2}}$ to the signals resulting from
the monitoring of $\varphi$ and from the monitoring of $\varphi_{1}$ and
$\varphi_{2}$ where $\oplus_{D_{2}}$, $\otimes_{D_{2}}$ and $\odot_{D_{2}}$
depend the _signal domain_ used to represent satisfaction values.

Algorithm 1 Monitoring algorithm

1:function Monitor($\mathcal{S}$, $\vec{x}$, $\psi$)

2: case $\psi=\nu$

3: $\tilde{\sigma}=[]$

4: for all $\ell\in L$ do

5: for all $t\in\mathcal{T}(\vec{x}(\ell))$ do

6: $\tilde{\sigma}(\ell,t)=\iota(\mu)(\vec{x}(\ell,t))$

7: end for

8: end for

9: return $\tilde{\sigma}$

10: case $\psi=\neg\psi_{1}$

11: $\tilde{\sigma}_{1}=\textsc{Monitor}(\mathcal{S},\vec{x},\psi_{1})$

12: $\tilde{\sigma}=[]$

13: for all $\ell\in L$ do

14: for all $t\in\mathcal{T}(\tilde{\sigma}_{1}(\ell))$ do

15: $\tilde{\sigma}(\ell,t)=\odot_{D_{2}}\tilde{\sigma}_{1}(\ell,t)$

16: end for

17: end for

18: return $\tilde{\sigma}$

19: case $\psi=\psi_{1}\wedge\psi_{2}$

20: $\tilde{\sigma}_{1}=\textsc{Monitor}(\mathcal{S},\vec{x},\psi_{1})$

21: $\tilde{\sigma}_{2}=\textsc{Monitor}(\mathcal{S},\vec{x},\psi_{2})$

22: $\tilde{\sigma}=[]$

23: for all $\ell\in L$ do

24: for all
$t\in\mathcal{T}(\tilde{\sigma}_{1}(\ell))\cup\mathcal{T}(\tilde{\sigma}_{2}(\ell))$
do

25:
$\tilde{\sigma}(\ell,t)=\tilde{\sigma}_{1}(\ell,t)\otimes_{D_{2}}\tilde{\sigma}_{2}(\ell,t)$

26: end for

27: end for

28: return $\tilde{\sigma}$

29: case $\psi=\psi_{1}\mathrm{U}_{[t1,t2]}\psi_{2}$

30: $\tilde{\sigma}_{1}=\textsc{Monitor}(\mathcal{S},\vec{x},\psi_{1})$

31: $\tilde{\sigma}_{2}=\textsc{Monitor}(\mathcal{S},\vec{x},\psi_{2})$

32: $\tilde{\sigma}=[]$

33: for all $\ell\in L$ do

34:
$\tilde{\sigma}(\ell)=\textsc{Until}(t1,t2,\tilde{\sigma}_{1}(\ell),\tilde{\sigma}_{2}(\ell))$

35: end for

36: return $\tilde{\sigma}$

37: case $\psi=\psi_{1}\mathrm{S}_{[t1,t2]}\psi_{2}$

38: $\tilde{\sigma}_{1}=\textsc{Monitor}(\mathcal{S},\vec{x},\psi_{1})$

39: $\tilde{\sigma}_{2}=\textsc{Monitor}(\mathcal{S},\vec{x},\psi_{2})$

40: $\tilde{\sigma}=[]$

41: for all $\ell\in L$ do

42:
$\tilde{\sigma}(\ell)=\textsc{Since}(t1,t2,\tilde{\sigma}_{1}(\ell),\tilde{\sigma}_{2}(\ell))$

43: end for

44: return $\tilde{\sigma}$

45: case $\psi=\psi_{1}\mathcal{R}_{[d_{1},d_{2}]}^{f}\psi_{2}$

46: $\tilde{\sigma}_{1}=\textsc{Monitor}(\mathcal{S},\vec{x},\psi_{1})$

47: $\tilde{\sigma}_{2}=\textsc{Monitor}(\mathcal{S},\vec{x},\psi_{2})$

48: $\tilde{\sigma}=[]$

49: for all
$t\in\mathcal{T}(\tilde{\sigma}_{1})\cup\mathcal{T}(\tilde{\sigma}_{2})$ do

50:
$\tilde{\sigma}@t=\textsc{Reach}(\mathcal{S}(t),f,d_{1},d_{2},\tilde{\sigma}_{1}@t,\tilde{\sigma}_{2}@t)$

51: end for

52: return $\tilde{\sigma}$

53: case $\psi=\psi_{1}\mathcal{E}_{d}^{f}\psi_{2}$

54: $\tilde{\sigma}_{1}=\textsc{Monitor}(\mathcal{S},\vec{x},\psi_{1})$

55: $\tilde{\sigma}_{2}=\textsc{Monitor}(\mathcal{S},\vec{x},\psi_{2})$

56: $\tilde{\sigma}=[]$

57: for all
$t\in\mathcal{T}(\tilde{\sigma}_{1})\cup\mathcal{T}(\tilde{\sigma}_{2})$ do

58:
$\tilde{\sigma}@t=\textsc{Escape}(\mathcal{S}(t),f,d,\tilde{\sigma}_{1}@t,\tilde{\sigma}_{2}@t)$

59: end for

60: return $\tilde{\sigma}$

61:end function

Monitoring of temporal properties, namely
$\varphi_{1}\mathrm{U}_{[t_{1},t_{2}]}\varphi_{2}$ and
$\varphi_{1}\mathrm{S}_{[t_{1},t_{2}]}\varphi_{2}$, relies on functions Until
and Since. These are defined by using the same approach of [DFM13] and
[MN13a]. However, while their monitoring relies on classical Boolean and
arithmetic operators, here the procedure is parametrised with respect to
operators $\oplus_{D_{2}}$ and $\otimes_{D_{2}}$ of the considered semiring.

Algorithm 2 Monitoring function for _reach_ operator

1:function Reach($(L,\mathbf{W})$, $f:A\rightarrow B$, $d_{1}\in B$, $d_{2}\in
B$, $\mathbf{s}_{1}:L\rightarrow D_{2}$, $\mathbf{s}_{2}:L\rightarrow D_{2}$)

2: if $d_{2}\not=\top_{B}$ then

3: return BoundedReach($(L,\mathbf{W})$, $f$, $d_{1}$, $d_{2}$ ,
$\mathbf{s}_{1}$, $\mathbf{s}_{2}$)

4: else

5: return UnboundedReach($(L,\mathbf{W})$, $f$, $d_{1}$, $\mathbf{s}_{1}$,
$\mathbf{s}_{2}$)

6: end if

7:end function

To monitor $\varphi_{1}\>\mathcal{R}_{[d_{1},d_{2}]}^{f:A\rightarrow
B}\>\varphi_{2}$ we first compute the signals $\mathbf{s}_{1}$ and
$\mathbf{s}_{2}$, resulting from the monitoring of $\varphi_{1}$ and
$\varphi_{2}$. After that, the final result is obtained by aggregating the
spatial signals $\mathbf{s}_{1}@t$ and $\mathbf{s}_{2}@t$ at each time
$t\in\mathcal{T}(\mathbf{s}_{1})\cup\mathcal{T}(\mathbf{s}_{2})$ by using
function Reach defined in Algorithm 2. In this function two cases are
distinguished: $d_{2}\not=\top_{B}$ or $d_{2}=\top_{B}$. In the first case,
the resulting monitoring value is calculated via function BoundedReach defined
in Algoritm 3. Conversely, when $d_{2}=\top_{B}$ monitoring is performed by
relying on function UnoundedReach defined in Algoritm 4.

#### BoundedReach

Function BoundedReach, defined in Algorithm 3, takes as parameters the spatial
model $\langle L,\mathbf{W}\rangle$ at time $t$, the function $f:A\rightarrow
B$, used to compute the distances over paths, and the interval
$[d_{1},d_{2}]$, describing the reachability bound. The proposed algorithm is
based on a flooding that computes the output signal $\mathbf{s}$. At line $3$,
we inizialite the set $Q$, it contains all triples
$(\ell,s_{2}[\ell],\bot_{B})$, where $\bot_{B}$ is the minimum element of the
distance domain $B$ (e.g. if $B=\mathbb{R}_{\geq 0}$, $\bot_{B}=0$). Let us
denote $Q_{i}$ the value of $Q$ after $i$ iterations of loop starting at line
$4$. $Q_{i}$ contains a triple $(\ell,v,d)$ if and only if there exists a path
such that with $i$-steps we reach a distance $d<_{B}d_{2}$ and a monitored
value $v$. To compute the values in $Q_{i+1}$, for each element $(\ell,v,d)\in
Q_{i}$ we consider the locations $\ell^{\prime}$ next to $\ell$ at a distance
$w$ ($\ell^{\prime}\stackrel{{\scriptstyle w}}{{\mapsto}}\ell$) to compute the
items: $v^{\prime}=v\otimes\mathbf{s}_{1}(\ell^{\prime})$ and
$d^{\prime}=d+_{B}f(w)$. The element $(\ell^{\prime},v^{\prime},d^{\prime})$
is added to $Q_{i+1}$ if $d^{\prime}<_{B}d_{2}$, i.e. if the sum of the
current distance plus the distance between $\ell$ and $\ell^{\prime}$ is still
less than $d_{2}$. When $d^{\prime}\in[d_{1},d_{2}]$,
$\mathbf{s}(\ell^{\prime})$ is updated to take into account the new computed
value. We recal that $s$ stores the value of the semantics of the reach
operator.

Algorithm 3 Monitoring bounded reachability

1:function BoundedReach($(L,\mathbf{W})$, $f:A\rightarrow B$, $d_{1}\in
B$,$d_{2}\in B$, $\mathbf{s}_{1}:L\rightarrow D_{2}$,
$\mathbf{s}_{2}:L\rightarrow D_{2}$)

2: $\forall\ell\in
L.\mathbf{s}[\ell]=\left\\{\begin{array}[]{ll}\mathbf{s}_{2}[\ell]&d_{1}=\bot_{B}\\\
\bot_{D_{2}}&\mbox{otherwise}\end{array}\right.$

3: $Q=\\{(\ell,\mathbf{s}_{2}[\ell],\bot_{B})|\ell\in L\\}$

4: while $Q\not=\emptyset$ do

5: $Q^{\prime}=\emptyset$

6: for all $(\ell,v,d)\in Q$ do

7: for all $\ell^{\prime}:\ell^{\prime}\stackrel{{\scriptstyle
w}}{{\mapsto}}\ell$ do

8: $v^{\prime}=v~{}\otimes_{D_{2}}~{}\mathbf{s}_{1}[\ell^{\prime}]$

9: $d^{\prime}=d~{}+_{B}~{}f(w)$

10: if $(d_{1}\leq d^{\prime}\leq d_{2})$ then

11:
$\mathbf{s}[\ell^{\prime}]=\mathbf{s}[\ell^{\prime}]\oplus_{D_{2}}v^{\prime}$

12: end if

13: if $d^{\prime}<d_{2}$ then

14: if $\exists(\ell^{\prime},v^{\prime\prime},d^{\prime})\in Q^{\prime}$ then

15:
$Q^{\prime}=(Q^{\prime}-\\{(\ell^{\prime},v^{\prime\prime},d^{\prime})\\})\cup\\{(\ell^{\prime},v^{\prime}\oplus_{D_{2}}v^{\prime\prime},d^{\prime})\\}$

16: else

17: $Q^{\prime}=Q^{\prime}\cup\\{(\ell^{\prime},v^{\prime},d^{\prime})\\}$

18: end if

19: end if

20: end for

21: end for

22: $Q=Q^{\prime}$

23: end while

24: return $\mathbf{s}$

25:end function

#### UnboundedReach

Function UnboundedReach defined in Algoritm 4 is used when the interval in the
_reach_ formula is unbounded. In this case the function takes as parameters
the spatial model $\langle L,\mathbf{W}\rangle$ at time $t$, the function
$f:A\rightarrow B$, used to compute the distances over paths, and the lower
bound $d_{1}$, and returns a _spatial signal_ $\mathbf{s}$. If
$d_{1}=\bot_{B}$, i.e. when we are considering a totally unbound reach with no
constraint,s we initialize $\mathbf{s}=\mathbf{s}_{2}$. Otherwise, when
$d_{1}\not=\bot$, 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 $\mathbf{W}$. After that, $\mathbf{s}$
will contain the _reachability_ value computed up to the bound
$[d_{1},d_{1}+d_{max}]$ (lines (5)-(6)). Hence, the computed values are _back
propagated_ until a fix point is reached. This will guarantee that for each
location, only the values of $\mathbf{s}_{2}$ at a path distance
$[d_{1},\top_{B}]$ are considered in computation of reachability values.

Algorithm 4 Monitoring unbounded reachability

1:function UnboundedReach($(L,\mathbf{W})$, $f:A\rightarrow B$, $d_{1}\in B$,
$\mathbf{s}_{1}:L\rightarrow D_{2}$, $\mathbf{s}_{2}:L\rightarrow D_{2}$)

2: if $d_{1}=\bot_{B}$ then

3: $\mathbf{s}=\mathbf{s}_{2}$

4: else

5: $d_{max}=\max\\{f(w)|\exists.\ell,\ell^{\prime}\in
L:\ell\stackrel{{\scriptstyle w}}{{\mapsto}}\ell^{\prime}\\}$

6:
$\mathbf{s}=\textsc{BoundedReach}((L,\mathbf{W}),f,d_{1},d_{1}+_{B}d_{max},\mathbf{s}_{1},\mathbf{s}_{2})$

7: end if

8: $T=L$

9: while $T\not=\emptyset$ do

10: $T^{\prime}=\emptyset$

11: for all $\ell\in T$ do

12: for all $\ell^{\prime}:\ell^{\prime}\stackrel{{\scriptstyle
w}}{{\mapsto}}\ell$ do

13:
$v^{\prime}=(\mathbf{s}[\ell]\otimes_{D_{2}}\mathbf{s}_{1}[\ell^{\prime}])\oplus_{D_{2}}\mathbf{s}[\ell^{\prime}]$

14: if $v^{\prime}\not=\mathbf{s}[\ell^{\prime}]$ then

15: $\mathbf{s}[\ell^{\prime}]=v^{\prime}$

16: $T^{\prime}=T^{\prime}\cup\\{\ell^{\prime}\\}$

17: end if

18: end for

19: end for

20: $T=T^{\prime}$

21: end while

22: return $\mathbf{s}$

23:end function

#### Escape

Monitoring algorithm for $\mathcal{E}_{[d_{1},d_{2}]}^{f:A\rightarrow
B}{\varphi}$ is reported in Algorithm 5. Given a spatial model $\langle
L,\mathbf{W}\rangle$ at time $t$, a distance function $f:A\rightarrow B$, an
interval $[d_{1},d_{2}]$, it computes the spatial signal representing the
monitoring value of $\mathcal{E}_{d}^{f}\varphi$ at time $t$. Function
$\mathsf{escape}$ first computes the _matrix distance_ $D$ (line 2), obtained
from the given space model and distance function $f$. After that, a matrix
$e:L\times L\rightarrow D_{2}$ is computed. The matrix $e$ is initialised so
that all the elements $e[\ell,\ell]$ in the diagonal are equal to
$\mathbf{s}_{1}(\ell)$, while all the other elements are set to $\bot_{D_{2}}$
(lines 3-4). After that, iteratively, elements of $e$ are updated by
considering the values in the neighbours in each location (lines 6-20). A
value $e[\ell_{1}^{\prime},\ell_{2}]$ is updated iff
$\mathbf{s}_{1}(\ell_{1}^{\prime})\otimes_{D_{2}}e[\ell_{1},\ell_{2}]>_{D_{2}}e[\ell_{1}^{\prime},\ell_{2}]$,
where $\ell_{1}^{\prime}$ is a neighbored of $\ell_{1}$. The updates ends when
a fixpoint is reached 444We prove that the loop always terminates in Lemma
Lemma.. At the end of the loop computation, the element $e[\ell_{1},\ell_{2}]$
contains the _escape_ value from $\ell_{1}$ to $\ell_{2}$, defined in the
semantics without the distance constraint. This latter is took in
consideration in line 23, where the final monitored value $s$ is computed. For
each $\ell$, the equation
$\bigoplus_{D_{2}}(\\{e[\ell,\ell^{\prime}]|D[\ell,\ell^{\prime}]\in[d_{1},d_{2}]\\})$
considers the minimum values $e[\ell,\ell^{\prime}]$ of all $\ell^{\prime}$
that satisfies the distance contraint, i.e. such that
$D[\ell,\ell^{\prime}]\in[d_{1},d_{2}]$.

Algorithm 5 Monitoring _escape_

1:function Escape($(L,\mathbf{W})$, $f:A\rightarrow B$, $d_{1}\in B$,$d_{2}\in
B$, $\mathbf{s}_{1}:L\rightarrow D_{2}$)

2: $D=\textsc{MinDistance}(L,\mathbf{W},f))$

3: $\forall\ell,\ell^{\prime}\in L.e[\ell,\ell^{\prime}]=\bot_{D_{2}}$

4: $\forall\ell\in L.e[\ell,\ell]=\mathbf{s}_{1}(\ell)$

5: $T=\\{(\ell,\ell)|\ell\in L\\}$

6: while $T\not=\emptyset$ do

7: $e^{\prime}=e$

8: $T^{\prime}=\emptyset$

9: for all $(\ell_{1},\ell_{2})\in T$ do

10: for all $\ell_{1}^{\prime}:\ell_{1}^{\prime}\stackrel{{\scriptstyle
w}}{{\mapsto}}\ell_{1}$ do

11:
$v=e[\ell_{1}^{\prime},\ell_{2}]\oplus_{D_{2}}(\mathbf{s}_{1}(\ell_{1}^{\prime})\otimes_{D_{2}}e[\ell_{1},\ell_{2}])$

12: if $v\not=e[\ell_{1}^{\prime},\ell_{2}]$ then

13: $T^{\prime}=T^{\prime}\cup\\{(\ell_{1}^{\prime},\ell_{2})\\}$

14: $e^{\prime}[\ell_{1}^{\prime},\ell_{2}]=v$

15: end if

16: end for

17: end for

18: T=T’

19: e=e’

20: end while

21: $\mathbf{s}=[]$

22: for all $\ell\in L$ do

23:
$\mathbf{s}(\ell)=\bigoplus_{D_{2}}(\\{e[\ell,\ell^{\prime}]|D[\ell,\ell^{\prime}]\in[d_{1},d_{2}]\\})$

24: end for

25: return $\mathbf{s}$

26:end function

###  6.2. Correctness

In this sub section we discuss the correctness of the algorithms.

######  Lemma (BoundedReach correctness).

Given an $A$-spatial model $\mathcal{S}=(L,\mathbf{W})$, a function
$f:A\rightarrow B$, an interval $[d_{1},d_{2}]$, ($d_{1},d_{2}\in B$,
$d_{1}\leq_{B}d_{2}$ and) $d_{2}\not=\top_{B}$), and two spatial signals
$\mathbf{s}_{1}:L\rightarrow D_{2}$, $\mathbf{s}_{2}:L\rightarrow D_{2}$ such
that
$\textsc{BoundedReach}((L,\mathbf{W}),f,d_{1},d_{2},\mathbf{s}_{1},\mathbf{s}_{2})=\mathbf{s}$.
For any $\ell\in L$, we have that:

$\mathbf{s}(\ell)={\oplus_{D_{2}}}_{\tau\in
Routes(\mathcal{S},\ell)}~{}~{}{\oplus_{D_{2}}}_{i:\left(d_{\tau}^{f}[i]\in[d_{1},d_{2}]\right)}\left(\mathbf{s}_{2}(\tau[i])\otimes_{D_{2}}{\otimes_{D_{2}}}_{j<i}\mathbf{s}_{1}(\tau[j])\right)$

###### Proof.

Let us denote by $\mathbf{s}_{i}$ and $Q_{i}$ the value of variables
$\mathbf{s}$ and $Q$ respectively in Algorithm 3 after $i$ iterations of the
_while-loop_ at line $(4)$. The statement follows directly from the following
properties and by observing that (since $f(w)>0$ for any $w\in A$) the
algorithm terminates after a finite number of iterations:

  1. $P1$:

if $(\ell,v,d)\in Q_{i}$ then $d\leq_{B}d_{2}$;

  2. $P2$:

if $(\ell,v_{1},d)\in Q_{i}$ and $(\ell,v_{2},d)\in Q_{i}$ then $v_{1}=v_{2}$;

  3. $P3$:

$(\ell,v,d)\in Q_{i}$ if and only if

$v={\oplus_{D_{2}}}_{\tau\in
Routes(\mathcal{S},\ell):d_{\tau}^{f}[i]=d}\mathbf{s}_{2}(\tau[i])\otimes_{D_{2}}\left({\otimes_{D_{2}}}_{j<i}\mathbf{s}_{1}(\tau[j])\right)$

  4. $P4$:

for any $\ell\in L$:

$\mathbf{s}_{i}[\ell]={\oplus_{D_{2}}}_{\tau\in
Routes(\mathcal{S},\ell)}~{}~{}{\oplus_{D_{2}}}_{k:k\leq
i\wedge\left(d_{\tau}^{f}[k]\in[d_{1},d_{2}]\right)}\left(\mathbf{s}_{2}(\tau[k])\otimes_{D_{2}}{\otimes_{D_{2}}}_{j<k}\mathbf{s}_{1}(\tau[j])\right)$

Properties $P1$ and $P2$ are direct consequences of instructions at lines
$(3)$ and $(13)-(19)$ of Algorithm 3. Indeed, $(\ell,v,d)\in Q_{0}$ if and
only if $d=\bot_{B}$ (line $(3)$), while $(\ell,v,d)$ is inserted in
$Q^{\prime}=Q_{i+1}$ if and only if $d<_{B}d_{2}$ (line $(13)$) and no other
$(\ell,v^{\prime},d)$ is already in $Q^{\prime}$ (lines $(14)-(18)$).

Property $P3$ can be proved by induction on $i$ by observing that the property
is satisfied by $Q_{0}$ and that for any $i$:

$(\ell^{\prime},v^{\prime},d^{\prime})\in Q_{i+1}\Leftrightarrow
d^{\prime}<_{B}d_{2}\mbox{ and }v^{\prime}={\oplus_{D_{2}}}_{(\ell,v,d)\in
Q_{i}:\ell^{\prime}\stackrel{{\scriptstyle w}}{{\mapsto}}\ell\wedge
d+f(w)=d^{\prime}}\left(\mathbf{s}_{1}(\ell^{\prime})\otimes_{D_{2}}v\right)$

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

$\small\begin{array}[]{rcl}v^{\prime}&=&{\oplus_{D_{2}}}_{(\ell,v,d)\in
Q_{i}:\ell^{\prime}\stackrel{{\scriptstyle w}}{{\mapsto}}\ell\wedge
d+f(w)=d^{\prime}}\left(\mathbf{s}_{1}(\ell^{\prime})\otimes_{D_{2}}{\oplus_{D_{2}}}_{\tau\in
Routes(\mathcal{S},\ell):d_{\tau}^{f}[i]=d}\mathbf{s}_{2}(\tau[i])\otimes_{D_{2}}\left({\otimes_{D_{2}}}_{j<i}\mathbf{s}_{1}(\tau[j])\right)\right)\\\
&=&{\oplus_{D_{2}}}_{\tau\in
Routes(\mathcal{S},\ell^{\prime}):d_{\tau}^{f}[i+1]=d^{\prime}}\mathbf{s}_{2}(\tau[i+1])\otimes_{D_{2}}\left({\otimes_{D_{2}}}_{j<i+1}\mathbf{s}_{1}(\tau[j])\right)\end{array}$

That is the statement of $P3$.

Finally, we can probe $P4$ by induction on $i$ by using $P3$ and by observing
that:

$\mathbf{s}_{i+1}[\ell^{\prime}]={\oplus_{D_{2}}}_{(\ell,v,d)\in
Q_{i}:\ell^{\prime}\stackrel{{\scriptstyle w}}{{\mapsto}}\ell\wedge
d+f(w)\in[d_{1},d_{2}]}\mathbf{s}_{i}[\ell^{\prime}]\oplus_{D_{2}}\left(\mathbf{s}_{1}[\ell^{\prime}]\otimes
v\right)$

∎

######  Lemma (UnboundedReach correctness).

Given an $A$-spatial model $(L,\mathbf{W})$, a function $f:A\rightarrow B$, a
value $d_{1}\in B$ ($d_{1}\not=\top_{B}$), and two spatial signals
$\mathbf{s}_{1}:L\rightarrow D_{2}$, $\mathbf{s}_{2}:L\rightarrow D_{2}$ such
that
$\textsc{UnboundedReach}((L,\mathbf{W}),f,d_{1},\mathbf{s}_{1},\mathbf{s}_{2})=\mathbf{s}$.
For any $\ell\in L$:

$\mathbf{s}(\ell)={\oplus_{D_{2}}}_{\tau\in
Routes(\mathcal{S}(t),\ell)}~{}~{}{\oplus_{D_{2}}}_{\ell^{\prime}\in\tau:\left(d_{\tau}^{f}[\ell^{\prime}]\geq
d_{1}\right)}\left(\mathbf{s}_{2}(\ell^{\prime})\otimes_{D_{2}}{\otimes_{D_{2}}}_{j<\tau(\ell^{\prime})}\mathbf{s}_{1}(\tau[j])\right)$

###### Proof.

Directly from the pseudo code in Algorithm 4 and from Lemma Lemma, we can
observe that the value $\mathbf{s}$ computed by function UnboundedReach is the
limit ($\mathbf{s}=\lim_{i\rightarrow\infty}\mathbf{s}_{i}$) of the sequence
of signals $\mathbf{s}_{i}$ such that for any $\ell\in L$:

$\mathbf{s}_{i+1}[\ell]=\bigoplus_{\ell\in L:\ell\stackrel{{\scriptstyle
w}}{{\mapsto}}\ell^{\prime}}(\mathbf{s}_{i}(\ell)\oplus\mathbf{s}_{1}(\ell^{\prime})\otimes\mathbf{s}_{i}(\ell^{\prime}))$

The initial spatial signal is $\mathbf{s}_{0}=\mathbf{s}_{2}$, if
$d_{1}=\bot_{B}$, while it is:

$\mathbf{s}_{0}[\ell]={\oplus_{D_{2}}}_{\tau\in
Routes(\mathcal{S},\ell)}~{}~{}{\oplus_{D_{2}}}_{i:\left(d_{\tau}^{f}[i]\in[d_{1},d_{1}+d_{max}]\right)}\left(\mathbf{s}_{2}(\tau[i])\otimes_{D_{2}}{\otimes_{D_{2}}}_{j<i}\mathbf{s}_{1}(\tau[j])\right)$

when $d_{1}\not=\bot_{B}$ and
$d_{max}=\max\\{f(w)|\exists.\ell,\ell^{\prime}\in
L:\ell\stackrel{{\scriptstyle w}}{{\mapsto}}\ell^{\prime}\\}$. In both the
cases, the statement follows by applying standard algebra and the properties
of $\oplus$ and $\otimes$. ∎

######  Lemma (Escape correctness).

Given an $A$-spatial model $(L,\mathbf{W})$, a function $f:A\rightarrow B$, an
interval $[d_{1},d_{2}]$, ($d_{1},d_{2}\in B$, $d_{1}\leq_{B}d_{2}$ and)
$d_{2}\not=\top_{B}$), and a spatial signal $\mathbf{s}_{1}:L\rightarrow
D_{2}$ such that
$\textsc{Escape}((L,\mathbf{W}),f,d_{1},d_{2},\mathbf{s}_{1})=\mathbf{s}$. For
any $\ell\in L$:

$\mathbf{s}(\ell)={\bigoplus_{D_{2}}}_{\tau\in
Routes((L,\mathbf{W}),\ell)}~{}~{}{\bigoplus_{D_{2}}}_{\ell^{\prime}\in\tau:\left(d_{(L,\mathbf{W})}^{f}[\ell,\ell^{\prime}]\in[d_{1},d_{2}]\right)}~{}~{}{\bigotimes_{D_{2}}}_{i\leq\tau(\ell^{\prime})}\mathbf{s}_{1}(\tau[i])$

###### 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:

  * $P1$

For any $\ell_{1},\ell_{2}$,
$D[\ell_{1},\ell_{2}]=d_{(L,\mathbf{W})}^{f}[\ell,\ell^{\prime}]$

  * $P2$

For any $i$:

$e_{i}[\ell_{1},\ell_{2}]={\bigoplus_{D_{2}}}_{\tau\in
Routes((L,\mathbf{W}),\ell)}~{}~{}{\bigotimes_{D_{2}}}_{j\leq\tau(\ell^{\prime})\wedge
j\leq i}\mathbf{s}_{1}(\tau[j])$

  * $P3$

The loop terminates after at most $k=|L|$ iterations and

$e_{k}[\ell_{1},\ell_{2}]={\bigoplus_{D_{2}}}_{\tau\in
Routes(\mathcal{S}(t),\ell)}~{}~{}{\bigotimes_{D_{2}}}_{j\leq\tau(\ell^{\prime})}\mathbf{s}_{1}(\tau[j])$

Property $P1$ follows directly from definition of
$d_{(L,\mathbf{W})}^{f}[\ell,\ell^{\prime}]$ and from the fact that
$\mathsf{MinDistance(L,\mathbf{W},f)}$ computes the matrix of min distances
computed in $\langle L,\mathbf{W}\rangle$ via $f$. Property $P2$ can be proved
by induction on $i$ and follows directly from the code of Algorithm 5.
Finally, $P3$ 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 $P1$, $P2$ and $P3$ above by observing that:

$\begin{array}[]{rcl}\mathbf{s}(\ell)&=&\bigoplus_{D_{2}}(\\{e[\ell,\ell^{\prime}]|D[\ell,\ell^{\prime}]\in[d_{1},d_{2}]\\})\\\
&=&\bigoplus_{D_{2}}(\\{e_{k}[\ell,\ell^{\prime}]|D[\ell,\ell^{\prime}]\in[d_{1},d_{2}]\\})\\\
&=&{\bigoplus_{D_{2}}}_{\tau\in
Routes(\mathcal{S}(t),\ell)}~{}~{}{\bigoplus_{D_{2}}}_{\ell^{\prime}\in\tau:\left(d_{(L,\mathbf{W})}^{f}[\ell,\ell^{\prime}]\in[d_{1},d_{2}]\right)}~{}~{}{\bigotimes_{D_{2}}}_{j\leq\tau(\ell^{\prime})}\mathbf{s}_{1}(\tau[j])\end{array}$

∎

######  Theorem.

Given a dynamical spatial model $\mathcal{S}$, a trace $\vec{x}$ and a formula
$\phi$,

$\textsc{Monitor}(\mathcal{S},\vec{x},\phi)=\tilde{\sigma}_{\phi}^{\mathcal{S},\vec{x}}$

###### Proof.

The proof easily follows by induction on $\phi$ by using Lemma Lemma, Lemma
Lemma and Lemma Lemma. ∎

###  6.3. Complexity

In this subsection we discuss the complexity of each algorithms.

######  Proposition (BoundedReach complexity).

Given an $A$-spatial model $\mathcal{S}=(L,\mathbf{W})$, a function
$f:A\rightarrow B$, an interval $[d_{1},d_{2}]$, ($d_{1},d_{2}\in B$,
$d_{1}\leq_{B}d_{2}$ and) $d_{2}\not=\top_{B}$), and two spatial signals
$\mathbf{s}_{1}:L\rightarrow D_{2}$, $\mathbf{s}_{2}:L\rightarrow D_{2}$ such
that
$\textsc{BoundedReach}((L,\mathbf{W}),f,d_{1},d_{2},\mathbf{s}_{1},\mathbf{s}_{2})=\mathbf{s}$.
We define $d_{min}=\min_{(\ell,w,\ell^{\prime})\in\mathbf{W}}(f(w))$ and
$k=\min\\{i|i*d_{min}>d_{2}\\}$, where $i*d_{min}$ indicates the sum of $i$
copies of $d_{min}$, then the algorithm terminates after
$O(k\cdot\beta_{d_{2}}\cdot|L|\cdot m)$ steps, where $m$ is the number of
edges and $\beta_{d_{2}}$ is an integer counting the _different distances_
accumulated after $k$ steps555 This value is in practice a constant and
depends on the weights associated with edges and on the bound $d_{2}$. For
instance, in the case of function $hop$ of Example Example $\beta=1$. In
general, $\beta_{d_{2}}$ has the same order of magnitude as $k$ considered
above..

###### Proof.

First, we need to compute the upper bound on the number of iterations of the
while loop starting at line (4). Let us denote by $Q_{k}$ the value of $Q$
after $k$ iterations. If $Q_{k}=\emptyset$, the loop stops after at most $k$
iterations. $Q_{k}$ is empty if no elements are added at that iteration. An
element $(\ell^{\prime},v^{\prime},d^{\prime})$ is not added to $Q_{k}$ iff
$d^{\prime}\geq d_{2}$ where $d^{\prime}=d+_{B}f(w)\geq d+_{B}d_{min}$ . Note
that, at the first iteration $Q_{0}$, $d=\bot_{B}$. At each iteration, we add
a value greater or equal to $d_{min}$, this means that after $k$ iterations
$d^{\prime}\geq k*d_{min}$ but $k*d_{min}>d_{2}$ for definition. Q can have at
most $\beta_{d_{2}}\cdot|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\cdot\beta_{d_{2}}\cdot|L|\cdot m)$ steps. ∎

######  Proposition (UnBoundedReach complexity).

Given an $A$-spatial model $(L,\mathbf{W})$, a function $f:A\rightarrow B$, a
value $d_{1}\in B$ ($d_{1}\not=\top_{B}$), and two spatial signals
$\mathbf{s}_{1}:L\rightarrow D_{2}$, $\mathbf{s}_{2}:L\rightarrow D_{2}$ such
that
$\textsc{UnboundedReach}((L,\mathbf{W}),f,d_{1},\mathbf{s}_{1},\mathbf{s}_{2})=\mathbf{s}$.
Let $d_{min}=\min_{(\ell,w,\ell^{\prime})\in\mathbf{W}}(f(w))$,
$d_{max}=\max_{(\ell,w,\ell^{\prime})\in\mathbf{W}}(f(w))$ and
$k=\min\\{i|i*d_{min}>d_{1}+d_{max}\\}$, the algorithm stops after
$O(k\cdot\beta_{d_{2}}\cdot|L|\cdot m)$ steps, where $m$ is the number edges
and $\beta_{d_{2}}$ is an integer counting the _different distances_
accumulated after $k$ steps. Furthermore, when $d_{1}=\bot_{B}$, this
complexity reduces to $O(|L|*m)$.

###### Proof.

We have already observed in Proposition Proposition that the first part of
Algorithm 4 terminates after $O(k\cdot\beta_{d_{2}}\cdot|L|\cdot m)$. We can
here observe that the second part of the algorithm (lines $(9)-(21)$) needs at
most $|L|\cdot m$ steps. This 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 after $O(k\cdot\beta_{d_{2}}\cdot|L|\cdot
m)+O(|L|\cdot m)=O(k\cdot\beta_{d_{2}}\cdot|L|\cdot m)$ steps. When
$d_{1}=\bot_{B}$ lines $(9)-(21)$ are not executed, then the algorithm
terminates after $O(|L|\cdot m)$. ∎

######  Proposition (Escape complexity).

Given an $A$-spatial model $(L,\mathbf{W})$, a function $f:A\rightarrow B$, an
interval $[d_{1},d_{2}]$, ($d_{1},d_{2}\in B$, $d_{1}\leq_{B}d_{2}$ and)
$d_{2}\not=\top_{B}$), and a spatial signal $\mathbf{s}_{1}:L\rightarrow
D_{2}$ such that
$\textsc{Escape}((L,\mathbf{W}),f,d_{1},d_{2},\mathbf{s}_{1})=\mathbf{s}$.
Algorithm terminates in at most $O(|L|\cdot m)$ steps, where $m$ is the number
of edges.

###### Proof.

The computation of function $\textsc{MinDistance}(L,\mathbf{W},f)$ needs
$O(m\log(|L|))$ steps. Moreover, from property $P3$ in the proof of Lemma
Lemma, we have that the loop at line (6) terminates after at most $|L|$
iterations. In each of these iterations each edge is taken into account at
most 2 times (one for each of the connected locations). This means that the
loop terminates after $O(|L|*m)$ steps. Finally, to compute the resulting
spatial signal, $O(|L|)$ steps are needed for the loop at line $(22)$.
Concluding, the algorithm terminates in $O(m\log(|L|))+O(|L|*m)+O(|L|)$, that
is $O(|L|*m)$. ∎

We can conclude this section by observing that the number of steps needed to
evaluate function Monitor in Algorithm 1 is linear in the size of $\phi$, 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.

##  7\. Case study: ZigBee protocol monitoring

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 Example), we consider as
spatial models both its proximity and connectivity graphs computed with
respect to the Cartesian coordinates (Example Example). Nodes have three kind
of roles: coordinator, router and EndDevice, as described in Example Example.
Moreover, each device is also equipped with a sensor to monitor its battery
level ($X_{B}$), the humidity ($X_{H}$) and the pollution ($X_{H}$) in its
position. The semiring is the union between the _max/min_ semiring
$\mathbb{R}^{\infty}$ (for the proximity graph) and the _integer_ semiring
$\mathbb{N}^{\infty}$ (for the connectivity graph). We will use also two types
of distances: ${\it hop}$ and the $\Delta$ distances described in Example
Example. Atomic propositions
$\\{{\color[rgb]{0.3,0.615,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.615,0.3}coord},{\color[rgb]{0.65,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.65,0.3,0.3}router},{\color[rgb]{0.3,0.3,0.615}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.615}end\\_dev}\\}$
describe the type of nodes. We also consider inequalities on the values that
are read from sensors, plus special propositions $@_{\ell}$ which encode the
address of a specific location, i.e. they are true only in the location
$\ell$.

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:

$\phi_{connect}=device\mathcal{R}_{[0,1]}^{hop}(router\mathcal{R}^{hop}coord)$
(1)

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 above 30%:

$\displaystyle\phi_{reliable\\_router}=((battery>0.5)\wedge
router)\mathcal{R}^{hop}coord$
$\displaystyle\phi_{reliable\\_connect}=device\mathcal{R}_{[0,1]}^{hop}(\phi_{reliable\\_router})$
(2)

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:

$\phi_{connect\\_restore}=\mathrm{G}(\neg\phi_{connect}\rightarrow\mathrm{F}_{[0,h]}\phi_{connect})$
(3)

Another class of properties of interest is the acyclicity of transmissions. To
this end, we need to force the connectivity graph to be direct, 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 $\ell$. This is captured by
$\phi^{\ell}_{acyclic}=\neg\phi^{\ell}_{cycle}$, where

$\phi^{\ell}_{cycle}=@_{\ell}\mathcal{R}_{[0,1]}^{hop}(\neg@_{\ell}\wedge\diamonddiamond^{hop}@_{\ell})$
(4)

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 an efficient monitoring, as global properties of networks
require more expressive and computationally expensive logics. 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 $\boxbox^{\Delta}\phi$, verified on the proximity graph, holds iff
$\phi$ holds in all the location 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 a
quantitative semantics, returning a measure of robustness of
(dis)satisfaction. As an example, we can monitor (5) if in each location an
high value of pollution eventually implies, within $T$ time units, an high
value of humidity, or (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) if a location which is not safe is at
distance at most $d$ from a location which is safe. Finally (8), we can check
if a target device (identified by $X_{S}=1$ is reachable from all the location
in less than d hops.

$\displaystyle\phi_{PH}=(X_{P}>150)\Rightarrow\mathrm{F}_{[0,T]}(X_{H}>100)$
(5)
$\displaystyle\phi_{Safe}=\mathrm{G}_{[0,T]}\mathcal{E}_{[d,\infty]}^{\Delta}\>{(X_{H}<90)\wedge(X_{P}<150)}$
(6) $\displaystyle\phi_{some}=\diamonddiamond_{[0,d]}^{\Delta}\phi_{Safe}$ (7)
$\displaystyle\phi_{target}=\boxbox^{hop}\diamonddiamond_{[0,d]}^{hop}\>{(X_{S}=1)}$
(8)

##  8\. Case study: epidemic spreading

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 an 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 kind 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, modelling 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 modelled as a lognormal distribution with cutoff (mean 10,
99 percentile 50, cutoff at 200).666Contact distributions are constructed to
resemble contact data collected by a regional government in Italy, which is
not publicly available. 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 which will be affected by the events.
Each node has assigned a random probability of taking part to 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, cutoff at 1000), to model
super-spreading effects.777Note 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.

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 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 modelling the spreading of
infection.

At each time step, the spatial model of the epidemic network is designed by
the pair $\langle L,\mathbf{W}\rangle$, where the set of locations $L$
corresponds to the set of agents and the proximity function $\mathbf{W}$ is
such that $(\ell_{i},w,\ell_{j})\in\mathbf{W}$ if and only there is a
probability greater than zero that $\ell_{i}$ and $\ell_{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_{\ell_{i},\ell_{j}}(t))$, where $p_{\ell_{i},\ell_{j}}(t)$ is the
infection probability at time t. Hence, higher is $w$, the lower is the
probability that agent $\ell_{i}$ is in infected by agent $\ell_{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\rightarrow\mathbb{T}\rightarrow\mathbb{Z}$ with only one signal
$\vec{x}(\ell)=\nu$ associating with each agent $\ell$ and at each time t, the
state
$x(\ell,t)\in\mathbb{S}=\\{\textbf{Susceptible},\textbf{Exposed},\textbf{Infected},\textbf{Recovered}\\}=\\{\textbf{S},\textbf{E},\textbf{I},\textbf{R}\\}$.
To give an idea to the behaviour of this models we plot in Figure 5 the number
of nodes in each state at each time for a random simulation.

Figure 5. Number of nodes in each state at each time for a random simulation.

The first property that we consider is:

$\phi_{dangerous\\_days}=\mathrm{G}(\textbf{Susceptible}\mathcal{R}_{[0,1]}^{hop}(\mathrm{F}_{[0,2]}(\textbf{Infected}))=>\mathrm{F}_{[0,7]}\textbf{Infected})$
(9)

$\phi_{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\pm 12.5$ nodes of the
network, considering 500 experiments, instead, considering only the dynamic
network the property is satisfied by $350\pm 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:

$\phi_{safe\\_radius}=\mathrm{G}(\boxbox_{[0,r]}^{weight}(\neg\textbf{Infected})=>\mathrm{G}_{[0,T]}(\neg\textbf{Infected}))$
(10)

$\phi_{safe}$ 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 $\leq 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
relation 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 it prevents from infection. If a location does not satisfy the
property it means that there is some infected node at distance more than $r$,
connected with it that cause 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$\phi_{safe\\_radius}$ versus
parameter r

##  9\. Conclusions

We presented STREL, a formal specification language to express and to monitor
spatio-temporal 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, real-valued) semantics,
defining an unified framework capturing all of them, based on constraint
semirings. We further provided a generic offline monitoring algorithm based on
such semiring formulation. We showed several examples of requirements that we
can monitor in our framework, considering two different case studies.

As future work, we plan to investigate an algorithm for online monitoring of
STREL properties. Furthermore, 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 to detect the responsible components when
a STREL requirement is violated.

## Acknowledgment

This research has been partially supported by the Austrian FWF projects ZK-35
and W1255-N23, by the Italian PRIN project “SEDUCE” n. 2017TWRCNB and by the
Italian PRIN project “IT-MaTTerS” n, 2017FTXR7S.

## References

  * [ACM02] Eugene Asarin, Paul Caspi, and Oded Maler.  Timed regular expressions.  J. ACM, 49(2):172–206, 2002.
  * [AFS+13] Houssam Abbas, Georgios E. Fainekos, Sriram Sankaranarayanan, Franjo Ivancic, and Aarti Gupta.  Probabilistic temporal logic falsification of cyber-physical systems.  ACM Transactions on Embedded Computing Systems, 12(s2):95:1–95:30, 2013.
  * [APHvB07] Marco Aiello, Ian Pratt-Hartmann, and Johan van Benthem, editors.  Handbook of Spatial Logics.  Springer, Dordrecht, Niederlande, 2007.
  * [Aur91] Franz Aurenhammer.  Voronoi diagrams—a survey of a fundamental geometric data structure.  ACM Comput. Surv., 23(3):345–405, 1991.
  * [BBC+20] Fabrizio Banci Buonamici, Gina Belmonte, Vincenzo Ciancia, Diego Latella, and Mieke Massink.  Spatial logics and model checking for medical imaging.  Int. J. Softw. Tools Technol. Transf., 22(2):195–217, 2020.
  * [BBL+20] Ezio Bartocci, Luca Bortolussi, Michele Loreti, Laura Nenzi, and Simone Silvetti.  Moonlight: A lightweight tool for monitoring spatio-temporal properties.  In Proc. of RV 2020: the 20th International Conference on Runtime Verification, volume 12399 of LNCS, pages 417–428. Springer, 2020\.
  * [BBLN17] Ezio Bartocci, Luca Bortolussi, Michele Loreti, and Laura Nenzi.  Monitoring mobile and spatially distributed cyber-physical systems.  In Proc. of MEMOCODE 2017: the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, pages 146–155, Vienna, Austria, 2017. ACM.
  * [BBM+15] Ezio Bartocci, Luca Bortolussi, Dimitrios Milios, Laura Nenzi, and Guido Sanguinetti.  Studying emergent behaviours in morphogenesis using signal spatio-temporal logic.  In Proc. of HSB 2015: the Fourth International Workshop on Hybrid Systems Biology, volume 9271 of LNCS, pages 156–172. Springer, 2015\.
  * [BBNS15] Ezio Bartocci, Luca Bortolussi, Laura Nenzi, and Guido Sanguinetti.  System design of stochastic models using robustness of temporal properties.  Theor. Comp. Sci., 587:3–25, 2015.
  * [BCCF19] Fred Brauer, Carlos Castillo-Chavez, and Zhilan Feng.  Mathematical Models in Epidemiology, volume 69 of Texts in Applied Mathematics.  Springer New York, New York, NY, 2019.
  * [BCLM19] Gina Belmonte, Vincenzo Ciancia, Diego Latella, and Mieke Massink.  Voxlogica: A spatial model checker for declarative image analysis.  In Proc. of TACAS 2019: the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 11427 of LNCS, pages 281–298. Springer, 2019.
  * [BCWZ02] Brandon Bennett, Anthony G. Cohn, Frank Wolter, and Michael Zakharyaschev.  Multi-dimensional modal logic as a framework for spatio-temporal reasoning.  Applied Intelligence, 17(3):239–251, September 2002.
  * [BDD+18] Ezio Bartocci, Jyotirmoy Deshmukh, Alexandre Donzé, Georgios Fainekos, Oded Maler, Dejan Ničković, and Sriram Sankaranarayanan.  Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications.  In Lectures on Runtime Verification, pages 135–175. Springer, 2018\.
  * [BDG+20] Ezio Bartocci, Jyotirmoy Deshmukh, Felix Gigler, Cristinel Mateis, Dejan Nickovic, and Xin Qin.  Mining shape expressions from positive examples.  IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 39(11):3809–3820, 2020.
  * [BFMN18] Ezio Bartocci, Thomas Ferrère, Niveditha Manjunath, and Dejan Nickovic.  Localizing faults in simulink/stateflow models with STL.  In Proc. of HSCC 2018: the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), pages 197–206. ACM, 2018.
  * [BM12] Kyungmin Bae and José Meseguer.  A rewriting-based model checker for the linear temporal logic of rewriting.  Electron. Notes Theor. Comput. Sci., 290:19–36, December 2012.
  * [BMM+19] Ezio Bartocci, Niveditha Manjunath, Leonardo Mariani, Cristinel Mateis, and Dejan Nickovic.  Automatic failure explanation in CPS models.  In Proc. of SEFM 2019: the 17th International Conference on Software Engineering and Formal Methods, volume 11724 of LNCS, pages 69–86. Springer, 2019.
  * [BMM+20] Ezio Bartocci, Niveditha Manjunath, Leonardo Mariani, Cristinel Mateis, Dejan Nickovic, and Fabrizio Pastore.  Cpsdebug: a tool for explanation of failures in cyber-physical systems.  In Proc. of ISSTA ’20: 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, USA, July 18-22, 2020, pages 569–572. ACM, 2020.
  * [BMR97] Stefano Bistarelli, Ugo Montanari, and Francesca Rossi.  Semiring-based constraint satisfaction and optimization.  J. ACM, 44(2):201–236, 1997.
  * [BMS15] Luca Bortolussi, Dimitrios Milios, and Guido Sanguinetti.  U-Check: Model checking and parameter synthesis under uncertainty.  In Proc. of QEST 2015: 12th Inter. Conf. on Quantitative Evaluation of Systems, volume 9259 of LNCS, pages 89–104. Springer, 2015\.
  * [BMS16] Luca Bortolussi, Dimitrios Milios, and Guido Sanguinetti.  Smoothed model checking for uncertain continuous-time markov chains.  Information and Computation, 247:235–253, 2016.
  * [BSM+10] D. Bresolin, P. Sala, D. Della Monica, A. Montanari, and G. Sciavicco.  A decidable spatial generalization of metric interval temporal logic.  In Proc. of TIME 2010: the 17th International Symposium on Temporal Representation and Reasoning, pages 95–102, Paris, France, 2010. IEEE.
  * [CC03] Lu?s Caires and Luca Cardelli.  A spatial logic for concurrency (part i).  Information and Computation, 186(2):194 – 235, 2003.
  * [CG00] Luca Cardelli and Andrew D. Gordon.  Anytime, anywhere: Modal logics for mobile ambients.  In Proc. of POPL ’00: the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 365–377, New York, NY, USA, 2000\. ACM.
  * [CGG+18] Vincenzo Ciancia, Stephen Gilmore, Gianluca Grilletti, Diego Latella, Michele Loreti, and Mieke Massink.  Spatio-temporal model checking of vehicular movement in public transport systems.  Int. J. Softw. Tools Technol. Transf., 20(3):289–311, 2018.
  * [CLLM14] Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink.  Specifying and verifying properties of space.  In Proc. of TCS 2014: the 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science, volume 8705 of Lecture Notes in Computer Science, pages 222–235, Rome, Italy, 2014. Springer.
  * [CLLM16] Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink.  Spatial logic and spatial model checking for closure spaces.  In Proc. of SFM 2016, volume 9700 of LNCS, pages 156–201, Bertinoro, Italy, 2016. Springer.
  * [CTR+20] D. Cereda, M. Tirani, F. Rovida, V. Demicheli, M. Ajelli, P. Poletti, F. Trentini, G. Guzzetta, V. Marziano, A. Barone, M. Magoni, S. Deandrea, G. Diurno, M. Lombardo, M. Faccini, A. Pan, R. Bruno, E. Pariani, G. Grasselli, A. Piatti, M. Gramegna, F. Baldanti, A. Melegaro, and S. Merler.  The early phase of the COVID-19 outbreak in Lombardy, Italy.  arXiv:2003.09320 [q-bio], March 2020.  arXiv: 2003.09320.
  * [DCLL09] Alexandre Donzé, Gilles Clermont, Axel Legay, and Christopher James Langmead.  Parameter synthesis in nonlinear dynamical systems: Application to systems biology.  In Proc. of RECOMB 2009: the 13th Annual International Conference on Research in Computational Molecular Biology, volume 5541 of LNCS, pages 155–169. Springer, 2009.
  * [Del34] Boris Delaunay.  Sur la sphère vide. a la mémoire de georges voronoï.  Bulletin de l’Académie des Sciences de l’URSS, 6:793–800, 1934\.
  * [DFM13] Alexandre Donzé, Thomas Ferrère, and Oded Maler.  Efficient robust monitoring for STL.  In Proc. of CAV 2013: the 25th International Conference on Computer Aided Verification, volume 8044 of LNCS, pages 264–279, Saint Petersburg, Russia, 2013. Springer.
  * [DKR09] Alexandre Donzé, Bruce Krogh, and Akshay Rajhans.  Parameter synthesis for hybrid systems with an application to simulink models.  In Proc. of HSCC 2009: the 12th International Conference on Hybrid Systems: Computation and Control, volume 5469 of LNCS, pages 165–179. Springer, 2009.
  * [DLL+11] Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, and Zheng Wang.  Time for statistical model checking of real-time systems.  In Proc. of CAV 2011: the 23rd International Conference on Computer Aided Verification, volume 6806 of LNCS, pages 349–355. Springer, 2011.
  * [EH83] E. Allen Emerson and Joseph Y. Halpern.  ”sometimes” and ”not never” revisited: On branching versus linear time.  In John R. Wright, Larry Landweber, Alan J. Demers, and Tim Teitelbaum, editors, Proc. of POPL 83: the Tenth Annual ACM Symposium on Principles of Programming Languages, pages 127–140, Austin, Texas, 1983. ACM Press.
  * [FB74] Raphael A. Finkel and Jon Louis Bentley.  Quad trees: A data structure for retrieval on composite keys.  Acta Informatica, 4:1–9, 1974.
  * [Gal99] Antony Galton.  The mereotopology of discrete space.  In Christian Freksa and DavidM. Mark, editors, Proc. of COSIT ’99: the International Conference on Spatial Information Theory: Cognitive and Computational Foundations of Geographic Information Science, volume 1661 of LNCS, pages 251–266, Berlin Heidelberg, 1999. Springer.
  * [GBB14] E. Aydin Gol, E. Bartocci, and C. Belta.  A formal methods approach to pattern synthesis in reaction diffusion systems.  In Proc. of CDC 2014: the 53rd IEEE Conference on Decision and Control, pages 108–113, Los Angeles, CA, USA, 2014. IEEE.
  * [GSC+09] Radu Grosu, Scott A. Smolka, Flavio Corradini, Anita Wasilewska, Emilia Entcheva, and Ezio Bartocci.  Learning and detecting emergent behavior in networks of cardiac myocytes.  Commun. ACM, 52(3):97–105, 2009.
  * [HJK+15] Iman Haghighi, Austin Jones, Zhaodan Kong, Ezio Bartocci, Radu Grosu, and Calin Belta.  SpaTeL: a novel spatial-temporal logic and its applications to networked systems.  In Proc. of HSCC’15: the 18th International Conference on Hybrid Systems: Computation and Control, pages 189–198, Seattle, WA, USA, 2015. IEEE.
  * [HSS08] Aric A. Hagberg, Daniel A. Schult, and Pieter J. Swart.  Exploring network structure, dynamics, and function using networkx.  In Gaël Varoquaux, Travis Vaught, and Jarrod Millman, editors, Proceedings of the 7th Python in Science Conference, pages 11 – 15, Pasadena, CA USA, 2008.
  * [JBGN18] Stefan Jaksic, Ezio Bartocci, Radu Grosu, and Dejan Nickovic.  An algebraic framework for runtime verification.  IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 37(11):2233–2243, 2018.
  * [Koy90] Ron Koymans.  Specifying real-time properties with metric temporal logic.  Real-Time Systems, 2(4):255–299, 1990.
  * [LM05] Alberto Lluch-Lafuente and Ugo Montanari.  Quantitative mu-calculus and CTL defined over constraint semirings.  Theor. Comput. Sci., 346(1):135–160, 2005.
  * [LSSKG05] J. O. Lloyd-Smith, S. J. Schreiber, P. E. Kopp, and W. M. Getz.  Superspreading and the effect of individual variation on disease emergence.  Nature, 438(7066):355–359, November 2005.  Number: 7066 Publisher: Nature Publishing Group.
  * [LWD+20] Ramanan Laxminarayan, Brian Wahl, Shankar Reddy Dudala, K Gopal, Chandra Mohan, S Neelima, K. S. Jawahar Reddy, J Radhakrishnan, and Joseph Lewnard.  Epidemiology and transmission dynamics of COVID-19 in two Indian states.  preprint, Epidemiology, July 2020.
  * [Mal16] Oded Maler.  Some thoughts on runtime verification.  In Proc. of RV 2016: the 16th International Conference on Runtime Verification, volume 10012 of LNCS, pages 3–14. Springer, 2016\.
  * [MBL+20] Meiyi Ma, Ezio Bartocci, Eli Lifland, John A. Stankovic, and Lu Feng.  Sastl: Spatial aggregation signal temporal logic for runtime monitoring in smart cities.  In Proc. of ICCPS 2020: the 11th ACM/IEEE International Conference on Cyber-Physical Systems, pages 51–62, Sydney, Australia, 2020. IEEE.
  * [MBL+21] Meiyi Ma, Ezio Bartocci, Eli Lifland, John A. Stankovic, and Lu Feng.  A novel spatial-temporal specification-based monitoring system for smart cities.  IEEE Internet of Things Journal, pages 1–1, 2021.
  * [MN04] Oded Maler and Dejan Nickovic.  Monitoring temporal properties of continuous signals.  In Proc. of FORMATS/FTRTFT 2004: the Joint International Conferences on Formal Modelling and Analysis of Timed Systems and on Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 3253 of LNCS, pages 152–166, Grenoble, France, 2004. Springer.
  * [MN13a] Oded Maler and Dejan Nickovic.  Monitoring properties of analog and mixed-signal circuits.  STTT, 15(3):247–268, 2013.
  * [MN13b] Oded Maler and Dejan Ničković.  Monitoring properties of analog and mixed-signal circuits.  STTT, 15(3):247–268, 2013.
  * [MR99] M. Marx and M. Reynolds.  Undecidability of compass logic.  J Logic Computation, 9(6):897–914, 1999.
  * [NBB+20] Laura Nenzi, Ezio Bartocci, Luca Bortolussi, Michele Loreti, and Ennio Visconti.  Monitoring spatio-temporal properties (invited tutorial).  In Proc. of RV 2020: the 20th International Conference on Runtime Verification, volume 12399 of LNCS, pages 21–46. Springer, 2020\.
  * [NBC+15] Laura Nenzi, Luca Bortolussi, Vincenzo Ciancia, Michele Loreti, and Mieke Massink.  Qualitative and quantitative monitoring of spatio-temporal properties.  In Proc. of RV 2015: the 6th International Conference on Runtime Verification, volume 9333, pages 21–37, Vienna, Austria, 2015. Springer.
  * [NBC+18] Laura Nenzi, Luca Bortolussi, Vincenzo Ciancia, Michele Loreti, and Mieke Massink.  Qualitative and quantitative monitoring of spatio-temporal properties with SSTL.  Log. Methods Comput. Sci., 14(4):1–38, 2018.
  * [PSCVMV15] Romualdo Pastor-Satorras, Claudio Castellano, Piet Van Mieghem, and Alessandro Vespignani.  Epidemic processes in complex networks.  Reviews of Modern Physics, 87(3):925–979, August 2015.  arXiv: 1408.2701.
  * [RKG+19] Denise Ratasich, Faiq Khalid, Florian Geissler, Radu Grosu, Muhammad Shafique, and Ezio Bartocci.  A roadmap toward the resilient internet of things for cyber-physical systems.  IEEE Access, 7:13260–13283, 2019.
  * [SKC+17] Sriram Sankaranarayanan, Suhas Akshar Kumar, Faye Cameron, B. Wayne Bequette, Georgios Fainekos, and David M. Maahs.  Model-based Falsification of an Artificial Pancreas Control System.  SIGBED Rev., 14(2):24–33, March 2017.
  * [SPB17] Simone Silvetti, Alberto Policriti, and Luca Bortolussi.  An active learning approach to the falsification of black box cyber-physical systems.  In Proc. of IFM 2017: the 13th International Conference on Integrated Formal Methods, volume 10510 of LNCS, pages 3–17. Springer, 2017.
  * [Tal08] Carolyn L. Talcott.  Cyber-physical systems and events.  In Software-Intensive Systems and New Computing Paradigms - Challenges and Visions, volume 5380 of LNCS, pages 101–115. Springer, Berlin, Heidelberg, 2008.
  * [TVG09] Y. Tan, M. C. Vuran, and S. Goddard.  Spatio-temporal event model for cyber-physical systems.  In 2009 29th IEEE International Conference on Distributed Computing Systems Workshops, pages 44–50, Montreal, QC, Canada, 2009. IEEE.
  * [YF17] Shakiba Yaghoubi and Georgios Fainekos.  Hybrid approximate gradient and stochastic descent for falsification of nonlinear systems.  In Proc. ACC 2017: the 2017 American Control Conference, pages 529–534. IEEE, 2017.
  * [YS06] Håkan L. S. Younes and Reid G. Simmons.  Statistical probabilistic model checking with a focus on time-bounded properties.  Inf. Comput., 204(9):1368–1409, 2006.