{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T04:47:00Z","timestamp":1743137220102,"version":"3.40.3"},"publisher-location":"Cham","reference-count":60,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031377082"},{"type":"electronic","value":"9783031377099"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We provide a novel method for sensitivity analysis of parametric robust Markov chains. These models incorporate parameters and sets of probability distributions to alleviate the often unrealistic assumption that precise probabilities are available. We measure sensitivity in terms of partial derivatives with respect to the uncertain transition probabilities regarding measures such as the expected reward. As our main contribution, we present an efficient method to compute these partial derivatives. To scale our approach to models with thousands of parameters, we present an extension of this method that selects the subset of<jats:italic>k<\/jats:italic>parameters with the highest partial derivative. Our methods are based on linear programming and differentiating these programs around a given value for the parameters. The experiments show the applicability of our approach on models with over a million states and thousands of parameters. Moreover, we embed the results within an iterative learning scheme that profits from having access to a dedicated sensitivity analysis.<\/jats:p>","DOI":"10.1007\/978-3-031-37709-9_4","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"62-85","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Efficient Sensitivity Analysis for\u00a0Parametric Robust Markov Chains"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5235-1967","authenticated-orcid":false,"given":"Thom","family":"Badings","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4205-1167","authenticated-orcid":false,"given":"Ahmadreza","family":"Marandi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0819-9985","authenticated-orcid":false,"given":"Ufuk","family":"Topcu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1318-8973","authenticated-orcid":false,"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"4_CR1","unstructured":"Abbas, K., Berkhout, J., Heidergott, B.: A critical account of perturbation analysis of markov chains. arXiv preprint arXiv:1609.04138 (2016)"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Agarwal, C., Guha, S., Kret\u00ednsk\u00fd, J., Muruganandham, P.: PAC statistical model checking of mean payoff in discrete- and continuous-time MDP. In: CAV (2). Lecture Notes in Computer Science, vol. 13372, pp. 3\u201325. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_1","DOI":"10.1007\/978-3-031-13188-2_1"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-3-030-25540-4_29","volume-title":"Computer Aided Verification","author":"P Ashok","year":"2019","unstructured":"Ashok, P., K\u0159et\u00ednsk\u00fd, J., Weininger, M.: PAC statistical model checking for markov decision processes and stochastic games. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 497\u2013519. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_29"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Badings, T., Sim\u00e3o, T.D., Suilen, M., Jansen, N.: Decision-making under uncertainty: beyond probabilities. Int. J. Softw. Tools Technol. Transf. (2023)","DOI":"10.1007\/s10009-023-00704-3"},{"issue":"5","key":"4_CR5","doi-asserted-by":"publisher","first-page":"803","DOI":"10.1007\/s10009-022-00673-z","volume":"24","author":"TS Badings","year":"2022","unstructured":"Badings, T.S., Cubuktepe, M., Jansen, N., Junges, S., Katoen, J., Topcu, U.: Scenario-based verification of uncertain parametric MDPs. Int. J. Softw. Tools Technol. Transf. 24(5), 803\u2013819 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Badings, T.S., Junges, S., Marandi, A., Topcu, U., Jansen, N.: Efficient sensitivity analysis for parametric robust markov chains (extended version). Tech. rep., CoRR, abs\/2305.01473 (2023)","DOI":"10.1007\/978-3-031-37709-9_4"},{"key":"4_CR7","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2019.104504","volume":"272","author":"C Baier","year":"2020","unstructured":"Baier, C., Hensel, C., Hutschenreiter, L., Junges, S., Katoen, J., Klein, J.: Parametric markov chains: PCTL complexity and fraction-free gaussian elimination. Inf. Comput. 272, 104504 (2020)","journal-title":"Inf. Comput."},{"key":"4_CR8","unstructured":"Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)"},{"key":"4_CR9","unstructured":"Barratt, S.: On the differentiability of the solution to convex optimization problems. arXiv preprint arXiv:1804.05098 (2018)"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1016\/j.tcs.2018.06.016","volume":"747","author":"A Bart","year":"2018","unstructured":"Bart, A., Delahaye, B., Fournier, P., Lime, D., Monfroy, \u00c9., Truchet, C.: Reachability in parametric interval markov chains using constraints. Theor. Comput. Sci. 747, 48\u201374 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR11","unstructured":"Bazaraa, M.S., Jarvis, J.J., Sherali, H.D.: Linear programming and network flows. John Wiley & Sons (2011)"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Ben-Tal, A., Ghaoui, L.E., Nemirovski, A.: Robust Optimization, Princeton Series in Applied Mathematics, vol. 28. Princeton University Press (2009)","DOI":"10.1515\/9781400831050"},{"key":"4_CR13","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/j.ic.2016.01.004","volume":"247","author":"L Bortolussi","year":"2016","unstructured":"Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous-time markov chains. Inf. Comput. 247, 235\u2013253 (2016)","journal-title":"Inf. Comput."},{"key":"4_CR14","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780199535255.001.0001","volume-title":"Concentration Inequalities - A Nonasymptotic Theory of Independence","author":"S Boucheron","year":"2013","unstructured":"Boucheron, S., Lugosi, G., Massart, P.: Concentration Inequalities - A Nonasymptotic Theory of Independence. Oxford University Press, Oxford (2013)"},{"key":"4_CR15","volume-title":"Convex Optimization","author":"SP Boyd","year":"2014","unstructured":"Boyd, S.P., Vandenberghe, L.: Convex Optimization. Cambridge University Press, Cambridge (2014)"},{"key":"4_CR16","unstructured":"Buckman, J., Hafner, D., Tucker, G., Brevdo, E., Lee, H.: Sample-efficient reinforcement learning with stochastic ensemble value expansion. In: NeurIPS, pp. 8234\u20138244 (2018)"},{"issue":"1","key":"4_CR17","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/TR.2015.2452931","volume":"65","author":"R Calinescu","year":"2016","unstructured":"Calinescu, R., Ghezzi, C., Johnson, K., Pezz\u00e8, M., Rafiq, Y., Tamburrelli, G.: Formal verification with confidence intervals to establish quality of service properties of software systems. IEEE Trans. Reliab. 65(1), 107\u2013125 (2016)","journal-title":"IEEE Trans. Reliab."},{"issue":"10","key":"4_CR18","doi-asserted-by":"publisher","first-page":"1382","DOI":"10.1109\/9.633827","volume":"42","author":"X Cao","year":"1997","unstructured":"Cao, X., Chen, H.: Perturbation realization, potentials, and sensitivity analysis of markov processes. IEEE Trans. Autom. Control 42(10), 1382\u20131393 (1997)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"4","key":"4_CR19","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1109\/87.701341","volume":"6","author":"X Cao","year":"1998","unstructured":"Cao, X., Wan, Y.: Algorithms for sensitivity analysis of markov systems through potentials and perturbation realization. IEEE Trans. Control Syst. Technol. 6(4), 482\u2013494 (1998)","journal-title":"IEEE Trans. Control Syst. Technol."},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-662-44584-6_16","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"T Chen","year":"2014","unstructured":"Chen, T., Feng, Y., Rosenblum, D.S., Su, G.: Perturbation analysis in verification of discrete-time markov chains. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 218\u2013233. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44584-6_16"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-030-30806-3_7","volume-title":"Reachability Problems","author":"V Chonev","year":"2019","unstructured":"Chonev, V.: Reachability in augmented interval markov chains. In: Filiot, E., Jungers, R., Potapov, I. (eds.) RP 2019. LNCS, vol. 11674, pp. 79\u201392. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30806-3_7"},{"key":"4_CR22","unstructured":"Cooman, G.D., Hermans, F., Quaeghebeur, E.: Sensitivity analysis for finite markov chains in discrete time. In: UAI, pp. 129\u2013136. AUAI Press (2008)"},{"issue":"12","key":"4_CR23","doi-asserted-by":"publisher","first-page":"6333","DOI":"10.1109\/TAC.2021.3133265","volume":"67","author":"M Cubuktepe","year":"2022","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J., Topcu, U.: Convex optimization for parameter synthesis in MDPs. IEEE Trans. Autom. Control 67(12), 6333\u20136348 (2022)","journal-title":"IEEE Trans. Autom. Control"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-31862-0_21","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"C Daws","year":"2005","unstructured":"Daws, C.: Symbolic and Parametric Model Checking of Discrete-Time Markov Chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280\u2013294. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31862-0_21"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-21690-4_13","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2015","unstructured":"Dehnert, C., et al.: PROPhESY: a probabilistic parameter synthesis tool. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214\u2013231. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_13"},{"key":"4_CR26","unstructured":"Delahaye, B.: Consistency for parametric interval markov chains. In: SynCoP. OASIcs, vol. 44, pp. 17\u201332. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015)"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-662-49122-5_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Delahaye","year":"2016","unstructured":"Delahaye, B., Lime, D., Petrucci, L.: Parameter synthesis for parametric interval markov chains. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 372\u2013390. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_18"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Fang, X., Calinescu, R., Gerasimou, S., Alhwikem, F.: Fast parametric model checking through model fragmentation. In: ICSE, pp. 835\u2013846. IEEE (2021)","DOI":"10.1109\/ICSE43902.2021.00081"},{"issue":"1","key":"4_CR29","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1109\/TSE.2015.2421318","volume":"42","author":"A Filieri","year":"2016","unstructured":"Filieri, A., Tamburrelli, G., Ghezzi, C.: Supporting self-adaptation via quantitative verification and sensitivity analysis at run time. IEEE Trans. Softw. Eng. 42(1), 75\u201399 (2016)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"5","key":"4_CR30","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6377(94)90084-1","volume":"15","author":"MC Fu","year":"1994","unstructured":"Fu, M.C., Hu, J.: Smoothed perturbation analysis derivative estimation for markov chains. Oper. Res. Lett. 15(5), 241\u2013251 (1994)","journal-title":"Oper. Res. Lett."},{"key":"4_CR31","unstructured":"Gurobi Optimization, LLC: Gurobi optimizer reference manual (2023). https:\/\/www.gurobi.com"},{"issue":"1","key":"4_CR32","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric markov models. Int. J. Softw. Tools Technol. Transf. 13(1), 3\u201319 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-030-17462-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2019","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 344\u2013350. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20"},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-030-94583-1_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Heck","year":"2022","unstructured":"Heck, L., Spel, J., Junges, S., Moerman, J., Katoen, J.-P.: Gradient-descent for randomized controllers under partial observability. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 127\u2013150. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_7"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Softw. Tools Technol. Transf. (2021)","DOI":"10.1007\/s10009-021-00633-z"},{"key":"4_CR36","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-68279-0_3","volume-title":"50 Years of Integer Programming 1958-2008","author":"AJ Hoffman","year":"2010","unstructured":"Hoffman, A.J., Kruskal, J.B.: Integral boundary points of convex polyhedra. In: J\u00fcnger, M., Liebling, T.M., Naddef, D., Nemhauser, G.L., Pulleyblank, W.R., Reinelt, G., Rinaldi, G., Wolsey, L.A. (eds.) 50 Years of Integer Programming 1958-2008, pp. 49\u201376. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-540-68279-0_3"},{"key":"4_CR37","doi-asserted-by":"crossref","unstructured":"Hoffman, A.J., Kruskal, J.B.: Integral boundary points of convex polyhedra. 50 Years of integer programming 1958\u20132008, p. 49 (2010)","DOI":"10.1007\/978-3-540-68279-0_3"},{"key":"4_CR38","doi-asserted-by":"publisher","unstructured":"Jansen, N., Junges, S., Katoen, J.: Parameter synthesis in markov models: a gentle survey. In: Principles of Systems Design. Lecture Notes in Computer Science, vol. 13660, pp. 407\u2013437. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-22337-2_20","DOI":"10.1007\/978-3-031-22337-2_20"},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266\u2013277. IEEE Computer Society (1991)","DOI":"10.1109\/LICS.1991.151651"},{"key":"4_CR40","unstructured":"Junges, S., et al.: Parameter synthesis for markov models. CoRR abs\/1903.07993 (2019)"},{"key":"4_CR41","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.jcss.2021.02.006","volume":"119","author":"S Junges","year":"2021","unstructured":"Junges, S., Katoen, J., P\u00e9rez, G.A., Winkler, T.: The complexity of reachability in parametric markov decision processes. J. Comput. Syst. Sci. 119, 183\u2013210 (2021)","journal-title":"J. Comput. Syst. Sci."},{"key":"4_CR42","doi-asserted-by":"publisher","unstructured":"Junges, S., Spaan, M.T.J.: Abstraction-refinement for hierarchical probabilistic models. In: CAV (1). Lecture Notes in Computer Science, vol. 13371, pp. 102\u2013123. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_6","DOI":"10.1007\/978-3-031-13185-1_6"},{"key":"4_CR43","unstructured":"Kakade, S.M.: On the sample complexity of reinforcement learning. Ph.D. thesis, University of London, University College London (United Kingdom) (2003)"},{"key":"4_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"1","key":"4_CR45","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s00165-006-0015-2","volume":"19","author":"R Lanotte","year":"2007","unstructured":"Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Parametric probabilistic transition systems for system design and analysis. Formal Aspects Comput. 19(1), 93\u2013109 (2007)","journal-title":"Formal Aspects Comput."},{"key":"4_CR46","doi-asserted-by":"publisher","unstructured":"Matousek, J., G\u00e4rtner, B.: Integer Programming and LP Relaxation, pp. 29\u201340. Springer, Berlin Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-30717-4_3","DOI":"10.1007\/978-3-540-30717-4_3"},{"key":"4_CR47","unstructured":"Moerland, T.M., Broekens, J., Jonker, C.M.: Model-based reinforcement learning: a survey. CoRR abs\/2006.16712 (2020)"},{"issue":"1","key":"4_CR48","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1561\/2200000038","volume":"7","author":"R Munos","year":"2014","unstructured":"Munos, R.: From bandits to monte-carlo tree search: The optimistic principle applied to optimization and planning. Found. Trends Mach. Learn. 7(1), 1\u2013129 (2014)","journal-title":"Found. Trends Mach. Learn."},{"key":"4_CR49","doi-asserted-by":"crossref","unstructured":"Neary, C., Verginis, C.K., Cubuktepe, M., Topcu, U.: Verifiable and compositional reinforcement learning systems. In: ICAPS, pp. 615\u2013623. AAAI Press (2022)","DOI":"10.1609\/icaps.v32i1.19849"},{"key":"4_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-319-92612-4_7","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"L Petrucci","year":"2018","unstructured":"Petrucci, L., van de Pol, J.: Parameter synthesis algorithms for parametric interval markov chains. In: Baier, C., Caires, L. (eds.) FORTE 2018. LNCS, vol. 10854, pp. 121\u2013140. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-92612-4_7"},{"key":"4_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-319-66335-7_16","volume-title":"Quantitative Evaluation of Systems","author":"E Polgreen","year":"2017","unstructured":"Polgreen, E., Wijesuriya, V.B., Haesaert, S., Abate, A.: Automated experiment design for data-efficient verification of parametric markov decision processes. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 259\u2013274. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66335-7_16"},{"key":"4_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-642-39799-8_35","volume-title":"Computer Aided Verification","author":"A Puggelli","year":"2013","unstructured":"Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 527\u2013542. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_35"},{"key":"4_CR53","doi-asserted-by":"crossref","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley (1994)","DOI":"10.1002\/9780470316887"},{"key":"4_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/11691372_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Sen","year":"2006","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Model-checking markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 394\u2013410. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_26"},{"key":"4_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-030-72016-2_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Spel","year":"2021","unstructured":"Spel, J., Junges, S., Katoen, J.-P.: Finding provably optimal markov chains. In: TACAS 2021. LNCS, vol. 12651, pp. 173\u2013190. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_10"},{"issue":"7","key":"4_CR56","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1109\/TSE.2015.2508444","volume":"42","author":"G Su","year":"2016","unstructured":"Su, G., Feng, Y., Chen, T., Rosenblum, D.S.: Asymptotic perturbation bounds for probabilistic model checking with empirically determined probability parameters. IEEE Trans. Software Eng. 42(7), 623\u2013639 (2016)","journal-title":"IEEE Trans. Software Eng."},{"key":"4_CR57","unstructured":"Suilen, M., Sim\u00e3o, T.D., Parker, D., Jansen, N.: Robust anytime learning of markov decision processes. In: NeurIPS, vol. 35, pp. 28790\u201328802. Curran Associates, Inc. (2022)"},{"issue":"6","key":"4_CR58","doi-asserted-by":"publisher","first-page":"1358","DOI":"10.1287\/opre.2014.1314","volume":"62","author":"W Wiesemann","year":"2014","unstructured":"Wiesemann, W., Kuhn, D., Sim, M.: Distributionally robust convex optimization. Oper. Res. 62(6), 1358\u20131376 (2014)","journal-title":"Oper. Res."},{"key":"4_CR59","doi-asserted-by":"crossref","unstructured":"Wolff, E.M., Topcu, U., Murray, R.M.: Robust control of uncertain markov decision processes with temporal logic specifications. In: CDC, pp. 3372\u20133379. IEEE (2012)","DOI":"10.1109\/CDC.2012.6426174"},{"key":"4_CR60","doi-asserted-by":"crossref","unstructured":"Wolsey, L.A.: Integer programming. John Wiley & Sons (2020)","DOI":"10.1002\/9781119606475"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37709-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,24]],"date-time":"2024-10-24T06:56:47Z","timestamp":1729753007000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37709-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377082","9783031377099"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37709-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}