{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T12:02:52Z","timestamp":1757592172174,"version":"3.40.3"},"publisher-location":"Cham","reference-count":77,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031757747"},{"type":"electronic","value":"9783031757754"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-75775-4_6","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T07:26:26Z","timestamp":1731396386000},"page":"115-142","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Modest Models and Tools for Real Stochastic Timed Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8807-1548","authenticated-orcid":false,"given":"Carlos E.","family":"Budde","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8528-9215","authenticated-orcid":false,"given":"Pedro R.","family":"D\u2019Argenio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9816-6989","authenticated-orcid":false,"given":"Juan A.","family":"Fraire","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3268-8674","authenticated-orcid":false,"given":"Arnd","family":"Hartmanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8269-9489","authenticated-orcid":false,"given":"Zhen","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"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","key":"6_CR1","DOI":"10.1145\/3158668"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209\u2013229. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57318-6_30"},{"issue":"2","key":"6_CR3","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. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"6_CR4","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1109\/MCOM.2015.7060480","volume":"53","author":"G Araniti","year":"2015","unstructured":"Araniti, G., et al.: Contact graph routing in DTN space networks: overview, enhancements and performance. IEEE Comms. Magazine 53(3), 38\u201346 (2015). https:\/\/doi.org\/10.1109\/MCOM.2015.7060480","journal-title":"IEEE Comms. Magazine"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-030-72013-1_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Ashok","year":"2021","unstructured":"Ashok, P., Jackermeier, M., K\u0159et\u00ednsk\u00fd, J., Weinhuber, C., Weininger, M., Yadav, M.: dtControl 2.0: explainable strategy representation via decision tree learning steered by experts. In: TACAS 2021. LNCS, vol. 12652, pp. 326\u2013345. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_17"},{"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","key":"6_CR6","DOI":"10.3233\/978-1-61499-627-9-1"},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/978-3-319-10575-8_28","volume-title":"Handbook of Model Checking","author":"C Baier","year":"2018","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963\u2013999. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28"},{"unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)","key":"6_CR8"},{"issue":"5","key":"6_CR9","first-page":"679","volume":"6","author":"R Bellman","year":"1957","unstructured":"Bellman, R.: A Markovian decision process. J. Math. Mech. 6(5), 679\u2013684 (1957)","journal-title":"J. Math. Mech."},{"issue":"10","key":"6_CR10","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. Software Eng. 32(10), 812\u2013830 (2006). https:\/\/doi.org\/10.1109\/TSE.2006.104","journal-title":"IEEE Trans. Software Eng."},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-540-45232-4_8","volume-title":"Computer Performance Evaluation. Modelling Techniques and Tools","author":"H Bohnenkamp","year":"2003","unstructured":"Bohnenkamp, H., Hermanns, H., Katoen, J.-P., Klaren, R.: The Modest modeling tool and its implementation. In: Kemper, P., Sanders, W.H. (eds.) TOOLS 2003. LNCS, vol. 2794, pp. 116\u2013133. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45232-4_8"},{"unstructured":"Bonet, B., Geffner, H.: Labeled RTDP: improving the convergence of real-time dynamic programming. In: Giunchiglia, E., Muscettola, N., Nau, D.S. (eds.) 13th International Conference on Automated Planning and Scheduling (ICAPS), pp. 12\u201321. AAAI (2003)","key":"6_CR12"},{"key":"6_CR13","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."},{"unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A.: Digging for decision trees: a case study in strategy sampling and learning. In: International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA) (2024), submitted, under review","key":"6_CR14"},{"issue":"6","key":"6_CR15","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":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-662-54580-5_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"CE Budde","year":"2017","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.) TACAS 2017. LNCS, vol. 10206, pp. 151\u2013168. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-030-83723-5_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends","author":"CE Budde","year":"2021","unstructured":"Budde, C.E., et al.: On correctness, precision, and performance in quantitative verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12479, pp. 216\u2013241. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-83723-5_15"},{"doi-asserted-by":"publisher","unstructured":"Bulychev, P.E., et al.: UPPAAL-SMC: Statistical model checking for priced timed automata. In: Wiklicky, H., Massink, M. (eds.) 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL). EPTCS, vol.\u00a085, pp. 1\u201316 (2012). https:\/\/doi.org\/10.4204\/EPTCS.85.1","key":"6_CR18","DOI":"10.4204\/EPTCS.85.1"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-030-17465-1_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Butkova","year":"2019","unstructured":"Butkova, Y., Fox, G.: Optimal time-bounded reachability analysis for concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 191\u2013208. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_11"},{"doi-asserted-by":"publisher","unstructured":"Butkova, Y., Hartmanns, A., Hermanns, H.: A Modest approach to Markov automata. ACM Trans. Model. Comput. Simul. 31(3), 14:1\u201314:34 (2021). https:\/\/doi.org\/10.1145\/3449355","key":"6_CR20","DOI":"10.1145\/3449355"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-319-24953-7_12","volume-title":"Automated Technology for Verification and Analysis","author":"Y Butkova","year":"2015","unstructured":"Butkova, Y., Hatefi, H., Hermanns, H., Kr\u010d\u00e1l, J.: Optimal continuous time markov decisions. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 166\u2013182. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_12"},{"unstructured":"Claus, C., Boutilier, C.: The dynamics of reinforcement learning in cooperative multiagent systems. In: Mostow, J., Rich, C. (eds.) 15th National Conference on Artificial Intelligence and 10th Innovative Applications of Artificial Intelligence Conference (AAAI, IAAI), pp. 746\u2013752. AAAI Press\/The MIT Press (1998)","key":"6_CR22"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-030-55754-6_17","volume-title":"NASA Formal Methods","author":"PR D\u2019Argenio","year":"2020","unstructured":"D\u2019Argenio, P.R., Fraire, J.A., Hartmanns, A.: Sampling distributed schedulers for\u00a0resilient space communication. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 291\u2013310. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_17"},{"doi-asserted-by":"crossref","unstructured":"D\u2019Argenio, P.R., Fraire, J.A., Hartmanns, A., Raverta, F.: Comparing statistical, analytical, and learning-based routing approaches for delay-tolerant networks. ACM Trans. Model. Comput. Simul. (2024). to appear","key":"6_CR24","DOI":"10.1145\/3665927"},{"key":"6_CR25","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.11214677","author":"PR D\u2019Argenio","year":"2024","unstructured":"D\u2019Argenio, P.R., Fraire, J.A., Hartmanns, A., Raverta, F.: Comparing statistical, analytical, and learning-based routing approaches for delay-tolerant networks (artifact). Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.11214677. , to appear","journal-title":"Zenodo"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-33693-0_7","volume-title":"Integrated Formal Methods","author":"PR D\u2019Argenio","year":"2016","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Legay, A., Sedwards, S.: Statistical approximation of optimal schedulers for probabilistic timed automata. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 99\u2013114. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_7"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-030-03421-4_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"PR D\u2019Argenio","year":"2018","unstructured":"D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: Lightweight statistical model checking in nondeterministic continuous time. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 336\u2013353. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_22"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45605-8_5","volume-title":"Process Algebra and Probabilistic Methods: Performance Modeling and Verification","author":"PR D\u2019Argenio","year":"2002","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reduction and Refinement Strategies for Probabilistic Analysis. In: Hermanns, H., Segala, R. (eds.) PAPM-PROBMIV 2002. LNCS, vol. 2399, pp. 57\u201376. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45605-8_5"},{"issue":"4","key":"6_CR29","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/S10009-015-0383-0","volume":"17","author":"PR D\u2019Argenio","year":"2015","unstructured":"D\u2019Argenio, P.R., Legay, A., Sedwards, S., Traonouez, L.M.: Smart sampling for lightweight verification of Markov decision processes. Int. J. Softw. Tools Technol. Transf. 17(4), 469\u2013484 (2015). https:\/\/doi.org\/10.1007\/S10009-015-0383-0","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Wolovick, N., Terraf, P.S., Celayes, P.: Nondeterministic labeled Markov processes: Bisimulations and logical characterization. In: 6th International Conference on Quantitative Evaluation of Systems (QEST). pp. 11\u201320. IEEE Computer Society (2009). https:\/\/doi.org\/10.1109\/QEST.2009.17","key":"6_CR30","DOI":"10.1109\/QEST.2009.17"},{"doi-asserted-by":"publisher","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Mikucionis, M., Taankvist, J.H.: Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol.\u00a09035, pp. 206\u2013211. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_16","key":"6_CR31","DOI":"10.1007\/978-3-662-46681-0_16"},{"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 (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_27","key":"6_CR32","DOI":"10.1007\/978-3-642-22110-1_27"},{"doi-asserted-by":"publisher","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: 25th Annual IEEE Symposium on Logic in Computer Science (LICS). pp. 342\u2013351. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/LICS.2010.41","key":"6_CR33","DOI":"10.1109\/LICS.2010.41"},{"doi-asserted-by":"publisher","unstructured":"Fehnker, A., Chaudhary, K.: Twenty percent and a few days \u2013 optimising a Bitcoin majority attack. In: Dutle, A., Mu\u00f1oz, C.A., Narkawicz, A. (eds.) 10th International NASA Formal Methods Symposium (NFM). Lecture Notes in Computer Science, vol. 10811, pp. 157\u2013163. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-77935-5_11","key":"6_CR34","DOI":"10.1007\/978-3-319-77935-5_11"},{"doi-asserted-by":"publisher","unstructured":"Fraire, J.A., De Jonck\u00e8re, O., Burleigh, S.C.: Routing in the space Internet: A contact graph routing tutorial. Journal of Network and Computer Applications 174, 102884 (2021). https:\/\/doi.org\/10.1016\/j.jnca.2020.102884","key":"6_CR35","DOI":"10.1016\/j.jnca.2020.102884"},{"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","key":"6_CR36","DOI":"10.1145\/1967701.1967710"},{"issue":"3","key":"6_CR37","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/S10009-007-0062-X","volume":"10","author":"G Frehse","year":"2008","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf. 10(3), 263\u2013279 (2008). https:\/\/doi.org\/10.1007\/S10009-007-0062-X","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"6_CR38","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/S10009-012-0244-Z","volume":"15","author":"H Garavel","year":"2013","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89\u2013107 (2013). https:\/\/doi.org\/10.1007\/S10009-012-0244-Z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"doi-asserted-by":"publisher","unstructured":"Giro, S., D\u2019Argenio, P.R.: Quantitative model checking revisited: Neither decidable nor approximable. In: Raskin, J.F., Thiagarajan, P.S. (eds.) 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). Lecture Notes in Computer Science, vol.\u00a04763, pp. 179\u2013194. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-75454-1_14","key":"6_CR39","DOI":"10.1007\/978-3-540-75454-1_14"},{"issue":"3","key":"6_CR40","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.entcs.2009.10.005","volume":"253","author":"S Giro","year":"2009","unstructured":"Giro, S., D\u2019Argenio, P.R.: On the expressive power of schedulers in distributed probabilistic systems. Electron. Notes Theor. Comput. Sci. 253(3), 45\u201371 (2009). https:\/\/doi.org\/10.1016\/j.entcs.2009.10.005","journal-title":"Electron. Notes Theor. Comput. Sci."},{"doi-asserted-by":"publisher","unstructured":"Haddad, S., Monmege, B.: Reachability in MDPs: Refining convergence of value iteration. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) 8th International Workshop on Reachability Problems (RP). Lecture Notes in Computer Science, vol.\u00a08762, pp. 125\u2013137. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11439-2_10","key":"6_CR41","DOI":"10.1007\/978-3-319-11439-2_10"},{"key":"6_CR42","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. Theor. Comput. Sci. 735, 111\u2013131 (2018). https:\/\/doi.org\/10.1016\/J.TCS.2016.12.003","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Hartmanns, A.: A comparison of time- and reward-bounded probabilistic model checking techniques. In: Fr\u00e4nzle, M., Kapur, D., Zhan, N. (eds.) Second International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA). Lecture Notes in Computer Science, vol.\u00a09984, pp. 85\u2013100 (2016). https:\/\/doi.org\/10.1007\/978-3-319-47677-3_6","key":"6_CR43","DOI":"10.1007\/978-3-319-47677-3_6"},{"doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Hartmanns, A.: Symblicit exploration and elimination for probabilistic model checking. In: Hung, C.C., Hong, J., Bechini, A., Song, E. (eds.) 36th ACM\/SIGAPP Symposium on Applied Computing (SAC). pp. 1798\u20131806. ACM (2021). https:\/\/doi.org\/10.1145\/3412841.3442052","key":"6_CR44","DOI":"10.1145\/3412841.3442052"},{"doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Hartmanns, A., Hensel, C., Klauck, M., Klein, J., Kret\u00ednsk\u00fd, J., Parker, D., Quatmann, T., Ruijters, E., Steinmetz, M.: The 2019 comparison of tools for the analysis of quantitative formal models (QComp 2019 competition report). In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) 25 Years of TACAS: TOOLympics. Lecture Notes in Computer Science, vol. 11429, pp. 69\u201392. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_5","key":"6_CR45","DOI":"10.1007\/978-3-030-17502-3_5"},{"issue":"2","key":"6_CR46","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."},{"doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: A web-based probabilistic model checker. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) 19th International Symposium on Formal Methods (FM). Lecture Notes in Computer Science, vol.\u00a08442, pp. 312\u2013317. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_22","key":"6_CR47","DOI":"10.1007\/978-3-319-06410-9_22"},{"doi-asserted-by":"publisher","unstructured":"Hartmanns, A.: An overview of Modest models and tools for real stochastic timed systems. In: Dubslaff, C., Luttik, B. (eds.) 5th Workshop on Models for Formal Analysis of Real Systems (MARS@ETAPS). EPTCS, vol.\u00a0355, pp. 1\u201312 (2022). https:\/\/doi.org\/10.4204\/EPTCS.355.1","key":"6_CR48","DOI":"10.4204\/EPTCS.355.1"},{"doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: The Modest Toolset: An integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, 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.\u00a08413, pp. 593\u2013598. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51","key":"6_CR49","DOI":"10.1007\/978-3-642-54862-8_51"},{"doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: Explicit model checking of very large MDP using partitioning and secondary storage. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) 13th International Symposium on Automated Technology for Verification and Analysis (ATVA). Lecture Notes in Computer Science, vol.\u00a09364, pp. 131\u2013147. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_10","key":"6_CR50","DOI":"10.1007\/978-3-319-24953-7_10"},{"doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: A Modest Markov automata tutorial. In: Kr\u00f6tzsch, M., Stepanova, D. (eds.) 15th International Reasoning Web Summer School. Lecture Notes in Computer Science, vol. 11810, pp. 250\u2013276. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31423-1_8","key":"6_CR51","DOI":"10.1007\/978-3-030-31423-1_8"},{"doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H., Berrang, P.: A comparative analysis of decentralized power grid stabilization strategies. In: Rose, O., Uhrmacher, A.M. (eds.) Winter Simulation Conference (WSC). pp. 158:1\u2013158:13. WSC (2012). https:\/\/doi.org\/10.1109\/WSC.2012.6465083","key":"6_CR52","DOI":"10.1109\/WSC.2012.6465083"},{"doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: Lahiri, S.K., Wang, C. (eds.) 32nd International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 12225, pp. 488\u2013511. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26","key":"6_CR53","DOI":"10.1007\/978-3-030-53291-8_26"},{"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 (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20","key":"6_CR54","DOI":"10.1007\/978-3-030-17462-0_20"},{"doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Sedwards, S., D\u2019Argenio, P.R.: Efficient simulation-based verification of probabilistic timed automata. In: 2017 Winter Simulation Conference (WSC). pp. 1419\u20131430. IEEE (2017). https:\/\/doi.org\/10.1109\/WSC.2017.8247885","key":"6_CR55","DOI":"10.1109\/WSC.2017.8247885"},{"unstructured":"Hatefi-Ardakani, H.: Finite horizon analysis of Markov automata. Ph.D. thesis, Saarland University, Germany (2017), http:\/\/scidok.sulb.uni-saarland.de\/volltexte\/2017\/6743\/","key":"6_CR56"},{"issue":"4","key":"6_CR57","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/S10009-021-00633-Z","volume":"24","author":"C Hensel","year":"2022","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/S10009-021-00633-Z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"unstructured":"Howard, R.A.: Dynamic Programming and Markov Processes. MIT Press (1960)","key":"6_CR58"},{"doi-asserted-by":"publisher","unstructured":"Kamali, M., Katoen, J.P.: Probabilistic model checking of AODV. In: Gribaudo, M., Jansen, D.N., Remke, A. (eds.) 17th International Conference on Quantitative Evaluation of Systems (QEST). Lecture Notes in Computer Science, vol. 12289, pp. 54\u201373. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-59854-9_6","key":"6_CR59","DOI":"10.1007\/978-3-030-59854-9_6"},{"doi-asserted-by":"publisher","unstructured":"Klauck, M., Hermanns, H.: A Modest approach to dynamic heuristic search in probabilistic model checking. In: Abate, A., Marin, A. (eds.) 18th International Conference on Quantitative Evaluation of Systems (QEST). Lecture Notes in Computer Science, vol. 12846, pp. 15\u201338. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-85172-9_2","key":"6_CR60","DOI":"10.1007\/978-3-030-85172-9_2"},{"doi-asserted-by":"publisher","unstructured":"K\u00f6hl, M.A., Klauck, M., Hermanns, H.: Momba: JANI meets Python. In: Groote, J.F., Larsen, K.G. (eds.) 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 12652, pp. 389\u2013398. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_23","key":"6_CR61","DOI":"10.1007\/978-3-030-72013-1_23"},{"unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Of cores: A partial-exploration framework for Markov decision processes. Log. Methods Comput. Sci. 16(4) (2020), https:\/\/lmcs.episciences.org\/6833","key":"6_CR62"},{"doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic 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. 585\u2013591. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","key":"6_CR63","DOI":"10.1007\/978-3-642-22110-1_47"},{"issue":"1","key":"6_CR64","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"MZ Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods Syst. Des. 29(1), 33\u201378 (2006). https:\/\/doi.org\/10.1007\/s10703-006-0005-2","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"6_CR65","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"MZ Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101\u2013150 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(01)00046-9","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"publisher","unstructured":"Lanotte, R., Merro, M., Munteanu, A.: A Modest security analysis of cyber-physical systems: A case study. In: Baier, C., Caires, L. (eds.) 38th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE). Lecture Notes in Computer Science, vol. 10854, pp. 58\u201378. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-92612-4_4","key":"6_CR66","DOI":"10.1007\/978-3-319-92612-4_4"},{"doi-asserted-by":"publisher","unstructured":"Legay, A., Sedwards, S., Traonouez, L.M.: Scalable verification of Markov decision processes. In: Canal, C., Idani, A. (eds.) 4th Workshop on Formal Methods in the Development of Software (WS-FMDS). Lecture Notes in Computer Science, vol.\u00a08938, pp. 350\u2013362. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-15201-1_23","key":"6_CR67","DOI":"10.1007\/978-3-319-15201-1_23"},{"doi-asserted-by":"publisher","unstructured":"Lewis, B., Hartmanns, A., Basu, P., Shridevi, R.J., Chakraborty, K., Roy, S., Zhang, Z.: Probabilistic verification for reliable network-on-chip system design. In: Larsen, K.G., Willemse, T.A.C. (eds.) 24th International Conference on Formal Methods for Industrial Critical Systems (FMICS). Lecture Notes in Computer Science, vol. 11687, pp. 110\u2013126. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-27008-7_7","key":"6_CR68","DOI":"10.1007\/978-3-030-27008-7_7"},{"unstructured":"Nakamoto, S.: Bitcoin: A peer-to-peer electronic cash system (2008), https:\/\/bitcoin.org\/bitcoin.pdf","key":"6_CR69"},{"issue":"3","key":"6_CR70","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/s10458-005-2631-2","volume":"11","author":"L Panait","year":"2005","unstructured":"Panait, L., Luke, S.: Cooperative multi-agent learning: The state of the art. Auton. Agents Multi Agent Syst. 11(3), 387\u2013434 (2005). https:\/\/doi.org\/10.1007\/s10458-005-2631-2","journal-title":"Auton. Agents Multi Agent Syst."},{"doi-asserted-by":"publisher","unstructured":"Quatmann, T., Katoen, J.: Sound value iteration. In: Chockler, H., Weissenbacher, G. (eds.) 30th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 10981, pp. 643\u2013661. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37","key":"6_CR71","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"6_CR72","doi-asserted-by":"publisher","DOI":"10.1016\/j.adhoc.2021.102663","volume":"123","author":"FD Raverta","year":"2021","unstructured":"Raverta, F.D., Fraire, J.A., Madoery, P.G., Demasi, R.A., Finochietto, J.M., D\u2019Argenio, P.R.: Routing in delay-tolerant networks under uncertain contact plans. Ad Hoc Netw. 123, 102663 (2021). https:\/\/doi.org\/10.1016\/j.adhoc.2021.102663","journal-title":"Ad Hoc Netw."},{"doi-asserted-by":"publisher","unstructured":"Roberts, R., Lewis, B., Hartmanns, A., Basu, P., Roy, S., Chakraborty, K., Zhang, Z.: Probabilistic verification for reliability of a two-by-two network-on-chip system. In: Lluch-Lafuente, A., Mavridou, A. (eds.) 26th International Conference on Formal Methods for Industrial Critical Systems (FMICS). Lecture Notes in Computer Science, vol. 12863, pp. 232\u2013248. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-85248-1_16","key":"6_CR73","DOI":"10.1007\/978-3-030-85248-1_16"},{"doi-asserted-by":"publisher","unstructured":"Rubino, G., Tuffin, B. (eds.): Rare Event Simulation using Monte Carlo Methods. Wiley (2009). https:\/\/doi.org\/10.1002\/9780470745403","key":"6_CR74","DOI":"10.1002\/9780470745403"},{"doi-asserted-by":"publisher","unstructured":"Sproston, J.: Decidable model checking of probabilistic hybrid automata. In: Joseph, M. (ed.) 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). Lecture Notes in Computer Science, vol.\u00a01926, pp. 31\u201345. Springer (2000). https:\/\/doi.org\/10.1007\/3-540-45352-0_5","key":"6_CR75","DOI":"10.1007\/3-540-45352-0_5"},{"key":"6_CR76","doi-asserted-by":"publisher","DOI":"10.1109\/TNN.1998.712192","volume-title":"Reinforcement learning - An introduction","author":"RS Sutton","year":"1998","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement learning - An introduction. MIT Press, Adaptive computation and machine learning (1998)"},{"doi-asserted-by":"publisher","unstructured":"Watkins, C.J.C.H., Dayan, P.: Q-learning. Mach. Learn. 8, 279\u2013292 (1992). https:\/\/doi.org\/10.1007\/BF00992698","key":"6_CR77","DOI":"10.1007\/BF00992698"}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75775-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T08:03:07Z","timestamp":1731398587000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75775-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031757747","9783031757754"],"references-count":77,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75775-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}