{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T17:04:30Z","timestamp":1785258270243,"version":"3.55.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032054340","type":"print"},{"value":"9783032054357","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T00:00:00Z","timestamp":1757635200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T00:00:00Z","timestamp":1757635200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-05435-7_9","type":"book-chapter","created":{"date-parts":[[2025,9,13]],"date-time":"2025-09-13T01:30:37Z","timestamp":1757727037000},"page":"140-159","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Alignment Monitoring"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2985-7724","authenticated-orcid":false,"given":"Thomas A.","family":"Henzinger","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8974-2542","authenticated-orcid":false,"given":"Konstantin","family":"Kueffner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-5468-7899","authenticated-orcid":false,"given":"Vasu","family":"Singh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-2194-9526","authenticated-orcid":false,"given":"I.","family":"Sun","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,9,12]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Abbas, H., Mittelmann, H., Fainekos, G.: Formal property verification in a conformance testing framework. In: 2014 Twelfth ACM IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 155\u2013164 (2014)","DOI":"10.1109\/MEMCOD.2014.6961854"},{"key":"9_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.18637\/jss.v110.i08","volume":"110","author":"S Allen","year":"2024","unstructured":"Allen, S.: Weighted scoringrules: emphasizing particular outcomes when evaluating probabilistic forecasts. J. Stat. Softw. 110, 1\u201326 (2024)","journal-title":"J. Stat. Softw."},{"issue":"3","key":"9_CR3","doi-asserted-by":"publisher","first-page":"906","DOI":"10.1137\/22M1532184","volume":"11","author":"S Allen","year":"2023","unstructured":"Allen, S., Ginsbourger, D., Ziegel, J.: Evaluating forecasts for high-impact events using transformed kernel scores. SIAM\/ASA J. Uncertain. Quant. 11(3), 906\u2013940 (2023)","journal-title":"SIAM\/ASA J. Uncertain. Quant."},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Ashok, P., Kwiatkowska, M.: Pac statistical model checking for Markov decision processes and stochastic games. In: TACAS (2019)","DOI":"10.1007\/978-3-030-25540-4_29"},{"issue":"8","key":"9_CR5","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1016\/j.jprocont.2009.04.007","volume":"19","author":"AS Badwe","year":"2009","unstructured":"Badwe, A.S., Gudi, R.D., Patwardhan, R.S., Shah, S.L., Patwardhan, S.C.: Detection of model-plant mismatch in mpc applications. J. Process Control 19(8), 1305\u20131313 (2009)","journal-title":"J. Process Control"},{"issue":"4","key":"9_CR6","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1016\/j.jprocont.2009.12.006","volume":"20","author":"AS Badwe","year":"2010","unstructured":"Badwe, A.S., Patwardhan, R.S., Shah, S.L., Patwardhan, S.C., Gudi, R.D.: Quantifying the impact of model-plant mismatch on controller performance. J. Process Control 20(4), 408\u2013425 (2010)","journal-title":"J. Process Control"},{"key":"9_CR7","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT press, Cambridge (2008)"},{"issue":"356","key":"9_CR8","doi-asserted-by":"publisher","first-page":"791","DOI":"10.1080\/01621459.1976.10480949","volume":"71","author":"GE Box","year":"1976","unstructured":"Box, G.E.: Science and statistics. J. Am. Stat. Assoc. 71(356), 791\u2013799 (1976)","journal-title":"J. Am. Stat. Assoc."},{"issue":"4","key":"9_CR9","doi-asserted-by":"publisher","first-page":"1368","DOI":"10.1287\/opre.2021.0792","volume":"72","author":"YJ Choe","year":"2024","unstructured":"Choe, Y.J., Ramdas, A.: Comparing sequential forecasters. Oper. Res. 72(4), 1368\u20131387 (2024)","journal-title":"Oper. Res."},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-67531-2_11","volume-title":"Runtime Verification","author":"A Desai","year":"2017","unstructured":"Desai, A., Dreossi, T., Seshia, S.A.: Combining model checking and runtime verification for safe robotics. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 172\u2013189. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-67531-2_11"},{"issue":"4","key":"9_CR11","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1109\/MCI.2015.2471196","volume":"10","author":"G Ditzler","year":"2015","unstructured":"Ditzler, G., Roveri, M., Alippi, C., Polikar, R.: Learning in nonstationary environments: a survey. IEEE Comput. Intell. Mag. 10(4), 12\u201325 (2015)","journal-title":"IEEE Comput. Intell. Mag."},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Ferrando, A., Malvone, V.: Runtime verification with imperfect information through indistinguishability relations. In: International Conference on Software Engineering and Formal Methods, pp. 335\u2013351. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-17108-6_21","DOI":"10.1007\/978-3-031-17108-6_21"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-030-17462-0_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Fulton","year":"2019","unstructured":"Fulton, N., Platzer, A.: Verifiably safe off-model reinforcement learning. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 413\u2013430. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_28"},{"issue":"1\u20132","key":"9_CR14","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0004-3702(00)00047-3","volume":"122","author":"R Givan","year":"2000","unstructured":"Givan, R., Leach, S., Dean, T.: Bounded-parameter Markov decision processes. Artif. Intell. 122(1\u20132), 71\u2013109 (2000)","journal-title":"Artif. Intell."},{"key":"9_CR15","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.tcs.2016.12.003","volume":"735","author":"S Haddad","year":"2018","unstructured":"Haddad, S., Monmege, B.: Interval iteration algorithm for MDPS and IMDPS. Theoret. Comput. Sci. 735, 111\u2013131 (2018)","journal-title":"Theoret. Comput. Sci."},{"key":"9_CR16","unstructured":"Hall\u00e9, S., Soueidi, C., Falcone, Y.: Leveraging runtime verification for the monitoring of digital twins. FMDT@ FM 3507 (2023)"},{"issue":"3","key":"9_CR17","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1093\/biomet\/asab047","volume":"109","author":"A Henzi","year":"2022","unstructured":"Henzi, A., Ziegel, J.F.: Valid sequential inference on probability forecast performance. Biometrika 109(3), 647\u2013663 (2022)","journal-title":"Biometrika"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Karimi, M., Kueffner, K., Mallik, K.: Runtime monitoring of dynamic fairness properties. In: Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency, pp. 604\u2013614 (2023)","DOI":"10.1145\/3593013.3594028"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Karimi, M., Kueffner, K., Mallik, K.: Monitoring algorithmic fairness. In: International Conference on Computer Aided Verification, pp. 358\u2013382. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_17","DOI":"10.1007\/978-3-031-37703-7_17"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Hinder, F., Vaquet, V., Hammer, B.: One or two things we know about concept drift\u2013a survey on monitoring evolving environments. arXiv preprint arXiv:2310.15826 (2023)","DOI":"10.3389\/frai.2024.1330257"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Holzmann, H., Klar, B.: Focusing on regions of interest in forecast evaluation. Ann. Appl. Stat. 11(4), 2404\u20132431 (2017). http:\/\/www.jstor.org\/stable\/26362191","DOI":"10.1214\/17-AOAS1088"},{"key":"9_CR22","unstructured":"Hosseinkhani, E., Leucker, M., Sachenbacher, M., Streichhahn, H., Vosteen, L.B.: A model-based approach for monitoring and diagnosing digital twin discrepancies. In: 35th International Conference on Principles of Diagnosis and Resilient Systems (DX 2024), pp.\u00a02\u20131. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2024)"},{"issue":"2","key":"9_CR23","doi-asserted-by":"publisher","first-page":"1055","DOI":"10.1214\/20-AOS1991","volume":"49","author":"SR Howard","year":"2021","unstructured":"Howard, S.R., Ramdas, A., McAuliffe, J., Sekhon, J.: Time-uniform, nonparametric, nonasymptotic confidence sequences. Ann. Stat. 49(2), 1055\u20131080 (2021)","journal-title":"Ann. Stat."},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Proceedings 1991 Sixth Annual IEEE Symposium on Logic in Computer Science, pp. 266\u2013267. IEEE Computer Society (1991)","DOI":"10.1109\/LICS.1991.151651"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/978-3-030-81688-9_26","volume-title":"Computer Aided Verification","author":"S Junges","year":"2021","unstructured":"Junges, S., Torfah, H., Seshia, S.A.: Runtime monitors for Markov decision processes. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 553\u2013576. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_26"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: The prism benchmark suite. In: 9th International Conference on Quantitative Evaluation of SysTems, pp. 203\u2013204. IEEE CS press (2012)","DOI":"10.1109\/QEST.2012.14"},{"issue":"1","key":"9_CR27","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-016-0241-z","volume":"49","author":"S Mitsch","year":"2016","unstructured":"Mitsch, S., Platzer, A.: Modelplex: verified runtime validation of verified cyber-physical system models. Formal Methods Syst. Des. 49(1), 33\u201374 (2016)","journal-title":"Formal Methods Syst. Des."},{"key":"9_CR28","first-page":"8702","volume":"34","author":"H Pouget","year":"2021","unstructured":"Pouget, H., Chockler, H., Sun, Y., Kroening, D.: Ranking policy decisions. Adv. Neural. Inf. Process. Syst. 34, 8702\u20138713 (2021)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Pranger, S., Chockler, H., Tappler, M., K\u00f6nighofer, B.: Test where decisions matter: importance-driven testing for deep reinforcement learning. In: Conference on Neural Information Processing Systems (NeurIPS) (2024)","DOI":"10.52202\/079017-0881"},{"key":"9_CR30","doi-asserted-by":"publisher","unstructured":"Qian, M., Mitsch, S.: Reward shaping from hybrid systems models in reinforcement learning. In: NASA formal methods symposium, pp. 122\u2013139. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_8","DOI":"10.1007\/978-3-031-33170-1_8"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Roehm, H., Oehlerking, J., Woehrle, M., Althoff, M.: Reachset conformance testing of hybrid automata. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, pp. 277\u2013286 (2016)","DOI":"10.1145\/2883817.2883828"},{"issue":"3","key":"9_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3306157","volume":"3","author":"H Roehm","year":"2019","unstructured":"Roehm, H., Oehlerking, J., Woehrle, M., Althoff, M.: Model conformance for cyber-physical systems: a survey. ACM Trans. Cyber-Phys. Syst. 3(3), 1\u201326 (2019)","journal-title":"ACM Trans. Cyber-Phys. Syst."},{"key":"9_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"534","DOI":"10.1007\/978-3-030-58583-9_32","volume-title":"Computer Vision \u2013 ECCV 2020","author":"T Stoffregen","year":"2020","unstructured":"Stoffregen, T., et al.: Reducing the sim-to-real gap for event cameras. In: Vedaldi, A., Bischof, H., Brox, T., Frahm, J.-M. (eds.) ECCV 2020. LNCS, vol. 12372, pp. 534\u2013549. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58583-9_32"},{"key":"9_CR34","doi-asserted-by":"publisher","unstructured":"Suilen, M., Badings, T., Bovy, E.M., Parker, D., Jansen, N.: Robust markov decision processes: a place where ai and formal methods meet. In: Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III, pp. 126\u2013154. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-75778-5_7","DOI":"10.1007\/978-3-031-75778-5_7"},{"key":"9_CR35","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/j.procir.2022.05.251","volume":"109","author":"P Trentsios","year":"2022","unstructured":"Trentsios, P., Wolf, M., Gerhard, D.: Overcoming the sim-to-real gap in autonomous robots. Procedia CIRP 109, 287\u2013292 (2022)","journal-title":"Procedia CIRP"},{"issue":"12","key":"9_CR36","doi-asserted-by":"publisher","first-page":"2823","DOI":"10.1109\/TSE.2020.2969178","volume":"47","author":"Y Yamagata","year":"2020","unstructured":"Yamagata, Y., Liu, S., Akazaki, T., Duan, Y., Hao, J.: Falsification of cyber-physical systems using deep reinforcement learning. IEEE Trans. Softw. Eng. 47(12), 2823\u20132840 (2020)","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-05435-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T16:48:11Z","timestamp":1785257291000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-05435-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,12]]},"ISBN":["9783032054340","9783032054357"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-05435-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,12]]},"assertion":[{"value":"12 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"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":"Graz","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Austria","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rv2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rv25.isec.tugraz.at\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}