{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T20:09:38Z","timestamp":1770754178473,"version":"3.50.0"},"reference-count":56,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2025,8,1]],"date-time":"2025-08-01T00:00:00Z","timestamp":1754006400000},"content-version":"vor","delay-in-days":1461,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"funder":[{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010663","name":"European Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100003187","name":"NSF","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100003187","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"DFG","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Computer and System Sciences"],"published-print":{"date-parts":[[2021,8]]},"DOI":"10.1016\/j.jcss.2021.02.006","type":"journal-article","created":{"date-parts":[[2021,3,8]],"date-time":"2021-03-08T16:42:09Z","timestamp":1615221729000},"page":"183-210","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":19,"special_numbering":"C","title":["The complexity of reachability in parametric Markov decision processes"],"prefix":"10.1016","volume":"119","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"first","affiliation":[]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]},{"given":"Guillermo A.","family":"P\u00e9rez","sequence":"additional","affiliation":[]},{"given":"Tobias","family":"Winkler","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.jcss.2021.02.006_br0010","doi-asserted-by":"crossref","DOI":"10.1016\/j.ic.2019.104504","article-title":"Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination","author":"Baier","year":"2020","journal-title":"Inf. Comput."},{"key":"10.1016\/j.jcss.2021.02.006_br0020","series-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"10.1016\/j.jcss.2021.02.006_br0030","series-title":"TACAS","first-page":"326","article-title":"Model repair for probabilistic systems","volume":"vol. 6605","author":"Bartocci","year":"2011"},{"issue":"4","key":"10.1016\/j.jcss.2021.02.006_br0040","doi-asserted-by":"crossref","first-page":"819","DOI":"10.1287\/moor.27.4.819.297","article-title":"The complexity of decentralized control of Markov decision processes","volume":"27","author":"Bernstein","year":"2002","journal-title":"Math. Oper. Res."},{"key":"10.1016\/j.jcss.2021.02.006_br0050","series-title":"TACAS","first-page":"396","article-title":"Bayesian statistical parameter synthesis for linear temporal properties of stochastic models","volume":"vol. 10806","author":"Bortolussi","year":"2018"},{"key":"10.1016\/j.jcss.2021.02.006_br0060","series-title":"STOC","first-page":"460","article-title":"Some algebraic and geometric computations in PSPACE","author":"Canny","year":"1988"},{"issue":"6","key":"10.1016\/j.jcss.2021.02.006_br0070","doi-asserted-by":"crossref","first-page":"589","DOI":"10.1007\/s00236-016-0265-2","article-title":"Precise parameter synthesis for stochastic biochemical systems","volume":"54","author":"Ceska","year":"2017","journal-title":"Acta Inform."},{"key":"10.1016\/j.jcss.2021.02.006_br0080","series-title":"FM","first-page":"101","article-title":"Counterexample-driven synthesis for probabilistic program sketches","volume":"vol. 11800","author":"Ceska","year":"2019"},{"key":"10.1016\/j.jcss.2021.02.006_br0090","series-title":"TACAS","first-page":"172","article-title":"Shepherding hordes of Markov chains","volume":"vol. 11428","author":"Ceska","year":"2019"},{"key":"10.1016\/j.jcss.2021.02.006_br0100","series-title":"FOSSACS","first-page":"270","article-title":"Robustness of structurally equivalent concurrent parity games","volume":"vol. 7213","author":"Chatterjee","year":"2012"},{"key":"10.1016\/j.jcss.2021.02.006_br0110","series-title":"AAAI","first-page":"3225","article-title":"A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs","author":"Chatterjee","year":"2016"},{"key":"10.1016\/j.jcss.2021.02.006_br0120","series-title":"CONCUR","first-page":"218","article-title":"Perturbation analysis in verification of discrete-time Markov chains","volume":"vol. 8704","author":"Chen","year":"2014"},{"key":"10.1016\/j.jcss.2021.02.006_br0130","series-title":"TASE","first-page":"85","article-title":"Model repair for Markov decision processes","author":"Chen","year":"2013"},{"issue":"7","key":"10.1016\/j.jcss.2021.02.006_br0140","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1016\/j.ipl.2013.01.004","article-title":"On the complexity of model checking interval-valued discrete time Markov chains","volume":"113","author":"Chen","year":"2013","journal-title":"Inf. Process. Lett."},{"key":"10.1016\/j.jcss.2021.02.006_br0150","series-title":"RP","first-page":"79","article-title":"Reachability in augmented interval Markov chains","volume":"vol. 11674","author":"Chonev","year":"2019"},{"key":"10.1016\/j.jcss.2021.02.006_br0160","series-title":"Markov Chains","author":"Chung","year":"1967"},{"key":"10.1016\/j.jcss.2021.02.006_br0170","series-title":"Computational models of games","author":"Condon","year":"1989"},{"key":"10.1016\/j.jcss.2021.02.006_br0180","series-title":"ATVA","first-page":"160","article-title":"Synthesis in pMDPs: a tale of 1001 parameters","volume":"vol. 11138","author":"Cubuktepe","year":"2018"},{"key":"10.1016\/j.jcss.2021.02.006_br0190","series-title":"ICTAC","first-page":"280","article-title":"Symbolic and parametric model checking of discrete-time Markov chains","volume":"vol. 3407","author":"Daws","year":"2004"},{"key":"10.1016\/j.jcss.2021.02.006_br0200","series-title":"CAV","first-page":"214","article-title":"A probabilistic parameter synthesis tool","volume":"vol. 9206","author":"Dehnert","year":"2015"},{"key":"10.1016\/j.jcss.2021.02.006_br0210","series-title":"CAV (2)","first-page":"592","article-title":"A storm is coming: a modern probabilistic model checker","volume":"vol. 10427","author":"Dehnert","year":"2017"},{"issue":"9\u201310","key":"10.1016\/j.jcss.2021.02.006_br0220","doi-asserted-by":"crossref","first-page":"1498","DOI":"10.1016\/j.artint.2011.01.001","article-title":"Efficient solutions to factored MDPs with imprecise transition probabilities","volume":"175","author":"Valdivia Delgado","year":"2011","journal-title":"Artif. Intell."},{"issue":"1","key":"10.1016\/j.jcss.2021.02.006_br0230","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1109\/TSE.2015.2421318","article-title":"Supporting self-adaptation via quantitative verification and sensitivity analysis at run time","volume":"42","author":"Filieri","year":"2016","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/j.jcss.2021.02.006_br0240","series-title":"ATVA","first-page":"300","article-title":"Accelerated model checking of parametric Markov chains","volume":"vol. 11138","author":"Gainer","year":"2018"},{"key":"10.1016\/j.jcss.2021.02.006_br0250","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1016\/j.tcs.2013.07.017","article-title":"Ferrer Fioriti. Distributed probabilistic input\/output automata: expressiveness, (un)decidability and algorithms","volume":"538","author":"Giro","year":"2014","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"10.1016\/j.jcss.2021.02.006_br0260","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/S0004-3702(00)00047-3","article-title":"Bounded-parameter Markov decision processes","volume":"122","author":"Givan","year":"2000","journal-title":"Artif. Intell."},{"key":"10.1016\/j.jcss.2021.02.006_br0270","article-title":"Finite Markov Chains and Algorithmic Applications","volume":"vol. 52","author":"H\u00e4ggstr\u00f6m","year":"2002"},{"key":"10.1016\/j.jcss.2021.02.006_br0280","series-title":"NASA Formal Methods","first-page":"146","article-title":"Synthesis for PCTL in parametric Markov decision processes","volume":"vol. 6617","author":"Moritz Hahn","year":"2011"},{"issue":"1","key":"10.1016\/j.jcss.2021.02.006_br0290","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","article-title":"Probabilistic reachability for parametric Markov models","volume":"13","author":"Moritz Hahn","year":"2010","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10.1016\/j.jcss.2021.02.006_br0300","article-title":"Dynamic Probabilistic Systems: Semi-Markov and Decision Processes","volume":"vol. 2","author":"Howard","year":"1971"},{"key":"10.1016\/j.jcss.2021.02.006_br0310","series-title":"GandALF","first-page":"16","article-title":"Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination","volume":"vol. 256","author":"Hutschenreiter","year":"2017"},{"key":"10.1016\/j.jcss.2021.02.006_br0320","series-title":"QEST","first-page":"404","article-title":"Accelerating parametric probabilistic verification","volume":"vol. 8657","author":"Jansen","year":"2014"},{"key":"10.1016\/j.jcss.2021.02.006_br0330","series-title":"LICS","first-page":"266","article-title":"Specification and refinement of probabilistic processes","author":"Jonsson","year":"1991"},{"key":"10.1016\/j.jcss.2021.02.006_br0340","series-title":"Parameter synthesis in Markov models","author":"Junges","year":"2020"},{"key":"10.1016\/j.jcss.2021.02.006_br0350","author":"Junges"},{"key":"10.1016\/j.jcss.2021.02.006_br0360","series-title":"UAI","first-page":"519","article-title":"Finite-state controllers of POMDPs using parameter synthesis","author":"Junges","year":"2018"},{"key":"10.1016\/j.jcss.2021.02.006_br0370","article-title":"Markov Decision Processes","author":"Kallenberg","year":"2011"},{"key":"10.1016\/j.jcss.2021.02.006_br0380","series-title":"Markov Chains","author":"Kemeny","year":"1976"},{"key":"10.1016\/j.jcss.2021.02.006_br0390","series-title":"Algorithms and Complexity: New Directions and Recent Results","article-title":"The complexity of nonuniform random number generation","author":"Knuth","year":"1976"},{"key":"10.1016\/j.jcss.2021.02.006_br0400","series-title":"CAV","first-page":"585","article-title":"PRISM 4.0: verification of probabilistic real-time systems","volume":"vol. 6806","author":"Kwiatkowska","year":"2011"},{"issue":"1","key":"10.1016\/j.jcss.2021.02.006_br0410","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/s00165-006-0015-2","article-title":"Parametric probabilistic transition systems for system design and analysis","volume":"19","author":"Lanotte","year":"2007","journal-title":"Form. Asp. Comput."},{"key":"10.1016\/j.jcss.2021.02.006_br0420","series-title":"CAV","first-page":"527","article-title":"Polynomial-time verification of PCTL properties of MDPs with convex uncertainties","volume":"vol. 8044","author":"Puggelli","year":"2013"},{"key":"10.1016\/j.jcss.2021.02.006_br0430","series-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"Puterman","year":"1994"},{"key":"10.1016\/j.jcss.2021.02.006_br0440","series-title":"ATVA","first-page":"50","article-title":"Parameter synthesis for Markov models: faster than ever","volume":"vol. 9938","author":"Quatmann","year":"2016"},{"issue":"3","key":"10.1016\/j.jcss.2021.02.006_br0450","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/S0747-7171(10)80003-3","article-title":"On the computational complexity and geometry of the first-order theory of the reals, part I: Introduction. Preliminaries. The geometry of semi-algebraic sets. the decision problem for the existential theory of the reals","volume":"13","author":"Renegar","year":"1992","journal-title":"J. Symb. Comput."},{"key":"10.1016\/j.jcss.2021.02.006_br0460","series-title":"Artificial Intelligence \u2013 A Modern Approach","author":"Russell","year":"2010"},{"key":"10.1016\/j.jcss.2021.02.006_br0470","series-title":"Thirty Essays on Geometric Graph Theory","first-page":"461","article-title":"Realizability of graphs and linkages","author":"Schaefer","year":"2013"},{"issue":"2","key":"10.1016\/j.jcss.2021.02.006_br0480","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/s00224-015-9662-0","article-title":"Fixed points, Nash equilibria, and the existential theory of the reals","volume":"60","author":"Schaefer","year":"2017","journal-title":"Theory Comput. Syst."},{"key":"10.1016\/j.jcss.2021.02.006_br0490","series-title":"TACAS","first-page":"394","article-title":"Model-checking Markov chains in the presence of uncertainties","volume":"vol. 3920","author":"Sen","year":"2006"},{"issue":"2","key":"10.1016\/j.jcss.2021.02.006_br0500","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/s10458-007-9026-5","article-title":"Formal models and algorithms for decentralized decision making under uncertainty","volume":"17","author":"Seuken","year":"2008","journal-title":"Auton. Agents Multi-Agent Syst."},{"issue":"4","key":"10.1016\/j.jcss.2021.02.006_br0510","doi-asserted-by":"crossref","first-page":"831","DOI":"10.1023\/B:JOTP.0000011995.28536.ef","article-title":"Continuity of the value of competitive Markov decision processes","volume":"16","author":"Solan","year":"2003","journal-title":"J. Theor. Probab."},{"key":"10.1016\/j.jcss.2021.02.006_br0560","series-title":"ATVA","first-page":"479","article-title":"Are Parametric Markov Chains Monotonic?","volume":"vol. 11781","author":"Spel","year":"2019"},{"key":"10.1016\/j.jcss.2021.02.006_br0520","series-title":"RP","first-page":"146","article-title":"Qualitative reachability for open interval Markov chains","volume":"vol. 11123","author":"Sproston","year":"2018"},{"issue":"4","key":"10.1016\/j.jcss.2021.02.006_br0530","doi-asserted-by":"crossref","first-page":"12:1","DOI":"10.1145\/2382559.2382563","article-title":"On the computational complexity of stochastic controller optimization in POMDPs","volume":"4","author":"Vlassis","year":"2012","journal-title":"ACM Trans. Comput. Theory"},{"key":"10.1016\/j.jcss.2021.02.006_br0540","series-title":"CONCUR","first-page":"14:1","article-title":"On the complexity of reachability in parametric Markov decision processes","volume":"vol. 140","author":"Winkler","year":"2019"},{"issue":"8\u20139","key":"10.1016\/j.jcss.2021.02.006_br0550","doi-asserted-by":"crossref","first-page":"945","DOI":"10.1016\/j.artint.2007.12.002","article-title":"Reachability analysis of uncertain systems using bounded-parameter Markov decision processes","volume":"172","author":"Wu","year":"2008","journal-title":"Artif. Intell."}],"container-title":["Journal of Computer and System Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0022000021000210?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0022000021000210?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,8,1]],"date-time":"2025-08-01T01:35:13Z","timestamp":1754012113000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0022000021000210"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8]]},"references-count":56,"alternative-id":["S0022000021000210"],"URL":"https:\/\/doi.org\/10.1016\/j.jcss.2021.02.006","relation":{},"ISSN":["0022-0000"],"issn-type":[{"value":"0022-0000","type":"print"}],"subject":[],"published":{"date-parts":[[2021,8]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"The complexity of reachability in parametric Markov decision processes","name":"articletitle","label":"Article Title"},{"value":"Journal of Computer and System Sciences","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.jcss.2021.02.006","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2021 Elsevier Inc.","name":"copyright","label":"Copyright"}]}}