{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T15:12:02Z","timestamp":1778080322517,"version":"3.51.4"},"publisher-location":"Singapore","reference-count":84,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819586165","type":"print"},{"value":"9789819586172","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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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-981-95-8617-2_6","type":"book-chapter","created":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T14:27:30Z","timestamp":1778077650000},"page":"159-210","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Model Checking, Performance Analysis, Synthesis and\u00a0Learning for\u00a0Cyber Physical Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5953-3384","authenticated-orcid":false,"given":"Kim G.","family":"Larsen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8157-5428","authenticated-orcid":false,"given":"Marius","family":"Miku\u010dionis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,1]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Alur, R., Bernadsky, M., Madhusudan, P.: Optimal reachability for weighted timed games. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) Automata, Languages and Programming. Lecture Notes in Computer Science, vol.\u00a03142, pp. 122\u2013133. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27836-8_13","DOI":"10.1007\/978-3-540-27836-8_13"},{"issue":"2","key":"6_CR2","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, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"6_CR3","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996). https:\/\/doi.org\/10.1145\/227595.227602","journal-title":"J. ACM"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Alur, R., La\u00a0Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Di\u00a0Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol.\u00a02034, pp. 49\u201362. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45351-2_8","DOI":"10.1007\/3-540-45351-2_8"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Arcile, J., Andr\u00e9, \u00c9.: Zone extrapolations in parametric timed automata. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NASA Formal Methods. Lecture Notes in Computer Science, vol. 13260, pp. 451\u2013469. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_24","DOI":"10.1007\/978-3-031-06773-0_24"},{"key":"6_CR6","doi-asserted-by":"publisher","unstructured":"Arcile, J., Andr\u00e9, \u00c9.: Zone extrapolations in parametric timed automata. Innov. Syst. Softw. Eng. 21, 707\u2013726 (2025). https:\/\/doi.org\/10.1007\/s11334-024-00554-5","DOI":"10.1007\/s11334-024-00554-5"},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"Asarin, E., Maler, O.: As soon as possible: time optimal control for timed automata. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol.\u00a01569, pp. 19\u201330. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48983-5_6","DOI":"10.1007\/3-540-48983-5_6"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. IFAC Proc. Vol. 31(18), 447\u2013452 (1998). https:\/\/doi.org\/10.1016\/S1474-6670(17)42032-5, 5th IFAC Conference on System Structure and Control 1998 (SSC\u201998), Nantes, France, 8\u201310 July","DOI":"10.1016\/S1474-6670(17)42032-5"},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol.\u00a01633, pp. 341\u2013353. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_30","DOI":"10.1007\/3-540-48683-6_30"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol.\u00a02619, pp. 254\u2013270. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_18","DOI":"10.1007\/3-540-36577-X_18"},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Behrmann, G., Bouyer, P., Larsen, K.G., Pel\u00e1nek, R.: Lower and upper bounds in zone-based abstractions of timed automata. Int. J. Softw. Tools Technol. Transf. 8, 204\u2013215 (2006). https:\/\/doi.org\/10.1007\/s10009-005-0190-0","DOI":"10.1007\/s10009-005-0190-0"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: Uppaal-tiga: time for playing games! In: Proceedings of the 19th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol.\u00a04590, pp. 121\u2013125. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_14","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Behrmann, G., et al.: UPPAAL 4.0. In: Third International Conference on the Quantitative Evaluation of Systems \u2013 (QEST 2006), pp. 125\u2013126. IEEE (2006). https:\/\/doi.org\/10.1109\/QEST.2006.59","DOI":"10.1109\/QEST.2006.59"},{"key":"6_CR14","doi-asserted-by":"publisher","unstructured":"Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing UPPAAL over 15 years. Softw. Pract. Exp. 41(2), 133\u2013142 (2011). https:\/\/doi.org\/10.1002\/spe.1006","DOI":"10.1002\/spe.1006"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Behrmann, G., et al.: Minimum-cost reachability for priced time automata. In: Di\u00a0Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol.\u00a02034, pp. 147\u2013161. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45351-2_15","DOI":"10.1007\/3-540-45351-2_15"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Beyond liveness: efficient parameter synthesis for time bounded liveness. In: Pettersson, P., Yi, W. (eds.) Formal Modeling and Analysis of Timed Systems, Third International Conference, FORMATS 2005, Uppsala, Sweden, 26\u201328 September 2005, Proceedings. Lecture Notes in Computer Science, vol.\u00a03829, pp. 81\u201394. Springer (2005). https:\/\/doi.org\/10.1007\/11603009_7","DOI":"10.1007\/11603009_7"},{"key":"6_CR17","doi-asserted-by":"publisher","unstructured":"Bisgaard, M., Gerhardt, D., Hermanns, H., Kr\u010d\u00e1l, J., Nies, G., Stenger, M.: Battery-aware scheduling in low orbit: the gomx\u20133 case. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016: Formal Methods. Lecture Notes in Computer Science, vol.\u00a09995, pp. 559\u2013576. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_34","DOI":"10.1007\/978-3-319-48989-6_34"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Bloem, R., K\u00f6nighofer, B., K\u00f6nighofer, R., Wang, C.: Shield synthesis: runtime enforcement for reactive systems. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol.\u00a09035, pp. 533\u2013548. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_51","DOI":"10.1007\/978-3-662-46681-0_51"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Boudjadar, A.J., et al.: Degree of schedulability of mixed-criticality real-time systems with probabilistic sporadic tasks. In: 2014 Theoretical Aspects of Software Engineering Conference, pp. 126\u2013130. IEEE (2014). https:\/\/doi.org\/10.1109\/TASE.2014.27","DOI":"10.1109\/TASE.2014.27"},{"key":"6_CR20","doi-asserted-by":"publisher","unstructured":"Bouyer, P.: Untameable timed automata! In: Alt, H., Habib, M. (eds.) STACS 2003. Lecture Notes in Computer Science, vol.\u00a02607, pp. 620\u2013631. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36494-3_54","DOI":"10.1007\/3-540-36494-3_54"},{"key":"6_CR21","doi-asserted-by":"publisher","unstructured":"Bouyer, P.: Forward analysis of updatable timed automata. Formal Methods Syst. Des. 24, 281\u2013320 (2004). https:\/\/doi.org\/10.1023\/B:FORM.0000026093.21513.31","DOI":"10.1023\/B:FORM.0000026093.21513.31"},{"issue":"5","key":"6_CR22","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1016\/j.ipl.2006.01.012","volume":"98","author":"P Bouyer","year":"2006","unstructured":"Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. Inf. Process. Lett. 98(5), 188\u2013194 (2006). https:\/\/doi.org\/10.1016\/j.ipl.2006.01.012","journal-title":"Inf. Process. Lett."},{"issue":"1","key":"6_CR23","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/S10703-007-0043-4","volume":"32","author":"P Bouyer","year":"2008","unstructured":"Bouyer, P., Brinksma, E., Larsen, K.G.: Optimal infinite scheduling for multi-priced timed automata. Formal Methods Syst. Des. 32(1), 3\u201323 (2008). https:\/\/doi.org\/10.1007\/S10703-007-0043-4","journal-title":"Formal Methods Syst. Des."},{"key":"6_CR24","doi-asserted-by":"publisher","unstructured":"Bouyer, P., Cassez, F., Fleury, E., Larsen, K.G.: Optimal strategies in priced timed game automata. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science, vol.\u00a03328, pp. 148\u2013160. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30538-5_13","DOI":"10.1007\/978-3-540-30538-5_13"},{"key":"6_CR25","doi-asserted-by":"publisher","unstructured":"Bouyer, P., Colange, M., Markey, N.: Symbolic optimal reachability in weighted timed automata. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol.\u00a09779, pp. 513\u2013530. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_28","DOI":"10.1007\/978-3-319-41528-4_28"},{"key":"6_CR26","doi-asserted-by":"publisher","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Ouaknine, J., Worrell, J.: Model checking real-time systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 1001\u20131046. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_29","DOI":"10.1007\/978-3-319-10575-8_29"},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Bouyer, P., Gastin, P., Herbreteau, F., Sankur, O., Srivathsan, B.: Zone-based verification of timed automata: extrapolations, simulations and what next? In: Bogomolov, S., Parker, D. (eds.) Formal Modeling and Analysis of Timed Systems. Lecture Notes in Computer Science, vol. 13465, pp. 16\u201342. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15839-1_2","DOI":"10.1007\/978-3-031-15839-1_2"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"Bouyer, P., Larsen, K.G., Markey, N., Rasmussen, J.I.: Almost optimal strategies in one clock priced timed games. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science, vol.\u00a04337, pp. 345\u2013356. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11944836_32","DOI":"10.1007\/11944836_32"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Brihaye, T., Bruy\u00e8re, V., Raskin, J.F.: On optimal timed strategies. In: Pettersson, P., Yi, W. (eds.) Formal Modeling and Analysis of Timed Systems. Lecture Notes in Computer Science, vol.\u00a03829, pp. 49\u201364. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11603009_5","DOI":"10.1007\/11603009_5"},{"key":"6_CR30","doi-asserted-by":"publisher","unstructured":"Brihaye, T., Geeraerts, G., Narayanan\u00a0Krishna, S., Manasa, L., Monmege, B., Trivedi, A.: Adding negative prices to priced timed games. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014 \u2013 Concurrency Theory. Lecture Notes in Computer Science, vol.\u00a08704, pp. 560\u2013575. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44584-6_38","DOI":"10.1007\/978-3-662-44584-6_38"},{"key":"6_CR31","doi-asserted-by":"publisher","unstructured":"Brihaye, T., Henzinger, T.A., Prabhu, V.S., Raskin, J.F.: Minimum-time reachability in timed games. In: Arge, L., Cachin, C., Jurdzi\u0144ski, T., Tarlecki, A. (eds.) Automata, Languages and Programming. Lecture Notes in Computer Science, vol.\u00a04596, pp. 825\u2013837. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73420-8_71","DOI":"10.1007\/978-3-540-73420-8_71"},{"key":"6_CR32","doi-asserted-by":"publisher","unstructured":"Brorholt, A.H., H\u00f8eg-Petersen, A.H., Larsen, K.G., Schilling, C.: Efficient shield synthesis via state-space transformation. In: Steffen, B. (ed.) Bridging the Gap Between AI and Reality. Lecture Notes in Computer Science, vol. 15217, pp. 206\u2013224. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-75434-0_14","DOI":"10.1007\/978-3-031-75434-0_14"},{"key":"6_CR33","doi-asserted-by":"publisher","unstructured":"Brorholt, A.H., Jensen, P.G., Larsen, K.G., Lorber, F., Schilling, C.: Shielded reinforcement learning for hybrid systems. In: Steffen, B. (ed.) Bridging the Gap Between AI and Reality. Lecture Notes in Computer Science, vol. 14380, pp. 33\u201354. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-46002-9_3","DOI":"10.1007\/978-3-031-46002-9_3"},{"key":"6_CR34","doi-asserted-by":"publisher","unstructured":"Brorholt, A.H., Larsen, K.G., Schilling, C.: Compositional shielding and reinforcement learning for multi-agent systems. In: Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems, pp. 399\u2013407. AAMAS 2025, International Foundation for Autonomous Agents and Multiagent Systems, Richland, SC (2025). https:\/\/doi.org\/10.5555\/3709347.3743554","DOI":"10.5555\/3709347.3743554"},{"key":"6_CR35","doi-asserted-by":"publisher","unstructured":"Bulychev, P., et al.: Monitor-based statistical model checking for weighted metric temporal logic. In: Bj\u00f8rner, N., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning. Lecture Notes in Computer Science, vol.\u00a07180, pp. 168\u2013182. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_15","DOI":"10.1007\/978-3-642-28717-6_15"},{"key":"6_CR36","doi-asserted-by":"publisher","unstructured":"Bulychev, P., David, A., Guldstrand\u00a0Larsen, K., Legay, A., Miku\u010dionis, M., B\u00f8gsted\u00a0Poulsen, D.: Checking and distributing statistical model checking. In: Goodloe, A.E., Person, S. (eds.) NASA Formal Methods. Lecture Notes in Computer Science, vol.\u00a07226, pp. 449\u2013463. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_39","DOI":"10.1007\/978-3-642-28891-3_39"},{"key":"6_CR37","doi-asserted-by":"publisher","unstructured":"Bulychev, P., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B.: Rewrite-based statistical model checking of WMTL. In: Runtime Verification. Lecture Notes in Computer Science, vol.\u00a07687, pp. 260\u2013275 (2012). https:\/\/doi.org\/10.1007\/978-3-642-35632-2_25","DOI":"10.1007\/978-3-642-35632-2_25"},{"key":"6_CR38","doi-asserted-by":"publisher","unstructured":"Bulychev, P.E., Cassez, F., David, A., Larsen, K.G., Raskin, J., Reynier, P.: Controllers with minimal observation power (application to timed systems). In: Chakraborty, S., Mukund, M. (eds.) Automated Technology for Verification and Analysis (ATVA 2012). Lecture Notes in Computer Science, vol.\u00a07561, pp. 223\u2013237. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_19","DOI":"10.1007\/978-3-642-33386-6_19"},{"key":"6_CR39","doi-asserted-by":"publisher","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de\u00a0Alfaro, L. (eds.) CONCUR 2005 \u2013 Concurrency Theory. Lecture Notes in Computer Science, vol.\u00a03653, pp. 66\u201380. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11539452_9","DOI":"10.1007\/11539452_9"},{"key":"6_CR40","doi-asserted-by":"publisher","unstructured":"Cassez, F., Jessen, J.J., Larsen, K.G., Raskin, J., Reynier, P.: Automatic synthesis of robust and optimal controllers \u2013 an industrial case study. In: Majumdar, R., Tabuada, P. (eds.) Hybrid Systems: Computation and Control (HSCC 2009). Lecture Notes in Computer Science, vol.\u00a05469, pp. 90\u2013104. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-00602-9_7","DOI":"10.1007\/978-3-642-00602-9_7"},{"key":"6_CR41","doi-asserted-by":"crossref","unstructured":"Clopper, C.J., Pearson, E.S.: The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika 26(4), 404\u2013413 (1934). http:\/\/www.jstor.org\/stable\/2331986","DOI":"10.1093\/biomet\/26.4.404"},{"key":"6_CR42","doi-asserted-by":"publisher","unstructured":"David, A., et al.: Statistical model checking for stochastic hybrid systems. In: Bartocci, E., Bortolussi, L. (eds.) Hybrid Systems and Biology (HSB). Electronic Proceedings in Theoretical Computer Science (EPTCS), vol.\u00a092, pp. 122\u2013136. Newcastle Upon Tyne, UK (2012). https:\/\/doi.org\/10.4204\/EPTCS.92.9","DOI":"10.4204\/EPTCS.92.9"},{"key":"6_CR43","doi-asserted-by":"publisher","unstructured":"David, A., et al.: On time with minimal expected cost! In: Cassez, F., Raskin, J.F. (eds.) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol.\u00a08837, pp. 129\u2013145. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_10","DOI":"10.1007\/978-3-319-11936-6_10"},{"key":"6_CR44","doi-asserted-by":"publisher","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Miku\u010dionis, M., Taankvist, J.H.: Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015). Lecture Notes in Computer Science, vol.\u00a09035, pp. 206\u2013211. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_16","DOI":"10.1007\/978-3-662-46681-0_16"},{"issue":"4","key":"6_CR45","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transfer 17(4), 397\u2013415 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0361-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"6_CR46","doi-asserted-by":"publisher","unstructured":"David, A., et al.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) Formal Modeling and Analysis of Timed Systems (FORMATS 2011). Lecture Notes in Computer Science, vol.\u00a06919, pp. 80\u201396. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24310-3_7","DOI":"10.1007\/978-3-642-24310-3_7"},{"key":"6_CR47","doi-asserted-by":"publisher","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for biological systems. Int. J. Softw. Tools Technol. Transf. 17, 351\u2013367 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0323-4","DOI":"10.1007\/s10009-014-0323-4"},{"key":"6_CR48","doi-asserted-by":"publisher","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification (CAV 2011). Lecture Notes in Computer Science, vol.\u00a06806, pp. 349\u2013355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_27","DOI":"10.1007\/978-3-642-22110-1_27"},{"key":"6_CR49","doi-asserted-by":"publisher","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M.: Schedulability of Herschel-Planck revisited using statistical model checking. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies, pp. 293\u2013307. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34032-1_28","DOI":"10.1007\/978-3-642-34032-1_28"},{"key":"6_CR50","doi-asserted-by":"publisher","unstructured":"David, A., Du, D., Larsen, K.G., Miku\u010dionis, M., Skou, A.: An evaluation framework for energy aware buildings using statistical model checking. Sci. China Inf. Sci. 55, 2694\u20132707 (2012). https:\/\/doi.org\/10.1007\/s11432-012-4742-0","DOI":"10.1007\/s11432-012-4742-0"},{"key":"6_CR51","doi-asserted-by":"publisher","unstructured":"David, N., et al.: Modelling social-technical attacks with timed automata. In: Proceedings of the 7th ACM CCS International Workshop on Managing Insider Security Threats, pp. 21\u201328. MIST 2015, Association for Computing Machinery, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2808783.2808787","DOI":"10.1145\/2808783.2808787"},{"key":"6_CR52","doi-asserted-by":"publisher","unstructured":"Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: Raskin, J.F., Thiagarajan, P.S. (eds.) Formal Modeling and Analysis of Timed Systems. Lecture Notes in Computer Science, vol.\u00a04763, pp. 114\u2013129. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75454-1_10","DOI":"10.1007\/978-3-540-75454-1_10"},{"key":"6_CR53","unstructured":"Eriksen, A.B., et al.: Uppaal Stratego for intelligent traffic lights. In: 12th ITS European Congress: ITS Beyond Borders. ERTICO \u2013 ITS Europe (2017). https:\/\/vbn.aau.dk\/en\/publications\/uppaal-stratego-for-intelligent-traffic-lights"},{"key":"6_CR54","doi-asserted-by":"publisher","unstructured":"Gastin, P., Mukherjee, S., Srivathsan, B.: Fast algorithms for handling diagonal constraints in timed automata. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 11561, pp. 41\u201359. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_3","DOI":"10.1007\/978-3-030-25540-4_3"},{"key":"6_CR55","doi-asserted-by":"publisher","unstructured":"van Glabbeek, R., H\u00f6fner, P., Portmann, M., Tan, W.L.: Modelling and verifying the AODV routing protocol. Distrib. Comput. 29, 279\u2013315 (2016). https:\/\/doi.org\/10.1007\/s00446-015-0262-7","DOI":"10.1007\/s00446-015-0262-7"},{"key":"6_CR56","doi-asserted-by":"publisher","unstructured":"Goorden, M.A., Larsen, K.G., Nielsen, J.E., Nielsen, T.D., Rasmussen, M.R., Srba, J.: Learning safe and optimal control strategies for storm water detention ponds. IFAC-PapersOnLine 54(5), 13\u201318 (2021). https:\/\/doi.org\/10.1016\/j.ifacol.2021.08.467, 7th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2021)","DOI":"10.1016\/j.ifacol.2021.08.467"},{"key":"6_CR57","doi-asserted-by":"publisher","unstructured":"Grobelna, I., Gajewski, K., Karatkevich, A.: A systematic review on the applications of uppaal. Sensors 25(11) (2025). https:\/\/doi.org\/10.3390\/s25113484","DOI":"10.3390\/s25113484"},{"key":"6_CR58","doi-asserted-by":"publisher","unstructured":"Guldstrand\u00a0Larsen, K., Lorber, F., Nielsen, B.: 20 years of real real time model validation. In: Havelund, K., Peleska, J., Roscoe, B., de\u00a0Vink, E. (eds.) Formal Methods. Lecture Notes in Computer Science, vol. 10951, pp. 22\u201336. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_2","DOI":"10.1007\/978-3-319-95582-7_2"},{"key":"6_CR59","doi-asserted-by":"publisher","unstructured":"Hansen, T.D., Ibsen-Jensen, R., Miltersen, P.B.: A faster algorithm for solving one-clock priced timed games. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 \u2013 Concurrency Theory. Lecture Notes in Computer Science, vol.\u00a08052, pp. 531\u2013545. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_37","DOI":"10.1007\/978-3-642-40184-8_37"},{"key":"6_CR60","doi-asserted-by":"publisher","unstructured":"Hasrat, I.R., Jensen, P.G., Larsen, K.G., Srba, J.: A toolchain for domestic heat-pump control using uppaalstratego. Sci. Comput. Program. 230, 102987 (2023). https:\/\/doi.org\/10.1016\/j.scico.2023.102987","DOI":"10.1016\/j.scico.2023.102987"},{"issue":"1","key":"6_CR61","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1016\/S0304-3975(99)00038-9","volume":"221","author":"TA Henzinger","year":"1999","unstructured":"Henzinger, T.A., Kopke, P.W.: Discrete-time control for rectangular hybrid automata. Theoret. Comput. Sci. 221(1), 369\u2013392 (1999). https:\/\/doi.org\/10.1016\/S0304-3975(99)00038-9","journal-title":"Theoret. Comput. Sci."},{"key":"6_CR62","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. In: Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS 1992), Santa Cruz, California, USA, 22\u201325 June 1992, pp. 394\u2013406. IEEE Computer Society (1992). https:\/\/doi.org\/10.1109\/LICS.1992.185551","DOI":"10.1109\/LICS.1992.185551"},{"key":"6_CR63","doi-asserted-by":"publisher","unstructured":"Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Better abstractions for timed automata. Inf. Comput. 251, 67\u201390 (2016). https:\/\/doi.org\/10.1016\/j.ic.2016.07.004","DOI":"10.1016\/j.ic.2016.07.004"},{"key":"6_CR64","doi-asserted-by":"publisher","unstructured":"Jaeger, M., Bacci, G., Bacci, G., Larsen, K.G., Jensen, P.G.: Approximating euclidean by imprecise Markov decision processes. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles. Lecture Notes in Computer Science, vol. 12476, pp. 275\u2013289. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_15","DOI":"10.1007\/978-3-030-61362-4_15"},{"key":"6_CR65","doi-asserted-by":"publisher","unstructured":"Jaeger, M., Jensen, P.G., Guldstrand\u00a0Larsen, K., Legay, A., Sedwards, S., Taankvist, J.H.: Teaching Stratego to play ball: optimal synthesis for continuous space MDPs. In: Chen, Y.F., Cheng, C.H., Esparza, J. (eds.) Automated Technology for Verification and Analysis, pp. 81\u201397. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_5","DOI":"10.1007\/978-3-030-31784-3_5"},{"key":"6_CR66","doi-asserted-by":"publisher","unstructured":"Jaeger, M., Larsen, K.G.: Reinforcement learning for discretized euclidean MDPs. In: Steffen, B. (ed.) Bridging the Gap Between AI and Reality, pp. 312\u2013335. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-75434-0_22","DOI":"10.1007\/978-3-031-75434-0_22"},{"key":"6_CR67","doi-asserted-by":"publisher","unstructured":"Jensen, N.\u00d8., Jensen, P.G., Larsen, K.G.: Dynamic extrapolation in extended timed automata. In: Li, Y., Tahar, S. (eds.) Formal Methods and Software Engineering (ICFEM 2023). Lecture Notes in Computer Science, vol. 14308, pp. 83\u201399. Springer, Singapore (2023). https:\/\/doi.org\/10.1007\/978-981-99-7584-6_6","DOI":"10.1007\/978-981-99-7584-6_6"},{"key":"6_CR68","doi-asserted-by":"publisher","unstructured":"Jensen, N.\u00d8., Larsen, K.G., Lime, D., Srba, J.: On-the-fly symbolic algorithm for timed ATL with abstractions. In: Bouyer, P., van\u00a0de Pol, J. (eds.) 36th International Conference on Concurrency Theory, CONCUR 2025, 26\u201329 August 2025, Aarhus, Denmark. LIPIcs, vol.\u00a0348, pp. 25:1\u201325:19. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2025). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2025.25","DOI":"10.4230\/LIPICS.CONCUR.2025.25"},{"key":"6_CR69","doi-asserted-by":"publisher","unstructured":"Jensen, P.G., Kiviriga, A., Guldstrand\u00a0Larsen, K., Nyman, U., Mija\u010dika, A., H\u00f8iriis\u00a0Mortensen, J.: Monte Carlo tree search for priced timed automata. In: \u00c1brah\u00e1m, E., Paolieri, M. (eds.) Quantitative Evaluation of Systems. Lecture Notes in Computer Science, vol. 13479, pp. 381\u2013398. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-16336-4_19","DOI":"10.1007\/978-3-031-16336-4_19"},{"key":"6_CR70","doi-asserted-by":"publisher","unstructured":"Jensen, P.G., Larsen, K.G., Srba, J., S\u00f8rensen, M.G., Taankvist, J.H.: Memory efficient data structures for explicit verification of timed systems. In: Badger, J.M., Rozier, K.Y. (eds.) NASA Formal Methods (NFM 2014). Lecture Notes in Computer Science, vol.\u00a08430, pp. 307\u2013312. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06200-6_26","DOI":"10.1007\/978-3-319-06200-6_26"},{"key":"6_CR71","doi-asserted-by":"publisher","unstructured":"Jessen, J.J., Rasmussen, J.I., Larsen, K.G., David, A.: Guided controller synthesis for climate controller using uppaal tiga. In: Raskin, J., Thiagarajan, P.S. (eds.) Formal Modeling and Analysis of Timed Systems (FORMATS 2007). Lecture Notes in Computer Science, vol.\u00a04763, pp. 227\u2013240. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-75454-1_17","DOI":"10.1007\/978-3-540-75454-1_17"},{"key":"6_CR72","doi-asserted-by":"publisher","unstructured":"Jurdzi\u0144ski, M., Trivedi, A.: Reachability-time games on timed automata. In: Arge, L., Cachin, C., Jurdzi\u0144ski, T., Tarlecki, A. (eds.) Automata, Languages and Programming. Lecture Notes in Computer Science, vol.\u00a04596, pp. 838\u2013849. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73420-8_72","DOI":"10.1007\/978-3-540-73420-8_72"},{"key":"6_CR73","doi-asserted-by":"publisher","unstructured":"J\u00f8rgensen, K.Y., Larsen, K.G., Srba, J.: Time-darts: a data structure for verification of closed timed automata. Electron. Proc. Theor. Comput. Sci. (EPTCS) 102, 141\u2013155 (2012). https:\/\/doi.org\/10.4204\/eptcs.102.13","DOI":"10.4204\/eptcs.102.13"},{"key":"6_CR74","doi-asserted-by":"publisher","unstructured":"Kupferschmid, S., Hoffmann, J., Dierks, H., Behrmann, G.: Adapting an AI planning heuristic for directed model checking. In: Valmari, A. (ed.) Model Checking Software (SPIN 2006). Lecture Notes in Computer Science, vol.\u00a03925, pp. 35\u201352. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691617_3","DOI":"10.1007\/11691617_3"},{"key":"6_CR75","doi-asserted-by":"publisher","unstructured":"Kupferschmid, S., Wehrle, M., Nebel, B., Podelski, A.: Faster than uppaal? In: Gupta, A., Malik, S. (eds.) Computer Aided Verification (CAV 2008). Lecture Notes in Computer Science, vol.\u00a05123, pp. 552\u2013555. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_53","DOI":"10.1007\/978-3-540-70545-1_53"},{"key":"6_CR76","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: compact data structure and state-space reduction. In: Proceedings of the Real-Time Systems Symposium, pp. 14\u201324. IEEE (1997). https:\/\/doi.org\/10.1109\/REAL.1997.641265","DOI":"10.1109\/REAL.1997.641265"},{"key":"6_CR77","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., et al.: As cheap as possible: efficient cost-optimal reachability for priced timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer Aided Verification (CAV 2001). Lecture Notes in Computer Science, vol.\u00a02102, pp. 493\u2013505. Springer (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_47","DOI":"10.1007\/3-540-44585-4_47"},{"key":"6_CR78","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Lorber, F., Nielsen, B.: 20 years of UPPAAL enabled industrial model-based validation and beyond. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice (ISoLA 2018). Lecture Notes in Computer Science, vol. 11247, pp. 212\u2013229. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03427-6_18","DOI":"10.1007\/978-3-030-03427-6_18"},{"issue":"1\u20132","key":"6_CR79","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transfer 1(1\u20132), 134\u2013152 (1997). https:\/\/doi.org\/10.1007\/s100090050010","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"6_CR80","doi-asserted-by":"publisher","unstructured":"Maler, O., Larsen, K.G., Krogh, B.H.: On zone-based analysis of duration probabilistic automata. In: Chen, Y., Rezine, A. (eds.) Proceedings of the 12th International Workshop on Verification of Infinite-State Systems, INFINITY 2010, Singapore, 21 September 2010. Electronic Proceedings in Theoretical Computer Science (EPTCS), vol.\u00a039, pp. 33\u201346 (2010). https:\/\/doi.org\/10.4204\/EPTCS.39.3","DOI":"10.4204\/EPTCS.39.3"},{"key":"6_CR81","doi-asserted-by":"publisher","unstructured":"Ruijters, E., Stoelinga, M.: Better railway engineering through statistical model checking. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA 2016). Lecture Notes in Computer Science, vol.\u00a09952, pp. 151\u2013165. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_10","DOI":"10.1007\/978-3-319-47166-2_10"},{"key":"6_CR82","doi-asserted-by":"publisher","unstructured":"Rutkowski, M.: Two-player reachability-price games on single-clock timed automata. Electron. Proc. Theor. Comput. Sci. (EPTCS) 57, 31\u201346 (2011). https:\/\/doi.org\/10.4204\/eptcs.57.3","DOI":"10.4204\/eptcs.57.3"},{"key":"6_CR83","doi-asserted-by":"publisher","unstructured":"Tollund, R.G., Johansen, N.S., Nielsen, K.\u00d8., Torralba, \u00c1., Larsen, K.G.: Optimal infinite temporal planning: cyclic plans for priced timed automata. In: Bernardini, S., Muise, C. (eds.) Proceedings of the Thirty-Fourth International Conference on Automated Planning and Scheduling, ICAPS 2024, Banff, Alberta, Canada, 1\u20136 June 2024, pp. 588\u2013596. AAAI Press (2024). https:\/\/doi.org\/10.1609\/ICAPS.V34I1.31521","DOI":"10.1609\/ICAPS.V34I1.31521"},{"key":"6_CR84","doi-asserted-by":"crossref","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117\u2013186 (1945). http:\/\/www.jstor.org\/stable\/2235829","DOI":"10.1214\/aoms\/1177731118"}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-8617-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T14:27:36Z","timestamp":1778077656000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-8617-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9789819586165","9789819586172"],"references-count":84,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-8617-2_6","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":"1 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Summer School on Engineering Trustworthy Software Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Beijing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","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":"17 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setss2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tis.ios.ac.cn\/SETSS2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}