{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T19:33:46Z","timestamp":1773776026446,"version":"3.50.1"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656323","type":"print"},{"value":"9783031656330","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Hybrid systems are often safety-critical and at the same time difficult to formally verify due to their mixed discrete and continuous behavior. To address this issue, we propose a novel incremental verification algorithm for hybrid systems based on online monitoring techniques and reachability analysis. To this end, we develop a four-valued semantics for signal temporal logic that allows us to distinguish two types of uncertainty: one arising from set-based evaluation and another one from the incremental nature of our algorithm. Using these semantics to continuously update the verification verdict, our verification algorithm is the first to run alongside the reachability analysis of the system to be verified. This makes it possible to stop the reachability analysis as soon as we obtain a conclusive verdict. We demonstrate the usefulness of our novel approach by several experiments.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_12","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"259-281","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Using Four-Valued Signal Temporal Logic for\u00a0Incremental Verification of\u00a0Hybrid Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-7202-5417","authenticated-orcid":false,"given":"Florian","family":"Lercher","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3733-842X","authenticated-orcid":false,"given":"Matthias","family":"Althoff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Ahmad, H., Jeannin, J.B.: A program logic to verify signal temporal logic specifications of hybrid systems. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 1\u201311 (2021). https:\/\/doi.org\/10.1145\/3447928.3456648","DOI":"10.1145\/3447928.3456648"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Althoff, M.: An introduction to CORA 2015. In: Proc. of the 1st and 2nd Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 120\u2013151 (2015). https:\/\/doi.org\/10.29007\/zbkv","DOI":"10.29007\/zbkv"},{"issue":"4","key":"12_CR3","doi-asserted-by":"publisher","first-page":"903","DOI":"10.1109\/TRO.2014.2312453","volume":"30","author":"M Althoff","year":"2014","unstructured":"Althoff, M., Dolan, J.M.: Online verification of automated road vehicles using reachability analysis. IEEE Trans. Rob. 30(4), 903\u2013918 (2014). https:\/\/doi.org\/10.1109\/TRO.2014.2312453","journal-title":"IEEE Trans. Rob."},{"issue":"1","key":"12_CR4","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1146\/annurev-control-071420-081941","volume":"4","author":"M Althoff","year":"2021","unstructured":"Althoff, M., Frehse, G., Girard, A.: Set propagation techniques for reachability analysis. Annual Rev. Control Robot. Autonom. Syst. 4(1), 369\u2013395 (2021). https:\/\/doi.org\/10.1146\/annurev-control-071420-081941","journal-title":"Annual Rev. Control Robot. Autonom. Syst."},{"key":"12_CR5","doi-asserted-by":"publisher","unstructured":"Althoff, M., Koschi, M., Manzinger, S.: CommonRoad: composable benchmarks for motion planning on roads. In: Proceedings of the IEEE Intelligent Vehicles Symposium (IV), pp. 719\u2013726 (2017). https:\/\/doi.org\/10.1109\/IVS.2017.7995802","DOI":"10.1109\/IVS.2017.7995802"},{"issue":"1","key":"12_CR6","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":"12_CR7","doi-asserted-by":"publisher","unstructured":"Bae, K., Lee, J.: Bounded model checking of signal temporal logic properties using syntactic separation. Proc. ACM Program. Lang. 3(POPL), 51:1\u201351:30 (2019). https:\/\/doi.org\/10.1145\/3290364","DOI":"10.1145\/3290364"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Bartocci, E., et al.: Specification-based monitoring of cyber-physical systems: A survey on theory, tools and applications. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification: Introductory and Advanced Topics, pp. 135\u2013175 (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_5","DOI":"10.1007\/978-3-319-75632-5_5"},{"issue":"3","key":"12_CR9","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1093\/logcom\/exn075","volume":"20","author":"A Bauer","year":"2010","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Log. Comput. 20(3), 651\u2013674 (2010). https:\/\/doi.org\/10.1093\/logcom\/exn075","journal-title":"J. Log. Comput."},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1\u201314:64 (2011). https:\/\/doi.org\/10.1145\/2000799.2000800","DOI":"10.1145\/2000799.2000800"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., Schilling, C.: JuliaReach: a toolbox for set-based reachability. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 39\u201344 (2019). https:\/\/doi.org\/10.1145\/3302504.3311804","DOI":"10.1145\/3302504.3311804"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Brieger, M., Mitsch, S., Platzer, A.: Dynamic logic of communicating hybrid programs (2023). https:\/\/doi.org\/10.48550\/arXiv.2302.14546","DOI":"10.48550\/arXiv.2302.14546"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Chai, M., Schlingloff, B.H.: Online monitoring of distributed systems with a five-valued LTL. In: Proceedings of the IEEE International Symposium on Multiple-Valued Logic (ISMVL), pp. 226\u2013231 (2014). https:\/\/doi.org\/10.1109\/ISMVL.2014.47","DOI":"10.1109\/ISMVL.2014.47"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification (CAV), pp. 258\u2013263 (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_18","DOI":"10.1007\/978-3-642-39799-8_18"},{"issue":"1","key":"12_CR15","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10703-017-0286-7","volume":"51","author":"JV Deshmukh","year":"2017","unstructured":"Deshmukh, J.V., Donz\u00e9, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. Formal Methods Syst. Design 51(1), 5\u201330 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0286-7","journal-title":"Formal Methods Syst. Design"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Donz\u00e9, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) Formal Modeling and Analysis of Timed Systems (FORMATS), pp. 92\u2013106 (2010). https:\/\/doi.org\/10.1007\/978-3-642-15297-9_9","DOI":"10.1007\/978-3-642-15297-9_9"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Ferr\u00e8re, T., Maler, O., Ni\u010dkovi\u0107, D., Pnueli, A.: From real-time logic to timed automata. J. ACM 66(3), 19:1\u201319:31 (2019). https:\/\/doi.org\/10.1145\/3286976","DOI":"10.1145\/3286976"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification (CAV), pp. 379\u2013395 (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30","DOI":"10.1007\/978-3-642-22110-1_30"},{"issue":"1","key":"12_CR19","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger, T.A.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998). https:\/\/doi.org\/10.1006\/jcss.1998.1581","journal-title":"J. Comput. Syst. Sci."},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Ho, H.M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal logic. In: Bonakdarpour, B., Smolka, S.A. (eds.) Runtime Verification (RV), pp. 178\u2013192 (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_15","DOI":"10.1007\/978-3-319-11164-3_15"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Hunter, P., Ouaknine, J., Worrell, J.: Expressive completeness for metric temporal logic. In: Proceedings of the ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 349\u2013357 (2013). https:\/\/doi.org\/10.1109\/LICS.2013.41","DOI":"10.1109\/LICS.2013.41"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Ishii, D., Yonezaki, N., Goldsztejn, A.: Monitoring temporal properties using interval analysis. IEICE Trans. Fundament. Electr. Commun. Comput. Sci. E99-A(2), 442\u2013453 (2016). https:\/\/doi.org\/10.1587\/transfun.E99.A.442","DOI":"10.1587\/transfun.E99.A.442"},{"issue":"4","key":"12_CR23","doi-asserted-by":"publisher","first-page":"150","DOI":"10.2307\/2267778","volume":"3","author":"SC Kleene","year":"1938","unstructured":"Kleene, S.C.: On notation for ordinal numbers. J. Symbolic Logic 3(4), 150\u2013155 (1938). https:\/\/doi.org\/10.2307\/2267778","journal-title":"J. Symbolic Logic"},{"key":"12_CR24","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2024.101491","volume":"53","author":"N Kochdumper","year":"2024","unstructured":"Kochdumper, N., Bak, S.: Fully automated verification of linear time-invariant systems against signal temporal logic specifications via reachability analysis. Nonlinear Anal. Hybrid Syst 53, 101491 (2024). https:\/\/doi.org\/10.1016\/j.nahs.2024.101491","journal-title":"Nonlinear Anal. Hybrid Syst"},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"Lee, J., Yu, G., Bae, K.: Efficient SMT-based model checking for signal temporal logic. In: Proceedings of the IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 343\u2013354 (2021). https:\/\/doi.org\/10.1109\/ASE51524.2021.9678719","DOI":"10.1109\/ASE51524.2021.9678719"},{"key":"12_CR26","doi-asserted-by":"publisher","unstructured":"Maler, O., Ni\u010dkovi\u0107, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems (FORMATS\/FTRTFT) pp. 152\u2013166 (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12","DOI":"10.1007\/978-3-540-30206-3_12"},{"issue":"3","key":"12_CR27","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10009-012-0247-9","volume":"15","author":"O Maler","year":"2013","unstructured":"Maler, O., Ni\u010dkovi\u0107, D.: Monitoring properties of analog and mixed-signal circuits. Int. J. Softw. Tools Technol. Transf. 15(3), 247\u2013268 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0247-9","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"12_CR28","doi-asserted-by":"publisher","unstructured":"Ni\u010dkovi\u0107, D., Lebeltel, O., Maler, O., Ferr\u00e8re, T., Ulus, D.: AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. Inter. J. Software Tools Technol. Transf. 22(6), 741\u2013758 (2020). https:\/\/doi.org\/10.1007\/s10009-020-00582-z","DOI":"10.1007\/s10009-020-00582-z"},{"issue":"2","key":"12_CR29","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A Platzer","year":"2008","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143\u2013189 (2008). https:\/\/doi.org\/10.1007\/s10817-008-9103-8","journal-title":"J. Autom. Reason."},{"key":"12_CR30","doi-asserted-by":"publisher","unstructured":"Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer International Publishing (2018). https:\/\/doi.org\/10.1007\/978-3-319-63588-0","DOI":"10.1007\/978-3-319-63588-0"},{"key":"12_CR31","doi-asserted-by":"publisher","unstructured":"Rajamani, R.: Vehicle Dynamics and Control. Springer (2012). https:\/\/doi.org\/10.1007\/978-1-4614-1433-9","DOI":"10.1007\/978-1-4614-1433-9"},{"key":"12_CR32","doi-asserted-by":"publisher","unstructured":"Roehm, H., Oehlerking, J., Heinz, T., Althoff, M.: STL model checking of continuous and hybrid systems. In: Artho, C., Legay, A., Peled, D. (eds.) Automated Technology for Verification and Analysis (ATVA), pp. 412\u2013427 (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_26","DOI":"10.1007\/978-3-319-46520-3_26"},{"key":"12_CR33","doi-asserted-by":"publisher","unstructured":"van der Schaft, A., Schumacher, H.: An Introduction to Hybrid Dynamical Systems. Springer (2000). https:\/\/doi.org\/10.1007\/BFb0109998","DOI":"10.1007\/BFb0109998"},{"key":"12_CR34","doi-asserted-by":"publisher","unstructured":"Thati, P., Ro\u015fu, G.: Monitoring algorithms for metric temporal logic specifications. Electr. Notes Theoretical Comput. Sci. 113, 145\u2013162 (2005). https:\/\/doi.org\/10.1016\/j.entcs.2004.01.029","DOI":"10.1016\/j.entcs.2004.01.029"},{"key":"12_CR35","doi-asserted-by":"publisher","unstructured":"Wright, T., Stark, I.: Property-directed verified monitoring of signal temporal logic. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) Runtime Verification (RV), pp. 339\u2013358 (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_19","DOI":"10.1007\/978-3-030-60508-7_19"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65633-0_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:05:55Z","timestamp":1721891155000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}