## 5 Exact Monitoring under Imperfect Information: The Model-Free Case
For each \(v\in V\) and each \(i\in\{t-\text{duration}(\phi),\ldots,t\}\), we declare a constant \[\texttt{m\_v\_i}=m_{v}(i).\]  
Figure 1: Model-free monitoring of temporal conditions under metric interval-type uncertainty. 2. For each \(v\in V\), we declare a variable o_v of type real and generate the bound constraints \[\texttt{o\_v}\geq-\epsilon_{v}\wedge\texttt{o\_v}\leq\epsilon_{v}\] representing the sensor offset for measuring \(v\). 3. For each \(v\in V\) and each \(i\in\{t-\text{duration}(\phi),\ldots,t\}\), we declare a variable e_v_i of type real and generate the bound constraints \[\texttt{e\_v\_i}\geq-\delta_{v}\wedge\texttt{e\_v\_i}\leq\delta_{v}\] representing the per-sample independent error. 4. For each \(v\in V\) and each \(i\in\{t-\text{duration}(\phi),\ldots,t\}\), we declare a variable \(v\_i\) of type real and generate a linear constraint \[v\_i+\texttt{o\_v}+\texttt{e\_v\_i}=\texttt{m\_v\_i}\] representing consistency between measurements and ground truth values as stated in Definition 3. 5. Using standard constructions of SMT-based bounded model checking, we add an SMT-LA encoding for validity of \(\phi\) at time \(t^{\prime}=t-\text{duration}(\phi)\) to the constraint system as follows: * For each subformula \(\psi\) of \(\phi\) and each time instant \(k\in\{t-\text{duration}(\phi),\ldots,t-\text{duration}(\psi)\}\) we add a Boolean variable \(\psi\_k\), * if \(\psi=\top\) then we assert constraints \(\psi\_k\) stating that \(\psi\) is invariantly true for each \(k\in\{t-\text{duration}(\phi),\ldots,t\}\), * if \(\psi=g\geq c\) then we add constraints \(\psi\_k\Leftrightarrow g[\vec{v}\_k/\vec{v}]\geq c\) for each \(k\in\{t-\text{duration}(\phi),\ldots,t\}\), * if \(\psi=\
eg\psi^{\prime}\) then we add \(\psi\_k\Leftrightarrow\
eg\psi^{\prime}\_k\) to the constraint system for each \(k\in\{t-\text{duration}(\phi),\ldots,t-\text{duration}(\psi)\}\), * if \(\psi=\psi^{\prime}\vee\psi^{\prime\prime}\) then we add constraints \(\psi\_k\Leftrightarrow(\psi^{\prime}\_k\vee\psi^{\prime\prime}\_k)\) for each \(k\in\{t-\text{duration}(\phi),\ldots,t-\text{duration}(\psi)\}\), * if \(\psi=\psi^{\prime}\mathbf{U}_{[t_{1},t_{2}]}\psi^{\prime\prime}\) then we add constraints \[\psi\_k\Leftrightarrow(\bigwedge_{i=k}^{k+t_{1}-1}\psi^{\prime}\_i)\wedge \bigvee_{i=k+t_{1}}^{k+t_{2}}\left(\psi^{\prime\prime}\_i\wedge\bigwedge_{j= k+t_{1}}^{i-1}\psi^{\prime}\_j\right)\] for each \(k\in\{t-\text{duration}(\phi),\ldots,t-\text{duration}(\psi)\}\), \(\phi\_t^{\prime}\) consequently is the root variable representing validity of \(\phi\) at time \(t^{\prime}=t-\text{duration}(\phi)\). 6. We finally add one of the two conjuncts (a) \(\
eg\phi\_t^{\prime}\) or (b) \(\phi\_t^{\prime}\) alternatively, where \(t^{\prime}=t-\text{duration}(\phi)\), to the resultant constraint system and check both variants for their satisfiability using an SMT-LA solver. Depending on the results of the two satisfiability checks, we report
* inconclusive if both systems are found to be satisfiable,
* \(\top\) if the system (a) containing \(\
eg\phi\_t^{\prime}\) is unsatisfiable,
* \(\bot\) if the system (b) containing \(\phi\_t^{\prime}\) is unsatisfiable,  
The resulting STL monitoring algorithm is best possible in that it is sound, conclusive, and complete:  
**Lemma 1**. : _The above algorithm \(M\) constitutes an exact monitor in the sense of Definition 5._Proof. : In order to show that \(M\) is exact, we have to prove that it is complete, conclusive, and sound. Completeness is straightforward, as the constraint system generated in steps 1 to 6 is finite. Its generation hence terminates, as do the subsequent satisfiability checks because SMT-LA is decidable.