Document Open Access Logo

On the Complexity of Reachability in Parametric Markov Decision Processes

Authors Tobias Winkler, Sebastian Junges , Guillermo A. Pérez , Joost-Pieter Katoen

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.14.pdf
  • Filesize: 0.55 MB
  • 17 pages

Document Identifiers

Author Details

Tobias Winkler
  • RWTH Aachen University, Germany
Sebastian Junges
  • RWTH Aachen University, Germany
Guillermo A. Pérez
  • University of Antwerp, Belgium
Joost-Pieter Katoen
  • RWTH Aachen University, Germany

Funding

This work has been supported by the DFG RTG 2236 "UnRAVeL", and the ERC Advanced Grant 787914 "FRAPPANT".

Acknowledgements

We would like to thank Krishnendu Chatterjee for his pointer to CSRGs.

Cite As Get BibTex

Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, and Joost-Pieter Katoen. On the Complexity of Reachability in Parametric Markov Decision Processes. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.CONCUR.2019.14

Abstract

This paper studies 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. Fixing values for all parameters yields MDPs. In particular, this paper studies the complexity of finding values for these parameters such that the induced MDP satisfies some reachability 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. Furthermore, we provide insights in the functions describing the induced reachability probabilities, and how pMDPs generalise concurrent stochastic reachability games.

Subject Classification

ACM Subject Classification
  • Theory of computation → Probabilistic computation
  • Theory of computation → Logic and verification
  • Theory of computation → Markov decision processes
Keywords
  • Parametric Markov decision processes
  • Formal verification
  • ETR
  • Complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Sebastian Arming, Ezio Bartocci, and Ana Sokolova. SEA-PARAM: exploring schedulers in parametric MDPs. In QAPL@ETAPS, volume 250 of EPTCS, pages 25-38, 2017. Google Scholar
  2. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  3. Ezio Bartocci, Radu Grosu, Panagiotis Katsaros, C. R. Ramakrishnan, and Scott A. Smolka. Model Repair for Probabilistic Systems. In TACAS, volume 6605 of LNCS, pages 326-340. Springer, 2011. Google Scholar
  4. Saugata Basu, Richard Pollack, and Marie-Françoise Roy. Existential theory of the reals. Algorithms in Real Algebraic Geometry, pages 505-532, 2006. Google Scholar
  5. Daniel S. Bernstein, Robert Givan, Neil Immerman, and Shlomo Zilberstein. The Complexity of Decentralized Control of Markov Decision Processes. Math. Oper. Res., 27(4):819-840, 2002. Google Scholar
  6. Luca Bortolussi and Simone Silvetti. Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models. In TACAS (2), volume 10806 of LNCS, pages 396-413. Springer, 2018. Google Scholar
  7. John F. Canny. Some Algebraic and Geometric Computations in PSPACE. In STOC, pages 460-467. ACM, 1988. Google Scholar
  8. Milan Ceska, Frits Dannenberg, Nicola Paoletti, Marta Kwiatkowska, and Lubos Brim. Precise parameter synthesis for stochastic biochemical systems. Acta Inf., 54(6):589-623, 2017. Google Scholar
  9. Krishnendu Chatterjee. Robustness of Structurally Equivalent Concurrent Parity Games. In FOSSACS, volume 7213 of LNCS, pages 270-285. Springer, 2012. Google Scholar
  10. Krishnendu Chatterjee, Martin Chmelik, and Jessica Davies. A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs. In AAAI, pages 3225-3232. AAAI Press, 2016. Google Scholar
  11. Krishnendu Chatterjee, Kristoffer Arnsfelt Hansen, and Rasmus Ibsen-Jensen. Strategy Complexity of Concurrent Safety Games. In MFCS, volume 83 of LIPIcs, pages 55:1-55:13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. Google Scholar
  12. Krishnendu Chatterjee and Thomas A. Henzinger. A survey of stochastic omega-regular games. J. Comput. Syst. Sci., 78(2):394-413, 2012. Google Scholar
  13. Taolue Chen, Yuan Feng, David S. Rosenblum, and Guoxin Su. Perturbation Analysis in Verification of Discrete-Time Markov Chains. In CONCUR, volume 8704 of LNCS, pages 218-233. Springer, 2014. Google Scholar
  14. Taolue Chen, Ernst Moritz Hahn, Tingting Han, Marta Z. Kwiatkowska, Hongyang Qu, and Lijun Zhang. Model Repair for Markov Decision Processes. In TASE, pages 85-92. IEEE Computer Society, 2013. Google Scholar
  15. Taolue Chen, Tingting Han, and Marta Z. Kwiatkowska. On the complexity of model checking interval-valued discrete time Markov chains. Inf. Process. Lett., 113(7):210-216, 2013. Google Scholar
  16. Ventsislav Chonev. Reachability in Augmented Interval Markov Chains. CoRR, abs/1701.02996, 2017. URL: http://arxiv.org/abs/1701.02996.
  17. Anne Condon. Computational models of games. ACM distinguished dissertations. MIT Press, 1989. Google Scholar
  18. Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, and Ufuk Topcu. Synthesis in pMDPs: A Tale of 1001 Parameters. In ATVA, volume 11138 of LNCS, pages 160-176. Springer, 2018. Google Scholar
  19. Conrado Daws. Symbolic and Parametric Model Checking of Discrete-Time Markov Chains. In ICTAC, volume 3407 of LNCS, pages 280-294. Springer, 2004. Google Scholar
  20. Luca de Alfaro, Thomas A. Henzinger, and Orna Kupferman. Concurrent reachability games. Theor. Comput. Sci., 386(3):188-217, 2007. Google Scholar
  21. Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes, Joost-Pieter Katoen, and Erika Ábrahám. PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. In CAV (1), volume 9206 of LNCS, pages 214-231. Springer, 2015. Google Scholar
  22. Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. A Storm is Coming: A Modern Probabilistic Model Checker. In CAV (2), volume 10427 of LNCS, pages 592-600. Springer, 2017. Google Scholar
  23. Karina Valdivia Delgado, Scott Sanner, and Leliane Nunes de Barros. Efficient solutions to factored MDPs with imprecise transition probabilities. Artif. Intell., 175(9-10):1498-1527, 2011. Google Scholar
  24. Antonio Filieri, Giordano Tamburrelli, and Carlo Ghezzi. Supporting Self-Adaptation via Quantitative Verification and Sensitivity Analysis at Run Time. IEEE Trans. Software Eng., 42(1):75-99, 2016. Google Scholar
  25. Paul Gainer, Ernst Moritz Hahn, and Sven Schewe. Accelerated Model Checking of Parametric Markov Chains. In ATVA, volume 11138 of LNCS, pages 300-316. Springer, 2018. Google Scholar
  26. Sergio Giro, Pedro R. D'Argenio, and Luis María Ferrer Fioriti. Distributed probabilistic input/output automata: Expressiveness, (un)decidability and algorithms. Theor. Comput. Sci., 538:84-102, 2014. Google Scholar
  27. Robert Givan, Sonia Leach, and Thomas Dean. Bounded-parameter Markov decision processes. Artif. Intell., 122(1-2):71-109, 2000. Google Scholar
  28. Ernst Moritz Hahn, Tingting Han, and Lijun Zhang. Synthesis for PCTL in Parametric Markov Decision Processes. In NASA Formal Methods, volume 6617 of LNCS, pages 146-161. Springer, 2011. Google Scholar
  29. Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. Probabilistic reachability for parametric Markov models. STTT, 13(1):3-19, 2010. Google Scholar
  30. David Handelman. Representing polynomials by positive linear functions on compact convex polyhedra. Pacific Journal of Mathematics, 132(1):35-62, 1988. Google Scholar
  31. Kristoffer Arnsfelt Hansen, Michal Koucký, and Peter Bro Miltersen. Winning Concurrent Reachability Games Requires Doubly-Exponential Patience. In LICS, pages 332-341. IEEE Computer Society, 2009. Google Scholar
  32. CJ Himmelberg, Thiruvenkatachari Parthasarathy, TES Raghavan, and FS Van Vleck. Existence of p-equilibrium and optimal stationary strategies in stochastic games. Proceedings of the American Mathematical Society, 60(1):245-251, 1976. Google Scholar
  33. Lisa Hutschenreiter, Christel Baier, and Joachim Klein. Parametric Markov Chains: PCTL Complexity and Fraction-free Gaussian Elimination. In GandALF, volume 256 of EPTCS, pages 16-30, 2017. Google Scholar
  34. Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, and Bernd Becker. Accelerating Parametric Probabilistic Verification. In QEST, volume 8657 of LNCS, pages 404-420. Springer, 2014. Google Scholar
  35. Bengt Jonsson and Kim Guldstrand Larsen. Specification and Refinement of Probabilistic Processes. In LICS, pages 266-277. IEEE Computer Society, 1991. Google Scholar
  36. Sebastian Junges, Erika Abraham, Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. Parameter Synthesis for Markov Models. CoRR, abs/1903.07993, 2019. URL: http://arxiv.org/abs/1903.07993.
  37. Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, and Bernd Becker. Finite-State Controllers of POMDPs using Parameter Synthesis. In UAI, pages 519-529. AUAI Press, 2018. Google Scholar
  38. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In CAV, volume 6806 of LNCS, pages 585-591. Springer, 2011. Google Scholar
  39. Ruggero Lanotte, Andrea Maggiolo-Schettini, and Angelo Troina. Parametric probabilistic transition systems for system design and analysis. Formal Asp. Comput., 19(1):93-109, 2007. Google Scholar
  40. Arnab Nilim and Laurent El Ghaoui. Robust Control of Markov Decision Processes with Uncertain Transition Matrices. Operations Research, 53(5):780-798, 2005. Google Scholar
  41. Thiruvenkatachari Parthasarathy. Discounted and positive stochastic games. Bulletin of the American Mathematical Society, 77(1):134-136, 1971. Google Scholar
  42. Alberto Puggelli, Wenchao Li, Alberto L. Sangiovanni-Vincentelli, and Sanjit A. Seshia. Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. In CAV, volume 8044 of LNCS, pages 527-542. Springer, 2013. Google Scholar
  43. Martin L. Puterman. Markov Decision Processes. Wiley, 1995. Google Scholar
  44. Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen. Parameter Synthesis for Markov Models: Faster Than Ever. In ATVA, volume 9938 of LNCS, pages 50-67, 2016. Google Scholar
  45. James Renegar. 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. Google Scholar
  46. Stuart J. Russell and Peter Norvig. Artificial Intelligence - A Modern Approach. Pearson Education, 2010. Google Scholar
  47. Marcus Schaefer. Realizability of Graphs and Linkages, pages 461-482. Springer New York, 2013. Google Scholar
  48. Marcus Schaefer and Daniel Stefankovic. Fixed Points, Nash Equilibria, and the Existential Theory of the Reals. Theory Comput. Syst., 60(2):172-193, 2017. Google Scholar
  49. Roberto Segala and Andrea Turrini. Comparative Analysis of Bisimulation Relations on Alternating and Non-Alternating Probabilistic Models. In QEST, pages 44-53. IEEE Computer Society, 2005. Google Scholar
  50. Koushik Sen, Mahesh Viswanathan, and Gul Agha. Model-Checking Markov Chains in the Presence of Uncertainties. In TACAS, volume 3920 of LNCS, pages 394-410. Springer, 2006. Google Scholar
  51. Sven Seuken and Shlomo Zilberstein. Formal models and algorithms for decentralized decision making under uncertainty. Autonomous Agents and Multi-Agent Systems, 17(2):190-250, 2008. Google Scholar
  52. Lloyd S. Shapley. Stochastic Games. PNAS, 39(10):1095-1100, 1953. Google Scholar
  53. Eilon Solan. Continuity of the value of competitive Markov decision processes. Journal of Theoretical Probability, 16(4):831-845, 2003. Google Scholar
  54. Jeremy Sproston. Qualitative Reachability for Open Interval Markov Chains. In RP, volume 11123 of LNCS, pages 146-160. Springer, 2018. Google Scholar
  55. Richard S. Sutton and Andrew G. Barto. Reinforcement learning - an introduction. Adaptive computation and machine learning. MIT Press, 1998. Google Scholar
  56. Nikos Vlassis, Michael L. Littman, and David Barber. On the Computational Complexity of Stochastic Controller Optimization in POMDPs. TOCT, 4(4):12:1-12:8, 2012. Google Scholar
  57. Wolfram Wiesemann, Daniel Kuhn, and Berç Rustem. Robust Markov Decision Processes. Math. Oper. Res., 38(1):153-183, 2013. Google Scholar
  58. Di Wu and Xenofon D. Koutsoukos. Reachability analysis of uncertain systems using bounded-parameter Markov decision processes. Artif. Intell., 172(8-9):945-954, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact