{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,2]],"date-time":"2026-08-02T15:35:49Z","timestamp":1785684949433,"version":"3.56.0"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2022,9,14]],"date-time":"2022-09-14T00:00:00Z","timestamp":1663113600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,9,14]],"date-time":"2022-09-14T00:00:00Z","timestamp":1663113600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2022,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We consider parametric Markov decision processes (pMDPs) that are augmented with unknown probability distributions over parameter values. The problem is to compute the probability to satisfy a temporal logic specification with any concrete MDP that corresponds to a sample from these distributions. As solving this problem precisely is infeasible, we resort to sampling techniques that exploit the so-called scenario approach. Based on a finite number of samples of the parameters, the proposed method yields high-confidence bounds on the probability of satisfying the specification. The number of samples required to obtain a high confidence on these bounds is independent of the number of states and the number of random parameters. Experiments on a large set of benchmarks show that several thousand samples suffice to obtain tight and high-confidence lower and upper bounds on the satisfaction probability.\n<\/jats:p>","DOI":"10.1007\/s10009-022-00673-z","type":"journal-article","created":{"date-parts":[[2022,9,14]],"date-time":"2022-09-14T13:04:40Z","timestamp":1663160680000},"page":"803-819","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Scenario-based verification of uncertain parametric MDPs"],"prefix":"10.1007","volume":"24","author":[{"given":"Thom","family":"Badings","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Murat","family":"Cubuktepe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ufuk","family":"Topcu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,9,14]]},"reference":[{"key":"673_CR1","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1613\/jair.5242","volume":"59","author":"A Ahmed","year":"2017","unstructured":"Ahmed, A., Varakantham, P., Lowalekar, M., Adulyasak, Y., Jaillet, P.: Sampling based approaches for minimizing regret in uncertain Markov decision processes (MDPs). J. Artif. Intell. Res. 59, 229\u2013264 (2017)","journal-title":"J. Artif. Intell. Res."},{"key":"673_CR2","doi-asserted-by":"crossref","unstructured":"Arming, S., Bartocci, E., Chatterjee, K., Katoen, J.P., Sokolova, A.: Parameter-Independent Strategies for pMDPs via POMDPs. In: QEST, pp. 53\u201370. Springer (2018)","DOI":"10.1007\/978-3-319-99154-2_4"},{"issue":"1","key":"673_CR3","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/0196-6774(90)90021-6","volume":"15","author":"J Aspnes","year":"1990","unstructured":"Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. J. Algorithms 15(1), 441\u2013460 (1990)","journal-title":"J. Algorithms"},{"key":"673_CR4","doi-asserted-by":"crossref","unstructured":"Bacci, G., Hansen, M., Larsen, K.G.: Model Checking Constrained Markov Reward Models with Uncertainties. In: QEST, pp. 37\u201351 (2019)","DOI":"10.1007\/978-3-030-30281-8_3"},{"key":"673_CR5","doi-asserted-by":"crossref","unstructured":"Badings, T.S., Jansen, N., Junges, S., Stoelinga, M., Volk, M.: Sampling-based verification of ctmcs with uncertain rates. In: International Conference on Computer Aided Verification (to appear). Springer (2022)","DOI":"10.1007\/978-3-031-13188-2_2"},{"key":"673_CR6","doi-asserted-by":"publisher","first-page":"104504","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.P., Klein, J.: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. Inf. Comput. 272, 104504 (2020)","journal-title":"Inf. Comput."},{"key":"673_CR7","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, London (2008)"},{"key":"673_CR8","volume-title":"Algorithms in Real Algebraic Geometry","author":"S Basu","year":"2010","unstructured":"Basu, S., Pollack, R., Roy, M.: Algorithms in Real Algebraic Geometry. Springer, Berlin (2010)"},{"key":"673_CR9","volume-title":"Introduction to Probability","author":"DP Bertsekas","year":"2000","unstructured":"Bertsekas, D.P., Tsitsiklis, J.N.: Introduction to Probability. Athena Scientinis, London (2000)"},{"key":"673_CR10","doi-asserted-by":"crossref","unstructured":"Bortolussi, L., Silvetti, S.: Bayesian statistical parameter synthesis for linear temporal properties of stochastic models. In: TACAS (2), Lecture Notes in Computer Science, vol. 10806, pp. 396\u2013413. Springer (2018)","DOI":"10.1007\/978-3-319-89963-3_23"},{"key":"673_CR11","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804441","volume-title":"Convex Optimization","author":"S Boyd","year":"2004","unstructured":"Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, New York (2004)"},{"issue":"5","key":"673_CR12","doi-asserted-by":"publisher","first-page":"742","DOI":"10.1109\/TAC.2006.875041","volume":"51","author":"GC Calafiore","year":"2006","unstructured":"Calafiore, G.C., Campi, M.C.: The scenario approach to robust control design. IEEE Trans. Autom. Contr. 51(5), 742\u2013753 (2006)","journal-title":"IEEE Trans. Autom. Contr."},{"issue":"3","key":"673_CR13","doi-asserted-by":"publisher","first-page":"1211","DOI":"10.1137\/07069821X","volume":"19","author":"MC Campi","year":"2008","unstructured":"Campi, M.C., Garatti, S.: The exact feasibility of randomized solutions of uncertain convex programs. SIAM J. Optim. 19(3), 1211\u20131230 (2008)","journal-title":"SIAM J. Optim."},{"issue":"3","key":"673_CR14","doi-asserted-by":"publisher","first-page":"1211","DOI":"10.1137\/07069821X","volume":"19","author":"MC Campi","year":"2008","unstructured":"Campi, M.C., Garatti, S.: The exact feasibility of randomized solutions of uncertain convex programs. SIAM J. Optim. 19(3), 1211\u20131230 (2008)","journal-title":"SIAM J. Optim."},{"issue":"2","key":"673_CR15","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/s10957-010-9754-6","volume":"148","author":"MC Campi","year":"2011","unstructured":"Campi, M.C., Garatti, S.: A sampling-and-discarding approach to chance-constrained optimization: feasibility and optimality. J. Optim. Theory Appl. 148(2), 257\u2013280 (2011)","journal-title":"J. Optim. Theory Appl."},{"key":"673_CR16","first-page":"996","volume":"2","author":"MC Campi","year":"2018","unstructured":"Campi, M.C., Garatti, S.: Introduction to the scenario approach. SIAM 2, 996 (2018)","journal-title":"SIAM"},{"key":"673_CR17","unstructured":"Cassandra, A., Littman, M.L., Zhang, N.L.: Incremental Pruning: A Simple, Fast, Exact Method for Partially Observable Markov Decision Processes. In: UAI, pp. 54\u201361 (1997)"},{"key":"673_CR18","doi-asserted-by":"crossref","unstructured":"Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M., Qu, H., Zhang, L.: Model Repair for Markov Decision Processes. In: TASE, pp. 85\u201392. IEEE CS (2013)","DOI":"10.1109\/TASE.2013.20"},{"key":"673_CR19","doi-asserted-by":"crossref","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J., Topcu, U.: Scenario-based verification of uncertain mdps. In: TACAS (1), Lecture Notes in Computer Science, vol. 12078, pp. 287\u2013305. Springer (2020)","DOI":"10.1007\/978-3-030-45190-5_16"},{"key":"673_CR20","doi-asserted-by":"crossref","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Papusha, I., Poonawala, H.A., Topcu, U.: Sequential Convex Programming for the Efficient Verification of Parametric MDPs. In: TACAS (2), LNCS, vol. 10206, pp. 133\u2013150 (2017)","DOI":"10.1007\/978-3-662-54580-5_8"},{"key":"673_CR21","doi-asserted-by":"crossref","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Synthesis in pMDPs: A tale of 1001 parameters. In: ATVA, LNCS, vol. 11138, pp. 160\u2013176. Springer (2018)","DOI":"10.1007\/978-3-030-01090-4_10"},{"key":"673_CR22","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: PAPM-PROBMIV, LNCS, vol. 2165, pp. 39\u201356. Springer (2001)","DOI":"10.1007\/3-540-44804-7_3"},{"key":"673_CR23","doi-asserted-by":"crossref","unstructured":"Daws, C.: Symbolic and Parametric Model Checking of Discrete-Time Markov chains. In: ICTAC, LNCS, vol. 3407, pp. 280\u2013294. Springer (2004)","DOI":"10.1007\/978-3-540-31862-0_21"},{"key":"673_CR24","doi-asserted-by":"crossref","unstructured":"Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J., \u00c1brah\u00e1m, E.: PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. In: CAV (1), LNCS, vol. 9206, pp. 214\u2013231. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_13"},{"key":"673_CR25","doi-asserted-by":"crossref","unstructured":"Dehnert, C., Junges, S., Katoen, J., Volk, M.: A Storm is Coming: A Modern Probabilistic Model Checker. In: CAV (2), LNCS, vol. 10427, pp. 592\u2013600. Springer (2017)","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"673_CR26","doi-asserted-by":"crossref","unstructured":"Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wasowski, A.: Decision problems for interval Markov chains. In: LATA, LNCS, vol. 6638, pp. 274\u2013285. Springer (2011)","DOI":"10.1007\/978-3-642-21254-3_21"},{"key":"673_CR27","doi-asserted-by":"crossref","unstructured":"Gainer, P., Hahn, E.M., Schewe, S.: Incremental verification of parametric and reconfigurable Markov chains. In: QEST, LNCS, vol. 11024, pp. 140\u2013156. Springer (2018)","DOI":"10.1007\/978-3-319-99154-2_9"},{"issue":"7","key":"673_CR28","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1016\/j.ifacol.2021.08.427","volume":"54","author":"S Garatti","year":"2021","unstructured":"Garatti, S., Campi, M.C.: The risk of making decisions from data through the lens of the scenario approach. IFAC-PapersOnLine 54(7), 607\u2013612 (2021)","journal-title":"IFAC-PapersOnLine"},{"issue":"1\u20132","key":"673_CR29","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0004-3702(00)00047-3","volume":"122","author":"R Givan","year":"2000","unstructured":"Givan, R., Leach, S., Dean, T.: Bounded-parameter Markov decision processes. Artif. Intell. 122(1\u20132), 71\u2013109 (2000)","journal-title":"Artif. Intell."},{"issue":"1","key":"673_CR30","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT 13(1), 3\u201319 (2010)","journal-title":"STTT"},{"key":"673_CR31","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1109\/TNANO.2002.807393","volume":"1","author":"J Han","year":"2002","unstructured":"Han, J., Jonker, P.: A system architecture solution for unreliable nanoelectronic devices. IEEE Trans. Nanotechnol. 1, 201\u2013208 (2002)","journal-title":"IEEE Trans. Nanotechnol."},{"key":"673_CR32","first-page":"88890","volume":"53","author":"H Hatefi","year":"2012","unstructured":"Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. ECEASST 53, 88890 (2012)","journal-title":"ECEASST"},{"key":"673_CR33","unstructured":"Haussler, D.: Probably approximately correct learning. In: AAAI, pp. 1101\u20131108. AAAI Press (1990)"},{"key":"673_CR34","doi-asserted-by":"crossref","unstructured":"Helmink, L., Sellink, M., Vaandrager, F.: Proof-Checking a Data Link Protocol. In: TYPES, LNCS, vol. 806, pp. 127\u2013165. Springer (1994)","DOI":"10.1007\/3-540-58085-9_75"},{"key":"673_CR35","unstructured":"Ho, C.P., Petrik, M.: Fast Bellman Updates for Robust MDPs. In: ICML (2018)"},{"key":"673_CR36","unstructured":"Junges, S., \u00c1brah\u00e1m, E., Hensel, C., Jansen, N., Katoen, J., Quatmann, T., Volk, M.: Parameter Synthesis for Markov Models. CoRR arXiv:1903.07993 (2019)"},{"key":"673_CR37","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: CAV, LNCS, vol. 6806, pp. 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"673_CR38","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: The PRISM Benchmark Suite. In: QEST, pp. 203\u2013204. IEEE CS (2012)","DOI":"10.1109\/QEST.2012.14"},{"key":"673_CR39","doi-asserted-by":"crossref","unstructured":"Llerena, Y.R.S., B\u00f6hme, M., Br\u00fcnink, M., Su, G., Rosenblum, D.S.: Verifying the Long-run Behavior of Probabilistic System Models in the Presence of Uncertainty. In: ESEC\/SIGSOFT FSE, pp. 587\u2013597. ACM (2018)","DOI":"10.1145\/3236024.3236078"},{"key":"673_CR40","doi-asserted-by":"crossref","unstructured":"McAllister, R., Peynot, T., Fitch, R., Sukkarieh, S.: Motion Planning and Stochastic Control with Experimental Validation on a Planetary Rover. In: IROS, pp. 4716\u20134723. IEEE (2012)","DOI":"10.1109\/IROS.2012.6386229"},{"issue":"4","key":"673_CR41","doi-asserted-by":"publisher","first-page":"1395","DOI":"10.1007\/s10270-012-0277-5","volume":"13","author":"I Meedeniya","year":"2014","unstructured":"Meedeniya, I., Moser, I., Aleti, A., Grunske, L.: Evaluating probabilistic models with uncertain model parameters. Softw. Syst. Model. 13(4), 1395\u20131415 (2014)","journal-title":"Softw. Syst. Model."},{"issue":"5","key":"673_CR42","doi-asserted-by":"publisher","first-page":"780","DOI":"10.1287\/opre.1050.0216","volume":"53","author":"A Nilim","year":"2005","unstructured":"Nilim, A., El Ghaoui, L.: Robust control of Markov decision processes with uncertain transition matrices. Oper. Res. 53(5), 780\u2013798 (2005)","journal-title":"Oper. Res."},{"issue":"1","key":"673_CR43","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1109\/TEC.2007.914174","volume":"23","author":"G Papaefthymiou","year":"2008","unstructured":"Papaefthymiou, G., Kl\u00f6ckl, B.: MCMC for wind power simulation. IEEE Trans. Energy Convers. 23(1), 234\u2013240 (2008)","journal-title":"IEEE Trans. Energy Convers."},{"key":"673_CR44","unstructured":"Pineau, J., Gordon, G., Thrun, S.: Point-Based Value Iteration: an Anytime Algorithm for POMDPs. In: IJCAI, pp. 1025\u20131030 (2003)"},{"key":"673_CR45","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The Temporal Logic of Programs. In: FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"673_CR46","doi-asserted-by":"crossref","unstructured":"Polgreen, E., Wijesuriya, V.B., Haesaert, S., Abate, A.: Data-efficient bayesian verification of parametric markov chains. In: QEST, Lecture Notes in Computer Science, vol. 9826, pp. 35\u201351. Springer (2016)","DOI":"10.1007\/978-3-319-43425-4_3"},{"key":"673_CR47","doi-asserted-by":"crossref","unstructured":"Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. In: CAV, pp. 527\u2013542. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_35"},{"key":"673_CR48","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"2014","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, London (2014)"},{"key":"673_CR49","doi-asserted-by":"crossref","unstructured":"Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.P.: Parameter Synthesis for Markov Models: Faster Than Ever. In: ATVA, LNCS, vol. 9938, pp. 50\u201367 (2016)","DOI":"10.1007\/978-3-319-46520-3_4"},{"key":"673_CR50","volume-title":"Artificial Intelligence: A Modern Approach","author":"SJ Russell","year":"2020","unstructured":"Russell, S.J., Norvig, P.: Artificial Intelligence: A Modern Approach, 4th edn. Pearson, New York (2020)","edition":"4"},{"key":"673_CR51","doi-asserted-by":"crossref","unstructured":"Scheftelowitsch, D., Buchholz, P., Hashemi, V., Hermanns, H.: Multi-Objective Approaches to Markov Decision Processes with Uncertain Transition Parameters. In: VALUETOOLS, pp. 44\u201351 (2017)","DOI":"10.1145\/3150928.3150945"},{"key":"673_CR52","doi-asserted-by":"crossref","unstructured":"Shmatikov, V.: Probabilistic analysis of an anonymity system. J. Comput. Secur. 12(3\u20134), 355\u2013377 (2004)","DOI":"10.3233\/JCS-2004-123-403"},{"key":"673_CR53","unstructured":"Steimle, L.N., Kaufman, D.L., Denton, B.T.: Multi-Model Markov Decision Processes. Optimization Online (2018)"},{"key":"673_CR54","volume-title":"Reinforcement Learning: An Introduction","author":"RS Sutton","year":"2018","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. MIT Press, London (2018)"},{"issue":"1","key":"673_CR55","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1287\/moor.1120.0566","volume":"38","author":"W Wiesemann","year":"2013","unstructured":"Wiesemann, W., Kuhn, D., Rustem, B.: Robust Markov decision processes. Math. Oper. Res. 38(1), 153\u2013183 (2013)","journal-title":"Math. Oper. Res."},{"key":"673_CR56","unstructured":"Winkler, T., Junges, S., P\u00e9rez, G.A., Katoen, J.P.: On the complexity of reachability in parametric Markov decision processes. In: CONCUR, LIPIcs, vol. 140, pp. 14:1\u201314:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"673_CR57","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"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00673-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-022-00673-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00673-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,16]],"date-time":"2022-11-16T10:11:44Z","timestamp":1668593504000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-022-00673-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,14]]},"references-count":57,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2022,10]]}},"alternative-id":["673"],"URL":"https:\/\/doi.org\/10.1007\/s10009-022-00673-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,9,14]]},"assertion":[{"value":"29 August 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 September 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}