{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:25:00Z","timestamp":1777519500759,"version":"3.51.4"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030995263","type":"print"},{"value":"9783030995270","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>First-order temporal logics and rule-based formalisms are two popular families of specification languages for monitoring. Each family has its advantages and only few monitoring tools support their combination. We extend metric first-order temporal logic (MFOTL) with a recursive let construct, which enables interleaving rules with temporal logic formulas. We also extend VeriMon, an MFOTL monitor whose correctness has been formally verified using the Isabelle proof assistant, to support the new construct. The extended correctness proof covers the interaction of the new construct with the existing verified algorithm, which is subtle due to the presence of the bounded future temporal operators. We demonstrate the recursive let\u2019s usefulness on several example specifications and evaluate our verified algorithm\u2019s performance against the DejaVu monitoring tool.<\/jats:p>","DOI":"10.1007\/978-3-030-99527-0_13","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:37:21Z","timestamp":1648535841000},"page":"236-253","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Verified First-Order Monitoring with Recursive Rules"],"prefix":"10.1007","author":[{"given":"Sheila","family":"Zingg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8314-2589","authenticated-orcid":false,"given":"Sr\u0111an","family":"Krsti\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3018-2557","authenticated-orcid":false,"given":"Martin","family":"Raszyk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8253-4513","authenticated-orcid":false,"given":"Joshua","family":"Schneider","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7982-2768","authenticated-orcid":false,"given":"Dmitriy","family":"Traytel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"13_CR1","unstructured":"Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley (1995)"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 44\u201357. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_5","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Basin, D., Dardinier, T., Heimes, L., Krsti\u0107, S., Raszyk, M., Schneider, J., Traytel, D.: A\u00a0formally verified, optimized monitor for metric first-order dynamic logic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS, vol. 12166, pp. 432\u2013453. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_25","DOI":"10.1007\/978-3-030-51074-9_25"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Basin, D., Klaedtke, F., M\u00fcller, S., Z\u0103linescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15:1\u201315:45 (2015). https:\/\/doi.org\/10.1145\/2699444","DOI":"10.1145\/2699444"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Basin, D., Klaedtke, F., Z\u0103linescu, E.: The MonPoly monitoring tool. In: Reger, G., Havelund, K. (eds.) RV-CuBES 2017. Kalpa Publications in Computing, vol.\u00a03, pp. 19\u201328. EasyChair (2017). https:\/\/doi.org\/10.29007\/89hs","DOI":"10.29007\/89hs"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Convent, L., Hungerecker, S., Leucker, M., Scheffel, T., Schmitz, M., Thoma, D.: TeSSLa: Temporal stream-based specification language. In: Massoni, T., Mousavi, M.R. (eds.) SBMF 2018. LNCS, vol. 11254, pp. 144\u2013162. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03044-5_10","DOI":"10.1007\/978-3-030-03044-5_10"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Cucala, D.J.T., Walega, P.A., Grau, B.C., Kostylev, E.V.: Stratified negation in Datalog with metric temporal operators. In: AAAI 2021. pp. 6488\u20136495. AAAI Press (2021)","DOI":"10.1609\/aaai.v35i7.16804"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., S\u00e1nchez, 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 Computer Society (2005). https:\/\/doi.org\/10.1109\/TIME.2005.26","DOI":"10.1109\/TIME.2005.26"},{"key":"13_CR9","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Rossi, F. (ed.) IJCAI 2013. pp. 854\u2013860. IJCAI\/AAAI (2013)"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Falcone, Y., Krsti\u0107, S., Reger, G., Traytel, D.: A taxonomy for classifying runtime verification tools. Int. J. Softw. Tools Technol. Transf. 23(2), 255\u2013284 (2021). https:\/\/doi.org\/10.1007\/s10009-021-00609-z","DOI":"10.1007\/s10009-021-00609-z"},{"key":"13_CR11","doi-asserted-by":"publisher","unstructured":"Gorostiaga, F., S\u00e1nchez, C.: Stream runtime verification of real-time event streams with the striver language. Int. J. Softw. Tools Technol. Transf. 23(2), 157\u2013183 (2021). https:\/\/doi.org\/10.1007\/s10009-021-00605-3","DOI":"10.1007\/s10009-021-00605-3"},{"key":"13_CR12","unstructured":"Haftmann, F.: Code generation from specifications in higher-order logic. Ph.D. thesis, Technical University Munich (2009)"},{"key":"13_CR13","doi-asserted-by":"publisher","unstructured":"Havelund, K.: Rule-based runtime verification revisited. Int. J. Softw. Tools Technol. Transf. 17(2), 143\u2013170 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0309-2","DOI":"10.1007\/s10009-014-0309-2"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Havelund, K., Peled, D.: An extension of LTL with rules and its application to runtime verification. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 239\u2013255. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_14","DOI":"10.1007\/978-3-030-32079-9_14"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Havelund, K., Peled, D., Ulus, D.: First-order temporal logic monitoring with BDDs. Formal Methods Syst. Des. 56(1), 1\u201321 (2020). https:\/\/doi.org\/10.1007\/s10703-018-00327-4","DOI":"10.1007\/s10703-018-00327-4"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Havelund, K., Reger, G., Thoma, D., Z\u0103linescu, E.: Monitoring events that carry data. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification \u2013 Introductory and Advanced Topics, LNCS, vol. 10457, pp. 61\u2013102. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_3","DOI":"10.1007\/978-3-319-75632-5_3"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Krsti\u0107, S., Schneider, J.: A benchmark generator for online first-order monitoring. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 482\u2013494. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_27","DOI":"10.1007\/978-3-030-60508-7_27"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Libkin, L.: Elements of Finite Model Theory. Springer (2004)","DOI":"10.1007\/978-3-662-07003-1"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Ronca, A., Kaminski, M., Grau, B.C., Motik, B., Horrocks, I.: Stream reasoning in temporal Datalog. In: McIlraith, S.A., Weinberger, K.Q. (eds.) AAAI 2018. pp. 1941\u20131948. AAAI Press (2018)","DOI":"10.1609\/aaai.v32i1.11537"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"S\u00e1nchez, C.: Online and offline stream runtime verification of synchronous systems. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 138\u2013163. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_9","DOI":"10.1007\/978-3-030-03769-7_9"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Schneider, J., Basin, D., Krsti\u0107, S., Traytel, D.: A\u00a0formally verified monitor for metric first-order temporal logic. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 310\u2013328. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_18","DOI":"10.1007\/978-3-030-32079-9_18"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Walega, P.A., Kaminski, M., Grau, B.C.: Reasoning over streaming data in metric temporal Datalog. In: AAAI 2019. pp. 3092\u20133099. AAAI Press (2019). https:\/\/doi.org\/10.1609\/aaai.v33i01.33013092","DOI":"10.1609\/aaai.v33i01.33013092"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Yellin, D.M.: Speeding up dynamic transitive closure for bounded degree graphs. Acta Informatica 30(4), 369\u2013384 (1993). https:\/\/doi.org\/10.1007\/BF01209711","DOI":"10.1007\/BF01209711"},{"key":"13_CR24","unstructured":"Zingg, S., Krsti\u0107, S., Raszyk, M., Schneider, J., Traytel, D.: VeriMon\u2019s development repository. https:\/\/bitbucket.org\/jshs\/monpoly\/src\/887b996966\/thys\/ (2021)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99527-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T08:47:08Z","timestamp":1710233228000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99527-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995263","9783030995270"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99527-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","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":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/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":"159","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":"46","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":"4","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":"10","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":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","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)"}}]}}