Keywords

1 Introduction

Online monitoring is a runtime verification (RV) technique [11] that, by sacrificing completeness, aims to lighten the burden caused by exhaustive formal methods. A monitor watches an unbounded sequence f of observations, called trace, one observation at a time. At each time \(n\ge 0\), it tries to provide information about the value assigned to f by the specification. For a boolean specification P, after each trace prefix s, the monitor may output one of three values: all infinite extensions of s satisfy P, violate P, or neither [15].

Quantitative specifications [21] generalize their boolean analogs by assigning each trace f a value from some richer domain. For example, the boolean specification \(\textsf{Resp}\) assigns true to f iff every observation \(\texttt {req}\) in f is eventually followed by an observation \(\texttt {ack}\) in f, while the quantitative specification \(\textsf{MaxRespTime}\) assigns the least upper bound on the number of observations between each \(\texttt {req}\) and the corresponding \(\texttt {ack}\), or \(\infty \) if there is no such upper bound.

In the limit monitoring of a quantitative specification \(\varPhi \) over a trace f, a limit (e.g., \(\limsup \), \(\liminf \)) of the infinite sequence of monitor outputs should provide information about the value \(\varPhi (f)\) assigned to the trace. For example, a “natural way to monitor” \(\textsf{MaxRespTime}\) is to have the monitor output, at each time, the maximum of (i) the maximal response time so far and (ii) the time since the least recent pending \(\texttt {req}\), if there is a pending \(\texttt {req}\). The \(\limsup \) (and \(\liminf \)) of this infinite output sequence converges towards \(\textsf{MaxRespTime}\).

In contrast to its boolean analog, the quantitative setting naturally supports approximation. A monitor has error \(\delta \ge 0\) if, for all infinite traces, the limit of the output sequence is within \(\delta \) of the specification value. In particular, this leads to precision-resource trade-offs for quantitative monitors: The provisioning of additional states, registers, or operations may reduce the error, and a larger error tolerance may enable monitors that use fewer resources.

In this paper, we provide a formal framework for studying such precision-resource trade-offs for an abstract definition of quantitative monitors. This abstract framework can be instantiated, for example, by finite-state monitors or register monitors, where a finite-state monitor remembers a bounded amount of information about each trace prefix, and a register monitor remembers a bounded number of integer values [32]. For us, an abstract monitor partitions, at each time n, all prefixes of length up to n into a finite number of equivalence classes such that if two prefixes \(s_1\) and \(s_2\) are equivalent, then the monitor outputs the same value after observing \(s_1\) and \(s_2\). The number of equivalence classes introduced at time n provides a natural measure for the resource use of the abstract monitor after n observations.

In this setting, where the resource use of a monitor is measured, we also want to measure the precision of a monitor. To define the precision of a monitor after a finite trace prefix, we need to enrich our definition of quantitative specifications: We let a quantitative specification assign values not only to infinite traces but also to finite traces. Indeed, many specification values for infinite traces are usually defined as limits [37]. For example, what we called above the “natural way to monitor” \(\textsf{MaxRespTime}\) using two counters is, in fact, the usual formal definition of the quantitative specification \(\textsf{MaxRespTime}\).

Once both specifications and monitors assign values to all finite traces, there is a natural definition for the precision of a monitor: At each time n, the prompt-error is the maximal difference between the monitor output and the specification value over all finite traces of length up to n. Furthermore, the limit-error is the least upper bound on the difference between the limit of monitor outputs and the limit of specification values over all infinite traces. Note that if the prompt-error of a monitor is 0, then so is the limit-error, but not necessarily vice versa. An exact-value monitor (i.e., a monitor with prompt-error \(\delta =0\)) implements the specification as it is defined. In contrast, an approximate monitor (i.e., a monitor with prompt-error \(\delta >0\)) of the same specification may use fewer resources. An approximate monitor may still achieve limit-error 0, which is a situation of particular interest that we study.

Given an abstract monitor, one way to obtain a new monitor that uses fewer resources use is to merge some equivalence classes, and one way to increase the precision is to split some equivalence classes. However, this naive approach toward reaching a desired precision or resource use is not always the best. For an approximate monitor with a given prompt-error and limit-error, the goal is resource-optimality, i.e., minimizing the resource use as much as the error threshold allows. We will see that merging the equivalence classes of a given monitor may not yield a resource-optimal one.

The limit-error of a monitor is bounded by its prompt-error. We also investigate the case where we require a certain limit-error while leaving the prompt-error potentially unbounded. We will see that allowing arbitrary prompt-error may not permit the monitor to save resources if the desired limit-error is fixed. We say that such specifications have resource-intensive limit behavior. In fact, \(\textsf{MaxRespTime}\) displays resource-intensive limit behavior. Other examples include a subclass of reversible specifications. Reversibility is a notion from automata theory characterized by the specification being realizable with a finite-state automaton that is both forward and backward deterministic. A similar notion, generalized to the quantitative setting, can be introduced in our framework, allowing an abstract monitor to process an infinite trace in a two-way fashion.

Overview. Section 2 formalizes the framework of abstract monitors and provides insights on relations between basic notions such as resource use and precision.

Section 3 focuses on monitoring with bounded error over finite traces. First, in Subsect. 3.1, we show that the exact-value monitor over finite traces is unique and resource-optimal for every specification. Additionally, for resource-optimal approximate monitors, we prove: (i) they are not unique in Subsect. 3.1, (ii) they do not necessarily follow the structure of the exact-value monitor in Subsect. 3.2, and (iii) they do not necessarily minimize their resource use at each time in Subsect. 3.2. Then, in Subsect. 3.3, we study precision-resource trade-off suitability: We exhibit (i) a specification for which we can arbitrarily improve the resource use by damaging precision, and (ii) another for which we arbitrarily improve the precision by damaging the resource use.

Section 4 focuses on monitoring without error on infinite traces. In particular, in Subsect. 4.1 we provide a condition for identifying specifications with resource-intensive limit behavior, for which having zero limit-error prevents the trade-off between resource use and error on finite traces. This condition captures two paradigmatic specifications: (i) maximal response-time and (ii) average response-time. Finally, in Subsect. 4.2 we investigate reversible specifications, which can be implemented in a manner both forward and backward deterministic. A subclass of reversible specifications have resource-intensive limit behavior, which we demonstrate through the average ping specification.

Section 5 concludes the paper and addresses future research directions our framework offers.

Related Work. In the boolean setting, several notions of monitorability have been proposed over the years [15, 30, 34]. Much of the theoretical efforts have focused on regular specifications [2, 14, 46], although some proposed more expressive models [9, 12, 26]. We refer the reader to [10] for coverage of these and more.

Verification of quantitative specifications [21, 41] have received significant attention, especially in the probabilistic setting [17, 20, 33]. In the context of RV, the literature on specifications with quantitative aspects features primarily metric temporal logic and signal temporal logic [38, 40, 43,44,45]. Other efforts include processing data streams with a focus on deciding their properties at runtime [5, 6] and an extension of weighted automata with monitor counters [22]. None of these works focus on monitoring quantitative specifications with approximate verdicts or the relation between monitorability and monitor resources.

Approximate methods have been used in verification for many years [25, 39]. Beyond the boolean setting, such approaches have appeared in the context of sensor networks for approximating aggregate functions in a distributed setting [24, 49, 50], in approximate determinization or minimization of quantitative models of computation [7, 16, 35], and also in online algorithms [3].

To the best of our knowledge, the use of approximate methods in monitoring mainly concentrates on the specification rather than taking approximateness as a monitor feature and studying the quality of monitor verdicts. In predictive or assumption-based monitoring [23, 54] and for monitoring hyperproperties [51], an over-approximation of the system under observation is used as an assumption to limit the set of possible traces [36]. Similarly, in runtime quantitative verification [18, 47], the underlying probabilistic model of the system is approximated and continually updated. For monitoring under partial observability, [4] describes an approach to approximate the given specification for minimizing the number of undetected violations. In the branching-time setting, [1] uses a monitorable under- or over-approximation of the given specification to construct an “optimal” monitor. Nonetheless, a form of distributed and approximate limit monitoring for spatial specifications was studied in [8]. None of these works consider approximateness as a monitor property to study the relation between monitor resources and the quality of its verdicts.

Recently, [32] introduced a concrete monitor model with integer-valued registers and studied their resource needs. This model was later used for limit monitoring of statistical indicators of traces under probabilistic assumptions [31]. A general framework for approximate limit monitoring of quantitative specifications was proposed in [37]. However, that framework focuses exclusively on limit behaviors and on specific monitor models such as finite automata and register machines, thus allowing only limited precision-cost analyses. The main innovations of the present work over previous work are twofold. First, we abstract the monitor model and its resource use away from specific machine models. Second, by introducing prompt-errors, we study the resource use of monitors over time and relate this to the monitoring precision over time. This more nuanced framework enables a more fine-grained analysis and comparison of different monitors for the same specification concerning their precision and resource use.

2 Definitional Framework

Let \(\varSigma = \{a,b,\ldots \}\) be a finite alphabet of observations. A trace is finite or infinite sequence of observations, which we respectively denote by \(s,r,t \in \varSigma ^*\) and \(f,g \in \varSigma ^\omega \). Given two traces \(s \in \varSigma ^*\) and \(w \in \varSigma ^* \cup \varSigma ^\omega \), we denote by \(s \prec w\) (resp. \(s \preceq w\)) that s is a strict (resp. non-strict) prefix of w. For \(n \in \mathbb {N}\) we define \(\varSigma ^{\le n} = \{s\in \varSigma ^* \;|\;|s|\le n\}\) where |s| refers to the length of s. Given \(a \in \varSigma \) and \(s \in \varSigma ^*\), we denote by \(|s|_a\) the number of occurrences of a in s.

We denote by \(\mathbb {N}\) the set of non-negative integers and by \(\mathbb {R}\) the set of real numbers. We also consider \(\overline{\mathbb {N}}= \mathbb {N}\cup \{+\infty \}\) and \(\overline{\mathbb {R}}= \mathbb {R}\cup \{{-}\infty , {+}\infty \}\).

A binary relation \({\sim }\) over \(\varSigma ^*\) is an equivalence relation when it is reflexive, symmetric, and transitive. For a given equivalence relation \({\sim }\) over \(\varSigma ^*\) and a finite trace \(s \in \varSigma ^*\), we denote by \([s]_{{\sim }}\) the equivalence class of \({\sim }\) in which s belongs. When \({\sim }\) is clear from the context, we write [s] instead. A right-monotonic relation \({\sim }\) over \(\varSigma ^*\) fulfills \(s_1\sim s_2 \Rightarrow s_1r \sim s_2r\) for all \(s_1,s_2,r \in \varSigma ^*\).

We use \(\Box \) and \(\Diamond \) to denote the linear temporal logic (LTL) operators always and eventually, respectively. See [48] for interpretation of LTL operators on infinite traces, and [19, 27, 29] on finite traces.

2.1 Quantitative Specifications

A limit-measure is a function from \(\overline{\mathbb {R}}^\omega \) to \(\overline{\mathbb {R}}\). Given an infinite sequence of real numbers \(x = x_1x_2\dots \), we define \(\liminf (x) = \lim _{n \mapsto +\infty } \inf \{x_i \;|\;i\ge n\}\) and \(\limsup (x) = \lim _{n \mapsto +\infty } \sup \{x_i \;|\;i\ge n\}\). Whenever \(\liminf (x) = \limsup (x)\) for a given sequence x, we simply write \(\lim (x)\). A value function \(\pi :\varSigma ^* \rightarrow \overline{\mathbb {R}}\) associates a value to each finite trace.

Definition 1 (specification)

A specification extends a value function by constraining its limit behavior. Syntactically, it is a tuple \(\varPhi = (\pi , \ell )\) where \(\pi :\varSigma ^* \rightarrow \overline{\mathbb {R}}\) is a value function and \(\ell \) is a limit-measure. Semantically, it is a function defined by \({[\!\![\varPhi ]\!\!]}(s) = \pi (s)\) when \(s \in \varSigma ^*\) and \({[\!\![\varPhi ]\!\!]}(f) = \ell (\pi (f))\) when \(f \in \varSigma ^\omega \), where \(\pi (f) = (\pi (s_i))_{i \in \mathbb {N}}\) is a sequence over the prefixes \(s_i \prec f\) of increasing length i.

Together with a given specification \(\varPhi \), we define the right-monotonic equivalence relation \({\sim }^*_{\varPhi }\) as follows. For all \(s_1, s_2 \in \varSigma ^*\) we have \(s_1 \sim ^*_\varPhi s_2\) iff \(\pi (s_1 r) = \pi (s_2 r)\) holds for all \(r \in \varSigma ^*\).

We define below the discounted response specification. Throughout the section, we will use this specification as a running example.

Example 2

Let \(\varSigma = \{\texttt {req}, \texttt {ack}, \texttt {other}\}\) and consider the LTL response specification \(P = \Box (\texttt {req}\rightarrow \Diamond \texttt {ack})\). Let \(0< \lambda < 1\) be a discount factor. We define \(\textsf{DiscResp}(s) = 1\) if \(s \in P\), and \(\textsf{DiscResp}(s) = \lambda ^n\) otherwise, where \(n = |s| - |r|\) and \(r \prec s\) is the longest prefix of s with \(r \in P\). We define \(\varPhi _{\textsf{DR}} = (\textsf{DiscResp}, \limsup )\), the discounted response specification. Intuitively, \(\varPhi _{\textsf{DR}}\) assigns each finite trace a value that shows how close the system behaves to P such that, at the limit, it denotes whether the infinite behavior satisfies P or not.

Now, take two traces \(s,r \in \varSigma ^*\). We claim that \(s \sim ^*_{\varPhi _{\textsf{DR}}} r\) iff either (i) both traces have no pending request or (ii) both have a request pending for the same number of steps. First, we assume \(s \sim ^*_{\varPhi _{\textsf{DR}}} r\) holds and note that we must have \(\varPhi _{\textsf{DR}}(st) = \varPhi _{\textsf{DR}}(rt)\) for every \(t \in \varSigma ^*\). Then, we eliminate the cases other than (i) and (ii) as follows. If, w.l.o.g., \(s \in P\) and \(r \notin P\), then \(\varPhi _{\textsf{DR}}(r) < \varPhi _{\textsf{DR}}(s) = 1\), thus \(s \not \sim ^*_{\varPhi _{\textsf{DR}}} r\). If, w.l.o.g., s has a request pending for i steps and r for \(j > i\) steps, then \(\varPhi _{\textsf{DR}}(r) = \lambda ^j < \lambda ^i = \varPhi _{\textsf{DR}}(s)\), thus \(s \not \sim ^*_{\varPhi _{\textsf{DR}}} r\). The other direction is similar.

2.2 Abstract Monitors

We are now ready to present our abstract definition of quantitative monitors.

Definition 3 (monitor)

A monitor \(\mathcal {M}= (\sim , \gamma )\) is a tuple consisting of a right-monotonic equivalence relation \({\sim }\) on \(\varSigma ^*\) and a function \(\gamma :({\varSigma ^* / \sim }) \rightarrow \overline{\mathbb {R}}\). Let \(\delta _{\textrm{fin}},\delta _{\lim } \in \overline{\mathbb {R}}\) be error thresholds. We say that \(\mathcal {M}\) is a \((\delta _{\textrm{fin}},\delta _{\lim })\)-monitor for a given specification \(\varPhi = (\pi , \ell )\) iff

  • \(|\pi (s) - \gamma ([s])| \le \delta _{\textrm{fin}}\) for all \(s \in \varSigma ^*\), and

  • \(|\ell (\pi (f)) - \ell (\gamma ([f]))| \le \delta _{\lim }\) for all \(f \in \varSigma ^\omega \).

where \(\gamma ([f]) = (\gamma ([s_i]))_{i \in \mathbb {N}}\) is a sequence over the prefixes \(s_i \prec f\) of increasing length i. We say that \(\mathcal {M}\) has a prompt-error of \(\delta _{\textrm{fin}}\) and a limit-error of \(\delta _{\lim }\).

We conveniently write \(\mathcal {M}(s) = \gamma ([s])\) when \(s \in \varSigma ^*\) and \(\mathcal {M}(f) = \ell (\gamma ([f]))\) when \(f \in \varSigma ^\omega \).

Observe that, for every specification, there is an obvious monitor that imitates exactly the specification, which we define as follows.

Definition 4 (exact-value monitor)

Let \(\varPhi = (\pi , \ell )\) be a specification. The exact-value monitor of \(\varPhi \) is defined as \(\mathcal {M}_\varPhi = (\sim _\varPhi ^*, s \mapsto \pi (s))\).

A monitor for a given specification is approximate when it differs from the specification’s exact-value monitor. Below we demonstrate the exact-value monitor and an approximate monitor for the discounted response specification.

Example 5

Recall from Example 2 the discounted response specification \(\varPhi _{\textsf{DR}}\). Clearly, its exact-value monitor is \(\mathcal {M}_{\varPhi _{\textsf{DR}}} = ({\sim }^*_{\varPhi _{\textsf{DR}}}, \gamma _{\varPhi _{\textsf{DR}}})\) where \(\gamma _{\varPhi _{\textsf{DR}}}([s]) = \varPhi _{\textsf{DR}}(s)\) for all \(s \in \varSigma ^*\). Let us define another monitor \(\mathcal {M}= (\sim , \gamma )\) such that \(s \sim r\) iff either \(s,r \in P\) or \(s,r \notin P\) for every \(s,r \in \varSigma ^*\); and \(\gamma ([s]) = 1\) if \(s \in P\), and \(\gamma ([s]) = 0\) if \(s \notin P\). Note that for every \(f \in \varSigma ^\omega \) we have \(f \in P\) iff infinitely many prefixes of f belong to P, therefore \(\mathcal {M}\) has no limit-error. However, it yields a prompt-error of \(\lambda \) since it immediately outputs 0 instead of discounting on finite traces. Hence, \(\mathcal {M}\) is a \((\lambda ,0)\)-monitor for \(\varPhi _{\textsf{DR}}\).

Next, we prove that our definition constrains monitors not to make two equivalent traces too distant.

Proposition 6

Let \(\mathcal {M}= ({\sim }, \gamma )\) be a \((\delta _{\textrm{fin}}, \delta _{\lim })\)-monitor for the specification \(\varPhi = (\pi , \ell )\). For all \(s_1,s_2\in \varSigma ^*\), if \(s_1 \sim s_2\), then \(|\varPhi (s_1) - \varPhi (s_2)| \le 2 \delta _{\textrm{fin}}\).

Proof

By definition of \(\mathcal {M}\) we have that \(-\delta _{\textrm{fin}} \le \pi (s_1)-\gamma ([s_1])\le \delta _{\textrm{fin}}\) as well as \(\delta _{\textrm{fin}} \ge -\pi (s_2)+\gamma ([s_2]) \ge -\delta _{\textrm{fin}}\). If \(s_1 \sim s_2\) then \(\gamma ([s_1])=\gamma ([s_2])\) and thus \(-2\delta _{\textrm{fin}} \le \pi (s_1)-\pi (s_2)\le 2\delta _{\textrm{fin}}\).    \(\square \)

2.3 Resource Use of Abstract Monitors

As we demonstrated above, quantitative monitors may have different degrees of precision. A natural question is whether monitors with different error thresholds use a different amount of resources. To answer this question in its generality, we consider the following model-oblivious notions of resource use.

Definition 7 (resource use)

Let \(\mathcal {M}= ({\sim }, \gamma )\) be a monitor. We consider two notions of resource use for \(\mathcal {M}\) defined as functions from \(\mathbb {N}\) to \(\mathbb {N}\). We define step-wise resource use as \(\textbf{r}_n(\mathcal {M}) = |\varSigma ^{\le n} / {\sim }| - |\varSigma ^{< n} / {\sim }|\), and total resource use as \(\textbf{R}_n(\mathcal {M}) = \sum _{i=0}^{n} \textbf{r}_i(\mathcal {M}) = |\varSigma ^{\le n} / {\sim }|\).

Given two monitors \(\mathcal {M}_1\) and \(\mathcal {M}_2\), we compare their resource use as follows. We write \(\textbf{r}(\mathcal {M}_1) < \textbf{r}(\mathcal {M}_2)\) when there exists \(n_0 \in \mathbb {N}\) such that for every \(n \ge n_0\) we have \(\textbf{r}_n(\mathcal {M}_1) < \textbf{r}_n(\mathcal {M}_2)\). In particular, when it holds for \(n_0 = 1\), we write \(\textbf{r}(\mathcal {M}_1) \ll \textbf{r}(\mathcal {M}_2)\). We define \(\textbf{R}(\mathcal {M}_1) < \textbf{R}(\mathcal {M}_2)\) and \(\textbf{R}(\mathcal {M}_1) \ll \textbf{R}(\mathcal {M}_2)\) similarly. Figure 1 shows how these notions relate. Moreover, definitions of \(\textbf{r}(\mathcal {M}_1) \propto \textbf{r}(\mathcal {M}_2)\) and \(\textbf{R}(\mathcal {M}_1) \propto \textbf{R}(\mathcal {M}_2)\) for \(\propto \; \in \{{\le },{\mathrel {\underline{\ll }}},{>},{\gg },{\ge },{\mathrel {\underline{\gg }}}\}\) are as expected.

The monitor \(\mathcal {M}_1\) uses at most as many resources as \(\mathcal {M}_2\) when we have \(\textbf{r}(\mathcal {M}_1)~\mathrel {\underline{\ll }}~\textbf{r}(\mathcal {M}_2)\). If we further have \(\textbf{r}_n(\mathcal {M}_1) < \textbf{r}_n(\mathcal {M}_2)\) for some \(n \ge 1\), then \(\mathcal {M}_1\) uses fewer resources than \(\mathcal {M}_2\). We similarly define the cases for using at least as many and more resources.

Given a specification \(\varPhi \) and a \((\delta _{\textrm{fin}}, \delta _{\lim })\)-monitor \(\mathcal {M}\) for \(\varPhi \), we say that \(\mathcal {M}\) is resource-optimal for \(\varPhi \) when for every \((\delta _{\textrm{fin}}, \delta _{\lim })\)-monitor \(\mathcal {M}'\) for \(\varPhi \) we have \(\textbf{r}(\mathcal {M}) \mathrel {\underline{\ll }}\textbf{r}(\mathcal {M}')\), i.e., \(\mathcal {M}\) uses at most as many resources as any other monitor \(\mathcal {M}'\) with the same error thresholds.

Example 8

Recall from Examples 2 and 5 the discounted response specification \(\varPhi _{\textsf{DR}}\), its exact-value monitor \(\mathcal {M}_{\varPhi _{\textsf{DR}}}\), and the \((\lambda ,0)\)-monitor \(\mathcal {M}\). We claim that \(\mathcal {M}\) uses fewer resources than \(\mathcal {M}_{\varPhi _{\textsf{DR}}}\). To show this, we first point out that \(\textbf{r}_0(\mathcal {M})~=~\textbf{r}_1(\mathcal {M})~=~1\) and \(\textbf{r}_n(\mathcal {M}) = 0\) for every \(n \ge 2\). However, \(\textbf{r}_n(\mathcal {M}_{\varPhi _{\textsf{DR}}}) \ge 1\) for every \(n \ge 0\) because at each step the trace \(\texttt {req}^n\) is not equivalent to any shorter trace. Therefore, while \(\mathcal {M}_{\varPhi _{\textsf{DR}}}\) is an infinite-state monitor, \(\mathcal {M}\) is a finite-state monitor, and \(\textbf{r}(\mathcal {M}) < \textbf{r}(\mathcal {M}_{\varPhi _{\textsf{DR}}})\).

Fig. 1.
figure 1

Implications between the comparisons of resource use.

Full size image

Finally, we conclude the description of our framework by proving the implications in Fig. 1 to establish how different ways to compare resource use of monitors relate as well as a refinement property for resource-optimal monitors.

Proposition 9

For every monitor \(\mathcal {M}_1\) and \(\mathcal {M}_2\) the implications in Fig. 1 hold.

Proposition 10

Let \(\varPhi \) be a specification and \(\delta _{\textrm{fin}}, \delta _{\lim }\) be two error thresholds. Given \((\delta _{\textrm{fin}}, \delta _{\lim })\)-monitors \(\mathcal {M}_1 = ({\sim _1}, \gamma _1)\) and \(\mathcal {M}_2 = ({\sim _2}, \gamma _2)\) for \(\varPhi \). If \({\sim _1} \subseteq {\sim _2}\) and \(\mathcal {M}_1\) is resource-optimal, then \({\sim _1} = {\sim _2}\). Thus, \(\mathcal {M}_2\) is also resource-optimal.

We remark that our definitional framework can be instantiated by existing monitor models, e.g., finite state automata [15] or register monitors [32, 37]. More concretely, let us consider the discounted response specification \(\varPhi _{\textsf{DR}}\) from Example 2. Its exact-value monitor \(\mathcal {M}_{\varPhi _{\textsf{DR}}}\) from Example 5 can be implemented by a register monitor that stores the value n in its single register while checking for the LTL specification P using its finite-state memory. On the other hand, the monitor \(\mathcal {M}\) from Example 5 can be implemented by a finite state machine.

3 Approximate Prompt Monitoring

The original purpose of a monitor is to provide continuous feedback about the system status with respect to the specification [13, 30]. Focusing only on limit monitoring may allow an unbounded prompt-error and thus fail to fulfill this task. In this section, we consider prompt monitoring, i.e., the case where the monitor performs bounded prompt-error. First, we remark that considering a bounded prompt-error implicitly bounds the limit-error by definition.

Fact 11

Let \(\varPhi \) be a specification and \(\delta _{\textrm{fin}}, \delta _{\lim }\in \overline{\mathbb {R}}\) be error thresholds. If \(\mathcal {M}\) is a \((\delta _{\textrm{fin}}, \delta _{\lim })\)-monitor for \(\varPhi \), then it is also a \((\delta _{\textrm{fin}}, x)\)-monitor for \(\varPhi \) where \(x= \min \{\delta _{\textrm{fin}}, \delta _{\lim }\}\).

3.1 Uniqueness of Resource-Optimal Prompt Monitors

The exact-value monitor is arguably the most natural monitor for a given specification. In fact, it is the unique error-free monitor that is resource-optimal.

Theorem 12

Let \(\varPhi \) be a specification, and \(\delta \in \overline{\mathbb {R}}\) be an error threshold. Then, \(\mathcal {M}_\varPhi \) is the unique resource-optimal \((0,\delta )\)-monitor for \(\varPhi \).

Proof

Let \(\varPhi = (\pi , \ell )\). Consider \(\mathcal {M}= ({\sim }, \gamma )\) as a resource-optimal \((0,\delta )\)-monitor for \(\varPhi \). We get \({\sim } \subseteq {\sim _{\varPhi }^*}\) thanks to the following implications.

$$\begin{aligned} s_1 \sim s_2&\implies \forall r\in \varSigma ^*,\, s_1r \sim s_2r&\quad \text {(right-monotonicity)}\\&\implies \forall r\in \varSigma ^*,\, \gamma ([s_1r]) = \gamma ([s_2r])&\quad \text {(definition)}\\&\implies \forall r\in \varSigma ^*,\, \pi (s_1r) = \pi (s_2r)&\quad \text {(prompt-error 0)}\\&\implies s_1 \sim _\varPhi ^* s_2&\quad \text {(definition)} \end{aligned}$$

On the one hand, we have that \({\sim } = {\sim _\varPhi ^*}\) by Proposition 10. On the other hand, we have that \(\gamma ([s]) = \pi (s)\) for all \(s\in \varSigma ^*\) since the prompt-error threshold is 0. As a direct consequence, \(\mathcal {M}= \mathcal {M}_\varPhi \).    \(\square \)

Fig. 2.
figure 2

A specification \(\varPhi \) over \(\varSigma = \{a,b,c\}\) where \(x > 0\) and \(y \le x\), and two resource-optimal (x, y)-monitors for \(\varPhi \) shown on top of the exact-value monitor \(\mathcal {M}_\varPhi \). As indicated by the output values on the dotted and dashed rectangles, the approximate monitors merge some equivalence classes of \(\mathcal {M}_\varPhi \) to save resources at the cost of losing precision.

Full size image

Unfortunately, the uniqueness of resource-optimal monitors does not necessarily hold once we allow erroneous monitor verdicts. For instance, Fig. 2 shows on the left a specification \(\varPhi \) parameterized by x and y, together with its exact-value monitor \(\mathcal {M}_\varPhi \) on the right. In addition, the figure highlights two ways to make \({\sim _{\varPhi }}\) coarser to obtain distinct resource-optimal (x, y)-monitors for \(\varPhi \).

Proposition 13

For all \(x > 0\) and \(y \le x\) there exists a specification \(\varPhi \) that admits multiple resource-optimal (x, y)-monitors.

Fig. 3.
figure 3

A specification for which no (1, 0)-monitor that \(\mathcal {M}_\varPhi \) refines is resource-optimal, and the witnessing resource-optimal approximate monitor that splits an equivalence class of the specification.

Full size image

3.2 Structure of Resource-Optimal Prompt Monitors

Regardless of the uniqueness, one can ask whether making \({\sim _{\varPhi }}\) coarser always yields a resource-optimal approximate monitor. Here, we answer this question negatively. In particular, Fig. 3 shows on the left a specification \(\varPhi \) and on the right a resource-optimal (1, 0)-monitor \(\mathcal {M}= ({\sim }, \gamma )\) for \(\varPhi \) with \(ab \not \sim ba\), although \(ab \sim ^*_{\varPhi } ba\).

Proposition 14

There exists a (1, 0)-monitor \(\mathcal {M}= ({\sim }, \gamma )\) for some specification \(\varPhi \) such that for every other (1, 0)-monitor \(\mathcal {M}' = ({\sim '}, \gamma ')\) we have that \({\sim _\varPhi } \subseteq {\sim '}\) implies \(\textbf{r}(\mathcal {M}) \ll \textbf{r}(\mathcal {M}')\).

We established that the structure of the exact-value monitor does not necessarily provide insights into finding a resource-optimal approximate monitor. In fact, as we demonstrate in Fig. 4, there exist a specification such that its resource-optimal (1, 1)-monitor \(\mathcal {M}\) never minimizes the resource use \(\textbf{r}_i(\mathcal {M})\).

Proposition 15

There exists a specification \(\varPhi \) admitting a (1, 1)-monitor \(\mathcal {M}=({\sim }, \gamma )\) such that for all equivalence relations \(\approx \) over \(\varSigma ^*\) and \(n\in \mathbb {N}\) we have that \(|\varSigma ^{\le n}/{\sim }|\) is strictly greater than

$$ \min \bigg \{|\varSigma ^{\le n}/{\approx }\; \Big | \; \forall s_1, s_2 \in \varSigma ^{\le n}: s_1\approx s_2\Rightarrow \Big . \bigwedge \begin{array}{l} \forall r\in \varSigma ^*: s_1r\approx s_2r \\ |\varPhi (s_1)-\varPhi (s_2)|\le 1 \end{array}\bigg \}.$$

Proof

Let \(\varPhi = (\pi , \limsup )\) be a specification from \(\varSigma = \{a,b\}\) to \(\mathbb {N}\) where \(\pi \) is defined as follows.

$$\begin{aligned} \pi :s \mapsto {\left\{ \begin{array}{ll} 8 |s| &{} \text {if }s \in b^* \\ 8 |s| - 16k + 4 &{} \text {if }s \in (b^+ a^+)^k\text { for some }k \ge 1 \\ 8 |s| - 16k + 2 &{} \text {if }s \in (b^+ a^+)^k b^+\text { for some }k \ge 1 \\ 8 |s| - 2 &{} \text {if }s \in a^+ \\ 8 |s| - 16k + 10 &{} \text {if }s \in (a^+ b^+)^k\text { for some }k \ge 1 \\ 8 |s| - 16k - 4 &{} \text {if }s \in (a^+ b^+)^k a^+\text { for some }k \ge 1 \\ \end{array}\right. } \end{aligned}$$

Let \(n \in \mathbb {N}\). The key argument is that it is beneficial to put \(a^n\) and \(b^n\) in the same equivalence class for minimizing \(\textbf{r}_n\) since \(|\varPhi (a^n) - \varPhi (b^n)| = 2\) and since no other trace in \(\varSigma ^{\le n}\) admits a value close to either \(\varPhi (a^n)\) or \(\varPhi (b^n)\). However, once we consider traces of length \(n+1\), we introduce several values close to \(\varPhi (a^n)\) as well as \(\varPhi (b^n)\), but not both at the same time. Therefore, to minimize the resource use \(\textbf{r}_{n+1}\) while maintaining the prompt-error bound of 1, it becomes beneficial to put \(a^n\) and \(b^n\) in distinct equivalence classes.    \(\square \)

Fig. 4.
figure 4

A resource-optimal (1,1)-monitor for the specification \(\varPhi \) of Proposition 15 that never minimizes its step-wise resource use \(\textbf{r}_n\) (black). Attempting to minimize \(\textbf{r}_n\) at each step n results in taking \(a^n\) and \(b^n\) as equivalent, but breaking the equivalence at step \(n+1\) as the prompt-error bound would be violated otherwise (gray).

Full size image

3.3 Unbounded Precision-Resource Trade-Offs for Prompt Monitors

In this subsection, we exhibit specifications admitting an infinite sequence of monitors that trade precision and resource use. First, we investigate the maximal response-time specification by demonstrating how a monitor can save more and more resources by increasing both its prompt- and limit-error.

Example 16

Let \(\varSigma = \{\texttt {req}, \texttt {ack}, \texttt {other}\}\) and consider the usual LTL response specification \(P = \Box (\texttt {req}\rightarrow \Diamond \texttt {ack})\). We define \(\textsf{CurResp}(s) = 0\) if \(s\in P\), and \(\textsf{CurResp}(s) = |s| - |r|\) otherwise, where \(r \prec s\) is the longest prefix with \(r \in P\). Now, let \(\textsf{MaxResp}(s) = \sup _{r \preceq s} \textsf{CurResp}(r)\) and define \(\varPhi _{\textsf{MR}} = (\textsf{MaxResp}, \lim )\), which we call the maximal response-time specification. Note that \(\textsf{CurResp}\) outputs the current response-time for a finite trace, and \(\textsf{MaxResp}\) outputs the maximum response-time so far.

Consider the monitor \(\mathcal {M}= ({\sim }, \gamma )\) that counts the response time when there is an open \(\texttt {req}\), but only stores an approximation of the maximum when an \(\texttt {ack}\) occurs. More explicitly, let \({\sim }\) and \(\gamma \) be such that we have the following: \(\mathcal {M}(s) = 5k+2\) if \(s\in P\), where \(k \in \mathbb {N}\) satisfies \(5k \le \textsf{MaxResp}(s) < 5(k+1)\); and \(\mathcal {M}(s) = \max \{\mathcal {M}(r), \mathsf {CurResp(s)}\}\) otherwise, where \(r \prec s\) is the longest prefix with \(r \in P\). We claim that \(\mathcal {M}\) is a (2, 2)-monitor for \(\varPhi _{\textsf{MR}}\). First, observe that whenever there is no pending request, i.e., \(s\in P\), the monitor has a prompt-error of at most 2 by construction. Indeed, \(\textsf{MaxResp}(s) \in \{5k + i \;|\;i \in \{0,1,2,3,4\}\}\). In the case of a pending request, i.e., \(s\notin P\), there is a prompt-error only when the monitor’s approximation of the maximum-so-far is not replaced by the current response time. Again, by construction, we can bound this error by 2. Intuitively, \(\mathcal {M}\) achieves this approximation by merging in \({\sim }\) some equivalence classes of \(\sim ^*_{\varPhi _{\textsf{MR}}}\) where there are no pending requests. One can thus verify that \(\textbf{r}(\mathcal {M}) < \textbf{r}(\mathcal {M}_{\varPhi _{\textsf{MR}}})\).

The construction described in Example 16 can be generalized to identify a precision-resource trade-off with an infinite hierarchy of approximate monitors.

Theorem 17

For all \(\delta \in \mathbb {N}\), there exists a \((\delta ,\delta )\)-monitor \(\mathcal {M}_\delta \) for the maximal response-time specification. Furthermore, \(\textbf{r}(\mathcal {M}_i) < \textbf{r}(\mathcal {M}_j)\) for all \(i > j\), and \(\mathcal {M}_0\) is the exact-value monitor.

Proof

Let \(\varPhi _{\textsf{MR}} = (\textsf{MaxResp}, \lim )\) be the maximal response-time specification as introduced in Example 16. Let \(\delta \in \mathbb {N}\) and \(s \in \varSigma ^*\). If s does not have a pending request, we define \(\mathcal {M}_\delta (s) = k(2\delta + 1) + \delta \) where \(k \in \mathbb {N}\) satisfies \(k(2\delta + 1) \le \textsf{MaxResp}(s) < (k+1)(2\delta +1)\). Otherwise, if s has a pending request, we define \(\mathcal {M}_\delta (s) =\max \{\mathcal {M}_\delta (r), \mathsf {CurResp(s)}\}\) where \(r \prec s\) is the longest prefix with no pending request. We construct the \((\delta ,\delta )\)-monitor \(\mathcal {M}_\delta \) for \(\varPhi _{\textsf{MR}}\) as in Example 16. In particular, \(\mathcal {M}_0\) is the exact-value monitor. Indeed, \(\delta =0\) implies \(\mathcal {M}_\delta (s)= k = \textsf{MaxResp}(s)\) when s does not have a pending request, and otherwise \(\mathcal {M}_\delta (s) = \sup _{r \preceq s} \mathsf {CurResp(r)} = \textsf{MaxResp}(s)\) by definition. For all \(i>j\), the monitor \(\mathcal {M}_i\) partitions the traces with no pending requests into sets of cardinality \(2i+1\) while \(\mathcal {M}_j\) does so using sets of cardinality \(2j+1\). Then, the equivalence relation used by \(\mathcal {M}_i\) is coarser than that of \(\mathcal {M}_j\), and thus \(\textbf{r}(\mathcal {M}_i) < \textbf{r}(\mathcal {M}_j)\).    \(\square \)

Note that, except \(\mathcal {M}_0\), the monitors given by Theorem 17 have non-zero limit-error. We explore in Sect. 4 the specifications for which having fewer resources than the exact-value monitor forces a non-zero limit-error. Moreover, we show in Example 25 that the maximal response-time is one of these specifications.

Next, we investigate the server/client specification by demonstrating how a monitor can be more and more precise by increasing its resource use.

Example 18

Consider a server that receives requests and issues acknowledgments. The number of simultaneous requests the system can handle is determined at runtime through a preprocessing computation. We describe a specification that, at its core, requires that every request is acknowledged and the server never has more open requests than it can handle. In particular, until the server is turned off, the specification assigns a value to each finite trace, denoting the likelihood and criticality of a potential immediate violation.

Let \(\varSigma = \{\texttt {req}, \texttt {ack}, \texttt {other}, \texttt {off}\}\) be an alphabet, \(\lambda \in (0,1)\) be a discount factor, and \(\varLambda > 0\) be an integer denoting the request threshold. For every \(s \in \varSigma ^*\) we denote by \(\textsf{NumReq}(s)\) the number of pending requests in s. We define the server/client specification \(\varPhi _{\textsf{SC}} = (\pi , \lim )\) where \(\pi \) is defined as follows.

  • \(\pi (s) = 0\) if s contains an occurrence of \(\texttt {off}\),

  • \(\pi (s) = \textsf{NumReq}(s) \lambda ^{|s|}\) if \(\textsf{NumReq}(r) \le \varLambda \) for all \(r \preceq s\), and otherwise

  • \(\pi (s) = \textsf{NumReq}(r) \lambda ^{|r|}\) where \(r \preceq s\) is the shortest with \(\textsf{NumReq}(r) > \varLambda \).

Theorem 19

For every positive integer \(\varLambda \) and real number \(0 < \delta \le \varLambda \), there exists a \((\delta ,\delta )\)-monitor \(\mathcal {M}_\delta \) for the server/client specification \(\varPhi _{\textsf{SC}}\). Furthermore, \(\mathcal {M}_\delta \) uses finitely many resources.

Proof

Let \(\varLambda \) and \(\delta \) be as above, and consider the set X we define as follows: \(X = \{s \in \varSigma ^* \;|\;\sup _{r_1\in \varSigma ^*}\{\pi (sr_1)\} - \inf _{r_2\in \varSigma ^*}\{\pi (sr_2)\} \ge \delta \}\). Note that X is finite. On the one hand, only a finite number of prefixes of a trace admitting an occurrence of \(\texttt {off}\) can belong to X since \(\delta >0\) and by definition of \(\varPhi _{\textsf{SC}}\). On the other hand, only a finite number of prefixes of a trace in which no \(\texttt {off}\) occurs can belong to X since the discounting forces the value of \(\varPhi _{\textsf{SC}}\) to converge to 0. We construct \(\mathcal {M}_\delta \) such that, if the trace belongs to X, it outputs the value given by the specification, otherwise it outputs the value of the shortest prefix that does not belong to X. In other words, \(\mathcal {M}_\delta \) does not distinguish traces with the same prefix not belonging to X and thus admits at most 2|X| equivalence classes.    \(\square \)

4 Approximate Limit Monitoring

In contrast to Sect. 3 where we tackle the limit monitoring problem indirectly with a bounded prompt-error, here we bound the limit-error directly and allow arbitrary prompt-error.

Example 20

Let \(\varPhi = (\pi , \liminf )\) be a specification over \(\varSigma = \{\texttt {safe}, \texttt {danger}, \texttt {off}\}\) such that \(\pi (s) = 2^{|r|}\) if s does not contain \(\texttt {off}\), where r is the longest suffix of s of the form \(\texttt {safe}^*\), and \(\pi (s) = |s|_{\texttt {danger}}\) otherwise. Intuitively, \(\varPhi \) assigns each trace a confidence value while the system is on and how many times the system was in danger otherwise. We describe an approximate monitor with unbounded prompt-error and bounded but non-zero limit-error.

Let \({\sim }\) be a right-monotonic equivalence relation and \(\gamma \) an output function such that \(\mathcal {M}= ({\sim }, \gamma )\) satisfies the following: \(\mathcal {M}(s) = \infty \) when s has no \(\texttt {off}\) and ends with \(\texttt {safe}\), \(\mathcal {M}(s) = 0\) when s has no \(\texttt {off}\) and ends with \(\texttt {danger}\), and \(\mathcal {M}(s) = 9k+4\) otherwise, where \(k \in \mathbb {N}\) satisfies \(9k \le |s|_{\texttt {danger}} < 9(k+1)\). Notice that the monitor partitions \(\mathbb {N}\) into intervals and takes traces with a “close enough” number of \(\texttt {danger}\)’s equivalent – as in Example 16. It is easy to see that \(\mathcal {M}\) is a \((\infty , 4)\)-monitor for \(\varPhi \).

At its core, the limit-error threshold of a monitor is a theoretical guarantee since we cannot compute arbitrary limit-measures at runtime. Then, as a starting point, we insist that the monitor has zero limit-error, which is a reasonable requirement given that we allow unbounded prompt-error. In this case, the monitoring is still potentially approximate since we allow any error on finite traces. To talk about specifications for which saving resources by allowing prompt-error is not possible, we define the following notion.

Definition 21 (resource-intensive limit behavior)

A specification \(\varPhi \) has resource-intensive limit behavior iff its exact-value monitor \(\mathcal {M}_\varPhi \) is a resource-optimal \((\delta ,0)\)-monitor for any \(\delta \ge 0\).

First, we identify a sufficient condition for a specification to be resource-intensive limit behavior. Then, we present reversible specifications and show a subclass of them that satisfy our condition.

4.1 Specifications with Resource-Intensive Limit Behavior

Let \(\varPhi = (\pi , \ell )\) be a specification and recall the equivalence \({\sim }^*_{\varPhi }\) that, for every \(s_1,s_2 \in \varSigma ^*\), is defined as \(s_1 \sim ^*_\varPhi s_2\) iff \(\pi (s_1 r) = \pi (s_2 r)\) holds for all \(r \in \varSigma ^*\). To investigate the limit behavior of a specification, we define the following equivalence relation: for every \(s_1,s_2 \in \varSigma ^*\) we have \(s_1 \sim ^\omega _\varPhi s_2\) iff \(\ell (\pi (s_1 f)) = \ell (\pi (s_2 f))\) holds for all \(f \in \varSigma ^\omega \). Intuitively, traces with indistinguishable limit behavior are equivalent according to this relation. As a direct consequence of Fact 11, the following holds.

Fact 22

For every specification \(\varPhi \), we have that \({\sim }^*_\varPhi \subseteq {\sim }^\omega _\varPhi \).

However, the converse does not necessarily hold, as we demonstrate with Example 23 below. We will show later that, when it holds, the specification has resource-intensive limit behavior.

Example 23

Recall the discounted response specification \(\varPhi _{\textsf{DR}}\) in Example 2, and that for all \(s,r \in \varSigma ^*\), we have \(s \sim ^*_{\varPhi _{\textsf{DR}}} r\) iff either (i) both traces have no pending \(\texttt {req}\) or (ii) both have a \(\texttt {req}\) pending for the same number of steps.

Let \(s,r \in \varSigma ^*\). We claim \(s \sim ^\omega _{\varPhi _{\textsf{DR}}} r\) iff either both traces have a pending request or both do not. Indeed, if s has a pending request and r does not, then we have \(\varPhi (s.\texttt {other}^\omega ) = 0\) but \(\varPhi (r.\texttt {other}^\omega ) = 1\). For the other direction, simply observe that if \(s \sim ^\omega _{\varPhi _{\textsf{DR}}} r\) then \(\varPhi (s.\texttt {other}^\omega ) = \varPhi (r.\texttt {other}^\omega )\), but the equality does not hold if s has a pending request and r does not (or vice versa). Having these characterizations at hand, we immediately observe that \(s \sim ^*_{\varPhi _{\textsf{DR}}} r\) implies \(s \sim ^\omega _{\varPhi _{\textsf{DR}}} r\).

Notice that the approximate monitor \(\mathcal {M}\) for \(\varPhi _{\textsf{DR}}\) we constructed in Example 5 follows exactly the limit behavior of the specification. We were able to take advantage of the fact that \({\sim ^\omega _{\varPhi _{\textsf{DR}}}}\) is coarser than \({\sim ^*_{\varPhi _{\textsf{DR}}}}\) and design \(\mathcal {M}\) such that it saves resources by allowing some prompt-error but no limit-error. We generalize this observation by showing that we could not have designed such a monitor if these equivalences had overlapped.

Theorem 24

Let \(\varPhi \) be a specification. If \({\sim }^*_\varPhi = {\sim }^\omega _\varPhi \) then \(\varPhi \) has resource-intensive limit behavior.

Proof

Let \(\mathcal {M}= ({\sim }, \gamma )\) be a resource-optimal \((\delta ,0)\)-monitor for \(\varPhi \). Suppose towards contradiction that \({\sim }^*_\varPhi = {\sim }^\omega _\varPhi \) and \(\mathcal {M}_\varPhi \) is not resource-optimal for \(\varPhi \). In particular \({\sim } \ne {\sim }_\varPhi ^*\). Since the limit-error threshold is 0, we get \({\sim } \subseteq {\sim _{\varPhi }^*}\) by the following.

$$\begin{aligned} s_1 \sim s_2&\implies \forall f\in \varSigma ^\omega ,\, \ell (\gamma ([s_1f])) = \ell (\gamma ([s_2f]))&\quad \text {(right-monotonicity)}\\&\iff \forall f\in \varSigma ^\omega ,\, \ell (\pi (s_1f)) = \ell (\pi (s_2f))&\quad \text {(limit-error 0)}\\&\iff s_1 \sim _\varPhi ^\omega s_2&\quad \text {(definition)}\\&\iff s_1 \sim _\varPhi ^* s_2&\quad \text {(hypothesis)} \end{aligned}$$

The contradiction is then raised by Proposition 10 implying that \({\sim } = {\sim _\varPhi ^*}\).    \(\square \)

As demonstrated in Example 5 and discussed above, the discounted response specification does not display resource-intensive limit behavior. We give below two examples of specifications with resource-intensive limit behavior. Let us start with the maximal response-time specification.

Example 25

Consider the maximal response-time specification \(\varPhi _{\textsf{MR}} = (\textsf{MaxResp}, \lim )\) from Example 16. We argue that \(\sim ^*_{\varPhi _{\textsf{MR}}}\) and \(\sim ^\omega _{\varPhi _{\textsf{MR}}}\) overlap.

Suppose towards contradiction that there exist \(s,r \in \varSigma ^*\) such that \(s \sim ^\omega _{\varPhi _{\textsf{MR}}} r\) and \(s \not \sim ^*_{\varPhi _{\textsf{MR}}} r\). Then, there is \(t \in \varSigma ^*\) with \(\varPhi _{\textsf{MR}}(st) \ne \varPhi _{\textsf{MR}}(rt)\). If at least one of st or rt has no pending request, take the continuation \(\texttt {other}^\omega \) to reach a contradiction to \(s \sim ^\omega _{\varPhi _{\textsf{MR}}} r\). Otherwise, if in both st and rt the current response time is smaller than the maximum among granted requests, then the continuation \(\texttt {ack}^\omega \) yields a contradiction. The same continuation covers the case when both current response times are greater. Finally, assume w.l.o.g. that the current response time is smaller than the maximum among granted requests in st and greater in rt. In this case, \(\texttt {ack}^\omega \) yields a contradiction again because their outputs stay the same as \(\varPhi _{\textsf{MR}}(st)\) and \(\varPhi _{\textsf{MR}}(rt)\), respectively. Therefore, we have \(s \sim ^*_{\varPhi _{\textsf{MR}}} r\), and thus \(\sim ^*_{\varPhi _{\textsf{MR}}}\) and \(\sim ^\omega _{\varPhi _{\textsf{MR}}}\) overlap.

Next, we describe the average response-time specification and argue that it displays resource-intensive limit behavior.

Example 26

Let \(\varSigma = \{\texttt {req}, \texttt {ack}, \texttt {other}\}\) and consider the usual LTL response specification \(P = \Box (\texttt {req}\rightarrow \Diamond \texttt {ack})\). For \(s \in \varSigma ^*\), we denote by \(\textsf{RespTime}(s)\) the total number of letters between the matching \(\texttt {req}\)-\(\texttt {ack}\) pairs in s, and by \(\textsf{NumReq}(s)\) the number of valid \(\texttt {req}\)’s in s. For all \(s \in \varSigma ^*\), we fix \(p(s) = 1\) if \(s \in P\), and \(p(s) = 0\) otherwise. Then, we define \(\textsf{RespTime}(s) = \sum _{r \preceq s} 1 - p(r) \) and \(\textsf{NumReq}(s) = |P_s|\) where \(P_s = \{r \preceq s \;|\;\exists t \in \varSigma ^* ,\, r = t.\texttt {req}\wedge p(t) = 1 \}\) is the set of valid requests in s. We define the average response-time specification as \(\varPhi _{\textsf{AR}} = (\textsf{AvgResp}, \liminf )\) where we let \(\textsf{AvgResp}(s) = \frac{\textsf{RespTime}(s)}{\textsf{NumReq}(s)}\) for all \(s \in \varSigma ^*\).

We claim that \(\sim ^*_{\varPhi _{\textsf{AR}}}\) and \(\sim ^\omega _{\varPhi _{\textsf{AR}}}\) overlap. To show this, one can proceed similarly as in Example 25. The cases with no pending requests are similar. When both traces have a pending request and their output values differ, extend both with \(\texttt {ack}^\omega \) to get a contradiction.

4.2 Reversible Specifications

The reversible subclass of specifications enjoys the ability to move between computation steps forward and backward deterministically. Such specifications received particular interest in the literature since they can be implemented on hardware without energy dissipation [42, 52]. Since it imitates the specification, the exact-value monitor of a reversible specification can roll back its computation, if allowed, without needing additional memory. From an automata-theoretic perspective, reversibility can be seen as the automaton being both forward and backward deterministic. Algebraically, this is captured by the syntactic monoid being a group.

Definition 27 (reversible specification)

A specification \(\varPhi \) is reversible iff \(({\varSigma ^*}/{\sim }^*_\varPhi , \cdot , \varepsilon )\) is a group.

First, we describe the average ping specification – a variant of the average response-time specification where a single \(\texttt {ping}\) event captures \(\texttt {req}\) and \(\texttt {ack}\) events, and time proceeds through clock \(\texttt {tick}\) events. We then show that this specification is reversible.

Example 28

Let \(\varSigma = \{\texttt {ping}, \texttt {tick}, \texttt {other}\}\). Let \(\textsf{ValidTick}(s) = |s|_{\texttt {tick}} - |r|_{\texttt {tick}}\) where \(r \preceq s\) is the longest prefix with no \(\texttt {ping}\), and let \(\textsf{NumPing}(s) = |s|_{\texttt {ping}}\). The average ping specification is defined as \(\varPhi _{\textsf{AP}} = (\textsf{AvgPing}, \liminf )\) where, for all \(s \in \varSigma ^*\), we let \(\textsf{AvgPing}(s) = \frac{\textsf{ValidTick}(s)}{\textsf{NumPing}(s)}\) if \(\textsf{NumPing}(s) > 0\); and \(\textsf{AvgPing}(s) = -1\) otherwise.

We argue that this specification is reversible. To see why, first observe for all \(s,r \in \varSigma ^*\) that we have \(s \sim ^*_{\varPhi _{\textsf{AP}}} r\) iff (i) \(\textsf{NumPing}(s) = \textsf{NumPing}(r)\) and (ii) \(\textsf{ValidTick}(s) = \textsf{ValidTick}(r)\). We particularly show for every \(s,r,t \in \varSigma ^*\) that if \(s \not \sim ^*_{\varPhi _{\textsf{AP}}} r\) then \(st \not \sim ^*_{\varPhi _{\textsf{AP}}} rt\), therefore \({\sim ^*_{\varPhi _{\textsf{AP}}}}\) yields a group. Let \(s,r \in \varSigma ^*\) be such that \(s \not \sim ^*_{\varPhi _{\textsf{AP}}} r\) and let \(t \in \varSigma ^*\) be arbitrary. Suppose the condition (i) above does not hold. Since the \(\textsf{NumPing}\) values increase monotonically with every \(\texttt {ping}\), we get \(\textsf{NumPing}(st) - \textsf{NumPing}(rt) = \textsf{NumPing}(s) - \textsf{NumPing}(r)\), which is non-zero by supposition. If (ii) does not hold, it does not hold for st and rt either by a similar reasoning. Hence we have \(st \not \sim ^*_{\varPhi _{\textsf{AP}}} rt\).

Intuitively, we can backtrack the information on these functions: The value of \(\textsf{NumPing}\) is decremented with each preceding \(\texttt {ping}\), while \(\textsf{ValidTick}\) is decremented with each preceding \(\texttt {tick}\) until it hits 0. It means that \({\sim }^*_{\varPhi _{\textsf{AP}}}\) can be seen as an automaton that is both forward and backward deterministic.

We identify below a well-behaved subclass of reversible specifications with resource-intensive limit behavior.

Theorem 29

Let \(\varPhi \) be a reversible specification. If for every \(s,r \in \varSigma ^*\) with \(s \sim ^\omega _\varPhi r\) there exists \(t \in \varSigma ^*\) with \(st \sim ^*_\varPhi rt\), then \(\varPhi \) has resource-intensive limit behavior.

Proof

We show that the reversibility of \(\varPhi \), together with the above assumption, implies \({\sim }^*_\varPhi = {\sim }^\omega _\varPhi \). Note that the inclusion \({\sim }^*_\varPhi \subseteq {\sim }^\omega _\varPhi \) always holds as stated by Fact 22. Assuming \(({\varSigma ^*}/{\sim }^*_\varPhi , \cdot , \varepsilon )\) is a group, we have \(s_1r \sim ^*_\varPhi s_2r \Rightarrow s_1 \sim ^*_\varPhi s_2\) for all \(s_1, s_2, r\in \varSigma ^*\). The inclusion \({\sim }^\omega _\varPhi \subseteq {\sim }^*_\varPhi \) holds since having \(s_1 \not \sim ^*_\varPhi s_2\) implies for all \(r\in \varSigma ^*\) that \(s_1r \not \sim ^*_\varPhi s_2r\), which in turn implies \(s_1 \not \sim ^\omega _\varPhi s_2\) by our initial assumption. Finally, by Theorem 24, we obtain that \(\varPhi \) has resource-intensive limit behavior.    \(\square \)

Recall the average ping specification from Example 28. It is reversible, as discussed earlier, and satisfies the condition in Theorem 29, therefore it has resource-intensive limit behavior. Finally, we present the maximal ping – a similarly simple variant of the maximal response-time specification. We demonstrate that this specification is not reversible, although it has resource-intensive limit behavior.

Example 30

Let \(\varSigma = \{\texttt {ping}, \texttt {other}\}\) and consider the boolean specification \(P =~\Box \Diamond \texttt {ping}\). Let \(\textsf{CurPing}(s)\) and \(\textsf{MaxPing}(s)\) be defined similarly as for the maximal response-time specification in Example 16. We fix \(\varPhi _{\textsf{MP}} = (\textsf{MaxPing}, \lim )\) which we call the maximal ping specification. Consider \(s = \texttt {ping}. \texttt {other}\) and \(r = \texttt {ping}. \texttt {other}. \texttt {other}\). While \(s \not \sim ^*_{\varPhi _{\textsf{MP}}} r\), we have \(s r \sim ^*_{\varPhi _{\textsf{MP}}} r r\), therefore \({\sim ^*_{\varPhi _{\textsf{MP}}}}\) does not yield a group. Intuitively, this is because we cannot backtrack the information on the running maximum. However, similarly as for the maximal-response time specification in Example 16, one can verify that \({\sim }^*_{\varPhi _{\textsf{MP}}} = {\sim }^\omega _{\varPhi _{\textsf{MP}}}\).

Note that a notion of reversibility exists for abstract monitors as well: A monitor \(\mathcal {M}=~({\sim }, \gamma )\) where \(\sim \) yields a group enjoys reversibility. In particular, this ability allows the monitor to return to a previous computation step without using additional resources and thus consider a different trace suffix.

5 Conclusion and Future Work

We formalize a framework that supports reasoning about precision-resource trade-offs for the approximate and exact monitoring of quantitative specifications. Unlike previous results, which analyze trade-offs for specific machine models such as register monitors [32, 37], the framework presented in this paper studies for the first time an abstract notion of monitors, independent of the representation model, and separates the monitor errors on finite traces from those at the limit. These innovations allow us to design and study monitors that keep the focus on the resources needed for the approximate monitoring of quantitative specifications with a given precision. We provide several examples of when approximate monitoring can save resources and investigate when it fails to achieve this goal.

An expected future work is to provide a procedure for constructing a concrete (exact or approximate) monitor from an abstract description. Monitors having finitely many equivalence classes can be naturally mapped to finite-state automata. For a monitor with infinitely many equivalence classes, the model must be an infinite-state transition system. Yet, there are different levels of infinite state space. It can be generated, for example, by a finite collection of registers [32] or by a pushdown system [28]. Even when two abstract monitors are mapped to register automata with the same number of registers, they may differ in the type of operations used or the run-time needed per observation. It is also worth emphasizing that saving a single register may save infinitely many resources. Our current results do not provide such performance, so it is a natural future direction. To this end, we can consider alternative approaches to evaluate a monitor based on the number of violations of the error-threshold.

Another direction is on the relevance of resources through time. Our notion of resource use covers the number of equivalence classes added at time n, but an assumption that the monitor can release resources would trigger more possibilities. We can extend our framework to dynamic abstract monitors in a way that is related to existing works on dynamic programming for model checking [53]. Intuitively, a dynamic abstract monitor keeps track of the equivalence classes that can be reused in the future and prunes all the others to reduce resource use.