{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:39:48Z","timestamp":1780994388550,"version":"3.54.1"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720155","type":"print"},{"value":"9783030720162","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We investigate efficient algorithms for the online monitoring of properties written in metric temporal logic (MTL). We employ an abstract algebraic semantics based on semirings. It encompasses the Boolean semantics and a quantitative semantics capturing the robustness of satisfaction, which is based on the max-min semiring over the extended real numbers. We provide a precise equational characterization of the class of semirings for which our semantics can be viewed as an approximation to an alternative semantics that quantifies the distance of a system trace from the set of all traces that satisfy the desired property.<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_18","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T22:03:37Z","timestamp":1616191417000},"page":"330-348","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring"],"prefix":"10.1007","author":[{"given":"Konstantinos","family":"Mamouras","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Agnishom","family":"Chattopadhyay","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhifu","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","unstructured":"Abbas, H., Alur, R., Mamouras, K., Mangharam, R., Rodionova, A.: Real-time decision policies with predictable performance. Proceedings of the IEEE, Special Issue on Design Automation for Cyber-Physical Systems 106(9), 1593\u20131615 (2018). https:\/\/doi.org\/10.1109\/JPROC.2018.2853608","DOI":"10.1109\/JPROC.2018.2853608"},{"key":"18_CR2","doi-asserted-by":"publisher","unstructured":"Abbas, H., Mangharam, R.: Generalized robust MTL semantics for problems in cardiac electrophysiology. In: ACC 2018. pp. 1592\u20131597. IEEE (2018). https:\/\/doi.org\/10.23919\/ACC.2018.8431460","DOI":"10.23919\/ACC.2018.8431460"},{"key":"18_CR3","doi-asserted-by":"publisher","unstructured":"Abbas, H., Mittelmann, H.D., Fainekos, G.E.: Formal property verification in a conformance testing framework. In: MEMOCODE 2014. pp. 155\u2013164. IEEE (2014). https:\/\/doi.org\/10.1109\/MEMCOD.2014.6961854","DOI":"10.1109\/MEMCOD.2014.6961854"},{"key":"18_CR4","doi-asserted-by":"publisher","unstructured":"Abbas, H., Rodionova, A., Mamouras, K., Bartocci, E., Smolka, S.A., Grosu, R.: Quantitative regular expressions for arrhythmia detection. IEEE\/ACM Transactions on Computational Biology and Bioinformatics 16(5), 1586\u20131597 (2019). https:\/\/doi.org\/10.1109\/TCBB.2018.2885274","DOI":"10.1109\/TCBB.2018.2885274"},{"key":"18_CR5","doi-asserted-by":"publisher","unstructured":"Akazaki, T., Hasuo, I.: Time robustness in MTL and expressivity in hybrid system falsification. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 356\u2013374. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_21","DOI":"10.1007\/978-3-319-21668-3_21"},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Alur, R., Fisman, D., Mamouras, K., Raghothaman, M., Stanford, C.: Streamable regular transductions. Theoretical Computer Science 807, 15\u201341 (2020). https:\/\/doi.org\/10.1016\/j.tcs.2019.11.018","DOI":"10.1016\/j.tcs.2019.11.018"},{"key":"18_CR7","doi-asserted-by":"publisher","unstructured":"Alur, R., Mamouras, K., Stanford, C.: Automata-based stream processing. In: ICALP 2017. Leibniz International Proceedings in Informatics (LIPIcs), vol. 80, pp. 112:1\u2013112:15. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2017). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2017.112","DOI":"10.4230\/LIPIcs.ICALP.2017.112"},{"key":"18_CR8","doi-asserted-by":"publisher","unstructured":"Alur, R., Mamouras, K., Stanford, C.: Modular quantitative monitoring. Proceedings of the ACM on Programming Languages 3(POPL), 50:1\u201350:31 (2019). https:\/\/doi.org\/10.1145\/3290363","DOI":"10.1145\/3290363"},{"key":"18_CR9","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L.: Monitoring mobile and spatially distributed cyber-physical systems. In: MEMOCODE 2017. pp. 146\u2013155. ACM (2017). https:\/\/doi.org\/10.1145\/3127041.3127050","DOI":"10.1145\/3127041.3127050"},{"key":"18_CR10","doi-asserted-by":"publisher","unstructured":"Benveniste, A., Le Guernic, P., Jacquemot, C.: Synchronous programming with events and relations: The SIGNAL language and its semantics. Science of Computer Programming 16(2), 103\u2013149 (1991). https:\/\/doi.org\/10.1016\/0167-6423(91)90001-E","DOI":"10.1016\/0167-6423(91)90001-E"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Berry, G., Gonthier, G.: The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming 19(2), 87\u2013152 (1992). https:\/\/doi.org\/10.1016\/0167-6423(92)90005-V","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"18_CR12","doi-asserted-by":"publisher","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: LUSTRE: A declarative language for real-time programming. In: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. pp. 178\u2013188. POPL \u201987, ACM, New York, NY, USA (1987). https:\/\/doi.org\/10.1145\/41625.41641","DOI":"10.1145\/41625.41641"},{"key":"18_CR13","doi-asserted-by":"publisher","unstructured":"Chattopadhyay, A., Mamouras, K.: A verified online monitor for metric temporal logic with quantitative semantics. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 383\u2013403. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_21","DOI":"10.1007\/978-3-030-60508-7_21"},{"key":"18_CR14","doi-asserted-by":"publisher","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: Runtime monitoring of synchronous systems. In: TIME 2005. pp. 166\u2013174. IEEE (2005). https:\/\/doi.org\/10.1109\/TIME.2005.26","DOI":"10.1109\/TIME.2005.26"},{"key":"18_CR15","doi-asserted-by":"publisher","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 in System Design 51(1), 5\u201330 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0286-7","DOI":"10.1007\/s10703-017-0286-7"},{"key":"18_CR16","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-319-11164-3_19"},{"key":"18_CR17","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"18_CR18","unstructured":"Donz\u00e9, A.: Breach: A MATLAB toolbox for simulation-based design of dynamical\/CPS\/hybrid systems. https:\/\/github.com\/decyphir\/breach (2021), [Online; accessed January 22, 2021]"},{"key":"18_CR19","doi-asserted-by":"publisher","unstructured":"Donz\u00e9, A., Ferr\u00e8re, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264\u2013279. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_19","DOI":"10.1007\/978-3-642-39799-8_19"},{"key":"18_CR20","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.) FORMATS 2010. LNCS, vol. 6246, pp. 92\u2013106. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15297-9_9","DOI":"10.1007\/978-3-642-15297-9_9"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Dreossi, T., Dang, T., Donz\u00e9, A., Kapinski, J., Jin, X., Deshmukh, J.V.: Efficient guiding strategies for testing of temporal properties of hybrid systems. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 127\u2013142. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_10","DOI":"10.1007\/978-3-319-17524-9_10"},{"key":"18_CR22","doi-asserted-by":"publisher","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science 410(42), 4262\u20134291 (2009). https:\/\/doi.org\/10.1016\/j.tcs.2009.06.021","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"18_CR23","doi-asserted-by":"publisher","unstructured":"Faymonville, P., Finkbeiner, B., Schledjewski, M., Schwenger, M., Stenger, M., Tentrup, L., Torfah, H.: StreamLAB: Stream-based monitoring of cyber-physical systems. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 421\u2013431. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_24","DOI":"10.1007\/978-3-030-25540-4_24"},{"key":"18_CR24","doi-asserted-by":"publisher","unstructured":"Ferr\u00e8re, T., Maler, O., Ni\u010dkovi\u0107, D., Pnueli, A.: From real-time logic to timed automata. Journal of the ACM 66(3), 19:1\u201319:31 (2019). https:\/\/doi.org\/10.1145\/3286976","DOI":"10.1145\/3286976"},{"key":"18_CR25","doi-asserted-by":"publisher","unstructured":"Hoxha, B., Abbas, H., Fainekos, G.E.: Benchmarks for temporal logic requirements for automotive systems. In: ARCH@CPSWeek 2014, 2015. EPiC Series in Computing, vol. 34, pp. 25\u201330. EasyChair (2014). https:\/\/doi.org\/10.29007\/xwrs","DOI":"10.29007\/xwrs"},{"key":"18_CR26","doi-asserted-by":"publisher","unstructured":"Jak\u0161i\u0107, S., Bartocci, E., Grosu, R., Nguyen, T., Ni\u010dkovi\u0107, D.: Quantitative monitoring of STL with edit distance. Formal Methods in System Design 53(1), 83\u2013112 (2018). https:\/\/doi.org\/10.1007\/s10703-018-0319-x","DOI":"10.1007\/s10703-018-0319-x"},{"key":"18_CR27","doi-asserted-by":"publisher","unstructured":"Jak\u0161i\u0107, S., Bartocci, E., Grosu, R., Ni\u010dkovi\u0107, D.: An algebraic framework for runtime verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 37(11), 2233\u20132243 (2018). https:\/\/doi.org\/10.1109\/TCAD.2018.2858460","DOI":"10.1109\/TCAD.2018.2858460"},{"key":"18_CR28","unstructured":"Kahn, G.: The semantics of a simple language for parallel programming. Information Processing 74, 471\u2013475 (1974)"},{"key":"18_CR29","doi-asserted-by":"publisher","unstructured":"Kong, L., Mamouras, K.: StreamQL: A query language for processing streaming time series. Proceedings of the ACM on Programming Languages 4(OOPSLA) (2020). https:\/\/doi.org\/10.1145\/3428251","DOI":"10.1145\/3428251"},{"key":"18_CR30","doi-asserted-by":"publisher","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255\u2013299 (1990). https:\/\/doi.org\/10.1007\/BF01995674","DOI":"10.1007\/BF01995674"},{"key":"18_CR31","doi-asserted-by":"publisher","unstructured":"Lee, E.A., Messerschmitt, D.G.: Static scheduling of synchronous data flow programs for digital signal processing. IEEE Transactions on Computers C-36(1), 24\u201335 (1987). https:\/\/doi.org\/10.1109\/TC.1987.5009446","DOI":"10.1109\/TC.1987.5009446"},{"key":"18_CR32","unstructured":"Lemire, D.: Streaming maximum-minimum filter using no more than three comparisons per element. Nordic Journal of Computing 13(4), 328\u2013339 (2006)"},{"key":"18_CR33","doi-asserted-by":"publisher","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FTRTFT 2004, FORMATS 2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"18_CR34","doi-asserted-by":"publisher","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: Real time temporal logic: Past, present, future. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 2\u201316. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11603009_2","DOI":"10.1007\/11603009_2"},{"key":"18_CR35","doi-asserted-by":"publisher","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 274\u2013289. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11867340_20","DOI":"10.1007\/11867340_20"},{"key":"18_CR36","doi-asserted-by":"publisher","unstructured":"Mamouras, K., Raghothaman, M., Alur, R., Ives, Z.G., Khanna, S.: StreamQRE: Modular specification and efficient evaluation of quantitative queries over streaming data. In: PLDI 2017. pp. 693\u2013708. ACM (2017). https:\/\/doi.org\/10.1145\/3062341.3062369","DOI":"10.1145\/3062341.3062369"},{"key":"18_CR37","doi-asserted-by":"publisher","unstructured":"Mamouras, K., Wang, Z.: Online signal monitoring with bounded lag. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (2020). https:\/\/doi.org\/10.1109\/TCAD.2020.3013053","DOI":"10.1109\/TCAD.2020.3013053"},{"key":"18_CR38","unstructured":"The Valgrind Developers: Valgrind: An instrumentation framework for building dynamic analysis tools. https:\/\/valgrind.org\/ (2021), [Online; accessed January 22, 2021]"},{"key":"18_CR39","doi-asserted-by":"publisher","unstructured":"Ulus, D.: Timescales: A benchmark generator for MTL monitoring tools. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 402\u2013412. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_25","DOI":"10.1007\/978-3-030-32079-9_25"},{"key":"18_CR40","unstructured":"Ulus, D.: The Reelay monitoring tool. https:\/\/doganulus.github.io\/reelay\/ (2020), [Online; accessed August 20, 2020]"},{"key":"18_CR41","unstructured":"Wolff, M.: Heaptrack: A heap memory profiler for Linux. https:\/\/github.com\/KDE\/heaptrack (2021), [Online; accessed January 22, 2021]"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72016-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T00:08:54Z","timestamp":1616371734000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"141","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}