# Distributed Monitoring of Timed Properties

Léo Henry, Thierry Jéron, Nicolas Markey, Victor Roussanaly

► To cite this version:

Léo Henry, Thierry Jéron, Nicolas Markey, Victor Roussanaly. Distributed Monitoring of Timed Properties. RV 2024 - 24th International Conference on Runtime Verification, Doğan Ulus, Oct 2024, Istanbul, Turkey. pp.260. hal-04701084

HAL Id: hal-04701084

https://hal.science/hal-04701084v1

Submitted on 30 Sep 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Distributed Monitoring of Timed Properties

Léo Henry¹, Thierry Jéron², Nicolas Markey², and Victor Roussanaly³

¹ University College London, UK

² IRISA, CNRS & Inria & Univ. Rennes, France

³ Université de Lorraine, France

**Abstract.** In formal verification, runtime monitoring consists of observing the execution of a system in order to decide as quickly as possible whether or not it satisfies a given property. We consider monitoring in a distributed setting, for properties given as reachability timed automata. In such a setting, the system is made of several components, each equipped with its own local clock and monitor. The monitors observe events occurring on their associated component, and receive timestamped events from other monitors through FIFO channels. Since clocks are local, they cannot be perfectly synchronized, resulting in imprecise timestamps. Consequently, they must be seen as intervals, leading monitors to consider possible reorderings of events. In this context, each monitor aims to provide, as early as possible, a verdict on the property it is monitoring, based on its potentially incomplete and imprecise knowledge of the current execution. In this paper, we propose an on-line monitoring algorithm for timed properties, robust to time imprecision and partial information from distant components. We first identify the date at which a monitor can safely compute a verdict based on received events. We then propose a monitoring algorithm that updates this date when new information arrives, maintains the current set of states in which the property can reside, and updates its verdict accordingly.

## 1 Introduction

*Runtime verification.* Formal verification is a branch of computer science that aims to check whether computer systems satisfy their requirements. This includes in particular model checking [10,3] and deductive verification [20,15], which work offline and check properties of all behaviours of the system under study. In contrast, runtime verification [23,4] is a set of efficient techniques to monitor the behaviour of a *running* system, and to detect, as early as possible during the execution, whether some properties are satisfied or violated. This domain of formal verification has been extensively studied over the last 25 years, and is now mature enough to be applied in various application domains.

As real-life systems typically comprise several connected components, runtime verification techniques must be adapted to handle situations where the behaviours of the components are only partially known and may be imprecise: each component is equipped with a monitor, and monitors exchange information asynchronously with each other.
Because the system is distributed, we assume that each monitor only has access to a local clock, which may slightly drift w.r.t a reference clock. Hence the dates of the events are only known with a limited precision, and the exact order of the events occurring on different subsystems may be unknown. We assume that communications between local monitors are FIFO; this way, when a monitor receives the information that some event took place on some subsystem, it also knows all the events that have occurred earlier on that subsystem.

Thanks to these hypotheses, each monitor can determine a time in the past for which it currently has enough information to decide whether the property it is checking already held, or failed to hold, at that time. We consider real-time properties modelled as timed automata (TA) [1]; the expressiveness of these models allows to account for the precise timing of events, which magnifies the impact of the lack of an observable global clock.

**Example 1.** Consider a private (e.g., enterprise, university) network with a set of terminals and servers containing user account data logged in and a router connected to them. Properties of interest can be that (1) all machines should remain connected to the network and (2) no account should be logged in more than one terminal at a time. Even if two terminals signal that they are connected to a given account, a monitor has to wait to ensure that no "log out" message is pending from one of the two terminals. Plus, once such signals are received, the approximate timings may lead to situations where two terminals may or may not have been connected to the same user session at the same time, with no ability to conclude.

***Our contributions.*** We present a monitoring algorithm for properties expressed as (deterministic) TAs in a distributed setting without a global clock. Each monitor keeps track of the most recent date at which it has collected the full history (relying on the assumption that communications with other monitors are FIFO). The prefix of the collected trace at this time already contains uncertainty, due to the absence of a global clock, which entails that reordering events from distinct components must be considered. The computation of a verdict is based on the incremental update of a structure that encodes the set of states compatible with the prefix of the collected trace up to the time of interest. We show that the monitoring algorithm is sound and complete.

***Related works.*** This paper studies distributed runtime verification for timed properties described as timed automata [1]. Several related approaches have been developed in the literature. Extensions of Linear-time Temporal Logic (LTL) integrating dense time have been explored for runtime verification and monitor synthesis [6]. Among them, Metric Temporal Logic (MTL) is of particular interest as it is directly related to TAs [25] and is equipped with a progression function allowing to evaluate formulas at runtime [28]. Similarly, Timed Regular Expressions are as expressive as TAs and can be translated to TAs [2]. The tool Montre [29] monitors them using timed pattern matching. Monitoring TA models has been realized in the case of one-clock non-deterministic TAs [19]. Pinisetty et al. [26] introduce a predictive setting for runtime verification of timed properties, leveraging reachability analysis to anticipate the detection of verdicts.
The aforementioned approaches consider that the monitored system is cen-
tralized and the decision procedure is fed with a unique trace containing complete
observations. Decentralized runtime verification [7] (see also a recent overview
in [13]) handles separate traces corresponding to each monitor. Decentralized
(also called synchronous) methods however assume the existence of a global
clock shared by all components and monitors. We relax this assumption here,
and consider asynchronous distributed monitoring (or distributed monitoring
for short). For a discussion on the links and differences between synchronous and
asynchronous methods, see [16].

Most approaches in decentralized runtime verification take as input Linear-
time Temporal Logic formulas [7,11,17] or finite-state automata [14,12]. These
approaches monitor specifications of discrete time, which does not account for the
physical time that impacts the evaluation of the specifications nor the moment at
which monitors perform their evaluation and deliver their verdicts. An approach
close to ours is [5], in which properties are specified in an extension of Metric
Temporal Logic to tackle both timing and data values. Similar to us, the authors
also deal with out-of-order messages, but also failures and lost messages. However,
they consider that local clocks are accurate.

Distributed runtime verification exhibits similarities with diagnosis [30,31] ([9] for TAs), which aims to identify the occurrence of a fault and the component(s) responsible for it after a finite number of discrete steps, and has to cope with partial observation. Our approach differs from diagnosis, as we assume that monitors'(combined) local information suffices to detect violations; diagnosis does not aim to check membership to an arbitrary timed regular expression. The approach of [21] for robust diagnosis shares several common aspects with ours. While centralized, it considers diagnosis where communication between the system and the diagnoser is subject to varying latency, clock drift and out-of-order observation. The problem is different but is similar in spirit: incrementally building a verdict based on approximate and partial timed observations. Moreover some constructions have clear similarities, which is not surprising: in both cases the language of runs compatible with the current partial and approximate observation has to be considered. Other approaches comparable to ours perform monitoring on timed properties in a decentralized [27] or distributed [18] fashion. Our own approach discusses distributed monitoring directly on timed automata models.

2 Preliminaries

We present the basic hypotheses about our formalization of the distributed
monitoring problem in Section 2.1, the notions of words and languages at play in
Sections 2.2 and 2.3, and timed automata in Section 2.4.

## 2.1 Distributed timed systems

We consider systems made of *n* independent components ($C_i$)$_{1 \le i \le n}$. Each $C_i$ is
observed by a local monitor $M_i$. The components being independent, we assume
that each $C_i$ has its own finite alphabet of actions $\mathbf{Act}_i$, disjoint from the alphabets of the other components. We write $\mathbf{Act} = \bigsqcup_{1 \le i \le n} \mathbf{Act}_i$ for the alphabet of all actions. For an action $a \in \mathbf{Act}_i$, we write $\mathrm{Comp}(a) = i$. An action $a$ fired by component $C_i$ is observed and timestamped by its monitor $M_i$, giving rise to an event $(a, t)$ in $\mathbf{Act}_i \times \mathbb{R}_{\ge 0}$. We assume the following about the system:

**Respective knowledge:** monitors know each others' alphabets of actions;

**Communication:** monitors send messages to their peers, carrying the timestamped events they observed (and events they learnt about from other monitors) in the order in which they observed them. We assume that local events can be strictly ordered.

**Communication channels:** communications between monitors obey a FIFO policy with no message loss: messages are received in the order they were sent, and any sent message is eventually received, although no upper bound on communication delays is assumed.

**Communication topology:** the connectivity is such that a monitor $M_i$ can receive messages (either directly or indirectly) from any monitor $M_j$ managing some action appearing in $M_i$'s property.

**Local liveness:** at any given time, each monitor will eventually have a local observation in the future, and will eventually send it to the other monitors.

**Time approximation:** monitors do not share a global clock, but one can assume that each local clock has a maximal skew $\varepsilon$ with respect to a global reference clock$^4$. We suppose that clocks are non-decreasing.

Most of these assumptions are easy to satisfy. A FIFO policy can be achieved by numbering the events exchanged between one monitor and another, ensuring that a monitor can handle events in the order they were sent. Local liveness can be ensured by adding empty events that are sent when no events have been observed for a long duration. The main practical constraints are the absence of message losses, and the bound on clock skews. However, even these assumptions can be mitigated. Message losses can be detected using the message numbering, while a mechanism such as Network Time Protocol (NTP) can be used to limit the skew to $\varepsilon$.

We consider that each monitor is in charge of verifying some property (given as a timed automaton, see Sect. 2.4). As the monitoring algorithms and properties are symmetric for each such monitor, we restrict our dissertation to a fixed monitor $M_i$ and assume that the entire set $\mathbf{Act}$ of actions is necessary for its property (some of these actions are still observed by other monitors).

## 2.2 Timed words and languages

We consider intervals in $\mathbb{R}$, denoted $\mathcal{I}(\mathbb{R})$. For an interval $I = \langle l, u \rangle$, with $\langle \cdot \in \{(), [] \}$ and $\rangle \in \{(), []\}$, we write $\mathrm{lb}(I) = l$, $\mathrm{ub}(I) = u$ for its lower and upper bounds. For two intervals $I_1, I_2$ of $\mathbb{R}$, we write $I_1 < I_2$ if $\mathrm{ub}(I_1) \le \mathrm{lb}(I_2)$; when this

<footnote n="4">⁴ Our approach can be easily generalized to different $\varepsilon$ for each monitor, with our theorems depending on the greatest one.</footnote>
condition is met, the intervals intersect in at most one point. We also consider
intervals of natural numbers and write $\llbracket 1; m \rrbracket$ for $\{k \in \mathbb{N} \mid 1 \le k \le m\}$.

*Timed Words and Languages.* We consider timed words built on the alphabet of ac-
tions Act as (finite or infinite) sequences $\sigma = (a_k, t_k)_{k \in \llbracket 1;m \rrbracket}^5$ of events in $\text{Act} \times \mathbb{R}_{\ge 0}$
whose sequence of dates $(t_k)_{k \in \llbracket 1;m \rrbracket}$ is non-decreasing. We write $\sigma[k] = (a_k, t_k)$
for its k-th event. For any interval $I$ of $\mathbb{R}_{\ge 0}$, we write $\sigma|_I$ for the subword of $\sigma$
restricted to dates in $I$, and $\sigma|_t$ as a shorthand for $\sigma|_{[0,t]}$ with $t \in \mathbb{R}_{\ge 0}$. For a finite
timed word $\sigma = (a_k, t_k)_{k \in \llbracket 1;m \rrbracket}$, we write $|\sigma| = m$ for its length, $\text{firstt}(\sigma) = t_1$
and $\text{lastt}(\sigma) = t_m$ respectively for the dates of its first and last events; for the
empty word $\gamma$, we let $\text{firstt}(\gamma) = \text{lastt}(\gamma) = 0$. Two timed words $\sigma_1$ and $\sigma_2$
can be concatenated into $\sigma_1 \cdot \sigma_2$ if, and only if, $\text{lastt}(\sigma_1) \le \text{firstt}(\sigma_2)$. For any
interval $I \subseteq \mathbb{R}_{\ge 0}$, we write $\text{TT}_I(\text{Act})$ for the set of timed words in $(\text{Act} \times I)^*$, and
$\text{TT}(\text{Act}) = \text{TT}_{\mathbb{R}_{\ge 0}}(\text{Act})$. A language of timed words is any subset of $\text{TT}(\text{Act})$.

For two languages of timed words $L_1$ and $L_2$, their concatenation $L_1 \cdot L_2$ is
defined and equal to $\{\sigma_1 \cdot \sigma_2 \mid \sigma_1 \in L_1, \sigma_2 \in L_2\}$ if, and only if, $\text{supp}\{\text{lastt}(\sigma_1) \mid \sigma_1 \in L_1\} \le \inf\{\text{firstt}(\sigma_2) \mid \sigma_2 \in L_2\}$. The restriction to an interval naturally
generalizes to languages: for a language $L \subseteq \text{TT}(\text{Act})$ and an interval $I$ of $\mathbb{R}$,
$L|_I = \{\sigma|_I \mid \sigma \in L\}$.

*Projections on monitors.* In our setting, *Act* is the disjoint union of alphabets $\text{Act}_i$.
For a timed word $\sigma$, we write $\mathfrak{p}_i(\sigma)$ for the projection on the actions monitored
by $M_i$, defined by induction as $\mathfrak{p}_i(\gamma) = \gamma$ for the empty word, and $\mathfrak{p}_i(\sigma \cdot (a, t)) =
\mathfrak{p}_i(\sigma) \cdot (a, t)$ if $a \in \text{Act}_i$ and $\mathfrak{p}_i(\sigma \cdot (a, t)) = \mathfrak{p}_i(\sigma)$ otherwise.

Conversely, we define a tensor operation on timed words $\sigma_1 \otimes \sigma_2$ that merges
the events while re-ordering them by ascending timestamps. This operation is
such that $\sigma = \otimes_{i \in \llbracket 1:n \rrbracket} \mathfrak{p}_i(\sigma)$.

## 2.3 Approximate Timed Words

If we had perfect clocks, timed words as defined above would be the model of
choice for representing the knowledge of the monitors; restriction to intervals
would be used to identify the part of the knowledge that each monitor knows
is complete (as opposed to the part of the knowledge where informations from
some of the components did not arrive yet).

In the context of distributed monitoring, we consider that the clocks of the
monitors may be imprecise, resulting in a potential drift of up to a uniform
bound $\epsilon$ w.r.t. a reference clock. Because of this, we have to rely on a notion of
*approximate timed words*, and to define restriction to intervals for this new model.

Because of timing imprecisions, an event $(a, t)$, made of action $a$ timestamped
with $t$ by the monitor that observed it, may have happened anywhere in the
interval $[t - \epsilon, t + \epsilon] \cap \mathbb{R}_{\ge 0}$ with respect to the reference clock$^6$. Thus, while
the information collected by a monitor has the form of a timed word $\sigma =$

<footnote>$^5$ We abusively use such a notation for both finite and infinite sequences.</footnote>

<footnote>$^6$ Intersection with $\mathbb{R}_{\ge 0}$ is used to rule out events with negative dates.</footnote>
$(a_k, t_k)_{k \in [1;m]}$, the real date of each event $(a_k, t_k)$ lies in the interval $I_k = [t_k - \varepsilon, t_k + \varepsilon] \cap \mathbb{R}_{\ge 0}$. We call approximate timed word of $\sigma$, the sequence $\nu(\sigma) = (a_k, I_k)_{k \in [1;m]}$.

**Approximate timed words.** An approximate timed word (ATW for short) is a sequence of pairs $\nu = (a_k, I_k)_{k \in [1;m]}$ such that, for all $k \in [1;m]$, $a_k \in \mathbf{Act}$ and $I_k \in \mathcal{I}(\mathbb{R})$ is an interval (open or closed for generality). We denote by $\mathbf{ATW}(\mathbf{Act})$ the set of approximate timed words on $\mathbf{Act}$.

With any approximate timed word, we associate two languages: its *ordered* language and its *non-ordered* language. Intuitively, the *ordered* language of $\nu$ is the language of timed words that respect the order of the events and the intervals given by $\nu$, while the *non-ordered* language will be the union of the ordered languages for all possible reoderings of the events.

The ordered semantics defines a “tube” of timed words with the same untimed projection. It is defined as follows:

$$ \llbracket (a_k, I_k)_{k \in [1;m]} \rrbracket_{\text{ord}} = \{ (a_k, t_k)_{k \in [1;m]} \in \mathbf{TT}(\mathbf{Act}) \mid \forall k \in [1;m]. t_k \in I_k \} $$

By definition of $\mathbf{TT}(\mathbf{Act})$, the sequence $(t_k)_{k \in [1;m]}$ is non-decreasing, which induces constraints on subsequent $t_k$'s. Notice that $\llbracket \nu \rrbracket_{\text{ord}} = \emptyset$ when $I_k = \emptyset$ for some $k$, or if no increasing sequences of dates can be found in the sequence $(I_k)_{k \in [1;m]}$.

In order to define the *non-ordered language* of $\nu$, we introduce the subset $\mathcal{F}(\nu)$ of permutations of events in $\nu$ that respect the strict order of events sharing the same component (each monitor knows the order of events occurring in the component it supervises). We define it as follows, with $\mathbf{Perms}(\llbracket 1;m \rrbracket)$ being the set of permutations of $\llbracket 1;m \rrbracket$:

$$ \mathcal{F}((a_k, I_k)_{k \in [1;m]}) = \{ f \in \mathbf{Perms}(\llbracket 1;m \rrbracket) \mid \forall k, l \in [1;m]. (\mathbf{Comp}(a_k) = \mathbf{Comp}(a_l) \wedge k < l) \Rightarrow f(k) < f(l) \}. $$

Then for $f \in \mathcal{F}(\nu)$, we abuse the notation and write $f(\nu)$ for the ATW $(a_{f(k)}, I_{f(k)})_{k \in [1;m]}$. Finally, we define the (*non-ordered*) language of $\nu$ as the set of timed words that respect both the intervals given by $\nu$, and the strict local order on each component:

$$ \llbracket \nu \rrbracket = \bigcup_{f \in \mathcal{F}(\nu)} \llbracket f(\nu) \rrbracket_{\text{ord}}. $$

Intuitively, this language includes commutations of events that occurred at sufficiently close dates on different components: indeed, if $\nu = \nu_1 \cdot (b_k, t) \cdot (b_l, t') \cdot \nu_2$ with $\mathbf{Comp}(b_k) \neq \mathbf{Comp}(b_l)$ and $|t - t'| \le 2\varepsilon$, then $\llbracket \nu \rrbracket$ contains timed words with form $\sigma_1 \cdot (b_k, t) \cdot (b_l, t') \cdot \sigma_2$ and $\sigma_1 \cdot (b_l, t' - \varepsilon) \cdot (b_k, t + \varepsilon) \cdot \sigma_2$.

Back to the monitoring problem, given some monitor and an observation prefix $\sigma$ that is sufficient (in some sense clarified later), considering the imprecision due to the skew $\varepsilon$ in the approximate timed word $\nu(\sigma)$, the *non-ordered* language $\llbracket \nu(\sigma) \rrbracket$ is the set of executions that could produce this observation prefix, hence that has to be considered for monitoring.
Operations on approximate timed words. We now focus on defining a restriction of approximate timed words to an interval of dates. This will be useful for the incremental update of the monitor's knowledge (see Sect. 3.3). Semantically, the restriction of an ATW $\nu$ to an interval $I$ is the set of restrictions to $I$ of all the timed words contained in $[[\nu]]$. In this section, we present a syntactic definition, which will be the basis of an effective computation.

To this aim, we first define intersection: for $\nu = (a_k, I_k)_{k \in \llbracket 1;m \rrbracket}$ and an interval $I$, the intersection of $\nu$ with $I$ is the ATW $\nu \cap I = (a_k, I_k \cap I)_{k \in \llbracket 1;m \rrbracket}$. Notice that $[[\nu \cap I]]_{ord} = [[\nu \cap I]] = \emptyset$ if $I_k \cap I = \emptyset$ for some $k \in \llbracket 1;m \rrbracket$.

Our syntactic definition of restriction adapts the notion of subword. For any interval $I$ of $\mathbb{R}_{\ge 0}$, and two ATW $\nu'$ and $\nu''$, we say that $\nu' = \nu'_1 \cdots \nu'_n$ is a subword of $\nu'' = \nu''_1 \cdot \nu''_1 \cdots \nu''_n \cdot \nu''_{n+1}$ conditioned by $I$, written $\nu' \preceq_I \nu''$, if, and only if,

- for all $l \in \llbracket 1; n+1 \rrbracket$, for any $(a_k, I_k)$ in $\nu''_l$, $\neg(I_k \subseteq I)$: all events in $\nu''_l$ (which are dropped) may occur outside of $I$;

- for all $l \in \llbracket 1; n \rrbracket$, for any $(a'_{k'}, I'_{k'})$ in $\nu'_l$, $I'_{k'} \cap I \neq \emptyset$: all events in $\nu'_l$ (which are not dropped) may occur in $I$;

- there is $f \in \mathcal{F}(\nu'')$ s.t. $f(\nu'') = \nu_1 \cdot \nu' \cdot \nu_3$ for some $\nu_1$ and $\nu_3$: this encodes the fact that two events in the same component can not be permuted.

We can now define the (syntactic) restriction of an approximate timed word $\nu$ to an interval $I$ as $\nu|_I = \{\nu'_l \mid \nu' \preceq_I \nu\}$. As a shorthand, for a timestamp $T$, we write $\nu|_{[0,T]} = \nu|_T$. We overload the term restriction of $\nu$ to $I$ because of the characterization of Lemma 1 below: the syntactic restriction corresponds to the semantic approach of taking the language of timed words associated with $\nu$, and restricting each of its words. This provides us with a way of representing, manipulating and computing restriction of ATW to intervals:

**Lemma 1.** For any approximate timed word $\nu$ and any timestamp $T$, it holds $\cup_{\nu' \in \nu|_T} [[\nu']] = [[\nu]]|_T$.

Following this, we write $[[\nu|_T]]$ for $\cup_{\nu' \in \nu|_T} [[\nu']]$.

*Example 2.* Consider the approximate timed word $\nu = (a, [1,3])(b, [2,4])(c, [3,5])$, and $I = [0,3]$ with the components of the actions being pair-wise different. Then:

- $\nu \cap I$ is the approximate timed word $(a, [1,3])(b, [2,3])(c, \{3\})$.

- assuming that all three events occur on different components (and can then be freely swapped), the set $\{\nu' \mid \nu' \preceq_I \nu\}$ is

$$ \{\epsilon, (a, [1,3]), (a, [1,3])(b, [2,4]), (a, [1,3])(c, [3,5]), \\ (a, [1,3])(b, [2,4])(c, [3,5]), (b, [2,4]), (b, [2,4])(c, [3,5]), (c, [3,5])\} $$

(in other terms, all subwords are allowed, since all intervals intersect $I$ and none of them are included in $I$). It follows that $\nu|_I$ is the union of $\epsilon$, $(a, [1,3])$, $(a, [1,3])(b, [2,3])$, $(a, [1,3])(c, [3,3])$, $(a, [1,3])(b, [2,3])(c, [3,3])$, $(b, [2,3])$, $(b, [2,3])(c, [3,3])$ and $(c, [3,3])$.

Now, assume that $b$ and $c$ relate to the same component, so that they cannot be swapped. In this case, $(a, [1,3])(c, [3,5])$ is no longer a subword of $\nu$ for $I$, because the third condition is no longer fulfilled.
## 2.4 Formalism for timed systems

We monitor properties given as TAs, which are standard formalism for expressing properties of time-constrained systems: the aim of our monitoring procedure is to decide if the execution we are (partially and imprecisely) observing is (or will be) accepted by a given timed automaton. We introduce the formalism of timed automata in this section.

Let $X$ be a finite set of clocks. A clock valuation is a function $v: X \to \mathbb{R}_{\ge 0}$. We write $\mathcal{V}(X)$ for the set of valuations. The initial valuation is $\mathbf{0}: x \in X \mapsto \mathbf{0}$; a time elapse for a delay $t \in \mathbb{R}_{\ge 0}$ maps valuation $v$ to $v+t$: $x \mapsto v(x)+t$, and a clock reset for a subset $X' \subseteq X$ maps $v$ to $v_{[X']}$ such that $v_{[X']}(x) = v(x)$ if $x \notin X'$, and $v_{[X']}(x) = 0$ otherwise.

A zone is a finite conjunction of clock constraints of the forms $x_1 \bowtie n$ and $x_1 - x_2 \bowtie n$, with $x_1, x_2 \in X$, $\bowtie \in \{<, \leq, =, \geq, >\}$ and $n \in \mathbb{N}$. We write $\mathcal{Z}(X)$ for the set of zones of X. We write $v \models z$ and say that $v$ satisfies $z$ when the values of the clocks in $v$ satisfy the constraints in $z$.

**Definition 2.** A timed automaton (TA) is a tuple $\mathcal{A} = (\mathcal{L}, \ell_{init}, \mathbf{Act}, X, E)$ where $\mathcal{L}$ is a finite set of locations containing the initial location $\ell_{init}$, $\mathbf{Act}$ and $X$ are finite sets of actions and clocks respectively, and $E \subseteq \mathcal{L} \times \mathcal{Z}(X) \times \mathbf{Act} \times 2^X \times \mathcal{L}$ is the set of transitions. For a transition $(\ell, g, a, z, \ell') \in E$, we call $\ell$ its source, $\ell'$ its target, $g$ and $a$ its guard and action and $z$ its reset set. We call configurations of $\mathcal{A}$ the triples $(\ell, v, t) \in \mathcal{L} \times \mathcal{V} \times \mathbb{R}_{\ge 0}$, and initial configuration the configuration $(\ell_{init}, \mathbf{0}, 0)$.

**Remark 1.** We add to the usual notion of configuration a date representing the instant at which the system is in this configuration (after a given behaviour). We do this because our reasoning is based on timestamps, not delays, following the definition of timed words based on observations. This can be readily implemented by giving an additional clock (which is never reset) to the TA.

A timed word $\sigma = (a_i, t_i)_{1 \le i}$ is a trace of a timed automaton if, starting from the initial configuration $(\ell_{init}, \mathbf{0}, 0)$, one can find a sequence $\rho = ((\ell_{i-1}, v_{i-1}, t_{i-1}) \xrightarrow{\delta_i} (\ell_{i-1}, v_{i-1} + \delta_i, t_{i-1} + \delta_i) \xrightarrow{e_i} (\ell_i, v_i, t_{i-1} + \delta_i))_{1 \le i}$ with $e_i = (\ell_{i-1}, g_i, a_i, z_i, \ell_i) \in E$, $\delta_i = t_i - t_{i-1}$ (with $t_0 = 0$), and at each step $v_{i-1} + \delta_i \models g_i$ and $v_i = (v_{i-1} + \delta_i)_{[z_i]}$. Such a sequence $\rho$ is called a (finite or infinite) run, and we write $\text{trace}(\rho) = \sigma$. A timed word $\sigma$ is a partial trace if there exists a timed word $\sigma'$ such that $\sigma' \cdot \sigma$ is a trace. A partial trace thus corresponds to a partial run that does not (necessarily) start from $(\ell_{init}, \mathbf{0}, 0)$. For a (partial) trace $\sigma$ with $\text{firstt}(\sigma) \ge t$, we write $(\ell, v, t) \stackrel{\sigma}{\rightsquigarrow_t} (\ell', v', t')$ when $\sigma$ leads from configuration $(\ell, v, t)$ to configuration $(\ell', v', t')$.

A timed automaton is said *deterministic* if for any two transitions $(\ell, g, a, z, \ell')$ and $(\ell, g', a, z', \ell')$ such that $g \cap g' \neq \emptyset$, it holds $g = g'$ and $z = z'$. It is said *complete* when for any configuration $(\ell, v, t)$ and action $a \in \mathbf{Act}$, there is at least a transition $(\ell, g, a, z, \ell')$ such that $v \models g$. When considering complete deterministic automata, the trace function defined above is a bijection, and we identify traces
with their associated runs. In this context, we add the possibility of having a
final delay after a trace: for a configuration $(\ell, v, t)$, a date $t''$ and a (partial)
trace $\sigma$ such that firstt$(\sigma) \ge t$ and lastt$(\sigma) = t' \le t''$ we write $(\ell, v, t)$ after$_t^{t''}$ $\sigma$
for the unique configuration $(\ell', v'', t'')$ such that $(\ell, v, t) \stackrel{\sigma}{\rightsquigarrow}_t (\ell', v', t') \xrightarrow{t''-t'} (\ell', v'', t'')$, i.e., reached from $(\ell, v, t)$ after the trace $\sigma$ followed by the delay $t''-t'$.
This can be generalized to sets of configurations and languages: for a set of
configurations $S$ and a language of timed words $L$, such that $\inf\{\text{firstt}(\sigma) \mid \sigma \in L\} \ge t$ and $\supp\{\text{lastt}(\sigma) \mid \sigma \in L\} \le t''$, $S$ after$_t^{t''}$ $L = \{(\ell', v', t'') \mid \exists(\ell, v, t) \in S, \exists\sigma \in L, (\ell', v', t') = (\ell, v, t) \text{ after}_t^{t''} \sigma\}$. Finally, we define the corresponding
notion when no date is given: $S$ after $L = \{(\ell', v', t') \mid \exists(\ell, v, t) \in S, \exists\sigma \in L, \exists t', (\ell', v', t') = (\ell, v, t) \text{ after}_t^{t'} \sigma\}$. Notice that in this last definition, $t$ and $t'$
are not bound and can range on all values such that after$_t^{t'}$ is defined.

Modelling properties. The property associated with monitor $M_i$ is defined by a deterministic and complete TA $\mathcal{A}_i$ and a subset $\mathcal{F}_i$ of locations specifying a reachability property$^7$: we write $[\mathcal{A}_i, \mathcal{F}_i]$ for the set of (runs of) finite traces $\sigma$ that end in some location of $\mathcal{F}_i$ when applied to $\mathcal{A}_i$ from its initial configuration $(\ell_{init}, \mathbf{0}, 0)$; we extend $[\mathcal{A}_i, \mathcal{F}_i]$ (absusively keeping the same notation) to include runs of infinite traces $\sigma$ for which there is a length $k$ such that all prefixes of $\sigma$ of length larger than $k$ are in $[\mathcal{A}_i, \mathcal{F}_i]$.

Given a property specified by $\mathcal{A}_i$ and $\mathcal{F}_i$, a finite trace $\sigma$ is a good prefix
(resp. bad prefix) if for all infinite continuations $\sigma \cdot \sigma' \in (\mathbf{Act} \times \mathbb{R}_{\ge 0})^\omega$ of $\sigma$,
$\sigma \cdot \sigma' \in [\mathcal{A}_i, \mathcal{F}_i]$ (resp. $\sigma \cdot \sigma' \notin [\mathcal{A}_i, \mathcal{F}_i]$). In terms of automata, this means that
the prefix reached some configuration in $\mathcal{L}_i \times \mathcal{V} \times \mathbb{R}_{\ge 0}$ from which it will always
eventually stay in $\mathcal{F}_i \times \mathcal{V} \times \mathbb{R}_{\ge 0}$ (resp. it never visited and will never visit $\mathcal{F}_i$). We
note this set of configurations $\mathit{Inev}(\mathcal{F}_i)$ (resp. $\mathit{Never}(\mathcal{F}_i)$). Good prefixes (resp. bad
prefixes) are then traces of runs in $[\mathcal{A}_i, \mathit{Inev}(\mathcal{F}_i)]$ (resp. $[\mathcal{A}_i, \mathit{Never}(\mathcal{F}_i)]$). Starting
from $\mathcal{F}_i$, the state sets $\mathit{Inev}(\mathcal{F}_i)$ and $\mathit{Never}(\mathcal{F}_i)$ can be computed off-line by a
zone-based co-reachability analysis [8]. Thanks to this, we restrict our focus to the
reachability of pairs of locations and zones without loss of generality. These notions
can be extended to languages, thus to approximate timed words. A language
$L \in \mathbf{TT}_{\mathbf{Act}}$ is a good (resp. bad) language prefix if $L \subseteq [\mathcal{A}_i, \mathit{Inev}(\mathcal{F}_i)]$ (resp.
$L \subseteq [\mathcal{A}_i, \mathit{Never}(\mathcal{F}_i)]$). These can also be computed using $\mathit{Inev}(\mathcal{F}_i)$ and $\mathit{Never}(\mathcal{F}_i)$.

3 Monitoring with complete information

The role of monitoring algorithms is to provide us with verdicts when analyzing
executions of the system. Since we want this to be performed online, verdicts
should be given as soon as possible, based on the observation of a finite execution
prefix. However, in the context of distributed systems, the observation collected by
a monitor at a given date may be imperfect, with missing events and approximate

<footnote n="7">⁷ We here restrict to deterministic and complete TAs for simplicity, but generalization to non-deterministic and incomplete TAs is easy.</footnote>
dates. We first identify the points in time where we have enough information to decide a verdict in Sect. 3.1, and then define our verdicts of interest in Sect. 3.2. Using this, we explain the data structure we use and its related operations in Sect. 3.3, and explain how to compute a verdict in Sect. 3.4.

## 3.1 Point of Certainty

When the components of the system perform actions, their corresponding monitors $(M_j)_{j \in [1:n]}$ instantly observe these actions and timestamp them with the value of their (local) clock. However, they need to wait for the communication of other monitors in order to collect the information about the other components' events.

**Communication policy.** We consider the simple policy in which each monitor $M_j$ instantly sends its observations (action performed and timestamp) to every other monitor $M_i$ that needs it for checking its property, grouping in the same message all the events that occurred at the same instant<fnref n="8" />. As there are no bounds in communication delays, monitors still have to deal with partial and out-of-order information. Moreover, local time approximation induces imprecision in event dates. To make monitoring sound, we first determine the time point at which we can safely monitor with no missing event.

Formally, consider the global observation $\sigma^o$ such that at a given global time $t^g$, the observation collected by all monitors is hence $\sigma^o_{|t^g}$. We know that the global trace $\sigma^g$ of the run of the system is such that $\sigma^g \in [\nu(\sigma^o)]$. This trace can not be observed, yet it is the one we want to monitor, hence we will start our reasoning from (prefixes of) the language $[\nu(\sigma^o)]$.

Moreover, no single monitor has access to $\sigma^o_{|t^g}$ at time $t^g$ due to the need for synchronization. Let the collected trace at $t$ by $M_i$, written $\sigma_i(t)$, be the monitoring information gathered by a monitor $M_i$ at the $M_i$-local time $t$. It is composed of a subset of the global observation $\sigma^o_{|t+\epsilon}$, containing at least its own local observation $p_i(\sigma^o)|_t$ and events received from other monitors, forming for each monitor $M_j$ a timed word $p_j(\sigma^o)|_{t_j}$ with $t_j \le t + 2\epsilon$. Indeed, communication being FIFO, $M_i$ receives the information from each individual $M_j$ in order, but potentially with $M_j$-local timestamps up to $t + 2\epsilon$, as both the $M_i$-local time $t$ and the $M_j$-local time can skew by a maximum of $\epsilon$ from the global time.

For $M_i$ at $M_i$-local date $t$, consider the set

$$ \{(j, t_j) \in [1; n] \times \mathbb{R}_{\ge 0} | j \ne i \wedge (\text{lastt}(p_j(\sigma_i(t))) = t_j)\} \cup \{(i, t)\} $$

of pairs made of the index $j$ of each monitor coupled with the timestamp of the last observation received from $M_j$ by $M_i$. Let $(\text{jmin}_k)_{k \in [1:n]} = (\text{jmin}_k, \text{tmin}_k)_{k \in [1:n]}$ be the sequence obtained by ordering this set of pairs by ascending timestamp<fnref n="9" />.

<footnote n="8">⁸ This technical detail is useful for Prop. 3 to ensure that all events of same date issued from the same component are collected simultaneously. It can be implemented by waiting any non null delay before sending a message aggregating the observations.</footnote>

<footnote n="9">⁹ We should write $(\text{jmin}_k(t))_{k \in [1:n]} = (\text{jmin}_k(t), \text{tmin}_k(t))_{k \in [1:n]}$, i.e., parametrize by $t$, but we will often forget $t$ when clear from the context.</footnote>
<figure><img src="image_2.png" /><figcaption>Fig. 1: A global finite trace $\sigma^g$ (top), its corresponding global observation $\sigma^o$ at local $M_i$-time $t$ (below) with rectangles figuring global time approximation ($\varepsilon = 0.7$), the collected trace $\sigma_1(t) = (a, 1)(c, 2)(b, 3)(b, 5)(c, 5.5)(a, 7)(a, 10)$ (middle), i.e., observation of $M_1$ completed with some events received from $M_2$ and $M_3$, the projections observed locally by three monitors $M_1, M_2, M_3$ at $t$ (bottom). Dashed lines represent information uncertainty, e.g., $M_1$ ignores what happened after the last event received from each of the other monitors.</figcaption></figure>

Initially, those timestamps are all 0, and any order may be chosen. Then, this sequence with its ordering can be easily maintained on-the-fly when new events are observed or received by $M_i$. Clearly, $(\mathit{jmin}_1, \mathit{tmin}_1)$ identifies the monitor $M_j$ for which $M_i$ is aware of the earliest timestamp (in its local time). In the absence of a skew, $M_i$ would be sure to have complete information from all other monitors at time $\mathit{tmin}_1$, with $\mathit{jmin}_1$ being the monitor for which the last event known by $M_i$ (if any) is the oldest. However, as time is approximated, and since verdicts should be given on global traces, knowing all events at local times up to $\mathit{tmin}_1$ only certifies that all events have been recorded for global time up to $\mathit{tmin}_1 - \varepsilon$, as seen in Ex. 3. Notice that this also entails that the verdict can be given at $t$ only if $t \ge \varepsilon$.

*Example 3.* In Fig. 1, for monitor $M_1$, $\mathit{jmin}_1 = 2$ at time $t$. Yet, if the verdict was given with respect to observations after the last event from $M_2$, the last event from $M_3$, which happened before it but was marked with a later timestamp, would be missed. The verdict should thus restrict to the earliest possible global date for the last event of $M_2$, namely $\mathit{tmin}_1 - \varepsilon$.

Conversely, we are sure that for all monitors, we collected some event with timestamp at least $\mathit{tmin}_1$. As local times are non-decreasing and communications are FIFO, no monitor can send a new observation with global time below $\mathit{tmin}_1 - \varepsilon$. Thus, we know that all events of global time below $\mathit{tmin}_1 - \varepsilon$ have already been collected by $M_i$. The set of possible traces of the system corresponding to that observation is $\nu(\sigma_i(t))|_{\mathit{tmin}_1 - \varepsilon}$. This is the purpose of the first part of the following proposition. The second part claims that, indeed, the observation at $\mathit{tmin}_1(t) - \varepsilon$ is in the set of “tubes” of possible observations of $\sigma^g$ restricted to $\mathit{tmin}_1(t) - \varepsilon$.
<figure><img src="image_3.png" /><figcaption>Fig. 2: Hasse diagram of the verdict preorder</figcaption></figure>

**Proposition 3.** For any monitor $M_i$, at any local time $t \ge \varepsilon$, $\sigma^g_{|tmin_1(t)-\varepsilon}$ belongs to $[\nu(\sigma_i(t))|_{tmin_1(t)-\varepsilon}]$. Similarly, $\sigma_i(t)|_{tmin_1(t)-\varepsilon}$ belongs to $[\nu(\sigma^g)|_{tmin_1(t)-\varepsilon}]$.

## 3.2 Verdicts at $tmin_1 - \varepsilon$

As demonstrated by Prop. 3, at global time $tmin_1 - \varepsilon$ the global trace $\sigma^g_{|tmin_1-\varepsilon}$ necessarily belongs to the language of traces compatible with the collected trace for $M_i$ at local time $t$, restricted to $tmin_1 - \varepsilon$. Consequently, this is a sufficient language to ensure safe monitoring, in the sense that a *definitive verdict* (True, False or *Inconclusive*) for this language built from a current observed trace cannot be changed by future observations.

To go a step further, we add *transient* verdicts to the definitive verdicts: Poss True (resp. Poss False) means that the property can not be falsified (resp. verified), although it is still possible to reach an *inconclusive* verdict instead of a *True* (resp. *False*) one. The induced pre-order of verdicts $\leqsim$ is displayed in Fig. 2. The *verdict function* $V(t)$ then links at each date $t$ the compatible traces $[\nu(\sigma_i(t))|_{tmin_1(t)-\varepsilon}]$ with the property specified by $A_i$. Formally $V(t)$ is

- True when $[\nu(\sigma_i(t))|_{tmin_1(t)-\varepsilon}]$ is a good language prefix;

- False when $[\nu(\sigma_i(t))|_{tmin_1(t)-\varepsilon}]$ is a bad language prefix;

- Inconclusive when $[\nu(\sigma_i(t))|_{tmin_1(t)-\varepsilon}]$ intersects both languages $[A_i, Inev(F_i)]$ and $[A_i, Never(F_i)]$;

- Poss True when $[\nu(\sigma_i(t))|_{tmin_1(t)-\varepsilon}]$ intersects $[A_i, Inev(F_i)]$ but no higher verdict (True or *Inconclusive*) applies;

- Poss False when $[\nu(\sigma_i(t))|_{tmin_1(t)-\varepsilon}]$ intersects $[A_i, Never(F_i)]$ but no higher verdict (False or *Inconclusive*) applies;

- $\perp$ by default, if none of these conditions holds.

Because properties are specified by complete TAs, all traces and their continuations are traces of the TA, and since good/bad prefixes are closed under continuation, verdicts can only progress to higher verdicts in the above pre-order:

**Lemma 4.** For a fixed monitor $M_i$ with a property $(A_i, F_i)$, for any $t' > t$, we have $V(t) \leqsim V(t')$.

In particular, *definitive* verdicts remain true eternally as soon as they hold. We say that $\sigma$ is $\varepsilon$-conclusive when $\nu(\sigma)$ yields a definitive non-*Inconclusive* verdict (recall that $\nu(\sigma)$ depends on $\varepsilon$ for the size of its intervals). Equivalently:

**Definition 5.** For a fixed monitor $M_i$ with a property $(A_i, F_i)$ and a skew $\varepsilon$, we say that a timed word $\sigma$ is $\varepsilon$-conclusive when $[\nu(\sigma)]$ is either a good or a bad language prefix.
## 3.3 Data structure

So far, we have defined verdicts with respect to the language $[\nu(\sigma_i(t))|_{\text{tmin}_1(t)-\varepsilon}]$. However, in order to incrementally compute verdicts when new observations arrive, it will be more adequate to manipulate sets of configurations reached after this language. The next proposition justifies the adequacy of this approach.

**Proposition 6.** The verdict $V(t)$ at $M_i$-local date $t$ can be computed by checking whether the set of configurations $(\ell_{init}, \mathbf{0}, 0)$ after$^{\text{tmin}_1(t)-\varepsilon}$ $[\nu(\sigma_i(t))|_{\text{tmin}_1(t)-\varepsilon}]$ intersects or is included in $\text{Inev}(\mathcal{F}_i)$ or $\text{Never}(\mathcal{F}_i)$.

In the following, we proceed in steps to define the computation of the above set of configurations: first, we decompose the computation on unordered languages into computations on ordered ones, where permutations of events are fixed (Prop. 8). We encode them in a data structure $R(t)$ that represents both the set of configurations reached after some trace in $[\nu(\sigma_i(t))|_{\text{tmin}_1(t)-\varepsilon}]$, and the remaining events necessary for incremental computation. Then, we intersect the sets of configurations with the precise time of interest $(\text{tmin}_1 - \varepsilon)$ to obtain the equality with the above set (Prop. 10). Finally, we show how to incrementally update the proposed data structure when new observations are collected.

*Decomposition of {($\ell_{init}, \mathbf{0}, 0$)} after $[\nu(\sigma_i(t))|_{\text{tmin}_1(t)-\varepsilon}]$.* The separation of an unordered language into a union of ordered ones requires considering permutations of the restriction $\nu(\sigma_i(t))|_{\text{tmin}_1(t)-\varepsilon}$. For this, we define the decomposition of an ATW $\nu$ at some date $T$, as the set of all possible prefixes of $\nu|_T$ paired with the set of events that are yet to be accounted for, as this set will be necessary to incrementally update the data structure.

**Definition 7.** The decomposition of $\nu \in \text{ATW}(\text{Act})$ at global time $T$ is

$$ \mathcal{D}(\nu, T) = \{(f(\nu_1); \nu_2) \mid \nu = \nu_1 \otimes \nu_2 \wedge \nu_1 \preceq_{[0,T]} \nu \wedge f \in \mathcal{F}(\nu_1)\}. $$

For a pair $(\nu_1; \nu_2)$ in $\mathcal{D}(\nu, T)$, $\nu_1$ corresponds to a permutation of an element in $\nu|_T$, while $\nu_2$ lists the remaining events that are not taken into account in $\nu_1$. We can then use the decomposition to express the unordered language of a restriction as a union of ordered ones as follows.

**Proposition 8.** $[\nu|_T] = \bigcup_{(\nu_1; \nu_2) \in \mathcal{D}(\nu, T)} [[\nu_1 \cap [0, T]]]_{\text{ord}}$

We are now ready to define our data structure $R(t)$ (we should write $R_i(t)$ but the monitor is clear from the context), which encodes the configurations reached through each $\nu_1$ in the decomposition, associated with its remainder $\nu_2$:

**Definition 9.** For a monitor $M_i$ and a local time $t$, we define $R(t)$, as

$$ R(t) = \{(\ell_{init}, \mathbf{0}, 0) \text{ after } [\nu_1]_{\text{ord}}; \nu_2) \mid (\nu_1; \nu_2) \in \mathcal{D}(\nu(\sigma_i(t)), \text{tmin}_1(t) - \varepsilon)\}. $$
The set $\mathbb{R}(t)$ represents a set of configurations in which the system can be after some sequence of events in $\nu(\sigma_i(t))|_{\text{tmin}_1(t)-\varepsilon}$. A restriction to dates before $\text{tmin}_1(t) - \varepsilon$ is still necessary (see the intersection with $[0, T]$ in Prop. 8). In order to add this constraint, we call state of $\mathbb{R}(t)$ the set of configurations $\text{state}(\mathbb{R}(t)) = \bigcup_{(S, \nu_2) \in \mathbb{R}(t)} \{(\ell, v, t) \in S \mid t = \text{tmin}_1(t) - \varepsilon\}$ and get the desired equality:

**Proposition 10.** state($\mathbb{R}(t)$) = $\{(\ell_{\text{init}}, 0, 0)\}$ after$_0^{\text{tmin}_1(t)-\varepsilon}$ $[[\nu(\sigma_i(t))|_{\text{tmin}_1(t)-\varepsilon}]$

*Example 4.* Let us consider the example from Fig. 1 with the collected trace at time $t = 10$ being $\sigma_i(t) = (a, 1)(c, 2)(b, 3)(b, 5)(c, 5.5)(a, 7)(a, 10)$ and the skew $\varepsilon = 0.7$. We have $\text{tmin}_1 - \varepsilon = 4.8$. We first have to consider the set $C$ of all possible configurations reached by an interleaving of the first three observations $(a, 1)(c, 2)(b, 3)$. Then, we have to consider every case for the events $(b, 5)(c, 5.5)$ that can occur before or after $\text{tmin}_1 - \varepsilon$. $\mathbb{R}(10)$ is then composed of the following elements, for each $c \in C$:

- $(c; \nu((b, 5)(c, 5.5)(a, 7)(a, 10))),$ meaning that all events occur after time 4.8;

- $(c \text{ after } [[(b, [4.3, 5.7])]_{\text{ord}}; \nu((c, 5.5)(a, 7)(a, 10)))$, considering that the event $b$ happened before time 4.8;

- $(c \text{ after } [(c, [4.8, 6.2])]_{\text{ord}}; \nu((b, 5)(a, 7)(a, 10))),$ considering that $c$ occured before time 4.8.

- the two elements $(c \text{ after } [[(b, [4.3, 5.7])(c, [4.8, 6.2])]_{\text{ord}}; \nu((a, 7)(a, 10)))$ and $(c \text{ after } [(c, [4.8, 6.2])(b, [4.3, 5.7])]_{\text{ord}}; \nu((a, 7)(a, 10)))$ considering that both $b$ and $c$ occurred before time 4.8, thus both orderings should be considered.

Note that $\mathbb{R}(10)$ contains configurations that can only be reached if the collected events occur after $\text{tmin}_1 - \varepsilon$, but they do not appear in state($\mathbb{R}(10)$), since we only consider configurations that are reached at time $\text{tmin}_1 - \varepsilon$, meaning that the events leading to these configurations must have occurred before this time.

*Updates of R.* When time passes, new events may be collected. If they do not change $\text{tmin}_1$, the only updates to $\mathbb{R}$ is their addition to $\nu_2$. If $\text{tmin}_1$ changes at $t' > t$ because of newly collected events $\nu'$, then the combination of $\mathbb{R}(t)$ and $\nu'$ contains all the necessary information to update $\mathbb{R}$, as each element of $\mathbb{R}(t)$ encodes all of $\nu(\sigma_i(t))|_{\text{tmin}_1(t)-\varepsilon}$. Thus, updating the structure is only a matter of selecting, for each $(S, \nu_2) \in \mathbb{R}(t)$, the possible sub-words of $\nu_2 \cdot \nu'$ to apply after $S$.

**Proposition 11.** Let $t' \ge t$ and $\nu'$ be the sequence of events received in the interval $(t, t']$ (i.e., such that $\sigma_i(t') = \sigma_i(t) \otimes \nu'$), then

$$R(t') = \{(S \text{ after } [[\nu'_1]_{\text{ord}}; \nu'_2) \mid (S; \nu_2) \in \mathbb{R}(t), (\nu'_1, \nu'_2) \in \mathcal{D}(\nu_2 \otimes \nu', \text{tmin}_1(t') - \varepsilon)\}.$$

Intuitively, for each pair $(S, \nu_2)$ in $\mathbb{R}(t)$, the extension of $\nu_2$ with the newly collected events $\nu'$ is decomposed at $\text{tmin}_1(t') - \varepsilon$. For each possible element $(\nu'_1, \nu'_2)$ in this decomposition, $\mathbb{R}(t')$ builds the pair made of the set $S$ after $[[\nu'_1]_{\text{ord}}$ associated with the remainder $\nu'_2$. We call next($\mathbb{R}(t), t'$) the function that computes $\mathbb{R}(t')$ at the time $t'$ when $\text{tmin}_1(\cdot)$ changes according to Prop. 11. We now have a data structure that can be used to compute the set of configurations needed to infer verdicts (Prop. 10) and can be updated incrementally based on the new collected observations and $\text{tmin}_1(\cdot) - \varepsilon$ (Prop. 11).
### 3.4 Monitoring at $tmin_1(\cdot) - \varepsilon$

The previous discussions lead to the monitoring algorithm presented in Algorithm 1. It uses a triple of boolean values $(I, N, C)$ encoding the intersection of state($R$) respectively with $Inev(\mathcal{F}_i)$, $Never(\mathcal{F}_i)$ and the complement of their union. The algorithm starts with $R$ being the initial state with no remaining events, the minimal time for monitoring $tmin = \varepsilon$, $jtmin$ initially set to $(k, 0)_{k \in \llbracket 1; n \rrbracket}$. Each new collected sequence of observations from a monitor $M_j$ (recall that monitors group all events with same date in a unique message) is added to all continuations $\nu$ in $R$, and $jtmin$ is updated. If $tmin_1$ has changed, $tmin$ and $R$ are updated (as discussed above). The update of $(I, N, C)$ determines the verdict which is returned if definitive (a lazy evaluation of $(I, N, C)$ optimizes the update, $I$ and $N$ being non-decreasing, while $C$ is non-increasing). We do not detail here the communication of verdicts between monitors which could help anticipate their termination.

<table><caption>**Algorithm 1:** The monitor $M_i$'s algorithm to monitor at $tmin_1(\cdot) - \varepsilon$.</caption><thead><tr><th></th><th></th></tr></thead><tbody><tr><td>Init:</td><td>R = {((<i>l</i><sub>init</sub>, 0, 0); [])}; tmin = ε; jtmin = (k, 0)<sub>k∈{1,n}</sub>; verdict(i) := ⊥;<br>(I, N, C) := ((<i>l</i><sub>init</sub>, 0, 0) ∈ Inev(<i>F</i><sub>i</sub>), (<i>l</i><sub>init</sub>, 0, 0) ∈ Never(<i>F</i><sub>i</sub>), ¬(I ∨ N));</td></tr><tr><td>1</td><td>while True do</td></tr><tr><td>2</td><td>Receive sequence (<i>a</i><sub>1</sub>, <i>t</i><sub>a</sub>) ... (<i>a</i><sub>n</sub>, <i>t</i><sub>a</sub>) from monitor <i>M</i><sub>j</sub>, <i>j</i> ∈ {1; n};</td></tr><tr><td>3</td><td>R := {(<i>S</i>, <i>ν</i> ⊗ <i>ν</i>((<i>a</i><sub>1</sub>, <i>t</i><sub>a</sub>) ... (<i>a</i><sub>n</sub>, <i>t</i><sub>a</sub>))) | (<i>S</i>, <i>ν</i>) ∈ <i>R</i>};</td></tr><tr><td>4</td><td>update jtmin;</td></tr><tr><td>5</td><td>if tmin<sub>1</sub> > tmin then</td></tr><tr><td>6</td><td>tmin := tmin<sub>1</sub>;</td></tr><tr><td>7</td><td>R := next(<i>R</i>, tmin<sub>1</sub> - ε);</td></tr><tr><td>8</td><td><i>I</i> := <i>I</i> ∨ (state(<i>R</i>) ∩ Inev(<i>F</i><sub>i</sub>) ≠ ∅);</td></tr><tr><td>9</td><td><i>N</i> := <i>N</i> ∨ (state(<i>R</i>) ∩ Never(<i>F</i><sub>i</sub>) ≠ ∅);</td></tr><tr><td>10</td><td><i>C</i> := <i>C</i> ∧ (state(<i>R</i>) ∩ <span style="text-decoration: overline;">Inev(<i>F</i><sub>i</sub>) ∪ Never(<i>F</i><sub>i</sub>)</span>) ≠ ∅;</td></tr><tr><td>11</td><td>switch (<i>I</i>, <i>N</i>, <i>C</i>) do</td></tr><tr><td>12</td><td>case (1, 1, *) do return (verdict(i):=Inconclusive);</td></tr><tr><td>13</td><td>case (1, 0, 0) do return (verdict(i):=True);</td></tr><tr><td>14</td><td>case (0, 1, 0) do return (verdict(i):=False);</td></tr><tr><td>15</td><td>case (1, 0, 1) do verdict(i):=Poss True;</td></tr><tr><td>16</td><td>case (0, 1, 1) do verdict(i):=Poss False;</td></tr></tbody></table>

**Proposition 12.** *Algorithm 1 sets the verdict to $V(t)$.*

We can prove the following soundness and completeness of the monitoring algorithm. Notice that completeness is limited to $2\varepsilon$-conclusive executions.

**Theorem 13.** *Monitoring at $tmin_1(\cdot) - \varepsilon$ is sound and complete where, for any local monitor $M_i$ and its property $(A_i, \mathcal{F}_i)$:*

soundness means that for any global trace $\sigma^g \in \text{TT}(\text{Act})$ produced at date $T \in \mathbb{R}_{\ge 0}$, if $\text{verdict}(i) = \text{True}$ at time $T$, then $\sigma^g$ is a good prefix of $(A_i, \mathcal{F}_i)$
(respectively, if verdict(i) = False at time T, then σ⁹ is a bad prefix of (Aᵢ, Fᵢ)). Furthermore, if verdict(i) = Inconclusive, then neither σ⁹ nor its possible continuations are 2ε-conclusive on (Aᵢ, Fᵢ).

completeness means that for any global trace σ<sup>g</sup> ∈ TT(Act), if a prefix of σ<sup>g</sup> is 2ε-conclusive and good (respectively, bad) on (A<sub>i</sub>, F<sub>i</sub>) then there exists some date T ∈ R<sub>≥0</sub> such that verdict(i) = True (respectively, verdict(i) = False).

4 Conclusion

This paper presents a distributed approach to monitor properties specified as
deterministic timed automata when faced with approximation on events dates.
The approach relies on the identification of the point in time at which sufficient
information has been gathered by the local monitor to compute a verdict and
the incremental computation of the set of states of the property compatible with
the collected observation at this point in time This requires the careful account
of potential permutations of events emanating from distant components.

This method allows to apply monitoring on complex systems that are dis-
tributed in space and whose behaviours depend strongly on time, further increasing
the reach of this popular runtime verification method. It is interesting to notice
the timely nature of this contribution, as the interest for distributed systems is
developing not only in verification (see related works) but also in model learning
([24,22] discrete time), which could soon allow to automatically generate mod-
els of systems and specifications, allowing—at longer term—for fully black-box
distributed tools requiring no expert knowledge.

While we ensured the soundness and completeness of our algorithm, its
efficiency still needs to be experimented. Future works should include the imple-
mentation and test of this algorithm against realistic models and properties. This
implementation could be then compared to the one presented in [27] that allows
decentralized monitoring of regular timed expressions (but without clock skew),
which can be generated from a timed automaton. Additionally, our algorithm
could be extended in several ways. First, with additional hypotheses (e.g., maxi-
mal throughput of components), we could issue verdicts earlier by anticipating the
occurrence of events. This would require an extension of the structure R, adding
a level of uncertainty. The balance between the gain of anticipation and the cost
of updating this structure would certainly be an issue and requires experimental
tuning. Using similar techniques, we believe we can handle properties defined by
non-deterministic timed automata, at least for one-clock automata [19]. Finally,
we can also try to reduce the communication overhead. Indeed, we assumed that
all the local observations are forwarded to every other monitor, which can be
improved in several ways, depending on the system topology.

***Acknowledgements.*** This work was partially supported by the EPSRC Standard Grant CLeVer (EP/S028641/1).
## References

1. Rajeev Alur and David L. Dill. A theory of timed automata. *Theoretical Computer Science*, 126(2):183-235, 1994.

2. Eugene Asarin, Paul Caspi, and Oded Maler. Timed regular expressions. *J. ACM*, 49(2):172-206, 2002.

3. Christel Baier and Joost-Pieter Katoen. *Principles of Model-Checking*. MIT Press, May 2008.

4. Ezio Bartocci and Yliès Falcone, editors. *Lectures on Runtime Verification*, volume 10457 of *Lecture Notes in Computer Science*. Springer-Verlag, 2018.

5. David Basin, Felix Klaedtke, and Eugen Zălinescu. Runtime verification over out-of-order streams. *ACM Transactions on Computational Logic*, 21(1):1-43, October 2019.

6. Andreas Bauer, Martin Leucker, and Christian Schallhart. Runtime verification for LTL and TLTL. *ACM Trans. Softw. Eng. Methodol.*, 20(4):14:1-14:64, September 2011.

7. Andreas Klaus Bauer and Yliès Falcone. Decentralised LTL monitoring. In Dimitra Giannakopoulou and Dominique Méry, editors, *FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings*, volume 7436 of *Lecture Notes in Computer Science*, pages 85-100. Springer, 2012.

8. Johan Bengtsson and Wang Yi. Timed automata: Semantics, algorithms and tools. In Jörg Desel, Wolfgang Reisig, and Grzegorz Rozenberg, editors, *Lectures on Concurrency and Petri Nets*, volume 2098 of *Lecture Notes in Computer Science*, pages 87-124. Springer-Verlag, 2004.

9. Patricia Bouyer, Léo Henry, Samy Jaziri, Thierry Jéron, and Nicolas Markey. Diagnosing timed automata using timed markings. *Int. J. Softw. Tools Technol. Transf.*, 23(2):229-253, 2021.

10. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem. *Handbook of Model Checking*. Springer-Verlag, April 2018.

11. Christian Colombo and Yliès Falcone. Organising LTL monitors over distributed systems with a global clock. *Formal Methods Syst. Des.*, 49(1-2):109-158, 2016.

12. Antoine El-Hokayem and Yliès Falcone. On the monitoring of decentralized specifications: Semantics, properties, analysis, and simulation. *ACM Trans. Softw. Eng. Methodol.*, 29(1):1:1-1:57, 2020.

13. Yliès Falcone. On decentralized monitoring. In Ayoub Nouri, Weimin Wu, Kamel Barkaoui, and ZhiWu Li, editors, *Verification and Evaluation of Computer and Communication Systems - 15th International Conference, VECoS 2021, Virtual Event, November 22-23, 2021, Revised Selected Papers*, volume 13187 of *Lecture Notes in Computer Science*, pages 1-16. Springer, 2021.

14. Yliès Falcone, Tom Cornebize, and Jean-Claude Fernandez. Efficient and generalized decentralized monitoring of regular languages. In Erika Ábrahám and Catuscia Palamidessi, editors, *Formal Techniques for Distributed Objects, Components, and Systems - 34th IFIP WG 6.1 International Conference, FORTE 2014, Held as Part of the 9th International Federated Conference on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3-5, 2014. Proceedings*, volume 8461 of *Lecture Notes in Computer Science*, pages 66-83. Springer, 2014.

15. Jean-Christophe Filliâtre. Deductive software verification. *International Journal on Software Tools for Technology Transfer*, 13(5):397-403, October 2011.

16. Adrian Francalanza, Jorge A. Pérez, and César Sánchez. Runtime verification for decentralised and distributed systems. In Ezio Bartocci and Yliès Falcone, editors,
*Lectures on Runtime Verification - Introductory and Advanced Topics*, volume 10457 of *Lecture Notes in Computer Science*, pages 176–210. Springer, 2018.

17. Florian Gallay and Yliès Falcone. Decentralized LTL enforcement. In *Pierre Ganty and Davide Bresolin, editors, Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2021, Padua, Italy, 20-22 September 2021*, volume 346 of *EPTCS*, pages 135–151, 2021.

18. Ritam Ganguly, Yingjie Xue, Aaron Jonckheere, Parker Ljung, Benjamin Schornstein, Borzoo Bonakdarpour, and Maurice Herlihy. Distributed runtime verification of metric temporal properties. *Journal of Parallel and Distributed Computing*, 185:104801, 2024.

19. Alejandro Grez, Filip Mazowiecki, Michal Pilipczuk, Gabriele Puppis, and Cristian Riveros. The monitoring problem for timed automata. *CoRR*, abs/2002.07049, 2020.

20. Charles Antony Richard Hoare. An axiomatic basis for computer programming. *Communications of the ACM*, 12(10):576–580, October 1969.

21. Maximilian A. Köhl and Holger Hermanns. Model-based diagnosis of real-time systems: Robustness against varying latency, clock drift, and out-of-order observations. *ACM Transactions on Embedded Computing Systems*, 22(4):68:1–68:48, 2023.

22. Faezeh Labbaf, Jan Friso Groote, Hossein Hojjat, and Mohammad Reza Mousavi. Compositional learning for interleaving parallel automata. In *Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings*, volume 13992 of *Lecture Notes in Computer Science*, pages 413–435. Springer, 2023.

23. Martin Leucker and Christian Schallart. A brief account of runtime verification. *Journal of Logic and Algebraic Programming*, 78(5):293–303, May 2009.

24. Thomas Neele and Matteo Sammartino. Compositional automata learning of synchronous systems. In *International Conference on Fundamental Approaches to Software Engineering*, pages 47–66. Springer Nature Switzerland, 2023.

25. Dejan Nickovic and Oded Maler. AMT: a property-based monitoring tool for analog systems. In *Jean-François Raskin and P. S. Thiagarajan, editors, Proceedings of the 5th International Conference on Formal modeling and analysis of timed systems (FORMATS 2007)*, volume 4763 of *Lecture Notes in Computer Science*, pages 304–319. Springer-Verlag, 2007.

26. Srinivas Pinisetty, Thierry Jéron, Stavros Tripakis, Yliès Falcone, Hervé Marchand, and Viorel Preoteasa. Predictive runtime verification of timed properties. *J. Syst. Softw.*, 132:353–365, 2017.

27. Victor Roussanaly and Yliès Falcone. Decentralised runtime verification of timed regular expressions. In *Alexander Artikis, Roberto Posenato, and Stefano Tonetta, editors, 29th International Symposium on Temporal Representation and Reasoning, TIME 2022, November 7-9, 2022, Virtual Conference*, volume 247 of *LIPIcs*, pages 6:1–6:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.

28. Prasanna Thati and Grigore Rosu. Monitoring algorithms for metric temporal logic specifications. *Electronic Notes in Theoretical Computer Science*, 113:145–162, 2005.

29. Dogan Ulus. Montre: A tool for monitoring timed regular expressions. In *Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I*, volume 10426 of *Lecture Notes in Computer Science*, pages 329–335. Springer, 2017.
30. Yin Wang, Tae-Sic Yoo, and Stéphane Lafortune. Diagnosis of discrete event systems using decentralized architectures. *Discret. Event Dyn. Syst.*, 17(2):233–263, 2007.

31. Xiang Yin and Stéphane Lafortune. Codiagnosability and coobservability under dynamic observations: Transformation and verification. *Autom.*, 61:241–252, 2015.