日本ソフトウェア科学会第 37 回大会 (2020 年度) 講演論文集

Widest Paths and Global Propagation in
Bounded Value Iteration for Stochastic Games
Kittiphon Phalakarn, Toru Takisaka, Thomas Haas, Ichiro Hasuo
Solving stochastic games with the reachability objective is a fundamental problem, especially in quantitative
verification and synthesis. For this purpose, bounded value iteration (BVI) attracts attention as an eﬃcient
iterative method. However, BVI’s performance is often impeded by costly end component (EC) computationthat is needed to ensure convergence. Our contribution is a novel BVI algorithm that conducts, in addition
to local propagation by the Bellman update that is typical of BVI, global propagation of upper bounds
that is not hindered by ECs. To conduct global propagation in a computationally tractable manner, weconstruct a weighted graph and solve the widest path problem in it. Our experiments show the algorithm’s
performance advantage over the previous BVI algorithms that rely on EC computation.

to a designated target state.

1 Introduction

Stochastic games are a fundamental construct

1. 1 Stochastic Game (SG)in theoretical computer science, especially in the

A stochastic game [13] is a two-player gameanalysis of probabilistic systems. Its complexity

played on a graph. In an SG, an action a of ais interesting in its own: the problem of thresh-

player causes a transition from the current state s

old reachability—whether Maximizer has a strat-

to a successor s′ , with the latter chosen from a pre-egy that ensures the reachability probability to be′

scribed probability distribution δ(s, a, s ). Underat least given p—is known to be in UP ∩ coUP [19],the reachability objective, the two players (called

but no polynomial algorithm is known. The prac-

Maximizer and Minimizer ) aim to maximize andtical significance of SGs comes from the number

minimize, respectively, the reachability probabilityof problems that can be encoded to SGs and thensolved. Examples include the following: solving∗ 確率的ゲーム上の有界価値反復法における最大経路幅問

題と全域伝播The content of this paper is previously publishedin proceedings of the 32nd International Conference
on Computer-Aided Verification (CAV 2020) [24].

Kittiphon Phalakarn, ウォータールー大学, Universityof Waterloo, Waterloo, Canada.
Toru Takisaka, Ichiro Hasuo, 国立情報学研究所, National Institute of Informatics, Tokyo, Japan.
Thomas Haas, ブラウンシュヴァイク工科大学, Technical University of Braunschweig, Braunschweig,
Germany.
Ichiro Hasuo, 総合研究大学院大学, The Graduate University for Advanced Studies (SOKENDAI), Tokyo,
Japan.

deterministic parity games [8], solving stochastic
games with the parity or mean-payoﬀ objective [1],and a variety of probabilistic verification and reactive synthesis problems in diﬀerent application domains such as cyber-physical systems. See e.g. [25].
SGs are often called 2.5-player games, where
probabilistic branching is counted as 0.5 players.
They generalize deterministic automata (0-player),
Markov chains (MCs, 0.5-player), nondeterministic automata (1-player), Markov decision processes(MDPs, 1.5-player) and (deterministic) games (2-player). Many theoretical considerations on thesegeneral. Even worse, one cannot know how close

special cases carry over smoothly to SGs. However,the current approximant Xi ⊥ is to the desired func-

SGs have their peculiarities, too. One example istion V (G) [18]. In summary, VI as an iterative

the treatment of end components in bounded value

approximation method does not give any precision

iteration, as we describe later.

guarantee.

1. 3 Bounded Value Iteration (BVI) and1. 2 Value Iteration (VI)End Components

ability probability, that is, the reachability prob-

Bounded value iteration (BVI) has been actively

ability when both Maximizer and Minimizer takestudied as an extension of VI that comes with atheir optimal strategies. The function that returns

precision guarantee [2, 3, 5, 16, 18, 20, 23]. Its corethese optimal reachability probabilities is called thevalue function V (G) of the SG G; our interest is in

ideas are the following two.
L0 ≤ L1 ≤ · · ·Firstly, BVI com-≤computing this value function, desirably construct-

putes not only iter-U0 ≥ U1 ≥ · · ·≥In an SG, we are interested in the optimal reach-V (G)ing optimal strategies for the two players at the(2)
ative lower bounds Li = Xi ⊥ for V (G), but alsosame time. For this purpose, two principal families

iterative upper bounds Ui , as shown on the rightof solution methods are strategy iteration (SI) [19]in (2). This gives us a precision guarantee—V (G)and value iteration (VI) [10,13]—the latter is com-must lie between the approximants Li and Ui .
Secondly, for computing upper bounds Ui , BVI

monly preferred for performance reasons.
The mathematical principle that underpins VI isthe characterization of thespnuses the Bellman operator again: Ui = Xi ⊤ where

7 s1

p1

'

..
.

⊤ is the greatest element of the function spacesn

S → [0, 1]. This leads to the following approximation sequence that is dual to (1):value function V (G) as theleast fixed point (lfp) of an function update op-⊤ ≥ X⊤ ≥ X2 ⊤ ≥ · · · .

erator X called the Bellman operator. The Bell-The sequence (3) converges to the greatest fixedman operator X back-propagates function values

point (gfp) νX of X, which must be above the lfp

by one step, using the average.

V (G) = µX. Therefore the elements in (3) are all

For the simple(3)

case of Markov chains shown on the right, it is de∑fined by (Xf )(s) = i pi · f (si ), turning a function

above V (G).

f : S → [0, 1] (i.e., assignment of “scores” to states)

necessarily the same as µX. Therefore the upper

to Xf : S → [0, 1].

bounds U0 ≥ U1 ≥ · · · given by (3) may not con-

Since V (G) is the lfp µX, Kleene’s fixed point

verge to V (G). In other words, for a given threshold ε > 0, the bounds in (2) may fail to achieve

theorem tells us the sequence⊥ ≤ X⊥ ≤ X2 ⊥ ≤ · · · ,The problem, however, is that the gfp νX is not(1)

Ui − Li ≤ ε, no matter how large i is.

where ⊥ is the least element of the function space

In the lit-

S → [0, 1], converges to V (G) = µX. VI consists

erature, theof the iterative approximation of V (G) via the se-source of thisquence (1).

convergence

An issue from the practical point of view, how-

issue has been

ever, is that Xi ⊥ never becomes equal to V (G) in

identified to

~ 1
sI

?

s

1

0

1

図 1: A Markov chain (MC) for

which the naive BVI fails to converge

be end components (ECs) in MCs/MDPs/SGs.

V (G)(sI ).

ECs are much like loops without exits—an example

Such global propagation is easier said thanis in Fig. 1, where we use a Markov chain (MC) for

done—in fact, the very advantage of VI is that thesimplicity. Any function f that assigns the same

global quantities (namely reachability probabilities)

value to the states sI and s can be a fixed point of

get computed by iterations of local propagation.

the Bellman operator X (that back-propagates f by

Conducting global propagation in a computation-

averages); therefore, the gfp νX assigns 1 to bothally tractable manner requires a careful choice ofsI and s. In contrast, (µX)(sI ) = (µX)(s) = 0,

its venue. The solution in this paper is to com-which says one never reaches the target 1 from sIpute widest paths in a suitable (directed) weighted

or s (which is obvious).

graph.

Most previous works on BVI have focused on theMore specifically, in each iteration where we com-

problem of how to deal with ECs. Their solutions

pute an upper bound Ui , we conduct the following

are to get somehow rid of ECs. For example, ECs in

operations.

MDPs are discovered and collapsed in [5, 18]; ECs• (Player reduction) We turn the given SG G

in SGs cannot simply be collapsed, and an elab-

into an MDP Mi , by restricting Minimizer’s

orate method is proposed in the recent work [20]actions to the empirically optimal ones. The

that deflates them. This is the context of the cur-latter means they are optimal with respect torent work, and we aim to enhance BVI for SGs.

the current under-approximation Li of V (G).
• (Local propagation) The MDP Mi is then

1. 4 Contribution: Global Propagation inturned into a weighted graph (WG) Wi . The
construction of Wi consists of the application

BVI with Widest Paths
The algorithms in [20] seem to be the only BVIof X to the previous bound Ui−1 (i.e. local

algorithms known for SGs. In their performance,

propagation), and forgetting the information

however, EC computation often becomes a bottle-

that cannot be expressed in a weighted graphneck. Our contribution in this paper is a new BVI(such as the precise transition probabilities

algorithm for SGs that is free from the need for EC

δ(s, a, s′ ) that depend on the action a).

computation.

Due to this information loss, our analysis in

The key idea of our algorithm is global propa-

Wi is necessarily approximate. Nevertheless,gation for upper bounds, as sketched below. In

the benefit of Wi ’s simplicity is significant, as

each iteration for upper bounds U0 ≥ U1 ≥ · · · , wein the following step.

conduct global propagation, in addition to the lo-• (Global propagation) In the WG Wi , we solve

cal propagation in the usual BVI. The latter means

the widest path problem. This classic graph-the application of X to X ⊤, leading to X⊤; thistheoretic problem can be solved eﬃciently, e.g.,

local propagation, as we previously discussed, getsby the Dijkstra algorithm. The widest pathtrapped in end components. In contrast, our global

width gives a new upper bound Ui .

i

i+1

propagation looks at paths from each state s to the

Our algorithm satisfies soundness (V (G) ≤ Ui )target 1, ignoring end components. For example,

and convergence (Ui → V (G) as i → ∞). That

in Fig. 1, our global propagation sees that there is

the upper bounds decrease (U0 ≥ U1 ≥ · · · ) will

no path from sI to the target 1, and consequently

be obvious by construction. Hence, it always ter-assigns 0 as an upper bound for the value function

minates and returns an approximation of optimal

reachability probability within the required preci-

1. 6 Organizationsion. Proofs of these properties can be found in [24].

In §2 we present some preliminaries. In §3 we

We have also implemented our algorithm. Ourreview VI and BVI with an emphasis on the role ofexperiments compare its performance to the algo-

Kleene’s fixed point theorem. This paves the way

rithms from [20] (the original one and its learning-to §4 where we present our algorithm, as well as its

based variation). The results show our consistentsoundness and convergence properties. Experiment

performance advantage: depending on SGs, ourresults are shown in §5.

performance is from comparable to dozens of times
faster. The advantage is especially eminent in SGs

2 Preliminaries

with many ECs.

We fix some basic notations. Let X be a set. We

1. 5 Related Works

let X ∗ denote the set of finite sequences over X,∪
that is, X ∗ = i∈N X i . We let X + = X ∗ \ {ε},VI and BVI have been pursued principally forwhere ε denotes the empty sequence (of length 0).

MDPs. The only work we know that deals with

The set of infinite sequences over X is denoted by

SGs is [20]—with the exception of [26] that works

X ω . The set of functions from X to Y is denoted

in a restricted setting where every end component

by X → Y .

belongs exclusively to either player. The work closest to ours is therefore [20], in that we solve the2. 1 Stochastic Gamessame problem.

In a stochastic game, two players (Maximizer □For MDPs, the idea of BVI is first introducedand Minimizer ⃝) play against each other. The

in [23]; they worked in a limited setting where ECs

goals of the two players are to maximize and mini-

do not cause the convergence issue. Its extension

mize the value function, respectively. Many diﬀer-

to general MDPs with the reachability objective

ent definitions are possible for value functions. In

is presented in [5, 18], where ECs are computed

this paper (as well as all the works on (bounded)and then collapsed. BVI is studied under diﬀerent

value iteration), we focus on the reachability objec-

names in these works: bounded real time dynamic

tive, in which case a value function is defined byprogramming [5,23] and interval iteration [18]. The

the reachability probability to a designated target

work [20] is an extension of this line of work fromstate 1.

MDPs to SGs.
The work [20] has seen a few extensions to more

Definition 2.1 (stochastic game) A stochastic

advanced settings: black-box settings [3], concur-

game (SG) is a tuple G

rent reachability [16], and generalized reachability

1, 0, A, Av, δ) where

Most BVI algorithms involve EC computation
The EC algorithmin [14,15] is used in [18,20]; more recent algorithms
include [7, 9].

(S, S□ , S⃝ , sI ,• S is a finite set of states, partitioned into S□

games [2].

(although ours does not).

=and S⃝ (i.e., S = S□ ∪ S⃝ , S□ ∩ S⃝ = ∅).
s ∈ S□ is Maximizer’s state; s ∈ S⃝ is Minimizer’s state.
• sI ∈ S is an initial state, 1 ∈ S□ is a target,and 0 ∈ S⃝ is a sink.
• A is a finite set of actions.
• Av : S → 2A defines the set of actions that areavailable at each state s ∈ S.
• δ : S × A × S → [0, 1] is a transition function, where δ(s, a, s′ ) gives a probability withwhich to reach the state s′ when the action a
is taken at the state s. The value δ(s, a, s′ )is non-zero only if a ∈ Av(s); it must sat∑′isfys′ ∈S δ(s, a, s ) = 1 for all s ∈ S anda ∈ Av(s).
We assume that each of 1 and 0 allows only one
action that leads to a self-loop with probability 1.

図 2: A stochastic game (SG), an example

Moreover, for theoretical convenience, we assume
that all SGs are non-blocking. That is, Av(s) ̸= ∅for each s ∈ S.
We introduce some notations: post(s, a) = {s′ |′= S ′ ∩ S□
δ(s, a, s′ ) > 0}, and for S ′ ⊆ S, we let S□′
and S⃝= S ′ ∩ S⃝ .

Definition 2.2 (MDP, MC) An SG such thatS□ = S \ {0} (i.e. Minimizer is absent) is called

example but not exclusively, by reaching 0.
Both players choose their actions according totheir strategies.

It is well-known [13] that posi-tional (also called memoryless) and deterministic(also called pure) strategies are complete for finite
SGs with the reachability objective.
Definition 2.4 (strategy, path) Let G be thea Markov decision process (MDP). We often omit

SG in Def. 2.1. A strategy for Maximizer in G is

the second and third components for MDPs, writ-a function σ : S□ → A such that σ(s) ∈ Av(s) foring M = (S, sI , 1, 0, A, Av, δ).
An SG such that |Av(s)| = 1 for each s ∈S—both Maximizer and Minimizer are absent—iscalled a Markov chain (MC). It is also denoted simply by a tuple G = (S, sI , 1, 0, δ) where its transition function is of the type δ : S × S → [0, 1].
Every notion for SGs that appears below applies
to MDPs and MCs, too.
Example 2.3 Fig. 2 presents an example of an
SG. At the state s1 of Minimizer, two actions α
and β are in Av(s1 ). If Minimizer chooses α, thenext state is s2 with probability δ(s1 , α, s2 ) = 1.
If Minimizer instead chooses β, the next state is 1
with probability δ(s1 , β, 1) = 0.8 or 0 with probability δ(s1 , β, 0) = 0.2.
Maximizer’s goal is to reach 1 as often as possible by choosing suitable actions. Minimizer’s goal
is to avoid reaching 1—this can be achieved, foreach s ∈ S□ . A strategy for Minimizer is definedsimilarly. The set of Maximizer’s strategies in G isdenoted by strG□ ; that of Minimizer’s is denoted by
strG⃝ .
Strategies τ ∈ strG□ and σ ∈ strG⃝ in G turn thegame G into a Markov chain, which is denoted byG τ,σ . Similarly, a strategy τ for Maximizer (whois the only player) in an MDP M induces an MC,
denoted by Mτ .
A sequence s0 a0 s1 a1 s2 a2 . . . ∈ (S × A)ω is called
an infinite path in G if for all i ∈ N it satisfies
ai ∈ Av(si ) and si+1 ∈ post(si , ai ).

A prefixs0 a0 s1 . . . sk of an infinite path ending with a stateis called a finite path. If G is an MC, then we omit
actions in a path and write s0 s1 s2 . . . or s0 s1 . . . sk .
Given a game G and strategies τ, σ for the twoplayers, the induced MC G τ,σ assigns to each states ∈ S a probability distribution Pτ,σs . The distribution is with respect to the standard measurablestructure of S ω ; see, e.g., [4, Chap. 10]. For eachmeasurable subset X ⊆ Sω, Pτ,σs (X) is the prob-

ability with which G τ,σ , starting from the state s,
produces an infinite path π that belongs to X.
It is well-known that all the LTL properties are

and a weight function w : E → [0, 1] where [0, 1] isthe unit interval.
A (finite) path in a WG is defined in the usualgraph-theoretic way.
In the widest path problem, an edge weight

In the current setting withw(v, v ′ ) is thought of as its capacity, and the ca-

the reachability objective, we are interested in thepacity of a path is determined by its bottleneck.

probability of eventually reaching 1, denoted by

The problem asks for a path with the greatest ca-Pτ,σs (♢1).

pacity. In this paper, we use the following all-sourceωmeasurable in S .

single-destination version of the problem.
Definition 2.5 (value function V (G)) Let G be
the SG in Def. 2.1. The value function V (G) of G

Definition 2.8 (the widest path problem) A (fi-is defined bynite) path in W = (V, E, w) is a sequence v0 v1 . . . vn

V (G)(s) = maxof vertices such that (vi , vi+1 ) ∈ E for each i ∈min Pτ,σs (♢1)

τ ∈strG σ∈strG
⃝
□

= min

[0, n − 1]. The width of a path v0 v1 . . . vn is given

max Pτ,σs (♢1),σ∈strGτ ∈strG⃝□by mini∈[0,n−1] w(vi , vi+1 ).

where the last equality is shown in [13].

The widest path problem (WPP) is the following

We say a strategy τ of Maximizer’s is optimal
if V (G)(s) = minσ Pτ,σs (♢1) for each s ∈ S; similarly, we say a strategy σ of Minimizer’s is optimal
if V (G)(s) = maxσ Pσ,τs (♢1) for each s ∈ S.
We write V for V (G) when the dependence on G

problem.
Given: a WG W = (V, E, w) and a target vertex vt ∈ V.
Answer: for each v ∈ V , the widest width ofthe paths from v to vt , that is,is clear from the context.

maxby S♢1 . That is, S♢1 = {s ∈ S | V (G)(s) > 0}.

minn∈N,v=v0 ,v1 ,...,vn =vt i∈[0,n−1]

The set of states with a non-zero value is denotedw(vi , vi+1 ),We let WPW(W, vt ) denote a function thatsolves this problem, and let WPath(W, vt ) denote a

Example 2.6 Consider the SG G from Fig. 2.

function that assigns to each v ∈ V a widest path toAt s2 , Maximizer’s action should be α.

Hence,

vt . Furthermore, we assume the following property

V (G)(s2 ) = 0.9. At s1 , if Minimizer chooses α,of WPath: if WPath(W, vt )(v0 ) = v0 v1 . . . vk vt ,then the probability of reaching 1 will be 0.9 bythen WPath(W, vt )(vi ) = vi vi+1 . . . vk vt for each

V (G)(s2 ). Thus, Minimizer should choose β at s1 ,i ∈ [0, k].

which yields V (G)(s1 ) = 0.8. Finally, at sI , γ isthe best choice, since Maximizer can choose thisaction infinitely often until it gets to s2 . We have
V (G)(sI ) = 0.9.

Eﬃcient algorithms are known for WPW(W, vt ).
An example is the Dijkstra search algorithm with
Fibonacci heaps [17]; it is originally for the singlesource all-destination version but its adaptation
is easy.

2. 2 The Widest Path Problem
Definition 2.7 (weighted graph) A (directed)
weighted graph (WG) is a triple W = (V, E, w) ofa finite set V of vertices, a set E ⊆ V × V of edges,

The algorithm runs in time O(|E| +|V | log |V |).

It returns a widest path in addi-

tion to its width, too, computing the function
WPath(W, vt ) with the property required in thewe have

above.

()(νX)(s) = inf (Xi ⊤)(s)

3 (Bounded) Value Iterationi∈Nfor each s ∈ S.

3. 1 Bellman Operator and Value Itera-

2. Symmetrically, X has the least fixed point (lfp)tionµX : S → [0, 1], obtained as the limit of the as-

The following construct—used for “local propa-

cending chain

gation” in computing the value function—is cen-⊥ ≤ X⊥ ≤ X2 ⊥ ≤ · · · ,tral to formal analysis of probabilistic systems and(4)where ⊥(s) = 0 for each s ∈ S. That is, wegames.

have)((µX)(s) = sup (Xi ⊥)(s)Definition 3.1 (Bellman Operator) Let G =(S, S□ , S⃝ , sI , 1, 0, A, Av, δ) be a stochastic game.

i∈Nfor each s ∈ S.

For each state s ∈ S, an available action a ∈ Av(s),and f : S → [0, 1], we define a function Xa f : S →[0, 1] by the following.
1
if s = 1,
(Xa f )(s) = 0
if s = 0,



∑

′
′
 ′ δ(s, a, s ) · f (s ) if s ̸= 0, 1.
s ∈S
These functions are used in the following definition

The following characterization is fundamental.
See, e.g., [10].
Theorem 3.3 Let G be a stochastic game. The
value function V = V (G) (Def. 2.5) coincides withthe least fixed point µX.

of the Bellman operator X : (S → [0, 1]) → (S →The fact that V (G) is the least fixed point of X

[0, 1]) over G: maxa∈Av(s) (Xa f )(s)(Xf )(s) =mina∈Av(s) (Xa f )(s)implies the following: a strategy τ of Maximizer is(())
optimal if and only if Xτ (s) V (G) (s) = V (G)(s)

if s ∈ S□
if s ∈ S⃝

The function space S → [0, 1] inherits the usual
order ≤ between real numbers in the unit interval[0, 1], that is, f ≤ g if f (s) ≤ g(s) for each s ∈ S.
The Bellman operator X over S → [0, 1] is clearlymonotone; it is easily seen to preserve max andholds for each s ∈ S□ ; similarly for Minimizer.
We say a ∈ Av(s) is optimal at s if Xa V (G)(s) =V (G)(s) holds; otherwise a is suboptimal.
Lem. 3.2.2 & Thm. 3.3 suggest iterative underapproximation of V (G) by ⊥ ≤ X⊥ ≤ X2 ⊥ ≤ · · · .
This is the principle of value iteration (VI); see Algorithm 1.

min, using the fact that the state space S of an
SG is finite. Therefore we obtain the following, as

Example 3.4 The values Li computed by Algo-consequences of Kleene’s fixed point theorem.

rithm 1, for the SG in Fig. 2, are shown in thefollowing table. The values at 0 and 1 are omitted.

Lemma 3.2 Assume the setting of Def. 3.1.
1. The Bellman operator X has the greatest fixed

s

L0

L1

L2

L3

L4

L5

point (gfp) νX : S → [0, 1]. It is obtained as the

sI

0

0

0.54

0.83

0.87

0.89

s1

0

0

0.8

0.8

0.8

0.8

s2

0

0.9

0.9

0.9

0.9

0.9

limit of the descending ω-chain⊤ ≥ X⊤ ≥ X2 ⊤ ≥ · · · ,where ⊤ is the greatest element of S → [0, 1](i.e., ⊤(s) = 1 for each s ∈ S). In other words,

...

V (G)
0.9

...

0.8
0.9

Li (sI ) converges to, but is never equal to,
V (G)(sI ). The converges rate can be arbitrarily
slow: for any ε ∈ (0, 1) and k ∈ N there is an SG G
and a state s such that V (G)(s) − Lk (s) > ε. One

Algorithm 1: Value iteration (VI) for a stochastic game G = (S, S□ , S⃝ , sI , 1, 0, A, Av, δ) and astopping threshold ∆ > 0
1

procedure VI(G, ∆)2

L0 ← ⊥

3

while Li (sI ) − Li−1 (sI ) < ∆ do// Typical stopping criterioni++4

Li ← XLi−1

56// Initialize lower bound// Bellman update

return Li (sI )sees this by modifying Fig. 2 with δ(sI , γ, s2 ) = ε′′′and δ(sI , γ, sI ) = 1−ε , where ε > 0 is an arbitrarysmall positive constant.
There is no known stopping criterion for VI (Algorithm 1) with a precision guarantee, besides theone in [10] that is too pessimistic to be practical.
The one shown in Line 3 (“little progress”) is acommonly used heuristic, but it is known to leadto arbitrarily wrong results [18].

technical challenge addressed in the previous works
on BVI, including [5, 20].
In those works, the source of the failure of convergence is identified to be end components. See
the (very simple) Markov chain in Fig. 1, where
the reachability probability from sI to 1 is clearly
0. However, due to the loop between sI and s, thevalues Ui (sI ) and Ui (s)—these get updated to theaverage of Ui−1 at successors—are easily seen toremain 1. Roughly speaking, end components gen-

3. 2 Bounded Value Iteration
When we turn back to Lem. 3.2, Lem. 3.2.1
suggests another iterative approximation, namely
over-approximation of the value function V by
⊤ ≥ X⊤ ≥ X2 ⊤ ≥ · · · . The chain converges to
the gfp νX that is necessarily above the lfp µX.
This is the principle that underlies bounded value
iteration (BVI); see Algorithm 2 for its naive prototype. BVI has been actively studied in the literature [2, 3, 5, 16, 18, 20, 23], sometimes under different names (such as bounded real time dynamic
programming [5, 23] or interval iteration [18]).
BVI comes with a precision guarantee: since
V (G) lies between Li and Ui (whose gap is at mostε), the approximation Li is at most ε apart from
V (G).
The catch, however, is that µX and νX may
not coincide, and therefore the overapproximation
might not converge to the desired µX. This means
Algorithm 2 might not terminate. This is the maineralize such loops defined in MDPs and SGs (thedefinitions are graph-theoretic, in terms of strongly
connected components).

End components cause

non-convergence of naive BVI, essentially for thereason we just described.
The solutions previously proposed to this challenge have been to “get rid of end components.”
For MDPs (1.5 players), the collapsing techniquedetects end components and collapses each of theminto a single state [5, 18]. After doing so, the Bellman operator X has a unique fixed point (therefore µX = νX), assuring convergence of BVI (Algorithm 2). In the case of SGs (2.5 players), end
components cannot simply be collapsed into single
states—they must be handled carefully, taking the“best exits” into account. This is the key idea ofthe deflating technique proposed for SGs in [20].

4 Our Algorithm: Bounded Value Iteration with Upper Bounds Given by

Algorithm 2: Bounded value iteration (BVI) for a stochastic game G = (S, S□ , S⃝ , sI , 1,
0, A, Av, δ) and a stopping threshold ε > 0—a naive prototype that suﬀers from end components
1

procedure VI(G, ε)2

L0 ← ⊥, U0 ← ⊤3while Ui (sI ) − Li (sI ) > ε do456// Initialize lower and upper bound// Check the gap at the initial statei++
Li ← XLi−1 , Ui ← XUi−1// Bellman update

return Li (sI )Widest Paths

a weighted graph (WG) Wi .

In our algorithm, like in other BVI algorithm,

The construction here is local propagation

we iteratively construct upper and lower boundsof the previous upper bound Ui−1 , from

Ui , Li of the value function V (G) at the same time.

each state s to its predecessors in Mi .

See (2). In updating Ui , however, we go beyond theThis is much like an application of the Bell-local propagation by the Bellman update and con-man operator X.

duct global propagation, too. This frees us from

– (Global propagation by widest paths)

the curse of end components. The outline of ourFinally, we solve the widest path problem

algorithm is as follows.

in the WG Wi , from each state s to the• The lower bound Li is given by Li = Xi ⊥, fol-target state 1. The maximum path width

lowing Lem. 3.2.2 and Thm. 3.3. This is thefrom s to 1 is used as the value of the up-same as the other VI algorithms.

per bound Ui (s).

• The upper bounds Ui is constructed in the fol-This way, we conduct global propagation of

lowing three steps, using a global propagation

upper bounds, for which end componentsthat takes advantage of fast widest path algo-pose no threats. Our global propagation

rithms.

is still computationally feasible, thanks to– (Player reduction) Firstly, we turn thethe preprocessing in the previous step that

SG G into an MDP Mi by fixing Mini-

turns a problem on an MDP into one on amizer’s strategy to a specific one σi .

WG (modulo some sound approximation).

Any choice of σi would do for the sake of

The use of global propagation for upper bounds issoundness (that is, V (G) ≤ Ui ). However,a distinguishing feature of our algorithm. This isfor convergence (that is, Ui → V (G) as

unlike other BVI algorithms (such as [5, 20]) wherei → ∞), it is important to have σ0 , σ1 , . . .

upper-bound propagation is only local and step-

eventually converge to Minimizer’s opti-

wise. The latter gets trapped when it encounters

mal strategy σ⃝ . Therefore we let Li —thean EC—therefore some trick such as collapsing [5]current lower estimate of V (G)—induceand deflating [20] is needed—while our global prop-

σi .

agation looks directly at the target state 1.

Recall that Li converges to V (G)(Lem. 3.2.2, Thm. 3.3).

The above outline is presented as pseudocode in– (Preprocessing by local propaga-

Algorithm 3. We describe the three steps in thetion) Secondly, we turn the MDP Mi into

rest of the section. In particular, we exhibit theAlgorithm 3: Our BVI algorithm via widest paths. Here G = (S, S□ , S⃝ , sI , 1, 0, A, Av, δ) is an
SG; ε > 0 is a stopping threshold.
1

procedure BVI WP(G, ε)2

L0 ← ⊥, U0 ← ⊤, i ← 03while Ui (sI ) − Li (sI ) > ε do

4

i++

5

Li ← XLi−1

6

Mi ← MPlRd (G, Li )// player reduction

7

Wi ← WLcPg (Mi , Ui−1 )// local propagation

8

Ui ← min{Ui−1 , WPW(Wi )}9// value iteration for lower bounds// widest path computation

return Ui (sI )definitions of MPlRd and WLcPg (WPW has beenmizer’s.

defined and discussed in Def. 2.8) as well as correctness of the algorithm (§4. 3). Proofs of theorems in

In Algorithm 3, we will be using the MDP induced by the following specific Minimizer restric-

this section can be found in [24].

tion induced by a function f .
4. 1 Player Reduction:from SGs to

MDPs
In Line 6, Algorithm 3 reduces the input SG G
into an MDP M1 by 1) restricting actions (from
Av to Av′ ), and 2) turning Minimizer’s states into
Maximizer’s.
Definition 4.1 (the MDP M(G, Av′ )) Let G be′

the game in Algorithm 3, and Av : S → 2 be suchA

that ∅ ̸= Av′ (s) ⊆ Av(s) for each s ∈ S.
Then the MDP given by the tuple (S, S \Definition 4.3 (the MDP MPlRd (G, f )) Let G
be the game in Algorithm 3, and f : S → [0, 1]
be a function. The MDP MPlRd (G, f ) is defined
to be M(G, Avf ) (Def. 4.1), where the function
Avf : S → 2A is defined as follows: for s ∈ S□
we let Avf (s) = Av(s); and for s ∈ S⃝ we let
Avf (s) = {a ∈ Av(s)| ∀b ∈ Av(s). (Xa f )(s) ≤ (Xb f )(s)}.

(5)

The function Avf is a Minimizer restriction in G
(Def. 4.2).

{0}, {0}, sI , 1, 0, A, Av′ , δ) shall be denoted by

The intuition of (5) is that a = arg minb∈Av(s) (Xb f )(s).

M(G, Av′ ), and we say it is induced from G by re-In the use of this construction in Algorithm 3,

stricting Av to Av′ .

the function f will be our “best guess” Li of

The following class of action restrictions will be

the value function V (G).

In this situation,arg minb∈Av(s) (Xb f )(s) is the best action for Mini-

heavily used.

mizer based on the guess f = Li .
Definition 4.2 (Minimizer restriction) Let G
be as in Algorithm 3.

A Minimizer restrictionof Av is a function Av′ : S → 2A such that 1)∅ ̸= Av′ (s) ⊆ Av(s) for each s ∈ S, and 2)
Av′ (s) = Av(s) for each state s ∈ S□ of Maxi-

Definition 4.4 (the MDP Mi , and Avi ) In Algorithm 3, the MDP Mi is given by MPlRd (G, Li ) =M(G, AvLi ). We write Avi for available actions inMi , that is, Mi = (S, 1, 0, A, Avi , δ).

that a similar “look-ahead” can be done by solving
the widest path problem in the following weighted

In the case of Algorithm 3,

the MDPs

M0 , M1 , . . . do not only “converge” to G, but also

graph.

“reach G in finitely many steps,” in the following

Definition 4.7 (the WG WLcPg (M, f )) Let M =sense.

(S, 1, 0, A, Av′ , δ) be an MDP, and f : S → [0, 1].

Lemma 4.5 In Algorithm 3, there exists iM ∈ Nsuch that, for each i ≥ iM , we have V (G) = V (Mi ).
4. 2 Local Propagation:from MDPs to

WGs

The WG WLcPg (M, f ) is the following triple(S, E, w).
• Its set of vertices is S.
• We have (s, s′ ) ∈ E if and only if, for somea ∈ Av′ (s), we have s′ ∈ post(s, a) (i.e.,δ(s, a, s′ ) > 0).

Here is a technical observation that motivates thefunction WLcPg .
Lemma 4.6 Let G be the game in Algorithm 3,• The weight function w : E → [0, 1] is given byw(s, s′ ) ={}max Xa f (s) a ∈ Av′ (s), s′ ∈ post(s, a) .
(7)

and Av′ : S → 2A be a Minimizer restriction

In (7), the function f —that is, the previous up-(Def. 4.2).
1. For each state s ∈ S, we have( ())
V (G)(s) ≤ maxa∈Av′ (s) Xa V (G) (s).

per bound Ui−1 in Algorithm 3—is propagated one

2. For each k ∈ N, we haveing these propagated values as weights in a WG

V (G)(s0 ) ≤maxaks0 −→s1 −→ ··· −→ in Av′
a0

a1

(

step by the application of Xa . This way of encodseems pretty rough. For example, in case both s′())
Xak V (G) (sk ),and s′′ are in post(s, a) for each a ∈ Av′ (s), we havew(s, s′ ) = w(s, s′′ ), no matter what the transition(6)
where the maximum is taken over a0 , s1 , a1 ,probabilities from s to s′ , s′′ are. The return for∈this paid price (namely the information lost in thepost(s0 , a0 ), a1 ∈ Av′ (s1 ), . . . , sk ∈ post(sk−1 ,rough encoding) is that the resulting data structureak−1 ), ak ∈ Av′ (sk ).

(WG) allows fast global analysis via the widest path

. . . , sk , ak such that a0∈

Av′ (s0 ), s1

problem. Our experiment results in §5 demonstrate

Lem. 4.6.2, although not itself used in the followingthat this rough yet global approximation can maketechnical development, suggests the idea of global

upper bounds quickly converge.

propagation for upper bounds. Note that a boundis given in (6) for each k; it is possible that a bound

4. 3 Soundness and Convergencefor some k > 1 is tighter than that for k = 1, moti-

In Algorithm 3, an SG G is turned into an MDPvating us to take a “look-ahead” further than one

Mi and then to a WG Wi . Our claim is that com-step.

puting a widest path in Wi gives the next upper

However, the bound in (6) is not particularlybound Ui in the iteration. The following properties

tuned for tractability: computation of the maxi-

assure correctness and termination of Algorithm 3.

mum involves words whose number is exponential
in k, and moreover, we want to do so for many k’s.
In the end, our main technical contribution is

Theorem 4.8 (soundness) In Algorithm 3, V (G) ≤Ui holds for each i ∈ N.

erature: mdsm [11], cloud [6], teamform [12] andinvestor [22].

In addition, we used our model

Theorem 4.9 (convergence) In Algorithm 3,

manyECs—an artificial model with many ECs—to

let the while loop iterate forever. Then Ui → V (G)assess the eﬀect of ECs on performance. The model

as i → ∞.

manyECs is presented in the appendix. Each of

5 Experiment Results
5. 1 Experiment Settings
We compare the following four algorithms.
• WP is our BVI algorithm via widest paths.
It avoids end component (EC) computation by
global propagation of upper bounds.

these five models comes with a model parameter
N.
There is another model called cdmsn in [20]. We
do not discuss cdmsn since all the algorithms (oursand those from [20]) terminated within 0.001 seconds.

• DFL is the implementation of the main algorithm in [20]. It relies on EC computation for
deflating.
• DFL m is our modification of DFL, wheresome unnecessary repetition of EC computation is removed.
• DFL BRTDP is the learning-based variant of
DFL. It restricts bound update to those states
which are visited by simulations. See [20] fordetails.

5. 2 Results
The number i of iterations and the running timefor each algorithm and each input SG is shownin Table 1. For DFL BRTDP, the ratio of states
visited by the algorithm is shown in percentage;
the smaller it is, the more eﬃcient the algorithm
is in reducing the state space. Each number for
DFL BRTDP (a probabilistic algorithm) is the average over 5 runs.

The latter three—coming from [20]—are the only
existing BVI algorithms for SGs with a convergenceguarantee, to the best of our knowledge. The implementation of DFL and DFL BRTDP is provided
by the authors of [20].
The four algorithms are implemented on top of
PRISM-games [21] version 2.0. We used the stopping threshold ε = 10−6 . The experiments wereconducted on Dell Inspiron 3421 Laptop with 4.00
GB RAM and Intel(R) Core(TM) i5-3337U 1.80
GHz processor.
In the implementations of DFL and DFL BRTDP,
the deflating operation is applied only once every
five iterations [20, §B.3]. Following this, our WP
also solves the widest path problem (Line 8) only
once every five iterations, while other operations
are applied in each iteration.
For input SGs, we took four models from the lit-

5. 3 Discussion
We observe consistent performance advantage of
our algorithm (WP). Even in the mdsm model
where the DFL algorithms do not suﬀer from EC
computation (#EC is just 1), WP’s performanceis comparable to DFL. The cloud model is where
the learning-based approach in [20] works well—see visit% that are very small. Our WP performs
comparably against DFL BRTDP, too.
The performance advantage of our WP algorithm is eminent, not only in the artificial model ofmanyECs (where WP is faster by magnitudes), butalso in the realistic model investor that comes froma financial application scenario [22]. The results forthese two models suggest that WP is indeed advantageous when EC computation poses a bottleneckfor other algorithms.
Overall, we observe that our WP algorithm can

表 1: Experimental results, comparing WP (our algorithm) with those in [20]. N is a model parameter(the bigger the more complex). #states, #trans, #EC show the numbers of states, transitions and ECs in
the SG, respectively. itr is the number i of iterations at termination; time is the execution time in seconds.
For each SG, the fastest algorithm is shaded in green. The settings that did not terminate are shaded ingray; TO is time out (6 hours), OOM is out of memory, and SO is stack overflow.

model

mdsm

cloud

teamform

investor

manyECsN#states#trans

#EC

DFL
itr

DFL m

DFL BRTDP

time

itr

time

itr

visit%

time

itr

WP
time

3

62245

151143

1

121

3

121

4

17339

49.3

15

120

5

4

335211882765

1

125

15

125

47

91301

42.1

86

124

38

5

8842

60437

4421

7

7

7

1

167

6.9

14

7

<1

6

34954

274965

17477

11

177

11

5

41

0.6

3

11

1

7

1394021237525

69701

11

19721

11

62

41

0.2

4

11

5

3

12475

15228

2754

2

<1

2

<1

972

49.0

137

2

<1

4154

34.6

4

96665

116464

19800

2

<1

2

<1

9603

2

<1

5

9079931084752

176760

2

<1

2

<1

TO

2

<1

50

211321673810

29690

441

184

441

100

8075212587510114390

801

3318

249

TO

364

48

OOM

TO

688

736

500

1004

3007

502

6

7

6

7

TO

5

<1

1000

2004

6007

1002

6

51

6

51

TO

5

<1

5000

10004

30007

5002

SO

TO

5

<1

SO

be the first choice when it comes to solving SGs: forthe results in [20] are extended and used in [2,3,16].

some models, it runs much faster than other algo-

In doing so, we hope to make essential use of struc-rithms; for other models, even if the performancestures that are unique to those advanced problemof other algorithms diﬀers a lot, WP’s performancesettings. Another important direction is to push

is comparable with the best algorithm.

forward the idea of global propagation in verification and synthesis, seeking further instances of

6 Conclusions and Future Workthe idea.

In this paper, we presented a new BVI algorithm

tion idea in the context of reinforcement learning—for solving stochastic games.

Finally, pursuing the global propaga-

It features global

where problems are often formalized using MDPs

propagation of upper bounds by widest paths, via

and the Bellman operator is heavily utilized—may

a novel encoding of the problem to a suitableopen up another fruitful collaboration between for-weighted graph. This way we avoid computation

mal methods and statistical machine learning.

of end components that often penalizes the performance of the other BVI-based algorithms. Our ex-

Acknowledgment

perimental comparison with known BVI algorithms

The authors are supported by ERATO HASUO

for SGs demonstrates the eﬃciency of our algo-

Metamathematics for Systems Design Project (No.

rithm. For correctness of the algorithm, we pre-JPMJER1603), JST; I.H. is supported by Grant-in-

sented proofs for soundness and convergence.

Aid No. 15KT0012, JSPS. Thanks are due to Max-

Extending the current algorithm for more ad-imilian Weininger and Edon Kelmendi for sharing

vanced settings is future work—this is much liketheir implementation, and to Pranav Ashok andDavid Sprunger for useful discussions and comments.
参 考 文 献[ 1 ] Andersson, D. and Miltersen, P. B.: The Complexity of Solving Stochastic Games on Graphs,
Algorithms and Computation, 20th International
Symposium, ISAAC 2009, Honolulu, Hawaii, USA,
December 16-18, 2009. Proceedings, Dong, Y., Du,
D., and Ibarra, O. H.(eds.), Lecture Notes in Computer Science, Vol. 5878, Springer, 2009, pp. 112–
121.
[ 2 ] Ashok, P., Kretinsky, J., and Weininger, M.:
Approximating Values of Generalized-Reachability
Stochastic Games, CoRR, Vol. abs/1908.05106(2019).
[ 3 ] Ashok, P., Kretı́nský, J., and Weininger, M.:
PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games, Computer
Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July
15-18, 2019, Proceedings, Part I, Dillig, I. andTasiran, S.(eds.), Lecture Notes in Computer Science, Vol. 11561, Springer, 2019, pp. 497–519.
[ 4 ] Baier, C. and Katoen, J.-P.: Principles of model
checking, MIT press, 2008.
[ 5 ] Brázdil, T., Chatterjee, K., Chmelik, M., Forejt,
V., Kretı́nský, J., Kwiatkowska, M. Z., Parker,
D., and Ujma, M.: Verification of Markov Decision Processes Using Learning Algorithms, Automated Technology for Verification and Analysis 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings, Cassez, F. and Raskin, J.(eds.), Lecture
Notes in Computer Science, Vol. 8837, Springer,
2014, pp. 98–114.
[ 6 ] Calinescu, R., Kikuchi, S., and Johnson, K.:
Compositional Reverification of Probabilistic Safety
Properties for Large-Scale Complex IT Systems,
Large-Scale Complex IT Systems. Development,
Operation and Management - 17th Monterey Workshop 2012, Oxford, UK, March 19-21, 2012, Revised Selected Papers, Calinescu, R. and Garlan, D.(eds.), Lecture Notes in Computer Science,Vol. 7539, Springer, 2012, pp. 303–329.
[ 7 ] Chatterjee, K., Dvorák, W., Henzinger, M.,
and Svozil, A.: Near-Linear Time Algorithms forStreett Objectives in Graphs and MDPs, 30th International Conference on Concurrency Theory,
CONCUR 2019, August 27-30, 2019, Amsterdam,
the Netherlands., Fokkink, W. and van Glabbeek,
R.(eds.), LIPIcs, Vol. 140, Schloss Dagstuhl Leibniz-Zentrum für Informatik, 2019, pp. 7:1–7:16.
[ 8 ] Chatterjee, K. and Fijalkow, N.: A reduction
from parity games to simple stochastic games, Proceedings of Second International Symposium on
Games, Automata, Logics and Formal Verification,
GandALF 2011, Minori, Italy, 15-17th June 2011,

D’Agostino, G. and La Torre, S.(eds.), EPTCS,
Vol. 54, 2011, pp. 74–86.
[ 9 ] Chatterjee, K. and Henzinger, M.: Eﬃcient anddynamic algorithms for alternating büchi games andmaximal end-component decomposition, Journal of
the ACM (JACM), Vol. 61, No. 3(2014), pp. 15.
[10] Chatterjee, K. and Henzinger, T. A.: Value
Iteration, 25 Years of Model Checking - History,
Achievements, Perspectives, Grumberg, O. andVeith, H.(eds.), Lecture Notes in Computer Science,Vol. 5000, Springer, 2008, pp. 107–138.
[11] Chen, T., Forejt, V., Kwiatkowska, M. Z.,
Parker, D., and Simaitis, A.: Automatic verificationof competitive stochastic systems, Formal Methods
in System Design, Vol. 43, No. 1(2013), pp. 61–92.
[12] Chen, T., Kwiatkowska, M. Z., Parker, D., andSimaitis, A.: Verifying Team Formation Protocols
with Probabilistic Model Checking, Computational
Logic in Multi-Agent Systems - 12th International
Workshop, CLIMA XII, Barcelona, Spain, July
17-18, 2011. Proceedings, Leite, J., Torroni, P.,Ågotnes, T., Boella, G., and van der Torre, L.(eds.),
Lecture Notes in Computer Science, Vol. 6814,
Springer, 2011, pp. 190–207.
[13] Condon, A.: The Complexity of Stochastic
Games, Inf. Comput., Vol. 96, No. 2(1992), pp. 203–
224.
[14] Courcoubetis, C. and Yannakakis, M.: The
Complexity of Probabilistic Verification, J. ACM,
Vol. 42, No. 4(1995), pp. 857–907.
[15] De Alfaro, L.: Formal verification of probabilistic systems, Citeseer, 1997.
[16] Eisentraut, J., Kretinsky, J., and Rotar, A.:
Stopping Criteria for Value and Strategy Iteration on Concurrent Stochastic Reachability Games,
CoRR, Vol. abs/1909.08348(2019).
[17] Fredman, M. L. and Tarjan, R. E.: Fibonacci
heaps and their uses in improved network optimization algorithms, J. ACM, Vol. 34, No. 3(1987),
pp. 596–615.
[18] Haddad, S. and Monmege, B.: Interval iteration
algorithm for MDPs and IMDPs, Theoretical Computer Science, Vol. 735(2018), pp. 111–131.
[19] Hoﬀman, A. J. and Karp, R. M.: On nonterminating stochastic games, Management Science,Vol. 12, No. 5(1966), pp. 359–370.
[20] Kelmendi, E., Krämer, J., Křetı́nskỳ, J., andWeininger, M.: Value iteration for simple stochastic
games: stopping criterion and learning algorithm,
International Conference on Computer Aided Verification, Springer, 2018, pp. 623–642.
[21] Kwiatkowska, M., Parker, D., and Wiltsche, C.:
PRISM-games: Verification and Strategy Synthesis for Stochastic Multi-player Games with Multiple Objectives, International Journal on Software
Tools for Technology Transfer, Vol. 20, No. 2(2017),
pp. 195210.
[22] McIver, A. and Morgan, C.: Results on thequantitative µ-calculus qMµ, ACM Trans. Comput.
Log., Vol. 8, No. 1(2007), pp. 3.
[23] McMahan, H. B., Likhachev, M., and Gordon, G. J.: Bounded real-time dynamic programming: RTDP with monotone upper bounds and performance guarantees, Machine Learning, Proceedings of the Twenty-Second International Conference (ICML 2005), Bonn, Germany, August 7-11,
2005, Raedt, L. D. and Wrobel, S.(eds.), ACM International Conference Proceeding Series, Vol. 119,
ACM, 2005, pp. 569–576.
[24] Phalakarn, K., Takisaka, T., Haas, T., andHasuo, I.: Widest Paths and Global Propagationin Bounded Value Iteration for Stochastic Games,
Computer Aided Verification - 32nd International
Conference, CAV 2020, Los Angeles, CA, USA,
July 21-24, 2020, Proceedings, Part II, Lahiri, S. K.
and Wang, C.(eds.), Lecture Notes in Computer Science, Vol. 12225, Springer, 2020, pp. 349–371.
[25] Svorenová, M. and Kwiatkowska, M.: Quantitative verification and strategy synthesis for stochastic
games, Eur. J. Control, Vol. 30(2016), pp. 15–30.
[26] Ujma, M.: On Verication and Controller Synthesis for Probabilistic Systems at Runtime, PhD
Thesis, Wolfson College, Univ. Oxford, 2015.