{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T02:32:40Z","timestamp":1774319560070,"version":"3.50.1"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711763","type":"print"},{"value":"9783031711770","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we present a tool for monitoring the traces of cyber-physical systems (CPS) at runtime, with respect to <jats:italic>Signal Temporal Logic<\/jats:italic> (STL) specifications. Our tool is based on the recent advances of <jats:italic>causation monitoring<\/jats:italic>, which reports not only whether an executing trace violates the specification, but also <jats:italic>how relevant<\/jats:italic> the increment of the trace at each instant is to the specification violation. In this way, it can deliver more information about system evolution than classic online robust monitors. Moreover, by adapting two dynamic programming strategies, our implementation significantly improves the efficiency of causation monitoring, allowing its deployment in practice. The tool is implemented as a  executable and can be easily adapted to monitor CPS in different formalisms. We evaluate the efficiency of the proposed monitoring tool, and demonstrate its superiority over existing robust monitors in terms of the information it can deliver about system evolution.<\/jats:p>","DOI":"10.1007\/978-3-031-71177-0_18","type":"book-chapter","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:10:51Z","timestamp":1726121451000},"page":"286-304","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["CauMon: An Informative Online Monitor for\u00a0Signal Temporal Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3854-9846","authenticated-orcid":false,"given":"Zhenya","family":"Zhang","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9260-9697","authenticated-orcid":false,"given":"Jie","family":"An","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6253-4062","authenticated-orcid":false,"given":"Paolo","family":"Arcaini","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8300-4650","authenticated-orcid":false,"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,13]]},"reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-642-19835-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Annpureddy","year":"2011","unstructured":"Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254\u2013257. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_21"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75632-5","volume-title":"Lectures on Runtime Verification","year":"2018","unstructured":"Bartocci, E., Falcone, Y. (eds.): Lectures on Runtime Verification. LNCS, vol. 10457. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5"},{"key":"18_CR3","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Ferr\u00e8re, T., Manjunath, N., Ni\u010dkovi\u0107, D.: Localizing faults in Simulink\/Stateflow models with STL. In: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (Part of CPS Week), pp. 197\u2013206. HSCC 2018, Association for Computing Machinery, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3178126.3178131","DOI":"10.1145\/3178126.3178131"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/11944836_25","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"A Bauer","year":"2006","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260\u2013272. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11944836_25"},{"issue":"4","key":"18_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 1\u201364 (2011). https:\/\/doi.org\/10.1145\/2000799.2000800","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"1","key":"18_CR6","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. Des. 51(1), 5\u201330 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0286-7","journal-title":"Formal Methods Syst. Des."},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-319-11164-3_19","volume-title":"Runtime Verification","author":"A Dokhanchi","year":"2014","unstructured":"Dokhanchi, A., Hoxha, B., Fainekos, G.: On-line monitoring for temporal logic robustness. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 231\u2013246. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_19"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167\u2013170. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_17"},{"key":"18_CR9","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":"Formal Modeling and Analysis of Timed Systems","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.) FORMATS 2010. LNCS, vol. 6246, pp. 92\u2013106. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15297-9_9"},{"key":"18_CR10","doi-asserted-by":"publisher","unstructured":"Ernst, G., et al.: ARCH-COMP 2021 category report: falsification with validation of results. In: Frehse, G., Althoff, M. (eds.) 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21). EPiC Series in Computing, vol.\u00a080, pp. 133\u2013152. EasyChair (2021). https:\/\/doi.org\/10.29007\/xwl1","DOI":"10.29007\/xwl1"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Ernst, G., et al.: ARCH-COMP 2020 category report: falsification. In: Frehse, G., Althoff, M. (eds.) 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20). EPiC Series in Computing, vol.\u00a074, pp. 140\u2013152. EasyChair (2020). https:\/\/doi.org\/10.29007\/trr1","DOI":"10.29007\/trr1"},{"key":"18_CR12","doi-asserted-by":"publisher","unstructured":"Ernst, G., et al.: ARCH-COMP 2022 category report: falsification with Ubounded resources. In: Frehse, G., Althoff, M., Schoitsch, E., Guiochet, J. (eds.) Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22). EPiC Series in Computing, vol.\u00a090, pp. 204\u2013221. EasyChair (2022). https:\/\/doi.org\/10.29007\/fhnk","DOI":"10.29007\/fhnk"},{"issue":"42","key":"18_CR13","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"GE Fainekos","year":"2009","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoret. Comput. Sci. 410(42), 4262\u20134291 (2009). https:\/\/doi.org\/10.1016\/j.tcs.2009.06.021","journal-title":"Theoret. Comput. Sci."},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-319-11164-3_15","volume-title":"Runtime Verification","author":"H-M Ho","year":"2014","unstructured":"Ho, H.-M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal logic. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 178\u2013192. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_15"},{"key":"18_CR15","doi-asserted-by":"publisher","unstructured":"Jak\u0161i\u0107, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., Ni\u010dkovi\u00e9, D.: From signal temporal logic to FPGA monitors. In: Proceedings of the 2015 ACM\/IEEE International Conference on Formal Methods and Models for Codesign, pp. 218\u2013227. MEMOCODE 2015, IEEE Computer Society, USA (2015). https:\/\/doi.org\/10.1109\/MEMCOD.2015.7340489","DOI":"10.1109\/MEMCOD.2015.7340489"},{"key":"18_CR16","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s10703-018-0319-x","volume":"53","author":"S Jak\u0161i\u0107","year":"2018","unstructured":"Jak\u0161i\u0107, S., Bartocci, E., Grosu, R., Nguyen, T., Ni\u010dkovi\u0107, D.: Quantitative monitoring of STL with edit distance. Formal Methods Syst. Des. 53, 83\u2013112 (2018). https:\/\/doi.org\/10.1007\/s10703-018-0319-x","journal-title":"Formal Methods Syst. Des."},{"key":"18_CR17","doi-asserted-by":"publisher","unstructured":"Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.: Powertrain control verification benchmark. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, pp. 253\u2013262. HSCC 2014, ACM, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2562059.2562140","DOI":"10.1145\/2562059.2562140"},{"issue":"4","key":"18_CR18","first-page":"328","volume":"13","author":"D Lemire","year":"2006","unstructured":"Lemire, D.: Streaming maximum-minimum filter using no more than three comparisons per element. Nordic J. Comput. 13(4), 328\u2013339 (2006)","journal-title":"Nordic J. Comput."},{"key":"18_CR19","doi-asserted-by":"publisher","unstructured":"Lima, L., Herasimau, A., Raszyk, M., Traytel, D., Yuan, S.: Explainable online monitoring of metric temporal logic. In: Sankaranarayanan, S., Sharygina, N. (eds.) International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 13994, pp. 473\u2013491. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_28","DOI":"10.1007\/978-3-031-30820-8_28"},{"key":"18_CR20","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":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Menghi, C., et al.: ARCH-COMP23 category report: Falsification. In: Frehse, G., Althoff, M. (eds.) Proceedings of 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH23). EPiC Series in Computing, vol.\u00a096, pp. 151\u2013169. EasyChair (2023). https:\/\/doi.org\/10.29007\/6nqs","DOI":"10.29007\/6nqs"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-540-75454-1_22","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"D Nickovic","year":"2007","unstructured":"Nickovic, D., Maler, O.: AMT: A property-based monitoring tool for analog systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 304\u2013319. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75454-1_22"},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1007\/978-3-030-59152-6_34","volume-title":"Automated Technology for Verification and Analysis","author":"D Ni\u010dkovi\u0107","year":"2020","unstructured":"Ni\u010dkovi\u0107, D., Yamaguchi, T.: RTAMT: online robustness monitors from STL. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 564\u2013571. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_34"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-319-63387-9_17","volume-title":"Computer Aided Verification","author":"K Selyunin","year":"2017","unstructured":"Selyunin, K., et al.: Runtime monitoring with recovery of the SENT communication protocol. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 336\u2013355. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_17"},{"key":"18_CR25","unstructured":"Ulus, D.: Online monitoring of metric temporal logic using sequential networks. arXiv preprint arXiv:1901.00175 (2019)"},{"key":"18_CR26","doi-asserted-by":"publisher","unstructured":"Zhang, Z., An, J., Arcaini, P., Hasuo, I.: Online causation monitoring of signal temporal logic. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, pp. 62\u201384. Springer Nature Switzerland, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_4","DOI":"10.1007\/978-3-031-37706-8_4"},{"issue":"11","key":"18_CR27","doi-asserted-by":"publisher","first-page":"4421","DOI":"10.1109\/TCAD.2022.3197693","volume":"41","author":"Z Zhang","year":"2022","unstructured":"Zhang, Z., Arcaini, P., Xie, X.: Online reset for signal temporal logic monitoring. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(11), 4421\u20134432 (2022). https:\/\/doi.org\/10.1109\/TCAD.2022.3197693","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"issue":"11","key":"18_CR28","doi-asserted-by":"publisher","first-page":"2894","DOI":"10.1109\/TCAD.2018.2858463","volume":"37","author":"Z Zhang","year":"2018","unstructured":"Zhang, Z., Ernst, G., Sedwards, S., Arcaini, P., Hasuo, I.: Two-layered falsification of hybrid systems guided by monte Carlo tree search. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 37(11), 2894\u20132905 (2018)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"18_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-030-25540-4_23","volume-title":"Computer Aided Verification","author":"Z Zhang","year":"2019","unstructured":"Zhang, Z., Hasuo, I., Arcaini, P.: Multi-armed bandits for Boolean connectives in hybrid system falsification. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 401\u2013420. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_23"},{"key":"18_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1007\/978-3-030-81685-8_29","volume-title":"Computer Aided Verification","author":"Z Zhang","year":"2021","unstructured":"Zhang, Z., Lyu, D., Arcaini, P., Ma, L., Hasuo, I., Zhao, J.: Effective hybrid system falsification using monte Carlo tree search guided by QB-robustness. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 595\u2013618. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_29"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71177-0_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:13:30Z","timestamp":1726121610000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71177-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,13]]},"ISBN":["9783031711763","9783031711770"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71177-0_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,13]]},"assertion":[{"value":"13 September 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":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}