Time for Timed Monitorability

TL;DR

This work analyzes monitorability for real-time properties expressed as Timed Automata. It establishes a sharp boundary: strong and weak monitorability are decidable for deterministic Timed Muller Automata ($DTMA$) but undecidable for nondeterministic Timed Büchi Automata ($TBA$), with the notable exception of bounded weak $\bot$-monitorability for $TBA$. It further refines monitoring with step-bounded horizons and time-horizon verdicts, providing effective, zone-based methods for $DTMA$ and illustrating practical benefits for runtime verification of real-time systems. Overall, the results motivate using deterministic automata for monitorability analysis and offer actionable metrics to bound and schedule monitoring decisions in real time.

Abstract

Monitoring is an important part of the verification toolbox, in particular in situations where exhaustive verification using, e.g., model-checking is infeasible. The goal of online monitoring is to determine the satisfaction or violation of a specification during runtime, i.e., based on finite execution prefixes. However, not every specification is amenable to monitoring, e.g., properties for which no finite execution can witness satisfaction or violation. Monitorability is the question of whether a given specification is amenable to monitoring, and has been extensively studied in discrete time. Here, we study the monitorability problem for real-time properties expressed as Timed Automata. For specifications given by deterministic Timed Muller Automata, we prove decidability while we show that the problem is undecidable for specifications given by nondeterministic Timed Büchi automata. Furthermore, we refine monitorability to also determine bounds on the number of events as well as the time that must pass before monitoring the property may yield an informative verdict. We prove that for deterministic Timed Muller automata, such bounds can be effectively computed. In contrast we show that for nondeterministic Timed Büchi automata such bounds are not computable.

Figures (5)

• Figure 1: DTBA for the language of the MITL formula $\varphi = F_{[0,10]}a \land G_{[0,20]}\neg b$ and its negation: If location $\varphi$ ($\neg \varphi$) is accepting then it accepts $L(\varphi)$ ($L(\neg \varphi)$, respectively).
• Figure 2: The TBA $\mathcal{A}\xspace'$ constructed for the proof of Theorem \ref{['thm:undecmoni']}.
• Figure 3: The TBA $\mathcal{A}\xspace'$ constructed for the proof of Theorem \ref{['thm:undecmoni']}.
• Figure 4: The TBA $\mathcal{A}\xspace^{\prime}\xspace$ constructed for the proof of Theorem \ref{['thm:undecmoni']}. Intuitively, $\mathcal{A}\xspace^{\prime}\xspace$ has two disjoint copies of the locations of $\mathcal{A}\xspace$ and $\Sigma$-labeled transitions lead from both copies to the second copy, while $\#$-labeled transitions from the second copy lead to the first copy. The first copy additionally has $\#$-labeled self-loops on all locations and $\#$-labeled transitions to $r$.
• Figure 5: Representation of all states of an automaton $\mathcal{A}$. On the left, only the empty language states $S^{\emptyset}_{\mathcal{A}\xspace}$ and non-empty language states $S^{ne}_{\mathcal{A}\xspace}$ are shown. On the right, the states in $\textit{Pre}^*_\mathcal{A}\xspace(S^{\emptyset}_{\mathcal{A}\xspace}\xspace)$ are gray. The solid arrows are examples of possible transitions and the dashed arrows are examples of impossible transitions. A state in $S^{\emptyset}_{\mathcal{A}\xspace}$ has no accepting run, thus cannot reach $S^{ne}_{\mathcal{A}\xspace}$. A state in $S^{ne}_{\mathcal{A}\xspace}$ might reach a state in $S^{\emptyset}_{\mathcal{A}\xspace}$. A state outside $\textit{Pre}^*_\mathcal{A}\xspace(S^{\emptyset}_{\mathcal{A}\xspace}\xspace)$ cannot reach $S^{\emptyset}_{\mathcal{A}\xspace}$.

Theorems & Definitions (40)

• Example 1
• Proposition 1
• Proposition 2: alur1996mitlbrihaye2017mightyl
• Example 2
• Definition 1: Observation
• Definition 2: Timed Monitoring Function
• Example 3
• Proposition 3: Effectiveness of Timed Monitoring DBLP:conf/formats/GrosenKLZ22
• Definition 3: Timed Monitorability
• Example 4