×

zbMATH — the first resource for mathematics

The complexity of reachability in parametric Markov decision processes. (English) Zbl 07332998
Summary: This article presents the complexity of reachability decision problems for parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over a finite set of parameters. In particular, we study the complexity of finding values for these parameters such that the induced MDP satisfies some maximal or minimal reachability probability constraints. We discuss different variants depending on the comparison operator in the constraints and the domain of the parameter values. We improve all known lower bounds for this problem, and notably provide ETR-completeness results for distinct variants of this problem.
MSC:
68-XX Computer science
Software:
PROPhESY; PRISM; Storm
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baier, Christel; Hensel, Christian; Hutschenreiter, Lisa; Junges, Sebastian; Katoen, Joost-Pieter; Klein, Joachim, Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination, Inf. Comput. (2020) · Zbl 1443.68101
[2] Baier, Christel; Katoen, Joost-Pieter, Principles of Model Checking (2008), MIT Press · Zbl 1179.68076
[3] Bartocci, Ezio; Grosu, Radu; Katsaros, Panagiotis; Ramakrishnan, C. R.; Smolka, Scott A., Model repair for probabilistic systems, (TACAS. TACAS, LNCS, vol. 6605 (2011), Springer), 326-340 · Zbl 1316.68070
[4] Bernstein, Daniel S.; Givan, Robert; Immerman, Neil; Zilberstein, Shlomo, The complexity of decentralized control of Markov decision processes, Math. Oper. Res., 27, 4, 819-840 (2002) · Zbl 1082.90593
[5] Bortolussi, Luca; Silvetti, Simone, Bayesian statistical parameter synthesis for linear temporal properties of stochastic models, (TACAS. TACAS, LNCS, vol. 10806 (2018), Springer), 396-413 · Zbl 1423.68322
[6] Canny, John F., Some algebraic and geometric computations in PSPACE, (STOC (1988), ACM), 460-467
[7] Ceska, Milan; Dannenberg, Frits; Paoletti, Nicola; Kwiatkowska, Marta; Brim, Lubos, Precise parameter synthesis for stochastic biochemical systems, Acta Inform., 54, 6, 589-623 (2017) · Zbl 1373.92038
[8] Ceska, Milan; Hensel, Christian; Junges, Sebastian; Katoen, Joost-Pieter, Counterexample-driven synthesis for probabilistic program sketches, (FM. FM, LNCS, vol. 11800 (2019), Springer), 101-120
[9] Ceska, Milan; Jansen, Nils; Junges, Sebastian; Katoen, Joost-Pieter, Shepherding hordes of Markov chains, (TACAS. TACAS, LNCS, vol. 11428 (2019), Springer), 172-190
[10] Chatterjee, Krishnendu, Robustness of structurally equivalent concurrent parity games, (FOSSACS. FOSSACS, LNCS, vol. 7213 (2012), Springer), 270-285 · Zbl 1352.68178
[11] Chatterjee, Krishnendu; Chmelik, Martin; Davies, Jessica, A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs, (AAAI (2016), AAAI Press), 3225-3232
[12] Chen, Taolue; Feng, Yuan; Rosenblum, David S.; Su, Guoxin, Perturbation analysis in verification of discrete-time Markov chains, (CONCUR. CONCUR, LNCS, vol. 8704 (2014), Springer), 218-233 · Zbl 1417.68100
[13] Chen, Taolue; Moritz Hahn, Ernst; Han, Tingting; Kwiatkowska, Marta Z.; Qu, Hongyang; Zhang, Lijun, Model repair for Markov decision processes, (TASE (2013), IEEE Computer Society), 85-92
[14] Chen, Taolue; Han, Tingting; Kwiatkowska, Marta Z., On the complexity of model checking interval-valued discrete time Markov chains, Inf. Process. Lett., 113, 7, 210-216 (2013) · Zbl 1259.68150
[15] Chonev, Ventsislav, Reachability in augmented interval Markov chains, (RP. RP, LNCS, vol. 11674 (2019), Springer), 79-92 · Zbl 07121138
[16] Chung, Kai Lai, Markov Chains (1967), Springer
[17] Condon, Anne, Computational models of games (1989), MIT Press, ACM Distinguished Dissertations
[18] Cubuktepe, Murat; Jansen, Nils; Junges, Sebastian; Katoen, Joost-Pieter; Topcu, Ufuk, Synthesis in pMDPs: a tale of 1001 parameters, (ATVA. ATVA, LNCS, vol. 11138 (2018), Springer), 160-176
[19] Daws, Conrado, Symbolic and parametric model checking of discrete-time Markov chains, (ICTAC. ICTAC, LNCS, vol. 3407 (2004), Springer), 280-294 · Zbl 1108.68497
[20] Dehnert, Christian; Junges, Sebastian; Jansen, Nils; Corzilius, Florian; Volk, Matthias; Bruintjes, Harold; Katoen, Joost-Pieter; Prophesy, Erika Ábrahám, A probabilistic parameter synthesis tool, (CAV. CAV, LNCS, vol. 9206 (2015), Springer), 214-231
[21] Dehnert, Christian; Junges, Sebastian; Katoen, Joost-Pieter; Volk, Matthias, A storm is coming: a modern probabilistic model checker, (CAV (2). CAV (2), LNCS, vol. 10427 (2017), Springer), 592-600
[22] Valdivia Delgado, Karina; Sanner, Scott; de Barros, Leliane Nunes, Efficient solutions to factored MDPs with imprecise transition probabilities, Artif. Intell., 175, 9-10, 1498-1527 (2011) · Zbl 1230.90115
[23] Filieri, Antonio; Tamburrelli, Giordano; Ghezzi, Carlo, Supporting self-adaptation via quantitative verification and sensitivity analysis at run time, IEEE Trans. Softw. Eng., 42, 1, 75-99 (2016)
[24] Gainer, Paul; Hahn, Ernst Moritz; Schewe, Sven, Accelerated model checking of parametric Markov chains, (ATVA. ATVA, LNCS, vol. 11138 (2018), Springer), 300-316
[25] Giro, Sergio; D’Argenio, Pedro R.; María, Luis, Ferrer Fioriti. Distributed probabilistic input/output automata: expressiveness, (un)decidability and algorithms, Theor. Comput. Sci., 538, 84-102 (2014) · Zbl 1359.68168
[26] Givan, Robert; Leach, Sonia; Dean, Thomas, Bounded-parameter Markov decision processes, Artif. Intell., 122, 1-2, 71-109 (2000) · Zbl 0948.68171
[27] Häggström, Olle, Finite Markov Chains and Algorithmic Applications, London Mathematical Society Student Texts, vol. 52 (2002), Cambridge University Press · Zbl 0999.60001
[28] Moritz Hahn, Ernst; Han, Tingting; Zhang, Lijun, Synthesis for PCTL in parametric Markov decision processes, (NASA Formal Methods. NASA Formal Methods, LNCS, vol. 6617 (2011), Springer), 146-161
[29] Moritz Hahn, Ernst; Hermanns, Holger; Zhang, Lijun, Probabilistic reachability for parametric Markov models, Int. J. Softw. Tools Technol. Transf., 13, 1, 3-19 (2010)
[30] Howard, R. A., Dynamic Probabilistic Systems: Semi-Markov and Decision Processes, Decision and Control, vol. 2 (1971), John Wiley & Sons · Zbl 0227.90032
[31] Hutschenreiter, Lisa; Baier, Christel; Klein, Joachim, Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination, (GandALF. GandALF, EPTCS, vol. 256 (2017)), 16-30
[32] Jansen, Nils; Corzilius, Florian; Volk, Matthias; Wimmer, Ralf; Ábrahám, Erika; Katoen, Joost-Pieter; Becker, Bernd, Accelerating parametric probabilistic verification, (QEST. QEST, LNCS, vol. 8657 (2014), Springer), 404-420
[33] Jonsson, Bengt; Larsen, Kim Guldstrand, Specification and refinement of probabilistic processes, (LICS (1991), IEEE Computer Society), 266-277 · Zbl 0967.68514
[34] Junges, Sebastian, Parameter synthesis in Markov models (2020), RWTH Aachen University, PhD thesis
[35] Junges, Sebastian; Abraham, Erika; Hensel, Christian; Jansen, Nils; Katoen, Joost-Pieter; Quatmann, Tim; Volk, Matthias, Parameter synthesis for Markov models (2019), CoRR
[36] Junges, Sebastian; Jansen, Nils; Wimmer, Ralf; Quatmann, Tim; Winterer, Leonore; Katoen, Joost-Pieter; Becker, Bernd, Finite-state controllers of POMDPs using parameter synthesis, (UAI (2018), AUAI Press), 519-529
[37] Kallenberg, Lodewijk, Markov Decision Processes, Lecture Notes (2011), University of Leiden · Zbl 0825.90776
[38] Kemeny, John G.; Laurie Snell, J., Markov Chains (1976), Springer · Zbl 0328.60035
[39] Knuth, D.; Yao, A., The complexity of nonuniform random number generation, (Algorithms and Complexity: New Directions and Recent Results (1976), Academic Press) · Zbl 0395.65004
[40] Kwiatkowska, Marta Z.; Norman, Gethin; Parker, David, PRISM 4.0: verification of probabilistic real-time systems, (CAV. CAV, LNCS, vol. 6806 (2011), Springer), 585-591
[41] Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Troina, Angelo, Parametric probabilistic transition systems for system design and analysis, Form. Asp. Comput., 19, 1, 93-109 (2007) · Zbl 1111.68084
[42] Puggelli, Alberto; Li, Wenchao; Sangiovanni-Vincentelli, Alberto L.; Seshia, Sanjit A., Polynomial-time verification of PCTL properties of MDPs with convex uncertainties, (CAV. CAV, LNCS, vol. 8044 (2013), Springer), 527-542 · Zbl 1435.68202
[43] Puterman, Martin L., Markov Decision Processes: Discrete Stochastic Dynamic Programming (1994), John Wiley & Sons · Zbl 0829.90134
[44] Quatmann, Tim; Dehnert, Christian; Jansen, Nils; Junges, Sebastian; Katoen, Joost-Pieter, Parameter synthesis for Markov models: faster than ever, (ATVA. ATVA, LNCS, vol. 9938 (2016), Springer), 50-67 · Zbl 1398.68346
[45] Renegar, James, 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, 3, 255-300 (1992) · Zbl 0763.68042
[46] Russell, Stuart J.; Norvig, Peter, Artificial Intelligence - A Modern Approach (2010), Pearson Education · Zbl 0835.68093
[47] Schaefer, Marcus, Realizability of graphs and linkages, (Thirty Essays on Geometric Graph Theory (2013), Springer: Springer New York), 461-482 · Zbl 1272.05135
[48] Schaefer, Marcus; Stefankovic, Daniel, Fixed points, Nash equilibria, and the existential theory of the reals, Theory Comput. Syst., 60, 2, 172-193 (2017) · Zbl 1362.68088
[49] Sen, Koushik; Viswanathan, Mahesh; Agha, Gul, Model-checking Markov chains in the presence of uncertainties, (TACAS. TACAS, LNCS, vol. 3920 (2006), Springer), 394-410 · Zbl 1180.68179
[50] Seuken, Sven; Zilberstein, Shlomo, Formal models and algorithms for decentralized decision making under uncertainty, Auton. Agents Multi-Agent Syst., 17, 2, 190-250 (2008)
[51] Solan, Eilon, Continuity of the value of competitive Markov decision processes, J. Theor. Probab., 16, 4, 831-845 (2003) · Zbl 1044.90087
[52] Spel, Jip; Junges, Sebastian; Katoen, Joost-Pieter, Are Parametric Markov Chains Monotonic?, (ATVA. ATVA, LNCS, vol. 11781 (2019), Springer), 479-496 · Zbl 1437.68121
[53] Sproston, Jeremy, Qualitative reachability for open interval Markov chains, (RP. RP, LNCS, vol. 11123 (2018), Springer), 146-160 · Zbl 06963056
[54] Vlassis, Nikos; Littman, Michael L.; Barber, David, On the computational complexity of stochastic controller optimization in POMDPs, ACM Trans. Comput. Theory, 4, 4, 12:1-12:8 (2012) · Zbl 1322.68111
[55] Winkler, Tobias; Junges, Sebastian; Pérez, Guillermo A.; Katoen, Joost-Pieter, On the complexity of reachability in parametric Markov decision processes, (CONCUR. CONCUR, LIPIcs, vol. 140 (2019), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 14:1-14:17
[56] Wu, Di; Koutsoukos, Xenofon D., Reachability analysis of uncertain systems using bounded-parameter Markov decision processes, Artif. Intell., 172, 8-9, 945-954 (2008) · Zbl 1183.68406
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.