## 5 Exact Monitoring under Imperfect Information: The Model-Free Case  
As a motivating example consider the time series of inexact measurements depicted in Figure 1, where  
* \(t\) denotes time instant of the measurement (for simplicity considered to be exactly known and to coincide with the time of its associated ground truth values--both simplifications can be relaxed),
* \(x\) is the unknown ground-truth value of the physical quantity \(x\) under observation,
* black dots denote inexact measurements \(m_{i}\) taken at time instances \(i=1\ldots 14\),
* perpendicular intervals attached to measurements indicate error margins: measurements may deviate by \(\pm 1\) from ground truth; \(\pm 0.5\) thereof can be attributed to an unknown constant sensor offset, leaving another \(\pm 0.5\) to random measurement noise,
* the red areas, corresponding to the state predicate \(x<2\lor x>5\), indicate critical values for \(x\), e.g., a geo-fencing condition not to be violated,the monitoring condition \(\phi=\mathbf{G}_{\leq 12}(x\geq 2\wedge x\leq 5)\) is to be decided at time \(t=13\) for time \(t^{\prime}=t-\text{duration}(\phi)=t-12=1\), i.e., whether \(x\in[2,5]\), avoiding the red range, holds throughout the depicted time interval \(I\). The uncertainty intervals depicted are tight insofar that, first, their width is \(\pm 1\) and thus coincides with the sum of the two errors sensor offset and random noise and, second, that in the absence of any known model of the system dynamics, no reach-set propagation across time instances is possible. Evaluation of \(\phi\) based on interval arithmetic [12] therefore remains inconclusive, given that some uncertainty intervals (namely the ones at times \(t=3\) and \(t=12\)) overlap with the red areas, yet none falls completely into this forbidden range. As the intervals depicted represent the sharpest possible state estimates w.r.t. the metric error model discussed here, monitoring approaches based on first applying best-possible state estimation and subsequently evaluation of the monitoring condition are equally prone to remaining inconclusive. Using affine arithmetic [13] and SAT modulo theory solving over linear arithmetic (SMT-LA) [14], we will, however, be able to decide that \(\phi\) is violated at time \(t^{\prime}=1\). The core argument in the detailed, general construction to follow is that we can represent the possible ground truth values \(x_{i}=\tau(i)(x)\) relating to the measurements \(m_{i}\) as \(x_{i}+o+e_{i}=m_{i}\) with \(o\in[-0.5,0.5]\) representing the unknown, yet bounded sensor offset and \(e_{i}\in[-0.5,0.5]\) for \(i=1\ldots 13\) representing per-sample independent error. Now observe that \(m_{3}=5.7\wedge m_{12}=2.6\wedge x_{3}+o+e_{3}=m_{3}\wedge x_{12}+o+e_{12}=m_{ 12}\wedge o,e_{3},e_{12}\in[-0.5,0.5]\wedge x_{3},x_{12}\in[2,5]\) is unsatisfiable. The latter can be decided with SMT-LA solving. The unsatisfiability proves that at least one of \(x_{3}\), \(x_{12}\) definitely falls into the red range due to the dependence introduced by the sensor offset. For the full construction let us assume that  
1. \(\phi\) mentions the state variables \(V\subset Var\);
2. for each \(v\in V\) we are having a sensor with maximal offset \(e_{v}\geq 0\) and maximum random per-sample error \(\delta_{v}\geq 0\); (We will later relax the assumption that all variables in \(\phi\) be directly observable through a sensor. To be meaningful, such partial observation does, however, require a system model permitting to infer information over unobservable variables, which is subject of the next section.) 3. that these sensors have provided measurements \(m_{v}(i)\) for each variable \(v\in V\) and each time instant \(i\in\{t-\text{duration}(\phi),\ldots,t\}\). (We will likewise relax the assumption that each time point be observed by the sensors in the section to follow.) We then build a linear constraint system, i.e., a Boolean combination of linear constraints as follows:  
1.