{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,30]],"date-time":"2026-07-30T17:06:09Z","timestamp":1785431169389,"version":"3.56.0"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227195","type":"print"},{"value":"9783032227201","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T00:00:00Z","timestamp":1775779200000},"content-version":"vor","delay-in-days":99,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22720-1_1","type":"book-chapter","created":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T15:30:40Z","timestamp":1775748640000},"page":"1-12","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Methods meet Digital Twins: Challenges and Opportunities"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5382-3949","authenticated-orcid":false,"given":"Einar Broch","family":"Johnsen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0996-2543","authenticated-orcid":false,"given":"Eduard","family":"Kamburjan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9446-9541","authenticated-orcid":false,"given":"Andrea","family":"Pferscher","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9948-2748","authenticated-orcid":false,"given":"Silvia Lizeth","family":"Tapia Tarifa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,10]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Ahlgren, J., Bojarczuk, K., Drossopoulou, S., Dvortsova, I., George, J., Gucevska, N., Harman, M., Lomeli, M., Lucas, S.M.M., Meijer, E., Omohundro, S., Rojas, R., Sapora, S., Zhou, N.: Facebook\u2019s cyber-cyber and cyber-physical digital twins. In: Proc. Evaluation and Assessment in Software Engineering (EASE 2021). pp.\u00a01\u20139. ACM (2021). https:\/\/doi.org\/10.1145\/3463274.3463275","DOI":"10.1145\/3463274.3463275"},{"key":"1_CR2","doi-asserted-by":"publisher","unstructured":"Arcaini, P., Riccobene, E., Scandurra, P.: Modeling and analyzing MAPE-K feedback loops for self-adaptation. In: Inverardi, P., Schmerl, B.R. (eds.) Proc. 10th Intl. Symp. on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2015). pp. 13\u201323. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/SEAMS.2015.10","DOI":"10.1109\/SEAMS.2015.10"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Baier, C., de\u00a0Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963\u2013999. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Baresi, L., Ghezzi, C.: The disappearing boundary between development-time and run-time. In: Proc. Workshop on Future of Software Engineering Research, (FoSER 2010). pp. 17\u201322. ACM (2010). https:\/\/doi.org\/10.1145\/1882362.1882367","DOI":"10.1145\/1882362.1882367"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., Chapman, R., Cleaveland, R., Garavel, H., Gu, R., ter Horst, I., Keiren, J.J.A., Lecomte, T., Leuschel, M., Rozier, K.Y., Sampaio, A., Seceleanu, C., Thomas, M., Willemse, T.A.C., Zhang, L.: Formal Methods in Industry. Formal Aspects Comput. 37(1), 7:1\u20137:38 (2025). https:\/\/doi.org\/10.1145\/3689374","DOI":"10.1145\/3689374"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Billey, A., Wuest, T.: Energy digital twins in smart manufacturing systems: A case study. Robotics Comput. Integr. Manuf. 88, 102729 (2024). https:\/\/doi.org\/10.1016\/J.RCIM.2024.102729","DOI":"10.1016\/J.RCIM.2024.102729"},{"key":"1_CR7","doi-asserted-by":"publisher","unstructured":"Birchler, C., Khatiri, S., Rani, P., Kehrer, T., Panichella, S.: A roadmap for simulation-based testing of autonomous cyber-physical systems: Challenges and future direction. ACM Trans. Softw. Eng. Methodol. 34(5), 152:1\u2013152:9 (2025). https:\/\/doi.org\/10.1145\/3711906","DOI":"10.1145\/3711906"},{"key":"1_CR8","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N.S., Phan, A., Fleckenstein, L.: $$\\nu $$z - an optimizing SMT solver. In: Proc. TACAS 2015. LNCS, vol.\u00a09035, pp. 194\u2013199. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_14","DOI":"10.1007\/978-3-662-46681-0_14"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Blair, G.S., Bencomo, N., France, R.B.: Models@ run.time. Computer 42(10), 22\u201327 (2009). https:\/\/doi.org\/10.1109\/MC.2009.326","DOI":"10.1109\/MC.2009.326"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Braun, S., Dalibor, M., Jansen, N., Jarke, M., Koren, I., Quix, C., Rumpe, B., Wimmer, M., Wortmann, A.: Engineering digital twins and digital shadows as key enablers for industry 4.0. In: Digital Transformation - Core Technologies and Emerging Topics from a Computer Science Perspective, pp. 3\u201331. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-662-65004-2_1","DOI":"10.1007\/978-3-662-65004-2_1"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Chang, X., Zhang, R., Mao, J., Fu, Y.: Digital twins in transportation infrastructure: An investigation of the key enabling technologies, applications, and challenges. IEEE Trans. Intell. Transp. Syst. 25(7), 6449\u20136471 (2024). https:\/\/doi.org\/10.1109\/TITS.2024.3401716","DOI":"10.1109\/TITS.2024.3401716"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Chrszon, P., Dubslaff, C., Kl\u00fcppelholz, S., Baier, C.: ProFeat: Feature-Oriented Engineering for Family-Based Probabilistic Model Checking. Formal Aspects Comput. 30(1), 45\u201375 (2018). https:\/\/doi.org\/10.1007\/s00165-017-0432-4","DOI":"10.1007\/s00165-017-0432-4"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Classen, A., Cordy, M., Schobbens, P.Y., Heymans, P., Legay, A., Raskin, J.F.: Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking. IEEE Transaction on Software Engineering 39(8), 1069\u20131089 (2013). https:\/\/doi.org\/10.1109\/TSE.2012.86","DOI":"10.1109\/TSE.2012.86"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Dubslaff, C., Koopmann, P., Turhan, A.: Enhancing probabilistic model checking with ontologies. Formal Aspects Comput. 33(6), 885\u2013921 (2021). https:\/\/doi.org\/10.1007\/S00165-021-00549-0","DOI":"10.1007\/S00165-021-00549-0"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Fitzgerald, J., Gomes, C., Larsen, P.G. (eds.): The Engineering of Digital Twins. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-66719-0","DOI":"10.1007\/978-3-031-66719-0"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Gleirscher, M., Marmsoler, D.: Formal Methods in Dependable Systems Engineering: A Survey of Professionals from Europe and North America. Empir. Softw. Eng. 25(6), 4473\u20134546 (2020). https:\/\/doi.org\/10.1007\/s10664-020-09836-5","DOI":"10.1007\/s10664-020-09836-5"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Gomes, C., Thule, C., Broman, D., Larsen, P.G., Vangheluwe, H.: Co-simulation: A survey. ACM Comput. Surv. 51(3), 49:1\u201349:33 (2018). https:\/\/doi.org\/10.1145\/3179993","DOI":"10.1145\/3179993"},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"Hallsteinsen, S., Hinchey, M., Park, S., Schmid, K.: Dynamic Software Product Lines. In: Systems and Software Variability Management: Concepts, Tools and Experiences, pp. 253\u2013260. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36583-6_16","DOI":"10.1007\/978-3-642-36583-6_16"},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Hansen, S.T., Kamburjan, E., Kazemi, Z.: Monitoring reconfigurable simulation scenarios in co-simulated digital twins. In: Proc. 12th Intl. Symp. on Leveraging Applications of Formal Methods, Verification and Validation. Application Areas (ISoLA 2024). LNCS, vol. 15223, pp. 47\u201361. Springer (2024).https:\/\/doi.org\/10.1007\/978-3-031-75390-9_4","DOI":"10.1007\/978-3-031-75390-9_4"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Hierons, R.M., Bogdanov, K., Bowen, J.P., Cleaveland, R., Derrick, J., Dick, J., Gheorghe, M., Harman, M., Kapoor, K., Krause, P.J., L\u00fcttgen, G., Simons, A.J.H., Vilkomir, S.A., Woodward, M.R., Zedan, H.: Using formal specifications to support testing. ACM Comput. Surv. 41(2), 9:1\u20139:76 (2009). https:\/\/doi.org\/10.1145\/1459352.1459354","DOI":"10.1145\/1459352.1459354"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Hinchey, M., Park, S., Schmid, K.: Building Dynamic Software Product Lines. IEEE Computer 45(10), 22\u201326 (2012). https:\/\/doi.org\/10.1109\/MC.2012.332","DOI":"10.1109\/MC.2012.332"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Hogan, A., et al.: Knowledge graphs. ACM Comput. Surv. 54(4) (Jul 2021). https:\/\/doi.org\/10.1145\/3447772","DOI":"10.1145\/3447772"},{"key":"1_CR23","doi-asserted-by":"publisher","unstructured":"de\u00a0la Iglesia, D.G., Weyns, D.: MAPE-K formal templates to rigorously design behaviors for self-adaptive systems. ACM Trans. Auton. Adapt. Syst. 10(3), 15:1\u201315:31 (2015). https:\/\/doi.org\/10.1145\/2724719","DOI":"10.1145\/2724719"},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"John, T., Johnsen, E.B., Kamburjan, E., Steinh\u00f6fel, D.: Language-based testing for knowledge graphs. In: Proc. 22nd European Semantic Web Conf. (ESWC 2025). LNCS, vol. 15719, pp. 24\u201346. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-94578-6_2","DOI":"10.1007\/978-3-031-94578-6_2"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"John, T., Kamburjan, E., Johnsen, E.B.: Mutation-based integration testing of knowledge graph applications. In: Proc. 35th Intl. Symp. on Software Reliability Engineering (ISSRE 2024). pp. 475\u2013486. IEEE (2024). https:\/\/doi.org\/10.1109\/ISSRE62328.2024.00052","DOI":"10.1109\/ISSRE62328.2024.00052"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"John, T., Kamburjan, E., Johnsen, E.B.: Mutation-based testing of knowledge graphs. Empir. Softw. Eng. (2026), to appear.","DOI":"10.1007\/s10664-026-10810-w"},{"key":"1_CR27","doi-asserted-by":"publisher","unstructured":"John, T., Kamburjan, E., Johnsen, E.B.: RDFMutate: Mutation-based generation of knowledge graphs. In: Proc. 24th Intl. Semantic Web Conf. (ISWC 2025). LNCS, vol. 16141, pp. 295\u2013312. Springer (2026). https:\/\/doi.org\/10.1007\/978-3-032-09530-5_17","DOI":"10.1007\/978-3-032-09530-5_17"},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: A core language for abstract behavioral specification. In: Proc. FMCO. LNCS, vol.\u00a06957, pp. 142\u2013164. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-25271-6_8","DOI":"10.1007\/978-3-642-25271-6_8"},{"key":"1_CR29","doi-asserted-by":"publisher","unstructured":"Kamburjan, E., Bencomo, N., Tapia\u00a0Tarifa, S.L., Johnsen, E.B.: Declarative lifecycle management in digital twins. In: Proc. 1st Intl. Conf. on Engineering Digital Twins (EDTconf 2024). pp. 353\u2013\u2013363. MODELS Companion\u201924, ACM (2024). https:\/\/doi.org\/10.1145\/3652620.3688248","DOI":"10.1145\/3652620.3688248"},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"Kamburjan, E., Gurov, D.: Multi-perspective correctness of programs. In: Proc. 22nd Intl. Colloquium on Theoretical Aspects of Computing (ICTAC 2025). LNCS, vol. 16237, pp. 69\u201386. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-032-11176-0_6","DOI":"10.1007\/978-3-032-11176-0_6"},{"key":"1_CR31","doi-asserted-by":"publisher","unstructured":"Kamburjan, E., Klungre, V.N., Qu, Y., Schlatte, R., Kostylev, E.V., Giese, M., Johnsen, E.B.: Semantically reflected programs. CoRR abs\/2509.03318 (2025). https:\/\/doi.org\/10.48550\/ARXIV.2509.03318","DOI":"10.48550\/ARXIV.2509.03318"},{"key":"1_CR32","doi-asserted-by":"publisher","unstructured":"Kamburjan, E., Klungre, V.N., Schlatte, R., Johnsen, E.B., Giese, M.: Programming and debugging with semantically lifted states. In: Proc. 18th Extended Semantic Web Conference (ESWC 2021). LNCS, vol. 12731, pp. 126\u2013142. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-77385-4_8","DOI":"10.1007\/978-3-030-77385-4_8"},{"key":"1_CR33","doi-asserted-by":"publisher","unstructured":"Kamburjan, E., Pferscher, A., Schlatte, R., Sieve, R., Tapia\u00a0Tarifa, S.L., Johnsen, E.B.: Semantic reflection and digital twins: A comprehensive overview. In: The Combined Power of Research, Education, and Dissemination: Essays Dedicated to Tiziana Margaria on the Occasion of Her 60th Birthday, LNCS, vol. 15240, pp. 129\u2013145. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-73887-6_11","DOI":"10.1007\/978-3-031-73887-6_11"},{"key":"1_CR34","doi-asserted-by":"publisher","unstructured":"Kamburjan, E., Sieve, R., Baramashetru, C.P., Amato, M., Barmina, G., Occhipinti, E., Johnsen, E.B.: GreenhouseDT: An exemplar for digital twins. In: Proc. 19th Intl. Symp. on Software Eng. for Adaptive and Self-Managing Systems (SEAMS 2024). pp. 175\u2013181. ACM (2024). https:\/\/doi.org\/10.1145\/3643915.3644108","DOI":"10.1145\/3643915.3644108"},{"key":"1_CR35","doi-asserted-by":"publisher","unstructured":"Kl\u00f8vstad, \u00c5.A.A., Kobialka, P., Sieve, R., Pferscher, A., Slaughter, L., Tapia\u00a0Tarifa, S.L., Johnsen, E.B.: What-if scenarios for the BedreFlyt digital twin. In: Principles of formal quantitative analysis \u2014 Essays dedicated to Christel Baier on the occasion of her 60th birthday. p. 360\u2013381. LNCS, Springer (2026). https:\/\/doi.org\/10.1007\/978-3-031-97439-7_18","DOI":"10.1007\/978-3-031-97439-7_18"},{"key":"1_CR36","doi-asserted-by":"publisher","unstructured":"Kobialka, P., Pferscher, A., Bergersen, G.R., Johnsen, E.B., Tapia\u00a0Tarifa, S.L.: Stochastic games for user journeys. In: Proc. 26th Intl. Symp. on Formal Methods (FM 2024). LNCS, vol. 14934, pp. 167\u2013186. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-71177-0_12","DOI":"10.1007\/978-3-031-71177-0_12"},{"key":"1_CR37","doi-asserted-by":"publisher","unstructured":"Kobialka, P., Tapia Tarifa, S.L., Bergersen, G.R., Johnsen, E.B.: User journey games: automating user-centric analysis. Softw. Syst. Model. 23(3), 605\u2013624 (2024). https:\/\/doi.org\/10.1007\/S10270-024-01148-2","DOI":"10.1007\/S10270-024-01148-2"},{"key":"1_CR38","unstructured":"Korn, M.: Formal-Methods Support for Runtime Adaptation in Self-Adaptive Systems. Ph.D. thesis, Dresden University of Technology, Germany (2025)"},{"key":"1_CR39","doi-asserted-by":"publisher","unstructured":"Kristensen, M.H., Bonizzi, A., Gomes, C., Hansen, S.T., Martin, C.I.I., Iven, H., Kamburjan, E., Larsen, P.G., Leucker, M., Talasila, P., Tang, V.T., Tonetta, S., Vosteen, L.B., Wright, T.: Runtime verification of autonomous systems utilizing digital twins as a service. In: Proc. Intl. Conf. on Autonomic Computing and Self-Organizing Systems (ACSOS 2024). pp. 121\u2013127. IEEE (2024). https:\/\/doi.org\/10.1109\/ACSOS-C63493.2024.00042","DOI":"10.1109\/ACSOS-C63493.2024.00042"},{"key":"1_CR40","doi-asserted-by":"publisher","unstructured":"Kritzinger, W., Karner, M., Traar, G., Henjes, J., Sihn, W.: Digital twin in manufacturing: A categorical literature review and classification. IFAC-PapersOnLine 51(11), 1016\u20131022 (2018). https:\/\/doi.org\/10.1016\/j.ifacol.2018.08.474","DOI":"10.1016\/j.ifacol.2018.08.474"},{"key":"1_CR41","doi-asserted-by":"publisher","unstructured":"Kruger, L., Kobialka, P., Pferscher, A., Johnsen, E.B., Junges, S., Rot, J.: Incremental fingerprinting in an open world. In: Proc. CSF 2026. IEEE (2026). https:\/\/doi.org\/10.48550\/arXiv.2601.21680, to appear.","DOI":"10.48550\/arXiv.2601.21680"},{"key":"1_CR42","doi-asserted-by":"publisher","unstructured":"Laubenbacher, R., Mehrad, B., Shmulevich, I., Trayanova, N.: Digital twins in medicine. Nat Comput Sci 4, 184\u2013191 (2024). https:\/\/doi.org\/10.1038\/s43588-024-00607-6","DOI":"10.1038\/s43588-024-00607-6"},{"key":"1_CR43","doi-asserted-by":"publisher","unstructured":"Michael, J., et al.: Model-driven engineering for digital twins: Opportunities and challenges. Syst. Eng. 28(5), 659\u2013670 (2025). https:\/\/doi.org\/10.1002\/SYS.21815","DOI":"10.1002\/SYS.21815"},{"key":"1_CR44","doi-asserted-by":"publisher","unstructured":"Michalec, O.: Models vs infrastructures? on the role of digital twins\u2019 hype in anticipating the governance of the UK energy industry. Environmental Science & Policy 168, 104041 (2025). https:\/\/doi.org\/10.1016\/j.envsci.2025.104041","DOI":"10.1016\/j.envsci.2025.104041"},{"key":"1_CR45","doi-asserted-by":"publisher","unstructured":"Muctadir, H.M., Kamburjan, E., Cleophas, L., van den Brand, M.: A consistency management framework for digital twin models. Journal of Systems and Software 234, 112750 (2026). https:\/\/doi.org\/10.1016\/j.jss.2025.112750","DOI":"10.1016\/j.jss.2025.112750"},{"key":"1_CR46","doi-asserted-by":"publisher","unstructured":"National Academies of Sciences, Engineering, and Medicine (NASEM): Foundational Research Gaps and Future Directions for Digital Twins. The National Academies Press (2024). https:\/\/doi.org\/10.17226\/26894","DOI":"10.17226\/26894"},{"key":"1_CR47","unstructured":"Pferscher, A., Wunderling, B., Aichernig, B.K., Muskardin, E.: Mining digital twins of a VPN server. In: Proc. Workshop on Applications of Formal Methods and Digital Twins. CEUR Workshop Proc.\u00a0 vol.\u00a03507. CEUR-WS.org (2023), https:\/\/ceur-ws.org\/Vol-3507\/paper6.pdf"},{"key":"1_CR48","doi-asserted-by":"publisher","unstructured":"P\u00e4\u00dfler, J., ter Beek, M.H., Damiani, F., Dubslaff, C., Johnsen, E.B., Tapia\u00a0Tarifa, S.L.: Feature-oriented modelling and analysis of a self-adaptive robotic system. Formal Aspects Comput. 37(4), 1\u201339 (2025). https:\/\/doi.org\/10.1145\/3709159","DOI":"10.1145\/3709159"},{"key":"1_CR49","doi-asserted-by":"publisher","unstructured":"P\u00e4\u00dfler, J., ter Beek, M.H., Damiani, F., Johnsen, E.B., Tapia\u00a0Tarifa, S.L.: Analysing self-adaptive systems as software product lines. Journal of Systems and Software 222, 112324 (2025). https:\/\/doi.org\/10.1016\/j.jss.2024.112324","DOI":"10.1016\/j.jss.2024.112324"},{"key":"1_CR50","doi-asserted-by":"publisher","unstructured":"Sieve, R., Kamburjan, E., Damiani, F., Johnsen, E.B.: Declarative dynamic object reclassification. In: Proc. ECOOP 2025. LIPIcs, vol.\u00a0333, pp. 29:1\u201329:31. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2025). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2025.29","DOI":"10.4230\/LIPICS.ECOOP.2025.29"},{"key":"1_CR51","doi-asserted-by":"publisher","unstructured":"Sieve, R., Kobialka, P., Slaughter, L., Schlatte, R., Johnsen, E.B., Tapia\u00a0Tarifa, S.L.: BedreFlyt: Improving patient flows through hospital wards with digital twins. In: Proc. First Intl. Workshop on Autonomous Systems Quality Assurance and Prediction with Digital Twins (ASQAP 2025). EPTCS, vol.\u00a0418, pp. 1\u201315. Open Publishing Association (2025). https:\/\/doi.org\/10.4204\/EPTCS.418.1","DOI":"10.4204\/EPTCS.418.1"},{"key":"1_CR52","doi-asserted-by":"publisher","unstructured":"Torres, W., van\u00a0den Brand, M.G.J., Serebrenik, A.: A systematic literature review of cross-domain model consistency checking by model management tools. Softw. Syst. Model. 20(3), 897\u2013916 (2021). https:\/\/doi.org\/10.1007\/S10270-020-00834-1","DOI":"10.1007\/S10270-020-00834-1"},{"key":"1_CR53","doi-asserted-by":"publisher","unstructured":"Vaandrager, F.W.: Model learning. Commun. ACM 60(2), 86\u201395 (2017). https:\/\/doi.org\/10.1145\/2967606","DOI":"10.1145\/2967606"},{"key":"1_CR54","doi-asserted-by":"publisher","unstructured":"Vach\u00e1lek, J., Bartalsk\u00fd, L., Rovn\u00fd, O., \u0160i\u0161mi\u0161ov\u00e1, D., Morh\u00e1\u010d, M., Lok\u0161\u00edk, M.: The digital twin of an industrial production line within the Industry 4.0 concept. In: Proc. 21st Intl. Conf. on Process Control (PC 2017). pp. 258\u2013262 (2017). https:\/\/doi.org\/10.1109\/PC.2017.7976223","DOI":"10.1109\/PC.2017.7976223"},{"key":"1_CR55","doi-asserted-by":"publisher","unstructured":"Vall\u00e9e, A.: Digital twin for healthcare systems. Frontiers in Digital Health 5, 1253050 (Sep 2023). https:\/\/doi.org\/10.3389\/fdgth.2023.1253050","DOI":"10.3389\/fdgth.2023.1253050"},{"key":"1_CR56","unstructured":"Wagenmaker, A., Huang, K., Ke, L., Jamieson, K.G., Gupta, A.: Overcoming the sim-to-real gap: Leveraging simulation to learn to explore for real-world RL. In: Proc. NeuRIPS 2024 (2024), http:\/\/papers.nips.cc\/paper_files\/paper\/2024\/hash\/8fa068ffe59817175d176bd75641fe16-Abstract-Conference.html"},{"key":"1_CR57","doi-asserted-by":"publisher","unstructured":"Wallner, F., Aichernig, B.K., Burghard, C.: It\u2019s not a feature, it\u2019s a bug: Fault-tolerant model mining from noisy data. In: Proc. ICSE 2024. pp. 29:1\u201329:13. ACM (2024). https:\/\/doi.org\/10.1145\/3597503.3623346","DOI":"10.1145\/3597503.3623346"},{"key":"1_CR58","doi-asserted-by":"publisher","unstructured":"Weyns, D.: An Introduction to Self-Adaptive Systems: A Contemporary Software Engineering Perspective. Wiley-IEEE Computer Society Pr (2021). https:\/\/doi.org\/10.1002\/9781119574910","DOI":"10.1002\/9781119574910"},{"key":"1_CR59","doi-asserted-by":"publisher","unstructured":"Weyns, D., Iftikhar, M.U., de\u00a0la Iglesia, D.G., Ahmad, T.: A survey of formal methods in self-adaptive systems. In: Proc. Fifth Intl. C* Conf. on Computer Science & Software Engineering (C3S2E 2012). pp. 67\u201379. ACM (2012). https:\/\/doi.org\/10.1145\/2347583.2347592","DOI":"10.1145\/2347583.2347592"},{"key":"1_CR60","doi-asserted-by":"publisher","unstructured":"Wing, J.M.: A specifier\u2019s introduction to formal methods. Computer 23(9), 8\u201324 (1990). https:\/\/doi.org\/10.1109\/2.58215","DOI":"10.1109\/2.58215"},{"key":"1_CR61","doi-asserted-by":"publisher","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: Practice and experience. ACM Comput. Surv. 41(4), 19:1\u201319:36 (2009). https:\/\/doi.org\/10.1145\/1592434.1592436","DOI":"10.1145\/1592434.1592436"},{"key":"1_CR62","doi-asserted-by":"publisher","unstructured":"Zhao, W., Queralta, J.P., Westerlund, T.: Sim-to-real transfer in deep reinforcement learning for robotics: a survey. In: Proc. Symposium Series on Computational Intelligence (SSCI 2020). pp. 737\u2013744. IEEE (2020). https:\/\/doi.org\/10.1109\/SSCI47803.2020.9308468","DOI":"10.1109\/SSCI47803.2020.9308468"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22720-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,30]],"date-time":"2026-07-30T16:39:31Z","timestamp":1785429571000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22720-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227195","9783032227201"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22720-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"10 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}