Pith. sign in

REVIEW 4 major objections 4 minor 49 references

Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games

T0 review · 4 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Value iteration on concurrent stochastic games can now be stopped with a formally guaranteed ε-accuracy, by running a converging over-approximation alongside the usual under-approximation.

desk verdict First real candidate for a sound stopping criterion for value iteration on concurrent stochastic games, but the central convergence proof has a genuine domain bug that must be fixed before the termination claim is established. read the letter →

arxiv 2505.21087 v2 pith:W34UOZSI submitted 2025-05-27 cs.LO cs.AIcs.MA

Marta Grobelna , Jan Křetínský , Maximilian Weininger This is my paper
classification cs.LOcs.AIcs.MA MSC 91A1591A0591A50
keywords concurrentstochasticgamesvalueiterationboundedstoppingcriterionreachabilityandsafetyendcomponentsover-approximationformalverification
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper tackles a long-standing gap in the practical solution of concurrent stochastic games: standard value iteration converges to the true value only in the limit, and its usual stopping test, two consecutive iterates being close, can stop arbitrarily far from the answer. The authors prove that a second, over-approximating sequence can be made to converge downward to the same value, so the two bounds can be forced within any prescribed ε. If correct, this gives the first sound stopping criterion for value iteration on such games and turns it into an anytime algorithm for reachability and safety objectives. Earlier attempts failed because cyclic structures called end components inflate naive upper bounds; the paper isolates the problematic ones and removes their influence.

What carries the argument

The load-bearing object is the bloated end component (BEC): a set of states that can trap play forever under some strategy pair, where at every state Player R has a hazardous strategy, locally optimal, non-leaving, and weakly dominating all leaving strategies, so the Bellman update rewards staying and the naive upper bound never falls. Around this the paper builds strategy-level definitions of leaving, staying, trapping, and deflating strategies, and defines the exiting sub-game and the best exit value as the pressure coming from outside the component. Algorithm 3 finds maximal BECs, deflates every state's upper bound to the best exit value, removes the best exits, and recurses on the remaining maximal end components, exposing a hierarchical ordering of exits. The convergence argument rests on the Bellman operator B and the deflation operator D being order-preserving and Scott-continuous on the restricted domain of valid upper bounds, so the combined operator (D ∘ B) has a greatest fixpoint by lattice theory.

What would settle it

Take the concrete game of Fig. 2 with α = 0.2, β = 0.7, γ = 0.9 and ε = 0.001 from Example 40 and trace the iterates of Algorithm 1 with Algorithm 3. If at any iteration the deflated upper bound drops below the true value V_R(s) for some state, or if U_k fails to approach V_R from above, for instance by stagnating at a value strictly above the least fixpoint of the Bellman operator, then Theorem 37 is false. More generally, any CSG where (D ∘ B) does not converge to a fixpoint on the valid-upper-bound domain would falsify the proof.

Watch

Extended reading notes

Core claim

The central claim is Theorem 37: for every finite concurrent stochastic reachability or safety game, Algorithm 1 with the deflation routine of Algorithm 3 produces a monotone sequence of lower bounds L and upper bounds U that both converge to the true value V_R, and the algorithm terminates for every ε > 0 with U − L ≤ ε. Since the lower bounds converge from below by classical value iteration and the upper bounds are proven sound, never falling below V_R, the stopping condition inherits a guaranteed ε-precision. The proof identifies bloated end components, end components in which every state has a hazardous locally optimal strategy that keeps play inside, as the unique cause of upper-bound non-convergence, and shows that deflating each such component to its best exit value, recursively through the end-component hierarchy, forces the upper bound to continue decreasing. The paper presents this as the first valid stopping criterion for CSGs, superseding earlier attempts that were invalidated by counterexamples.

Load-bearing premise

Everything hinges on the deflation step being monotone and continuous on the special upper bounds the algorithm actually produces, even though the same deflation operator is not monotone on arbitrary valuations; if that restricted continuity fails in some game, the upper-bound sequence need not converge to a fixpoint and termination is lost.

Editorial extensions

If this is right

  • Every run of Algorithm 1 with Algorithm 3 can be stopped with a certificate: when the loop exits, the true value is guaranteed to lie in the reported interval of width at most ε.
  • The criterion applies to safety objectives as well as reachability, because the safety value is the dual of the reachability value, V_S = 1 − V_R, so one approximation run covers both.
  • Value iteration on concurrent stochastic games becomes an anytime algorithm: the interval [L_k, U_k] always contains the true value and shrinks monotonically to a point.
  • The recursive removal of best exits gives a structural description of how values inside an end component are determined by the values of its exits, which is what keeps deflation sound.
  • Games that converge quickly can be detected and stopped early, avoiding the doubly-exponential worst-case iteration count that a fixed a-priori bound would require.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A direct testable extension the paper does not run is an implementation of the scheme on standard concurrent-game benchmarks; the authors note that implementation is future work, but the stopping criterion is exactly what would make such an experiment meaningful.
  • The same strategy-set treatment of exits should transfer to other quantitative objectives on concurrent games, such as discounted or mean-payoff payoffs, where leaving a component is also a matter of vanishingly small mixing probabilities rather than a single action.
  • Because the soundness proof hinges on deflation being monotone only on valid upper bounds, any future optimization or parallelization of DEFLATE must preserve that invariant; breaking it would reintroduce the failure mode of earlier attempts.
  • The hierarchical decomposition of end components by best exits exposes a structural invariant, values inside a component are capped by values of its exits, that could inform strategy synthesis rather than only value approximation.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper introduces bounded value iteration for concurrent stochastic games (CSGs) with reachability and safety objectives. Standard value iteration computes an under-approximation but lacks a stopping criterion that guarantees a prescribed precision. The authors propose to complement the lower sequence with a convergent upper sequence, using a deflation operator that identifies and reduces so-called bloated end components (BECs), defined via new strategy-based notions of hazardous, trapping, and deflating strategies. The main claim (Theorem 37) is that the resulting algorithm produces monotone under- and over-approximations and terminates for every epsilon > 0. The proof of the central convergence lemma (Lemma 52) is the focus of this report.

Significance. If Theorem 37 is correct, the paper solves an open problem: it gives value iteration for CSGs a sound stopping criterion, a practically relevant improvement over the existential-theory-of-reals approach. The manuscript also provides useful conceptual contributions, including a careful strategy-based definition of BECs, a recursive deflation scheme, and concrete counter-examples to two earlier stopping-criterion proposals. The paper is clearly written and the technical apparatus is extensive. However, the central convergence proof contains a load-bearing gap: Lemma 52 claims Scott-continuity of the deflation operator D on a domain where D is not even monotone, as the authors themselves note in Remark 32. The termination proof therefore rests on an unproved fixpoint claim.

major comments (4)
  1. [Appendix C-D, Lemma 52] The proof of Lemma 52 explicitly sets out to show that D is Scott-continuous on the full domain V=[0,1]^|S|x[0,1]^|S|. This is impossible: Scott-continuity implies monotonicity, and Remark 32 states that D is not monotone on arbitrary valuations, with a counter-example in Appendix B-C. The proof must be restricted to valid upper bounds (Definition 33) or to the specific directed chain of iterates generated by (D∘B) from U0. As written, the proof does not establish the continuity required for the Kleene fixpoint argument, so the conclusion that lim_k (D∘B)^k(U0) is a fixpoint of D∘B is not justified.
  2. [Appendix C-D, Lemma 52] In the chain of equalities, the sets R'(s) and S'(s) are defined once using HazardsupD(X,s) and TrapsupD(X,s), where supD is the supremum of the directed set D. These fixed sets are then used for every d in D when the expression is identified with exitVal_d(X,s'). However, Definition 27 defines exitVal_d in terms of Hazard_d(X,s) and Trap_d(X,s), which can vary with d. Consequently, the equality `... = sup_{d in D} max_{s' in X} exitVal_d(X,s')` does not follow, and D(supD)=sup_d D(d) is not established.
  3. [Appendix C-D, Lemma 52, final step] The final equality `min(supD(s), sup_d bestExitVal_d(X)) = sup_d min(d(s), bestExitVal_d(X))` is not a consequence of Scott-continuity of min. The two arguments are coupled through the same d, and the CPO order on the upper-bound projection is the reverse pointwise order, which makes the interchange delicate. Without a valid interchange, the proof of D(supD)=sup D(D) fails, and the application of the fixpoint theorem is unsupported.
  4. [Theorem 37, proof] The proof asserts that the set C of states with maximal difference Delta(s)=U*(s)-VR(s) contains a BEC, and then considers a bottom BEC inside C. This is a load-bearing step for the contradiction argument, but no proof or reference is given in the proof of Theorem 37. The contraposition of Theorem 9 alone does not yield the existence of a BEC inside C; it only yields a BEC somewhere in S\(T∪WS). This step should be proven explicitly or derived from a cited lemma.
minor comments (4)
  1. [Appendix C-D, Lemma 52] There are two inconsistencies in the setup of the CPO: the bottom element is first defined as (0-vector, 1-vector) and then as (L0, U0), and the notation supD is used both for the CPO supremum and for pointwise numeric suprema in the same chain of equalities. These should be disambiguated.
  2. [Appendix C-D, Lemma 52] The reference to the fixpoint theorem is spelled 'Kleen's Fixpoint Theorem'; the correct spelling is Kleene.
  3. [Appendix B-C, Example 41] The example states that {s0,s1} is an EC for the game in Fig. 5, but the figure uses placeholders alpha, beta, gamma for leaving valuations; the description would be clearer if the possible staying and leaving transitions were listed explicitly.
  4. [Algorithm 2] In Line 2, 'B==CorB==emptyset' should be formatted as 'B==C or B==emptyset' for readability.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the CSG stopping criterion is derived from new definitions and operator-theoretic arguments, not from the target result or fitted data.

full rationale

The paper's central claim (Theorem 37) is proved by constructing a deflation operator D and showing that (D∘B) converges to a fixpoint; the algorithm takes only the game and ε as input, with no fitted parameters or data-dependent calibration, so the claimed stopping criterion is not forced by construction. The definitions of hazardous, trapping, deflating, and best-exit strategies (Defs. 16, 24, 25, 27-28) are given in terms of the current valuation and matrix-game values, and the soundness and order-preservation lemmas (Lem. 35-36) are proved rather than assumed. The paper does cite the authors' own prior work ([18], [29]) for the turn-based and MDP cases, but the concurrent generalization is argued in the text: Theorem 9 is proved in App. C-A, Theorem 21 in App. C-B, and Lemma 52 in App. C-D, so the load-bearing content is not reduced to a self-citation. The paper itself flags that D is not monotone on arbitrary valuations (Remark 32, App. B-C) and restricts to valid upper bounds; whether Lemma 52's Scott-continuity proof is correct, in particular the min/sup interchange and the dependence of R'(s) and S'(s) on sup D, is a proof-correctness concern, not circularity, since an unjustified interchange would be an error in the derivation rather than an equivalence of the conclusion to an input. For these reasons, no circular step can be exhibited.

Assumptions & free parameters 0 free parameters · 5 assumptions · 1 invented entities

The paper introduces no free parameters and no fitted quantities. Its technical machinery rests on standard game-theoretic and lattice-theoretic background, plus the paper-specific assumption that D is continuous on valid upper bounds, which is the main unresolved point.

assumptions (5)
  • domain assumption Concurrent stochastic games are determined and memoryless randomized strategies suffice for reachability and safety values.
    Invoked throughout Section II and cited to [21] and [16]; standard in the field.
  • standard math The minimax theorem for bilinear functions holds, allowing swap of inf and sup over compact strategy sets.
    Used in Lemma 48 Claim 2 (Appendix C-A) to prove continuity of the Bellman operator.
  • standard math Kleene and fixpoint theorems for continuous order-preserving maps on complete partial orders apply.
    Used in Lemma 48 and Lemma 52; cited to [13].
  • ad hoc to paper The deflation operator D is Scott-continuous on the relevant domain of valid upper bounds.
    This is the load-bearing premise of Lemma 52; the proof does not clearly restrict the domain, conflicting with Remark 32.
  • standard math MEC decomposition algorithms for CSGs are available and correct.
    Relied on in Algorithms 1-3; cited to [2], [12], and [46].
invented entities (1)
  • Bloated End Component (BEC) independent evidence
    purpose: A set of states inside an end component where locally optimal but non-leaving strategies prevent the naive upper bound from converging; deflating BECs yields a convergent over-approximation.
    The paper gives a characterization theorem (Theorem 21) connecting non-convergence to BECs, and the definitions are checkable on concrete games; no external empirical evidence is provided.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games." pith.science (2026). https://pith.science/paper/W34UOZSI

@misc{pith2026250521087,
  author       = {Pith},
  title        = {Pith review of: Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/W34UOZSI}},
  note         = {Machine review of arXiv:2505.21087}
}
abstract

We consider two-player zero-sum concurrent stochastic games (CSGs) played on graphs with reachability and safety objectives. These include degenerate classes such as Markov decision processes or turn-based stochastic games, which can be solved by linear or quadratic programming; however, in practice, value iteration (VI) outperforms the other approaches and is the most implemented method. Similarly, for CSGs, this practical performance makes VI an attractive alternative to the standard theoretical solution via the existential theory of reals. VI starts with an under-approximation of the sought values for each state and iteratively updates them, traditionally terminating once two consecutive approximations are $\epsilon$-close. However, this stopping criterion lacks guarantees on the precision of the approximation, which is the goal of this work. We provide bounded (a.k.a. interval) VI for CSGs: it complements standard VI with a converging sequence of over-approximations and terminates once the over- and under-approximations are $\epsilon$-close.

Figures

Figures reproduced from arXiv: 2505.21087 by the authors.

Figure 1
Figure 1. Example CSG called Hide-Run-or-Slip. and ΓS (s0 ) := {wait,throw}, s0 is the initial state denoted by the arrow with no predecessor state, and T := {shome}. The game has the following intuitive interpretation: Player R wants to get home without getting wet. Player S has a single snowball and can make player R wet by throwing it at player R. If player R runs and player S throws the ball, player R gets wet. If player … view at source ↗
Figure 2
Figure 2. CSG with non-single-state EC. The clouds represent the irrelevant parts of the game. 14 [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗
Figure 3
Figure 3. The resulting game after removing s2 from the game illustrated in [PITH_FULL_IMAGE:figures/full_fig_p015_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: The resulting game after removing s1 from the game illustrated in [PITH_FULL_IMAGE:figures/full_fig_p016_4.png]
Figure 5
Figure 5. Figure 5: Monotonicity is not guaranteed in general. [PITH_FULL_IMAGE:figures/full_fig_p016_5.png]
Figure 6
Figure 6. Figure 6: Counter example for the BVI provided in [7]. Case (ii) In this case it holds that TrapU⋆ (X ′ , s) = ∅. Thus, Player S prefers strategies that are leaving with respect to HazardU⋆ (X , s). Since X ′ is a bottom BEC at least one successor state does not belong to X . Th…

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

49 extracted references · 48 canonical work pages

  1. [7]

    Termination criteria for solving concurrent safety and reachability games

    Krishnendu Chatterjee, Luca de Alfaro, and Thomas A Henzinger. Termination criteria for solving concurrent safety and reachability games. InProceedings of the twentieth annual ACM-SIAM symposium on Discrete algorithms, pages 197–206. SIAM, 2009

    work page 2009

  2. [19]

    Stopping Criteria for Value and Strategy Iteration on Concurrent Stochastic Reachability Games, 2019

    Julia Eisentraut, Jan K ˇret´ınsk´y, and Alexej Rotar. Stopping Criteria for Value and Strategy Iteration on Concurrent Stochastic Reachability Games, 2019

    work page 2019

  3. [1]

    Value Iteration for Long-Run Average Reward in Markov Decision Processes

    Pranav Ashok, Krishnendu Chatterjee, Przemysław Daca, Jan K ˇret´ınsk´y, and Tobias Meggendorfer. Value Iteration for Long-Run Average Reward in Markov Decision Processes. In Rupak Majumdar and Viktor Kun ˇcak, editors,Computer Aided Verification. Springer International Publishing, 2017

    work page 2017

  4. [2]

    MIT Press, April 2008

    Christel Baier and Joost-Pieter Katoen.Principles of Model Checking. MIT Press, April 2008

    work page 2008

  5. [3]

    Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes

    Christel Baier, Joachim Klein, Linda Leuschner, David Parker, and Sascha Wunderlich. Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. In Rupak Majumdar and Viktor Kunˇcak, editors,Computer Aided Verification. Springer International Publishing, 2017

    work page 2017

  6. [4]

    Subgame Optimal Strategies in Finite Concurrent Games with Prefix-Independent Objectives

    Benjamin Bordais, Patricia Bouyer, and St ´ephane Le Roux. Subgame Optimal Strategies in Finite Concurrent Games with Prefix-Independent Objectives. In Orna Kupferman and Pawel Sobocinski, editors,Founda- tions of Software Science and Computation Structures, pages 541–560. Springer Nature Switzerland, 2023

    work page 2023

  7. [5]

    Verification of Markov decision processes using learning algorithms

    Tom´aˇs Br ´azdil, Krishnendu Chatterjee, Martin Chmelik, V ojt ˇech Forejt, Jan Kˇret´ınsk`y, Marta Kwiatkowska, David Parker, and Mateusz Ujma. Verification of Markov decision processes using learning algorithms. In International Symposium on Automated Technology for Verification and Analysis, pages 98–114. Springer, 2014

    work page 2014

  8. [6]

    Verification of Markov Decision Processes Using Learning Algorithms

    Tom´aˇs Br ´azdil, Krishnendu Chatterjee, Martin Chmel ´ık, V ojtˇech Forejt, Jan Kˇret´ınsk´y, Marta Kwiatkowska, David Parker, and Mateusz Ujma. Verification of Markov Decision Processes Using Learning Algorithms. In Franck Cassez and Jean-Fran c ¸ois Raskin, editors,Automated Technology for Verification and Analysis. Springer International Publishing, 2014

    work page 2014

Show all 49 references
  1. [8]

    Henzinger

    Krishnendu Chatterjee, Luca De Alfaro, and Thomas A. Henzinger. Qualitative concurrent parity games.ACM Transactions on Computational Logic, July 2011

    2011

  2. [9]

    Strategy improvement for concurrent reachability and safety games

    Krishnendu Chatterjee, Luca de Alfaro, and Thomas A Henzinger. Strategy improvement for concurrent reachability and safety games. arXiv preprint arXiv:1201.2834, 2012

    2012 arXiv

  3. [10]

    Strat- egy improvement for concurrent reachability and turn-based stochastic safety games.Journal of computer and system sciences, 79(5):640–657, 2013

    Krishnendu Chatterjee, Luca de Alfaro, and Thomas A Henzinger. Strat- egy improvement for concurrent reachability and turn-based stochastic safety games.Journal of computer and system sciences, 79(5):640–657, 2013

    2013

  4. [11]

    Henzinger

    Krishnendu Chatterjee and Thomas A. Henzinger. Value Iteration. In Orna Grumberg and Helmut Veith, editors,25 Years of Model Checking: History, Achievements, Perspectives. Springer, 2008

    2008

  5. [12]

    The complexity of probabilistic verification.Journal of the ACM, 42, July 1995

    Costas Courcoubetis and Mihalis Yannakakis. The complexity of probabilistic verification.Journal of the ACM, 42, July 1995

    1995

  6. [13]

    B. A. Davey and H. A. Priestley.Introduction to Lattices and Order. Cambridge University Press, Cambridge, 2 edition, 2002

    2002

  7. [14]

    How to specify and verify the long-run average behaviour of probabilistic systems

    Luca De Alfaro. How to specify and verify the long-run average behaviour of probabilistic systems. InProceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No. 98CB36226), pages 454–465. IEEE, 1998

    1998

  8. [15]

    Concurrent omega-regular games

    Luca de Alfaro and Thomas A Henzinger. Concurrent omega-regular games. InLogic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on, pages 141–154. IEEE, 2000

    2000

  9. [16]

    Concurrent reachability games.Theoretical Computer Science, 2007

    Luca De Alfaro, Thomas A Henzinger, and Orna Kupferman. Concurrent reachability games.Theoretical Computer Science, 2007

    2007

  10. [17]

    Quantitative solution of omega- regular games.Journal of Computer and System Sciences, 68(2):374 – 397, 2004

    Luca de Alfaro and Rupak Majumdar. Quantitative solution of omega- regular games.Journal of Computer and System Sciences, 68(2):374 – 397, 2004. Special Issue on STOC 2001

    2004

  11. [18]

    Value iteration for simple stochastic games: Stopping criterion and learning algorithm.Information and Computation, 2022

    Julia Eisentraut, Edon Kelmendi, Jan K ˇret´ınsk´y, and Maximilian Weininger. Value iteration for simple stochastic games: Stopping criterion and learning algorithm.Information and Computation, 2022

    2022

  12. [20]

    Recursive Concurrent Stochastic Games.Logical Methods in Computer Science, V olume 4, Issue 4, November 2008

    Kousha Etessami and Mihalis Yannakakis. Recursive Concurrent Stochastic Games.Logical Methods in Computer Science, V olume 4, Issue 4, November 2008

    2008

  13. [21]

    Everett.RECURSIVE GAMES, pages 47–78

    H. Everett.RECURSIVE GAMES, pages 47–78. Princeton University Press, 1957

    1957

  14. [22]

    Approximating the Value of a Concurrent Reachability Game in the Polynomial Time Hierarchy

    Søren Kristoffer Stiil Frederiksen and Peter Bro Miltersen. Approximating the Value of a Concurrent Reachability Game in the Polynomial Time Hierarchy. Springer, 2013

    2013

  15. [23]

    Interval iteration algorithm for mdps and imdps.Theoretical Computer Science, 735:111–131, 2018

    Serge Haddad and Benjamin Monmege. Interval iteration algorithm for mdps and imdps.Theoretical Computer Science, 735:111–131, 2018

    2018

  16. [24]

    Interval Iteration Algorithm for MDPs and IMDPs.Theoretical Computer Science, 2018

    Serge Haddad and Benjamin Monmege. Interval Iteration Algorithm for MDPs and IMDPs.Theoretical Computer Science, 2018

    2018

  17. [25]

    The Complexity of Solving Reachability Games Using Value and Strategy Iteration.Theory of Computing Systems, 55, 2014

    Kristoffer Arnsfelt Hansen, Rasmus Ibsen-Jensen, and Peter Bro Mil- tersen. The Complexity of Solving Reachability Games Using Value and Strategy Iteration.Theory of Computing Systems, 55, 2014

    2014

  18. [26]

    Tsigaridas

    Kristoffer Arnsfelt Hansen, Michal Koucky, Niels Lauritzen, Peter Bro Miltersen, and Elias P. Tsigaridas. Exact algorithms for solving stochastic games: Extended abstract. InProceedings of the Forty-Third Annual ACM Symposium on Theory of Computing, 2011

    2011

  19. [27]

    A Practitioner’s Guide to MDP Model Checking Algorithms

    Arnd Hartmanns, Sebastian Junges, Tim Quatmann, and Maximilian Weininger. A Practitioner’s Guide to MDP Model Checking Algorithms. In Sriram Sankaranarayanan and Natasha Sharygina, editors,Tools and Algorithms for the Construction and Analysis of Systems. Springer Nature Switz...

    2023

  20. [28]

    Hillier and Gerald J

    Frederick S. Hillier and Gerald J. Lieberman.Introduction to Operations Research. McGraw-Hill Higher Education, 2010

    2010

  21. [29]

    Stop- ping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives

    Jan Kˇret´ınsk´y, Tobias Meggendorfer, and Maximilian Weininger. Stop- ping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives. In2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2023

    2023

  22. [30]

    Comparison of algorithms for simple stochastic games

    Jan Kˇret´ınsk´y, Emanuel Ramneantu, Alexander Slivinskiy, and Maximil- ian Weininger. Comparison of algorithms for simple stochastic games. Information and Computation, 2022

    2022

  23. [31]

    P. R. Kumar and T. H. Shiau. Existence of Value and Randomized Strategies in Zero-Sum Discrete-Time Stochastic Dynamic Games.SIAM Journal on Control and Optimization, 19, 1981

    1981

  24. [32]

    Automated verification of concurrent stochastic games

    Marta Kwiatkowska, Gethin Norman, David Parker, and Gabriel Santos. Automated verification of concurrent stochastic games. InInternational Conference on Quantitative Evaluation of Systems, pages 223–239. Springer, 2018

    2018

  25. [33]

    PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time

    Marta Kwiatkowska, Gethin Norman, David Parker, and Gabriel Santos. PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification. Springer International Publishing, 2020

    2020

  26. [34]

    Donald A. Martin. The determinacy of blackwell games. 1998

    1998

  27. [35]

    Cambridge University Press, June 2020

    Michael Maschler, Shmuel Zamir, and Eilon Solan.Game Theory. Cambridge University Press, June 2020

    2020

  28. [36]

    Non-Cooperative Games

    John Nash. Non-Cooperative Games. 1951

    1951

  29. [37]

    John F. Nash. Equilibrium points in n-person games. 1950

    1950

  30. [38]

    New algorithms for solving zero-sum stochastic games.Mathematics of Operations Research, 46(1):255–267, 2021

    Miquel Oliu-Barton. New algorithms for solving zero-sum stochastic games.Mathematics of Operations Research, 46(1):255–267, 2021

    2021

  31. [39]

    Parthasarathy

    T. Parthasarathy. Discounted, positive, and noncooperative stochastic games.International Journal of Game Theory, 2(1):25–37, Dec 1973

    1973

  32. [40]

    Grant Olney Passmore and Paul B. Jackson. Combined decision techniques for the existential theory of the reals. InCalculemus/MKM, volume 5625 ofLecture Notes in Computer Science, pages 122–137. Springer, 2009

    2009

  33. [41]

    Puterman.Markov Decision Processes: Discrete Stochastic Dynamic Programming

    Martin L. Puterman.Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, 2009

    2009

  34. [42]

    T. E. S. Raghavan and J. A. Filar. Algorithms for stochastic games — A survey.Zeitschrift f ¨ur Operations Research, 35(6):437–472, 1991

    1991

  35. [43]

    G. H. R. Santos.Automatic Verification and Strategy Synthesis for Zero- Sum and Equilibria Properties of Concurrent Stochastic Games. PhD thesis, University of Oxford, 2020

    2020

  36. [44]

    Outline of a Mathematical Theory of Computation

    Dana Scott. Outline of a Mathematical Theory of Computation. Kiberneticheskij Sbornik. Novaya Seriya, 14, January 1977

    1977

  37. [45]

    Minimax Theorems and Their Proofs

    Stephen Simons. Minimax Theorems and Their Proofs. In Ding-Zhu Du and Panos M. Pardalos, editors,Minimax and Applications. Springer US, 1995

    1995

  38. [46]

    no state in X can depend on the outside

    Anton Wijs, Joost-Pieter Katoen, and Dragan Bo ˇsnaˇcki. Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components.Formal Methods in System Design, 48(3), June 2016. 13 APPENDIXA FURTHERDEFINITIONS ANDCONCEPTS A. Solving M...

    2016

  39. [47]

    We prove that X is a maximal BEC inCvia structural induction

    Direction “⇒” Let X ⊆Cbe a non-empty set of states and let X ∈FIND MBEC(G,C,U) . We prove that X is a maximal BEC inCvia structural induction. Basis step: Let B :={s∈C|Hazard U (C, s)̸=∅} . The recursive function FIND MBECs has two base cases that we consider now. If B=C holds...

  40. [48]

    We need to show that X ∈FIND MBEC(G,C,U) holds

    Direction “⇐” Let ∅ ̸=X ⊆Cbe a maximal BEC in the MECC . We need to show that X ∈FIND MBEC(G,C,U) holds. Let B :={s∈C|Hazard U (C, s)̸=∅} . Assume towards a contradiction that X/∈FIND MBEC(G,C,U) . As X is a maximal BEC in C, it must be true that B :={s∈C|Hazard U (C, s)̸=∅} ̸...

  41. [49]

    3) the set {s4, s3} does not constitute a BEC for the valuation U(s4) =U(s 3) =U(s 1) = 1 and U(s2) = 0

    In our algorithm (Alg. 3) the set {s4, s3} does not constitute a BEC for the valuation U(s4) =U(s 3) =U(s 1) = 1 and U(s2) = 0. Consequently, the while-loop of Alg. 3, which is responsible for deflating, is not executed and thus the values of all states are updated only using ...

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.