{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T13:44:43Z","timestamp":1743687883221},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030320782"},{"type":"electronic","value":"9783030320799"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-32079-9_14","type":"book-chapter","created":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T14:05:05Z","timestamp":1570111505000},"page":"239-255","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["An Extension of LTL with Rules and Its Application to Runtime Verification"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,10,1]]},"reference":[{"issue":"3","key":"14_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":"14_CR2","unstructured":"D\u2019Angelo, B., et al.: LOLA: runtime monitoring of synchronous systems. In: TIME 2005, pp. 166\u2013 174 (2005)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-75632-5_1","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1\u201333. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-75632-5_1"},{"issue":"3","key":"14_CR4","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/s10703-015-0222-7","volume":"46","author":"David Basin","year":"2015","unstructured":"Basin, D.A., Klaedtke, F., Marinovic, S., Zalinescu, E.n.: Monitoring of temporal first-order properties with aggregations. Formal Methods Syst. Des. 46(3), 262\u2013285 (2015)","journal-title":"Formal Methods in System Design"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-77395-5_11","volume-title":"Runtime Verification","author":"A Bauer","year":"2007","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Ta\u015f\u0131ran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 126\u2013138. Springer, Heidelberg (2007). \n                    https:\/\/doi.org\/10.1007\/978-3-540-77395-5_11"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-540-49382-2_27","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"J Bohn","year":"1998","unstructured":"Bohn, J., Damm, W., Grumberg, O., Hungar, H., Laster, K.: First-order-CTL model checking. In: Arvind, V., Ramanujam, S. (eds.) FSTTCS 1998. LNCS, vol. 1530, pp. 283\u2013294. Springer, Heidelberg (1998). \n                    https:\/\/doi.org\/10.1007\/978-3-540-49382-2_27"},{"issue":"3","key":"14_CR7","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":"14_CR8","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: \n                    \n                      \n                    \n                    $$10^{20}$$\n                   states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"issue":"2","key":"14_CR9","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":"14_CR10","unstructured":"DejaVu. \n                    https:\/\/github.com\/havelund\/dejavu"},{"key":"14_CR11","series-title":"Undergraduate Texts in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2355-7","volume-title":"Mathematical Logic","author":"H-D Ebbinghaus","year":"1984","unstructured":"Ebbinghaus, H.-D., Flum, J., Thomas, W.: Mathematical Logic. Undergraduate Texts in Mathematics. Springer, New York (1984). \n                    https:\/\/doi.org\/10.1007\/978-1-4757-2355-7"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Colombo, C., Pace, G.J., Schneider, G.: LARVA - safer monitoring of real-time Java programs. In: 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009), Hanoi, Vietnam, 23\u201327 November 2009, pp. 33\u201337. IEEE Computer Society (2009)","DOI":"10.1109\/SEFM.2009.13"},{"issue":"3","key":"14_CR13","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":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-57288-8_1","volume-title":"NASA Formal Methods","author":"H Frenkel","year":"2017","unstructured":"Frenkel, H., Grumberg, O., Sheinvald, S.: An automata-theoretic approach to modeling systems and specifications over infinite data. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 1\u201318. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-57288-8_1"},{"issue":"2","key":"14_CR15","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\u2013206 (2012)","journal-title":"IEEE Trans. Serv. Comput."},{"issue":"2","key":"14_CR16","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. STTT 17(2), 143\u2013170 (2015)","journal-title":"STTT"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-319-94111-0_2","volume-title":"Model Checking Software","author":"K Havelund","year":"2018","unstructured":"Havelund, K., Peled, D.: Efficient runtime verification of first-order temporal properties. In: Gallardo, M.M., Merino, P. (eds.) SPIN 2018. LNCS, vol. 10869, pp. 26\u201347. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-94111-0_2"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Havelund, K., Peled, D.A., Ulus, D.: First-order temporal logic monitoring with BDDs. In: FMCAD 2017, pp. 116\u2013123 (2017)","DOI":"10.23919\/FMCAD.2017.8102249"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Havelund, K., Peled, D.A., Ulus, D.: First-order temporal logic monitoring with BDDs. Formal Methods Syst. Des. 1\u201321 (2019)","DOI":"10.1007\/s10703-018-00327-4"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-75632-5_3","volume-title":"Lectures on Runtime Verification","author":"K Havelund","year":"2018","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. LNCS, vol. 10457, pp. 61\u2013102. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-75632-5_3"},{"key":"14_CR21","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). \n                    https:\/\/doi.org\/10.1007\/3-540-46002-0_24"},{"issue":"4","key":"14_CR22","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":"14_CR23","unstructured":"IEEE Standard for Property Specification Language (PSL), Annex B. IEEE Std 1850TM-2010 (2010)"},{"key":"14_CR24","unstructured":"JavaBDD. \n                    http:\/\/javabdd.sourceforge.net"},{"issue":"3","key":"14_CR25","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. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"14_CR26","series-title":"Specification","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Specification. Springer, New York (1992). \n                    https:\/\/doi.org\/10.1007\/978-1-4612-0931-7"},{"key":"14_CR27","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10009-011-0198-6","volume":"14","author":"PO Meredith","year":"2011","unstructured":"Meredith, P.O., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. STTT 14, 249\u2013289 (2011)","journal-title":"STTT"},{"key":"14_CR28","unstructured":"Mars Science Laboratory (MSL) mission website. \n                    http:\/\/mars.jpl.nasa.gov\/msl"},{"key":"14_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1007\/978-3-662-46681-0_55","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Reger","year":"2015","unstructured":"Reger, G., Cruz, H.C., Rydeheard, D.: MarQ: monitoring at runtime with QEA. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 596\u2013610. Springer, Heidelberg (2015). \n                    https:\/\/doi.org\/10.1007\/978-3-662-46681-0_55"},{"key":"14_CR30","unstructured":"Sistla, A.P.: Theoretical issues in the design and analysis of distributed systems, Ph.D. Thesis, Harvard University (1983)"},{"key":"14_CR31","first-page":"133","volume-title":"Formal Models and Semantics","author":"Wolfgang THOMAS","year":"1990","unstructured":"Thomas, W.: Automata on Infinite Objects, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 133\u2013192 (1990)"},{"issue":"1\/2","key":"14_CR32","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. Inf. Control 56(1\/2), 72\u201399 (1983)","journal-title":"Inf. Control"},{"key":"14_CR33","doi-asserted-by":"crossref","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths (Extended Abstract). In: FOCS 1983, pp. 185\u2013194 (1983)","DOI":"10.1109\/SFCS.1983.51"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-32079-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T14:14:15Z","timestamp":1570112055000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-32079-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030320782","9783030320799"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-32079-9_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"1 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Runtime Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rv2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.react.uni-saarland.de\/rv2019\/","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":"38","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":"14","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":"2","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":"37% - 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":"4","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":"4","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)"}}]}}