{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T02:57:52Z","timestamp":1791341872353,"version":"4.3.1"},"reference-count":31,"publisher":"MDPI AG","issue":"4","license":[{"start":{"date-parts":[[2022,4,11]],"date-time":"2022-04-11T00:00:00Z","timestamp":1649635200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Algorithms"],"abstract":"<jats:p>Signal Temporal Logic is a linear-time temporal logic designed for classifying the time-dependent signals originating from continuous-state or hybrid-state dynamical systems according to formal specifications. It has been conceived as a tool for systematizing the monitoring of cyber-physical systems, supporting the automatic translation of complex safety specifications into monitoring algorithms, faithfully representing their semantics. Almost all algorithms hitherto suggested do, however, assume perfect identity between the sensor readings, informing the monitor about the system state and the actual ground truth. Only recently have Visconti et al. addressed the issue of inexact measurements, taking up the simple model of interval-bounded per-sample error that is unrelated, in the sense of chosen afresh, across samples. We expand their analysis by decomposing the error into an unknown yet fixed offset and an independent per-sample error and show that in this setting, monitoring of temporal properties no longer coincides with collecting Boolean combinations of state predicates evaluated in each time instant over best-possible per-sample state estimates, but can be genuinely more informative in that it infers determinate truth values for monitoring conditions that interval-based evaluation remains inconclusive about. For the model-free as well as for the linear model-based case, we provide optimal evaluation algorithms based on affine arithmetic and SAT modulo theory, solving over linear arithmetic. The resulting algorithms provide conclusive monitoring verdicts in many cases where state estimations inherently remain inconclusive. In their model-based variants, they can simultaneously address the issues of uncertain sensing and partial observation.<\/jats:p>","DOI":"10.3390\/a15040126","type":"journal-article","created":{"date-parts":[[2022,4,12]],"date-time":"2022-04-12T00:23:11Z","timestamp":1649722991000},"page":"126","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["A Truly Robust Signal Temporal Logic: Monitoring Safety Properties of Interacting Cyber-Physical Systems under Uncertain Observation"],"prefix":"10.3390","volume":"15","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4280-8441","authenticated-orcid":false,"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Stuhlsatzenhaus 5, 66123 Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9138-8340","authenticated-orcid":false,"given":"Martin","family":"Fr\u00e4nzle","sequence":"additional","affiliation":[{"name":"Department of Computing Science, Carl von Ossietzky Universit\u00e4t, Ammerl\u00e4nder Heerstra\u00dfe 114-118, 26129 Oldenburg, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9672-2398","authenticated-orcid":false,"given":"Florian","family":"Kohn","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Stuhlsatzenhaus 5, 66123 Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul","family":"Kr\u00f6ger","sequence":"additional","affiliation":[{"name":"Department of Computing Science, Carl von Ossietzky Universit\u00e4t, Ammerl\u00e4nder Heerstra\u00dfe 114-118, 26129 Oldenburg, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"1968","published-online":{"date-parts":[[2022,4,11]]},"reference":[{"key":"ref_1","first-page":"28","article-title":"RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft","volume":"Volume 12225","author":"Lahiri","year":"2020","journal-title":"Proceedings of the 32nd International Conference, CAV 2020 Part II"},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Gautham, S., Jayakumar, A.V., Rajagopala, A., and Elks, C. (2021, January 10\u201312). Realization of a Model-Based DevOps Process for Industrial Safety Critical Cyber Physical Systems. Proceedings of the 4th IEEE International Conference on Industrial Cyber-Physical Systems (ICPS), Victoria, BC, Canada.","DOI":"10.1109\/ICPS49255.2021.9468213"},{"key":"ref_3","first-page":"152","article-title":"Monitoring Temporal Properties of Continuous Signals","volume":"Volume 3253","author":"Lakhnech","year":"2004","journal-title":"Joint International Conferences on Formal Modelling and Analysis of Timed Systems, Proceedings of the FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France, 22\u201324 September 2004"},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-319-75632-5_5","article-title":"Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications","volume":"Volume 10457","author":"Bartocci","year":"2018","journal-title":"Lectures on Runtime Verification\u2014Introductory and Advanced Topics"},{"key":"ref_5","unstructured":"Holberg, H.J., and H\u00e4usler, S. (2012). From Safety Requirements to Safety Monitors\u2014Automatic Synthesis in Compliance with ISO 26262, Embedded World."},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/11560647_17","article-title":"A Robust Interpretation of Duration Calculus","volume":"Volume 3722","author":"Hung","year":"2005","journal-title":"Proceedings of the Second International Colloquium on Theoretical Aspects of Computing\u2014ICTAC 2005"},{"key":"ref_7","first-page":"92","article-title":"Robust Satisfaction of Temporal Logic over Real-Valued Signals","volume":"Volume 6246","author":"Chatterjee","year":"2010","journal-title":"Proceedings of the 8th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2010"},{"key":"ref_8","first-page":"264","article-title":"Efficient Robust Monitoring for STL","volume":"Volume 8044","author":"Sharygina","year":"2013","journal-title":"Proceedings of the 25th International Conference on Computer Aided Verification, CAV 2013"},{"key":"ref_9","unstructured":"Maybeck, P.S. (1979). Stochastic models, estimation, and control. Mathematics in Science and Engineering, Academic Press."},{"key":"ref_10","first-page":"553","article-title":"Runtime Monitors for Markov Decision Processes","volume":"Volume 12760","author":"Silva","year":"2021","journal-title":"Computer Aided Verification"},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/978-3-030-01461-2_9","article-title":"The Demon, the Gambler, and the Engineer\u2014Reconciling Hybrid-System Theory with Metrology","volume":"Volume 11180","author":"Jones","year":"2018","journal-title":"Symposium on Real-Time and Hybrid Systems\u2014Essays Dedicated to Professor Chaochen Zhou on the Occasion of His 80th Birthday"},{"key":"ref_12","unstructured":"Arun-Kumar, S., M\u00e9ry, D., Saha, I., and Zhang, L. (2021, January 20\u201322). Online monitoring of spatio-temporal properties for imprecise signals. Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design, Virtual Event."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1023\/B:NUMA.0000049462.70970.b6","article-title":"Affine Arithmetic: Concepts and Applications","volume":"37","author":"Stolfi","year":"2004","journal-title":"Numer. Algorithms"},{"key":"ref_14","unstructured":"Wolfman, S.A., and Weld, D.S. (1999). The LPSAT Engine & Its Application to Resource Planning. Proceedings of the 16th International Joint Conference on Artifical Intelligence\u2014Volume 1, IJCAI\u201999, Morgan Kaufmann Publishers Inc."},{"key":"ref_15","unstructured":"Piterman, N., and Smolka, S. (2013, January 16\u201324). The MathSAT5 SMT Solver. Proceedings of the 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy. Lecture Notes in Computer Science."},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"743","DOI":"10.1007\/s10409-015-0525-3","article-title":"Interval arithmetic operations for uncertainty analysis with correlated interval variables","volume":"32","author":"Jiang","year":"2016","journal-title":"Acta Mech. Sin."},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/s10703-019-00332-1","article-title":"TeLEx: Learning signal temporal logic from positive examples using tightness metric","volume":"54","author":"Jha","year":"2019","journal-title":"Form. Methods Syst. Des."},{"key":"ref_18","unstructured":"Moore, R.E. (1966). Interval Analysis, Prentice-Hall."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1561\/1000000053","article-title":"Contracts for System Design","volume":"12","author":"Benveniste","year":"2018","journal-title":"Found. Trends Electron. Des. Autom."},{"key":"ref_20","unstructured":"Loper, G.B. (1950). Variable Gain Voltage Amplifier. (No. 2,497,835), U.S. Patent, Available online: https:\/\/patentimages.storage.googleapis.com\/52\/a3\/32\/2fca1a6d25a758\/US2497835.pdf."},{"key":"ref_21","first-page":"209","article-title":"Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure","volume":"1","author":"Herde","year":"2007","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"ref_22","unstructured":"Silva, J.P.M., and Sakallah, K.A. (1996, January 16\u201319). Conflict Analysis in Search Algorithms for Satisfiability. Proceedings of the Eigth International Conference on Tools with Artificial Intelligence, ICTAI \u201996, Toulouse, France."},{"key":"ref_23","unstructured":"Kuipers, B., and Webber, B.L. (1997, January 27\u201331). Using CSP Look-Back Techniques to Solve Real-World SAT Instances. Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, Providence, RI, USA."},{"key":"ref_24","first-page":"141","article-title":"Lazy Satisability Modulo Theories","volume":"3","author":"Sebastiani","year":"2007","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., and Bloem, R. (2018). Satisfiability Modulo Theories. Handbook of Model Checking, Springer International Publishing.","DOI":"10.1007\/978-3-319-10575-8"},{"key":"ref_26","first-page":"725","article-title":"Two Decades of Formal Methods in Industrial Products at BTC Embedded Systems","volume":"Volume 13047","author":"Huisman","year":"2021","journal-title":"Proceedings of the 24th International Symposium on Formal Methods, FM 2021"},{"key":"ref_27","unstructured":"Piskac, R., and Talupur, M. (2016, January 3\u20136). Accurate ICP-based floating-point reasoning. Proceedings of the 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA."},{"key":"ref_28","unstructured":"Herde, C. (2010). Efficient Solving of Large Arithmetic Constraint Systems with Complex Boolean Structure: Proof Engines for the Analysis of Hybrid Discrete-Continuous Systems. [Ph.D. Thesis, Carl von Ossietzky University of Oldenburg]."},{"key":"ref_29","unstructured":"Haubelt, C., and Timmermann, D. (2013, January 12\u201314). Recent Improvements in the SMT Solver iSAT. Proceedings of the Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Warnem\u00fcnde, Germany."},{"key":"ref_30","unstructured":"Harrison, M.A., Banerji, R.B., and Ullman, J.D. (1971, January 3\u20135). The Complexity of Theorem-Proving Procedures. Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, Shaker Heights, OH, USA."},{"key":"ref_31","doi-asserted-by":"crossref","unstructured":"Amri, M., Becis, Y., Aubry, D., Ramdani, N., and Fr\u00e4nzle, M. (2015, January 24\u201328). Robust indoor location tracking of multiple inhabitants using only binary sensors. Proceedings of the IEEE International Conference on Automation Science and Engineering, CASE 2015, Gothenburg, Sweden.","DOI":"10.1109\/CoASE.2015.7294061"}],"container-title":["Algorithms"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1999-4893\/15\/4\/126\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T22:51:58Z","timestamp":1760136718000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1999-4893\/15\/4\/126"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,11]]},"references-count":31,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2022,4]]}},"alternative-id":["a15040126"],"URL":"https:\/\/doi.org\/10.3390\/a15040126","relation":{},"ISSN":["1999-4893"],"issn-type":[{"value":"1999-4893","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,11]]}}}