## 8 Conclusions  
In this article we have shown that the monitoring under uncertain environmental observation of properties expressed in linear-time temporal logic is fundamentally different from state estimation under uncertainty. While accurate state estimation followed by evaluation of the monitoring property provides a sound mechanism, this two-step algorithm may remain unnecessarily inconclusive. We have exposed two sample cases where a direct evaluation of the temporal logic property, for which we gave the formal constructions via a reduction to SAT modulo theory solving over linear arithmetic, yields definite results, whereas the two-step algorithm based on state estimation remains inconclusive. The reason is that durational properties expressed by temporal logic induce rather complex relations between successive values of signals and that these relations overlap and interfere with the cross-measurement relations induced by measurements of dynamically related variables as well as by dependencies between measurements. The single-step reduction exposed in this article encodes both the specification formula to be monitored and the error model for measurements into a common logical representation such that the interaction between these two cross-time-instant relations can be analyzed and exploited for more informed verdicts.  
In the present article, we have analyzed these effects theoretically and on small, prototypic examples, within a setting of non-stochastic, metrically constrained error, where the different types of measurement error are interval-bounded. Future work will address real-life benchmark applications from the air taxi domain and extend the theory to a stochastic setting, where both measurement errors and uncertain system dynamics are described by distributions rather than metric intervals. Furthermore, we will address runtime efficiency by devising structural SMT approaches exploiting the particular problem structure rather than using problem-agnostic general purpose SMT solvers. Where this does not suffice to obtain real-time capabilities suitable for online monitoring, we will reduce computational complexity by appropriate approximation algorithms providing real-time capabilities in settings where the exact reductions and the SAT modulo theory algorithms used herein do not feature sufficient performance.  
A further issue of interest could be the handling of outliers in the measured time series, where tolerance of the monitoring verdict against \(k\in\mathbb{N}\) outliers would constitute a useful relaxation of the monitoring requirement. In such a relaxation, a monitor alarm would be suppressed if, at most, \(k\) measurements can be replaced by (arbitrarily different or bounded-offset) valuations that render the monitoring condition true when combined with the ground-truth of the remaining noisy measurements. Such tolerance against a fixed number of outliers can well be encoded and solved via SMT, as has been demonstrated in [31].  
Conceptualization, B.F., M.F., F.K. and P.K.; Formal analysis, B.F., M.F. and P.K.; Funding acquisition, B.F. and M.F.; Investigation, M.F. and P.K.; Methodology, B.F., M.F., F.K. and P.K.; Project administration, B.F., M.F. and P.K.; Software, M.F. and F.K.; Supervision, B.F. and M.F.; Visualization, M.F.; Writing--original draft, M.F.; Writing--review & editing, B.F., M.F., F.K. and P.K. All authors have read and agreed to the published version of the manuscript.  
The research herein has been supported by Deutsche Forschungsgemeinschaft under grant DFG FR 2715/5-1 \"Konfliktresolution und kausale Inferenz mittels integrierter sozio-technischer Modellbildung\" and as as part of the Collaborative Research Center Foundations of \"Perspicuous Software Systems\" (TRR 248, 389792660) as well as by the State of Lower Saxony within the collaborative research scheme Zukunftslabor Mobilitat.  
Not applicable.  
The authors declare no conflict of interest.