The complexity of reachability in parametric Markov decision processes

Baier, 2020, Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination, Inf. Comput., 10.1016/j.ic.2019.104504 Baier, 2008 Bartocci, 2011, Model repair for probabilistic systems, vol. 6605, 326 Bernstein, 2002, The complexity of decentralized control of Markov decision processes, Math. Oper. Res., 27, 819, 10.1287/moor.27.4.819.297 Bortolussi, 2018, Bayesian statistical parameter synthesis for linear temporal properties of stochastic models, vol. 10806, 396 Canny, 1988, Some algebraic and geometric computations in PSPACE, 460 Ceska, 2017, Precise parameter synthesis for stochastic biochemical systems, Acta Inform., 54, 589, 10.1007/s00236-016-0265-2 Ceska, 2019, Counterexample-driven synthesis for probabilistic program sketches, vol. 11800, 101 Ceska, 2019, Shepherding hordes of Markov chains, vol. 11428, 172 Chatterjee, 2012, Robustness of structurally equivalent concurrent parity games, vol. 7213, 270 Chatterjee, 2016, A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs, 3225 Chen, 2014, Perturbation analysis in verification of discrete-time Markov chains, vol. 8704, 218 Chen, 2013, Model repair for Markov decision processes, 85 Chen, 2013, On the complexity of model checking interval-valued discrete time Markov chains, Inf. Process. Lett., 113, 210, 10.1016/j.ipl.2013.01.004 Chonev, 2019, Reachability in augmented interval Markov chains, vol. 11674, 79 Chung, 1967 Condon, 1989 Cubuktepe, 2018, Synthesis in pMDPs: a tale of 1001 parameters, vol. 11138, 160 Daws, 2004, Symbolic and parametric model checking of discrete-time Markov chains, vol. 3407, 280 Dehnert, 2015, A probabilistic parameter synthesis tool, vol. 9206, 214 Dehnert, 2017, A storm is coming: a modern probabilistic model checker, vol. 10427, 592 Valdivia Delgado, 2011, Efficient solutions to factored MDPs with imprecise transition probabilities, Artif. Intell., 175, 1498, 10.1016/j.artint.2011.01.001 Filieri, 2016, Supporting self-adaptation via quantitative verification and sensitivity analysis at run time, IEEE Trans. Softw. Eng., 42, 75, 10.1109/TSE.2015.2421318 Gainer, 2018, Accelerated model checking of parametric Markov chains, vol. 11138, 300 Giro, 2014, Ferrer Fioriti. Distributed probabilistic input/output automata: expressiveness, (un)decidability and algorithms, Theor. Comput. Sci., 538, 84, 10.1016/j.tcs.2013.07.017 Givan, 2000, Bounded-parameter Markov decision processes, Artif. Intell., 122, 71, 10.1016/S0004-3702(00)00047-3 Häggström, 2002, Finite Markov Chains and Algorithmic Applications, vol. 52 Moritz Hahn, 2011, Synthesis for PCTL in parametric Markov decision processes, vol. 6617, 146 Moritz Hahn, 2010, Probabilistic reachability for parametric Markov models, Int. J. Softw. Tools Technol. Transf., 13, 3, 10.1007/s10009-010-0146-x Howard, 1971, Dynamic Probabilistic Systems: Semi-Markov and Decision Processes, vol. 2 Hutschenreiter, 2017, Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination, vol. 256, 16 Jansen, 2014, Accelerating parametric probabilistic verification, vol. 8657, 404 Jonsson, 1991, Specification and refinement of probabilistic processes, 266 Junges, 2020 Junges Junges, 2018, Finite-state controllers of POMDPs using parameter synthesis, 519 Kallenberg, 2011, Markov Decision Processes Kemeny, 1976 Knuth, 1976, The complexity of nonuniform random number generation Kwiatkowska, 2011, PRISM 4.0: verification of probabilistic real-time systems, vol. 6806, 585 Lanotte, 2007, Parametric probabilistic transition systems for system design and analysis, Form. Asp. Comput., 19, 93, 10.1007/s00165-006-0015-2 Puggelli, 2013, Polynomial-time verification of PCTL properties of MDPs with convex uncertainties, vol. 8044, 527 Puterman, 1994 Quatmann, 2016, Parameter synthesis for Markov models: faster than ever, vol. 9938, 50 Renegar, 1992, 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, J. Symb. Comput., 13, 255, 10.1016/S0747-7171(10)80003-3 Russell, 2010 Schaefer, 2013, Realizability of graphs and linkages, 461 Schaefer, 2017, Fixed points, Nash equilibria, and the existential theory of the reals, Theory Comput. Syst., 60, 172, 10.1007/s00224-015-9662-0 Sen, 2006, Model-checking Markov chains in the presence of uncertainties, vol. 3920, 394 Seuken, 2008, Formal models and algorithms for decentralized decision making under uncertainty, Auton. Agents Multi-Agent Syst., 17, 190, 10.1007/s10458-007-9026-5 Solan, 2003, Continuity of the value of competitive Markov decision processes, J. Theor. Probab., 16, 831, 10.1023/B:JOTP.0000011995.28536.ef Spel, 2019, Are Parametric Markov Chains Monotonic?, vol. 11781, 479 Sproston, 2018, Qualitative reachability for open interval Markov chains, vol. 11123, 146 Vlassis, 2012, On the computational complexity of stochastic controller optimization in POMDPs, ACM Trans. Comput. Theory, 4, 12:1, 10.1145/2382559.2382563 Winkler, 2019, On the complexity of reachability in parametric Markov decision processes, vol. 140, 14:1 Wu, 2008, Reachability analysis of uncertain systems using bounded-parameter Markov decision processes, Artif. Intell., 172, 945, 10.1016/j.artint.2007.12.002