{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T07:40:02Z","timestamp":1750318802157,"version":"3.41.0"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T00:00:00Z","timestamp":1712361600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T00:00:00Z","timestamp":1712361600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"name":"Madrid Regional Government","award":["S2018\/TCS-4339 (BLOQUES-CM)","S2018\/TCS-4339 (BLOQUES-CM)"],"award-info":[{"award-number":["S2018\/TCS-4339 (BLOQUES-CM)","S2018\/TCS-4339 (BLOQUES-CM)"]}]},{"name":"PRODIGY","award":["TED2021-132464B-I00","TED2021-132464B-I00"],"award-info":[{"award-number":["TED2021-132464B-I00","TED2021-132464B-I00"]}]},{"name":"MCIN\/AEI","award":["10.13039\/501100011033\/","10.13039\/501100011033\/"],"award-info":[{"award-number":["10.13039\/501100011033\/","10.13039\/501100011033\/"]}]},{"name":"European Union NextGenerationEU\/PRTR"},{"name":"Nomadic Labs and the Tezos Foundation"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2025,6]]},"DOI":"10.1007\/s11334-024-00557-2","type":"journal-article","created":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T13:01:47Z","timestamp":1712408507000},"page":"673-686","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["General monitorability of totally ordered verdict domains"],"prefix":"10.1007","volume":"21","author":[{"given":"Felipe","family":"Gorostiaga","sequence":"first","affiliation":[]},{"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,6]]},"reference":[{"key":"557_CR1","doi-asserted-by":"crossref","unstructured":"Havelund K, Peled D (2018) Runtime verification: from propositional to first-order temporal logic. In: Proceeding of the 18th international conference on runtime verification (RV\u201918). LNCS, vol 11237, pp 90\u2013112. Springer, Berlin, Heidelberg","DOI":"10.1007\/978-3-030-03769-7_7"},{"key":"557_CR2","doi-asserted-by":"crossref","unstructured":"Emerson EA, Clarke EM (1980) Characterizing correctness properties of parallel programs using fixpoints. In: Proceeding of the 7th colloquium on automata, languages and programming (ICALP\u201980). LNCS, vol 85, pp 169\u2013181. Springer, Berlin, Heidelberg","DOI":"10.1007\/3-540-10003-2_69"},{"key":"557_CR3","doi-asserted-by":"crossref","unstructured":"Queille J-P, Sifakis J (1982) Specification and verification of concurrent systems in CESAR. In: Symposium on programming. LNCS, vol 137, pp 337\u2013351, Springer, Berlin, Heidelberg","DOI":"10.1007\/3-540-11494-7_22"},{"key":"557_CR4","doi-asserted-by":"crossref","unstructured":"Havelund K, Goldberg A (2005) Verify your runs. In: Proceeding of the first IFIP TC 2\/WG 2.3 conference on verified software: theories, tools, experiments (VSTTE\u201905). LNCS, vol 4171, pp 374\u2013383. Springer, Berlin, Heidelberg","DOI":"10.1007\/978-3-540-69149-5_40"},{"issue":"5","key":"557_CR5","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 (2009) A brief account of runtime verification. J Logic Algebr Programm 78(5):293\u2013303","journal-title":"J Logic Algebr Programm"},{"key":"557_CR6","doi-asserted-by":"crossref","unstructured":"Bartocci E, Falcone Y (eds.) (2018) Lectures on runtime verification-introductory and advanced topics. LNCS, vol 10457. Springer, Berlin, Heidelberg","DOI":"10.1007\/978-3-319-75632-5"},{"key":"557_CR7","doi-asserted-by":"crossref","unstructured":"Havelund K, Ro\u015fu G (2002) Synthesizing monitors for safety properties. In: Proceeding of the 8th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201902). LNCS, vol 2280, pp 342\u2013356. Springer, Berlin, Heidelberg","DOI":"10.1007\/3-540-46002-0_24"},{"key":"557_CR8","doi-asserted-by":"crossref","unstructured":"Eisner C, Fisman D, Havlicek J, Lustig Y, McIsaac A, Campenhout DV (2003) Reasoning with temporal logic on truncated paths. In: Proceeding of the 15th international conference on computer aided verification (CAV\u201903). LNCS, vol 2725, pp 27\u201339. Springer, Berlin, Heidelberg","DOI":"10.1007\/978-3-540-45069-6_3"},{"issue":"4","key":"557_CR9","doi-asserted-by":"publisher","first-page":"14","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","journal-title":"ACM Trans Softw Eng Methodol"},{"issue":"2","key":"557_CR10","first-page":"226","volume":"89","author":"K Sen","year":"2003","unstructured":"Sen K, Ro\u015fu G (2003) Generating optimal monitors for extended regular expressions. ENTCS 89(2):226\u2013245","journal-title":"ENTCS"},{"issue":"2","key":"557_CR11","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1145\/506147.506151","volume":"49","author":"E Asarin","year":"2002","unstructured":"Asarin E, Caspi P, Maler O (2002) Timed regular expressions. J ACM 49(2):172\u2013206","journal-title":"J ACM"},{"key":"557_CR12","doi-asserted-by":"crossref","unstructured":"Barringer H, Goldberg A, Havelund K, Sen K (2004) Rule-based runtime verification. In: Proceeding of the 5th international conference on verification, model checking and abstract interpretation (VMCAI\u201904). LNCS, vol 2937, pp 44\u201357. Springer, Berlin, Heidelberg","DOI":"10.1007\/978-3-540-24622-0_5"},{"issue":"2","key":"557_CR13","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/s10515-005-6205-y","volume":"12","author":"G Ro\u015fu","year":"2005","unstructured":"Ro\u015fu G, Havelund K (2005) Rewriting-based techniques for runtime verification. Autom Softw Eng 12(2):151\u2013197","journal-title":"Autom Softw Eng"},{"key":"557_CR14","doi-asserted-by":"crossref","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: Proceeding of the 12th international symposium of temporal representation and reasoning (TIME\u201905), pp 166\u2013174. IEEE CS Press, Burlington, VT, USA","DOI":"10.1109\/TIME.2005.26"},{"key":"557_CR15","unstructured":"De\u00a0Giacomo G, Vardi MY (2013) Linear temporal logic and linear dynamic logic on finite traces. In: Proceeding of the 23rd international joint conference on artificial intelligence (IJCAI\u201914), pp 854\u2013860. AAAI Press, Palo Alto, California"},{"key":"557_CR16","doi-asserted-by":"crossref","unstructured":"Reinbacher T, Rozier KY, Schumann J (2014) Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Proceeding of the 20th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201914). LNCS, vol 8413, pp 357\u2013372. Springer, Berlin, Heidelberg","DOI":"10.1007\/978-3-642-54862-8_24"},{"key":"557_CR17","doi-asserted-by":"crossref","unstructured":"Bauer A, Leucker M, Schallhart C (2007) The good, the bad, and the ugly\u2014but how ugly is ugly? In: Proceeding of the 7th international workshop on runtime verification (RV\u201907). LNCS, vol 4839, pp 126\u2013138. Springer, Berlin, Heidelberg","DOI":"10.1007\/978-3-540-77395-5_11"},{"key":"557_CR18","doi-asserted-by":"publisher","unstructured":"Stucki S, S\u00e1nchez C, Schneider G, Bonakdarpour B (2019) Gray-box monitoring of hyperproperties. In: Ter Beek MH, McIver A, Oliveira JN (eds.) Formal methods\u2014the next 30 years-third world congress, FM 2019. Lecture Notes in Computer Science, vol 11800, pp 406\u2013424. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-030-30942-8_25","DOI":"10.1007\/978-3-030-30942-8_25"},{"key":"557_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-020-00358-w","author":"S Stucki","year":"2020","unstructured":"Stucki S, S\u00e1nchez C, Schneider G, Bonarkdarpour B (2020) Gray-box monitoring of hyperproperties with an application to privacy. Formal Methods Syst Desing. https:\/\/doi.org\/10.1007\/s10703-020-00358-w","journal-title":"Formal Methods Syst Desing"},{"key":"557_CR20","doi-asserted-by":"crossref","unstructured":"Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: Proceeding of the 14th international symposium on formal methods (FM\u201906). LNCS, vol 4085, pp 573\u2013586. Springer, Berlin, Heidelberg","DOI":"10.1007\/11813040_38"},{"issue":"2","key":"557_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2699444","volume":"62","author":"DA Basin","year":"2015","unstructured":"Basin DA, Klaedtke F, M\u00fcller S, Zalinescu E (2015) Monitoring metric first-order temporal properties. J ACM 62(2):1\u201345","journal-title":"J ACM"},{"key":"557_CR22","doi-asserted-by":"crossref","unstructured":"Colombo C, Pace GJ, Schneider G (2008) Dynamic event-based runtime monitoring of real-time and contextual properties. In: Proceeding of the 13th international workshop on formal methods for industrial critical systems (FMICS\u201908). LNCS, vol 5596, pp 135\u2013149. Springer, Berlin, Heidelberg","DOI":"10.1007\/978-3-642-03240-0_13"},{"issue":"3","key":"557_CR23","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.entcs.2008.11.019","volume":"220","author":"M Faella","year":"2008","unstructured":"Faella M, Legay A, Stoelinga M (2008) Model checking quantitative linear time logic. Electron Notes Theor Comput Sci 220(3):61\u201377. https:\/\/doi.org\/10.1016\/j.entcs.2008.11.019","journal-title":"Electron Notes Theor Comput Sci"},{"key":"557_CR24","doi-asserted-by":"publisher","unstructured":"S\u00e1nchez C (2018) Online and offline stream runtime verification of synchronous systems. In: Proceeding of the 18th international conference on runtime verification (RV\u201918). LNCS, vol 11237, pp 138\u2013163. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-030-03769-7_9","DOI":"10.1007\/978-3-030-03769-7_9"},{"key":"557_CR25","doi-asserted-by":"publisher","unstructured":"Faymonville P, Finkbeiner B, Schirmer S, Torfah H (2016) A stream-based specification language for network monitoring. In: Proceeding of the 16th international conference on runtime verification (RV\u201916). LNCS, vol 10012, pp 152\u2013168. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-319-46982-9_10","DOI":"10.1007\/978-3-319-46982-9_10"},{"key":"557_CR26","doi-asserted-by":"crossref","unstructured":"Gorostiaga F, S\u00e1nchez C (2018) Striver: stream runtime verification for real-time event-streams. In: Proceeding of the 18th international conference on runtime verification (RV\u201918). LNCS, vol 11237, pp 282\u2013298. Springer, Berlin, Heidelberg","DOI":"10.1007\/978-3-030-03769-7_16"},{"key":"557_CR27","doi-asserted-by":"crossref","unstructured":"Convent L, Hungerecker S, Leucker M, Scheffel T, Schmitz M, Thoma D (2018) TeSSLa: temporal stream-based specification language. In: Proceeding of the 21st Brazilian symposium on formal methods (SBMF\u201918). LNCS, vol 11254. Springer, Berlin, Heidelberg","DOI":"10.1007\/978-3-030-03044-5_10"},{"key":"557_CR28","doi-asserted-by":"publisher","unstructured":"Henzinger TA, Sara\u00e7 NE (2021) Quantitative and approximate monitoring. In: Proceedings of the 36th annual ACM\/IEEE symposium on logic in computer science. LICS \u201921. Association for Computing Machinery, New York, NY, USA. https:\/\/doi.org\/10.1109\/LICS52264.2021.9470547","DOI":"10.1109\/LICS52264.2021.9470547"},{"key":"557_CR29","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.ins.2016.10.030","volume":"377","author":"Y Li","year":"2017","unstructured":"Li Y, Droste M, Lei L (2017) Model checking of linear-time properties in multi-valued systems. Inf Sci 377:51\u201374. https:\/\/doi.org\/10.1016\/j.ins.2016.10.030","journal-title":"Inf Sci"},{"key":"557_CR30","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Mazzocchi N, E NS (2023) Quantitative safety and liveness. In: Proceeding of the 26th international conference on foundations of software science and computation structures (FoSSaCS\u201923). LNCS, vol 13992, pp 349\u2013370. Springer, Cham","DOI":"10.1007\/978-3-031-30829-1_17"},{"key":"557_CR31","doi-asserted-by":"publisher","unstructured":"Alpern B, Schneider FB (1985) Defining liveness. Inf Process Lett 21(4):181\u2013185. https:\/\/doi.org\/10.1016\/0020-0190(85)90056-0","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"557_CR32","doi-asserted-by":"crossref","unstructured":"Zhang X, Leucker M, Dong W (2012) Runtime verification with predictive semantics. In: Proceeding of the 4th international symposium NASA formal methods (NFM\u201912). LNCS, pp 418\u2013432. Springer, Berlin, Heidelberg","DOI":"10.1007\/978-3-642-28891-3_37"},{"key":"557_CR33","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Sara\u00e7 NE (2020) Monitorability under assumptions. In: Proceeding of the 20th international conference on runtime verification (RV\u201920). LNCS, vol 12399, pp 3\u201318. Springer, Berlin, Heidelberg","DOI":"10.1007\/978-3-030-60508-7_1"},{"key":"557_CR34","doi-asserted-by":"crossref","unstructured":"Leucker M, S\u00e1nchez C, Scheffel T, Schmitz M, Thoma D (2019) Runtime verification for timed event streams with partial information. In: Proceeding of the 19th international conference on runtime verification (RV\u201919). LNCS, vol 11757, pp 273\u2013291. Springer, Berlin, Heidelberg","DOI":"10.1007\/978-3-030-32079-9_16"},{"key":"557_CR35","unstructured":"Kauffman S, Havelund K, Fischmeister S (2020) What can we monitor over unreliable channels? Int J Softw Tools Technol Trans 1\u201324"},{"key":"557_CR36","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/3-540-55719-9_97","volume-title":"Automata, languages and programming","author":"E Chang","year":"1992","unstructured":"Chang E, Manna Z, Pnueli A (1992) Characterization of temporal property classes. In: Kuich W (ed) Automata, languages and programming. Springer, Berlin, pp 474\u2013486"},{"key":"557_CR37","doi-asserted-by":"publisher","unstructured":"Kallwies H, Leucker M, S\u00e1nchez C, Scheffel T (2022) Anticipatory recurrent monitoring with uncertainty and assumptions. In: Proceeding of the 22nd international conference on runtime verification (RV\u201922). LNCS, vol 13498, pp 181\u2013199. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-031-17196-3_10","DOI":"10.1007\/978-3-031-17196-3_10"},{"key":"557_CR38","doi-asserted-by":"publisher","unstructured":"Gorostiaga F, S\u00e1nchez C (2022) Monitorability of expressive verdicts. In: Proceeding of the 14th international symposium on NASA formal methods (NFM\u201922). LNCS, vol 13260, pp 693\u2013712. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-031-06773-0_37","DOI":"10.1007\/978-3-031-06773-0_37"},{"key":"557_CR39","doi-asserted-by":"crossref","unstructured":"Almagor S, Boker U, Kupferman O (2014) Discounting in LTL. In: Proceeding of the 20th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201914). LNCS, vol 8413, pp 424\u2013439. Springer, Berlin, Heidelberg","DOI":"10.1007\/978-3-642-54862-8_37"},{"key":"557_CR40","doi-asserted-by":"publisher","unstructured":"Laroussinie F, Meyer A, Petonnet E (2010) Counting LTL. In: Proceeding of the 2010 17th international symposium on temporal representation and reasoning (TIME\u201910), pp 51\u201358. IEEE, Burlington, VT, USA. https:\/\/doi.org\/10.1109\/TIME.2010.20","DOI":"10.1109\/TIME.2010.20"},{"key":"557_CR41","unstructured":"Tabuada P, Neider D (2016) Robust linear temporal logic. In: Proceeding of the 25th EACSL annual conference on computer science logic (CSL\u201916). LIPIcs, vol 62, pp 10\u201311021. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Marseille, France"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-024-00557-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-024-00557-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-024-00557-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T07:05:36Z","timestamp":1750316736000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-024-00557-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,6]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6]]}},"alternative-id":["557"],"URL":"https:\/\/doi.org\/10.1007\/s11334-024-00557-2","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"type":"print","value":"1614-5046"},{"type":"electronic","value":"1614-5054"}],"subject":[],"published":{"date-parts":[[2024,4,6]]},"assertion":[{"value":"14 February 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 February 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 April 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no Conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}