{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T09:51:24Z","timestamp":1773827484123,"version":"3.50.1"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2021,7,12]],"date-time":"2021-07-12T00:00:00Z","timestamp":1626048000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,7,12]],"date-time":"2021-07-12T00:00:00Z","timestamp":1626048000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2021,8]]},"DOI":"10.1007\/s10009-021-00626-y","type":"journal-article","created":{"date-parts":[[2021,7,12]],"date-time":"2021-07-12T21:02:27Z","timestamp":1626123747000},"page":"547-563","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["An extension of first-order LTL with rules with application to runtime verification"],"prefix":"10.1007","volume":"23","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,12]]},"reference":[{"issue":"3","key":"626_CR1","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"626_CR2","doi-asserted-by":"crossref","unstructured":"Attard, D.P., Cassar, I., Francalanza, A., Aceto, L., Ing\u00f3lfsd\u00f3ttir, A.: A runtime monitoring tool for actor-based systems. In: Gay, S., Ravara, A. (eds) Behavioural Types: from Theory to Tools, Chapter 3, pp. 49\u201376, River Publishers, Denmark (2017)","DOI":"10.1201\/9781003337331-3"},{"key":"626_CR3","doi-asserted-by":"crossref","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification, Verification, Model Checking, and Abstract Interpretation (VMCAI\u201904), LNCS, vol. 44\u201357. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"626_CR4","doi-asserted-by":"crossref","unstructured":"Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. J. Log. Comput. (JLC), Vol. 20, No. 3. Oxford University Press, Oxford, pp. 675\u2013706 (2008)","DOI":"10.1093\/logcom\/exn076"},{"key":"626_CR5","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Leucker, M., Reger, G.: An introduction to runtime verification, lectures on runtime verification - introductory and advanced topics, LNCS, vol. 1\u201323. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-75632-5_1"},{"issue":"3","key":"626_CR6","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/s10703-015-0222-7","volume":"46","author":"DA Basin","year":"2015","unstructured":"Basin, D.A., Klaedtke, F., Marinovic, S., Zalinescu, En: Monitoring of temporal first-order properties with aggregations. Form. Meth. Syst. Des. 46(3), 262\u2013285 (2015)","journal-title":"Form. Meth. Syst. Des."},{"issue":"2","key":"626_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2699444","volume":"62","author":"DA Basin","year":"2015","unstructured":"Basin, D.A., Klaedtke, F., M\u00fcller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 1\u201345 (2015)","journal-title":"J. ACM"},{"key":"626_CR8","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly?, Workshop on Runtime Verification (RV\u201907), LNCS, vol. 126\u2013138. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-77395-5_11"},{"key":"626_CR9","doi-asserted-by":"crossref","unstructured":"Bohn, J., Damm, W., Grumberg, O., Hungar, H., Laster, K.: First-order CTL model checking, International Conference on Foundations of Software Technology and Theoretical Computer Science, (FSTTCS\u201998), LNCS, vol. 283\u2013294. Springer, Berlin (1998)","DOI":"10.1007\/978-3-540-49382-2_27"},{"issue":"3","key":"626_CR10","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv."},{"issue":"2","key":"626_CR11","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ states and beyond. Inform. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inform. Comput."},{"issue":"2","key":"626_CR12","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1145\/210197.210200","volume":"20","author":"J Chomicki","year":"1995","unstructured":"Chomicki, J.: Efficient checking of temporal integrity constraints using bounded history encoding. ACM Trans. Database Syst. 20(2), 149\u2013186 (1995)","journal-title":"ACM Trans. Database Syst."},{"key":"626_CR13","volume-title":"Model checking","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Chambridge (2000)"},{"key":"626_CR14","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, International Symposium on Temporal Representation and Reasoning (TIME\u201905), IEEE, 166-174. (2005)"},{"issue":"2","key":"626_CR15","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. J. Softw. Tools Technol. Transf. 18(2), 205\u2013225 (2016)","journal-title":"J. Softw. Tools Technol. Transf."},{"key":"626_CR16","unstructured":"DejaVu, https:\/\/github.com\/havelund\/dejavu"},{"key":"626_CR17","volume-title":"Mathematical Logic. Undergraduate texts in mathematics","author":"H-D Ebbinghaus","year":"1984","unstructured":"Ebbinghaus, H.-D., Flum, J., Thomas, W.: Mathematical Logic. Undergraduate texts in mathematics. Springer, Berlin (1984)"},{"issue":"3","key":"626_CR18","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/s10009-011-0196-8","volume":"14","author":"Y Falcone","year":"2012","unstructured":"Falcone, Y., Fernandez, J.-C., Mounier, L.: What can you verify and enforce at runtime? STTT 14(3), 349\u2013382 (2012)","journal-title":"STTT"},{"key":"626_CR19","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/0004-3702(82)90020-0","volume":"19","author":"C Forgy","year":"1982","unstructured":"Forgy, C.: Rete: A Fast algorithm for the many pattern\/many object pattern match problem. Artif. Intell. 19, 17\u201337 (1982)","journal-title":"Artif. Intell."},{"key":"626_CR20","doi-asserted-by":"crossref","unstructured":"Frenkel, H., Grumberg, O., Sheinvald, S.: An automata-theoretic approach to modeling systems and specifications over infinite data, NASA Formal Methods (NFM 17), LNCS, vol. 1\u201318. Springer, Berlin (2017)","DOI":"10.1007\/978-3-319-57288-8_1"},{"key":"626_CR21","doi-asserted-by":"crossref","unstructured":"Geist, J., Rozier, K.Y., Schumann, J.: Runtime observer pairs and Bayesian network reasoners on-board FPGAs: Flight-certifiable system health management for embedded systems, International Conference on Runtime Verification (RV\u201914), LNCS, vol. 215\u2013230. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-11164-3_18"},{"key":"626_CR22","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D.A., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. PSTV 3\u201318 (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"issue":"2","key":"626_CR23","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1109\/TSC.2011.10","volume":"5","author":"S Hall\u00e9","year":"2012","unstructured":"Hall\u00e9, S., Villemaire, R.: Runtime enforcement of web service message contracts with data. IEEE Trans. Serv. Comput. 5(2), 192 (2012)","journal-title":"IEEE Trans. Serv. Comput."},{"key":"626_CR24","doi-asserted-by":"crossref","unstructured":"Havelund, K., Peled, D.A., Ulus, D.: First-order temporal logic monitoring with BDDs, Formal Methods in Computer Aided Design (FMCAD\u201917), IEEE, pp. 116\u2013123 (2017)","DOI":"10.23919\/FMCAD.2017.8102249"},{"key":"626_CR25","doi-asserted-by":"crossref","unstructured":"Havelund, K., Peled, D.: Efficient runtime verification of first-order temporal properties. International Symposium on Model Checking Software (SPIN\u201918), LNCS Volume 10869, Springer, Berlin, pp. 26\u201347 (2018)","DOI":"10.1007\/978-3-319-94111-0_2"},{"key":"626_CR26","doi-asserted-by":"crossref","unstructured":"Havelund, K., Reger, G., Thoma, D., Z\u0103linescu, E.: Monitoring events that carry data, Lectures on Runtime Verification\u2014Introductory and Advanced Topics, LNCS, vol. 61\u2013102. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-75632-5_3"},{"key":"626_CR27","doi-asserted-by":"crossref","unstructured":"Havelund, K., Rosu, G.: Synthesizing monitors for safety properties, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 02), LNCS, vol. 342\u2013356. Springer, Berlin (2002)","DOI":"10.1007\/3-540-46002-0_24"},{"key":"626_CR28","doi-asserted-by":"crossref","unstructured":"Havelund, K.: Data automata in Scala, Theoretical Aspects of Software Engineering (TASE\u201914), IEEE Computer Society, pp. 1\u20139 (2014)","DOI":"10.1109\/TASE.2014.37"},{"issue":"2","key":"626_CR29","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10009-014-0309-2","volume":"17","author":"K Havelund","year":"2015","unstructured":"Havelund, K.: Rule-based runtime verification revisited. Softw. Tools Technol. Transf. 17(2), 143\u2013170 (2015)","journal-title":"Softw. Tools Technol. Transf."},{"key":"626_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-018-00327-4","volume":"56","author":"K Havelund","year":"2019","unstructured":"Havelund, K., Peled, D.A., Ulus, D.: First-order temporal logic monitoring with BDDs. Form. Meth. Syst. Des. 56, 1\u201321 (2019)","journal-title":"Form. Meth. Syst. Des."},{"issue":"4","key":"626_CR31","doi-asserted-by":"publisher","first-page":"880","DOI":"10.1145\/502090.502100","volume":"48","author":"L Hella","year":"2001","unstructured":"Hella, L., Libkin, L., Nurmonen, J., Wong, L.: Logics with aggregate operators. J. ACM 48(4), 880\u2013907 (2001)","journal-title":"J. ACM"},{"key":"626_CR32","unstructured":"IEEE Standard for Property Specification Language (PSL), Annex B. IEEE Std 1850TM-2010, (2010)"},{"key":"626_CR33","unstructured":"JavaBDD, http:\/\/javabdd.sourceforge.net"},{"issue":"3","key":"626_CR34","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Form. Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"626_CR35","doi-asserted-by":"crossref","unstructured":"Maler, O., Nic\u0306kovi\u0107, D.: Monitoring properties of analog and mixed-signal circuits. Int. J. Softw. Tools Technol. Transf., Springer, Berlin, vol. 15, pp. 247\u2013268, (2013)","DOI":"10.1007\/s10009-012-0247-9"},{"key":"626_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems\u2014Specification","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems\u2014Specification. Springer, Berlin (1992)"},{"key":"626_CR37","unstructured":"Mars Science Laboratory (MSL) mission website. http:\/\/mars.jpl.nasa.gov\/msl"},{"key":"626_CR38","doi-asserted-by":"crossref","unstructured":"Meredith, P.O., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Transf. vol. 14, pp. 249\u2013289. Springer, Berlin (2012)","DOI":"10.1007\/s10009-011-0198-6"},{"issue":"4","key":"626_CR39","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/s11334-013-0223-x","volume":"9","author":"L Pike","year":"2013","unstructured":"Pike, L., Wegmann, N., Niller, S., Goodloe, A.: Copilot: Monitoring embedded systems. Innov. Syst. Softw. Eng. 9(4), 235\u2013255 (2013)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"626_CR40","doi-asserted-by":"crossref","unstructured":"Reger, G., Cruz, H., Rydeheard, D.: MarQ: Monitoring at runtime with QEA, Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915), LNCS, vol. 596\u2013610. Springer, Berlin (2015)","DOI":"10.1007\/978-3-662-46681-0_55"},{"key":"626_CR41","doi-asserted-by":"crossref","unstructured":"Schneider, J., Basin, D., Krsti\u0107, S., Traytel, D.: A formally verified monitor for metric first-order temporal logic, International Conference on Runtime Verification (RV\u201919), LNCS, vol. 310\u2013328. Springer, Berlin (2019)","DOI":"10.1007\/978-3-030-32079-9_18"},{"key":"626_CR42","doi-asserted-by":"crossref","unstructured":"Shafiei, N., Havelund, K., Mehlitz, P.C.: Actor-based runtime verification with MESA, International Conference on Runtime Verification (RV\u201920), LNCS, vol. 221\u2013240. Springer, Berlin (2020)","DOI":"10.1007\/978-3-030-60508-7_12"},{"key":"626_CR43","unstructured":"Sistla, A.P.: Theoretical Issues in the Design and Analysis of Distributed Systems, Ph.D Thesis, Harvard University, (1983)"},{"key":"626_CR44","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Automata on infinite objects, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 133\u2013192 (1990)","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"626_CR45","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths, Annual Symposium on Foundations of Computer Science (SFCS\u201983), ACM, pp. 185\u2013194"},{"issue":"1\/2","key":"626_CR46","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Inform. Contl. 56(1\/2), 72\u201399 (1983)","journal-title":"Inform. Contl."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00626-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-021-00626-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00626-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,5]],"date-time":"2023-11-05T23:21:53Z","timestamp":1699226513000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-021-00626-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,12]]},"references-count":46,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["626"],"URL":"https:\/\/doi.org\/10.1007\/s10009-021-00626-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,7,12]]},"assertion":[{"value":"6 May 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 July 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}