Time for Timed Monitorability

This work makes monitoring of real-time systems more useful by examining the monitorability problem for real-time properties and by introducing qualitative refinements of the verdict ?. We consider real-time properties expressed by Timed Automata (TA) over infinite words [3]. Nondeterministic Timed Büchi Automata (TBA) are used for model checking tools like Uppaal [25] and for monitoring temporal logics [23, 20, 14] and are strictly more expressive than deterministic Timed Muller Automata (DTMA). We prove that strong and weak monitorability are undecidable for nondeterministic TBA, but decidable for DTMA. Thus, one can algorithmically determine that it is futile to monitor properties like ${\phi }_3$, thereby increasing the applicability of monitoring of real-time systems.

Furthermore, we introduce monitorability with step-bounded horizons that strengthens monitorability by limiting the number of events in a timed-word before a conclusive verdict must be reached. A step-bounded horizon allows one to determine for a given property and $n\in \mathbb{N}$, if a conclusive verdict is possible within $n$ steps, enabling corrective actions earlier. Again, we show that monitorability with step-bounded horizons is undecidable for nondeterministic TBA, but decidable for DTMA.

Finally, we refine monitoring of real-time properties with time-horizon verdicts. Here, the verdict ? is enhanced with information about the minimum time until a conclusive verdict may be reached. Intuitively, before this time is reached, the monitor will only yield the inconclusive verdict ?, i.e., no information can be gained from querying the monitor before. This notion was introduced by Grosen et al. [23] as “time-predictive” monitoring. Here, we formally prove that time-horizon queries can be computed effectively for DTMA.

Thus, our results highlight the importance of properties being given by deterministic timed automata when checking monitorability. This is in contrast to monitoring itself, where it suffices to have nondeterministic automata for the property and its negation [23], which is, e.g., the case when specifying properties in Metric Interval Temporal Logic [4]. Finally, we show that it is necessary to have automata for the property and the complement, as the monitoring function is otherwise not effectively computable.

A timed Büchi automaton (TBA) is a tuple $𝒜=(Q,Q_0,\mathrm{\Sigma },𝒳,\mathrm{\Delta },F)$ where $Q$ is a finite set of locations, $Q_0\subseteq Q$ is the set of initial locations, $\mathrm{\Sigma }$ is an alphabet, $𝒳$ is a finite set of clocks, $F\subseteq Q$ is a set of accepting locations, and $\mathrm{\Delta }\subseteq Q\times Q\times \mathrm{\Sigma }\times 2^{𝒳}\times G(𝒳)$ is a set of transitions, where $G(𝒳)$ is the set of clock constraints over $𝒳$. A transition $(q,q^{\prime },\alpha ,\lambda ,g)\in \mathrm{\Delta }$ is an edge from $q$ to $q^{\prime }$ with label $\alpha \in \mathrm{\Sigma }$, where $\lambda \in 2^{𝒳}$ is a set of clocks to be reset and $g\in G(𝒳)$ is a clock constraint. A clock constraint is a finite conjunction of atomic constraints of the form $x\sim n$ where $x\in 𝒳$, $n\in \mathbb{N}$, and . A state of $𝒜$ is a pair $(q,v)$ where $q\in Q$ and $v:𝒳\to {ℝ}_{\ge 0}$ is a clock valuation.

A run of $𝒜$ from a state $(q_0,v_0)$ over an infinite word $(\sigma ,\tau )\in T{\mathrm{\Sigma }}^{\omega }$ is a sequence of steps of the form

where for every $i\ge 1$, there is a transition $(q_{i-1},q_i,{\sigma }_i,{\lambda }_i,g_i)\in \mathrm{\Delta }$ 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$ is satisfied by $v_{i-1}+{\tau }_i-{\tau }_{i-1}$ (where we use ${\tau }_0=0$). For a run r, $\text{inf}(r)\subseteq Q$ denotes the set of locations visited infinitely often in $r$. A run $r$ is (Büchi) accepting if $\text{inf}(r)\cap F\ne \mathrm{\varnothing }$.

A timed Muller automaton (TMA) $𝒜=(Q,Q_0,\mathrm{\Sigma },𝒳,\mathrm{\Delta },ℱ)$ is like a TBA, but the set $F$ of accepting locations is replaced by a set $ℱ\subseteq 2^Q$ of sets of locations. A run $r$ of $𝒜$ is (Muller) accepting if $\text{inf}(r)\in ℱ$.

The language $L(𝒜)$ of a timed (Büchi or Muller) automaton is the set of words $\rho \in T{\mathrm{\Sigma }}^{\omega }$ such that $𝒜$ has an accepting run over $\rho$.

An automaton is deterministic if the set of initial locations is a singleton and if all edges from the same location and with the same label must have disjoint clock constraints. We use the abbreviations DTBA and DTMA to refer to the two deterministic automaton models.

We use Metric Interval Temporal Logic (MITL) to formally express properties to be monitored. The syntax of MITL formulas over a finite alphabet $\mathrm{\Sigma }$ is defined as

where $p\in \mathrm{\Sigma }$ and $I$ ranges over non-singular intervals over ${ℝ}_{\ge 0}$ with endpoints in $\mathbb{N}\cup \{\mathrm{\infty }\}$. Note that we often write $\sim n$ for $I=\{d\in {ℝ}_{\ge 0}\mid d\sim n\}$ where , and $n\in \mathbb{N}$. We also define the standard syntactic sugar $\text{true}=p\vee \neg p$, $\text{false}=\neg \text{true}$, $\phi \wedge \psi =\neg (\neg \phi \vee \neg \psi )$, $\phi \to \psi =\neg \phi \vee \psi$, $F_I\phi =\text{true}{U}_I\phi$, and $G_I\phi =\neg F_I\neg \phi$.

The semantics of MITL is defined over infinite timed words. Given such a timed word $\rho =({\sigma }_1,{\tau }_1)({\sigma }_2,{\tau }_2)\mathrm{\cdots }\in T{\mathrm{\Sigma }}^{\omega }$, a position $i\ge 1$, and an MITL formula $\phi$, we inductively define the satisfaction relation $\rho ,i\vDash \phi$ as follows:

• $\mathrm{■}$

  $\rho ,i\vDash p$ if and only if $p={\sigma }_i$.

• $\mathrm{■}$

  $\rho ,i\vDash \neg \phi$ if and only if $\rho ,i\vDash ̸\phi$.

• $\mathrm{■}$

  $\rho ,i\vDash \phi \vee \psi$ if $\rho ,i\vDash \phi$ or $\rho ,i\vDash \psi$.

• $\mathrm{■}$

  $\rho ,i\vDash X_I\phi$ if and only if $\rho ,(i+1)\vDash \phi$ and ${\tau }_{i+1}-{\tau }_i\in I$.

• $\mathrm{■}$

  $\rho ,i\vDash \phi U_I\psi$ if and only if there exists $k\ge i$ s.t. $\rho ,k\vDash \psi$, ${\tau }_k-{\tau }_i\in I$, and $\rho ,j\vDash \phi$ for all .

We write $\rho \vDash \phi$ whenever $\rho ,1\vDash \phi$, and say that $\rho$ satisfies $\phi$. The language $\text{L}(\phi )$ of an MITL formula $\phi$ is the set of all infinite timed words that satisfy $\phi$.

The monitoring problem asks to make verdicts about the satisfaction or violation of properties (over infinite timed words) after having observed only a finite prefix. Here, we follow the classical approach of considering the possible extensions of a finite observations.

We continue with giving some intuition for the three-valued monitoring approach. Here, one is given an observation and aims to determine whether a property $\phi$ (of infinite timed words) is already satisfied, already violated, or neither.

• $\mathrm{■}$

  If all possible extensions of the observation satisfy $\phi$, then we give the corresponding verdict $\top$ signifying that the observation conclusively witnesses satisfaction of $\phi$.

• $\mathrm{■}$

  If all possible extensions of the observation violate $\phi$, then we give the corresponding verdict $\perp$ signifying that the observation conclusively witnesses violation of $\phi$.

• $\mathrm{■}$

  Otherwise, i.e., if there is an extension of the observation that satisfies $\phi$ and there is a extension of the observation that violates $\phi$, then we give the inconclusive verdict ?.

Let us formalize this intuition.

Recall that TBA are not closed under complement [3], so this result is not applicable to all properties accepted by TBA. However, for the important special case of properties $\phi$ specified in MITL, $V_{\phi }$ is effectively computable, as MITL properties are closed under complementation (as the logic allows for negations) and MITL formulas can be translated into equivalent TBA (see Proposition 3). Similarly, when $\phi$ is given by a DTMA, then $V_{\phi }$ is effectively computable, as DTMA are closed under complementation and can be turned into equivalent TBA [3].

However, it was previously open whether $V_{\phi }$ was computable if $\phi$ was given by a non-deterministic automaton, but we did not have access to an automaton for the complement $T{\mathrm{\Sigma }}^{\omega }\setminus \phi$. In Section 3, we answer the question negatively.

Not every property is amenable to monitoring, e.g., for $\phi =G_{\ge 0}{F}_{\ge 0}a$, we have $V_{\phi }(\rho ,t)=\text{?}$ for every observation $(\rho ,t)$. The reason is that every $\rho$ can be extended to satisfy $\phi$ and can be extended to violate $\phi$. In the untimed setting, much effort has been put into characterizing the monitorable properties, i.e., those for which monitoring can generate some information. Here, we consider monitorability in the timed setting.

Let us continue by collecting some simple consequences of Definition 9.

In the following we study the decidability of monitorability, i.e., we consider the following decision problems where properties are given by timed automata:

1. 1.

   Given a property $\phi$, is $\phi$ strongly monitorable?

2. 2.

   Given a property $\phi$, is $\phi$ weakly monitorable?

3. 3.

   Given a property $\phi$ and an observation $(\rho ,t)$, is $\phi$ strongly $(\rho ,t)$-monitorable?

4. 4.

   Given a property $\phi$ and an observation $(\rho ,t)$, is $\phi$ weakly $(\rho ,t)$-monitorable?

By definition, if Problem 3 is decidable for a class of properties, then Problem 1 is also decidable for the same class of properties. Hence, if Problem 1 is undecidable for a class of properties, then Problem 3 is also undecidable for the same class of properties. A similar relation holds between Problem 2 and Problem 4.

For every property $\phi \subseteq T{\mathrm{\Sigma }}^{\omega }$, we have $V_{\phi }(\epsilon ,0)=\top$ if and only if $\phi =T{\mathrm{\Sigma }}^{\omega }$. Hence, universality of a TBA $𝒜$ reduces to checking whether $V_{L(𝒜)}(\epsilon ,0)=\top$. As universality for timed automata is undecidable [5], the monitoring function cannot be computable. $◀$

Note that the specification automaton $𝒜$ is part of the input in the problem considered in Theorem 13. We leave it open whether $V_{L(𝒜)}$ is computable for every fixed $𝒜$, i.e., in the setting where only the observation is the input.

Next, we turn our attention to deciding monitorability for TBA.

Strong monitorability for untimed non-deterministic Büchi Automata is PSpace-complete [17], which can be shown by a reduction from the universality problem [18]. Analogously, we reduce the (undecidable [3]) universality problem for non-deterministic timed automata (over finite words) to the problem of strong monitorability, following Diekert, Muscholl, and Walukiewicz [18].

Let $𝒜=(Q,Q_0,\mathrm{\Sigma },𝒳,\mathrm{\Delta },F)$ be such a timed automaton, i.e., a finite run is accepting if it ends in a location in $F$. We assume w.l.o.g. that $𝒜$ is complete in the sense that every word has a run. This can always be achieved by adding a fresh sink location and by rerouting all missing transitions to it.

We add a new letter $\mathrm{\#}\notin \mathrm{\Sigma }$ to obtain ${\mathrm{\Sigma }}_{\mathrm{\#}}=\mathrm{\Sigma }\cup \{\mathrm{\#}\}$ and construct a TBA ${𝒜}^{\prime }=(Q^{\prime },Q_0,{\mathrm{\Sigma }}_{\mathrm{\#}},𝒳,{\mathrm{\Delta }}^{\prime },F^{\prime })$ from $𝒜$ such that ${𝒜}^{\prime }$ is strongly monitorable if and only if $\text{L}(𝒜)=T{\mathrm{\Sigma }}^{\ast }$. To this end, we introduce three new locations $r,s,t$, i.e., $Q^{\prime }=Q\cup \{r,s,t\}$. Next, we define ${\mathrm{\Delta }}^{\prime }$ (see Figure 2) by copying the transitions from $\mathrm{\Delta }$ and by adding the following transitions, where we write $q\stackrel{𝑎}{\to }{q}^{\prime }$ to denote $(q,q^{\prime },a,\mathrm{\varnothing },\text{true})$:

• $\mathrm{■}$

  $\{q\stackrel{\#}{\to }r\mid q\in Q\setminus F\}$: from every non-accepting location of $𝒜$, there is a $\mathrm{\#}$-transition to $r$.

• $\mathrm{■}$

  $\{r\stackrel{𝑎}{\to }s,s\stackrel{𝑎}{\to }s\mid a\in \mathrm{\Sigma }\}$: for every $a\ne \mathrm{\#}$ there is an $a$-transition from $r$ to $s$ and an $a$-labeled self-loop on $s$.

• $\mathrm{■}$

  $\{s\stackrel{\#}{\to }r,r\stackrel{\#}{\to }r\}$: there is a $\mathrm{\#}$-transition from $s$ to $r$ and a $\mathrm{\#}$-labeled self-loop on $r$.

• $\mathrm{■}$

  $\{q\stackrel{\#}{\to }t\mid q\in F\}$: from every accepting location there is a $\mathrm{\#}$-transition to $t$.

• $\mathrm{■}$

  $\{t\stackrel{𝑎}{\to }t\mid a\in {\mathrm{\Sigma }}_{\mathrm{\#}}\}$: for every letter in ${\mathrm{\Sigma }}_{\mathrm{\#}}$, there is a self-loop on $t$ labeled with that letter.

We define the accepting locations of ${𝒜}^{\prime }$ as $F^{\prime }=Q\cup \{r,t\}$.

Figure 2 shows the TBA ${𝒜}^{\prime }$ with the locations of the (finite-word) timed automaton $𝒜$ partitioned into $F$ and $Q\setminus F$. In the figure, the new locations $r,s,$ and $t$ and accompanying transitions are shown separately from the original automaton. Double circles denote accepting locations. Intuitively, processing a $\mathrm{\#}$ from an accepting location of $𝒜$ takes the run to the accepting sink $t$. On the other hand, processing a $\mathrm{\#}$ from a non-accepting location of $𝒜$ takes the run to a component where the run continuation is accepting if and only if it processes infinitely many $\mathrm{\#}$’s.

It remains to show that the language $\text{L}({𝒜}^{\prime })$ is strongly monitorable if and only if $\text{L}(𝒜)=T{\mathrm{\Sigma }}^{\ast }$. One direction is trivial: If $\text{L}(𝒜)=T{\mathrm{\Sigma }}^{\ast }$, then $\text{L}({𝒜}^{\prime })=T{\mathrm{\Sigma }}_{\mathrm{\#}}^{\omega }$, as all words without a $\mathrm{\#}$ can be processed using the states of the complete automaton $𝒜$ (which are all accepting in ${𝒜}^{\prime }$) and all words with a $\mathrm{\#}$ can be accepted by moving to state $t$ (which is an accepting sink) when processing the first $\mathrm{\#}$. Hence, $\text{L}({𝒜}^{\prime })$ is strongly monitorable.

On the other hand, if $\text{L}(𝒜)\ne T{\mathrm{\Sigma }}^{\ast }$, then there exists a finite word $\rho \notin \text{L}(𝒜)$. Hence, every run prefix of ${𝒜}^{\prime }$ processing $\rho {\cdot }_{\tau (\rho )}(\mathrm{\#},\tau (\rho ))$ must be in location $r$. Now, chose some $a\in \mathrm{\Sigma }$. Then, for all ${\rho }^{\prime \prime }\in T{\mathrm{\Sigma }}_{\mathrm{\#}}^{\ast }$, we have:

• $\mathrm{■}$

  $\rho {\cdot }_{\tau (\rho )}(\mathrm{\#},\tau (\rho ))\cdot {\rho }^{\prime \prime }\cdot (a,0)(a,1)(a,2)\mathrm{\cdots }\notin L({𝒜}^{\prime })$ (as it contains only finitely many $\mathrm{\#}$).

• $\mathrm{■}$

  $\rho {\cdot }_{\tau (\rho )}(\mathrm{\#},\tau (\rho ))\cdot {\rho }^{\prime \prime }\cdot (\mathrm{\#},0)(\mathrm{\#},1)(\mathrm{\#},2)\mathrm{\cdots }\in L({𝒜}^{\prime })$ (as it contains infinitely many $\mathrm{\#}$).

Hence, $V_{L({𝒜}^{\prime })}(\rho {\cdot }_{\tau (\rho )}(\mathrm{\#},\tau (\rho ))\cdot {\rho }^{\prime \prime })=\text{?}$ for all ${\rho }^{\prime \prime }$. Thus, $L({𝒜}^{\prime })$ is not strongly monitorable.

In the case for weak monitorability we reduce the (undecidable [3]) universality problem for TBA (not TA as we did in the strong case). Additionally, as an intermediate step, we consider a problem about Brzozowski derivatives of properties of infinite timed words: Let $\rho \in T{\mathrm{\Sigma }}^{\ast }$ be a finite timed word and $\phi \subseteq T{\mathrm{\Sigma }}^{\omega }$ be such a property. We say that $\rho$ is a universal prefix for $\phi$ if the Brzozowski derivative

of $\phi$ and $\rho$ is equal to $T{\mathrm{\Sigma }}^{\omega }$. Note that if $\phi$ is equal to $T{\mathrm{\Sigma }}^{\omega }$, then every prefix is universal for $\phi$. However, the property $(a,0)\cdot T{\mathrm{\Sigma }}^{\omega }$ has a universal prefix (e.g., $(a,0)$), but is not universal.

Further, we say that $\phi$ is weakly $\top$-monitorable (cp. Definition 21) if and only if there is a $\rho$ such that $V_{\phi }(\rho )=\top$, i.e., in comparison to (standard) weak monitorability, we only consider the verdict $\top$. Note that $\phi$ has a universal prefix if and only if it is weakly $\top$-monitorable.

So, it remains to first reduce universality of TBA to the existence of a universal prefix for languages of TBA and then to reduce weak $\top$-monitorability to weak monitorability.

We begin with reducing TBA universality to the existence of universal prefixes. Intuitively, we add edges allowing to “restart” a run which allows every prefix to simulate the empty prefix. Then, every prefix behaves like the empty prefix, which is universal if and only if the automaton is universal.

Let $𝒜=(Q,Q_0,\mathrm{\Sigma },𝒳,\mathrm{\Delta },F)$ be a TBA. We add a new letter $\mathrm{\#}\notin \mathrm{\Sigma }$ to obtain ${\mathrm{\Sigma }}_{\mathrm{\#}}=\mathrm{\Sigma }\cup \{\mathrm{\#}\}$ and construct a TBA ${𝒜}^{\prime }=(Q^{\prime },Q_0,{\mathrm{\Sigma }}_{\mathrm{\#}},𝒳,{\mathrm{\Delta }}^{\prime },F^{\prime })$ from $𝒜$ such that $\text{L}(𝒜)=T{\mathrm{\Sigma }}^{\omega }$ if and only if ${𝒜}^{\prime }$ has a universal prefix. To this end, we introduce two new locations $r$ and $s$, i.e., $Q^{\prime }=Q\cup \{r,s\}$. Next, we define ${\mathrm{\Delta }}^{\prime }$ (see Figure 3) by copying the transitions from $\mathrm{\Delta }$ and by adding the following transitions, where we write $q\stackrel{𝑎}{\to }{q}^{\prime }$ to denote $(q,q^{\prime },a,\mathrm{\varnothing },\text{true})$:

• $\mathrm{■}$

  $\{q\stackrel{𝑎}{\to }r\mid q\in Q_0,a\in {\mathrm{\Sigma }}_{\mathrm{\#}}\}$: from every initial location of $𝒜$, there is an $a$-transition to $r$ for every $a\in {\mathrm{\Sigma }}_{\mathrm{\#}}$.

• $\mathrm{■}$

  $\{r\stackrel{𝑎}{\to }s,s\stackrel{𝑎}{\to }s\mid a\in \mathrm{\Sigma }\}$: for every $a\ne \mathrm{\#}$ there is an $a$-transition from $r$ to $s$ and an $a$-labeled self-loop on $s$.

• $\mathrm{■}$

  $\{s\stackrel{\#}{\to }r,r\stackrel{\#}{\to }r\}$: there is a $\mathrm{\#}$-transition from $s$ to $r$ and a $\mathrm{\#}$-labeled self-loop on $r$.

• $\mathrm{■}$

  $\{(q,q_0,\mathrm{\#},𝒳,\text{true})\mid q\in Q,q\in Q_0\}$: from every location there is a $\mathrm{\#}$-transition to each initial location, which resets all clocks.

We define the accepting locations of ${𝒜}^{\prime }$ as $F^{\prime }=Q\cup \{r\}$.

Let $\text{L}(𝒜)=T{\mathrm{\Sigma }}^{\omega }$ and fix some ${\mu }^{\prime }\in T{\mathrm{\Sigma }}_{\mathrm{\#}}^{\omega }$. If ${\mu }^{\prime }$ contains infinitely many $\mathrm{\#}$’s, then it is accepted by ${𝒜}^{\prime }$ using the new states $r$ and $s$. On the other hand, if ${\mu }^{\prime }$ contains only finitely many $\mathrm{\#}$’s, then it has the form

for some $n\ge 0$, where the ${\rho }_i$ and ${\mu }^{\prime \prime }$ are $\mathrm{\#}$-free. As each ${\rho }_i$ is a prefix of some word in $\text{L}(𝒜)=T{\mathrm{\Sigma }}^{\omega }$ and ${\mu }^{\prime \prime }$ is in $\text{L}(𝒜)=T{\mathrm{\Sigma }}^{\omega }$, one can construct an accepting run of ${𝒜}^{\prime }$ on ${\mu }^{\prime }$. Thus, $\text{L}({𝒜}^{\prime })=T{\mathrm{\Sigma }}_{\mathrm{\#}}^{\omega }$, i.e., $\epsilon$ is a universal prefix of ${𝒜}^{\prime }$.

Now for the other direction. If a word $\rho$ is a universal prefix of ${𝒜}^{\prime }$, then for all $\mu \in T{\mathrm{\Sigma }}^{\omega }$, the word $\rho \cdot (\mathrm{\#},0)\cdot \mu$ is accepted by ${𝒜}^{\prime }$. Hence, there is an accepting run of ${𝒜}^{\prime }$ on $\rho \cdot (\mathrm{\#},0)\cdot \mu$. As all $\mathrm{\#}$-transitions lead to an initial state of $𝒜$ and reset the clocks, and as $\mu$ does not contain any $\mathrm{\#}$’s, the suffix of the run on $\mu$ must also be an accepting run of $𝒜$, i.e., we have $\mu \in \text{L}(𝒜)$. Thus, $\text{L}(𝒜)=T{\mathrm{\Sigma }}^{\omega }$. This concludes the first step of our proof.

In the second and last step of our proof we reduce weak $\top$-monitorability to (standard) weak monitorability. Intuitively, we manipulate the automaton so that it can never give the verdict $\perp$ while preserving the existence of observations that yield the verdict $\top$.

Let $𝒜=(Q,Q_0,\mathrm{\Sigma },𝒳,\mathrm{\Delta },F)$ be a TBA. We add a new letter $\mathrm{\#}\notin \mathrm{\Sigma }$ to obtain ${\mathrm{\Sigma }}_{\mathrm{\#}}=\mathrm{\Sigma }\cup \{\mathrm{\#}\}$ and construct a TBA ${𝒜}^{\prime }=(Q^{\prime },Q_0^{\prime },{\mathrm{\Sigma }}_{\mathrm{\#}},𝒳,{\mathrm{\Delta }}^{\prime },F^{\prime })$ from $𝒜$ such that $𝒜$ is weakly $\top$-monitorable if and only if ${𝒜}^{\prime }$ is weakly monitorable.

Now $Q^{\prime }$ essentially contains two copies of $Q$: $Q_1=Q\times \{1\}$ and $Q_2=Q\times \{2\}$ as well as a new additional accepting location $r$. The transition relation of ${𝒜}^{\prime }$ is defined as follows (see also Figure 4), we write $q\stackrel{𝑎}{\to }{q}^{\prime }$ to denote $(q,q^{\prime },a,\mathrm{\varnothing },\text{true})$:

• $\mathrm{■}$

  $\{(q,1)\stackrel{\#}{\to }(q,1),(q,1)\stackrel{\#}{\to }r\mid q\in Q\}$: locations of $Q_1$ have a $\mathrm{\#}$-labeled self-loop and a $\mathrm{\#}$-transition to $r$.

• $\mathrm{■}$

  $\{((q,1),(q^{\prime },2),a,\lambda ,g)\mid (q,q^{\prime },a,\lambda ,g)\in \mathrm{\Delta }\}$: locations of $Q_1$ have their $\mathrm{\Sigma }$-labeled transitions redirected to $Q_2$.

• $\mathrm{■}$

  $\{(q,2),(q^{\prime },2),a,\lambda ,g)\mid (q,q^{\prime },a,\lambda ,g)\in \mathrm{\Delta }\}$: locations of $Q_2$ have copies of the $\mathrm{\Sigma }$-labeled transitions from $𝒜$.

• $\mathrm{■}$

  $\{(q,2)\stackrel{\#}{\to }(q,1)\mid q\in Q\}$: locations of $Q_2$ have $\mathrm{\#}$-labeled transitions directed back to $Q_1$.

• $\mathrm{■}$

  $\{r\stackrel{\#}{\to }r\}$: The new location $r$ has a $\mathrm{\#}$-labeled self-loop.

The set $Q_0^{\prime }$ of initial locations of ${𝒜}^{\prime }$ is $Q_0\times \{1\}$ and the set $F^{\prime }$ of accepting locations of ${𝒜}^{\prime }$ is $F\times \{2\}\cup \{r\}$.

Now, let $\rho \in T{\mathrm{\Sigma }}^{\ast }$ be a timed word witnessing weak $\top$-monitorability of $𝒜$, i.e., $\rho \cdot \mu \in L(𝒜)$ for every $\mu \in T{\mathrm{\Sigma }}^{\omega }$. We define ${\rho }^{\prime }=\rho$. In $𝒜$, processing ${\rho }^{\prime }$ leads to a location in $Q_2$. We argue that ${\rho }^{\prime }$ witnesses weak monitorability of ${𝒜}^{\prime }$. To this end, consider any ${\mu }^{\prime }\in T{\mathrm{\Sigma }}_{\mathrm{\#}}^{\omega }$ and let $\mu$ be obtained from ${\mu }^{\prime }$ by removing all occurrences of $\mathrm{\#}$. If $\mu$ is infinite, we may simply mimic the accepting run of $𝒜$ on $\mu$ from $\rho$ in ${𝒜}^{\prime }$. Clearly, this will also be accepting. If $\mu$ is finite, ${\mu }^{\prime }$ must have a suffix of the form $({\mathrm{\#}}^{\omega },\tau )$, where $\tau$ is a sequence of timepoints. This suffix is accepted by utilizing the $\mathrm{\#}$ transitions to $r$, from where the suffix $({\mathrm{\#}}^{\omega },\tau )$ can be accepted.

For the opposite direction, let ${\rho }^{\prime }\in T{\mathrm{\Sigma }}_{\mathrm{\#}}^{\ast }$ be a timed word witnessing weak monitorability of ${𝒜}^{\prime }$. That is, either ${\rho }^{\prime }\cdot {\mu }^{\prime }\in L({𝒜}^{\prime })$ for all ${\mu }^{\prime }$ or ${\rho }^{\prime }\cdot {\mu }^{\prime }\notin L({𝒜}^{\prime })$ for all ${\mu }^{\prime }$. However, note that for any finite ${\rho }^{\prime }$, we have ${\rho }^{\prime }\cdot (\mathrm{\#},0)(\mathrm{\#},1)(\mathrm{\#},2)\mathrm{\cdots }\in L({𝒜}^{\prime })$, due to the $\mathrm{\#}$-labeled transition to $r$, from where $(\mathrm{\#},0)(\mathrm{\#},1)(\mathrm{\#},2)\mathrm{\cdots }$ is accepted. Thus, we must be in the first case where we have ${\rho }^{\prime }\cdot {\mu }^{\prime }\in L({𝒜}^{\prime })$ for all ${\mu }^{\prime }$.

Now, let $\rho \in T{\mathrm{\Sigma }}^{\ast }$ be obtained from ${\rho }^{\prime }$ by stripping all occurrences of $\mathrm{\#}$ in ${\rho }^{\prime }$. We show that $\rho$ is a word witnessing weak $\top$-monitorability of $𝒜$. Note that any run of ${𝒜}^{\prime }$ on ${\rho }^{\prime }$ reaching a location in $Q_1$ or $Q_2$ can be mimicked by a run of $𝒜$ on $\rho$ reaching the corresponding location in $Q$. Let $\mu \in T{\mathrm{\Sigma }}^{\omega }$. Then ${\rho }^{\prime }\cdot \mu \in L({𝒜}^{\prime })$. Clearly, this must be due to an accepting run where a suffix of the run processing $\mu$ stays in $Q_2$. Hence, $\rho \cdot \mu \in L(𝒜)$, as we may mimic, for the prefix $\rho$, the prefix processing ${\rho }^{\prime }$ of the accepting run of ${𝒜}^{\prime }$ processing ${\rho }^{\prime }\cdot \mu$, and, for the suffix $\mu$, we simply copy the run staying in $Q_2$. $◀$

Due to Remark 12, we also obtain the undecidability of strong and weak $(\rho ,t)$-monitorability.

Fix a TMA $𝒜=(Q,Q_0,\mathrm{\Sigma },𝒳,\mathrm{\Delta },ℱ)$. The translation from TMA to TBA relies on the fact that $\text{L}(𝒜)={\bigcup }_{F\in ℱ}\text{L}({𝒜}_F)$, where ${𝒜}_F$ is the TMA $(Q,Q_0,\mathrm{\Sigma },𝒳,\mathrm{\Delta },\{F\}\}$. Alur and Dill translated each such ${𝒜}_F$ into an equivalent TBA ${𝒜}_F^{\prime }$ with set $Q\times \{0,1,\mathrm{\dots },|F|\}$ of locations and the same clocks as $𝒜$. Then, the disjoint union of the ${𝒜}_F^{\prime }$ for $F\in ℱ$ is a TBA that is equivalent to $𝒜$.

The TBA ${𝒜}_F^{\prime }$ constructed by Alur and Dill satisfy the following fact: $\text{L}({𝒜}_F^{\prime },((q,0),v))=\text{L}({𝒜}_F,(q,v))$ for all locations $q$ of $𝒜$ and all clock valuations. Thus, we have

Hence, we can symbolically compute the non-empty language states of $𝒜$ by symbolically computing the non-empty states of the ${𝒜}_F^{\prime }$ and then project the states of the form $(q,0)$ to $q$, but leaving the zones unchanged. $◀$

Using this result, we can decide monitorability.

We assume w.l.o.g. that the DTMA we are using are complete in the sense that every word has a run, which then must be unique due to determinism. This can always be achieved by adding a fresh sink location and by rerouting all missing transitions to it (while preserving determinism). Then, the reach-set ${𝒯}_{𝒜}(\rho ,t)$ of any observation $(\rho ,t)$ is a singleton set, as $𝒜$ is deterministic and complete. Thus, we identify ${𝒯}_{𝒜}(\rho ,t)$ with the unique state in it.

Now, given $𝒜$, we first compute the set $S_{𝒜}^{ne}$ of non-empty language states (see Lemma 18). Its complement is the set of empty language states, i.e., the set of states for which there is no accepting run starting there. Let us denote this set as $S_{𝒜}^{\mathrm{\varnothing }}=\overline{S_{𝒜}^{ne}}$ and note that we have ${𝒯}_{𝒜}(\rho ,t)\in S_{𝒜}^{\mathrm{\varnothing }}$ if and only if $V_{L(𝒜)}(\rho ,t)=\perp$, i.e., we can characterize the negative verdict in terms of the set $S_{𝒜}^{\mathrm{\varnothing }}$.

We now use backwards reachability to compute the set of states that can reach $S_{𝒜}^{\mathrm{\varnothing }}$. These are the states from where it is possible to reach a $\perp$-verdict. The sets $S_{𝒜}^{ne}$, $S_{𝒜}^{\mathrm{\varnothing }}$ and ${\text{Pre}}_{𝒜}^{\ast }(S_{𝒜}^{\mathrm{\varnothing }})$ are illustrated in Fig. 5, where ${\text{Pre}}_{𝒜}^{\ast }(S_{𝒜}^{\mathrm{\varnothing }})$ is the gray area.

By definition, we have ${𝒯}_{𝒜}(\rho ,t)\in {\text{Pre}}_{𝒜}^{\ast }(S_{𝒜}^{\mathrm{\varnothing }})$ if and only if there exists a ${\rho }^{\prime }\in T{\mathrm{\Sigma }}^{\ast }$ and a $t^{\prime }\in {ℝ}_{\ge 0}$ such that $s_0\stackrel{\rho {\cdot }_t{\rho }^{\prime }}{\to }(q,v)$ with $(q,v+t^{\prime })\in S_{𝒜}^{\mathrm{\varnothing }}$, where $s_0$ denotes the unique initial state of $𝒜$. The latter condition is equivalent to the existence of a ${\rho }^{\prime }\in T{\mathrm{\Sigma }}^{\ast }$ such that $s_0\stackrel{\rho {\cdot }_t{\rho }^{\prime }}{\to }{s}^{\prime }$ for some $s^{\prime }\in S_{𝒜}^{\mathrm{\varnothing }}$. Hence, ${𝒯}_{𝒜}(\rho ,t)\in {\text{Pre}}_{𝒜}^{\ast }(S_{𝒜}^{\mathrm{\varnothing }})$ if and only if there exists a ${\rho }^{\prime }\in T{\mathrm{\Sigma }}^{\ast }$ such that $V_{L(𝒜)}(\rho {\cdot }_t{\rho }^{\prime })=\perp$. Thus, ${𝒯}_{𝒜}(\rho ,t)\notin {\text{Pre}}_{𝒜}^{\ast }(S_{𝒜}^{\mathrm{\varnothing }})$ if and only if monitoring any extension of $(\rho ,t)$ will not provide the verdict $\perp$, i.e., $V_{L(𝒜)}(\rho {\cdot }_t{\rho }^{\prime })\ne \perp$ for all ${\rho }^{\prime }\in T{\mathrm{\Sigma }}^{\ast }$. Since DTMA are complementable, we can compute $S_{\overline{𝒜}}^{\mathrm{\varnothing }}$ for a complement automaton $\overline{𝒜}$ of $𝒜$ and provide the dual characterization for the $\top$-verdict: ${𝒯}_{\overline{𝒜}}(\rho ,t)\notin {\text{Pre}}_{\overline{𝒜}}^{\ast }(S_{\overline{𝒜}}^{\mathrm{\varnothing }})$ if and only if $V_{L(𝒜)}(\rho {\cdot }_t{\rho }^{\prime })\ne \top$ for all ${\rho }^{\prime }\in T{\mathrm{\Sigma }}^{\ast }$. Here, we rely on the fact that we have $V_L(\rho ,t)=\top$ if and only if $V_{\overline{L}}(\rho ,t)=\perp$ and $V_L(\rho ,t)=\perp$ if and only if $V_{\overline{L}}(\rho ,t)=\top$.

Now, recall that we can complement DTMA by only changing the acceptance condition, i.e., we can assume w.l.o.g. that $𝒜$ and $\overline{𝒜}$ have the same locations, clocks, and transitions, and thus we have ${𝒯}_{𝒜}(\rho ,t)={𝒯}_{\overline{𝒜}}(\rho ,t)$ for all $(\rho ,t)$.

Hence, using the above characterizations, we have ${𝒯}_{𝒜}(\rho ,t)\in S_{𝒜}^{\mathrm{\varnothing }}\cup S_{\overline{𝒜}}^{\mathrm{\varnothing }}$ if and only if $V_{L(𝒜)}(\rho ,t)\in \{\top ,\perp \}$ and thus ${𝒯}_{𝒜}(\rho ,t)\in {\text{Pre}}_{𝒜}^{\ast }(S_{𝒜}^{\mathrm{\varnothing }}\cup S_{\overline{𝒜}}^{\mathrm{\varnothing }})$ if and only if there exists a ${\rho }^{\prime }\in T{\mathrm{\Sigma }}^{\ast }$ such that $V_{L(𝒜)}(\rho {\cdot }_t{\rho }^{\prime })\in \{\top ,\perp \}$. Thus, $L(𝒜)$ is weakly $(\rho ,t)$-monitorable if and only if