{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,10,27]],"date-time":"2022-10-27T04:11:56Z","timestamp":1666843916515},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2020,6,8]],"date-time":"2020-06-08T00:00:00Z","timestamp":1591574400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,6,8]],"date-time":"2020-06-08T00:00:00Z","timestamp":1591574400000},"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,4]]},"DOI":"10.1007\/s10009-020-00566-z","type":"journal-article","created":{"date-parts":[[2020,6,8]],"date-time":"2020-06-08T05:04:05Z","timestamp":1591592645000},"page":"137-154","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automata-based monitoring for LTL-FO$$^+$$"],"prefix":"10.1007","volume":"23","author":[{"given":"Rapha\u00ebl","family":"Khoury","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sylvain","family":"Hall\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yannick","family":"Lebrun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,6,8]]},"reference":[{"key":"566_CR1","first-page":"68","volume-title":"FM 2012: Formal Methods\u201418th International Symposium, Paris, France, August 27\u201331, 2012. Proceedings, volume 7436 of Lecture Notes in Computer Science","author":"H Barringer","year":"2012","unstructured":"Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.E.: Quantified event automata: towards expressive and efficient runtime monitors. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012: Formal Methods\u201418th International Symposium, Paris, France, August 27\u201331, 2012. Proceedings, volume 7436 of Lecture Notes in Computer Science, pp. 68\u201384. Springer, Berlin (2012)"},{"key":"566_CR2","first-page":"44","volume-title":"VMCAI, volume 2937 of Lecture Notes in Computer Science","author":"H Barringer","year":"2004","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI, volume 2937 of Lecture Notes in Computer Science, pp. 44\u201357. Springer, Berlin (2004)"},{"key":"566_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Lectures on Runtime Verification\u2014Introductory and Advanced Topics","year":"2018","unstructured":"Bartocci, E., Falcone, Y. (eds.): Lectures on Runtime Verification\u2014Introductory and Advanced Topics. Lecture Notes in Computer Science, vol. 10457. Springer, Berlin (2018)"},{"key":"566_CR4","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci and Falcone [3], pp. 1\u201333 (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_1","DOI":"10.1007\/978-3-319-75632-5_1"},{"issue":"3","key":"566_CR5","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, E.: Monitoring of temporal first-order properties with aggregations. Formal Methods Syst. Design 46(3), 262\u2013285 (2015)","journal-title":"Formal Methods Syst. Design"},{"key":"566_CR6","first-page":"59","volume-title":"From Propositional to First-Order Monitoring","author":"A Bauer","year":"2013","unstructured":"Bauer, A., K\u00fcster, J.-C., Vegliach, G.: From Propositional to First-Order Monitoring, pp. 59\u201375. Springer, Berlin (2013)"},{"key":"566_CR7","unstructured":"Clark, J., DeRose, S.: XML path language (XPath). Technical report, World Wide Web Consortium (1999). https:\/\/www.w3.org\/TR\/1999\/REC-xpath-19991116\/"},{"key":"566_CR8","doi-asserted-by":"crossref","unstructured":"Colombo, C., Pace, G.J., Schneider, G.: Larva\u2014safer monitoring of real-time java programs. In: 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM), pp. 33\u201337. IEEE Computer Society (2009)","DOI":"10.1109\/SEFM.2009.13"},{"issue":"3","key":"566_CR9","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1016\/j.jcss.2006.10.006","volume":"73","author":"A Deutsch","year":"2007","unstructured":"Deutsch, A., Sui, L., Vianu, V.: Specification and verification of data-driven web applications. J. Comput. Syst. Sci. 73(3), 442\u2013474 (2007)","journal-title":"J. Comput. Syst. Sci."},{"key":"566_CR10","first-page":"241","volume-title":"Runtime Verification\u201418th International Conference, RV 2018, Limassol, Cyprus, November 10\u201313, 2018, Proceedings, volume 11237 of Lecture Notes in Computer Science","author":"Y Falcone","year":"2018","unstructured":"Falcone, Y., Krstic, S., Reger, G., Traytel, D.: A taxonomy for classifying runtime verification tools. In: Colombo, C., Leucker, M. (eds.) Runtime Verification\u201418th International Conference, RV 2018, Limassol, Cyprus, November 10\u201313, 2018, Proceedings, volume 11237 of Lecture Notes in Computer Science, pp. 241\u2013262. Springer, Berlin (2018)"},{"issue":"2","key":"566_CR11","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/B:FORM.0000017718.28096.48","volume":"24","author":"B Finkbeiner","year":"2004","unstructured":"Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Formal Methods Syst. Des. 24(2), 101\u2013127 (2004). https:\/\/doi.org\/10.1023\/B:FORM.0000017718.28096.48","journal-title":"Formal Methods Syst. Des."},{"issue":"11","key":"566_CR12","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1109\/MC.2018.2876075","volume":"51","author":"S Hall\u00e9","year":"2018","unstructured":"Hall\u00e9, S., Khoury, R., Awesso, M.: Streamlining the inclusion of computer experiments in a research paper. IEEE Comput. 51(11), 78\u201389 (2018)","journal-title":"IEEE Comput."},{"key":"566_CR13","doi-asserted-by":"crossref","unstructured":"Hall\u00e9, S., Villemaire, R.: Runtime monitoring of message-based workflows with data. In: EDOC, pp. 63\u201372. IEEE Computer Society (2008)","DOI":"10.1109\/EDOC.2008.32"},{"issue":"2","key":"566_CR14","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."},{"key":"566_CR15","doi-asserted-by":"publisher","unstructured":"Hall\u00e9, S., Khoury, R.: Benchmark for Pelota vs. BeepBeep 1.x, experimental package (2020). https:\/\/doi.org\/10.5281\/zenodo.3763804","DOI":"10.5281\/zenodo.3763804"},{"key":"566_CR16","doi-asserted-by":"publisher","unstructured":"Havelund, K., Reger, G., Thoma, D., Zalinescu, E.: Monitoring events that carry data. In Bartocci and Falcone [3], pp. 61\u2013102 (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_3","DOI":"10.1007\/978-3-319-75632-5_3"},{"issue":"1\u20133","key":"566_CR17","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1016\/j.apal.2005.06.007","volume":"138","author":"IM Hodkinson","year":"2006","unstructured":"Hodkinson, I.M.: Complexity of monodic guarded fragments over linear and real time. Ann. Pure Appl. Logic 138(1\u20133), 94\u2013125 (2006)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"2","key":"566_CR18","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(94)90242-9","volume":"134","author":"M Kaminski","year":"1994","unstructured":"Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329\u2013363 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"566_CR19","doi-asserted-by":"crossref","unstructured":"Khoury, R., Hall\u00e9, S., Waldmann, O.: Execution trace analysis using LTL-FO+. In: 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (IsoLa 16), Corfu, Greece (2016)","DOI":"10.1007\/978-3-319-47169-3_26"},{"issue":"3","key":"566_CR20","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Log. 2(3), 408\u2013429 (2001)","journal-title":"ACM Trans. Comput. Log."},{"issue":"3","key":"566_CR21","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/1013560.1013562","volume":"5","author":"F Neven","year":"2004","unstructured":"Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Logic 5(3), 403\u2013435 (2004)","journal-title":"ACM Trans. Comput. Logic"},{"key":"566_CR22","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS\u201977, pp. 46\u201357. IEEE Computer Society, Washington, DC, USA (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"566_CR23","unstructured":"Pretschner, A., B\u00fcchler, M., Harvan, M., Schaefer, C., Walter, T.: Usage control enforcement with data flow tracking for X11. In: Proceedings of 5th International Workshop on Security and Trust Management (STM), pp. 124\u2013137. Elsevier (2009)"},{"key":"566_CR24","doi-asserted-by":"crossref","unstructured":"Segoufin, L.: Automata and logics for words and trees over an infinite alphabet. In: \u00c9sik, Z. (ed) Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25\u201329, 2006, Proceedings, volume 4207 of Lecture Notes in Computer Science, pp. 41\u201357. Springer (2006)","DOI":"10.1007\/11874683_3"},{"key":"566_CR25","first-page":"176","volume-title":"RV, volume 4839 of Lecture Notes in Computer Science","author":"V Stolz","year":"2007","unstructured":"Stolz, V.: Temporal assertions with parametrised propositions. In: Sokolsky, O., Tasiran, S. (eds.) RV, volume 4839 of Lecture Notes in Computer Science, pp. 176\u2013187. Springer, Berlin (2007)"},{"key":"566_CR26","first-page":"347","volume-title":"Mathematics of Multisets","author":"A Syropoulos","year":"2001","unstructured":"Syropoulos, A.: Mathematics of Multisets, pp. 347\u2013358. Springer, Berlin (2001)"},{"issue":"1","key":"566_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M Vardi","year":"1994","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"issue":"1","key":"566_CR28","doi-asserted-by":"publisher","first-page":"1:1","DOI":"10.1145\/2700529","volume":"15","author":"S Varvaressos","year":"2017","unstructured":"Varvaressos, S., Lavoie, K., Gaboury, S., Hall\u00e9, S.: Automated bug finding in video games: a case study for runtime monitoring. Comput. Entertain. 15(1), 1:1\u20131:28 (2017)","journal-title":"Comput. Entertain."}],"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-020-00566-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-020-00566-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00566-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,27]],"date-time":"2022-10-27T00:41:53Z","timestamp":1666831313000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-020-00566-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,8]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,4]]}},"alternative-id":["566"],"URL":"https:\/\/doi.org\/10.1007\/s10009-020-00566-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,6,8]]},"assertion":[{"value":"8 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}