{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:53Z","timestamp":1784837813450,"version":"3.55.0"},"publisher-location":"Cham","reference-count":85,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031223365","type":"print"},{"value":"9783031223372","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-22337-2_20","type":"book-chapter","created":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T10:08:41Z","timestamp":1672222121000},"page":"407-437","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Parameter Synthesis in Markov Models: A Gentle Survey"],"prefix":"10.1007","author":[{"given":"Nils","family":"Jansen","sequence":"first","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"}]}],"member":"297","published-online":{"date-parts":[[2022,12,29]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m, E., Bartocci, E., Bonakdarpour, B., Dobe, O.: Parameter synthesis for probabilistic hyperproperties. In: LPAR. EPiC Series in Computing, vol. 73, pp. 12\u201331. EasyChair (2020)","DOI":"10.29007\/37lf"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-030-72016-2_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Andriushchenko","year":"2021","unstructured":"Andriushchenko, R., \u010ce\u0161ka, M., Junges, S., Katoen, J.-P.: Inductive synthesis for probabilistic programs reaches new horizons. In: Groote, J.F., Larsen, K.G. (eds.) TACAS 2021. LNCS, vol. 12651, pp. 191\u2013209. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_11"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-319-99154-2_4","volume-title":"Quantitative Evaluation of Systems","author":"S Arming","year":"2018","unstructured":"Arming, S., Bartocci, E., Chatterjee, K., Katoen, J.-P., Sokolova, A.: Parameter-independent strategies for pMDPs via POMDPs. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 53\u201370. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99154-2_4"},{"key":"20_CR4","doi-asserted-by":"publisher","first-page":"803","DOI":"10.1007\/s10009-022-00673-z","volume":"24","author":"T Badings","year":"2022","unstructured":"Badings, T., Cubuktepe, M., Jansen, N., et al.: Scenario-based verification of uncertain parametric MDPs. Int. J. Softw. Tools Technol. Transf. 24, 803\u2013819 (2022). https:\/\/doi.org\/10.1007\/s10009-022-00673-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"20_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: CAV (2022, to appear)","DOI":"10.1007\/978-3-031-13188-2_2"},{"key":"20_CR6","doi-asserted-by":"publisher","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 963\u2013999. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"20_CR7","doi-asserted-by":"crossref","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)","DOI":"10.1016\/j.ic.2019.104504"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-319-91908-9_21","volume-title":"Computing and Software Science","author":"C Baier","year":"2019","unstructured":"Baier, C., Hermanns, H., Katoen, J.-P.: The 10,000 facets of MDP model checking. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 420\u2013451. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_21"},{"key":"20_CR9","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"20_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, E., Truchet, C.: Reachability in parametric interval Markov chains using constraints. Theor. Comput. Sci. 747, 48\u201374 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-19835-9_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Bartocci","year":"2011","unstructured":"Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326\u2013340. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_30"},{"key":"20_CR12","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":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-319-89963-3_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Bortolussi","year":"2018","unstructured":"Bortolussi, L., Silvetti, S.: Bayesian statistical parameter synthesis for linear temporal properties of stochastic models. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 396\u2013413. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_23"},{"key":"20_CR14","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, Cambridge (2004)"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-39799-8_7","volume-title":"Computer Aided Verification","author":"L Brim","year":"2013","unstructured":"Brim, L., \u010ce\u0161ka, M., Dra\u017ean, S., \u0160afr\u00e1nek, D.: Exploring parameter space of stochastic biochemical systems using quantitative model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 107\u2013123. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_7"},{"key":"20_CR16","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/j.jss.2018.05.013","volume":"143","author":"R Calinescu","year":"2018","unstructured":"Calinescu, R., Ceska, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: Efficient synthesis of robust models for stochastic systems. J. Syst. Softw. 143, 140\u2013158 (2018)","journal-title":"J. Syst. Softw."},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Canny, J.F.: Some algebraic and geometric computations in PSPACE. In: STOC, pp. 460\u2013467. ACM (1988)","DOI":"10.1145\/62212.62257"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-319-12982-2_7","volume-title":"Computational Methods in Systems Biology","author":"M \u010ce\u0161ka","year":"2014","unstructured":"\u010ce\u0161ka, M., Dannenberg, F., Kwiatkowska, M., Paoletti, N.: Precise parameter synthesis for stochastic biochemical systems. In: Mendes, P., Dada, J.O., Smallbone, K. (eds.) CMSB 2014. LNCS, vol. 8859, pp. 86\u201398. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12982-2_7"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-030-30942-8_8","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"M \u010ce\u0161ka","year":"2019","unstructured":"\u010ce\u0161ka, M., Hensel, C., Junges, S., Katoen, J.-P.: Counterexample-driven synthesis for probabilistic program sketches. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 101\u2013120. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_8"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-030-17465-1_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M \u010ce\u0161ka","year":"2019","unstructured":"\u010ce\u0161ka, M., Jansen, N., Junges, S., Katoen, J.-P.: Shepherding hordes of Markov chains. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 172\u2013190. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_10"},{"key":"20_CR21","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1613\/jair.967","volume":"17","author":"H Chan","year":"2002","unstructured":"Chan, H., Darwiche, A.: When do numbers really matter? J. Artif. Intell. Res. 17, 265\u2013287 (2002)","journal-title":"J. Artif. Intell. Res."},{"issue":"1","key":"20_CR22","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/j.ic.2018.02.019","volume":"259","author":"G Chatzieleftheriou","year":"2018","unstructured":"Chatzieleftheriou, G., Katsaros, P.: Abstract model repair for probabilistic systems. Inf. Comput. 259(1), 142\u2013160 (2018)","journal-title":"Inf. Comput."},{"key":"20_CR23","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":"20_CR24","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 Computer Society (2013)","DOI":"10.1109\/TASE.2013.20"},{"issue":"3","key":"20_CR25","doi-asserted-by":"publisher","first-page":"1528","DOI":"10.1137\/120871390","volume":"23","author":"X Chen","year":"2013","unstructured":"Chen, X., Niu, L., Yuan, Y.: Optimality conditions and a smoothing trust region Newton method for non-Lipschitz optimization. SIAM J. Optimiz. 23(3), 1528\u20131552 (2013)","journal-title":"SIAM J. Optimiz."},{"key":"20_CR26","unstructured":"Chonev, V.: Reachability in augmented interval Markov chains. CoRR abs\/1701.02996 (2017)"},{"key":"20_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_15"},{"issue":"1","key":"20_CR28","first-page":"281","volume":"16","author":"D Cousineau","year":"2009","unstructured":"Cousineau, D.: Fitting the three-parameter Weibull distribution: review and evaluation of existing and new methods. IEEE DEIS 16(1), 281\u2013288 (2009)","journal-title":"IEEE DEIS"},{"key":"20_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-030-01090-4_10","volume-title":"Automated Technology for Verification and Analysis","author":"M Cubuktepe","year":"2018","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.-P., Topcu, U.: Synthesis in pMDPs: a tale of 1001 parameters. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 160\u2013176. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_10"},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Convex optimization for parameter synthesis in MDPs. IEEE Trans. Autom. Control (2022)","DOI":"10.1109\/TAC.2021.3133265"},{"key":"20_CR31","doi-asserted-by":"crossref","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Marandi, A., Suilen, M., Topcu, U.: Robust finite-state controllers for uncertain POMDPs. In: AAAI, pp. 11792\u201311800. AAAI Press (2021)","DOI":"10.1609\/aaai.v35i13.17401"},{"key":"20_CR32","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":"20_CR33","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":"20_CR34","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1016\/j.peva.2017.09.006","volume":"117","author":"J Esparza","year":"2017","unstructured":"Esparza, J., Hoffmann, P., Saha, R.: Polynomial analysis algorithms for free choice probabilistic workflow nets. Perform. Eval. 117, 104\u2013129 (2017)","journal-title":"Perform. Eval."},{"key":"20_CR35","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":"20_CR36","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."},{"key":"20_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-030-01090-4_18","volume-title":"Automated Technology for Verification and Analysis","author":"P Gainer","year":"2018","unstructured":"Gainer, P., Hahn, E.M., Schewe, S.: Accelerated model checking of parametric Markov chains. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 300\u2013316. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_18"},{"issue":"1\u20132","key":"20_CR38","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.M., Dean, T.L.: Bounded-parameter Markov decision processes. Artif. Intell. 122(1\u20132), 71\u2013109 (2000)","journal-title":"Artif. Intell."},{"key":"20_CR39","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1016\/j.peva.2018.11.006","volume":"130","author":"A Gouberman","year":"2019","unstructured":"Gouberman, A., Siegle, M., Tati, B.: Markov chains with perturbed rates to absorption: theory and application to model repair. Perform. Eval. 130, 32\u201350 (2019)","journal-title":"Perform. Eval."},{"issue":"1","key":"20_CR40","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":"20_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-030-31304-3_32","volume-title":"Computational Methods in Systems Biology","author":"M Hajnal","year":"2019","unstructured":"Hajnal, M., Nouvian, M., Petrov, T., \u0160afr\u00e1nek, D.: Data-informed parameter synthesis for population Markov chains. In: Bortolussi, L., Sanguinetti, G. (eds.) CMSB 2019. LNCS, vol. 11773, pp. 383\u2013386. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31304-3_32"},{"issue":"4","key":"20_CR42","doi-asserted-by":"publisher","first-page":"445","DOI":"10.3233\/FI-2013-952","volume":"128","author":"Y Han","year":"2013","unstructured":"Han, Y.: State elimination heuristics for short regular expressions. Fundam. Inform. 128(4), 445\u2013462 (2013)","journal-title":"Fundam. Inform."},{"key":"20_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-030-85172-9_3","volume-title":"Quantitative Evaluation of Systems","author":"A Hartmanns","year":"2021","unstructured":"Hartmanns, A., Katoen, J.-P., Kohlen, B., Spel, J.: Tweaking the odds in probabilistic timed automata. In: Abate, A., Marin, A. (eds.) QEST 2021. LNCS, vol. 12846, pp. 39\u201358. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85172-9_3"},{"issue":"1","key":"20_CR44","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1109\/JPROC.2009.2032356","volume":"98","author":"M Haselman","year":"2010","unstructured":"Haselman, M., Hauck, S.: The future of integrated circuits: a survey of nanoelectronics. Proc. IEEE 98(1), 11\u201338 (2010)","journal-title":"Proc. IEEE"},{"issue":"2","key":"20_CR45","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/0020-0190(90)90107-9","volume":"35","author":"T Herman","year":"1990","unstructured":"Herman, T.: Probabilistic self-stabilization. Inf. Process. Lett. 35(2), 63\u201367 (1990)","journal-title":"Inf. Process. Lett."},{"key":"20_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1007\/978-3-030-81688-9_27","volume-title":"Computer Aided Verification","author":"S Holtzen","year":"2021","unstructured":"Holtzen, S., Junges, S., Vazquez-Chanlatte, M., Millstein, T., Seshia, S.A., Van den Broeck, G.: Model checking finite-horizon Markov chains with probabilistic inference. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 577\u2013601. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_27"},{"key":"20_CR47","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley (2003)"},{"key":"20_CR48","doi-asserted-by":"crossref","unstructured":"Hutschenreiter, L., Baier, C., Klein, J.: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. In: GandALF. EPTCS, vol. 256, pp. 16\u201330 (2017)","DOI":"10.4204\/EPTCS.256.2"},{"key":"20_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-319-10696-0_31","volume-title":"Quantitative Evaluation of Systems","author":"N Jansen","year":"2014","unstructured":"Jansen, N., et al.: Accelerating parametric probabilistic verification. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 404\u2013420. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10696-0_31"},{"key":"20_CR50","unstructured":"Junges, S.: Parameter synthesis in Markov models. Dissertation, RWTH Aachen University (2020)"},{"key":"20_CR51","unstructured":"Junges, S., et al.: Parameter synthesis for Markov models. CoRR abs\/1903.07993 (2019)"},{"key":"20_CR52","unstructured":"Junges, S., et al.: Finite-state controllers of POMDPs using parameter synthesis. In: UAI, pp. 519\u2013529. AUAI Press (2018)"},{"key":"20_CR53","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., 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":"20_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-031-13185-1_6","volume-title":"Computer Aided Verification 2022","author":"S Junges","year":"2022","unstructured":"Junges, S., Spaan, M.T.J.: Abstraction-refinement for hierarchical probabilistic models. In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13371, pp. 102\u2013123. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_6"},{"key":"20_CR55","doi-asserted-by":"crossref","unstructured":"Katoen, J.P.: The probabilistic model checking landscape. In: LICS, pp. 31\u201345. ACM (2016)","DOI":"10.1145\/2933575.2934574"},{"key":"20_CR56","unstructured":"Knuth, D., Yao, A.: The complexity of nonuniform random number generation (chap). In: Algorithms and Complexity: New Directions and Recent Results. Academic Press (1976)"},{"key":"20_CR57","doi-asserted-by":"crossref","unstructured":"Kochenderfer, M.J.: Decision Making Under Uncertainty: Theory and Application. MIT Press, Cambridge (2015)","DOI":"10.7551\/mitpress\/10187.001.0001"},{"issue":"2","key":"20_CR58","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1023\/A:1014745904458","volume":"8","author":"I Kozine","year":"2002","unstructured":"Kozine, I., Utkin, L.V.: Interval-valued finite Markov chains. Reliab. Comput. 8(2), 97\u2013113 (2002)","journal-title":"Reliab. Comput."},{"key":"20_CR59","unstructured":"Krak, T.E., T\u2019Joens, N., Bock, J.D.: Hitting times and probabilities for imprecise Markov chains. In: ISIPTA. PMLR, vol. 103, pp. 265\u2013275. PMLR (2019)"},{"key":"20_CR60","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\u20132","key":"20_CR61","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0004-3702(02)00378-8","volume":"147","author":"O Madani","year":"2003","unstructured":"Madani, O., Hanks, S., Condon, A.: On the undecidability of probabilistic planning and related stochastic optimization problems. Artif. Intell. 147(1\u20132), 5\u201334 (2003)","journal-title":"Artif. Intell."},{"key":"20_CR62","unstructured":"Mao, Y., Szmuk, M., Xu, X., Acikmese, B.: Successive Convexification: A Superlinearly Convergent Algorithm for Non-convex Optimal Control Problems. arXiv preprint arXiv:1804.06539 (2018)"},{"issue":"5","key":"20_CR63","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."},{"key":"20_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-319-17524-9_21","volume-title":"NASA Formal Methods","author":"S Pathak","year":"2015","unstructured":"Pathak, S., \u00c1brah\u00e1m, E., Jansen, N., Tacchella, A., Katoen, J.-P.: A greedy approach for the efficient repair of stochastic models. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 295\u2013309. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_21"},{"key":"20_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-030-85037-1_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A Peruffo","year":"2021","unstructured":"Peruffo, A., Abate, A.: Formal abstraction and synthesis of parametric stochastic processes. In: Dima, C., Shirmohammadi, M. (eds.) FORMATS 2021. LNCS, vol. 12860, pp. 135\u2013153. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85037-1_9"},{"key":"20_CR66","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":"20_CR67","unstructured":"Poupart, P., Boutilier, C.: Bounded finite state controllers. In: NIPS, pp. 823\u2013830. MIT Press (2003)"},{"key":"20_CR68","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":"20_CR69","doi-asserted-by":"crossref","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley (1994)","DOI":"10.1002\/9780470316887"},{"key":"20_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-46520-3_4","volume-title":"Automated Technology for Verification and Analysis","author":"T Quatmann","year":"2016","unstructured":"Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.-P.: Parameter synthesis for Markov models: faster than ever. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 50\u201367. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_4"},{"key":"20_CR71","unstructured":"Russell, S.J., Norvig, P.: Artificial Intelligence - A Modern Approach (3. internat. edn.). Pearson Education (2010)"},{"key":"20_CR72","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-030-86772-0_20","volume-title":"Symbolic and Quantitative Approaches to Reasoning with Uncertainty","author":"B Salmani","year":"2021","unstructured":"Salmani, B., Katoen, J.-P.: Fine-tuning the odds in Bayesian networks. In: Vejnarov\u00e1, J., Wilson, N. (eds.) ECSQARU 2021. LNCS (LNAI), vol. 12897, pp. 268\u2013283. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86772-0_20"},{"key":"20_CR73","doi-asserted-by":"crossref","unstructured":"Salmani, B., Katoen, J.P.: Automatically finding the right probabilities in Bayesian networks. arXiv preprint (2022, to appear)","DOI":"10.1613\/jair.1.14044"},{"issue":"8","key":"20_CR74","doi-asserted-by":"publisher","first-page":"1314","DOI":"10.1016\/j.ijar.2009.06.007","volume":"50","author":"D Skulj","year":"2009","unstructured":"Skulj, D.: Discrete time Markov chains with interval probabilities. Int. J. Approx. Reason. 50(8), 1314\u20131329 (2009)","journal-title":"Int. J. Approx. Reason."},{"key":"20_CR75","doi-asserted-by":"publisher","unstructured":"Spaan, M.T.J.: Partially observable Markov decision processes. In: Wiering, M., van Otterlo, M. (eds.) Reinforcement Learning. ALO, vol. 12, pp. 387\u2013414. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27645-3_12","DOI":"10.1007\/978-3-642-27645-3_12"},{"key":"20_CR76","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":"20_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-030-31784-3_28","volume-title":"Automated Technology for Verification and Analysis","author":"J Spel","year":"2019","unstructured":"Spel, J., Junges, S., Katoen, J.-P.: Are parametric Markov chains monotonic? In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 479\u2013496. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_28"},{"key":"20_CR78","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"},{"key":"20_CR79","doi-asserted-by":"crossref","unstructured":"Suilen, M., Jansen, N., Cubuktepe, M., Topcu, U.: Robust policy synthesis for uncertain POMDPs via convex optimization. In: IJCAI, pp. 4113\u20134120 (2020). ijcai.org","DOI":"10.24963\/ijcai.2020\/569"},{"key":"20_CR80","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327\u2013338. IEEE Computer Society (1985)","DOI":"10.1109\/SFCS.1985.12"},{"key":"20_CR81","doi-asserted-by":"crossref","unstructured":"Vlassis, N., Littman, M.L., Barber, D.: On the computational complexity of stochastic controller optimization in POMDPs. ACM Trans. Comput. Theory 4(4), 12:1\u201312:8 (2012)","DOI":"10.1145\/2382559.2382563"},{"issue":"1","key":"20_CR82","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s00446-021-00408-4","volume":"35","author":"M Volk","year":"2022","unstructured":"Volk, M., Bonakdarpour, B., Katoen, J.P., Aflaki, S.: Synthesizing optimal bias in randomized self-stabilization. Distrib. Comput. 35(1), 37\u201357 (2022)","journal-title":"Distrib. Comput."},{"issue":"1","key":"20_CR83","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":"20_CR84","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"},{"issue":"1","key":"20_CR85","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10107-015-0893-2","volume":"151","author":"Y Yuan","year":"2015","unstructured":"Yuan, Y.: Recent advances in trust region algorithms. Math. Program. 151(1), 249\u2013281 (2015). https:\/\/doi.org\/10.1007\/s10107-015-0893-2","journal-title":"Math. Program."}],"container-title":["Lecture Notes in Computer Science","Principles of Systems Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22337-2_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,11]],"date-time":"2024-10-11T02:55:33Z","timestamp":1728615333000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22337-2_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223365","9783031223372"],"references-count":85,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22337-2_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}