{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,19]],"date-time":"2025-11-19T14:44:25Z","timestamp":1763563465996,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031656293"},{"type":"electronic","value":"9783031656309"}],"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,25]],"date-time":"2024-07-25T00:00:00Z","timestamp":1721865600000},"content-version":"vor","delay-in-days":206,"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>Runtime verification is a technique for monitoring a system\u2019s behavior against a formal specification. Monitors must produce verdicts that are sound with respect to the specification. Anticipation is the ability to immediately produce verdicts when the monitor can confidently predict the inevitability of the verdict.<\/jats:p><jats:p>Stream runtime verification is a specialized form of runtime verification tailored to the monitoring and verification of data streams. In this paper we study anticipatory monitoring for stream runtime verification. More specifically, we present an algorithm with anticipation for monitoring of Lola specifications, which we then extend to exploit assumptions and tolerate uncertainties. As perfect anticipation is in general not computable, we use techniques from abstract interpretation, especially widening, to approximate anticipatory monitoring verdicts. Finally, we report on three empirical cases studies using a prototype implementation of a symbolic instantiation of our approach.<\/jats:p>","DOI":"10.1007\/978-3-031-65630-9_7","type":"book-chapter","created":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T22:01:56Z","timestamp":1721858516000},"page":"133-155","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["General Anticipatory Runtime Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-8348-6163","authenticated-orcid":false,"given":"Raik","family":"Hipler","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8301-4752","authenticated-orcid":false,"given":"Hannes","family":"Kallwies","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3696-9222","authenticated-orcid":false,"given":"Martin","family":"Leucker","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3927-4773","authenticated-orcid":false,"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,25]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-642-29860-8_27","volume-title":"Runtime Verification","author":"D Basin","year":"2012","unstructured":"Basin, D., Harvan, M., Klaedtke, F., Z\u0103linescu, E.: MONPOLY: monitoring usage-control policies. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 360\u2013364. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_27"},{"key":"7_CR2","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":"3","key":"7_CR3","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":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-030-32079-9_10","volume-title":"Runtime Verification","author":"A Cimatti","year":"2019","unstructured":"Cimatti, A., Tian, C., Tonetta, S.: Assumption-based runtime verification with partial observability and resets. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 165\u2013184. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_10"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-030-88494-9_11","volume-title":"Runtime Verification","author":"A Cimatti","year":"2021","unstructured":"Cimatti, A., Tian, C., Tonetta, S.: Assumption-based runtime verification of infinite-state systems. In: Feng, L., Fisman, D. (eds.) RV 2021. LNCS, vol. 12974, pp. 207\u2013227. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88494-9_11"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-030-03044-5_10","volume-title":"Formal Methods: Foundations and Applications","author":"L Convent","year":"2018","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, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03044-5_10"},{"key":"7_CR7","unstructured":"Cousot, P.: Principles of Abstract Interpretation. The MIT Press (2021)"},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages (POL 1977), pp. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"D\u2019Angelo, B., et al.: LOLA: runtime monitoring of synchronous systems. In: Proceedings of the 12th International Symposium of Temporal Representation and Reasoning (TIME 2005), pp. 166\u2013174. IEEE Computer Society (2005). https:\/\/doi.org\/10.1109\/TIME.2005.26","DOI":"10.1109\/TIME.2005.26"},{"issue":"2","key":"7_CR10","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/s10009-015-0380-3","volume":"18","author":"N Decker","year":"2016","unstructured":"Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. Int. J. Softw. Tools Technol. Transf. 18(2), 205\u2013225 (2016). https:\/\/doi.org\/10.1007\/s10009-015-0380-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-030-25540-4_24","volume-title":"Computer Aided Verification","author":"P Faymonville","year":"2019","unstructured":"Faymonville, P., et al.: 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"},{"key":"7_CR12","unstructured":"Faymonville, P., Finkbeiner, B., Schwenger, M., Torfah, H.: Real-time stream-based monitoring. CoRR abs\/1711.03829 (2017). http:\/\/arxiv.org\/abs\/1711.03829"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Felli, P., Montali, M., Patrizi, F., Winkler, S.: Monitoring arithmetic temporal properties on finite traces. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI 2023), pp. 6346\u20136354. AAAI Press (2023). https:\/\/doi.org\/10.1609\/aaai.v37i5.25781","DOI":"10.1609\/aaai.v37i5.25781"},{"key":"7_CR14","unstructured":"Goldberg, A., Havelund, K.: Automated runtime verification with eagle. In: Proceedings of the 3rd International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, (MSVVEIS 2005). INSTICC Press (2005)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-030-03769-7_16","volume-title":"Runtime Verification","author":"F Gorostiaga","year":"2018","unstructured":"Gorostiaga, F., S\u00e1nchez, C.: Striver: stream runtime verification for real-time event-streams. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 282\u2013298. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_16"},{"key":"7_CR16","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/s10009-021-00605-3","volume":"23","author":"F Gorostiaga","year":"2021","unstructured":"Gorostiaga, F., S\u00e1nchez, C.: Stream runtime verification of real-time event streams with the Striver language. Int. J. Softw. Tools Technol. Transfer 23, 157\u2013183 (2021). https:\/\/doi.org\/10.1007\/s10009-021-00605-3","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342\u2013356. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_24"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-60508-7_1","volume-title":"Runtime Verification","author":"TA Henzinger","year":"2020","unstructured":"Henzinger, T.A., Sara\u00e7, N.E.: Monitorability under assumptions. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 3\u201318. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_1"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Kallwies, H., Leucker, M., S\u00e1nchez, C.: Symbolic runtime verification for monitoring under uncertainties and assumptions. In: Bouajjani, A., Hol\u00edk, L., Wu, Z. (eds.) ATVA 2022. LNCS, vol. 13505, pp. 117\u2013134. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_8","DOI":"10.1007\/978-3-031-19992-9_8"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Kallwies, H., Leucker, M., S\u00e1nchez, C.: General anticipatory monitoring for temporal logics on finite traces. In: Katsaros, P., Nenzi, L. (eds.) RV 2023. LNCS, vol. 14245, pp. 106\u2013125. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-44267-4_6","DOI":"10.1007\/978-3-031-44267-4_6"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Kallwies, H., Leucker, M., S\u00e1nchez, C., Scheffel, T.: Anticipatory recurrent monitoring with uncertainty and assumptions. In: Dang, T., Stolz, V. (eds.) RV 2022. LNCS, vol. 13498, pp. 181\u2013199. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17196-3_10","DOI":"10.1007\/978-3-031-17196-3_10"},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Kallwies, H., Leucker, M., Schmitz, M., Schulz, A., Thoma, D., Weiss, A.: TeSSLa - an ecosystem for runtime verification. In: Dang, T., Stolz, V. (eds.) RV 2022. LNCS, vol. 13498, pp. 314\u2013324. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17196-3_20","DOI":"10.1007\/978-3-031-17196-3_20"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Koenig, N.P., Howard, A.: Design and use paradigms for Gazebo, an open-source multi-robot simulator. In: Proceedings of the 2004 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS 2004), vol.\u00a03, pp. 2149\u20132154. IEEE (2004). https:\/\/doi.org\/10.1109\/IROS.2004.1389727","DOI":"10.1109\/IROS.2004.1389727"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-642-35632-2_10","volume-title":"Runtime Verification","author":"M Leucker","year":"2013","unstructured":"Leucker, M.: Sliding between model checking and runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 82\u201387. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35632-2_10"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-030-32079-9_16","volume-title":"Runtime Verification","author":"M Leucker","year":"2019","unstructured":"Leucker, M., S\u00e1nchez, C., Scheffel, T., Schmitz, M., Thoma, D.: Runtime verification for timed event streams with partial information. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 273\u2013291. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_16"},{"issue":"5","key":"7_CR26","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebraic Methods Program. 78(5), 293\u2013303 (2009). https:\/\/doi.org\/10.1016\/j.jlap.2008.08.004","journal-title":"J. Log. Algebraic Methods Program."},{"key":"7_CR27","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":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"7_CR29","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on the Foundations of Computer Science (FOCS-1977), pp. 46\u201357. IEEE Computer Society Press (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR30","unstructured":"Quigley, M., et al.: ROS: an open-source robot operating system. In: Workshops at the IEEE International Conference on Robotics and Automation (ICRA90), vol.\u00a03 (2009)"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-54862-8_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Reinbacher","year":"2014","unstructured":"Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 357\u2013372. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_24"},{"key":"7_CR32","unstructured":"Schmitz, M.: Efficient implementation of stream transformations. Ph.D. thesis, University of L\u00fcbeck, Germany (2024). https:\/\/www.zhb.uni-luebeck.de\/epubs\/ediss3011.pdf"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-540-45069-6_28","volume-title":"Computer Aided Verification","author":"S Shoham","year":"2003","unstructured":"Shoham, S., Grumberg, O.: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 275\u2013287. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_28"},{"key":"7_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1007\/978-3-030-25540-4_30","volume-title":"Computer Aided Verification","author":"M Waga","year":"2019","unstructured":"Waga, M., Andr\u00e9, \u00c9., Hasuo, I.: Symbolic monitoring against specifications parametric in time and data. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 520\u2013539. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_30"},{"key":"7_CR35","doi-asserted-by":"publisher","unstructured":"Waga, M., Andr\u00e9, \u00c9., Hasuo, I.: Model-bounded monitoring of hybrid systems. ACM Trans. Cyber-Phys. Syst. 6:4(30), 1\u201326 (2021). https:\/\/doi.org\/10.1145\/3529095","DOI":"10.1145\/3529095"}],"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-65630-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T22:02:31Z","timestamp":1721858551000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65630-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656293","9783031656309"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65630-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"25 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"}}]}}