## 4 The Monitoring Problem  
Assume that we want to continuously monitor truth of a safety requirement \(\phi\) stated as a bounded-time STL formula. In reality, we can only do so based on a set \(m_{S_{1}}\) to \(m_{S_{n}}\) of time series of measurements obtained through different sensors \(S_{1}\) to \(S_{n}\). Each of these sensors is inexact, none can predict the future, and even together they provide only partial introspection into the set \(\mathit{Var}\) of signals generated by the system under monitoring. The problem at hand is to, at any time \(t\in\mathbb{N}\), generate as precise as possible verdicts about the truth of the monitoring condition \(\phi\) at time \(t-\text{duration}(\phi)\) given the imprecise measurements provided by the sensor array \(S_{1}\) to \(S_{n}\) up to time \(t\). Doing so requires identifying the full set of ground-truth signals possible given a set of inexact measurements. This, however, coincides with the notion of consistency stated in Definition 3. **Definition 4**. : _Let \(S_{1}\) to \(S_{n}\) be a set of sensors, each qualified by an individual maximum sensor offset \(\varepsilon_{S_{i}}\) and an individual maximum random error \(\delta_{S_{i}}\), which observe (not necessarily different) signals \(\sigma_{S_{i}}\in\mathit{Var}\) at (potentially diverse) time instants \(T_{S_{i}}\subseteq\mathbb{N}\). Let \(t\in\mathbb{N}\) be the current time and \(m_{S_{i}}:T_{S_{i}}\cap\mathbb{N}_{\leq t}\to\mathbb{R}\) be the time series representing measurements obtained by the different sensors \(S_{i}\) up to time \(t\)._  
_The possible ground truth associated to the time series \(m_{S_{1}}\) to \(m_{S_{n}}\) is the set of all trajectories \(\tau\) satisfying \(m_{S_{1}},\dots,m_{S_{n}}\vdash\tau\), i.e., being consistent with all available measurements simultaneously. We signify the set of all possible ground truth trajectories corresponding to a set of measurements \(m_{S_{1}},\dots,m_{S_{n}}\) by_  
\[GT(m_{S_{1}},\dots,m_{S_{n}})=\{\tau:\mathbb{N}\to\Sigma\mid m_{S_{1}},\dots,m_{S_{n}}\vdash\tau\}.\]The monitoring problem now is to characterize the possible ground truth exactly and to determine the possible truth values of the monitoring condition \(\phi\) across the possible ground truth:  
**Definition 5**. : _Let \(\phi\) be a bounded-time STL formula according to the syntax from Definition 1, \(t\in\mathbb{N}\) be the current time, and \(m_{S_{i}}:T_{S_{i}}\cap\mathbb{N}_{\leq t}\to\mathbb{R}\), for \(S_{1}\) to \(S_{n}\), be time series representing measurements obtained by the different sensors \(S_{i}\) up to time \(t\)._  
_Let \(M\) be an algorithm taking as arguments a current time \(t\), a vector of time series \(m_{S_{i}}:T_{S_{i}}\cap\mathbb{N}_{\leq t}\to\mathbb{R}\) and computing a verdict in \(\mathbb{R}^{+}=\mathbb{B}\cup\{\texttt{inconclusive}\}\). In the sequel, we denote termination of \(M\) with verdict \(x\) by \(M(t,m_{S_{1}},\ldots,m_{S_{n}})=x\). We say that \(M\) is sound iff_  
1. \(M(t,m_{S_{1}},\ldots,m_{S_{n}})=\top\) _implies that_ \(\forall\tau\in GT(m_{S_{1}},\ldots,m_{S_{n}}):\tau,t-duration(\phi)\models\phi\) _and_
2. \(M(t,m_{S_{1}},\ldots,m_{S_{n}})=\bot\) _implies that_ \(\forall\tau\in GT(m_{S_{1}},\ldots,m_{S_{n}}):\tau,t-duration(\phi)\models \
eg\phi\) _holds for all_ \(t\) _and_ \(m_{S_{i}}\)_._
3. \(M\) _is_ complete _iff_ \(M\) _terminates on all_ \(t\) _and_ \(m_{S_{i}}\)_._
4. \(M(t,m_{S_{1}},\ldots,m_{S_{n}})=\texttt{inconclusive}\) _implies that_ \(\exists\tau,\tau^{\prime}\in GT(m_{S_{1}},\ldots,m_{S_{n}}):\tau,t-duration( \phi)\models\phi\wedge\tau^{\prime},t-duration(\phi)\models\
eg\phi\) _holds for all_ \(t\) _and_ \(m_{S_{i}}\)_._  
_We call \(M\) exact iff \(M\) is sound, conclusive, and complete._  
A sound monitor thus provides correct verdicts only, but may refuse decisive verdicts by non-termination or by reporting inconclusive. A complete monitor always provides some verdict, including inconclusive. A sound and complete monitor may thus still be uninformative by delivering sound but vacuous inconclusive verdicts.