{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T03:53:50Z","timestamp":1768708430434,"version":"3.49.0"},"reference-count":39,"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,8,18]],"date-time":"2022-08-18T00:00:00Z","timestamp":1660780800000},"content-version":"vor","delay-in-days":260,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"royal academy of engineering, under the chairs in emerging technologies scheme"},{"name":"ukri\u2019s tas node in verifiability","award":["EP\/V026801"],"award-info":[{"award-number":["EP\/V026801"]}]},{"name":"ukri\u2019s tas node in verifiability","award":["EP\/V026801"],"award-info":[{"award-number":["EP\/V026801"]}]},{"name":"royal academy of engineering, under the chairs in emerging technologies scheme"},{"DOI":"10.13039\/501100004702","name":"Universit\u00e0 degli Studi di Genova","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004702","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>This paper presents an extension of the Predictive Runtime Verification (PRV) paradigm to consider multiple models of the System Under Analysis (SUA). We call this extension <jats:italic>Multi-Model<\/jats:italic> PRV. Typically, PRV attempts to predict the satisfaction or violation of a property based on a trace and a (single) formal model of the SUA. However, contemporary node- or component-based systems (e.g. robotic systems) may benefit from monitoring based on a model of each component. We show how a Multi-Model PRV approach can be applied in either a <jats:italic>centralised<\/jats:italic> or a <jats:italic>compositional<\/jats:italic> way (where the property is compositional), as best suits the SUA. Crucially, our approach is formalism-agnostic. We demonstrate our approach using an illustrative example of a Mars Curiosity rover simulation and evaluate our contribution via a prototype implementation.<\/jats:p>","DOI":"10.1007\/s10703-022-00395-7","type":"journal-article","created":{"date-parts":[[2022,8,18]],"date-time":"2022-08-18T16:03:17Z","timestamp":1660838597000},"page":"44-76","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Bridging the gap between single- and multi-model predictive runtime verification"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8711-4670","authenticated-orcid":false,"given":"Angelo","family":"Ferrando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rafael C.","family":"Cardoso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marie","family":"Farrell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matt","family":"Luckcuck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabio","family":"Papacchini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viviana","family":"Mascardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,18]]},"reference":[{"key":"395_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126:183\u2013235","journal-title":"Theor Comput Sci"},{"key":"395_CR2","doi-asserted-by":"crossref","unstructured":"Ancona D, Ferrando A, Mascardi V (2016) Comparing trace expressions and linear temporal logic for runtime verification. In: Theory and practice of formal methods-essays dedicated to Frank de Boer on the Occasion of His 60th Birthday, LNCS, vol 9660, pp 47\u201364. Springer","DOI":"10.1007\/978-3-319-30734-3_6"},{"key":"395_CR3","doi-asserted-by":"crossref","unstructured":"Babaee R, Gurfinkel A, Fischmeister S (2018) Prevent : a predictive run-time verification framework using statistical learning. In: Software engineering and formal methods, LNCS, vol 10886, pp 205\u2013220. Springer","DOI":"10.1007\/978-3-319-92970-5_13"},{"key":"395_CR4","doi-asserted-by":"crossref","unstructured":"Bartocci E, Grosu R, Karmarkar A, Smolka SA, Stoller SD, Zadok E, Seyster J (2013) Adaptive runtime verification. In: Runtime verification, LNCS, vol 7687, pp 168\u2013182. Springer","DOI":"10.1007\/978-3-642-35632-2_18"},{"key":"395_CR5","doi-asserted-by":"crossref","unstructured":"Bauer A, Leucker M, Schallhart C (2006) Monitoring of real-time properties. In: Foundations of software technology and theoretical computer science, LNCS, vol 4337, pp 260\u2013272. Springer","DOI":"10.1007\/11944836_25"},{"key":"395_CR6","doi-asserted-by":"crossref","unstructured":"Bauer A, Leucker M, Schallhart C (2007) The good, the bad, and the ugly, but how ugly is ugly? In: Runtime verification, LNCS, vol 4839, pp 126\u2013138. Springer","DOI":"10.1007\/978-3-540-77395-5_11"},{"issue":"3","key":"395_CR7","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 Logic Comput 20(3):651\u2013674","journal-title":"J Logic Comput"},{"issue":"4","key":"395_CR8","doi-asserted-by":"publisher","first-page":"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):1\u201314","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"395_CR9","doi-asserted-by":"crossref","unstructured":"Blech JO, Falcone Y, Becker K (2012) Towards certified runtime verification. In: Formal methods and software engineering, LNCS, vol 7635, pp 494\u2013509. Springer","DOI":"10.1007\/978-3-642-34281-3_34"},{"key":"395_CR10","doi-asserted-by":"crossref","unstructured":"Cardoso RC, Farrell M, Luckcuck M, Ferrando A, Fisher M (2020) Heterogeneous verification of an autonomous curiosity rover. In: NASA formal methods symposium, LNCS, vol 12229, pp 353\u2013360. Springer","DOI":"10.1007\/978-3-030-55754-6_20"},{"issue":"1\u20132","key":"395_CR11","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10703-016-0251-x","volume":"49","author":"C Colombo","year":"2016","unstructured":"Colombo C, Falcone Y (2016) Organising LTL monitors over distributed systems with a global clock. Formal Methods Syst. Des. 49(1\u20132):109\u2013158. https:\/\/doi.org\/10.1007\/s10703-016-0251-x","journal-title":"Formal Methods Syst. Des."},{"key":"395_CR12","doi-asserted-by":"publisher","unstructured":"Couvreur J (1999) On-the-fly verification of linear temporal logic. In: JM Wing, J\u00a0Woodcock, J\u00a0Davies (eds.) FM\u201999-Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20\u201324, 1999, Proceedings, Volume I, Lecture Notes in Computer Science, vol 1708, pp 253\u2013271. Springer . https:\/\/doi.org\/10.1007\/3-540-48119-2_16","DOI":"10.1007\/3-540-48119-2_16"},{"key":"395_CR13","doi-asserted-by":"publisher","unstructured":"Daniele M, Giunchiglia F, Vardi MY (1999) Improved automata generation for linear temporal logic. In: N\u00a0Halbwachs, DA Peled (eds.) Computer aided verification, 11th International Conference, CAV \u201999, Trento, Italy, July 6\u201310, 1999, Proceedings, Lecture Notes in Computer Science, vol 1633, pp 249\u2013260. Springer. https:\/\/doi.org\/10.1007\/3-540-48683-6_23","DOI":"10.1007\/3-540-48683-6_23"},{"issue":"2\u20133","key":"395_CR14","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/s10703-016-0261-8","volume":"50","author":"JV Deshmukh","year":"2017","unstructured":"Deshmukh JV, Majumdar R, Prabhu VS (2017) Quantifying conformance using the Skorokhod metric. Formal Methods Syst Des 50(2\u20133):168\u2013206. https:\/\/doi.org\/10.1007\/s10703-016-0261-8","journal-title":"Formal Methods Syst Des"},{"key":"395_CR15","doi-asserted-by":"publisher","unstructured":"Duret-Lutz A, Poitrenaud D (2004) SPOT: an extensible model checking library using transition-based generalized b\u00fcchi automata. In: D\u00a0DeGroot, PG Harrison, HAG Wijshoff, Z\u00a0Segall (eds.) 12th International Workshop on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS 2004), 4\u20138 October 2004, Vollendam, pp 76\u201383. IEEE Computer Society. https:\/\/doi.org\/10.1109\/MASCOT.2004.1348184","DOI":"10.1109\/MASCOT.2004.1348184"},{"key":"395_CR16","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: Computer aided verification, LNCS, vol 2725, pp 27\u201339. Springer","DOI":"10.1007\/978-3-540-45069-6_3"},{"issue":"1","key":"395_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3355181","volume":"29","author":"A El-Hokayem","year":"2020","unstructured":"El-Hokayem A, Falcone Y (2020) On the monitoring of decentralized specifications: semantics, properties, analysis, and simulation. ACM Trans Softw Eng Methodol 29(1):1\u201357","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"395_CR18","doi-asserted-by":"publisher","unstructured":"Etessami K, Holzmann GJ (2000) Optimizing b\u00fcchi automata. In: C\u00a0Palamidessi (ed.) CONCUR 2000-concurrency theory, 11th International Conference, University Park, PA, USA, August 22\u201325, 2000, Proceedings, Lecture Notes in Computer Science, vol 1877, pp 153\u2013167. Springer. https:\/\/doi.org\/10.1007\/3-540-44618-4_13","DOI":"10.1007\/3-540-44618-4_13"},{"key":"395_CR19","doi-asserted-by":"crossref","unstructured":"Falcone Y, Jaber M, Nguyen TH, Bozga M, Bensalem S (2011) Runtime verification of component-based systems. In: Software Engineering and Formal Methods, LNCS, vol 7041, pp 204\u2013220. Springer","DOI":"10.1007\/978-3-642-24690-6_15"},{"key":"395_CR20","doi-asserted-by":"crossref","unstructured":"Ferrando A, Cardoso RC, Fisher M, Ancona D, Franceschini L, Mascardi V (2020) ROSMonitoring: a runtime verification framework for ROS. In: towards autonomous robotic systems conference, LNCS, vol 12228, pp 387\u2013399. Springer","DOI":"10.1007\/978-3-030-63486-5_40"},{"key":"395_CR21","unstructured":"Ferrando A, Dennis LA, Ancona D, Fisher M, Mascardi V (2018) Recognising assumption violations in autonomous systems verificaion. In: Autonomous agents and multiagent systems, pp 1933\u20131935. IFAAMAS\/ACM"},{"key":"395_CR22","doi-asserted-by":"crossref","unstructured":"Francalanza A, P\u00e9rez JA, S\u00e1nchez C (2018) Runtime verification for decentralised and distributed systems. In: Lectures on runtime verification, LNCS, vol 10457, pp 176\u2013210. Springer","DOI":"10.1007\/978-3-319-75632-5_6"},{"key":"395_CR23","doi-asserted-by":"crossref","unstructured":"Havelund K, Goldberg A (2005) Verify your runs. In: Verified software: theories, tools, experiments, LNCS, vol 4171, pp 374\u2013383. Springer","DOI":"10.1007\/978-3-540-69149-5_40"},{"key":"395_CR24","volume-title":"Introduction to automata. Theory Addison\u2013Wesley, languages and computation","author":"JE Hopcroft","year":"1979","unstructured":"Hopcroft JE, Ullman JD (1979) Introduction to automata. Theory Addison\u2013Wesley, languages and computation. Longman, London"},{"key":"395_CR25","doi-asserted-by":"crossref","unstructured":"Huang J, Erdogan C, Zhang Y, Moore B, Luo Q, Sundaresan A, Rosu G (2014) ROSRV: runtime verification for robots. In: Runtime verification, LNCS, vol 8734, pp 247\u2013254. Springer","DOI":"10.1007\/978-3-319-11164-3_20"},{"issue":"1","key":"395_CR26","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s10703-018-0319-x","volume":"53","author":"S Jak\u0161i\u0107","year":"2018","unstructured":"Jak\u0161i\u0107 S, Bartocci E, Grosu R, Nguyen T, Ni\u010dkovi\u0107 D (2018) Quantitative monitoring of STL with edit distance. Formal Methods Syst Des 53(1):83\u2013112. https:\/\/doi.org\/10.1007\/s10703-018-0319-x","journal-title":"Formal Methods Syst Des"},{"issue":"4","key":"395_CR27","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans R (1990) Specifying real-time properties with metric temporal logic. Real Time Syst 2(4):255\u2013299","journal-title":"Real Time Syst"},{"key":"395_CR28","doi-asserted-by":"crossref","unstructured":"Leucker M (2012) Sliding between model checking and runtime verification. In: Runtime verification, LNCS, vol 7687, pp 82\u201387. Springer","DOI":"10.1007\/978-3-642-35632-2_10"},{"key":"395_CR29","doi-asserted-by":"crossref","unstructured":"Lichtenstein O, Pnueli A, Zuck LD (1985) The glory of the past. In: Logics of programs, LNCS, vol 193, pp 196\u2013218. Springer","DOI":"10.1007\/3-540-15648-8_16"},{"key":"395_CR30","doi-asserted-by":"crossref","unstructured":"Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signals. In: Formal techniques, modelling and analysis of timed and fault-tolerant systems, LNCS, vol 3253, pp 152\u2013166. Springer","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"395_CR31","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1016\/j.jss.2017.06.060","volume":"132","author":"S Pinisetty","year":"2017","unstructured":"Pinisetty S, J\u00e9ron T, Tripakis S, Falcone Y, Marchand H, Preoteasa V (2017) Predictive runtime verification of timed properties. J Syst Softw 132:353\u2013365","journal-title":"J Syst Softw"},{"key":"395_CR32","doi-asserted-by":"publisher","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, Providence, Rhode Island, USA, 31 October-1 November 1977, pp 46\u201357. IEEE Computer Society. https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"395_CR33","doi-asserted-by":"publisher","unstructured":"Pnueli A, Zaks A (2008) On the merits of temporal testers. In: O\u00a0Grumberg, H\u00a0Veith (eds.) 25 Years of model checking-history, achievements, perspectives, Lecture Notes in Computer Science, vol 5000, pp 172\u2013195. Springer. https:\/\/doi.org\/10.1007\/978-3-540-69850-0_11","DOI":"10.1007\/978-3-540-69850-0_11"},{"key":"395_CR34","doi-asserted-by":"publisher","unstructured":"Qin X, Deshmukh JV (2020) Clairvoyant monitoring for signal temporal logic. In: N\u00a0Bertrand, N Jansen (eds.) Formal modeling and analysis of timed systems, vol 12288, pp 178\u2013195. Springer International Publishing. https:\/\/doi.org\/10.1007\/978-3-030-57628-8_11. Lecture Notes in Computer Science","DOI":"10.1007\/978-3-030-57628-8_11"},{"issue":"2","key":"395_CR35","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/S1571-0661(04)80409-2","volume":"66","author":"X Thirioux","year":"2002","unstructured":"Thirioux X (2002) Simple and efficient translation from LTL formulas to Buchi automata. Electron Notes Theor Comput Sci 66(2):145\u2013159. https:\/\/doi.org\/10.1016\/S1571-0661(04)80409-2","journal-title":"Electron Notes Theor Comput Sci"},{"key":"395_CR36","unstructured":"Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the symposium on logic in computer science, pp 332\u2013344. IEEE Computer Society"},{"key":"395_CR37","doi-asserted-by":"crossref","unstructured":"Yoon H, Chou Y, Chen X, Frew EW, Sankaranarayanan S (2019) Predictive runtime monitoring for linear stochastic systems and applications to geofence enforcement for UAVs. In: Runtime verification, LNCS, vol 11757, pp 349\u2013367. Springer","DOI":"10.1007\/978-3-030-32079-9_20"},{"key":"395_CR38","doi-asserted-by":"crossref","unstructured":"Yu K, Chen Z, Dong W (2014) A predictive runtime verification framework for cyber-physical systems. In: Software security and reliability-companion, pp. 223\u2013227. IEEE","DOI":"10.1109\/SERE-C.2014.43"},{"key":"395_CR39","doi-asserted-by":"crossref","unstructured":"Zhang X, Leucker M, Dong W (2012) Runtime verification with predictive semantics. In: NASA formal methods, LNCS, vol 7226, pp 418\u2013432. Springer","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-00395-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-022-00395-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-022-00395-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,27]],"date-time":"2022-12-27T10:17:55Z","timestamp":1672136275000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-022-00395-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12]]},"references-count":39,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["395"],"URL":"https:\/\/doi.org\/10.1007\/s10703-022-00395-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,12]]},"assertion":[{"value":"21 June 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 July 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 August 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"Not applicable.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}