{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,22]],"date-time":"2026-05-22T15:05:31Z","timestamp":1779462331433,"version":"3.53.1"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T00:00:00Z","timestamp":1769904000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,3,23]],"date-time":"2026-03-23T00:00:00Z","timestamp":1774224000000},"content-version":"vor","delay-in-days":50,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2026,2]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Quantitative monitoring mitigates two issues observed in exhaustive, qualitative verification approaches, namely the state-space explosion problem and the rigidity of their binary verdicts. This is achieved through (i) analysing individual executions instead of building the whole state-space and (ii) providing a robustness measure instead of yes\/no answers. In this paper, we consider real-time systems where executions and specifications are modelled as timed signals and Signal Temporal Logic (STL) formulae, respectively. We propose a new temporal robustness measure\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$\\delta $<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>\u03b4<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    for STL, based on a new distance that we define over timed signals. In contrast with existing measures,\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$\\delta $<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>\u03b4<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    provides a precise quantification of distances between the monitored signal and the boundary separating faulty and non-faulty executions w.r.t. an STL property. Thus,\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$\\delta $<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>\u03b4<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    is suitable for a wide range of real-life perturbations, such as those affecting exclusively a particular time window within a signal. Though we prove that computing\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$\\delta $<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>\u03b4<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    is NP-hard in general, we provide efficient algorithms for a practical fragment of STL. In particular, this fragment includes the key property of bounded response. This paper is an extension of\u00a0(Rino et\u00a0al. in Joint International Conference on Quantitative Evaluation of SysTems &amp; International Conference on Formal Modeling and Analysis of Timed Systems (QEST+FORMATS), 2024), published at QEST+FORMATS 2024. The extension includes implementation of algorithms to compute\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$\\delta $<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>\u03b4<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    in a prototype tool, and an evaluation of our approach on a case study of quality assessment of insulin controllers for diabetic patients.\n                  <\/jats:p>","DOI":"10.1007\/s10009-026-00852-2","type":"journal-article","created":{"date-parts":[[2026,3,23]],"date-time":"2026-03-23T15:06:19Z","timestamp":1774278379000},"page":"71-103","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Efficiently computable temporal robustness for a practical STL fragment"],"prefix":"10.1007","volume":"28","author":[{"given":"Neha","family":"Rino","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mohammed","family":"Foughali","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florian","family":"Renkin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eugene","family":"Asarin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,3,23]]},"reference":[{"key":"852_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-68416-6_11","volume-title":"Joint International Conference on Quantitative Evaluation of SysTems & International Conference on Formal Modeling and Analysis of Timed Systems (QEST+FORMATS)","author":"N. Rino","year":"2024","unstructured":"Rino, N., Foughali, M., Asarin, E.: Efficiently computable distance-based robustness for a practical fragment of STL. In: Hillston, J., Soudjani, S., Waga, M. (eds.) Joint International Conference on Quantitative Evaluation of SysTems & International Conference on Formal Modeling and Analysis of Timed Systems (QEST+FORMATS). Lecture Notes in Computer Science, vol.\u00a014996. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-68416-6_11. Full version: https:\/\/hal.science\/hal-04622387"},{"key":"852_CR2","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/j.entcs.2009.02.044","volume":"231","author":"P. Bouyer","year":"2009","unstructured":"Bouyer, P.: Model-checking timed temporal logics. Electron. Notes Theor. Comput. Sci. 231, 323\u2013341 (2009). https:\/\/doi.org\/10.1016\/j.entcs.2009.02.044","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"852_CR3","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2023.102928","volume":"142","author":"M. Foughali","year":"2023","unstructured":"Foughali, M., Hladik, P., Zuepke, A.: Compositional verification of embedded real-time systems. J. Syst. Archit. 142, 102928 (2023). https:\/\/doi.org\/10.1016\/j.sysarc.2023.102928","journal-title":"J. Syst. Archit."},{"key":"852_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35746-6_1","volume-title":"Tools for Practical Software Verification, LASER","author":"E.M. Clarke","year":"2011","unstructured":"Clarke, E.M., Klieber, W., Nov\u00e1cek, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) Tools for Practical Software Verification, LASER. Lecture Notes in Computer Science, vol.\u00a07683, pp.\u00a01\u201330. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-35746-6_1"},{"key":"852_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT)","author":"O. Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). Lecture Notes in Computer Science, vol.\u00a03253, pp.\u00a0152\u2013166. Springer, Berlin (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"key":"852_CR6","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-88562-7_19","volume-title":"International Conference on Computational Methods in Systems Biology (CMSB)","author":"A. Rizk","year":"2008","unstructured":"Rizk, A., Batt, G., Fages, F., Soliman, S.: On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. In: Heiner, M., Uhrmacher, A.M. (eds.) International Conference on Computational Methods in Systems Biology (CMSB), vol.\u00a05307, pp.\u00a0251\u2013268. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-88562-7_19"},{"key":"852_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-15297-9_9","volume-title":"International Conference Formal Modeling and Analysis of Timed Systems (FORMATS)","author":"A. Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) International Conference Formal Modeling and Analysis of Timed Systems (FORMATS). Lecture Notes in Computer Science, vol.\u00a06246, pp.\u00a092\u2013106. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-15297-9_9"},{"key":"852_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-95561-8_1","volume-title":"Software Verification","author":"T.A. Henzinger","year":"2022","unstructured":"Henzinger, T.A.: Quantitative monitoring of software. In: Bloem, R., Dimitrova, R., Fan, C., Sharygina, N. (eds.) Software Verification. Lecture Notes in Computer Science, vol.\u00a013124, pp.\u00a03\u20136. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-95561-8_1"},{"issue":"1","key":"852_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF03018603","volume":"22","author":"M.M. Fr\u00e9chet","year":"1906","unstructured":"Fr\u00e9chet, M.M.: Sur quelques points du calcul fonctionnel. Rend. Circ. Mat. Palermo 22(1), 1\u201372 (1906). https:\/\/doi.org\/10.1007\/BF03018603","journal-title":"Rend. Circ. Mat. Palermo"},{"issue":"3","key":"852_CR10","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1137\/1101022","volume":"1","author":"A.V. Skorokhod","year":"1956","unstructured":"Skorokhod, A.V.: Limit theorems for stochastic processes. Theory Probab. Appl. 1(3), 261\u2013290 (1956). https:\/\/doi.org\/10.1137\/1101022","journal-title":"Theory Probab. Appl."},{"key":"852_CR11","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/s10851-006-0647-0","volume":"27","author":"A. Efrat","year":"2007","unstructured":"Efrat, A., Fan, Q., Venkatasubramanian, S.: Curve matching, time warping, and light fields: new algorithms for computing similarity between curves. J. Math. Imaging Vis. 27, 203\u2013216 (2007). https:\/\/doi.org\/10.1007\/s10851-006-0647-0","journal-title":"J. Math. Imaging Vis."},{"issue":"42","key":"852_CR12","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"G.E. Fainekos","year":"2009","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262\u20134291 (2009). https:\/\/doi.org\/10.1016\/j.tcs.2009.06.021","journal-title":"Theor. Comput. Sci."},{"key":"852_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BFb0014736","volume-title":"Hybrid and Real-Time Systems","author":"V. Gupta","year":"1997","unstructured":"Gupta, V., Henzinger, T.A., Jagadeesan, R.: Robust timed automata. In: Maler, O. (ed.) Hybrid and Real-Time Systems. Lecture Notes in Computer Science, vol.\u00a01201, pp.\u00a0331\u2013345. Springer, Berlin (1997). https:\/\/doi.org\/10.1007\/BFb0014736"},{"issue":"1","key":"852_CR14","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1145\/3550072","volume":"22","author":"A. Rodionova","year":"2023","unstructured":"Rodionova, A., Lindemann, L., Morari, M., Pappas, G.J.: Temporal robustness of temporal logic specifications: analysis and control design. ACM Trans. Embed. Comput. Syst. 22(1), 13\u201311344 (2023). https:\/\/doi.org\/10.1145\/3550072","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"852_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-030-00151-3_12","volume-title":"International Conference Formal Modeling and Analysis of Timed Systems (FORMATS)","author":"E. Asarin","year":"2018","unstructured":"Asarin, E., Basset, N., Degorre, A.: Distance on timed words and applications. In: Jansen, D.N., Prabhakar, P. (eds.) International Conference Formal Modeling and Analysis of Timed Systems (FORMATS). Lecture Notes in Computer Science, vol.\u00a011022, pp.\u00a0199\u2013214. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-00151-3_12"},{"issue":"1","key":"852_CR16","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R. Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996). https:\/\/doi.org\/10.1145\/227595.227602","journal-title":"J. ACM"},{"key":"852_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/MEMOCODE51338.2020.9315156","volume-title":"International Conference on Formal Methods and Models for System Design (MEMOCODE)","author":"M. Foughali","year":"2020","unstructured":"Foughali, M., Bensalem, S., Combaz, J., Ingrand, F.: Runtime verification of timed properties in autonomous robots. In: Capodieci, N. (ed.) International Conference on Formal Methods and Models for System Design (MEMOCODE), pp.\u00a01\u201312 (2020). https:\/\/doi.org\/10.1109\/MEMOCODE51338.2020.9315156"},{"key":"852_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-73368-3_12","volume-title":"International Conference on Computer Aided Verification (CAV)","author":"O. Maler","year":"2007","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: On synthesizing controllers from bounded-response properties. In: Damm, W., Hermanns, H. (eds.) International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol.\u00a04590, pp.\u00a095\u2013107. Springer, Berlin (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_12"},{"key":"852_CR19","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1109\/JCIT.1990.128356","volume-title":"Next Decade in Information Technology: Jerusalem Conference on Information Technology","author":"T.A. Henzinger","year":"1990","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: An interleaving model for real-time. In: Nerode, A., Taitslin, M. (eds.) Next Decade in Information Technology: Jerusalem Conference on Information Technology, pp.\u00a0717\u2013730 (1990). https:\/\/doi.org\/10.1109\/JCIT.1990.128356"},{"key":"852_CR20","unstructured":"PyO3 Developers: PyO3: Rust bindings for Python (2024). https:\/\/github.com\/PyO3\/pyo3"},{"key":"852_CR21","doi-asserted-by":"publisher","first-page":"87","DOI":"10.3233\/978-1-61499-649-1-87","volume-title":"Jupyter Notebooks\u2014a Publishing Format for Reproducible Computational Workflows","author":"T. Kluyver","year":"2016","unstructured":"Kluyver, T., Ragan-Kelley, B., P\u00e9rez, F., Granger, B., Bussonnier, M., Frederic, J., Kelley, K., Hamrick, J., Grout, J., Corlay, S., Ivanov, P., Avila, D., Abdalla, S., Willing, C., Jupyter Development Team: Jupyter Notebooks\u2014a Publishing Format for Reproducible Computational Workflows. Loizides, F., Scmidt, B. (eds.), pp.\u00a087\u201390. IOS Press, Amsterdam (2016). https:\/\/doi.org\/10.3233\/978-1-61499-649-1-87"},{"key":"852_CR22","unstructured":"Hsieh, C., Donz\u00e9, A.: CyPhAi case studies. https:\/\/github.com\/CyPhAi-Project\/CyPhAI-Case-Studies"},{"key":"852_CR23","unstructured":"Xie, J.: Simglucose v0.2.1 (2018). https:\/\/github.com\/jxx123\/simglucose"},{"key":"852_CR24","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1177\/193229680900300","volume":"3","author":"B. Kovatchev","year":"2009","unstructured":"Kovatchev, B., Breton, M., Dalla Man, C., Cobelli, C., et al.: In silico preclinical trials: a proof of concept in closed-loop control of type 1 diabetes. J. Diabetes Sci. Technol. 3, 44\u201355 (2009). https:\/\/doi.org\/10.1177\/193229680900300","journal-title":"J. Diabetes Sci. Technol."},{"issue":"12","key":"852_CR25","doi-asserted-by":"publisher","first-page":"3344","DOI":"10.2337\/db06-0419","volume":"55","author":"G.M. Steil","year":"2006","unstructured":"Steil, G.M., Rebrin, K., Darwin, C., Hariri, F., Saad, M.F.: Feasibility of automating insulin delivery for the treatment of type 1 diabetes. Diabetes 55(12), 3344\u20133350 (2006). https:\/\/doi.org\/10.2337\/db06-0419","journal-title":"Diabetes"},{"key":"852_CR26","series-title":"Proceedings of Machine Learning Research","first-page":"508","volume-title":"Proceedings of the 5th Machine Learning for Healthcare Conference","author":"I. Fox","year":"2020","unstructured":"Fox, I., Lee, J., Pop-Busui, R., Wiens, J.: Deep reinforcement learning for closed-loop blood glucose control. In: Doshi-Velez, F., Fackler, J., Jung, K., Kale, D., Ranganath, R., Wallace, B., Wiens, J. (eds.) Proceedings of the 5th Machine Learning for Healthcare Conference. Proceedings of Machine Learning Research, vol.\u00a0126, pp.\u00a0508\u2013536 (2020). https:\/\/proceedings.mlr.press\/v126\/fox20a.html"},{"key":"852_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-23820-3_1","volume-title":"Runtime Verification","author":"F. Cameron","year":"2015","unstructured":"Cameron, F., Fainekos, G., Maahs, D.M., Sankaranarayanan, S.: Towards a verified artificial pancreas: challenges and solutions for runtime verification. In: Bartocci, E., Majumdar, R. (eds.) Runtime Verification. Lecture Notes in Computer Science, vol.\u00a09333, pp.\u00a03\u201317. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_1"},{"key":"852_CR28","series-title":"LIPIcs","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4230\/LIPICS.ECOOP.2025.1","volume-title":"European Conference on Object-Oriented Programming (ECOOP)","author":"M. Amara","year":"2025","unstructured":"Amara, M., Bernardi, G., Foughali, M., Francalanza, A.: A theory of (linear-time) timed monitors. In: European Conference on Object-Oriented Programming (ECOOP). LIPIcs, vol.\u00a0333, pp.\u00a01\u201330 (2025). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2025.1"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-026-00852-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-026-00852-2","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-026-00852-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,22]],"date-time":"2026-05-22T14:13:44Z","timestamp":1779459224000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-026-00852-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2]]},"references-count":28,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,2]]}},"alternative-id":["852"],"URL":"https:\/\/doi.org\/10.1007\/s10009-026-00852-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2]]},"assertion":[{"value":"27 February 2026","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 March 2026","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}