research-article

Open access

Approximating Values of Generalized-Reachability Stochastic Games

Authors:

Krishnendu Chatterjee,

Jan Křetínský,

Maximilian Weininger,

Tobias WinklerAuthors Info & Claims

LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

Pages 102 - 115

https://doi.org/10.1145/3373718.3394761

Published: 08 July 2020 Publication History

Abstract

Simple stochastic games are turn-based 2½-player games with a reachability objective. The basic question asks whether one player can ensure reaching a given target with at least a given probability. A natural extension is games with a conjunction of such conditions as objective. Despite a plethora of recent results on the analysis of systems with multiple objectives, the decidability of this basic problem remains open. In this paper, we present an algorithm approximating the Pareto frontier of the achievable values to a given precision. Moreover, it is an anytime algorithm, meaning it can be stopped at any time returning the current approximation and its error bound.

References

[1]

Rajeev Alur and David L. Dill. 1994. A Theory of Timed Automata. Theor. Comput. Sci. 126, 2 (1994), 183--235.

Digital Library

[2]

Pranav Ashok, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretínský, and Tobias Meggendorfer. 2017. Value Iteration for Long-Run Average Reward in Markov Decision Processes. In CAV. 201--221. https://doi.org/10.1007/978-3-319-63387-9_10

[3]

Pranav Ashok, Krishnendu Chatterjee, Jan Kretinsky, Maximilian Weininger, and Tobias Winkler. 2020. Approximating Values of Generalized-Reachability Stochastic Games. CoRR abs/1908.05106 (2020).

[4]

Christel Baier, Marcus Daum, Clemens Dubslaff, Joachim Klein, and Sascha Klüppelholz. 2014. Energy-Utility Quantiles. In NASA Formal Methods. 285--299.

[5]

Christel Baier, Clemens Dubslaff, and Sascha Klüppelholz. 2014. Tradeoff analysis meets probabilistic model checking. In CSL-LICS. 1:1--1:10.

[6]

Christel Baier, Clemens Dubslaff, Sascha Klüppelholz, Marcus Daum, Joachim Klein, Steffen Märcker, and Sascha Wunderlich. 2014. Probabilistic Model Checking and Non-standard Multi-objective Reasoning. In FASE. 1--16.

[7]

Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking.

[8]

Nicolas Basset, Marta Z. Kwiatkowska, Ufuk Topcu, and Clemens Wiltsche. 2015. Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives. In TACAS (Lecture Notes in Computer Science), Vol. 9035. Springer, 256--271.

[9]

Nicolas Basset, Marta Z. Kwiatkowska, and Clemens Wiltsche. 2018. Compositional strategy synthesis for stochastic games with multiple objectives. Inf. Comput. 261, Part (2018), 536--587.

[10]

Tomás Brázdil, Václav Brozek, Krishnendu Chatterjee, Vojtech Forejt, and Antonín Kucera. 2014. Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. LMCS 10, 1 (2014). https://doi.org/10.2168/LMCS-10(1:13)2014

[11]

Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretínský, Marta Z. Kwiatkowska, David Parker, and Mateusz Ujma. 2014. Verification of Markov Decision Processes Using Learning Algorithms. In ATVA (Lecture Notes in Computer Science), Vol. 8837. Springer, 98--114.

[12]

Tomás Brázdil, Krishnendu Chatterjee, Vojtech Forejt, and Antonín Kucera. 2013. Trading Performance for Stability in Markov Decision Processes. In LICS. 331--340.

[13]

Romain Brenguier and Vojtech Forejt. 2016. Decidability Results for Multi-objective Stochastic Games. In ATVA (Lecture Notes in Computer Science), Vol. 9938. 227--243.

[14]

Romain Brenguier and Jean-François Raskin. 2015. Pareto Curves of Multidimensional Mean-Payoff Games. In CAV (2) (Lecture Notes in Computer Science), Vol. 9207. Springer, 251--267.

[15]

Krishnendu Chatterjee. 2007. Markov Decision Processes with Multiple Long-Run Average Objectives. In FSTTCS (Lecture Notes in Computer Science), Vol. 4855. Springer, 473--484.

[16]

Krishnendu Chatterjee and Laurent Doyen. 2016. Perfect-Information Stochastic Games with Generalized Mean-Payoff Objectives. In LICS. ACM, 247--256.

[17]

Krishnendu Chatterjee and Nathanaël Fijalkow. 2011. A reduction from parity games to simple stochastic games. In GandALF. 74--86. https://doi.org/10.4204/EPTCS.54.6

[18]

Krishnendu Chatterjee, Vojtech Forejt, and Dominik Wojtczak. 2013. Multi-objective Discounted Reward Verification in Graphs and MDPs. In LPAR. 228--242.

[19]

Krishnendu Chatterjee and Thomas A Henzinger. 2008. Value iteration. In 25 Years of Model Checking. Springer, 107--138.

[20]

Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, and Arjun Radhakrishna. 2010. Gist: A Solver for Probabilistic Games. In CAV. 665--669. https://doi.org/10.1007/978-3-642-14295-6_57

[21]

Krishnendu Chatterjee, Zuzana Kretínská, and Jan Kretínský. 2017. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. Logical Methods in Computer Science 13, 2 (2017).

[22]

Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, and Aistis Simaitis. 2013. PRISM-games: A Model Checker for Stochastic Multi-Player Games. In TACAS (Lecture Notes in Computer Science), Vol. 7795. Springer, 185--191.

[23]

Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, Aistis Simaitis, and Clemens Wiltsche. 2013. On Stochastic Games with Multiple Objectives. In MFCS (Lecture Notes in Computer Science), Vol. 8087. Springer, 266--277.

[24]

Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, Aistis Simaitis, and Clemens Wiltsche. 2013. On Stochastic Games with Multiple Objectives. Technical Report. 266--277 pages.

[25]

Taolue Chen, Marta Z. Kwiatkowska, Aistis Simaitis, and Clemens Wiltsche. 2013. Synthesis for Multi-objective Stochastic Games: An Application to Autonomous Urban Driving. In QEST. 322--337. https://doi.org/10.1007/978-3-642-40196-1_28

[26]

Chih-Hong Cheng, Alois Knoll, Michael Luttenberger, and Christian Buckl. 2011. GAVS+: An Open Platform for the Research of Algorithmic Game Solving. In ETAPS. 258--261. https://doi.org/10.1007/978-3-642-19835-9_22

[27]

Anne Condon. 1992. The complexity of stochastic games. Information and Computation 96, 2 (1992), 203--224.

Digital Library

[28]

Anne Condon. 1993. On Algorithms for Simple Stochastic Games. In Advances in Computational Complexity Theory, volume 13 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, 51--73.

[29]

Costas Courcoubetis and Mihalis Yannakakis. 1995. The Complexity of Probabilistic Verification. J. ACM 42, 4 (July 1995), 857--907.

Digital Library

[30]

Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis. 2008. Multi-Objective Model Checking of Markov Decision Processes. Logical Methods in Computer Science 4, 4 (2008).

[31]

J.A. Filar, D. Krass, and K.W Ross. 1995. Percentile performance criteria for limiting average Markov decision processes. Automatic Control, IEEE Transactions on 40, 1 (Jan 1995), 2--10.

[32]

Vojtech Forejt, Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. 2011. Quantitative Multi-objective Verification for Probabilistic Systems. In TACAS. 112--127. https://doi.org/10.1007/978-3-642-19835-9_11

[33]

Vojtech Forejt, Marta Z. Kwiatkowska, and David Parker. 2012. Pareto Curves for Probabilistic Model Checking. In ATVA (Lecture Notes in Computer Science), Vol. 7561. Springer, 317--332.

[34]

Christoph Haase, Stefan Kiefer, and Markus Lohrey. 2017. Computing quantiles in Markov chains with multi-dimensional costs. In LICS. 1--12.

[35]

Serge Haddad and Benjamin Monmege. 2018. Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735 (2018), 111--131.

[36]

A. Hatcher. 2002. Algebraic Topology. Cambridge University Press. https://books.google.de/books?id=BjKs86kosqgC

[37]

Edon Kelmendi, Julia Krämer, Jan Kretínský, and Maximilian Weininger. 2018. Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm. In CAV. https://doi.org/10.1007/978-3-319-96145-3_36

[38]

Marta Kwiatkowska, David Parker, and Clemens Wiltsche. 2016. PRISM-Games 2.0: A Tool for Multi-objective Strategy Synthesis for Stochastic Games. In TACAS (Lecture Notes in Computer Science), Vol. 9636. Springer, 560--566.

[39]

Marta Kwiatkowska, David Parker, and Clemens Wiltsche. 2018. PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives. STTT 20, 2 (2018), 195--210.

Digital Library

[40]

Marta Z. Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In CAV (Lecture Notes in Computer Science), Vol. 6806. Springer, 585--591.

[41]

H. Brendan Mcmahan, Maxim Likhachev, and Geoffrey J. Gordon. 2005. Bounded real-time dynamic programming: RTDP with monotone upper bounds and performance guarantees. In ICML 05. 569--576.

[42]

Christos H. Papadimitriou and Mihalis Yannakakis. 2000. On the Approximability of Trade-offs and Optimal Access of Web Sources. In FOCS. IEEE Computer Society, 86--92.

[43]

Martin L. Puterman. 2014. Markov decision processes: Discrete stochastic dynamic programming. John Wiley & Sons.

[44]

Mickael Randour, Jean-François Raskin, and Ocan Sankur. 2015. Percentile Queries in Multi-dimensional Markov Decision Processes. In CAV (1) (Lecture Notes in Computer Science), Vol. 9206. Springer, 123--139.

[45]

Mickael Randour, Jean-François Raskin, and Ocan Sankur. 2017. Percentile queries in multi-dimensional Markov decision processes. Formal Methods in System Design 50, 2-3 (2017), 207--248. https://doi.org/10.1007/s10703-016-0262-7

Digital Library

[46]

María Svorenová and Marta Kwiatkowska. 2016. Quantitative verification and strategy synthesis for stochastic games. Eur. J. Control 30 (2016), 15--30. https://doi.org/10.1016/j.ejcon.2016.04.009

[47]

Yaron Velner. 2015. Robust Multidimensional Mean-Payoff Games are Undecidable. In FoSSaCS. Springer, 312--327.

Cited By

Main JRandour M(2024)Different Strokes in Randomised Strategies: Revisiting Kuhn's Theorem under Finite-Memory AssumptionsInformation and Computation10.1016/j.ic.2024.105229(105229)Online publication date: Oct-2024
https://doi.org/10.1016/j.ic.2024.105229
Chatterjee KKatoen JMohr SWeininger MWinkler T(2024)Stochastic games with lexicographic objectivesFormal Methods in System Design10.1007/s10703-023-00411-463:1-3(40-80)Online publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1007/s10703-023-00411-4
Berthon RKatoen JWinkler T(2024)Markov Decision Processes with Sure Parity and Multiple Reachability ObjectivesReachability Problems10.1007/978-3-031-72621-7_14(203-220)Online publication date: 25-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-72621-7_14
Show More Cited By

Index Terms

Approximating Values of Generalized-Reachability Stochastic Games
1. Mathematics of computing
  1. Probability and statistics
2. Theory of computation
  1. Logic
    1. Verification by model checking
  2. Theory and algorithms for application domains
    1. Algorithmic game theory and mechanism design
      1. Algorithmic game theory

Recommendations

Strategy improvement for concurrent reachability and turn-based stochastic safety games

We consider concurrent games played on graphs. At every round of a game, each player simultaneously and independently selects a move; the moves jointly determine the transition to a successor state. Two basic objectives are the safety objective to stay ...
A survey of partial-observation stochastic parity games

We consider two-player zero-sum stochastic games on graphs with -regular winning conditions specified as parity objectives. These games have applications in the design and control of reactive systems. We survey the complexity results for the problem of ...
Concurrent reachability games

We consider concurrent two-player games with reachability objectives. In such games, at each round, player 1 and player 2 independently and simultaneously choose moves, and the two choices determine the next state of the game. The objective of player 1 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

July 2020

986 pages

ISBN:9781450371049

DOI:10.1145/3373718

Conference Chairs:
Holger Hermanns,
Lijun Zhang,
Naoki Kobayashi,
General Chair:
Dale Miller

Copyright © 2020 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation
EACSL: European Association for Computer Science Logic
IEEE-CS\DATC: IEEE Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 July 2020

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Funding Sources

Conference

LICS '20

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science

July 8 - 11, 2020

Saarbrücken, Germany

Acceptance Rates

LICS '20 Paper Acceptance Rate 69 of 174 submissions, 40%;

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
551
Total Downloads

Downloads (Last 12 months)118
Downloads (Last 6 weeks)20

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Main JRandour M(2024)Different Strokes in Randomised Strategies: Revisiting Kuhn's Theorem under Finite-Memory AssumptionsInformation and Computation10.1016/j.ic.2024.105229(105229)Online publication date: Oct-2024
https://doi.org/10.1016/j.ic.2024.105229
Chatterjee KKatoen JMohr SWeininger MWinkler T(2024)Stochastic games with lexicographic objectivesFormal Methods in System Design10.1007/s10703-023-00411-463:1-3(40-80)Online publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1007/s10703-023-00411-4
Berthon RKatoen JWinkler T(2024)Markov Decision Processes with Sure Parity and Multiple Reachability ObjectivesReachability Problems10.1007/978-3-031-72621-7_14(203-220)Online publication date: 25-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-72621-7_14
Watanabe KVegt MJunges SHasuo I(2024)Compositional Value Iteration with Pareto CachingComputer Aided Verification10.1007/978-3-031-65633-0_21(467-491)Online publication date: 26-Jul-2024
https://doi.org/10.1007/978-3-031-65633-0_21
Křetínský JMeggendorfer TWeininger M(2023)Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175771(1-14)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175771
Eisentraut JKelmendi EKřetínský JWeininger M(2022)Value iteration for simple stochastic gamesInformation and Computation10.1016/j.ic.2022.104886285:PBOnline publication date: 15-Jun-2022
https://dl.acm.org/doi/10.1016/j.ic.2022.104886
Křetínský JRamneantu ESlivinskiy AWeininger M(2022)Comparison of algorithms for simple stochastic gamesInformation and Computation10.1016/j.ic.2022.104885289:PBOnline publication date: 1-Nov-2022
https://dl.acm.org/doi/10.1016/j.ic.2022.104885
Winkler TWeininger M(2021)Stochastic Games with Disjunctions of Multiple ObjectivesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.346.6346(83-100)Online publication date: 17-Sep-2021
https://doi.org/10.4204/EPTCS.346.6
Weininger MGrover KMisra SKřetínský J(2021)Guaranteed Trade-Offs in Dynamic Information Flow Tracking Games2021 60th IEEE Conference on Decision and Control (CDC)10.1109/CDC45484.2021.9683447(3786-3793)Online publication date: 14-Dec-2021
https://dl.acm.org/doi/10.1109/CDC45484.2021.9683447
Kwiatkowska MNorman GParker DSantos G(2021)Automatic verification of concurrent stochastic systemsFormal Methods in System Design10.1007/s10703-020-00356-y58:1-2(188-250)Online publication date: 22-Jan-2021
https://dl.acm.org/doi/10.1007/s10703-020-00356-y
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents