{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:42:57Z","timestamp":1759365777437,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032057914","type":"print"},{"value":"9783032057921","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:00:00Z","timestamp":1759363200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:00:00Z","timestamp":1759363200000},"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-05792-1_5","type":"book-chapter","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T10:31:33Z","timestamp":1759314693000},"page":"83-94","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Statistical Model Checking Beyond Means: Quantiles, CVaR, and\u00a0the\u00a0DKW Inequality"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8807-1548","authenticated-orcid":false,"given":"Carlos E.","family":"Budde","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3268-8674","authenticated-orcid":false,"given":"Arnd","family":"Hartmanns","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1712-2165","authenticated-orcid":false,"given":"Tobias","family":"Meggendorfer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0163-2152","authenticated-orcid":false,"given":"Maximilian","family":"Weininger","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8047-4094","authenticated-orcid":false,"given":"Patrick","family":"Wienh\u00f6ft","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,10,2]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018). https:\/\/doi.org\/10.1145\/3158668","DOI":"10.1145\/3158668"},{"key":"5_CR2","volume-title":"Advanced Econometrics","author":"T Amemiya","year":"1985","unstructured":"Amemiya, T.: Advanced Econometrics. Harvard University Press, Boston (1985)"},{"key":"5_CR3","first-page":"249","volume":"43","author":"TW Anderson","year":"1969","unstructured":"Anderson, T.W.: Confidence limits for the value of an arbitrary bounded random variable with a continuous distribution function. Bull. Int. Stat. Inst. 43, 249\u2013251 (1969)","journal-title":"Bull. Int. Stat. Inst."},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Baier, C.: Probabilistic model checking. In: Esparza, J., Grumberg, O., Sickert, S. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series \u2013 D: Information and Communication Security, vol.\u00a045, pp. 1\u201323. IOS Press (2016). https:\/\/doi.org\/10.3233\/978-1-61499-627-9-1","DOI":"10.3233\/978-1-61499-627-9-1"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 963\u2013999. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"5_CR6","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2024.105214","volume":"301","author":"C Baier","year":"2024","unstructured":"Baier, C., Chatterjee, K., Meggendorfer, T., Piribauer, J.: Entropic risk for turnbased stochastic games. Inf. Comput. 301, 105214 (2024). https:\/\/doi.org\/10.1016\/J.IC.2024.105214","journal-title":"Inf. Comput."},{"key":"5_CR7","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008). https:\/\/mitpress.mit.edu\/books\/principles-model-checking"},{"key":"5_CR8","unstructured":"Baier, C., Piribauer, J., Starke, M.: Risk-averse optimization of total rewards in Markovian models using deviation measures. In: CONCUR. LIPIcs, vol.\u00a0311, pp. 9:1\u20139:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024)"},{"issue":"10","key":"5_CR9","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"HC Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H.C., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.P.: Modest: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812\u2013830 (2006). https:\/\/doi.org\/10.1109\/TSE.2006.104","journal-title":"IEEE Trans. Softw. Eng."},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/j.jcss.2016.09.009","volume":"84","author":"T Br\u00e1zdil","year":"2017","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Forejt, V., Kucera, A.: Trading performance for stability in Markov decision processes. J. Comput. Syst. Sci. 84, 144\u2013170 (2017)","journal-title":"J. Comput. Syst. Sci."},{"key":"5_CR11","unstructured":"Brihaye, T., Chatterjee, K., Mohr, S., Weininger, M.: Risk-aware Markov decision processes using cumulative prospect theory. In: LICS (2025). https:\/\/arxiv.org\/abs\/2505.09514"},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/J.SCICO.2019.01.006","volume":"174","author":"CE Budde","year":"2019","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A.: Automated compositional importance splitting. Sci. Comput. Program. 174, 90\u2013108 (2019). https:\/\/doi.org\/10.1016\/J.SCICO.2019.01.006","journal-title":"Sci. Comput. Program."},{"issue":"6","key":"5_CR13","doi-asserted-by":"publisher","first-page":"759","DOI":"10.1007\/S10009-020-00563-2","volume":"22","author":"CE Budde","year":"2020","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: An efficient statistical model checker for nondeterminism and rare events. Int. J. Softw. Tools Technol. Transf. 22(6), 759\u2013780 (2020). https:\/\/doi.org\/10.1007\/S10009-020-00563-2","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 10206, pp. 151\u2013168. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9","DOI":"10.1007\/978-3-662-54580-5_9"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Budde, C.E., Hartmanns, A., Meggendorfer, T., Weininger, M., Wienh\u00f6ft, P.: Sound statistical model checking for probabilities and expected rewards. In: TACAS (1). Lecture Notes in Computer Science, vol. 15696, pp. 167\u2013190. Springer, Heidelberg (2025). https:\/\/doi.org\/10.1007\/978-3-031-90643-5_9","DOI":"10.1007\/978-3-031-90643-5_9"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Budde, C.E., Hartmanns, A., Meggendorfer, T., Weininger, M., Wienh\u00f6ft, P.: Statistical model checking beyond means: Quantiles, CVaR, and the DKW inequality (extended version). CoRR (2025). https:\/\/doi.org\/10.48550\/arXiv.2509.11859","DOI":"10.48550\/arXiv.2509.11859"},{"issue":"4","key":"5_CR17","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1093\/biomet\/26.4.404","volume":"26","author":"C Clopper","year":"1934","unstructured":"Clopper, C., Pearson, E.: The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika 26(4), 404\u2013413 (1934). https:\/\/doi.org\/10.1093\/biomet\/26.4.404","journal-title":"Biometrika"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Fraire, J.A., Hartmanns, A., Raverta, F.D.: Comparing statistical, analytical, and learning-based routing approaches for delay-tolerant networks. ACM Trans. Model. Comput. Simul. 35(2) (2025). https:\/\/doi.org\/10.1145\/3665927","DOI":"10.1145\/3665927"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: Lightweight statistical model checking in nondeterministic continuous time. In: Margaria, T., Steffen, B. (eds.) 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA). Lecture Notes in Computer Science, vol. 11245, pp. 336\u2013353. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_22","DOI":"10.1007\/978-3-030-03421-4_22"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Monti, R.E.: Input\/output stochastic automata with urgency: confluence and weak determinism. In: Fischer, B., Uustalu, T. (eds.) 15th International Colloquium on Theoretical Aspects of Computing (ICTAC). Lecture Notes in Computer Science, vol. 11187, pp. 132\u2013152. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-030-02508-3_8","DOI":"10.1007\/978-3-030-02508-3_8"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) 23rd International Conference on Computer Aided Verification (CAV). 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"},{"issue":"3","key":"5_CR22","doi-asserted-by":"publisher","first-page":"642","DOI":"10.1214\/aoms\/1177728174","volume":"27","author":"A Dvoretzky","year":"1956","unstructured":"Dvoretzky, A., Kiefer, J., Wolfowitz, J.: Asymptotic minimax character of the sample distribution function and of the classical multinomial estimator. Ann. Math. Stat. 27(3), 642\u2013669 (1956). https:\/\/doi.org\/10.1214\/aoms\/1177728174","journal-title":"Ann. Math. Stat."},{"issue":"4","key":"5_CR23","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/S10009-014-0329-Y","volume":"17","author":"C Ellen","year":"2015","unstructured":"Ellen, C., Gerwinn, S., Fr\u00e4nzle, M.: Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains. Int. J. Softw. Tools Technol. Transf. 17(4), 485\u2013504 (2015). https:\/\/doi.org\/10.1007\/S10009-014-0329-Y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"5_CR24","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/s007800200072","volume":"6","author":"H F\u00f6llmer","year":"2002","unstructured":"F\u00f6llmer, H., Schied, A.: Convex measures of risk and trading constraints. Finan. Stochast. 6, 429\u2013447 (2002)","journal-title":"Finan. Stochast."},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Fr\u00e4nzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurability and safety verification for stochastic hybrid systems. In: Caccamo, M., Frazzoli, E., Grosu, R. (eds.) 14th ACM International Conference on Hybrid Systems: Computation and Control (HSCC). pp. 43\u201352. ACM (2011). https:\/\/doi.org\/10.1145\/1967701.1967710","DOI":"10.1145\/1967701.1967710"},{"issue":"2","key":"5_CR26","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/S10703-012-0167-Z","volume":"43","author":"EM Hahn","year":"2013","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 43(2), 191\u2013232 (2013). https:\/\/doi.org\/10.1007\/S10703-012-0167-Z","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: The Modest Toolset: an integrated environment for quantitative modelling and verification. In: Abraham, E., Havelund, K. (eds.) 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 8413, pp. 593\u2013598. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner\u2019s guide to MDP model checking algorithms. In: Sankaranarayanan, S., Sharygina, N. (eds.) 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 13993, pp. 469\u2013488. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_24","DOI":"10.1007\/978-3-031-30823-9_24"},{"key":"5_CR29","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: Vojnar, T., Zhang, L. (eds.) 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 11427, pp. 344\u2013350. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20","DOI":"10.1007\/978-3-030-17462-0_20"},{"issue":"301","key":"5_CR30","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1080\/01621459.1963.10500830","volume":"58","author":"W Hoeffding","year":"1963","unstructured":"Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58(301), 13\u201330 (1963). https:\/\/doi.org\/10.1080\/01621459.1963.10500830","journal-title":"J. Am. Stat. Assoc."},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"Kr\u00e4hmann, D., Schubert, J., Baier, C., Dubslaff, C.: Ratio and weight quantiles. In: Italiano, G.F., Pighizzini, G., Sannella, D. (eds.) 40th International Symposium on Mathematical Foundations of Computer Science 2015 (MFCS). Lecture Notes in Computer Science, vol.\u00a09234, pp. 344\u2013356. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48057-1_27","DOI":"10.1007\/978-3-662-48057-1_27"},{"key":"5_CR32","doi-asserted-by":"publisher","unstructured":"K\u0159et\u00ednsk\u00fd, J.: Survey of statistical verification of linear unbounded properties: model checking and distances. In: ISoLA (1). Lecture Notes in Computer Science, vol. 9952, pp. 27\u201345. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_3","DOI":"10.1007\/978-3-319-47166-2_3"},{"key":"5_CR33","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Conditional value-at-risk for reachability and mean payoff in Markov decision processes. In: Dawar, A., Gr\u00e4del, E. (eds.) 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 609\u2013618. ACM (2018).https:\/\/doi.org\/10.1145\/3209108.3209176","DOI":"10.1145\/3209108.3209176"},{"key":"5_CR34","doi-asserted-by":"publisher","unstructured":"Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical model checking. In: Steffen, B., Woeginger, G.J. (eds.) Computing and Software Science \u2013 State of the Art and Perspectives, Lecture Notes in Computer Science, vol. 10000, pp. 478\u2013504. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_23","DOI":"10.1007\/978-3-319-91908-9_23"},{"issue":"3","key":"5_CR35","doi-asserted-by":"publisher","first-page":"1057","DOI":"10.1016\/j.ejor.2023.06.022","volume":"311","author":"S Ma","year":"2023","unstructured":"Ma, S., Ma, X., Xia, L.: A unified algorithm framework for mean-variance optimization in discounted Markov decision processes. Eur. J. Oper. Res. 311(3), 1057\u20131067 (2023)","journal-title":"Eur. J. Oper. Res."},{"key":"5_CR36","unstructured":"Mannor, S., Tsitsiklis, J.N.: Mean-variance optimization in Markov decision processes. In: ICML, pp. 177\u2013184. Omnipress (2011)"},{"issue":"2","key":"5_CR37","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1111\/j.1540-6261.1991.tb02669.x","volume":"46","author":"HM Markowitz","year":"1991","unstructured":"Markowitz, H.M.: Foundations of portfolio theory. J. Finan. 46(2), 469\u2013477 (1991)","journal-title":"J. Finan."},{"key":"5_CR38","doi-asserted-by":"publisher","unstructured":"Massart, P.: The tight constant in the Dvoretzky-Kiefer-Wolfowitz inequality. Ann. Probab. 18(3), 1269\u20131283 (1990). https:\/\/doi.org\/10.1214\/aop\/1176990746","DOI":"10.1214\/aop\/1176990746"},{"key":"5_CR39","doi-asserted-by":"publisher","unstructured":"Niehage, M., Hartmanns, A., Remke, A.: Learning optimal decisions for stochastic hybrid systems. In: Arun-Kumar, S., M\u00e9ry, D., Saha, I., Zhang, L. (eds.) 19th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), pp. 44\u201355. ACM (2021). https:\/\/doi.org\/10.1145\/3487212.3487339","DOI":"10.1145\/3487212.3487339"},{"key":"5_CR40","doi-asserted-by":"publisher","unstructured":"Pilch, C., Remke, A.: Statistical model checking for hybrid Petri nets with multiple general transitions. In: 47th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 475\u2013486. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/DSN.2017.41","DOI":"10.1109\/DSN.2017.41"},{"key":"5_CR41","unstructured":"Piribauer, J., Sankur, O., Baier, C.: The variance-penalized stochastic shortest path problem. In: ICALP. LIPIcs, vol.\u00a0229, pp. 129:1\u2013129:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"5_CR42","doi-asserted-by":"publisher","unstructured":"Randour, M., Raskin, J.F., Sankur, O.: Percentile queries in multi-dimensional Markov decision processes. Formal Methods Syst. Des. 50(2\u20133), 207\u2013248 (2017). https:\/\/doi.org\/10.1007\/S10703-016-0262-7","DOI":"10.1007\/S10703-016-0262-7"},{"issue":"7","key":"5_CR43","doi-asserted-by":"publisher","first-page":"1443","DOI":"10.1016\/S0378-4266(02)00271-6","volume":"26","author":"RT Rockafellar","year":"2002","unstructured":"Rockafellar, R.T., Uryasev, S.: Conditional value-at-risk for general loss distributions. J. Bank. Finan. 26(7), 1443\u20131471 (2002)","journal-title":"J. Bank. Finan."},{"issue":"4","key":"5_CR44","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00122574","volume":"5","author":"A Tversky","year":"1992","unstructured":"Tversky, A., Kahneman, D.: Advances in prospect theory: cumulative representation of uncertainty. J. Risk Uncertain. 5(4), 297\u2013323 (1992)","journal-title":"J. Risk Uncertain."},{"key":"5_CR45","doi-asserted-by":"publisher","unstructured":"Ummels, M., Baier, C.: Computing quantiles in Markov reward models. In: Pfenning, F. (ed.) Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, 16\u201324 March 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a07794, pp. 353\u2013368. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37075-5_23","DOI":"10.1007\/978-3-642-37075-5_23"},{"issue":"2","key":"5_CR46","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A Wald","year":"1945","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117\u2013186 (1945). https:\/\/doi.org\/10.1214\/aoms\/1177731118","journal-title":"Ann. Math. Stat."},{"key":"5_CR47","unstructured":"Wirch, J.L., Hardy, M.R.: Distortion risk measures: coherence and stochastic dominance. In: International Congress on Insurance: Mathematics and Economics, pp. 15\u201317. Citeseer (2001)"},{"key":"5_CR48","doi-asserted-by":"publisher","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) 14th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 2404, pp. 223\u2013235. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_17","DOI":"10.1007\/3-540-45657-0_17"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-05792-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T10:31:35Z","timestamp":1759314695000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-05792-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,2]]},"ISBN":["9783032057914","9783032057921"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-05792-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,2]]},"assertion":[{"value":"2 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The modes tool is available at . An artifact for this paper\u2014a reproduction package with the models and commands for the experiments in Sect.\u00a0\u2014is available at DOI\u00a0.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data Availability"}},{"value":"QEST+FORMATS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aarhus","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denmark","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":"26 August 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 August 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"qest2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.qest-formats.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}