Document Open Access Logo

Combinations of Qualitative Winning for Stochastic Parity Games

Authors Krishnendu Chatterjee, Nir Piterman

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.6.pdf
  • Filesize: 497 kB
  • 17 pages

Document Identifiers

Author Details

Krishnendu Chatterjee
  • IST Austria, Klosterneuburg, Austria
Nir Piterman
  • University of Gothenburg, Sweden
  • University of Leicester, UK

Funding

  • Chatterjee, Krishnendu: This research is funded by Austrian Science Fund (FWF) NFN Grant S11407-N23 (RiSE/SHiNE), and Vienna Science and Technology Fund (WWTF) Project ICT15-003.
  • Piterman, Nir: This research is funded by the ERC consolidator grant D-SynMA under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 772459).

Cite AsGet BibTex

Krishnendu Chatterjee and Nir Piterman. Combinations of Qualitative Winning for Stochastic Parity Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.6

Abstract

We study Markov decision processes and turn-based stochastic games with parity conditions. There are three qualitative winning criteria, namely, sure winning, which requires all paths to satisfy the condition, almost-sure winning, which requires the condition to be satisfied with probability 1, and limit-sure winning, which requires the condition to be satisfied with probability arbitrarily close to 1. We study the combination of two of these criteria for parity conditions, e.g., there are two parity conditions one of which must be won surely, and the other almost-surely. The problem has been studied recently by Berthon et al. for MDPs with combination of sure and almost-sure winning, under infinite-memory strategies, and the problem has been established to be in NP cap co-NP. Even in MDPs there is a difference between finite-memory and infinite-memory strategies. Our main results for combination of sure and almost-sure winning are as follows: (a) we show that for MDPs with finite-memory strategies the problem is in NP cap co-NP; (b) we show that for turn-based stochastic games the problem is co-NP-complete, both for finite-memory and infinite-memory strategies; and (c) we present algorithmic results for the finite-memory case, both for MDPs and turn-based stochastic games, by reduction to non-stochastic parity games. In addition we show that all the above complexity results also carry over to combination of sure and limit-sure winning, and results for all other combinations can be derived from existing results in the literature. Thus we present a complete picture for the study of combinations of two qualitative winning criteria for parity conditions in MDPs and turn-based stochastic games.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Two Player Games
  • Stochastic Games
  • Parity Winning Conditions

Metrics

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

Related Versions

References

  1. S. Almagor, O. Kupferman, and Y. Velner. Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis. In 27th International Conference on Concurrency Theory, volume 59 of LIPIcs, pages 9:1-9:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  2. R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. J.ACM, 49(5):672-713, 2002. Google Scholar
  3. C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. Google Scholar
  4. N. Basset, M.Z. Kwiatkowska, U. Topcu, and C. Wiltsche. Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives. In Proc. 21st Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 9035 of Lecture Notes in Computer Science, pages 256-271. Springer, 2015. Google Scholar
  5. R. Berthon, M. Randour, and J.-F. Raskin. Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes. In 44th International Colloquium on Automata, Languages, and Programming, volume 80 of LIPIcs, pages 121:1-121:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. Google Scholar
  6. T. Brázdil, V. Brozek, K. Chatterjee, V. Forejt, and A. Kucera. Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. In Proc. 26rd IEEE Symp. on Logic in Computer Science, pages 33-42. IEEE Computer Society Press, 2011. Google Scholar
  7. V. Bruyère, E. Filiot, M. Randour, and J.-F. Raskin. Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. Inf. Comput., 254:259-295, 2017. Google Scholar
  8. C. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan. Deciding Parity Games in Quasipolynomial Time. In Proc. 49th ACM Symp. on Theory of Computing, pages 252-263. ACM Press, 2017. Google Scholar
  9. K. Chatterjee. Stochastic ω-regular Games. PhD thesis, University of California at Berkeley, 2007. Google Scholar
  10. K. Chatterjee and L. Doyen. Perfect-Information Stochastic Games with Generalized Mean-Payoff Objectives. In Proc. 31st IEEE Symp. on Logic in Computer Science, pages 247-256. ACM Press, 2016. Google Scholar
  11. K. Chatterjee, L. Doyen, M. Randour, and J.-F. Raskin. Looking at mean-payoff and total-payoff through windows. Information and Computation, 242:25-52, 2015. Google Scholar
  12. K. Chatterjee and M. Henzinger. Faster and Dynamic Algorithms For Maximal End-Component Decomposition And Related Graph Problems In Probabilistic Verification. In SODA'11. SIAM, 2011. Google Scholar
  13. K. Chatterjee, T.A. Henzinger, and N. Piterman. Generalized Parity Games. In Proc. 10th Int. Conf. on Foundations of Software Science and Computation Structures, volume 4423 of Lecture Notes in Computer Science, pages 153-167, Braga, Porgugal, 2007. Springer. Google Scholar
  14. K. Chatterjee, M. Jurdziński, and T.A. Henzinger. Simple Stochastic Parity Games. In Proc. 12th Annual Conf. of the European Association for Computer Science Logic, Lecture Notes in Computer Science, pages 100-113. Springer, 2003. Google Scholar
  15. K. Chatterjee, M. Jurdziński, and T.A. Henzinger. Quantitative Stochastic Parity Games. In Symposium on Discrete Algorithms, pages 114-123. SIAM, 2004. Google Scholar
  16. K. Chatterjee, Z. Komárková, and J. Kretínský. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. In Proc. 30th IEEE Symp. on Logic in Computer Science, pages 244-256. IEEE Computer Society Press, 2015. Google Scholar
  17. K. Chatterjee, R. Majumdar, and T.A. Henzinger. Markov Decision Processes with multiple objectives. In Proc. 23rd Symp. on Theoretical Aspects of Computer Science, volume 3884 of Lecture Notes in Computer Science, pages 325-336. Springer, 2006. Google Scholar
  18. K. Chatterjee and N. Piterman. Combinations of Qualitative Winning for Stochastic Parity Games. Technical report, arXiv, 2018. URL: http://arxiv.org/abs/1804.03453.
  19. Krishnendu Chatterjee and Monika Henzinger. Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition. J. ACM, 61(3):15:1-15:40, 2014. Google Scholar
  20. T. Chen, V. Forejt, M.Z. Kwiatkowska, A. Simaitis, and C. Wiltsche. On Stochastic Games with Multiple Objectives. In 38th Int. Symp. on Mathematical Foundations of Computer Science, volume 8087 of Lecture Notes in Computer Science, pages 266-277. Springer, 2013. Google Scholar
  21. A. Church. Logic, arithmetics, and automata. In Proc. Int. Congress of Mathematicians, 1962, pages 23-35. Institut Mittag-Leffler, 1963. Google Scholar
  22. A. Condon. The complexity of stochastic games. Information and Computation, 96:203-224, 1992. Google Scholar
  23. C. Courcoubetis and M. Yannakakis. The Complexity of Probabilistic Verification. jacm, 42(4):857-907, 1995. Google Scholar
  24. K. Etessami, M.Z. Kwiatkowska, M.Y. Vardi, and M. Yannakakis. Multi-Objective Model Checking of Markov Decision Processes. Logical Methods in Computer Science, 4(4), 2008. Google Scholar
  25. Jerzy Filar and Koos Vrieze. Competitive Markov decision processes. Springer, 1996. Google Scholar
  26. V. Forejt, M.Z. Kwiatkowska, G. Norman, D. Parker, and H. Qu. Quantitative Multi-objective Verification for Probabilistic Systems. In Proc. 17th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 6605 of Lecture Notes in Computer Science, pages 112-127. Springer, 2011. Google Scholar
  27. H. Gimbert and E. Kelmendi. Two-Player Perfect-Information Shift-Invariant Submixing Stochastic Games Are Half-Positional. CoRR, abs/1401.6575, 2014. URL: http://arxiv.org/abs/1401.6575.
  28. H. Gimbert and W. Zielonka. Games Where You Can Play Optimally Without Any Memory. In 16th Int. Conf. on Concurrency Theory, volume 3653 of Lecture Notes in Computer Science, pages 428-442. Springer, 2005. Google Scholar
  29. M. Jurdziński. Small Progress Measures for Solving Parity Games. In Proc. 17th Symp. on Theoretical Aspects of Computer Science, volume 1770 of Lecture Notes in Computer Science, pages 290-301, Lille, France, 2000. Springer. Google Scholar
  30. M. Jurdzinski and R. Lazic. Succinct progress measures for solving parity games. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 1-9, Reykjavik, Iceland, 2017. IEEE Computer Society Press. Google Scholar
  31. D.A. Martin. The Determinacy of Blackwell Games. The Journal of Symbolic Logic, 63(4):1565-1581, 1998. Google Scholar
  32. A. Pnueli and R. Rosner. On the Synthesis of a Reactive Module. In Proc. 16th ACM Symp. on Principles of Programming Languages, pages 179-190. ACM Press, 1989. Google Scholar
  33. Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, 1st edition, 1994. Google Scholar
  34. M. Randour, J.-F. Raskin, and O. Sankur. Variations on the Stochastic Shortest Path Problem. In Proc. 16th Int. Conf. on Verification, Model Checking, and Abstract Interpretation, volume 8931 of Lecture Notes in Computer Science, pages 1-18. Springer, 2015. Google Scholar
  35. W. Thomas. Automata on infinite objects. Handbook of Theoretical Computer Science, pages 133-191, 1990. Google Scholar
  36. Y. Velner, K. Chatterjee, L. Doyen, T.A. Henzinger, A. Rabinovich, and J.-F. Raskin. The complexity of multi-mean-payoff and multi-energy games. Information and Computation, 241:177-196, 2015. 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 Imprint Privacy Contact