Monitoring Real-Time Systemsunder Parametric DelayM. Fränzle has been funded by Deutsche Forschungsgemeinschaft under grant FR 2715/5-1 and by the State of Lower Saxony, Zukunftslabor Mobilität.
T.M. Grosen, K.G. Larsen, and M. Zimmermann have been supported by DIREC - Digital Research Centre Denmark.

Martin Fränzle1Thomas M. Grosen2Kim G. Larsen2Martin Zimmermann2

Fränzle et al.

Carl von Ossietzky Universität, Oldenburg, Germany

Aalborg University, Aalborg, Denmark

Online monitoring of embedded real-time systems can be achieved by reduction of an adequate property language, like Metric Interval Temporal Logic, to timed automata and symbolic execution of the resulting automata on the trace observed from the system. This direct construction however only is faithful if observation of the trace is immediate in the sense that the monitor can assign exact time stamps to the actions it observes, which is rarely true in practice due to the substantial and fluctuating parametric delays introduced by the circuitry connecting the observed system to its monitoring device. We present a purely zone-based online monitoring procedure and its implementation which handle such parametric delays exactly without recurrence to costly verification procedures for parametric timed automata.

§ INTRODUCTION

Online monitoring is an important tool to ensure functional correctness of safety-critical systems.
It analyses the execution traces observed from the system during its runtime by determining in real-time whether the observed traces satisfy the system's specification.
Continuous online monitoring consequently is concerned with unbounded time horizons, unlike offline monitoring where a fixed finite trace is analysed after the execution has terminated.
Hence, specifications for online monitoring are typically defined over infinite traces, the most significant approach being temporal logics.
As specifications often include  real-time requirements, e.g., “every request is answered within 10 milliseconds”, we focus here on metric-time temporal logics over timed words.
More precisely, we consider Metric Interval Temporal Logic (MITL) [2], which offers a good balance between expressiveness and algorithmic properties.
For example, the request-response specification above is expressed by the MITL formula $ G_{\ge 0}(\texttt{req} \rightarrow F_{\le 10} \texttt{resp})$.

While the specifications classify infinite traces, the traces observed online and to be checked against the specification remain finite.
Nevertheless, one can still return verdicts: for example, every infinite extension of a finite trace with some request that is not answered within 10 milliseconds violates the request-response specification above.
Hence, violation of the specification is already witnessed by such a finite trace.
Dually, consider the specification “system calibration is completed within 500 milliseconds”, expressed by the formula $F_{\le 500}\texttt{cc}$ with the proposition $\texttt{cc}$ representing the completion of calibration.
Every infinite extension of a finite trace on which the calibration is completed within 400 milliseconds satisfies the specification.
Hence, satisfaction of the specification is already witnessed by such a finite trace.
However, there are also traces and specifications for which no verdict can currently be drawn, like in the situation where no calibration has been observed yet at current time of 350 milliseconds.
As usual, we capture these three situations with the three verdicts $\top$ (satisfaction for every extension), $\bot$ (violation for every extension), and $\unknown$ (inconclusive).

Online monitoring can be achieved by compiling the MITL specification into an equivalent timed Büchi automaton and then symbolically executing the automaton on the observed trace of the system [7, 12].
However, this approach is correct only if the actions of the monitored system can be observed immediately by the monitor.
In practice, there is usually a communication delay between the system and the monitor. This delay is induced by various types of circuitry at their interfaces, like technical sensors, conversion between analog and digital signals, and communication networks forwarding signals to the monitor.

Consequently, the monitored system and the symbolic execution are no longer synchronized but deviate by a delay, for which only bounds, yet not exact values tend to be known.
Even then, one can still provide meaningful verdicts, see Fig. <ref>:
The specification $F_{\le 10} a \land G_{\le 20}\neg b$ expresses that an $a$ occurs within
10 milliseconds and no $b$ occurs within
20 milliseconds. The observed trace shows the first $a$ at 17.3 milliseconds and the first $b$ at 27.1 milliseconds.
This observation only is consistent with satisfaction of the constraint $F_{\le 10} a$ if $a$'s observation delay exceeds 7.3 milliseconds, while satisfaction of $G_{\le 20}\neg b$ requires a delay of at most 7.1 milliseconds for $b$.
When unknown communication delays vary by a jitter of less than 0.2 milliseconds, the specification definitely is violated.

Monitoring under observation delay: at time $t=27.1$ we can conclusively decide that the MITL property $F_{[0,10]}a \land G_{[0,20]}\neg b$ is violated irrespective of the latency of the observation channel, provided its jitter is less than 0.2.

*Our Contribution.
We follow the approach described in McGraw-Hill's Encyclopedia of Networking and Telecommunications [15] where a communication delay consists of a constant part (latency) and varying part (jitter).
Based on previous work by Grosen et al. [12] on online monitoring of MITL specifications without delay via timed Büchi automata, we present a symbolic MITL monitoring algorithm that provides exact verdicts under unknown delay consisting of parametric (i.e. unknown within bounds) latency and jitter.
While an unknown delay is a timing parameter, our construction avoids the semidecidability [3] of analysis for parameterized timed automata, and instead uses only classical clock zones [9].

In addition, our approach has the advantage that it is even more informative than typical monitoring algorithms, which only return a verdict in $\{\top,\bot,\unknown\}$.
Recall the example specification $F_{\le 10} a \land G_{\le 20}\neg b$.
Now, consider a trace with an $a$ occurring after 17.3 milliseconds and a $b$  after 27.5 milliseconds.
Using reasoning as above, one can see that the specification is satisfied when the delay is in the interval $[7.3,7.5)$, while for all other delays it is violated.
Our algorithm, for which we also provide a prototype implementation and experimental evaluation,  computes the set of potential delays under which the specification is satisfied as well as the set of potential delays under which the specification is violated.

All proofs omitted due to space restrictions can be found in the appendix.

*Related Work.
Our automata-based monitoring of finite traces against  specifications over infinite words using the three verdicts $\{\top,\bot,\unknown \}$ follows the seminal work of Bauer et al. [7], who presented monitoring algorithms for LTL and timed LTL.
Their algorithm for timed LTL is based on clock regions [1], while we follow the approach of Grosen et al. [12] and use clock zones [9], whose performance is an order of magnitude faster.
Also, they translated timed LTL into event-clock automata, which are less expressive than the timed Büchi automata () used both by Grosen et al. [12] and here.

As our algorithms work with , we also support MITL specifications, as these can be compiled into .
The monitoring problem for MITL (without delay) has been investigated before.
Baldor et al. showed how to construct a monitor for dense-time MITL formulas by constructing a tree of timed transducers [5].
Ho et al. split unbounded and bounded parts of MITL formulas for monitoring, using traditional LTL monitoring for the unbounded parts and permitting a simpler construction for the (finite-word) bounded parts [13].

There is also a large body of work on monitoring with finite-word semantics.
Roşu et al. focussed on discrete-time finite-word MTL [16], while Basin et al. proposed algorithms for monitoring real-time finite-word properties [6] and compared the differences between different time models. André et al. consider monitoring finite logs of parameterized timed and hybrid systems [19].
Finally, Ulus et al. described monitoring timed regular expressions over finite words using unions of two-dimensional zones [17, 18].

§ PRELIMINARIES

The set of natural numbers (excluding zero) is $\nats$, we define $\nats_0 = \nats \cup \{0\}$, the set of rational numbers is $\rats$, the set of non-negative rational numbers  is $\nnrats$.
the set of real numbers is $\reals$, and the set of non-negative real numbers  is $\nnreals$.
The powerset of a set $S$ is denoted by $\pow{S}$.

*Timed Words.
A timed word over a finite alphabet $\Sigma$ is a pair $\rho = (\sigma, \tau)$ where $\sigma$ is a nonempty word over $\Sigma$ and and $\tau$ is a sequence of non-decreasing non-negative real numbers of the same length as $\sigma$.
Timed words may be finite or infinite; in the latter case, we require $\limsup \tau = \infty$, i.e., time diverges. The set of finite timed words is denoted by $\TSigma^*$ and the set of infinite timed words by $\TSigma^\omega$.
We also represent a timed word as a sequence of pairs $(\sigma_1,\tau_1), (\sigma_2,\tau_2), \ldots$.  If $\rho=(\sigma_1,\tau_1), (\sigma_2,\tau_2), \ldots (\sigma_n,\tau_n)$ is a finite timed word, we denote by $\tau(\rho)$ the total time duration of $\rho$, i.e., $\tau_n$.

If $\rho_1=(\sigma^1_1,\tau^1_1),\ldots,(\sigma^1_n,\tau^1_n)$ is a finite timed word, $\rho_2=(\sigma^2_1,\tau^2_1),(\sigma^2_2,\tau^2_2),\ldots$ is a finite or infinite timed word, and $t \in \nnrats$ then the timed word concatenation $\rho_1 \cdot_t \rho_2$ is defined iff $\tau(\rho_1) \le t$. Then, $\rho_1 \cdot_t \rho_2 = (\sigma_1,\tau_1),(\sigma_2,\tau_2),\ldots$ such that

\[\sigma_i = \begin{cases}
\sigma^1_i & \text{iff } i\le n\\
\sigma^2_{i-n} & \text{else}
\end{cases}\quad\text{and}\quad
\tau_i = \begin{cases}
\tau^1_i & \text{iff } i\le n\\
\tau^2_{i-n}+t & \text{else}.
\end{cases}\]

*Timed Automata.

A timed Büchi automaton () $\aut = (Q, Q_0, \Sigma, C, \Delta, \mathcal{F})$ consists of a finite alphabet $\Sigma$, a finite set $Q$ of locations, a set $Q_0 \subseteq Q$ of initial locations, a finite set $C$ of clocks, a finite set $\Delta \subseteq Q \times Q \times \Sigma \times \pow{C} \times G(C)$ of transitions with $G(C)$ being the set of clock constraints over $C$, and a set $F \subseteq Q$ of accepting locations.
A transition $(q,q',a,\lambda, g)$ is an edge from $q$ to $q'$ on input symbol $a$, where $\lambda$ is the set of clocks to reset and $g$ is a clock constraint over $C$.
A clock constraint is a conjunction of atomic constraints of the form $x \sim n$, where $x$ is a clock, $n \in \nats_0$, and $\sim\ \in \{<, \leq, =, \geq, >\}$.
A state of $\aut$ is a pair $(q,v)$ where $q$ is a location in $Q$ and $v \colon C \rightarrow \nnreals$ is a valuation mapping clocks to their values.
For any $d \in \nnreals$, $v+d$ is the valuation $x \mapsto v(x) + d$.

A run of $\aut$ from a state $(q_0, v_0)$  over a timed word $(\sigma_1, \tau_1)  (\sigma_2, \tau_2)\cdots$ is a sequence of steps
$(q_0, v_0) \transition{1} (q_1,v_1) \transition{2} (q_2,v_2) \transition{3} \cdots $
where for all $i \geq 1$ there is a transition $(q_{i-1},q_{i},\sigma_{i},\lambda_i,g_i)$ such that $v_{i}(x) = 0$ for all $x$ in $\lambda_i$ and $v_{i}(x) = v_{i-1}(x) + (\tau_i - \tau_{i-1})$ otherwise, and $g_i$ is satisfied by the valuation $v_{i-1}+(\tau_{i} - \tau_{i-1})$.
Here, we use $\tau_0 = 0$.
Given a run $r$, we denote the set of locations visited infinitely many times by $r$ as $\infset{r}$.
A run $r$ of $\aut$ is accepting if $\infset{r} \cap F \neq \emptyset$.
The language of $\aut$ from a starting state $(q,v)$, denoted $\lang{\aut,(q,v)}$, is the set of all infinite timed words with an accepting run in $\mathcal{A}$ starting from $(q,v)$.
We define the language of $\aut$, written $\lang{\aut}$, to be $\bigcup_q \lang{\aut,(q,v_0)}$, where $q$ ranges over $Q_0$ and where $v_0(x) = 0$ for all $x \in C$.

*Metric Interval Temporal Logic.
We use Temporal interval logic () to express properties to be monitored; these are subsequently translated into equivalent which we use in our monitoring algorithm.

The syntax of formulas over a finite alphabet $\Sigma$ is defined as
\varphi ::= p \mid  \neg \varphi \mid  \varphi \vee \varphi \mid  X_I \varphi \mid  \varphi\ U_{I} \varphi\
where $p \in \Sigma$ and $I$ ranges over non-singular intervals over $\nnreals$ with endpoints in ${\nats \cup \{\infty\}}$.
We  write $\shortsim\,n$ for $I=\{d\in\nnreals\mid d\shortsim n\}$ for $\shortsim \in \{<,\leq,\geq,>\}$ and $n \in \nats$.

The satisfaction relation $\rho, i \models \varphi$ is defined for infinite timed words $\rho = (\sigma_1,\tau_1),(\sigma_2,\tau_2),\ldots$, positions $i \geq 1$, and formulas $\varphi$:

* $\rho,i \models p $  iff $p = \sigma_i$.

* $\rho,i \models \neg \varphi$ iff $\rho,i \not\models \varphi$.

* $\rho,i \models \varphi \vee \psi$  if $\rho,i \models \varphi$ or $\rho,i \models \psi$.

* $\rho,i \models X_I \varphi$ iff $\rho,(i+1) \models \varphi$ and $\tau_{i+1} - \tau_i \in I$.

* $\rho,i \models \varphi\ U_{I} \psi$ iff  there exists $k \geq i$ s.t. $\rho,k \models \psi$, $\tau_k - \tau_{i} \in I$, and $\rho,j \models \varphi$ for all $i \leq j < k$.

We write $\rho \models \varphi$ whenever $\rho, 1 \models \varphi$.  We also define the standard syntactic sugar:
$\true = p \vee \neg p$,
$\varphi \wedge \psi = \neg (\neg \varphi \vee \neg \psi)$,
$F_{I} \varphi = \true\ U_{I} \varphi$,
and $G_{I} \varphi = \neg F_{I} \neg \varphi$.
The language $\lang{\varphi}$ of an formula $\varphi$ is the set of all $\rho \in \TSigma^\omega$ such that $\rho\models\varphi$.

For each formula $\varphi$ there exists a $\aut$ with $\lang{\varphi} = \lang{\aut}$.

Fig. <ref> illustrates Theorem <ref> by providing 's for the formula $F_{[0,10]}a \land G_{[0,20]}\neg b$ from the introduction and its negation.

[node distance = 1.7cm, thick]
(q0)     [state, initial text=]          $q_0$;
(i)   at (0,.85) ;
(q1)     [state, right = of q0]    $q_1$;
(phi)    [state, right = of q1]    $\varphi$;
(notphi) [state, left = of q0]    $\neg\varphi$;

[->, thick] (i) edge (q0);
[->, thick] (q0) edge node[above] $a$ node[below]$x \leq 10$ (q1);
[->, thick] (q1) edge node[above] $a, b$ node[below]$x > 20$ (phi);

[->, thick] (q0) edge[bend right=30] node[above]$b$ (notphi);
[->, thick] (q0) edge[] node[above]$a$ node[below]$x > 10$ (notphi);

[->, thick] (q1) edge[bend left=30] node[above]$b$  node[below]$x\leq20$ (notphi);

[->, thick] (phi) edge [loop below] node[] $a,b$ (phi);
[->, thick] (q1) edge [loop below] node[above right=0.1cm] $a$ node[right] $x \leq 20$ (q1);
[->, thick] (notphi) edge[loop below] node[]$a,b$ (notphi);

An automaton for the language of the property $\varphi = F_{[0,10]}a \land G_{[0,20]}\neg b$ and its negation: If location $\varphi$ is accepting then it accepts $L(\varphi)$, if location $\neg\varphi$ is accepting then it accepts $L(\neg \varphi)$.

§ MONITORING UNDER DELAYED OBSERVATION

According to McGraw-Hill's Encyclopedia of Networking and Telecommunications [15], a communication delay consists of a constant part (latency) and varying part (jitter). We describe the delay as a pair $(\lat, \jit) \in \nnreals^2$ where $\lat$ is the constant latency for all signals and $\jit$ is the bound on the jitter. Thus, all signals from the system are delayed within $[\lat, \lat + \jit]$ before they arrive at the monitor.

In the simplest case, our obligation is to monitor violation of an MITL specification $\varphi$ by a system while observing the events through a channel $\chan$ featuring a constant, yet unknown (up to given, but maybe trivial, lower bound $l \in \nnreals$ and upper bound $u \in \nnreals$) transportation latency $\lat \in [l,u]$ and a varying jitter bounded by $\jit \in \nnreals$.

Fig. <ref> shows an example of a property and an observation that conclusively violates the specification at time 27.1, even if the channel latency $\lat \in[0,\infty[$ is unknown, as long as the
jitter is bounded by $0.2$.

We begin by formalizing the concept of observation, where the occurrence of observed events is constrained by a set $\delays$ capturing known bounds on the delay.

A delay set $\delays$ is a nonempty subset of $\nnreals^2$.
A $\delays$-observation is a finite timed word $\rho^*=(\sigma^*_1,\tau^*_1),\ldots,(\sigma^*_m,\tau^*_m)$ with $\tau_1^* \ge \lat$ for some $(\lat,\jit) \in\delays$.

As the ground-truth occurrence times of events in the system cannot be determined exactly from their delayed copies that the monitor receives through the communication channel, we have to consider all ground-truth timed words that the particular observation is consistent with, as follows.[Note that we simplify our definitions by assuming that jitter does not change the order of observations. Under the assumption that only a bounded number of events can be generated by the system in each unit of time, it is possible to take overtaking of events into account, by looking at all consistent permutations.
We refrain from doing so for the sake of clarity.]

A finite timed  word $\rho=(\sigma_1,\tau_1),\ldots,(\sigma_n,\tau_n)$ is consistent with a $\{(\lat,\jit)\}$-observation $\rho^*=(\sigma^*_1,\tau^*_1),\ldots,(\sigma^*_m,\tau^*_m)$ at observation time $t \in \nnreals$ under latency $\lat$ and jitter $\jit$ iff

* $\tau_i \le t$ for each $i\in\{1,\ldots,n\}$ and and $\tau^*_j \le t$ for each $j\in\{1,\ldots,m\}$,

* $n \ge m$, and $\sigma_i = \sigma^*_i$ and $\tau_i + \lat -\tau^*_i \in [0,\jit] $  for all $i \in \{1,\ldots,m\}$, and

* if $ n > m $ then $ \tau_{m+1} + \lat + \jit \ge t$.

We denote the set of timed words $\rho$ that are consistent with an $\{(\lat,\jit)\}$-observation $\rho^*$ at observation time $t$ under latency $\lat$ and jitter $\jit)$ by $\GT_{\lat,\jit}(\rho^*,t)$.
Then, we define $\GT_\delays(\rho^*,t)=\bigcup_{(\lat,\jit)\in\delays}\GT_{\lat,\jit}(\rho^*,t)$.

$\GT_\delays(\rho^*,t)$ thus collects the possible ground-truths that are consistent with the observation $\rho^*$ when the time elapsed since the system has started is $t$, and the delay $(\lat,\jit)$ is within the set $\delays$. Note that $\GT_\delays(\rho^*,t)$ is always nonempty, if $\rho^*$ is a $\delays$-observation and $t \ge \tau(\rho^*)$.

A monitor obviously ought to supply a verdict iff that verdict applies across all possible ground-truth timed words that the observed word explains.

Given a language $L \subseteq \TSigma^\omega$, a set of possible observation delays $\delays$, a $\delays$-observation $\rho^* \in \TSigma^*$, and an observation time $t \ge \tau(\rho^*)$, the function $\evalfuncsymbol_{\delays} \colon \pow{\TSigma^\omega}\rightarrow \TSigma^*  \times \nnreals \rightarrow \verdicts$ evaluates to the verdict

\[
\evalfuncd{\delays}{L}{\rho^*,t} = \left.
\begin{cases}
\top & \text{if } \rho \cdot_t \mu \in L $ for all $\rho \in \GT_{\delays}(\rho^*,t)$ and all $ \mu \in \TSigma^{\omega}, \\
\bot & \text{if } \rho \cdot_t \mu \notin L $ for all $\rho \in \GT_{\delays}(\rho^*,t)$ and all $ \mu \in \TSigma^{\omega}, \\
\unknown & \text{otherwise}.
\end{cases}
\right.
\]

$\evalfuncd{\delays}{L}{\rho^*,t}$ is undefined when $t < \tau(\rho^*)$.

Consider the property $\varphi = F_{[0,10]}a \land G_{[0,20]}\neg b$ and observed word $\rho^*=(a, 17.3), (b, 27.1)$ shown in Fig. <ref>, time point $t = 27.1$, and set of delays $\delays = \{(\lat, \jit) \mid \jit = 0.2\}$.
As the jitter is bounded by $0.2$, in all ground truths either $a$ occurred after time point 10, or $b$ occurred before time point 20. Thus, all extensions of all possible ground truths satisfy $\neg\varphi$, i.e., $\evalfuncd{\delays}{L(\varphi))}{\rho^*,t} = \bot$.

Note that for the special case of $\delays=\{(0,0)\}$ we cover classical (i.e., delay-free) monitoring [12].
Before we turn our attention to computing $\evalfuncsymbol$ we study some properties of our definition. First, let us note that the ability to make firm verdicts increases with increased certainty of the observation channel delay.

Let $L \subseteq \TSigma^\omega$, $\rho^* \in \TSigma^*$, let $\delays \subseteq \delays'$ be delay sets, let $\rho^*$ be a $\delays$-observation, and let $t \ge \tau(\rho^*)$.
Then, $\evalfuncd{\delays'}{L}{\rho^*,t}=\top$ implies $\evalfuncd{\delays}{L}{\rho^*,t}=\top$ and $\evalfuncd{\delays'}{L}{\rho^*,t}=\bot$ implies $\evalfuncd{\delays}{L}{\rho^*,t}=\bot$.

As a refinement of the verdict function in Definition <ref>, one may provide information about the delays $(\lat,\jit)$ that can explain an observation.
Given $L \subseteq \TSigma^\omega$, a finite timed word $\rho^* \in \TSigma^*$, and $t \ge \tau(\rho^*)$, the set of delays $\Delta(L,\rho^*,t)$ that are consistent with the observation $\rho^*$ at $t$ is defined as

\[ \Delta(L,\rho^*,t) = \{ (\lat,\jit) \mid
\exists \rho\in\GT_{\lat,\jit}(\rho^*,t)\, \exists \mu\in\TSigma^{\omega} \text{ s.t. }\rho \cdot_t \mu \in L\}. \]

We denote by $\Delta_{\delays}(L,\rho^*,t)$ the set $\Delta(L,\rho^*,t) \cap \delays$.
Now we can characterize the conclusive monitoring verdicts via these delay sets.

Given $L \subseteq \TSigma^\omega$, a set $\delays$ of delays, a $\delays$-observation $\rho^* \in \TSigma^*$, and $t \ge \tau(\rho^*)$, we have

* $\Delta_{\delays}(L,\rho^*,t)=\emptyset$ iff $\evalfuncd{\delays}{L}{\rho^*,t}=\bot$, and

* $\Delta_{\delays}(\overline{L},\rho^*,t)=\emptyset$ iff $\evalfuncd{\delays}{L}{\rho^*,t}=\top$.

But even in the case when both delay-sets are nonempty (i.e., the verdict is $\unknown$) we can still provide useful information in terms of the sets $\Delta(L, \rho^*, t)$ and $\Delta(\overline{L}, \rho^*, t)$ of consistent delays.
In particular, the set of consistent delays is non-increasing during observations.
To explain this, we first define a notion of extensions for finite timed words (w.r.t. a current time instants $t,t'$).
Formally, let $\rho=(\sigma_1,\tau_1),\ldots,(\sigma_n,\tau_n)$ and $\rho'=(\sigma'_1,\tau'_1),\ldots,(\sigma'_{n'},\tau'_{n'})$ be two finite timed words. Also let $t, t' \in \nnreals$.
Then, we define $(\rho,t)\sqsubseteq (\rho',t')$, if $n\leq n'$,  $\sigma_i=\sigma'_i $ and $\tau_i=\tau'_i$ for all $i\leq n$, and either $n = n'$ and $t\leq t'$ or $n< n'$ and $t\leq \tau'_{n+1}$.
By extending the observations, we (potentially) reduce the set of consistent delays.

Let $(\rho_1^*,t_1)\sqsubseteq (\rho_2^*,t_2)$ for finite timed words $\rho_1^*,\rho_2^*$ and $t_1 \ge \tau(\rho_1^*)$ and $t_2 \ge \tau(\rho_2^*)$. Then, $\Delta(L,\rho_1^*,t_1)\supseteq\Delta(L,\rho_2^*,t_2) $.

Another interesting point is that in some cases, no extension of the observed word will provide a definitive verdict.

Consider the language $L(F_{\le 10}a)$, the observation $\rho^* = (a,15)$, and the set $\delays = \{(\lat, 0) \mid \lat \in [0,10]\}$ of delays.
For any given $t \ge \tau(\rho^*)$ the set of consistent delays are $\Delta_\delays(L, \rho^*, t) = \{(\lat, 0) \mid \lat \in [5, 10]\}$ and $\Delta_\delays(\overline{L}, \rho^*, t) = \{(\lat, 0) \mid \lat \in [0, 5)\}$, i.e., both sets of consistent delays are a strict subset of $\delays$.
Further, due to Lemma <ref>, this will be the case, no matter what observations occur in the future.
Then, the verdict is $\unknown$, even if additional observations occur.

The following lemma formalizes this: as soon as the set of consistent delays w.r.t. $L$ ($\overline{L}$) is no longer equal to $\delays$, then the verdict cannot be $\top$ ($\bot$) anymore.

Let $L \subseteq \TSigma^\omega$, $\delays$ be a set of delays, and $\rho^*=(\sigma^*_1,\tau^*_1),\ldots,(\sigma^*_m,\tau^*_m)$ a nonempty $\delays$-observation. Then, for all $t > \tau(\rho^*)$

* $\Delta_\delays(L,\rho^*, t) \subsetneq \delays \cap \{(\lat, \jit) \mid \lat \le \tau^*_1\} $ implies there is no $ \rho^*_1\in\TSigma^*$ such that $ \evalfuncd{\delays}{L}{\rho^* \cdot_t \rho^*_1, t'} = \top $ for any $ t' \ge t+\tau(\rho^*_1)$, and

* $\Delta_\delays(\overline{L},\rho^*, t) \subsetneq \delays \cap \{(\lat, \jit) \mid \lat \le \tau^*_1\} $ implies there is no $ \rho^*_1\in\TSigma^*$ such that $ \evalfuncd{\delays}{L}{\rho^* \cdot_t \rho^*_1, t'} = \bot  $ for any $ t' \ge t+\tau(\rho^*_1)$.

Note that $\Delta_\delays(L,\rho^*, t) \subsetneq \delays \cap \{(\lat, \jit) \mid \lat \le \tau^*_1\} $ and $\Delta_\delays(\overline{L},\rho^*, t) \subsetneq \delays \cap \{(\lat, \jit) \mid \lat \le \tau^*_1\} $ can both be true simultaneously (as in Example <ref>). In this situation, we will under no future observation reach a conclusive verdict.

§ TOWARDS AN IMPLEMENTATION

Typically, monitoring algorithms rely on automata-based techniques.
To this end, first the specification and its complement are translated into suitable automata.
Then one computes the set of states reachable by processing the observation and then checks whether from one these states the automaton can still accept an infinite continuation. If this is the case for both automata, then the verdict is $\unknown$, if it is only the case for the automaton for the specification, then the verdict is $\top$, and vice versa for the complement automaton and $\bot$.

We want to follow the same blueprint, but we need to make adjustments to handle delay.
Intuitively, we need to compute all states that are reachable by possible ground-truths of a given observation.
However, a ground-truth may contain more events than the observation, as some events may not yet have been observed due to delay.
This complicates the construction of the set of reachable states, as an unbounded number of events may not yet have been observed.

In the definition of $\GT_\delays$ there is an implicit universal quantification over all possible sequences of such events that have not yet been observed.
We exploit the fact that the verdicts are defined with respect to all possible extensions $\mu$ of a possible ground-truth (i.e., also a universal quantification over the $\mu$'s) to move the universal quantification over events that have not yet been observed to the universal quantification of the extension $\mu$.
Then, a possible ground-truth has exactly the same number of events as the observation. We begin defining this restricted notion of possible ground-truth by strengthening Definition <ref>.

A finite timed  word $\rho=(\sigma_1,\tau_1), \ldots, (\sigma_n,\tau_n)$ is EL-consistent with a $\{(\lat,\jit)\}$-observation $\rho^*=(\sigma^*_1,\tau^*_1),\ldots,(\sigma^*_m,\tau^*_m)$ at observation time $t \in \nnreals$ under latency $\lat$ and jitter $\jit$ iff $\rho$ is consistent with $\rho^*$ at $t$ under $\lat$ and $\jit$ and $m = n$.
We denote the set of timed words $\rho$ that are EL-consistent with an observed timed word $\rho^*$ at observation time $t$ under latency $\lat$ and jitter $\jit$ by $\GT^\strict_{\lat,\jit}(\rho^*,t)$ and define $\GT^\strict_\delays(\rho^*,t) = \bigcup_{(\lat,\jit)\in\delays}\GT^\strict_{\lat,\jit}(\rho^*,t)$.

Now, we present the revised verdict function using only EL ground-truths. Note that moving the unobserved events from the possible ground-truth $\rho$ to the extension $\mu$ requires changing the time instant at which we concatenate the ground-truth and the extension: $t - (\lat + \jit)$ is the earliest time point at which an event can occur that may not yet have been observed at time $t$. Due to jitter however, there might also be events after $t - (\lat + \jit)$ that have been observed, which are in the possible ground-truth $\rho$: the last such event happened at time $\tau(\rho)$. Hence, we need to concatenate at time point $\max(\tau(\rho), t - (\lat + \jit))$.

Given $L \subseteq \TSigma^\omega$, a set $\delays$ of delays, a $\delays$-observation $\rho^* \in \TSigma^*$, and $t \ge \tau(\rho^*)$, the function $\evalfuncsymbolstrict_{\delays} \colon \pow{\TSigma^\omega}\rightarrow \TSigma^*  \times \nnreals \rightarrow \verdicts$ evaluates to the verdict

\[
\evalfuncdstrict{\delays}{L}{\rho^*,t} = \left.
\begin{cases}
\top & \text{if $\rho \cdot_{\max(\tau(\rho), t - (\lat + \jit))} \mu \in L $ for all $(\lat,\jit) \in \delays$,}\\
&\text{all $\rho \in \GT^\strict_{\lat,\jit}(\rho^*,t)$ and all $ \mu \in \TSigma^{\omega}$}, \\
\bot & \text{if $\rho \cdot_{\max(\tau(\rho), t - (\lat + \jit))} \mu \notin L $ for all $(\lat,\jit) \in \delays$,}\\
&\text{all $\rho \in \GT^\strict_{\lat,\jit}(\rho^*,t)$ and all $ \mu \in \TSigma^{\omega}$}, \\
\unknown & \text{otherwise}.
\end{cases}
\right.
\]

$\evalfuncdstrict{\delays}{L}{\rho^*,t}$ is undefined when $t < \tau(\rho^*)$.

Next, we show that both verdict functions coincide.

$\evalfuncdstrict{\delays}{L}{\rho^*,t} = \evalfuncd{\delays}{L}{\rho^*,t}$ for all $L \subseteq \TSigma^\omega$, all sets $\delays$ of delays, all $\delays$-observations $\rho^*$, and all $t \ge \tau(\rho^*)$.

Next, we show that we can indeed make the definition of $\evalfuncsymbolstrict$ effective using automata-theoretic constructions.
First, we formally capture the set of states that can be reached by processing the possible EL ground-truths of an observation. Let $\aut$ be a .
We write $(q_0, v_0) \xrightarrow{\rho}_\aut (q_n, v_n)$ for a finite timed word $\rho = (\sigma, \tau) \in \TSigma^*$ to denote the existence of a finite sequence of states $(q_0, v_0) \transition{1} (q_1,v_1) \transition{2} \cdots \transition{n} (q_n,v_n)$
of $\aut$ where for all $1 \leq i \leq n$ there is a transition $(q_{i-1},q_{i},\sigma_{i},\lambda_i,g_i)$ of $\aut$ such that $v_{i}(x) = 0$ for all $x$ in $\lambda_i$ and $v_{i-1}(x) + (t_i - t_{i-1})$ otherwise, and $g$ is satisfied by the valuation $v_{i-1}+(t_{i} - t_{i-1})$, where we use $t_0 = 0$.
Given a  $\aut$, a set $\delays$ of delays, a finite observed timed word $\rho \in \TSigma^*$, and $t \ge \tau(\rho)$,
we define

\begin{align*}
\terminal{\aut}{\delays}{\rho^*,t} = \{ &(q, v + \max(0,(t - (\tau(\rho) + \lat +\jit)))) \mid (q_0, v_0) \xrightarrow{\rho}_\aut (q, v) \text{ where }\\
& (q_0, v_0) \text{ with } q_0 \in Q_0 \text{, } v_0(x)=0 \text{ for all $c \in C$, and }  \\
&\rho \in \GT^\strict_{\lat,\jit}(\rho^*,t) \text{ for some } (\lat,\jit)\in\delays\}.
\end{align*}

We call this the reach-set of $\rho$ in $\aut$ at $t$ w.r.t. $\delays$.

Next, we define the set of states of a from where it is possible to reach an accepting location infinitely many times in the future, i.e., those states from which an accepting run is possible.
This is useful, because if processing a finite timed word leads to such a state, then the timed word can be extended to an infinite one in the language of the automaton, a notion that underlies the definitions of the verdict functions.
Given a $\aut = (Q, Q_0, \Sigma, C, \Delta, \mathcal{F})$, the set of states with nonempty language is

\[\nonempty{\aut} = \{ (q,v) \mid q \in Q, v \in C \rightarrow \nnreals \text{ s.t. } \lang{\aut, (q,v)} \neq \emptyset \}.\]

The set $\nonempty{\aut}$ can be computed using a zone-based fixpoint algorithm [12].
Using these definitions, we can give an effective definition of the verdict functions, which we show to be equivalent to the previous definitions and implementable.

In the following definition, $\tbaty$ denotes the set of all .

Given a  $\aut$, a complement automaton $\compautomaton$ (i.e., with $\lang{\compautomaton} = \TSigma^\omega \setminus \lang{\aut}$), a set $\delays$ of delays, a $\delays$-observation $\rho \in \TSigma^*$, and $t \ge \tau(\rho)$, ${\monitordelayssymbol \colon \tbaty \times \tbaty \rightarrow \TSigma^* \times \nnreals \rightarrow \verdicts}$ computes the verdict

\[
\monitordelays{\aut, \compautomaton}{\rho^*, t} = \left.
\begin{cases}
\top & \text{if } \terminal{\compautomaton}{\delays}{\rho^*,t} \cap \nonempty{\compautomaton} = \emptyset, \\
\bot & \text{if } \terminal{\aut}{\delays}{\rho^*,t} \cap \nonempty{\aut} = \emptyset, \\
\unknown & \text{otherwise.}
\end{cases}
\right.
\]

$\monitordelays{\aut, \compautomaton}{\rho^*, t}$ is undefined if $t < \tau(\rho)$.

Next we show that this automata-based definition of monitoring is equal to the verdict functions defined above.

$\monitordelays{\aut,\compautomaton}{\rho^*,t} = \evalfuncdstrict{\delays}{\lang{\aut}}{\rho^*,t}$ for all sets $\delays$ of delays, all  $\aut$ (and complement automata $\compautomaton$), all $\delays$-observations $\rho^*$, and all $t \ge \tau(\rho^*)$.

Recall that $\nonempty{\aut}$ can be computed for any given  $\aut$. Therefore, in the next section, we show how to calculate $\terminal{\aut}{\delays}{\rho^*,t}$ for a given  $\aut$, set $\delays$ of delays, observation $\rho^*$, and time point $t$ using a zone-based algorithm. This will then allow us to compute verdicts effectively.

§ A ZONE-BASED MONITORING ALGORITHM

In this section, we demonstrate how to compute the reach-set of $\rho$ in $\aut$ at $t$ w.r.t. $\delays$.
So far we have developed the theory with observations, latency, and jitter being reals.  Now, we are concerned with algorithms and thus assume all these quantities to be rationals.
For the monitoring algorithm, we use – as standard in analysing timed automata models – symbolic states being pairs $(q, Z)$ of locations and zones. A zone is a finite conjunction of constraints of the form $x \sim t$ and $x - x' \sim t$ for clocks $x,x'$, constants $t \in \nnrats$, and $\sim\ \in \{<, \leq, =, \geq, >\}$.
Given two zones $Z$ and $Z'$ over a set $C$ of clocks, and a set of clocks $\lambda \subseteq C$, we define the following operations on zones (which can be efficiently implemented using the DBM data-structure [9]):

* $Z[\lambda] = \{v \mid \exists v' \models Z \: \text{ s.t. }  v(x) = 0 \text{ if } x \in \lambda \text{, otherwise } v(x) = v'(x) \}$

* $Z^\nearrow = \{v \mid \exists v' \models Z \text{ s.t. }  v = v' + d  \text{ for some } d \in \nnreals\}$

* $Z \land Z' = \{v \mid v \models Z \textit{ and } v \models Z'\}$, and

We can use these functions  to compute the successor states after an input. Given a $\aut = (Q, Q_0, \Sigma, C, \Delta, \mathcal{F})$, a symbolic state $(q, Z)$, and a letter $a \in \Sigma$, we define $\post((q, Z), a) = \{ (q', Z') \mid (q,q',a,\lambda,g) \in \Delta, Z' = (Z^\nearrow \land g)[\lambda] \}$, as the set of states one can reach by taking an $a$-transition at some point in the future from $(q, Z)$.
Using $\post$ we can compute the successor states of a timed input $(a, \tau) \in \Sigma \times \nnrats$ by extending the zones with an additional clock $time$ just recording time since system start. The successors of a symbolic state is $\succc((q, Z), (a, \tau)) = \{(q', Z') \mid (q', Z'') \in \post((q, Z), a), Z' = Z'' \land time = \tau\}$ and the successors of a set of symbolic states $S$ is $\succc(S, (a, \tau)) = \bigcup_{(q', Z')\in S} \succc((q', Z'), (a, \tau))$.

In handling delayed observations, we assume that the delay set $\delays$ consists of pairs $(\delta,\varepsilon)$ where the latency $\delta$ is bounded by an interval $[l, u] \subseteq \nnreals$ for given $l,u \in \nnrats$, and that the jitter is bounded by a given $\jit \in \nnrats$.
To represent the latency and thereby be able to reason about and indirectly store the latency bounds, we add a clock $etime$ representing the “expected” real time that an event generated just now could be observed by the monitor after having been delayed according to the latency. This allows us to

* represent the actual latency as $etime-time$,

* represent the initial knowledge about latencies by initializing $etime-time$ to the initially known bounds on latency, namely $etime-time \in [l,u]$ by setting $time$ to 0 and constraining $etime$ to $[l,u]$,

*  refine our knowledge about the actual latency when observing an event $(\sigma^*, \tau^*)$ by then setting $etime$ to a value in $ [\tau^*-\varepsilon,\tau^*]$.

Consequently, we change the initial zones to include the latency bounds $l$ and $u$ as the differences between the clocks $etime$ and $time$. This way, $etime$ represents the expected time an event is observed (at the monitor) and $time$ represents the actual time the event happened (at the system). The aforementioned refinement (see Item <ref> above and Fig. <ref>) then permits to deduce actual latency ranges consistent with the specification (or its negation) from observation times of events.

In detail, this refinement of the $etime-time$ relation works as follows.
Given a $\aut$ extended with the clocks $time$ and $etime$, and an observation $(\sigma, \tau^*) \in \Sigma \times \nnrats$, the successors of $(q, Z)$ are

\begin{align*}
\succc_{d}((q, Z), (\sigma, \tau^*)) = \{(q', Z') \mid (q', Z'') \in \post((q, Z), \sigma),\\ Z' = Z'' \land etime \leq \tau^*  \land etime \geq \tau^* - \jit\}\
\end{align*}

and the successors $\succc_{d}(S, (\sigma, \tau^*))$ of a set of symbolic states $S$ is equal to $\cup_{(q, Z)\in S} \succc_{d}((q, Z), (\sigma, \tau^*))$.

The monitoring algorithm will essentially apply  $\succc_d$ repeatedly to update the reach-set.  The initial reach-set is given by the following zone $Z_0^{d}$ requiring all ordinary clocks of the TBA $\aut$ to be zero and with  $time$ and $etime$ satisfying  $etime - time \in [l, u]$.
That is

\[
Z_0^{d} \equiv
\underbrace{\vphantom{\bigwedge\nolimits_{ x \in C \cup \{\time\}}}\etime - \time \le u \land \time - \etime \le -l\,}_{\etime-\time \in [l,u]} \land
\underbrace{\bigwedge\nolimits_{ x \in C \cup \{\time\}} x = 0 }_{\text{$x_1,\ldots,x_{|C|} = 0$, $\time = 0$}}.
\]

Given a fixed jitter bound $\varepsilon$, we can now compute the reach-set after a sequence of observations under delay, where the latency is bounded in $[l,u]$.

Given a $\aut$,
a delay set $\delays = \{(\lat, \jit) \mid \lat \in [l, u]\}$ with $l, u, \jit \in \nnrats$,
a $\delays$-observation $\rho^* = (\sigma_1, \tau^*_1),\ldots,(\sigma_n, \tau^*_n)$, and $t \in \nnrats $ with $t \geq \tau^*_n$, the reach-set of $\rho^*$ can be computed as

\[\terminal{\aut}{\delays}{\rho^*,t} = \{(q', Z') \mid (q', Z'') \in S_n, Z' = Z''^\nearrow \land  \etime = t - \jit\}\]

where $S_0 = \{(q_0, Z_0^{d}) \mid q_0 \in Q_0\}$ and $S_i = \succc_d(S_{i-1}, (\sigma_i, \tau^*_i))$ for $i \in \{1,\ldots, n\}$.

This theorem allows us to implement a monitoring algorithm by computing the reach-sets and intersecting them with the set of nonempty language states.

The observation of events may lead to refinement of the difference between $\time$ and $\etime$ as depicted in Fig. <ref>.

Given $\aut$, $\delays$, $\rho^*$, $t$, and $S_n$ as in Theorem <ref>, we can compute the set of consistent delays by looking at the bounds on $etime - time$:

$\Delta_\delays( L(\aut), \rho^*, t) = \{(\lat, \jit) \in \delays \mid S \models etime - time = \lat\}$.

This information can be used to decorate the $\unknown$ verdict, so that we can report a set of bounds on the latency for which we would provide a $\top$ or $\bot$ verdict.

=5.5; =4; ł=0.3; =̆1.5; =1; =3;

[black!20] (,0) rectangle (,);

[very thick, ->] (0,0) – (0,) node[below right]etime;
[very thick, ->] (0,0) – (,0) node[below left]time;

[ultra thick, black!20!green] (0,ł) – (0,)̆;
(0,)̆ node[right]$u$;
(0,ł) node[right]$l$;

[dashed] (0,)̆ – (,+)̆;
[dashed] (0,ł) – (,+ł);

(2,0.25) node[]$\sigma$ enabled;
[dashed, latex reversed-latex reversed] (,0.5) – (,0.5);

[thick, blue, fill=blue!70!green!20] (, +ł) – (, +ł) – (, +)̆ – (, +)̆ – cycle;

[very thin] (2, 2+)̆ – (1.7, 4.3);
[very thin] (2, 2+ł) – (2.3, 1.4);

(1.5,4.5) node[]$etime - time \leq u$;
(2.5,1.2) node[]$time - etime \leq -l$;

=5.5; =4; ł=0.3; =̆1.5; =1; =3; =3.9; =0.2;

[very thick, ->] (0,0) – (0,) node[below right]etime;
[very thick, ->] (0,0) – (,0) node[below left]time;

[thick, blue, fill=blue!70!green!20] (, +ł) – (, +ł) – (, +)̆ – (, +)̆ – cycle;

[dashed] (0,+) node[left]$\tau$ node[above right=0.5]$etime \in [\tau-\jit, \tau]$ – (, +);
[dashed] (0,-) node[left]$\tau-\jit$ – (, -);
[very thick, red, fill=red!50] (--̆,-) – (,-) – (, +) – (+-,̆ +) – cycle;

[dashed] (--̆,-) – (--̆, 0.8);
[dashed] (,-) – (, 0.8);

[dashed] (--̆,0.5) – (--̆, 0);
[dashed] (,0.5) – (, 0);

[dashed, latex reversed-latex reversed] (--̆,1) – (,1);
(--̆+0.4, 0.7) node[]Event at sys-time;

=5.5; =4; ł=0.3; =̆1.5; =1; =3; =3.9; =0.2;

[very thick, ->] (0,0) – (0,) node[below right]etime;
[very thick, ->] (0,0) – (,0) node[below left]time;

[dashed] (, +ł) – (, +ł) – (, +)̆ – (, +)̆ – cycle;

[dashed] (0,-) node[left]$\tau-\jit$ – (, -);

[thick, black!60!green, fill=green!20] (--̆,-) – (,-) – (,-+-) – (, +)̆ – cycle;

Illustration of a single zone in the $\succc_{d}$ computation (only $\time$-$\etime$ plane depicted). Left: initial zone (in green) is diagonally extrapolated for time passage and then intersected with the guard of an edge. Middle: observing event $\sigma$ at time $\tau$. By restricting $etime$ to $[\tau-\jit, \tau]$, the clock $time$ is restricted to when the event could have occurred at the system. Right: computing the future zone we see that the bound on $time - etime$ is now stricter and thus the bounds for the consistent latencies are refined.

Let us show an example of our algorithm for monitoring under delayed observation.
Consider the property $\varphi = F_{[0,10]}a \land G_{[0,20]}$ from Fig. <ref>. The 's accepting $\lang{\varphi}$ and $\lang{\neg\varphi}$ are shown in Fig. <ref>.
The nonempty language states for $\aut_\varphi$ and $\aut_{\neg\varphi}$ are
$\nonempty{\aut_\varphi} = \{(q_0, \{x \le 10\}), (q_1, \emptyset), (\varphi, \emptyset)\}$ and
$\nonempty{\aut_{\neg\varphi}} = \{(q_0, \emptyset), (q_1, \{x \le 20\}), (\neg\varphi, \emptyset)\}$.
Let us assume the latency is between 0 and 10, and the jitter is bounded by $0.2$.
Now we compute the reach-sets $S_0$ (initial), $S_1$ (after $(a, 17.3)$), and $S_2$ (after $(b, 27.5)$) as

\begin{align*}
S_0 = \{&(q_0, \{x = 0,\ etime \leq 10,\ etime - x \in [0, 10]\})\},\\
S_1 = \{&(q_1, \{x \in [7.1, 10],\ etime \in [17.1, 17.3],\ etime - x \in [7.1, 10]\}),\\ &(\neg\varphi, \{x \in [10, 17.3],\ etime \in [17.1, 17.3],\ etime - x \le 7.3\})\}\text{, and}\\
S_2 = \{&(\varphi, \{x \in ]20, 20.4], etime \in [27.3, 27.5[,\ etime - x \in [7.1, 7.5]\}),\\
& (\neg\varphi, \{x \in [17.3, 27.5],\ etime \in [27.3, 27.5],\ etime - x \in [0, 10]\})\}.
\end{align*}

Note that we omit the clock time and only look at $x$ and $etime$ since $time$ and $x$ always have the same constraints.

All reach-sets intersect with both sets of nonempty language states; thus, the verdict is $\unknown$. However, we can refine this verdict with knowledge about the consistent delays that change after each observation.
The jitter bound is fixed at $0.2$, but the bounds on the latency can be found in the clock constraints on the difference between $etime$ and $x$.
For $\bot$, the latency range remains $[0,10]$ in all reach sets. For $\top$,
the consistent latency range is $[0, 10]$ in $S_0$, $[7.1, 10]$ in $S_1$, and it is $[7.1, 7.5[$ in $S_2$. This means that if the latency is outside $[7.1, 7.5[$, then the verdict is $\bot$.

On the other hand, for the observation $\rho^*=(a, 17.3), (b, 27.1)$ from Example <ref> (and using the same latency and jitter bounds as above), we compute the reach-sets $S_0$, $S_1$, and $S_2'$ where

\[
S_2' = \{(\neg\varphi, \{x \in [16.9, 27.1], etime \in [26.9, 27.1], etime - x \in [0, 10]\})\}
\]

As $S_2'$ has an  empty intersection with $\nonempty{\aut_\varphi}$, the verdict is $\bot$.

§ IMPLEMENTATION

We implemented the methods described in this paper in the tool MoniTAal[<https://github.com/DEIS-Tools/MoniTAal>] written in C++. This includes
the Difference Bounded Matrix data structure to handle clock-zones, parsing property automata modelled in Uppaal,
computing the set of nonempty language states, computing the reach-sets in an online fashion over an observed word based on latency and jitter bounds in $[0, \infty[$, providing verdicts $\top, \bot$ or $\unknown$ and latency bounds consistent with $\top$ and $\bot$.

We demonstrate MoniTAal on a trace generated by the gear controller model from [14]. The trace is generated in Uppaal [8] and the monitored properties are six response properties derived from error locations in the model. We show results with and without delay consisting of a latency in $[0,100]$ jitter bounded by $5$.
The results in Table <ref> show the number of observations, length (in time) of the observed word, the over running time, the maximal response time (the time it takes to process a single observation and return the next verdict), and the maximal number of stored symbolic states.
Under delay we see that the state storage grows linearly with the number of observations, which in turn results in a growing overhead when computing the reach-sets after each observation. The reason for this is the uncertainty of the delay increases the size of the reach-set.
Nevertheless, the maximal response time is in all cases less than 1.2 ms.
In the delay-free case, the memory usage is constant.

Results for simultaneously monitoring six response properties over a trace generated by the gear controller model from [14].

# Observ.     $\tau(\rho)$     2cTime (ms)     2cMax. resp. time ($\mu$s)    2c# Symbolic States

Delay     Delay-free     Delay     Delay-free     Delay     Delay-free

1000     63112       76     42     182     143     39     12

2000     124028      223     84     228     188     57     12

3000     184743      418     116     382     86     78     12

4000     244717      691     154     410     81     109     12

5000     306015      1037     198     571     281     135     12

6000     366814      1463     237     680     163     167     12

7000     438799      1973     278     767     175     192     12

8000     501070      2554     314     986     193     215     12

9000     563296      3212     357     1159     175     238     12

10000     624530     3929     384     1099     109      266     12

§ CONCLUSION

We have introduced a zone-based algorithm realizing optimal (in the sense of being anticipating [7]) online operational monitoring of embedded real-time systems when the communication between the monitor and the system is subject to unknown (up to bounds) delay. This situation is rather typical in practice as observations are mediated by sensors, may involve conversion between analog and digital, or pass communication networks and consequently are indirect in general, leading to delays and inexact time-stamping. Our constructions thus fill a gap in the pre-existing theories for monitoring hard real-time systems, which tend to assume full and exact temporal observability by immediate coupling or, equivalently, perfect synchrony between systems and their monitors.

A notable point of our construction is that it applies a reduction to simple timed automata and is purely zone-based despite the unknown communication delay being a timing parameter. The construction thus not only avoids the complexities of property analysis for parameterized timed automata [4], but also provides an instance of monitoring under uncertainty where the underlying arithmetic constraint systems remain of fixed dimensionality (namely the number of clocks in the property automata plus two for monitoring) despite their history dependence. This is in stark contrast to direct constraint encodings growing linearly over history length as in [11].

[1]
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science
126(2),  183–235 (1994).

[2]
Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality.
Journal of the ACM  43(1) (01 1996)

[3]
Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In:
Kosaraju, S.R., Johnson, D.S., Aggarwal, A. (eds.) Proceedings of the
Twenty-Fifth Annual ACM Symposium on Theory of Computing, May 16-18, 1993,
San Diego, CA, USA. pp. 592–601. ACM (1993).
10.1145/167088.167242, <https://doi.org/10.1145/167088.167242>

[4]
André, É., Lime, D., Roux, O.H.: Reachability and liveness in
parametric timed automata. Log. Methods Comput. Sci.  18(1) (2022).

[5]
Baldor, K., Niu, J.: Monitoring dense-time, continuous-semantics, metric
temporal logic. In: Runtime Verification. pp. 245–259. Springer Berlin
Heidelberg (2013). 10.1007/978-3-642-35632-2_24

[6]
Basin, D., Klaedtke, F., Zălinescu, E.: Algorithms for monitoring
real-time properties. In: RV. pp. 260–275. Springer (2012).

[7]
Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In:
Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006: Foundations of Software
Technology and Theoretical Computer Science. pp. 260–272. Springer, Berlin,
Heidelberg (2006). 10.1007/11944836_25

[8]
Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M.,
Corradini, F. (eds.) Formal Methods for the Design of Real-Time Systems,
International School on Formal Methods for the Design of Computer,
Communication and Software Systems, SFM-RT 2004, Bertinoro, Italy,
September 13-18, 2004, Revised Lectures. LNCS, vol. 3185, pp. 200–236.
Springer (2004). 10.1007/978-3-540-30080-9_7,

[9]
Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In:
Lectures on Concurrency and Petri Nets, Advances in Petri Nets. LNCS,
vol. 3098, pp. 87–124. Springer (2003). 10.1007/978-3-540-27755-2_3

[10]
Brihaye, T., Geeraerts, G., Ho, H.M., Monmege, B.: MightyL: A compositional
translation from MITL to timed automata. In: Computer Aided Verification.
pp. 421–440. Springer (2017). 10.1007/978-3-319-63387-9_21

[11]
Finkbeiner, B., Fränzle, M., Kohn, F., Kröger, P.: A truly robust
signal temporal logic: Monitoring safety properties of interacting
cyber-physical systems under uncertain observation. Algorithms
15(4),  126 (2022). 10.3390/a15040126

[12]
Grosen, T.M., Kauffman, S., Larsen, K.G., Zimmermann, M.: Monitoring timed
properties (revisited). In: Bogomolov, S., Parker, D. (eds.) Formal Modeling
and Analysis of Timed Systems - 20th International Conference, FORMATS
2022, Warsaw, Poland, September 13-15, 2022, Proceedings. LNCS, vol. 13465,
pp. 43–62. Springer (2022). 10.1007/978-3-031-15839-1_3

[13]
Ho, H.M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal
logic. In: Runtime Verification. pp. 178–192. Springer (2014).

[14]
Lindahl, M., Pettersson, P., Yi, W.: Formal Design and Analysis of a Gearbox
Controller. Springer International Journal of Software Tools for Technology
Transfer (STTT)  3(3),  353–368 (2001)

[15]
Sheldon, T.: McGraw-Hill's Encyclopedia of Networking and Telecommunications.
McGraw-Hill Professional (2001)

[16]
Thati, P., Rosu, G.: Monitoring algorithms for metric temporal logic
specifications. In: Havelund, K., Rosu, G. (eds.) Proceedings of the Fourth
Workshop on Runtime Verification, RV@ETAPS 2004, Barcelona, Spain, April 3,
2004. Electronic Notes in Theoretical Computer Science, vol. 113, pp.
145–162. Elsevier (2004). 10.1016/J.ENTCS.2004.01.029

[17]
Ulus, D., Ferrère, T., Asarin, E., Maler, O.: Timed pattern matching. In:
Formal Modeling and Analysis of Timed Systems. pp. 222–236. Springer (2014).

[18]
Ulus, D., Ferrère, T., Asarin, E., Maler, O.: Online timed pattern matching
using derivatives. In: Tools and Algorithms for the Construction and Analysis
of Systems. pp. 736–751. Springer (2016). 10.1007/978-3-662-49674-9_47

[19]
Waga, M., André, É., Hasuo, I.: Model-bounded monitoring of hybrid
systems. ACM Trans. Cyber Phys. Syst.  6(4),  30:1–30:26 (2022).
10.1145/3529095, <https://doi.org/10.1145/3529095>

§ PROOFS OMITTED IN THE MAIN PART

Throughout the appendix, we often need to shift a timed word in the sense that we add or subtract a $d \in\nnreals$ to each time point of $\rho$.
In the latter case, we need to be careful to ensure that the time points in the shifted word are still nonnegative.
For the sake of readability, let us introduce some notation for these operations.
Given a (finite or infinite) timed word $\rho = (\sigma_1, \tau_1),(\sigma_2, \tau_2),\ldots$ and such a $d \in \nnreals$,

* let $\rho+d$ denote the timed word $(\sigma_1, \tau_1+d),(\sigma_2, \tau_2+d),\ldots$, and

* if $d \le \tau_1$, let $\rho-d$ denote the timed word $(\sigma_1, \tau_1-d),(\sigma_2, \tau_2-d),\ldots$. This is well-defined, as we require that $\tau_1$ (and therefore each $\tau_i$) is at least $d$, so we never obtain negative time points in $\rho-d$.

The following properties follow directly from the definition of timed concatenation and will be applied in the proofs below.

Let $\rho = (\sigma_1, \tau_1),\ldots,(\sigma_n, \tau_n) \in \TSigma^*$, let $\mu = (\sigma_1', \tau_1'),(\sigma_2', \tau_2'),\ldots  \in \TSigma^\omega$, and let $t \le \tau(\rho)$.

Let $t' \in \nnreals$ be such that $t -t' \ge \tau(\rho)$. Then

\[
\rho \cdot_t \mu = \rho \cdot_{t-t'} (\mu+t').
\]

Let $0 \le t' \le t$, let $n' \in \{0,1, \ldots, n\}$ be such that $\tau_{n'} \le t' \le \tau_{n'+1}$ (were we use $t_0 = -\infty$ to allow $n'=0$ and $\tau_{n+1} = \infty$ to allow $n' = n$) and define $\rho_1 = (\sigma_1, \tau_1),\ldots,(\sigma_{n'}, \tau_{n'})$ as well as $\rho_2 = (\sigma_{n'+1}, \tau_{n'+1}),\ldots,(\sigma_n, \tau_n)$. Then

\[
\rho \cdot_t \mu = \rho_1 \cdot_{t'} ( (\rho_2-t') \cdot_{t-t'}\mu ).
\]

Let $t' \ge 0$ be such that $\tau(\rho) \le t-t'$, let $n' \ge 1$ be such that $\tau_{n'}' \le t' \le \tau_{n'+1}'$ (this is well-defined due to time-divergence), and define $\rho' = (\sigma_1', \tau_1'),\ldots,(\sigma_{n'}', \tau_{n'}')$ as well as $\mu' = (\sigma_{n'+1}', \tau_{n'+1}'),(\sigma_{n'+2}', \tau_{n'+2}'),\ldots$. Then

\[
\rho \cdot_{t-t'} \mu = (\rho \cdot_{t - t'} \rho') \cdot_t (\mu' - t').
\]

Furthermore, the following properties about consistent words will be useful in the proofs below.

Let $(\rho^*_1,t_1) \sqsubseteq (\rho_2^*, t_2)$, let $\rho_2 = (\sigma_1, \tau_1),\ldots,(\sigma_n,\tau_n) \in \GT_{\lat,\jit}(\rho_2^*, t_2)$, let $n' \in \{0,1,\ldots,n\}$ be such that $\tau_{n'} \le t_1 \le \tau_{n'+1}$ (were we use $t_0 = -\infty$ to allow $n'=0$ and $\tau_{n+1} = \infty$ to allow $n' = n$), and define $\rho_1 = (\sigma_1, \tau_1),\ldots,(\sigma_{n'},\tau_{n'})$. Then $\rho_1 \in \GT_{\lat,\jit}(\rho_1^*, t_1)$.

Let $\rho \in \GT_{\lat,\jit}^\strict(\rho^*,t)$, and let $\rho'$ be a finite timed word with $\tau(\rho') \le t - \max(\tau(\rho), t - (\lat+\jit))$. Then,
$\rho \cdot_{\max(\tau(\rho), t - (\lat+\jit))} \rho' \in \GT_{\lat,\jit}(\rho^*,t)$.

Let $\rho \in \GT_{\lat,\jit}(\rho^*,t)$, let $\rho$ have $m$ letters, and let $\rho'$ be the prefix of $\rho$ with $m$ letters. Then, $\rho' \in \GT_{\lat,\jit}^\strict(\rho^*,t)$.

We need to show that $\rho_1$ is consistent with $\rho_1^*$ at $t_1$ under $\lat$ and $\jit$. The first requirement of the definition of consistency follows from $\tau(\rho_1^*) \le t_1$ and the choice of $n'$ (which implies $\tau(\rho_1) \le t_1$).
The second requirement follows from the fact that $\rho_2$ is consistent with $\rho_2^*$ at $t_2$ under $\lat$ and $\jit$ and the fact that $\rho_1$ is a prefix of $\rho_2$ and $\rho_1^*$ is a prefix of $\rho_2^*$.
Finally, consider the third requirement and assume it is violated, i.e., let $\rho_1^*$ have $m$ letters and assume $\rho_1$ has at least $m+1$ letters such that the time point $\tau_{m+1}$ of the $(m+1)$-st letter of $\rho_1$ satisfies $\tau_{m+1} + \lat +\jit < t_1$. Then, as $\rho_2$ is consistent with $\rho_2^*$ at $t_2$ under $\lat$ and $\jit$, we obtain a contradiction.
Either $\rho_2^*$ has also $m$ letters. In this case, $\tau_{m+1} + \lat +\jit < t_1 \le t_2$ implies that the third requirement of the definition of consistency is violated for $\rho_2$ and $\rho_2^*$.
Otherwise, $\rho_2^*$ has at least $m+1$ letters. In this case $\tau_{m+1} + \lat +\jit < t_1 \le t_2$ implies that the second requirement of the definition of consistency is violated for $i = m+1$.

We have to show that $\rho \cdot_{\max(\tau(\rho), t - (\lat+\jit))} \rho'$ is consistent with $\rho^*$ at $t$ under $\lat$ and $\jit$. This follows directly from the fact that all events in $\rho'$ have time points (in $\rho \cdot_{\max(\tau(\rho), t - (\lat+\jit))} \rho'$) in the interval $[t-(\delta+\jit),t]$ and are therefore covered by the third requirement of the definition of consistency.

We need to show that $\rho'$ is EL-consistent with $\rho^*$ at $t$ under $\lat$ and $\jit$. By definition, $\rho'$ has the same length as $\rho^*$ and the first two requirements of the definition of consistency are satisfied, as $\rho$ is consistent with $\rho^*$ at $t$ under $\lat$ and $\jit$ and $\rho'$ is a prefix of $\rho$. Hence, it is EL-consistent, as the third requirement only refers to ground-truth that have more letters than the observation.

Now we are ready to present the proofs omitted in the main part.

§.§ Proof of Lemma <ref>

Recall that we need to show $\evalfuncd{\delays'}{L}{\rho^*,t}=\top$ implies $\evalfuncd{\delays}{L}{\rho^*,t}=\top$ and that $\evalfuncd{\delays'}{L}{\rho^*,t}=\bot$ implies $\evalfuncd{\delays}{L}{\rho^*,t}=\bot$ for $\delays \subseteq \delays'$.

Note that $\delays \subseteq \delays'$ implies $\GT_\delays(\rho^*,t) \subseteq \GT_{\delays'}(\rho^*,t)$. Thus, the universal quantification over possible ground-truths $\rho$ in the first two cases of the definition of $\evalfuncd{\delays}{L}{\rho^*,t}$ ranges over a subset of the possible ground-truths that are considered for $\evalfuncd{\delays'}{L}{\rho^*,t}$.
Hence, the result follows.

§.§ Proof of Lemma <ref>

Recall that we need to show

* $\Delta_{\delays}(L,\rho^*,t)=\emptyset$ iff $\evalfuncd{\delays}{L}{\rho^*,t}=\bot$, and

* $\Delta_{\delays}(\overline{L},\rho^*,t)=\emptyset$ iff $\evalfuncd{\delays}{L}{\rho^*,t}=\top$.

We have

\begin{align*}
{}&{}  \Delta_{\delays}(L,\rho^*,t)=\emptyset\\
\Leftrightarrow {}&{} \rho\cdot_t\mu \in\overline{L} \text{ for all $(\lat,\jit) \in \delays$, all $\rho \in \GT_{\lat,\jit}(\rho^*,t)$, and all $\mu \in \TSigma^\omega$}\\
\Leftrightarrow {}&{} \rho\cdot_t\mu \in\overline{L} \text{ for all $\rho \in \GT_{\delays}(\rho^*,t)$ and all $\mu \in \TSigma^\omega$}\\
\Leftrightarrow {}&{} \evalfuncd{\delays}{L}{\rho^*,t}=\bot.
\end{align*}

The second claim is obtained by a dual argument (swapping $\bot$ with $\top$ and $L$ with $\overline{L}$).

§.§ Proof of Lemma <ref>

Recall that we need to show $\Delta(L,\rho_1^*,t_1)\supseteq\Delta(L,\rho_2^*,t_2) $ for all $(\rho_1^*,t_1)\sqsubseteq (\rho_2^*,t_2)$.

Let $(\lat,\jit) \in \Delta(L,\rho_2^*,t_2)$, i.e., there exists $\rho_2 \in \GT_{\lat,\jit}(\rho_2^*,t_2)$ and a $\mu_2 \in \TSigma^\omega$ such that $\rho_2\cdot_{t_2}\mu_2 \in L$.

Let $\rho_2 = (\sigma_1, \tau_1), \ldots,(\sigma_n, \tau_n)$ and let $n'$ be maximal with $\tau_{n'} \le t_1$.
Then, Lemma <ref>.<ref> yields

\[
\rho_1 = (\sigma_1, \tau_1), \ldots,(\sigma_{n'}, \tau_{n'}) \in \GT_{\lat,\jit}(\rho_1^*,t_1)
\]

and an application of Remark <ref>.<ref> yields

\[
\rho_1 \cdot_{t_1} \Big(\big[ ( (\sigma_{n'+1}, \tau_{n'+1}), \ldots,(\sigma_n, \tau_n ))  - t_1 \big] \cdot_{t_2-t_1} \mu\Big)  = \rho_2\cdot_{t_2}\mu_2 \in L .
\]

This implies $(\lat,\jit) \in \Delta(L,\rho_1^*,t_1)$.

§.§ Proof of Lemma <ref>

Recall that we need to show

* $\Delta_\delays(L,\rho^*, t) \subsetneq \delays \cap \{(\lat, \jit) \mid \lat \le \tau^*_1\} $ implies there is no $ \rho^*_1\in\TSigma^*$ such that $ \evalfuncd{\delays}{L}{\rho^* \cdot_t \rho^*_1, t'} = \top $ for any $ t' \ge t+\tau(\rho^*_1)$, and

* $\Delta_\delays(\overline{L},\rho^*, t) \subsetneq \delays \cap \{(\lat, \jit) \mid \lat \le \tau^*_1\} $ implies there is no $ \rho^*_1\in\TSigma^*$ such that $ \evalfuncd{\delays}{L}{\rho^* \cdot_t \rho^*_1, t'} = \bot  $ for any $ t' \ge t+\tau(\rho^*_1)$.

for all $t \ge \tau(\rho^*)$.

Let  $\Delta_\delays(L,\rho^*, t) \subsetneq \delays \cap \{(\lat, \jit) \mid \lat \le \tau^*_1\} $, i.e., there is a $(\lat,\jit)\in\delays$ with $\lat \le \tau^*_1$ and
$(\lat,\jit)\notin \Delta_\delays(L,\rho^*, t)$.
Thus, by definition, for all $\rho \in \GT_{\lat,\jit}(\rho^*,t)$ and all $\mu \in \TSigma^\omega$ we have $\rho\cdot_t\mu \in \overline{L}$ ($\dagger$).

Now, let $\rho^*_1 \in \TSigma^*$ and assume, towards a contradiction, we have $\evalfuncd{\delays}{L}{\rho^* \cdot_t \rho_1^*, t'} = \top $ for $t' \ge t+\tau(\rho^*_1)$, i.e., for all $\rho' \in \GT_{\delays}(\rho^* \cdot_t \rho_1^*,t')$ and all $\mu \in \TSigma^\omega$ we have $\rho' \cdot_{t'}\mu \in L$ ($\dagger\dagger$).
As  $\GT_{\lat,\jit}(\rho^* \cdot_t \rho_1^*,t')$ is nonempty, let us fix one such $\rho' \in \GT_{\lat,\jit}(\rho^* \cdot_t \rho_1^*,t')$. Also, let us fix a $\mu \in \TSigma^\omega$.

Note that we have $(\rho^*, t) \sqsubseteq (\rho^* \cdot_t \rho_1^*, t')$.
So, let $\rho' = (\sigma_1 ,\tau_1), \ldots ,(\sigma_n,\tau_n)$ and let $n'$ be maximal with $\tau_{n'} \le t$.
Then, Lemma <ref>.<ref> yields

\[
\rho_1' =  (\sigma_1 ,\tau_1), \ldots ,(\sigma_{n'},\tau_{n'}) \in \GT_{\lat,\jit}(\rho^*,t)
\]

and application of Remark <ref>.<ref> yields

\[
\rho' \cdot_{t'}\mu = \rho_1' \cdot_t \underbrace{\Big( \big[ ((\sigma_{n'+1}, \tau_{n'+1}), \ldots,(\sigma_n, \tau_n))- t\big]  \cdot_{t'-t} \mu \Big)}_{=\mu'} .
\]

This yields the desired contradiction, as $\rho' \cdot_{t}\mu $ is in $L$ (see $\dagger\dagger$) while $\rho_1' \cdot_t\mu'$ is not in $L$ (see $\dagger$).

The second claim is proven by a dual argument (swapping $L$ with $\overline{L}$ and $\top$ with $\bot$).

§.§ Proof of Lemma <ref>

Recall that we need to show $\evalfuncdstrict{\delays}{L}{\rho^*,t} = \evalfuncd{\delays}{L}{\rho^*,t}$.

Let $\evalfuncd{\delays}{L}{\rho^*,t} = \top$.
We show $\evalfuncdstrict{\delays}{L}{\rho^*,t} = \top$ by proving that we have $\decorate{\rho} \cdot_{\max(\tau(\decorate{\rho}), t - (\lat + \jit))} \decorate{\mu} \in L$ for all $\decorate{\rho} \in \GT^\strict_{\lat,\jit}(\rho^*,t)$ for some $(\lat,\jit)\in \delays$ and all $\decorate{\mu} = (\sigma_1, \tau_1),(\sigma_2, \tau_2), \ldots \in \TSigma^\omega$.

First, consider the case where $\tau(\decorate{\rho}) < t - (\lat +\jit)$.
Let $n$ be maximal with $\tau_n \le \lat+\jit$ (this is well-defined due to time-divergence), let $\decorate{\rho_1} = (\sigma_1, \tau_1), \ldots, (\sigma_n, \tau_n)$ and $\decorate{\mu_2} = ((\sigma_{n+1}, \tau_{n+1}),(\sigma_{n+2}, \tau_{n+2}), \ldots)- (\lat + \jit)$.
Note that $\decorate{\mu_2}$ is well-defined as $\tau_{n+1}$ is, by the choice of $n$, greater than $\lat + \jit$.
Then, Lemma <ref>.<ref> yields $\decorate{\rho} \cdot_{t - (\lat + \jit)} \decorate{\rho_1}$ is in $\GT_{\lat,\jit}(\rho^*,t)$ and Remark <ref>.<ref> yields

\[
\decorate{\rho} \cdot_{\max(\tau(\decorate{\rho}), t - (\lat + \jit))} \decorate{\mu} = \decorate{\rho} \cdot_{ t - (\lat + \jit)} \decorate{\mu} = (\decorate{\rho} \cdot_{t - (\lat + \jit)} \decorate{\rho_1} ) \cdot_t \decorate{\mu_2}.
\]

Therefore, $\decorate{\rho} \cdot_{\max(\tau(\decorate{\rho}), t - (\lat + \jit))} \decorate{\mu}$ is the concatenation of the possible ground-truth $(\decorate{\rho} \cdot_{t - (\lat + \jit)} \decorate{\rho_1} )$ of $\rho^*$ and the  suffix $\decorate{\mu_2}$. As we have $\rho \cdot_t \mu \in L $ for all $\rho \in \GT_{\delays}(\rho^*,t)$ and all $ \mu \in \TSigma^{\omega}$ (due to $\evalfuncd{\delays}{L}{\rho^*,t} = \top$), we conclude $\decorate{\rho} \cdot_{\max(\tau(\decorate{\rho}), t - (\lat + \jit))} \decorate{\mu} \in L$ as required.

Now, consider the case where $\tau(\decorate{\rho}) \ge t - (\lat +\jit)$.
Note that we have $t - \tau(\decorate{\rho}) \ge 0$ due to $\decorate{\rho} \in \GT^\strict_{\lat,\jit}(\rho^*,t)$.
Hence, let $n$ be maximal with $\tau_n \le t - \tau(\rho')$ (again, this is well-defined due to time-divergence), let $\decorate{\rho_1} = (\sigma_1, \tau_1) \cdots (\sigma_n, \tau_n)$ and $\decorate{\mu_2} = ((\sigma_{n+1}, \tau_{n+1})(\sigma_{n+2}, \tau_{n+2}) \cdots)- (t - \tau(\decorate{\rho}))$.
Then, Lemma <ref>.<ref> yields $\decorate{\rho} \cdot_{\tau(\decorate{\rho})} \decorate{\rho_1}$ is in $\GT_{\lat,\jit}(\rho^*,t)$ and Remark <ref>.<ref> yields

\[
\decorate{\rho} \cdot_{\max(\tau(\decorate{\rho}), t - (\lat + \jit))} \decorate{\mu} = \decorate{\rho} \cdot_{\tau(\decorate{\rho})} \decorate{\mu} = (\decorate{\rho} \cdot_{\tau(\decorate{\rho})} \decorate{\rho_1} ) \cdot_t \decorate{\mu_2}.
\]

As $\decorate{\rho} \cdot_{\max(\tau(\decorate{\rho}), t - (\lat + \jit))} \decorate{\mu} $ is the concatenation of a possible ground-truth of $\rho^*$ and an arbitrary suffix, it is again, as required, in $L$.

Using a dual argument (i.e., swapping $\top$ with $\bot$ and $L$ with $\overline{L}$), we can show that $\evalfuncd{\delays}{L}{\rho^*,t} = \bot$ implies $\evalfuncdstrict{\delays}{L}{\rho^*,t} = \bot$.

Now, we show that $\evalfuncdstrict{\delays}{L}{\rho^*,t} = \top$ implies $\evalfuncd{\delays}{L}{\rho^*,t} = \top$. A dual argument again shows that $\evalfuncdstrict{\delays}{L}{\rho^*,t} = \bot$ implies $\evalfuncd{\delays}{L}{\rho^*,t} = \bot$.
This will then complete our proof, as both functions only have three elements in their codomain and we have shown that two of them have the same preimage w.r.t. both functions.

So, let $\evalfuncdstrict{\delays}{L}{\rho^*,t} = \top$.
We show $\evalfuncd{\delays}{L}{\rho^*,t} = \top$ by showing $\rho \cdot_t \mu \in L$ for all $\rho = (\sigma_1,\tau_1),\ldots,(\sigma_n, \tau_n) \in \GT_{\delays}(\rho^*,t)$ and all $ \mu = (\sigma_1', \tau_1'),(\sigma_2',\tau_2'),\ldots \in \TSigma^{\omega}$.
By definition, there is a $(\lat,\jit) \in\delays$ such that $\rho \in \GT_{\lat,\jit}(\rho^*,t)$.

Let $\rho^*$ have $m$ letters.
If $m = n$, then we also have $\rho \in \GT^\strict_{\delays}(\rho^*,t)$.
We consider two cases: If $\tau(\rho) < t-(\lat+\jit)$, then an application of Remark <ref>.<ref> yields

\[
\rho \cdot_t \mu
=\rho \cdot_{t - (\lat + \jit)} (\mu + (\lat+\jit))=\rho \cdot_{\max(\tau({\rho}), t - (\lat + \jit))} (\mu + (\lat+\jit)),
\]

and if $\tau(\rho) \ge t - (\lat+\jit)$, then an application of Remark <ref>.<ref> yields

\[
\rho \cdot_t \mu = \rho \cdot_{\tau(\rho)} (\mu+ (t - \tau(\rho)))= \rho \cdot_{\max(\tau({\rho}), t - (\lat + \jit))} (\mu+ (t - \tau(\rho))),
\]

where $t - \tau(\rho)$ is nonnegative by definition of consistency.
Hence, in both cases,  $\rho\cdot_t \mu$ is the concatenation of a possible EL ground-truth of $\rho^*$ and an arbitrary suffix.
Due to $\evalfuncdstrict{\delays}{L}{\rho^*,t} = \top$, all concatenations $\rho \cdot_{\max(\tau(\rho), t - (\lat + \jit))} \mu$ for $(\lat,\jit) \in \delays$, $\rho \in \GT^\strict_{\lat,\jit}(\rho^*,t)$, and $ \mu \in \TSigma^{\omega}$ are in $L$, which yields $\rho\cdot_t \mu \in L$.

It remains to consider the case where $n > m$, which we again split into two subcases. But first let us define $\rho_1=(\sigma_1,\tau_1)\cdots(\sigma_m, \tau_m)$ as well as $\rho_2 = (\sigma_{m+1},\tau_{m+1}) \cdots (\sigma_n, \tau_n)$. Lemma <ref>.<ref> yields $\rho_1 \in \GT^\strict_{\delays}(\rho^*,t)$.

First, consider the subcase where $\tau(\rho_1) < t - (\lat +\jit)$. By definition of consistency, $n > m$ implies $\tau_{m+1} +\lat +\jit \ge t$, and thus $\tau_{m+1} \ge t - (\lat + \jit)$ ($\dagger$).
Hence, an application of Remark <ref>.<ref> yields

\begin{align*}
\rho\cdot_t \mu = {}&{}
\rho_1 \cdot_{t - (\lat +\jit)} [ (\rho_2- (t - (\lat+\jit))) \cdot_{\lat+\jit} \mu ]\\
={}&{} \rho_1 \cdot_{\max(\tau(\rho_1), t - (\lat + \jit))} [ (\rho_2- (t - (\lat+\jit))) \cdot_{\lat+\jit} \mu ]
\end{align*}

Note that the first time point of $\rho_2$, $\tau_{m+1} $, is at least $(t - (\lat+\jit))$ as required, as $\tau_{m+1} \ge t - (\lat + \jit)$ (see $\dagger$).
Hence, $\rho\cdot_t \mu$ is the concatenation of a possible EL ground-truth of $\rho^*$ and an arbitrary suffix and therefore in $L$.

Finally, consider the subcase where $\tau(\rho_1) \ge t - (\lat +\jit)$.
Then, an application of Remark <ref>.<ref> yields

\begin{align*}
\rho\cdot_t \mu ={}&{}
\rho_1 \cdot_{\tau(\rho_1)} [(\rho_2- \tau(\rho_1)) \cdot_{t - \tau(\rho_1)} \mu ]\\
={}&{} \rho_1 \cdot_{\max(\tau(\rho_1), t - (\lat + \jit))} [(\rho_2- \tau(\rho_1)) \cdot_{t - \tau(\rho_1)} \mu ].
\end{align*}

Again, this is well-defined as we have $\tau_{m+1} \ge \tau(\rho_1)$ (as $\tau_{m+1}$ is the next time instant after $\tau_{m}=\tau(\rho_1)$ in $\rho$) and as  $t \ge \tau(\rho_1)$ by the definition of consistency.
Hence, $\rho\cdot_t \mu$ is again the concatenation of a possible EL ground-truth of $\rho^*$ and an arbitrary suffix and therefore in $L$.

§.§ Proof of Theorem <ref>

Recall that we need to show $\monitordelays{\aut,\compautomaton}{\rho^*,t} = \evalfuncdstrict{\delays}{\lang{\aut}}{\rho^*,t}$.

We will show that $\terminal{\aut'}{\delays}{\rho^*,t} \cap \nonempty{\aut'} $ is nonempty iff there exists a $\rho \in \GT^\strict_{\lat,\jit}(\rho^*,t)$ and a $\mu \in \TSigma^\omega$ with $\rho \cdot_{\max(\tau(\rho),(t - (\lat +\jit)))}\mu \in \lang{\aut'}$ for any  $\aut'$.
Then we obtain

* $\monitordelays{\aut,\compautomaton}{\rho^*,t} = \top$ iff $\evalfuncdstrict{\delays}{\lang{\aut}}{\rho^*,t} = \top$ by instantiating the equivalence for $\aut' = \compautomaton$, and

* $\monitordelays{\aut,\compautomaton}{\rho^*,t} = \bot$ iff $\evalfuncdstrict{\delays}{\lang{\aut}}{\rho^*,t} = \bot$ by instantiating the equivalence for $\aut' = \aut$.

This completes the proof, as both functions only have three elements in their codomain and we have shown that two of them have the same preimage  w.r.t. both functions.

So, let $\terminal{\aut'}{\delays}{\rho^*,t} \cap \nonempty{\aut'} \neq\emptyset$. Then, by definition, there is a state $(q,v')$ of $\aut'$ such that

* $(q_0, v_0) \xrightarrow{\rho}_{\aut'} (q, v)$ for some initial state $(q_0, v_0)$ of $\aut'$, some $\rho \in \GT^\strict_{\lat,\jit}(\rho^*,t)$  for some $(\lat,\jit)\in\delays$, and $v' = v + \max(0,(t - (\tau(\rho) + \lat +\jit)))$, and

* and there is an accepting infinite run of $\aut'$ starting in $(q,v')$ that processes some $\mu \in \TSigma^\omega$.

These two runs can be combined into an accepting run of $\aut'$ that starts in $(q_0, v_0)$ and processes

\[\rho \cdot_{\tau(\rho) + \max(0,(t - (\tau(\rho) + \lat +\jit)))} \mu = \rho \cdot_{\max(\tau(\rho),(t - (\lat +\jit)))} \mu,\]

which implies that it is in $\lang{\aut'}$ as required.

Conversely, let there be a $\rho \in  \GT^\strict_{\lat,\jit}(\rho^*,t)$ and a $\mu \in \TSigma^\omega$ with

\[\mu \cdot_{\max(\tau(\rho),(t - (\lat +\jit)))} \mu \in \lang{\aut'}.\]

Then, there exists an accepting run of $\aut'$ starting in some initial state $(q_0, v_0)$ that processes $\rho \cdot_{\max(\tau(\rho),(t - (\lat +\jit)))} \mu$.
This run can be split into

* $(q_0, v_0) \xrightarrow{\rho}_{\aut'} (q, v)$ for some state $(q,v)$ of $\aut'$ and

* an accepting infinite run of $\aut'$ starting in $(q,v')$ that processes $\mu$, where

\[v'=  v + \max(0,(t - (\tau(\rho) + \lat +\jit))) .\]

Hence, $(q, v') \in \terminal{\aut'}{\delays}{\rho^*,t} \cap \nonempty{\aut'}$, which is therefore, as required, nonempty.

§.§ Proof of Theorem <ref>

Below we give a sketch of a proof. Let $\rho^*=(\sigma^*_1,\tau^*_1),\ldots,(\sigma^*_n,\tau^*_n)$ be an observed timed word. We want to show that

\begin{equation}
\label{reach-alg}
\terminal{\aut}{\delays}{\rho^*,t} = \{(q', Z') \mid (q', Z'') \in S_n, Z' = Z''^\nearrow \land  \etime = t - \jit\}
\end{equation}

where $\terminal{\aut}{\delays}{\rho^*,t}$ is defined by

\begin{align*}
\terminal{\aut}{\delays}{\rho^*,t} = \{ &(q, v + \max(0,(t - (\tau(\rho) + \lat +\jit)))) \mid (q_0, v_0) \xrightarrow{\rho}_\aut (q, v) \text{ where }\\
& (q_0, v_0) \text{ with } q_0 \in Q_0 \text{, } v_0(x)=0 \text{ for all $c \in C$, and }  \\
&\rho \in \GT^\strict_{\lat,\jit}(\rho^*,t) \text{ for some } (\lat,\jit)\in\delays\}.
\end{align*}

in the setting where
$\delays = \{(\lat, \jit) \mid \lat \in [l, u]\}$ for given $l, u, \jit \in \nnrats$.
Also, recall that we have defined $S_0 = \{(q_0, Z_0^{d}) \mid q_0 \in Q_0\}$ and $S_i = \succc_d(S_{i-1}, (\sigma_i, \tau^*_i))$ for $i \in \{1,\ldots, n\}$.

Given the form of $\delays$ we can rewrite the definition of the reach-set to

\begin{align*}
\terminal{\aut}{\delays}{\rho^*,t} = \{ &(q, v + \max(0,(t - (\tau(\rho) + \lat +\jit)))) \mid (q_0, v_0) \xrightarrow{\rho}_\aut (q, v) \text{ where }\\
& (q_0, v_0) \text{ with } q_0 \in Q_0 \text{, } v_0(x)=0 \text{ for all $c \in C$, and }  \\
&\rho \in \GT^\strict_{\lat,\jit}(\rho^*,t) \text{ for some }  \delta\in[l,u]\}.
\end{align*}

Now, extending the transition relation $\xrightarrow{\rho}_\aut$ to clock valuations over the extended set of clocks $C\cup\{time, etime\}$, we may further reformulate the reach-set as follows:

\begin{align*}
\terminal{\aut}{\delays}{\rho^*,t} = \{ &(q_n, v^* + \max(0,(t - (v^*_n(etime)  +\jit)))) \mid (q_0, v^*_0) \xrightarrow{\rho}_\aut (q_n, v^*_n) \text{ where }\\
& (q_0, v^*_0) \text{ with } q_0 \in Q_0 \text{, } v^*_0(x)=0 \text{ for all $c \in C$, and }  \\
& v^*_0(etime)-v^*_0(time)\in [l,u] \text{ and } \\
& v^*_i(etime)\leq \tau^*_i \land v^*_i(etime)\geq \tau^*_i-\varepsilon \land \sigma_i=\sigma^*_i \text{ for } i\in\{0,\ldots,n\} \}.
\end{align*}

A key observation for the correctness of the above reformulation,  is that the extended clocks $etime$ and $time$ are not modified by the TBA $\aut$.  That is  $v^*_i(etime)-v^*_i(time)=v^*_0(etime)-v^*_0(time)\in [l,u]$ for all $i=\{0,\ldots,n\}$.

Now let $\terminal{\aut}{\delays,j}{\rho^*,t}$ for $j\in\{0,\ldots,n\}$ be defined as follows:

\begin{align*}
\terminal{\aut}{\delays,j}{\rho^*,t} = \{ &(q_j, v^*_j) \mid (q_0, v^*_0) \xrightarrow{\rho}_\aut (q_j, v^*_j) \text{ where }\\
& (q_0, v^*_0) \text{ with } q_0 \in Q_0 \text{, } v^*_0(x)=0 \text{ for all $c \in C$, and }  \\
& v^*_0(etime)-v^*_0(time)\in [l,u] \text{ and } \\
& v^*_i(etime)\leq \tau^*_i \land v^*_i(etime)\geq \tau^*_i-\varepsilon \land \sigma_i=\sigma^*_i \text{ for } i\in\{0,\ldots,j\} \}.
\end{align*}

Then clearly $\terminal{\aut}{\delays,0}{\rho^*,t}=\{(q_0, Z_0^{d}) \mid q_0 \in Q_0\}=S_0$ and
$\terminal{\aut}{\delays,j}{\rho^*,t} = \succc_d(\terminal{\aut}{\delays,j-1}{\rho^*,t}, (\sigma_i, \tau_i))$ for $j \in \{1,\ldots, n\}$, using standard arguments for the correcntess of symbolic exploration of timed automata, e.g. [9]. Finally, as $(t - (v^*_n(etime)  +\jit)))=((t-\jit)- v^*_n(etime))$ it follows that $\terminal{\aut}{\delays}{\rho^*,t}= \terminal{\aut}{\delays,n}{\rho^*,t}^\nearrow \land  \etime = t - \jit$.

§ MORE DETAILS ON THE IMPLEMENTATION

MoniTAal requires, as input, two automata accepting the complement language of the other, a series of observations, and optionally bounds on latency and jitter. MoniTAal can be run as a binary where the automata are parsed from a UPPAAL xml file while the observations are parsed as as text from a file or standard input. MoniTAal can also be used as a C++ library.

In Listing <ref> we give a short demonstration going through Example <ref> using MoniTAal.
In the output we see that the consistent latency for the $\top$ verdict ([style=console, basicstyle=]POSITIVE) verdict tightens to $[71, 100]$ and then $[71,75[$ while the final verdict is $\unknown$ ([style=console, basicstyle=]INCONCLUSIVE). Note that we multiply all values (in observations and automata) by 10 in order to use integer, rather than rational, time points.

[style=console, label=lst:example, caption=Demonstration of MoniTAal over Example <ref>.]
$ ./MoniTAal-bin -p positive delay.xml -n negative delay.xml -v --latencyl 0 --latencyu 10 --jitter 2
Input: @[173, 173] a

Verdict: INCONCLUSIVE
Consistent latencies: {[71,100]}
Jitter bound: 2
Consistent latencies: {[0,100]}
Jitter bound: 2

Input: @[271, 271] b

Verdict: INCONCLUSIVE
Consistent latencies: {[71,75)}
Jitter bound: 2
Consistent latencies: {[0,100]}
Jitter bound: 2
\end{lstlisting}

\end{document}