{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,5]],"date-time":"2026-07-05T21:55:09Z","timestamp":1783288509879,"version":"3.54.6"},"reference-count":30,"publisher":"University of Szeged","issue":"3","license":[{"start":{"date-parts":[[2025,11,26]],"date-time":"2025-11-26T00:00:00Z","timestamp":1764115200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Cybern"],"abstract":"<jats:p>This paper considers the issue of how to deal with Signal Temporal Logic (STL) when taking into account uncertainties. The STL is a formalism with a large expressiveness to describe real-time properties on real-value signals. It is particularly used for system verification. This work focuses on extensions of STL that handle bounded uncertainties on predicates or on the signal itself, by using tubes to represent the sets of signals. In this way, it becomes possible to robustly check the satisfaction of specifications for a noisy system. However, some cases are undecidable due to uncertainty, and other ones are too complex to determine. Mainly, this paper provides a literature review and compares the few state-of-the-art STL monitors able to deal with tubes. In addition, it proposes to go further by introducing Boolean intervals to formalize undecidable cases, and by implementing a new STL formalism applied to sets in DynIbex, a guaranteed integration tool. Thus, STL specifications can be validated in a guaranteed way for a simulated system. As a result, we obtain the same reliable result as the state-of-the-art, but faster. A robotic application with a drone is proposed to illustrate the concept.<\/jats:p>","DOI":"10.14232\/actacyb.315054","type":"journal-article","created":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T08:33:43Z","timestamp":1764318823000},"page":"383-403","source":"Crossref","is-referenced-by-count":3,"title":["Guaranteed Satisfaction of a Signal Temporal Logic Formula on Tubes"],"prefix":"10.14232","volume":"27","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1955-6725","authenticated-orcid":false,"given":"Joris","family":"Tillet","sequence":"first","affiliation":[{"id":[{"id":"https:\/\/ror.org\/042tfbd02","id-type":"ROR","asserted-by":"publisher"}],"name":"ENSTA Paris, Institut Polytechnique de Paris"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-2662-306X","authenticated-orcid":false,"given":"Antoine","family":"Besset","sequence":"additional","affiliation":[{"id":[{"id":"https:\/\/ror.org\/042tfbd02","id-type":"ROR","asserted-by":"publisher"}],"name":"ENSTA Paris, Institut Polytechnique de Paris"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6185-2480","authenticated-orcid":false,"given":"Julien","family":"Alexandre dit Sandretto","sequence":"additional","affiliation":[{"id":[{"id":"https:\/\/ror.org\/042tfbd02","id-type":"ROR","asserted-by":"publisher"}],"name":"ENSTA Paris, Institut Polytechnique de Paris"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"5401","published-online":{"date-parts":[[2025,11,26]]},"reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1080\/00207179.2019.1610903"},{"key":"ref2","article-title":"Validated explicit and implicit Runge-Kutta methods","volume":"22","author":"Alexandre Dit Sandretto","year":"2016","unstructured":"Alexandre Dit Sandretto, J. and Chapoutot, A. Validated explicit and implicit Runge-Kutta methods. Reliable Computing, 22, 2016.","journal-title":"Reliable Computing"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2023.3337744"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75632-5_5"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0286-7"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15297-9_9"},{"key":"ref7","first-page":"1238","article-title":"Model-based monitoring of dynamic systems","volume-title":"Proceedings of the 11th International Joint Conference on Artificial Intelligence","author":"Dvorak","year":"1989","unstructured":"Dvorak, D. and Kuipers, B. Model-based monitoring of dynamic systems. In Proceedings of the 11th International Joint Conference on Artificial Intelligence, volume 2 of IJCAI'89, pages 1238-1243, San Francisco, CA, USA, August 1989. Morgan Kaufmann Publishers Inc."},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.3390\/a15040126"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA48891.2023.10161409"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1587\/transfun.E99.A.442"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0249-6_2"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9413-9"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.cnsns.2020.105578"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10277-1"},{"key":"ref17","article-title":"Trajectory monitoring for a drone using interval analysis","volume-title":"Proceedings of the Workshop on Planning, Perception and Navigation for Intelligent Vehicles","author":"Largent","year":"2023","unstructured":"Largent, S. and Alexandre Dit Sandretto, J. Trajectory monitoring for a drone using interval analysis. In Proceedings of the Workshop on Planning, Perception and Navigation for Intelligent Vehicles, Kyoto, Japan, 2023."},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/3580490"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0305-8"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA48506.2021.9560929"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/CDC45484.2021.9683305"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-57172-5_6"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_26"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2017.03.020"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2016.XII.017"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2020.2998543"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2023.111445"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/3377868"}],"container-title":["Acta Cybernetica"],"original-title":[],"link":[{"URL":"https:\/\/cyber.bibl.u-szeged.hu\/index.php\/actcybern\/article\/download\/4566\/4126","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/cyber.bibl.u-szeged.hu\/index.php\/actcybern\/article\/download\/4566\/4126","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/cyber.bibl.u-szeged.hu\/index.php\/actcybern\/article\/download\/4566\/4126","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,24]],"date-time":"2026-06-24T09:39:40Z","timestamp":1782293980000},"score":1,"resource":{"primary":{"URL":"https:\/\/cyber.bibl.u-szeged.hu\/index.php\/actcybern\/article\/view\/4566"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,26]]},"references-count":30,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2026,6,22]]}},"URL":"https:\/\/doi.org\/10.14232\/actacyb.315054","relation":{},"ISSN":["2676-993X","0324-721X"],"issn-type":[{"value":"2676-993X","type":"electronic"},{"value":"0324-721X","type":"print"}],"subject":[],"published":{"date-parts":[[2025,11,26]]}}}