{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T09:29:26Z","timestamp":1766050166425,"version":"3.37.3"},"reference-count":61,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,10,21]],"date-time":"2022-10-21T00:00:00Z","timestamp":1666310400000},"content-version":"vor","delay-in-days":324,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"deutsche forschungsgemeinschaft","doi-asserted-by":"crossref","award":["434592664"],"award-info":[{"award-number":["434592664"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"name":"european research council","award":["683300"],"award-info":[{"award-number":["683300"]}]},{"DOI":"10.13039\/501100001659","name":"deutsche forschungsgemeinschaft","doi-asserted-by":"crossref","award":["389792660"],"award-info":[{"award-number":["389792660"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000001","name":"national science foundation","doi-asserted-by":"publisher","award":["1645824"],"award-info":[{"award-number":["1645824"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"engineering and physical sciences research council","doi-asserted-by":"publisher","award":["EP\/S032207\/1"],"award-info":[{"award-number":["EP\/S032207\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100019559","name":"Carl von Ossietzky Universit\u00e4t Oldenburg","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100019559","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Runtime monitoring is commonly used to detect the violation of desired properties in safety critical cyber-physical systems by observing its executions. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic (LTL) properties based on a three-valued semantics for a finite execution: the formula is already satisfied by the given execution, it is already violated, or it is still undetermined, i.e., it can still be satisfied and violated by appropriate extensions of the given execution. However, a wide range of formulas are not monitorable under this approach, meaning that there are executions for which satisfaction and violation will always remain undetermined no matter how it is extended. In particular, Bauer et al. report that 44% of the formulas they consider in their experiments fall into this category. Recently, a robust semantics for LTL was introduced to capture different degrees by which a property can be violated. In this paper we introduce a robust semantics for finite strings and show its potential in monitoring: every formula considered by Bauer et al. is monitorable under our approach. Furthermore, we discuss which properties that come naturally in LTL monitoring\u2014such as the realizability of all truth values\u2014can be transferred to the robust setting. We show that LTL formulas with robust semantics can be monitored by deterministic automata, and provide tight bounds on the size of the constructed automaton. Lastly, we report on a prototype implementation and compare it to the LTL monitor of Bauer et al. on a sample of examples.<\/jats:p>","DOI":"10.1007\/s10703-022-00398-4","type":"journal-article","created":{"date-parts":[[2022,10,21]],"date-time":"2022-10-21T07:04:01Z","timestamp":1666335841000},"page":"170-204","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["From LTL to rLTL monitoring: improved monitorability through robust semantics"],"prefix":"10.1007","volume":"59","author":[{"given":"Corto","family":"Mascle","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9276-6342","authenticated-orcid":false,"given":"Daniel","family":"Neider","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maximilian","family":"Schwenger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paulo","family":"Tabuada","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Weinert","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Zimmermann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,10,21]]},"reference":[{"key":"398_CR1","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-319-67471-1_2","volume-title":"CMSB 2017, LNCS","author":"H Abbas","year":"2017","unstructured":"Abbas H, Rodionova A, Bartocci E, Smolka SA, Grosu R (2017) Quantitative regular expressions for arrhythmia detection algorithms. In: Feret J, Koeppl H (eds) CMSB 2017, LNCS, vol 10545. Springer, Berlin, pp 23\u201339. https:\/\/doi.org\/10.1007\/978-3-319-67471-1_2"},{"key":"398_CR2","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-319-67531-2_3","volume-title":"RV 2017, LNCS","author":"F Adolf","year":"2017","unstructured":"Adolf F, Faymonville P, Finkbeiner B, Schirmer S, Torens C (2017) Stream runtime monitoring on UAS. In: Lahiri SK, Reger G (eds) RV 2017, LNCS, vol 10548. Springer, Berlin, pp 33\u201349. https:\/\/doi.org\/10.1007\/978-3-319-67531-2_3"},{"key":"398_CR3","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-319-21668-3_21","volume-title":"CAV 2015, LNCS","author":"T Akazaki","year":"2015","unstructured":"Akazaki T, Hasuo I (2015) Time robustness in MTL and expressivity in hybrid system falsification. In: Kroening D, Pasareanu CS (eds) CAV 2015, LNCS, vol 9207. Springer, Berlin, pp 356\u2013374. https:\/\/doi.org\/10.1007\/978-3-319-21668-3_21"},{"key":"398_CR4","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-662-49498-1_2","volume-title":"ESOP 2016, LNCS","author":"R Alur","year":"2016","unstructured":"Alur R, Fisman D, Raghothaman M (2016) Regular programming for quantitative properties of data streams. In: Thiemann P (ed) ESOP 2016, LNCS, vol 9632. Springer, Berlin, pp 15\u201340. https:\/\/doi.org\/10.1007\/978-3-662-49498-1_2"},{"key":"398_CR5","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1145\/3302504.3311812","volume-title":"HSCC 2019","author":"T Anevlavis","year":"2019","unstructured":"Anevlavis T, Neider D, Phillipe M, Tabuada P (2019) Evrostos: the rLTL verifier. In: Ozay N, Prabhakar P (eds) HSCC 2019. ACM, New York, pp 218\u2013223. https:\/\/doi.org\/10.1145\/3302504.3311812"},{"key":"398_CR6","doi-asserted-by":"publisher","unstructured":"Anevlavis T, Philippe M, Neider D, Tabuada P (2018) Verifying rLTL formulas: now faster than ever before! In: CDC 2018, pp 1556\u20131561. IEEE. https:\/\/doi.org\/10.1109\/CDC.2018.8619014","DOI":"10.1109\/CDC.2018.8619014"},{"issue":"2","key":"398_CR7","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/3491216","volume":"23","author":"T Anevlavis","year":"2022","unstructured":"Anevlavis T, Philippe M, Neider D, Tabuada P (2022) Being correct is not enough: efficient verification using robust linear temporal logic. ACM Trans Comput Log 23(2):8:1-8:39. https:\/\/doi.org\/10.1145\/3491216","journal-title":"ACM Trans Comput Log"},{"key":"398_CR8","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J (2008) Principles of model checking. MIT Press, Cambridge"},{"key":"398_CR9","doi-asserted-by":"publisher","unstructured":"Barringer H, Falcone Y, Havelund K, Reger G, Rydeheard DE (2012) Quantified event automata: towards expressive and efficient runtime monitors. In: Giannakopoulou D, M\u00e9ry D (eds) FM 2012, LNCS, vol 7436, pp 68\u201384. Springer. https:\/\/doi.org\/10.1007\/978-3-642-32759-9_9","DOI":"10.1007\/978-3-642-32759-9_9"},{"key":"398_CR10","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-319-96145-3_29","volume-title":"CAV 2018, LNCS","author":"E Bartocci","year":"2018","unstructured":"Bartocci E, Bloem R, Nickovic D, R\u00f6ck F (2018) A counting semantics for monitoring LTL specifications over finite traces. In: Chockler H, Weissenbacher G (eds) CAV 2018, LNCS, vol 10981. Springer, Berlin, pp 547\u2013564. https:\/\/doi.org\/10.1007\/978-3-319-96145-3_29"},{"issue":"3","key":"398_CR11","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/s10703-015-0222-7","volume":"46","author":"DA Basin","year":"2015","unstructured":"Basin DA, Klaedtke F, Marinovic S, Zalinescu E (2015) Monitoring of temporal first-order properties with aggregations. Form Methods Syst Des 46(3):262\u2013285. https:\/\/doi.org\/10.1007\/s10703-015-0222-7","journal-title":"Form Methods Syst Des"},{"key":"398_CR12","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-77395-5_11","volume-title":"RV 2007, LNCS","author":"A Bauer","year":"2007","unstructured":"Bauer A, Leucker M, Schallhart C (2007) The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky O, Tasiran S (eds) RV 2007, LNCS, vol 4839. Springer, Berlin, pp 126\u2013138. https:\/\/doi.org\/10.1007\/978-3-540-77395-5_11"},{"issue":"3","key":"398_CR13","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 (2010) Comparing LTL semantics for runtime verification. J Log Comput 20(3):651\u2013674. https:\/\/doi.org\/10.1093\/logcom\/exn075","journal-title":"J Log Comput"},{"issue":"4","key":"398_CR14","doi-asserted-by":"publisher","first-page":"14:1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer A, Leucker M, Schallhart C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol 20(4):14:1-14:64. https:\/\/doi.org\/10.1145\/2000799.2000800","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"398_CR15","doi-asserted-by":"publisher","unstructured":"Bernstein A, Harter PK Jr (1981) Proving real-time properties of programs with temporal logic. In: Howard J, Reed DP (ed) SOSP 1981. ACM, New York, pp 1\u201311. https:\/\/doi.org\/10.1145\/800216.806585","DOI":"10.1145\/800216.806585"},{"key":"398_CR16","doi-asserted-by":"publisher","unstructured":"Caspi P, Pilaud D, Halbwachs N, Plaice J (1987) Lustre: a declarative language for programming synchronous systems. In: POPL 1987, pp 178\u2013188. ACM Press, New York. https:\/\/doi.org\/10.1145\/41625.41641","DOI":"10.1145\/41625.41641"},{"key":"398_CR17","doi-asserted-by":"publisher","unstructured":"Cheng C (2021) Provably-robust runtime monitoring of neuron activation patterns. In: DATE 2021, pp 1310\u20131313. IEEE. https:\/\/doi.org\/10.23919\/DATE51398.2021.9473957","DOI":"10.23919\/DATE51398.2021.9473957"},{"key":"398_CR18","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-030-60508-7_22","volume-title":"RV 2020, LNCS","author":"J Cralley","year":"2020","unstructured":"Cralley J, Spantidi O, Hoxha B, Fainekos G (2020) Tltk: a toolbox for parallel robustness computation of temporal logic specifications. In: Deshmukh J, Nickovic D (eds) RV 2020, LNCS, vol 12399. Springer, Berlin, pp 404\u2013416. https:\/\/doi.org\/10.1007\/978-3-030-60508-7_22"},{"key":"398_CR19","doi-asserted-by":"publisher","unstructured":"D\u2019Angelo B, Sankaranarayanan S, S\u00e1nchez C, Robinson W, Finkbeiner B, Sipma HB, Mehrotra S, Manna Z (2005) LOLA: runtime monitoring of synchronous systems. In: TIME 2005, pp 166\u2013174. IEEE Computer Society. https:\/\/doi.org\/10.1109\/TIME.2005.26","DOI":"10.1109\/TIME.2005.26"},{"key":"398_CR20","doi-asserted-by":"publisher","unstructured":"Decker N, Leucker M, Thoma D (2013) Impartiality and anticipation for monitoring of visibly context-free properties. In: Legay A, Bensalem S (ed) RV 2013, LNCS, vol 8174, pp 183\u2013200. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-642-40787-1_11","DOI":"10.1007\/978-3-642-40787-1_11"},{"key":"398_CR21","doi-asserted-by":"publisher","unstructured":"Donz\u00e9 A, Ferr\u00e8re T, Maler O (2013) Efficient robust monitoring for STL. In: Sharygina N, Veith H (ed) CAV 2013, LNCS, vol 8044, pp 264\u2013279. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-642-39799-8_19","DOI":"10.1007\/978-3-642-39799-8_19"},{"key":"398_CR22","doi-asserted-by":"publisher","unstructured":"Drusinsky D (2000) The temporal rover and the ATG rover. In: Havelund K, Penix J, Visser W (ed) SPIN 2000, LNCS, vol 1885, pp 323\u2013330. Springer, Berlin. https:\/\/doi.org\/10.1007\/10722468_19","DOI":"10.1007\/10722468_19"},{"key":"398_CR23","doi-asserted-by":"publisher","unstructured":"Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: Boehm BW, Garlan D, Kramer J (ed) ICSE 1999, pp 411\u2013420. ACM, New York. https:\/\/doi.org\/10.1145\/302405.302672","DOI":"10.1145\/302405.302672"},{"key":"398_CR24","doi-asserted-by":"publisher","unstructured":"Eisner C, Fisman D, Havlicek J, Lustig Y, McIsaac A, Campenhout DV (2003) Reasoning with temporal logic on truncated paths. In: Hunt WA, Somenzi F (ed) CAV 2003, LNCS, vol 2725, pp 27\u201339. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-540-45069-6_3","DOI":"10.1007\/978-3-540-45069-6_3"},{"issue":"42","key":"398_CR25","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"GE Fainekos","year":"2006","unstructured":"Fainekos GE, Pappas GJ (2006) Robustness of temporal logic specifications for continuous-time signals. Theor Comput Sci 410(42):4262\u20134291. https:\/\/doi.org\/10.1016\/j.tcs.2009.06.021","journal-title":"Theor Comput Sci"},{"key":"398_CR26","doi-asserted-by":"publisher","unstructured":"Falcone Y, S\u00e1nchez C (eds) (2016) RV 2016, LNCS, vol 10012. Springer, New York. https:\/\/doi.org\/10.1007\/978-3-319-46982-9","DOI":"10.1007\/978-3-319-46982-9"},{"key":"398_CR27","doi-asserted-by":"publisher","unstructured":"Faymonville P, Finkbeiner B, Schirmer S, Torfah H A stream-based specification language for network monitoring. In: Falcone and S\u00e1nchez [26], pp 152\u2013168. https:\/\/doi.org\/10.1007\/978-3-319-46982-9_10","DOI":"10.1007\/978-3-319-46982-9_10"},{"key":"398_CR28","doi-asserted-by":"crossref","unstructured":"Faymonville P, Finkbeiner B, Schledjewski M, Schwenger M, Tentrup L, Stenger M, Torfah H (2019) Streamlab: stream-based monitoring of cyber-physical systems. In: CAV 2019. To appear","DOI":"10.1007\/978-3-030-25540-4_24"},{"key":"398_CR29","doi-asserted-by":"publisher","unstructured":"Finkbeiner B, Keller A, Schmidt J, Schwenger M (2021) Robust monitoring for medical cyber-physical systems. In: MCPS 2021, pp 17\u201322. Association for computing machinery, New York, USA. https:\/\/doi.org\/10.1145\/3446913.3460318","DOI":"10.1145\/3446913.3460318"},{"issue":"3","key":"398_CR30","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/s10703-005-3399-3","volume":"27","author":"B Finkbeiner","year":"2005","unstructured":"Finkbeiner B, Sankaranarayanan S, Sipma H (2005) Collecting statistics over runtime executions. Form Methods Syst Des 27(3):253\u2013274. https:\/\/doi.org\/10.1007\/s10703-005-3399-3","journal-title":"Form Methods Syst Des"},{"key":"398_CR31","doi-asserted-by":"publisher","unstructured":"Finkbeiner B, Torfah H (2017) The density of linear-time properties. In: D\u2019Souza D, Kumar KN (ed) ATVA 2017, LNCS, vol 10482, pp 139\u2013155. Springer, New York. https:\/\/doi.org\/10.1007\/978-3-319-68167-2_10","DOI":"10.1007\/978-3-319-68167-2_10"},{"key":"398_CR32","doi-asserted-by":"publisher","unstructured":"Gastin P, Oddoux D (2001) Fast LTL to B\u00fcchi automata translation. In: Berry G, Comon H, Finkel A (ed) CAV 2001, LNCS, vol 2102, pp 53\u201365. Springer, New York. https:\/\/doi.org\/10.1007\/3-540-44585-4_6","DOI":"10.1007\/3-540-44585-4_6"},{"key":"398_CR33","doi-asserted-by":"publisher","unstructured":"Hall\u00e9 S When RV meets CEP. In: Falcone and S\u00e1nchez [26], pp 68\u201391. https:\/\/doi.org\/10.1007\/978-3-319-46982-9_6","DOI":"10.1007\/978-3-319-46982-9_6"},{"key":"398_CR34","doi-asserted-by":"publisher","unstructured":"Havelund K, Rosu G (2002) Synthesizing monitors for safety properties. In: Katoen J, Stevens P (ed) TACAS 2002, LNCS, vol 2280, pp 342\u2013356. Springer, New York. https:\/\/doi.org\/10.1007\/3-540-46002-0_24","DOI":"10.1007\/3-540-46002-0_24"},{"issue":"2","key":"398_CR35","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/B:FORM.0000017721.39909.4b","volume":"24","author":"K Havelund","year":"2004","unstructured":"Havelund K, Rosu G (2004) An overview of the runtime verification tool Java PathExplorer. Form Methods Syst Des 24(2):189\u2013215. https:\/\/doi.org\/10.1023\/B:FORM.0000017721.39909.4b","journal-title":"Form Methods Syst Des"},{"key":"398_CR36","doi-asserted-by":"publisher","unstructured":"Isberner M, Howar F, Steffen B (2015) The open-source learnlib - A framework for active automata learning. In: Kroening D, Pasareanu CS (ed) CAV 2015 (Part I), LNCS, vol 9206, pp 487\u2013495. Springer, New York. https:\/\/doi.org\/10.1007\/978-3-319-21690-4_32","DOI":"10.1007\/978-3-319-21690-4_32"},{"issue":"1","key":"398_CR37","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s10703-018-0319-x","volume":"53","author":"S Jaksic","year":"2018","unstructured":"Jaksic S, Bartocci E, Grosu R, Nguyen T, Nickovic D (2018) Quantitative monitoring of STL with edit distance. Form Methods Syst Des 53(1):83\u2013112. https:\/\/doi.org\/10.1007\/s10703-018-0319-x","journal-title":"Form Methods Syst Des"},{"key":"398_CR38","unstructured":"Kret\u00ednsk\u00fd J, Meggendorfer T, Sickert S (2018) LTL store: repository of LTL formulae from literature and case studies. arXiv:1807.03296"},{"key":"398_CR39","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd J, Meggendorfer T, Sickert S (2018) Owl: A library for $$\\omega $$-words, automata, and LTL. In: Lahiri, Wang [41], pp 543\u2013550. https:\/\/doi.org\/10.1007\/978-3-030-01090-4_34","DOI":"10.1007\/978-3-030-01090-4_34"},{"issue":"3","key":"398_CR40","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman O, Vardi MY (2001) Model checking of safety properties. Form Methods Syst Des 19(3):291\u2013314. https:\/\/doi.org\/10.1023\/A:1011254632723","journal-title":"Form Methods Syst Des"},{"key":"398_CR41","doi-asserted-by":"publisher","unstructured":"Lahiri SK, Wang C (eds) (2018) ATVA 2018, LNCS, vol 11138. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-030-01090-4","DOI":"10.1007\/978-3-030-01090-4"},{"key":"398_CR42","first-page":"279","volume-title":"PDPTA 1999","author":"I Lee","year":"1999","unstructured":"Lee I, Kannan S, Kim M, Sokolsky O, Viswanathan M (1999) Runtime assurance based on formal specifications. In: Arabnia HR (ed) PDPTA 1999. CSREA Press, Las Vegas, pp 279\u2013287"},{"key":"398_CR43","doi-asserted-by":"publisher","unstructured":"Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signals. In: Lakhnech Y, Yovine S (ed) FORMATS and FTRTFT 2004, LNCS, vol 3253, pp 152\u2013166. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"398_CR44","doi-asserted-by":"publisher","unstructured":"Maler O, Nickovic D, Pnueli A (2008) Checking temporal properties of discrete, timed and continuous behaviors. In: Avron A, Dershowitz N, Rabinovich A (ed) Pillars of computer science, essays dedicated to Boris (Boaz) Trakhtenbrot on the occasion of his 85th birthday, LNCS, vol 4800, pp 475\u2013505. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-540-78127-1_26","DOI":"10.1007\/978-3-540-78127-1_26"},{"key":"398_CR45","doi-asserted-by":"publisher","unstructured":"Maler O, Pnueli A (1995) Timing analysis of asynchronous circuits using timed automata. In: Camurati P, Eveking H (ed) CHARME 1995, LNCS, vol 987, pp 189\u2013205. Springer, Cham. https:\/\/doi.org\/10.1007\/3-540-60385-9_12","DOI":"10.1007\/3-540-60385-9_12"},{"key":"398_CR46","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal verification of reactive systems-safety","author":"Z Manna","year":"1995","unstructured":"Manna Z, Pnueli A (1995) Temporal verification of reactive systems-safety. Springer, Berlin"},{"key":"398_CR47","doi-asserted-by":"publisher","unstructured":"Mascle C, Neider D, Schwenger M, Tabuada P, Weinert A, Zimmermann M (2020) From LTL to rltl monitoring: improved monitorability through robust semantics. In: Ames AD, Seshia SA, Deshmukh J (ed) HSCC 2020, pp 7:1\u20137:12. ACM, New York. https:\/\/doi.org\/10.1145\/3365365.3382197","DOI":"10.1145\/3365365.3382197"},{"key":"398_CR48","doi-asserted-by":"publisher","unstructured":"Medhat R, Bonakdarpour B, Fischmeister S, Joshi Y (2016) Accelerated runtime verification of LTL specifications with counting semantics. In: Falcone and S\u00e1nchez [26], pp 251\u2013267. https:\/\/doi.org\/10.1007\/978-3-319-46982-9_16","DOI":"10.1007\/978-3-319-46982-9_16"},{"issue":"1","key":"398_CR49","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10703-017-0275-x","volume":"51","author":"P Moosbrugger","year":"2017","unstructured":"Moosbrugger P, Rozier KY, Schumann J (2017) R2U2: monitoring and diagnosis of security threats for unmanned aerial systems. Form Methods Syst Des 51(1):31\u201361. https:\/\/doi.org\/10.1007\/s10703-017-0275-x","journal-title":"Form Methods Syst Des"},{"key":"398_CR50","doi-asserted-by":"publisher","unstructured":"Neider D, Weinert A, Zimmermann M (2019) Robust, expressive, and quantitative linear temporal logics: pick any two for free. In: Leroux J, Raskin J (ed) Proceedings tenth international symposium on games, automata, logics, and formal verification, GandALF 2019, Bordeaux, 2\u20133rd Sept 2019, EPTCS, vol 305, pp 1\u201316. https:\/\/doi.org\/10.4204\/EPTCS.305.1","DOI":"10.4204\/EPTCS.305.1"},{"key":"398_CR51","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2021.104810","author":"D Neider","year":"2021","unstructured":"Neider D, Weinert A, Zimmermann M (2021) Robust, expressive, and quantitative linear temporal logics: pick any two for free. Inf Comput. https:\/\/doi.org\/10.1016\/j.ic.2021.104810","journal-title":"Inf Comput"},{"key":"398_CR52","doi-asserted-by":"publisher","unstructured":"Pike L, Goodloe A, Morisset R, Niller S (2010) Copilot: a hard real-time runtime monitor. In: Barringer H, Falcone Y, Finkbeiner B, Havelund K, Lee I, Pace GJ, Rosu G, Sokolsky O, Tillmann N (ed) RV 2010, LNCS, vol 6418, pp 345\u2013359. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-642-16612-9_26","DOI":"10.1007\/978-3-642-16612-9_26"},{"key":"398_CR53","doi-asserted-by":"publisher","unstructured":"Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: Misra J, Nipkow T, Sekerinski E (ed) FM 2006, LNCS, vol 4085, pp 573\u2013586. Springer, Cham. https:\/\/doi.org\/10.1007\/11813040_38","DOI":"10.1007\/11813040_38"},{"key":"398_CR54","doi-asserted-by":"publisher","unstructured":"Rodionova A, Bartocci E, Nickovic D, Grosu R (2016) Temporal logic as filtering. In: Proceedings of the 19th international conference on hybrid systems: computation and control, HSCC \u201916, pp 11\u201320. ACM, New York. https:\/\/doi.org\/10.1145\/2883817.2883839","DOI":"10.1145\/2883817.2883839"},{"key":"#cr-split#-398_CR55.1","unstructured":"Roesch M (1999) Snort: lightweight intrusion detection for networks. In: Parter DW"},{"key":"#cr-split#-398_CR55.2","unstructured":"(ed) LISA 1999, pp 229-238. USENIX, Berkeley"},{"key":"398_CR56","doi-asserted-by":"publisher","unstructured":"Schwoon S, Esparza J (2005) A note on on-the-fly verification algorithms. In: Halbwachs N, Zuck LD (ed) TACAS 2005, LNCS, vol 3440, pp 174\u2013190. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-540-31980-1_12","DOI":"10.1007\/978-3-540-31980-1_12"},{"key":"398_CR57","doi-asserted-by":"publisher","unstructured":"Silvetti S, Nenzi L, Bartocci E, Bortolussi L (2018) Signal convolution logic. In: Lahiri and Wang [41], pp 267\u2013283. https:\/\/doi.org\/10.1007\/978-3-030-01090-4_16","DOI":"10.1007\/978-3-030-01090-4_16"},{"key":"398_CR58","doi-asserted-by":"publisher","unstructured":"Tabuada P, Neider D (2016) Robust linear temporal logic. In: Talbot J, Regnier L (ed) CSL 2016, LIPIcs, vol 62, pp 10:1\u201310:21. Schloss Dagstuhl-LZI. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2016.10","DOI":"10.4230\/LIPIcs.CSL.2016.10"},{"issue":"3","key":"398_CR59","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s00236-016-0284-z","volume":"55","author":"H Torfah","year":"2018","unstructured":"Torfah H, Zimmermann M (2018) The complexity of counting models of linear-time temporal logic. Acta Inf 55(3):191\u2013212. https:\/\/doi.org\/10.1007\/s00236-016-0284-z","journal-title":"Acta Inf"},{"key":"398_CR60","doi-asserted-by":"publisher","unstructured":"Zhang X, Leucker M, Dong W (2012) Runtime verification with predictive semantics. In: Goodloe A, Person S (ed) NFM 2012, LNCS, vol 7226, pp 418\u2013432. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-642-28891-3_37","DOI":"10.1007\/978-3-642-28891-3_37"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-022-00398-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-022-00398-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-022-00398-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,27]],"date-time":"2022-12-27T10:16:03Z","timestamp":1672136163000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-022-00398-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12]]},"references-count":61,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["398"],"URL":"https:\/\/doi.org\/10.1007\/s10703-022-00398-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2021,12]]},"assertion":[{"value":"28 June 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 September 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 October 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}