## 6 Exact Monitoring under Imperfect Information Given Uncertain Linear Dynamics  
Additional inferences about the correlation between systems states at different time instants, and consequently additional evidence refining monitoring verdicts, are available when we have access to a model of system dynamics. Beyond refined arguments concerning feasible ground-truth value ranges within the error margins, such a model also allows to bridge gaps in sensor information, like time instants missing in a time series or references to unobservable signals. As a motivating example consider the time series of inexact measurements depicted in Figure 2, where  
* \(t\) denotes time of measurement,
* \(x\) and \(y\) constitute the (mostly unobservable) systems state, which is subject to uncertain linear dynamics \(x^{\prime}=\frac{x}{\sqrt{2}}-\frac{y}{\sqrt{2}}\) and \(y^{\prime}=\frac{x}{\sqrt{2}}+\frac{y}{\sqrt{2}}\pm 0.1\),
* blue (green, resp.) crosses denote the unknown actual values of \(x\) (\(y\), resp.) along a system evolution,
* green dots denote two inexact measurements taken on \(y\) at time instants 1 and 5, which are the only measurements available for the system,
* perpendicular intervals of width \(\pm 1\) denote the error margins of these measurements, consisting of \(\pm 0.5\) independent per-measurement error and \(\pm 0.5\) unknown constant sensor offset,
* the red area indicates critical values for \(y\), namely \(y<0.2\),  
Figure 2: Model-based monitoring of temporal conditions under interval-type uncertainty and partial observation. * the monitoring condition to be decided at \(t=5\) for \(t^{\prime}=t-\text{duration}(\phi)=t-4=1\) is \(\phi=\mathbf{G}_{\leq 4}y\geq 0.2\), i.e., to decide whether the red area is avoided throughout time instants \(1,\ldots,5\). Evaluation of the monitoring condition over the uncertainty intervals remains inconclusive due to both the overlap of the given uncertainty intervals at times \(1\) and \(5\) with the red area and the lack of any information for the other times. Note that even most precise state estimation, while being able to deduce intervals for the possible ground truth values of \(y\) at time instants \(2\) to \(4\), cannot narrow down the intervals for \(y\) at time instants \(1\) and \(5\). Any monitoring approach based on a sequence of best-in-class state estimation and subsequent evaluation by a monitor thus is bound to remain inconclusive. Holistic treatment of the STL monitoring condition by affine arithmetic, however, can decide violation of the monitoring condition \(\phi\): the conjunction of the affine form representations of the relation between measurements and ground truth values with the equations for the system dynamics and with the monitoring condition constitutes an unsatisfiable linear constraint system (shown later in full detail). The formal construction relies on the encoding from the previous section and conjoins it with the equations characterizing the system dynamics. It is generated as follows:  
1. Identical to steps \(1\) to \(5\) from Section \(5\), with the slight variation that constants representing measurements (step \(1\)), slack variables for random noise (step \(3\)) and constraints \(v\_i+\text{o}\_v+\text{e}\_v\_i=\text{m}\_v\_i\) encoding consistency with measurements (second half of step \(4\)) are only generated for time instants where measurements are available. 2. For each \(v\in V\) and each \(i\in\{t-\text{duration}(\phi),\ldots,t-1\}\), declare a real variable u_v_i and generate the linear constraints \[ \begin{array}{ll}&\text{v}\_(i+1)=c_{1}\text{x}\_i+c_{2}\text{y}\_i+\ldots+c _{n}\text{z}\_i+c+\text{u}\_v\_i\\ \wedge&\text{u}\_v\_i\geq-\gamma\\ \wedge&\text{u}\_v\_i\leq\gamma\end{array} \] when the dynamics of \(v\) is given by the uncertain equation \(v^{\prime}=c_{1}x+c_{2}y+\ldots+c_{n}z+c\pm\gamma\). The uncertain offset u_v_i can be dropped when the dynamic equation is certain. 3.