{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:58Z","timestamp":1784837818542,"version":"3.55.0"},"reference-count":143,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2024,2,17]],"date-time":"2024-02-17T00:00:00Z","timestamp":1708128000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,2,17]],"date-time":"2024-02-17T00:00:00Z","timestamp":1708128000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100006254","name":"Ruhr-Universit\u00e4t Bochum","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100006254","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2024,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Markov chain analysis is a key technique in formal verification. A practical obstacle is that all probabilities in Markov models need to be known. However, system quantities such as failure rates or packet loss ratios, etc. are often not\u2014or only partially\u2014known. This motivates considering parametric models with transitions labeled with functions over parameters. Whereas traditional Markov chain analysis relies on a single, fixed set of probabilities, analysing parametric Markov models focuses on synthesising parameter values that establish a given safety or performance specification <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\varphi $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c6<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. Examples are: what component failure rates ensure the probability of a system breakdown to be below 0.00000001?, or which failure rates maximise the performance, for instance the throughput, of the system? This paper presents various analysis algorithms for parametric discrete-time Markov chains and Markov decision processes. We focus on three problems: (a) do all parameter values within a given region satisfy <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\varphi $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c6<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>?, (b) which regions satisfy <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\varphi $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c6<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and which ones do not?, and (c) an approximate version of (b) focusing on covering a large fraction of all possible parameter values. We give a detailed account of the various algorithms, present a software tool realising these techniques, and report on an extensive experimental evaluation on benchmarks that span a wide range of applications.<\/jats:p>","DOI":"10.1007\/s10703-023-00442-x","type":"journal-article","created":{"date-parts":[[2024,2,17]],"date-time":"2024-02-17T12:02:13Z","timestamp":1708171333000},"page":"181-259","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Parameter synthesis for Markov models: covering the parameter space"],"prefix":"10.1007","volume":"62","author":[{"given":"Sebastian","family":"Junges","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Erika","family":"\u00c1brah\u00e1m","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christian","family":"Hensel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1318-8973","authenticated-orcid":false,"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tim","family":"Quatmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthias","family":"Volk","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,2,17]]},"reference":[{"key":"442_CR1","unstructured":"(1999) IEEE wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) specification"},{"key":"442_CR2","unstructured":"Abbott J, Bigatti AM (2022) CoCoALib: a c++ library for doing computations in commutative algebra. http:\/\/cocoa.dima.unige.it\/cocoalib"},{"key":"442_CR3","doi-asserted-by":"crossref","unstructured":"Aflaki S, Volk M, Bonakdarpour B, Katoen JP, Storjohann A (2017) Automated fine tuning of probabilistic self-stabilizing algorithms. In: SRDS. IEEE Computer Society, pp 94\u2013103","DOI":"10.1109\/SRDS.2017.22"},{"key":"442_CR4","doi-asserted-by":"crossref","unstructured":"Amparore EG, Beccuti M, Donatelli S (2014) (Stochastic) model checking in GreatSPN. In: Petri Nets, LNCS, vol 8489. Springer, Berlin, pp 354\u2013363","DOI":"10.1007\/978-3-319-07734-5_19"},{"key":"442_CR5","doi-asserted-by":"crossref","unstructured":"Andova S, Hermanns H, Katoen JP (2003) Discrete-time rewards model-checked. In: FORMATS, LNCS, vol 2791. Springer, Berlin, pp 88\u2013104","DOI":"10.1007\/978-3-540-40903-8_8"},{"key":"442_CR6","doi-asserted-by":"crossref","unstructured":"Andr\u00e9 \u00c9, Delahaye B (2016) Consistency in parametric interval probabilistic timed automata. In: TIME. IEEE Computer Society, pp 110\u2013119","DOI":"10.1109\/TIME.2016.19"},{"key":"442_CR7","doi-asserted-by":"crossref","unstructured":"Angluin D (1980) Local and global properties in networks of processors (extended abstract). In: STOC. ACM, pp 82\u201393","DOI":"10.1145\/800141.804655"},{"key":"442_CR8","doi-asserted-by":"crossref","unstructured":"Arming S, Bartocci E, Sokolova A (2017) SEA-PARAM: exploring schedulers in parametric MDPs. In: QAPL@ETAPS, EPTCS, vol 250, pp 25\u201338","DOI":"10.4204\/EPTCS.250.3"},{"key":"442_CR9","doi-asserted-by":"crossref","unstructured":"Arming S, Bartocci E, Chatterjee K, Katoen JP, Sokolova A (2018) Parameter-independent strategies for pMDPs via POMDPs. In: QEST, LNCS, vol 11024. Springer, Berlin, pp 53\u201370","DOI":"10.1007\/978-3-319-99154-2_4"},{"key":"442_CR10","doi-asserted-by":"crossref","unstructured":"Bacci G, Delahaye B, Larsen KG, Mariegaard A (2021) Quantitative analysis of interval Markov chains. In: Model checking, synthesis, and learning, LNCS, vol 13030. Springer, Berlin, pp 57\u201377","DOI":"10.1007\/978-3-030-91384-7_4"},{"issue":"5","key":"442_CR11","doi-asserted-by":"crossref","first-page":"803","DOI":"10.1007\/s10009-022-00673-z","volume":"24","author":"TS Badings","year":"2022","unstructured":"Badings TS, Cubuktepe M, Jansen N, Junges S, Katoen J, Topcu U (2022) Scenario-based verification of uncertain parametric MDPs. Int J Softw Tools Technol Transf 24(5):803\u2013819","journal-title":"Int J Softw Tools Technol Transf"},{"key":"442_CR12","doi-asserted-by":"crossref","unstructured":"Badings TS, Jansen N, Junges S, Stoelinga M, Volk M (2022) Sampling-based verification of CTMCs with uncertain rates. In: CAV (2), LNCS, vol 13372. Springer, Berlin, pp 26\u201347","DOI":"10.1007\/978-3-031-13188-2_2"},{"key":"442_CR13","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen JP (2008) Principles of model checking. MIT Press, Cambridge"},{"key":"442_CR14","doi-asserted-by":"crossref","unstructured":"Baier C, Clarke EM, Hartonas-Garmhausen V, Kwiatkowska MZ, Ryan M (1997) Symbolic model checking for probabilistic processes. In: ICALP, LNCS, vol 1256. Springer, Berlin, pp 430\u2013440","DOI":"10.1007\/3-540-63165-8_199"},{"key":"442_CR15","doi-asserted-by":"crossref","unstructured":"Baier C, Klein J, Kl\u00fcppelholz S, M\u00e4rcker S (2014) Computing conditional probabilities in Markovian models efficiently. In: TACAS, LNCS, vol 8413. Springer, Berlin, pp 515\u2013530","DOI":"10.1007\/978-3-642-54862-8_43"},{"key":"442_CR16","doi-asserted-by":"crossref","unstructured":"Baier C, de\u00a0Alfaro L, Forejt V, Kwiatkowska M (2018) Model checking probabilistic systems. In: Handbook of model checking. Springer, Berlin, pp 963\u2013999","DOI":"10.1007\/978-3-319-10575-8_28"},{"issue":"104","key":"442_CR17","first-page":"504","volume":"272","author":"C Baier","year":"2020","unstructured":"Baier C, Hensel C, Hutschenreiter L, Junges S, Katoen J, Klein J (2020) Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. Inf Comput 272(104):504","journal-title":"Inf Comput"},{"key":"442_CR18","unstructured":"Barrett C, Fontaine P, Tinelli C (2016) The satisfiability modulo theories library (SMT-LIB). www.SMT-LIB.org"},{"key":"442_CR19","doi-asserted-by":"crossref","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 (2018) Reachability in parametric interval Markov chains using constraints. Theor Comput Sci 747:48\u201374","journal-title":"Theor Comput Sci"},{"key":"442_CR20","doi-asserted-by":"crossref","unstructured":"Bartocci E, Grosu R, Katsaros P, Ramakrishnan C, Smolka SA (2011) Model repair for probabilistic systems. In: TACAS, LNCS, vol 6605. Springer, Berlin, pp 326\u2013340","DOI":"10.1007\/978-3-642-19835-9_30"},{"key":"442_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in real algebraic geometry (algorithms and computation in mathematics)","author":"S Basu","year":"2006","unstructured":"Basu S, Pollack R, Roy MF (2006) Algorithms in real algebraic geometry (algorithms and computation in mathematics). Springer, New York"},{"issue":"1","key":"442_CR22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/jsco.2001.0494","volume":"33","author":"C Bauer","year":"2002","unstructured":"Bauer C, Frink A, Kreckel R (2002) Introduction to the Ginac framework for symbolic computation within the C++ programming language. J Symb Comput 33(1):1\u201312","journal-title":"J Symb Comput"},{"key":"442_CR23","volume-title":"Handbook of satisfiability, frontiers in artificial intelligence and applications","year":"2009","unstructured":"Biere A, Heule M, van Maaren H, Walsh T (eds) (2009) Handbook of satisfiability, frontiers in artificial intelligence and applications, vol 185. IOS Press, Amsterdam"},{"key":"442_CR24","volume-title":"Reliability and availability engineering: modeling, analysis, and applications","author":"A Bobbio","year":"2017","unstructured":"Bobbio A, Trivedi KS (2017) Reliability and availability engineering: modeling, analysis, and applications. Cambridge University Press, Cambridge"},{"key":"442_CR25","doi-asserted-by":"crossref","unstructured":"Bortolussi L, Silvetti S (2018) Bayesian statistical parameter synthesis for linear temporal properties of stochastic models. In: TACAS (2), LNCS, vol 10806. Springer, Berlin, pp 396\u2013413","DOI":"10.1007\/978-3-319-89963-3_23"},{"key":"442_CR26","doi-asserted-by":"crossref","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 (2016) Smoothed model checking for uncertain continuous-time Markov chains. Inf Comput 247:235\u2013253","journal-title":"Inf Comput"},{"issue":"2","key":"442_CR27","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1109\/TDSC.2009.45","volume":"7","author":"H Boudali","year":"2010","unstructured":"Boudali H, Crouzen P, Stoelinga M (2010) A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Trans Depend Secure Comput 7(2):128\u2013143","journal-title":"IEEE Trans Depend Secure Comput"},{"key":"442_CR28","doi-asserted-by":"crossref","DOI":"10.1201\/b10094","volume-title":"Design and safety assessment of critical systems","author":"M Bozzano","year":"2010","unstructured":"Bozzano M, Villafiorita A (2010) Design and safety assessment of critical systems. CRC Press, Cambridge"},{"key":"442_CR29","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1016\/j.ress.2014.07.003","volume":"132","author":"M Bozzano","year":"2014","unstructured":"Bozzano M, Cimatti A, Katoen JP, Katsaros P, Mokos K, Nguyen VY, Noll T, Postma B, Roveri M (2014) Spacecraft early design validation using formal methods. Reliab Eng Syst Saf 132:20\u201335","journal-title":"Reliab Eng Syst Saf"},{"key":"442_CR30","doi-asserted-by":"crossref","unstructured":"Brim L, Ceska M, Drazan S, Safr\u00e1nek D (2013) Exploring parameter space of stochastic biochemical systems using quantitative model checking. In: CAV, LNCS, vol 8044. Springer, Berlin, pp 107\u2013123","DOI":"10.1007\/978-3-642-39799-8_7"},{"key":"442_CR31","doi-asserted-by":"crossref","unstructured":"Bruttomesso R, Cimatti A, Franz\u00e9n A, Griggio A, Sebastiani R (2008) The MathSAT 4 SMT solver. In: CAV, LNCS, vol 5123. Springer, Berlin, pp 299\u2013303","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"442_CR32","doi-asserted-by":"crossref","unstructured":"Budde CE, Dehnert C, Hahn EM, Hartmanns A, Junges S, Turrini A (2017) JANI: quantitative model and tool interaction. In: TACAS (2), LNCS, vol 10206, pp 151\u2013168","DOI":"10.1007\/978-3-662-54580-5_9"},{"issue":"1","key":"442_CR33","doi-asserted-by":"crossref","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 (2016) Formal verification with confidence intervals to establish quality of service properties of software systems. IEEE Trans Reliab 65(1):107\u2013125","journal-title":"IEEE Trans Reliab"},{"key":"442_CR34","doi-asserted-by":"crossref","unstructured":"Calinescu R, Johnson K, Paterson C (2016) FACT: a probabilistic model checker for formal verification with confidence intervals. In: TACAS, LNCS, vol 9636. Springer, Berlin, pp 540\u2013546","DOI":"10.1007\/978-3-662-49674-9_32"},{"key":"442_CR35","doi-asserted-by":"crossref","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 (2018) Efficient synthesis of robust models for stochastic systems. J Syst Softw 143:140\u2013158","journal-title":"J Syst Softw"},{"issue":"3","key":"442_CR36","doi-asserted-by":"crossref","first-page":"1211","DOI":"10.1137\/07069821X","volume":"19","author":"MC Campi","year":"2008","unstructured":"Campi MC, Garatti S (2008) The exact feasibility of randomized solutions of uncertain convex programs. SIAM J Optim 19(3):1211\u20131230","journal-title":"SIAM J Optim"},{"issue":"2","key":"442_CR37","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/s10957-010-9754-6","volume":"148","author":"MC Campi","year":"2011","unstructured":"Campi MC, Garatti S (2011) A sampling-and-discarding approach to chance-constrained optimization: feasibility and optimality. J Optim Theory Appl 148(2):257\u2013280","journal-title":"J Optim Theory Appl"},{"key":"442_CR38","unstructured":"Cerotti D, Donatelli S, Horv\u00e1th A, Sproston J (2006) CSL model checking for generalized stochastic Petri nets. In: QEST. IEEE Computer Society, pp 199\u2013210"},{"key":"442_CR39","doi-asserted-by":"crossref","unstructured":"Ceska M, Dannenberg F, Kwiatkowska MZ, Paoletti N (2014) Precise parameter synthesis for stochastic biochemical systems. In: CMSB, LNCS, vol 8859. Springer, Berlin, pp 86\u201398","DOI":"10.1007\/978-3-319-12982-2_7"},{"key":"442_CR40","doi-asserted-by":"crossref","unstructured":"Ceska M, Pilar P, Paoletti N, Brim L, Kwiatkowska MZ (2016) PRISM-PSY: precise GPU-accelerated parameter synthesis for stochastic systems. In: TACAS, LNCS, vol 9636. Springer, Berlin, pp 367\u2013384","DOI":"10.1007\/978-3-662-49674-9_21"},{"key":"442_CR41","doi-asserted-by":"crossref","unstructured":"Ceska M, Jansen N, Junges S, Katoen J (2019) Shepherding hordes of Markov chains. In: TACAS (2), Lecture Notes in Computer Science, vol 11428. Springer, Berlin, pp 172\u2013190","DOI":"10.1007\/978-3-030-17465-1_10"},{"issue":"1","key":"442_CR42","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/j.ic.2018.02.019","volume":"259","author":"G Chatzieleftheriou","year":"2018","unstructured":"Chatzieleftheriou G, Katsaros P (2018) Abstract model repair for probabilistic systems. Inf Comput 259(1):142\u2013160","journal-title":"Inf Comput"},{"key":"442_CR43","doi-asserted-by":"crossref","unstructured":"Chen T, Hahn EM, Han T, Kwiatkowska M, Qu H, Zhang L (2013) Model repair for Markov decision processes. In: TASE. IEEE Computer Society, pp 85\u201392","DOI":"10.1109\/TASE.2013.20"},{"key":"442_CR44","doi-asserted-by":"crossref","unstructured":"Chen T, Feng Y, Rosenblum DS, Su G (2014) Perturbation analysis in verification of discrete-time Markov chains. In: CONCUR, LNCS, vol 8704. Springer, Berlin, pp 218\u2013233","DOI":"10.1007\/978-3-662-44584-6_16"},{"key":"442_CR45","unstructured":"Chonev V (2017) Reachability in augmented interval Markov chains. CoRR arXiv:1701.02996"},{"key":"442_CR46","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge"},{"key":"442_CR47","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: CAV, LNCS, vol 1855. Springer, Berlin, pp 154\u2013169","DOI":"10.1007\/10722167_15"},{"key":"442_CR48","unstructured":"Condon A (1990) On algorithms for simple stochastic games. In: Advances in computational complexity theory, DIMACS\/AMS, DIMACS series in discrete mathematics and theoretical computer science, vol 13, pp 51\u201372"},{"key":"442_CR49","doi-asserted-by":"crossref","unstructured":"Cook B (2018) Formal reasoning about the security of Amazon web services. In: CAV, LNCS, vol 10981. Springer, Berlin, pp 38\u201347","DOI":"10.1007\/978-3-319-96145-3_3"},{"key":"442_CR50","doi-asserted-by":"publisher","unstructured":"Coppit D, Sullivan KJ, Dugan JB (2000) Formal semantics of models for computational engineering: a case study on Dynamic Fault Trees. In: ISSRE. IEEE Computer Society, pp 270\u2013282. https:\/\/doi.org\/10.1109\/ISSRE.2000.885878","DOI":"10.1109\/ISSRE.2000.885878"},{"key":"442_CR51","volume-title":"Introduction to algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen TH, Leiserson CE, Rivest RL, Stein C (2009) Introduction to algorithms, 3rd edn. MIT Press, Cambridge","edition":"3"},{"key":"442_CR52","doi-asserted-by":"crossref","unstructured":"Corzilius F, Kremer G, Junges S, Schupp S, \u00c1brah\u00e1m E (2015) SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In: SAT, LNCS, vol 9340. Springer, Berlin, pp 360\u2013368","DOI":"10.1007\/978-3-319-24318-4_26"},{"key":"442_CR53","doi-asserted-by":"crossref","unstructured":"Costen C, Rigter M, Lacerda B, Hawes N (2023) Planning with hidden parameter polynomial MDPs. In: AAAI. AAAI Press, Pomona, pp 11,963\u201311,971","DOI":"10.1609\/aaai.v37i10.26411"},{"key":"442_CR54","doi-asserted-by":"crossref","unstructured":"Courcoubetis C, Yannakakis M (1988) Verifying temporal properties of finite-state probabilistic programs. In: FOCS. IEEE Computer Society, pp 338\u2013345","DOI":"10.1109\/SFCS.1988.21950"},{"issue":"1","key":"442_CR55","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1109\/TDEI.2009.4784578","volume":"16","author":"D Cousineau","year":"2009","unstructured":"Cousineau D (2009) Fitting the three-parameter Weibull distribution: review and evaluation of existing and new methods. IEEE Trans Dielectr Electr Insul 16(1):281\u2013288","journal-title":"IEEE Trans Dielectr Electr Insul"},{"key":"442_CR56","doi-asserted-by":"crossref","unstructured":"Cubuktepe M, Jansen N, Junges S, Katoen JP, Papusha I, Poonawala HA, Topcu U (2017) Sequential convex programming for the efficient verification of parametric MDPs. In: TACAS (2), LNCS, vol 10206, pp 133\u2013150","DOI":"10.1007\/978-3-662-54580-5_8"},{"key":"442_CR57","doi-asserted-by":"crossref","unstructured":"Cubuktepe M, Jansen N, Junges S, Katoen JP, Topcu U (2018) Synthesis in pMDPs: a tale of 1001 parameters. In: ATVA, LNCS, vol 11138. Springer, Berlin, pp 160\u2013176","DOI":"10.1007\/978-3-030-01090-4_10"},{"key":"442_CR58","doi-asserted-by":"crossref","unstructured":"Cubuktepe M, Jansen N, Junges S, Katoen J, Topcu U (2020) Scenario-based verification of uncertain MDPs. In: TACAS (1), LNCS, vol 12078. Springer, Berlin, pp 287\u2013305","DOI":"10.1007\/978-3-030-45190-5_16"},{"key":"442_CR59","doi-asserted-by":"crossref","unstructured":"Cubuktepe M, Jansen N, Junges S, Marandi A, Suilen M, Topcu U (2021) Robust finite-state controllers for uncertain POMDPs. In: AAAI. AAAI Press, Pomona, pp 11,792\u201311,800","DOI":"10.1609\/aaai.v35i13.17401"},{"issue":"12","key":"442_CR60","doi-asserted-by":"crossref","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 (2022) Convex optimization for parameter synthesis in MDPs. IEEE Trans Autom Control 67(12):6333\u20136348","journal-title":"IEEE Trans Autom Control"},{"key":"442_CR61","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio PR, Katoen JP, Ruys TC, Tretmans J (1997) The bounded retransmission protocol must be on time! In: TACAS, LNCS, vol 1217. Springer, Berlin, pp 416\u2013431","DOI":"10.1007\/BFb0035403"},{"key":"442_CR62","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio PR, Jeannet B, Jensen HE, Larsen KG (2001) Reachability analysis of probabilistic systems by successive refinements. In: PAPM-PROBMIV, LNCS, vol 2165. Springer, Berlin, pp 39\u201356","DOI":"10.1007\/3-540-44804-7_3"},{"key":"442_CR63","doi-asserted-by":"crossref","unstructured":"de Moura LM, Bj\u00f8rner N (2008) Z3: An efficient SMT solver. In: TACAS, LNCS, vol 4963. Springer, Berlin, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"442_CR64","doi-asserted-by":"crossref","unstructured":"Daws C (2004) Symbolic and parametric model checking of discrete-time Markov chains. In: ICTAC, LNCS, vol 3407. Springer, Berlin, pp 280\u2013294","DOI":"10.1007\/978-3-540-31862-0_21"},{"key":"442_CR65","doi-asserted-by":"crossref","unstructured":"Dehnert C, Junges S, Jansen N, Corzilius F, Volk M, Bruintjes H, Katoen JP, \u00c1brah\u00e1m E (2015) Prophesy: a probabilistic parameter synthesis tool. In: CAV, LNCS, vol 9206. Springer, Berlin, pp 214\u2013231","DOI":"10.1007\/978-3-319-21690-4_13"},{"key":"442_CR66","doi-asserted-by":"crossref","unstructured":"Dehnert C, Junges S, Katoen JP, Volk M (2017) A storm is coming: a modern probabilistic model checker. In: CAV, LNCS, vol 10427. Springer, Berlin, pp 592\u2013600","DOI":"10.1007\/978-3-319-63390-9_31"},{"issue":"9\u201310","key":"442_CR67","doi-asserted-by":"crossref","first-page":"1498","DOI":"10.1016\/j.artint.2011.01.001","volume":"175","author":"KV Delgado","year":"2011","unstructured":"Delgado KV, Sanner S, de Barros LN (2011) Efficient solutions to factored MDPs with imprecise transition probabilities. Artif Intell 175(9\u201310):1498\u20131527","journal-title":"Artif Intell"},{"key":"442_CR68","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1016\/j.artint.2015.09.005","volume":"230","author":"KV Delgado","year":"2016","unstructured":"Delgado KV, de Barros LN, Dias DB, Sanner S (2016) Real-time dynamic programming for Markov decision processes with imprecise probabilities. Artif Intell 230:192\u2013223","journal-title":"Artif Intell"},{"key":"442_CR69","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-01492-5","volume-title":"Handbook of weighted automata","author":"M Droste","year":"2009","unstructured":"Droste M, Kuich W, Vogler H (2009) Handbook of weighted automata. Springer, Berlin"},{"issue":"6","key":"442_CR70","doi-asserted-by":"crossref","first-page":"621","DOI":"10.1007\/s10009-006-0014-x","volume":"8","author":"M Duflot","year":"2006","unstructured":"Duflot M, Kwiatkowska MZ, Norman G, Parker D (2006) A formal analysis of bluetooth device discovery. STTT 8(6):621\u2013632","journal-title":"STTT"},{"issue":"3","key":"442_CR71","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1109\/24.159800","volume":"41","author":"JB Dugan","year":"1992","unstructured":"Dugan JB, Bavuso SJ, Boyd MA (1992) Dynamic fault-tree models for fault-tolerant computer systems. Trans Reliab 41(3):363\u2013377. https:\/\/doi.org\/10.1109\/24.159800","journal-title":"Trans Reliab"},{"issue":"1","key":"442_CR72","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1109\/TSE.2015.2421318","volume":"42","author":"A Filieri","year":"2016","unstructured":"Filieri A, Tamburrelli G, Ghezzi C (2016) Supporting self-adaptation via quantitative verification and sensitivity analysis at run time. IEEE Trans Software Eng 42(1):75\u201399","journal-title":"IEEE Trans Software Eng"},{"key":"442_CR73","doi-asserted-by":"crossref","unstructured":"Gainer P, Hahn EM, Schewe S (2018) Accelerated model checking of parametric Markov chains. In: ATVA, LNCS, vol 11138. Springer, Berlin, pp 300\u2013316","DOI":"10.1007\/978-3-030-01090-4_18"},{"issue":"1\u20132","key":"442_CR74","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/S0004-3702(00)00047-3","volume":"122","author":"R Givan","year":"2000","unstructured":"Givan R, Leach SM, Dean TL (2000) Bounded-parameter Markov decision processes. Artif Intell 122(1\u20132):71\u2013109","journal-title":"Artif Intell"},{"key":"442_CR75","doi-asserted-by":"crossref","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 (2019) Markov chains with perturbed rates to absorption: theory and application to model repair. Perform Evaluat 130:32\u201350","journal-title":"Perform Evaluat"},{"key":"442_CR76","unstructured":"Guennebaud G, Jacob B et\u00a0al (2010) Eigen v3. http:\/\/eigen.tuxfamily.org"},{"key":"442_CR77","doi-asserted-by":"crossref","unstructured":"Hahn EM, Hermanns H, Wachter B, Zhang L (2010) PARAM: a model checker for parametric Markov models. In: CAV, LNCS, vol 6174. Springer, Berlin, pp 660\u2013664","DOI":"10.1007\/978-3-642-14295-6_56"},{"issue":"1","key":"442_CR78","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2010","unstructured":"Hahn EM, Hermanns H, Zhang L (2010) Probabilistic reachability for parametric Markov models. STTT 13(1):3\u201319","journal-title":"STTT"},{"key":"442_CR79","doi-asserted-by":"crossref","unstructured":"Hahn EM, Han T, Zhang L (2011) Synthesis for PCTL in parametric Markov decision processes. In: NASA formal methods, LNCS, vol 6617. Springer, Berlin, pp 146\u2013161","DOI":"10.1007\/978-3-642-20398-5_12"},{"issue":"2","key":"442_CR80","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10703-012-0167-z","volume":"43","author":"EM Hahn","year":"2013","unstructured":"Hahn EM, Hartmanns A, Hermanns H, Katoen JP (2013) A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst Des 43(2):191\u2013232","journal-title":"Formal Methods Syst Des"},{"key":"442_CR81","doi-asserted-by":"crossref","unstructured":"Hahn EM, Hashemi V, Hermanns H, Lahijanian M, Turrini A (2017) Multi-objective robust strategy synthesis for interval Markov decision processes. In: QEST, LNCS, vol 10503. Springer, Berlin, pp 207\u2013223","DOI":"10.1007\/978-3-319-66335-7_13"},{"key":"442_CR82","doi-asserted-by":"crossref","unstructured":"Hahn EM, Hashemi V, Hermanns H, Lahijanian M, Turrini A (2019) Interval Markov decision processes with multiple objectives: From robust strategies to pareto curves. ACM Trans Model Comput Simul 29(4):27:1\u201327:31","DOI":"10.1145\/3309683"},{"key":"442_CR83","doi-asserted-by":"crossref","unstructured":"Han T, Katoen JP, Mereacre A (2008) Approximate parameter synthesis for probabilistic time-bounded reachability. In: RTSS. IEEE Computer Society, pp 173\u2013182","DOI":"10.1109\/RTSS.2008.19"},{"issue":"4","key":"442_CR84","doi-asserted-by":"crossref","first-page":"445","DOI":"10.3233\/FI-2013-952","volume":"128","author":"Y Han","year":"2013","unstructured":"Han Y (2013) State elimination heuristics for short regular expressions. Fundam Inform 128(4):445\u2013462","journal-title":"Fundam Inform"},{"issue":"1","key":"442_CR85","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/JPROC.2009.2032356","volume":"98","author":"M Haselman","year":"2010","unstructured":"Haselman M, Hauck S (2010) The future of integrated circuits: a survey of nanoelectronics. Proc IEEE 98(1):11\u201338","journal-title":"Proc IEEE"},{"key":"442_CR86","doi-asserted-by":"crossref","unstructured":"Heck L, Spel J, Junges S, Moerman J, Katoen J (2022) Gradient-descent for randomized controllers under partial observability. In: VMCAI, LNCS, vol. 13182. Springer, Berlin, pp 127\u2013150","DOI":"10.1007\/978-3-030-94583-1_7"},{"key":"442_CR87","doi-asserted-by":"crossref","unstructured":"Helmink L, Sellink MPA, Vaandrager FW (1993) Proof-checking a data link protocol. In: TYPES, LNCS, vol 806. Springer, Berlin, pp 127\u2013165","DOI":"10.1007\/3-540-58085-9_75"},{"issue":"2","key":"442_CR88","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/0020-0190(90)90107-9","volume":"35","author":"T Herman","year":"1990","unstructured":"Herman T (1990) Probabilistic self-stabilization. Inf Process Lett 35(2):63\u201367","journal-title":"Inf Process Lett"},{"key":"442_CR89","doi-asserted-by":"crossref","unstructured":"Holtzen S, Junges S, Vazquez-Chanlatte M, Millstein TD, Seshia SA, den Broeck GV (2021) Model checking finite-horizon Markov chains with probabilistic inference. In: CAV (2), LNCS, vol 12760. Springer, Berlin, pp 577\u2013601","DOI":"10.1007\/978-3-030-81688-9_27"},{"key":"442_CR90","volume-title":"Introduction to automata theory, languages, and computation","author":"JE Hopcroft","year":"2003","unstructured":"Hopcroft JE, Motwani R, Ullman JD (2003) Introduction to automata theory, languages, and computation. Addison-Wesley, Boston"},{"key":"442_CR91","doi-asserted-by":"crossref","unstructured":"Jansen N, Corzilius F, Volk M, Wimmer R, \u00c1brah\u00e1m E, Katoen JP, Becker B (2014) Accelerating parametric probabilistic verification. In: QEST, LNCS, vol 8657. Springer, Berlin, 404\u2013420","DOI":"10.1007\/978-3-319-10696-0_31"},{"key":"442_CR92","doi-asserted-by":"crossref","unstructured":"Jonsson B, Larsen KG (1991) Specification and refinement of probabilistic processes. In: LICS. IEEE Computer Society, pp 266\u2013277","DOI":"10.1109\/LICS.1991.151651"},{"issue":"1","key":"442_CR93","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/s10817-013-9281-x","volume":"51","author":"D Jovanovic","year":"2013","unstructured":"Jovanovic D, de Moura LM (2013) Cutting to the chase\u2014solving linear integer arithmetic. J Autom Reason 51(1):79\u2013108","journal-title":"J Autom Reason"},{"key":"442_CR94","unstructured":"Junges S (2020) Parameter synthesis in Markov models. Ph.D. thesis, RWTH Aachen University, Germany"},{"key":"442_CR95","doi-asserted-by":"crossref","unstructured":"Junges S, Spaan MTJ (2022) Abstraction-refinement for hierarchical probabilistic models. In: CAV (1), LNCS, vol 13371. Springer, Berlin, pp 102\u2013123","DOI":"10.1007\/978-3-031-13185-1_6"},{"key":"442_CR96","unstructured":"Junges S, Jansen N, Wimmer R, Quatmann T, Winterer L, Katoen JP, Becker B (2018) Finite-state controllers of POMDPs using parameter synthesis. In: UAI. AUAI Press, pp 519\u2013529"},{"key":"442_CR97","doi-asserted-by":"crossref","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 GA, Winkler T (2021) The complexity of reachability in parametric Markov decision processes. J Comput Syst Sci 119:183\u2013210","journal-title":"J Comput Syst Sci"},{"key":"442_CR98","doi-asserted-by":"crossref","unstructured":"Katoen JP (2016) The probabilistic model checking landscape. In: LICS. ACM","DOI":"10.1145\/2933575.2934574"},{"key":"442_CR99","unstructured":"Knuth D, Yao A (1976) Algorithms and complexity: new directions and recent results. Academic Press, chap The complexity of nonuniform random number generation"},{"issue":"2","key":"442_CR100","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1023\/A:1014745904458","volume":"8","author":"I Kozine","year":"2002","unstructured":"Kozine I, Utkin LV (2002) Interval-valued finite Markov chains. Reliable Comput 8(2):97\u2013113","journal-title":"Reliable Comput"},{"key":"442_CR101","doi-asserted-by":"crossref","unstructured":"Kurshan RP (2018) Transfer of model checking to industrial practice. In: Handbook of model checking. Springer, Berlin, pp 763\u2013793","DOI":"10.1007\/978-3-319-10575-8_23"},{"key":"442_CR102","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) Prism 4.0: verification of probabilistic real-time systems. In: CAV, LNCS, vol 6806. Springer, Berlin, pp 585\u2013591","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"442_CR103","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D (2012a) The PRISM benchmark suite. In: QEST. IEEE Computer Society, pp 203\u2013204","DOI":"10.1109\/QEST.2012.14"},{"issue":"4","key":"442_CR104","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/1364644.1364651","volume":"35","author":"MZ Kwiatkowska","year":"2008","unstructured":"Kwiatkowska MZ, Norman G, Parker D (2008) Using probabilistic model checking in systems biology. SIGMETRICS Perform Eval Rev 35(4):14\u201321","journal-title":"SIGMETRICS Perform Eval Rev"},{"issue":"4\u20136","key":"442_CR105","doi-asserted-by":"crossref","first-page":"661","DOI":"10.1007\/s00165-012-0227-6","volume":"24","author":"MZ Kwiatkowska","year":"2012","unstructured":"Kwiatkowska MZ, Norman G, Parker D (2012) Probabilistic verification of Herman\u2019s self-stabilisation algorithm. Formal Asp Comput 24(4\u20136):661\u2013670","journal-title":"Formal Asp Comput"},{"issue":"1","key":"442_CR106","doi-asserted-by":"crossref","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 (2007) Parametric probabilistic transition systems for system design and analysis. Formal Asp Comput 19(1):93\u2013109","journal-title":"Formal Asp Comput"},{"key":"442_CR107","doi-asserted-by":"crossref","unstructured":"Long F, Rinard M (2016) Automatic patch generation by learning correct code. In: POPL. ACM, pp 298\u2013312","DOI":"10.1145\/2914770.2837617"},{"key":"442_CR108","unstructured":"Mannor S, Mebel O, Xu H (2012) Lightning does not strike twice: robust MDPs with coupled uncertainty. In: ICML. icml.cc\/Omnipress"},{"issue":"2","key":"442_CR109","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/288197.581193","volume":"26","author":"MA Marsan","year":"1998","unstructured":"Marsan MA, Balbo G, Conte G, Donatelli S, Franceschinis G (1998) Modelling with generalized stochastic petri nets. SIGMETRICS Perform Evaluat Rev 26(2):2","journal-title":"SIGMETRICS Perform Evaluat Rev"},{"key":"442_CR110","doi-asserted-by":"crossref","unstructured":"McGlynn MJ, Borbash SA (2001) Birthday protocols for low energy deployment and flexible neighbor discovery in ad hoc wireless networks. In: MobiHoc. ACM, pp 137\u2013145","DOI":"10.1145\/501431.501435"},{"issue":"4","key":"442_CR111","doi-asserted-by":"crossref","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 (2014) Evaluating probabilistic models with uncertain model parameters. Softw Syst Model 13(4):1395\u20131415","journal-title":"Softw Syst Model"},{"issue":"6","key":"442_CR112","doi-asserted-by":"crossref","first-page":"1277","DOI":"10.1109\/18.45284","volume":"35","author":"M Mushkin","year":"1989","unstructured":"Mushkin M, Bar-David I (1989) Capacity and coding for the Gilbert\u2013Elliot channels. IEEE Trans Inf Theory 35(6):1277\u20131290","journal-title":"IEEE Trans Inf Theory"},{"key":"442_CR113","doi-asserted-by":"crossref","unstructured":"Neary C, Verginis CK, Cubuktepe M, Topcu U (2022) Verifiable and compositional reinforcement learning systems. In: ICAPS. AAAI Press, Pomona, pp 615\u2013623","DOI":"10.1609\/icaps.v32i1.19849"},{"issue":"6","key":"442_CR114","doi-asserted-by":"crossref","first-page":"561","DOI":"10.3233\/JCS-2006-14604","volume":"14","author":"G Norman","year":"2006","unstructured":"Norman G, Shmatikov V (2006) Analysis of probabilistic contract signing. J Comput Secur 14(6):561\u2013589","journal-title":"J Comput Secur"},{"issue":"10","key":"442_CR115","doi-asserted-by":"crossref","first-page":"1629","DOI":"10.1109\/TCAD.2005.852033","volume":"24","author":"G Norman","year":"2005","unstructured":"Norman G, Parker D, Kwiatkowska M, Shukla S (2005) Evaluating the reliability of NAND multiplexing with PRISM. IEEE Trans Comput Aided Des Integr Circuits Syst 24(10):1629\u20131637","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"issue":"3","key":"442_CR116","doi-asserted-by":"crossref","first-page":"354","DOI":"10.1007\/s11241-017-9269-4","volume":"53","author":"G Norman","year":"2017","unstructured":"Norman G, Parker D, Zou X (2017) Verification and control of partially observable probabilistic systems. Real-Time Syst 53(3):354\u2013402","journal-title":"Real-Time Syst"},{"key":"442_CR117","doi-asserted-by":"crossref","unstructured":"Pathak S, \u00c1brah\u00e1m E, Jansen N, Tacchella A, Katoen J (2015) A greedy approach for the efficient repair of stochastic models. In: NFM, LNCS, vol. 9058. Springer, Berlin, pp 295\u2013309","DOI":"10.1007\/978-3-319-17524-9_21"},{"key":"442_CR118","doi-asserted-by":"crossref","unstructured":"Petrucci L, van de Pol J (2018) Parameter synthesis algorithms for parametric interval Markov chains. In: FORTE, LNCS, vol. 10854. Springer, Berlin, pp 121\u2013140","DOI":"10.1007\/978-3-319-92612-4_7"},{"key":"442_CR119","doi-asserted-by":"crossref","unstructured":"Polgreen E, Wijesuriya VB, Haesaert S, Abate A (2016) Data-efficient bayesian verification of parametric Markov chains. In: QEST, LNCS, vol. 9826. Springer, Berlin, pp 35\u201351","DOI":"10.1007\/978-3-319-43425-4_3"},{"key":"442_CR120","doi-asserted-by":"crossref","unstructured":"Puggelli A, Li W, Sangiovanni-Vincentelli AL, Seshia SA (2013) Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: CAV, LNCS, vol 8044. Springer, Berlin, pp 527\u2013542","DOI":"10.1007\/978-3-642-39799-8_35"},{"key":"442_CR121","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316887","volume-title":"Markov decision processes: discrete stochastic dynamic programming","author":"ML Puterman","year":"1994","unstructured":"Puterman ML (1994) Markov decision processes: discrete stochastic dynamic programming. Wiley, New York"},{"key":"442_CR122","doi-asserted-by":"crossref","unstructured":"Quatmann T, Dehnert C, Jansen N, Junges S, Katoen JP (2016) Parameter synthesis for Markov models: Faster than ever. In: ATVA, LNCS, vol 9938, pp 50\u201367","DOI":"10.1007\/978-3-319-46520-3_4"},{"key":"442_CR123","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/j.cosrev.2015.03.001","volume":"15\u201316","author":"E Ruijters","year":"2015","unstructured":"Ruijters E, Stoelinga M (2015) Fault tree analysis: a survey of the state-of-the-art in modeling, analysis and tools. Comput Sci Rev 15\u201316:29\u201362","journal-title":"Comput Sci Rev"},{"key":"442_CR124","unstructured":"Russell SJ, Norvig P (2010) Artificial intelligence\u2014a modern approach (3. internat. ed.). Pearson Education, London"},{"key":"442_CR125","doi-asserted-by":"crossref","unstructured":"Sakarovitch J (2005) The language, the expression, and the (small) automaton. In: CIAA, LNCS, vol 3845. Springer, Berlin, pp 15\u201330","DOI":"10.1007\/11605157_2"},{"key":"442_CR126","doi-asserted-by":"crossref","unstructured":"Salmani B, Katoen J (2021) Fine-tuning the odds in bayesian networks. In: ECSQARU, LNCS, vol 12897. Springer, Berlin, pp 268\u2013283","DOI":"10.1007\/978-3-030-86772-0_20"},{"key":"442_CR127","doi-asserted-by":"crossref","unstructured":"Segala R, Turrini A (2005) Comparative analysis of bisimulation relations on alternating and non-alternating probabilistic models. In: QEST. IEEE Computer Society, pp 44\u201353","DOI":"10.1109\/QEST.2005.9"},{"issue":"10","key":"442_CR128","doi-asserted-by":"crossref","first-page":"1095","DOI":"10.1073\/pnas.39.10.1095","volume":"39","author":"LS Shapley","year":"1953","unstructured":"Shapley LS (1953) Stochastic games. Proc Natl Acad Sci 39(10):1095\u20131100","journal-title":"Proc Natl Acad Sci"},{"key":"442_CR129","doi-asserted-by":"crossref","unstructured":"Spel J, Junges S, Katoen J (2019) Are parametric Markov chains monotonic? In: ATVA, LNCS, vol 11781. Springer, Berlin, pp 479\u2013496","DOI":"10.1007\/978-3-030-31784-3_28"},{"key":"442_CR130","doi-asserted-by":"crossref","unstructured":"Spel J, Junges S, Katoen J (2021) Finding provably optimal Markov chains. In: TACAS (1), LNCS, vol 12651. Springer, Berlin, pp 173\u2013190","DOI":"10.1007\/978-3-030-72016-2_10"},{"issue":"7","key":"442_CR131","doi-asserted-by":"crossref","first-page":"623","DOI":"10.1109\/TSE.2015.2508444","volume":"42","author":"G Su","year":"2016","unstructured":"Su G, Feng Y, Chen T, Rosenblum DS (2016) Asymptotic perturbation bounds for probabilistic model checking with empirically determined probability parameters. IEEE Trans Software Eng 42(7):623\u2013639","journal-title":"IEEE Trans Software Eng"},{"key":"442_CR132","doi-asserted-by":"crossref","unstructured":"Suilen M, Jansen N, Cubuktepe M, Topcu U (2020) Robust policy synthesis for uncertain POMDPs via convex optimization. In: IJCAI, ijcai.org, pp 4113\u20134120","DOI":"10.24963\/ijcai.2020\/569"},{"key":"442_CR133","unstructured":"Suilen M, Sim\u00e3o TD, Parker D, Jansen N (2022) Robust anytime learning of Markov decision processes. In: NeurIPS"},{"key":"442_CR134","doi-asserted-by":"crossref","unstructured":"Tappler M, Aichernig BK, Bacci G, Eichlseder M, Larsen KG (2019) L$${}^{\\text{*}}$$-based learning of markov decision processes. In: FM, Lecture Notes in Computer Science, vol 11800. Springer, Berlin, pp 651\u2013669","DOI":"10.1007\/978-3-030-30942-8_38"},{"issue":"6","key":"442_CR135","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1007\/s10009-016-0433-2","volume":"19","author":"T van Dijk","year":"2017","unstructured":"van Dijk T, van de Pol J (2017) Sylvan: multi-core framework for decision diagrams. STTT 19(6):675\u2013696","journal-title":"STTT"},{"key":"442_CR136","doi-asserted-by":"crossref","unstructured":"Vardi MY (1985) Automatic verification of probabilistic concurrent finite-state programs. In: FOCS. IEEE Computer Society, pp 327\u2013338","DOI":"10.1109\/SFCS.1985.12"},{"key":"442_CR137","unstructured":"Vesely W, Stamatelatos M (2002) Fault tree handbook with aerospace applications. Tech. rep, NASA Headquarters, USA"},{"key":"442_CR138","doi-asserted-by":"crossref","unstructured":"Volk M, Junges S, Katoen JP (2016) Advancing dynamic fault tree analysis\u2014get succinct state spaces fast and synthesise failure rates. In: SAFECOMP, LNCS, vol 9922. Springer, Berlin, pp 253\u2013265","DOI":"10.1007\/978-3-319-45477-1_20"},{"issue":"1","key":"442_CR139","doi-asserted-by":"crossref","first-page":"370","DOI":"10.1109\/TII.2017.2710316","volume":"14","author":"M Volk","year":"2018","unstructured":"Volk M, Junges S, Katoen JP (2018) Fast dynamic fault tree analysis by model checking techniques. IEEE Trans Ind Inform 14(1):370\u2013379","journal-title":"IEEE Trans Ind Inform"},{"key":"442_CR140","first-page":"43","volume-title":"Automata studies","author":"J von Neumann","year":"1956","unstructured":"von Neumann J (1956) Probabilistic logics and synthesis of reliable organisms from unreliable components. In: Shannon C, McCarthy J (eds) Automata studies. Princeton University Press, Princeton, pp 43\u201398"},{"issue":"1","key":"442_CR141","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1287\/moor.1120.0566","volume":"38","author":"W Wiesemann","year":"2013","unstructured":"Wiesemann W, Kuhn D, Rustem B (2013) Robust Markov decision processes. Math Oper Res 38(1):153\u2013183","journal-title":"Math Oper Res"},{"key":"442_CR142","unstructured":"Winkler T, Junges S, P\u00e9rez GA, Katoen J (2019) On the complexity of reachability in parametric Markov decision processes. In: CONCUR, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, LIPIcs, vol 140, pp 14:1\u201314:17"},{"key":"442_CR143","unstructured":"Yang L, Murugesan S, Zhang J (2011) Real-time scheduling over Markovian channels: when partial observability meets hard deadlines. In: GLOBECOM. IEEE, pp 1\u20135"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00442-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00442-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00442-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,3]],"date-time":"2024-06-03T16:13:10Z","timestamp":1717431190000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00442-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,2,17]]},"references-count":143,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["442"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00442-x","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,2,17]]},"assertion":[{"value":"15 July 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 September 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 February 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}