Hugo Gimbert
email: hugo.gimbert@labri.fr

Florian Horn
email: florian.horn@liafa.jussieu.fr

Simple Stochastic Games with Few Random Vertices are Easy to Solve ⋆

We present a new algorithm for solving Simple Stochastic Games (SSGs). This algorithm is based on an exhaustive search of a special kind of positional optimal strategies, the f-strategies. The running time is O( |VR|! • (|V ||E| + |p|) ), where |V |, |VR|, |E| and |p| are respectively the number of vertices, random vertices and edges, and the maximum bit-length of a transition probability.

Our algorithm improves existing algorithms for solving SSGs in three aspects. First, our algorithm performs well on SSGs with few random vertices, second it does not rely on linear or quadratic programming, third it applies to all SSGs, not only stopping SSGs.

Introduction

Simple Stochastic Games (SSGs for short) are played by two players Max and Min in a sequence of steps. Players move a pebble along edges of a directed graph (V, E). There are three type of vertices: V Max is the set of vertices of player Max, V Min the set of vertices of player Min and V R the set of random vertices. When the pebble is on a vertex of V Max or V Min , the corresponding player chooses an outgoing edge and moves the pebble along it. When the pebble is on a random vertex, the successor is chosen randomly according to some fixed probability distribution: from vertex v ∈ V R the pebble moves towards vertex w ∈ V with some probability p(w|v) and the probability that the game stops is 0, i.e. w∈V p(w|v) = 1. An SSG is depicted on Figure 1, with vertices of V Max represented as , vertices of V Min represented as , and vertices of V R represented as ♦.

Player Max and Min have opposite goals, indeed player Max wants the pebble to reach a special vertex t ∈ V called the target vertex, if this happens the play is won by player Max. In the opposite case, the play proceeds forever without reaching t and is won by player Min. For technical reasons, we assume that t is a vertex of player Max and is absorbing. Strategies are used by players to choose their moves, a strategy tells where to move the pebble depending on the sequence of previous vertices, i.e. the finite path followed by the pebble from the beginning of the play. The value of a vertex v is the maximal probability with which player Max can enforce the play to reach the target vertex. When player Max, respectively player Min, uses an optimal strategy he ensures reaching the target with a probability greater, respectively smaller, than the value of the initial vertex. Notions of value and optimal strategies are formally defined in Section 1. We are interesting in solving SSGs, that is computing values and optimal strategies.

Applications. SSGs are a natural model of reactive systems, and algorithms for solving SSGs may be used for synthesizing controllers of such systems. For example an hardware component may be modelled as an SSG whose vertices are the global states of the component, the target is some error state to avoid, random states are used to model failure probabilities and stochastic behaviours of the environment, choices of player Min corresponds to actions available to the software driver and player Max corresponds to non-deterministic behaviour of the environnment. Then an optimal strategy for player Min in the SSG will correspond to a software driver minimizing the probability to enter the error state, whatever be the behaviour of the environnment.

Existing algorithms for solving SSGs. The complexity of solving SSGs was first considered by Condon [Con92], who proved that deciding whether the value of an SSG is greater than 1 2 is in NP ∩ co-NP. The algorithm provided in [START_REF] Condon | The complexity of stochastic games[END_REF] consists in first transforming the input SSG in a stopping SSG where the probability to reach a sink vertex is 1. The transformation keeps unchanged the fact that the initial vertex has value strictly greater than 1 2 but induces a quadratic blowup of the size of the SSG. The algorithm then non-deterministically guesses the values of vertices, which are rational numbers of linear size, and checks that these values are the unique solutions of some local optimality equations.

Three other kinds of algorithms for solving SSGs are presented in [START_REF] Condon | On algorithms for simple stochastic games[END_REF]. These algorithms require transformation of the initial SSG into an equivalent stopping SSG and are based on local optimality equations. First algorithm computes values of vertices using a quadratic program with linear constraints. Second algorithm computes iteratively from below the values of the SSGs, and the third is a strategy improvement algorithm à la Hoffman-Karp. These two last algorithms require solving an exponential number of linear programs, as it is the case for the algorithm recently proposed in [START_REF] Somla | New algorithms for solving simple stochastic games[END_REF].

Finally, these four algorithms suffer three main drawbacks.

First, these algorithms rely on solving either an exponential number of linear programs or a quadratic program, which may have prohibitive algorithmic cost and makes the implementation tedious.

Second, these algorithms only apply to the special class of stopping SSGs. Although it is possible to transform any SSG into a stopping SSG with arbitrarily small change of values, computing exact values this way requires to modify drastically the original SSG, introducing either |V | 2 new random vertices or new transition probabilities of bit-length quadratic in the original bit-length. This also makes the implementation tedious.

Third, the running time of these algorithms may a priori be exponential whatever be the number of random vertices of the input SSG, including the case of SSGs with no random vertices at all, also known as reachability games on graphs. However it is well-known that reachability games on graphs are solvable in quadratic time.

Notice that randomized algorithms do not perform much better since the best randomized algorithms [START_REF] Ludwig | A subexponential randomized algorithm for the simple stochastic game problem[END_REF][START_REF] Halman | Simple stochastic games, parity games, mean payoff games and discounted payoff games are all lp-type problems[END_REF] The key point of our algorithm is the fact that optimal strategies may be looked for in a strict subset of positional strategies, called the class of f -strategies. The f -strategies are in correspondence with permutations of random vertices. Our algorithm does an exhaustive search of optimal f -strategies among the |V R |! available ones and check their optimality. Optimality is easy to check, it consists in computing a reachability probability in a Markov Chain with V R states, which amounts to solving a linear system with at most |V R | equations.

Comparison with existing work. We improve existing results by three aspects: our algorithm performs better on SSGs with few random vertices, it is arguably much simpler, and we provide new insight about the structure of optimal strategies.

Our algorithm performs much better on SSGs with few random vertices than previously known algorithms. Indeed, its complexity is

O( |V R |! • (|V ||E| + |p|) ),
hence when there are no random vertices at all, our algorithm matches the usual quadratic complexity for solving reachability games on graphs. When the number of random vertices is fixed, our algorithm performs in polynomial time, and on the class of SSGs such that

|V R | ≤ |V Max | + |V Min | our algorithm is sub-exponential.
Our algorithm is arguably simpler than previously known algorithms. Indeed, it does not require use of linear or quadratic programming. Although linear programs can be solved in polynomial time [START_REF] Kachiyan | A polynomial time algorithm for linear programming[END_REF][START_REF] Renegar | A polynomial-time algorithm, based on newton's method, for linear programming[END_REF], solvers require high-precision arithmetics. By contrast, our algorithm is very elementary: it enumerates permutations of the random vertices and for each permutation, it solves a linear system of equations.

Our algorithm is also simpler because it applies directly to any kind of SSGs, whereas previously known algorithms require the transformation of the input SSG into a stopping SSG of quadratic size.

Plan. The paper is organised as follows. In the first section, we introduce formally SSGs, values and optimal strategies. In the second section, we present the notion of f -strategies. In the third section, we focuse on two properties of f -strategies: self-consistency and progressiveness. We prove that f -strategies that are both self-consistent and progressive are also optimal, and we prove the existence of such strategies. In the fourth section we describe our algorithm for solving SSGs.

Omited proofs can be found in the full version of the paper [START_REF] Gimbert | Solving simple stochastic games with few random vertices[END_REF].

Simple Stochastic Games

In this section we give formal definitions of an SSG, values and optimal strategies. An SSG is a tuple (V, V Max , V Min , V R , E, t, p), where (V, E) is a graph, (V Max , V Min , V R ) is partition of V , t ∈ V is the target vertex and for every v ∈ V R and w ∈ V , p(w|v) is the transition probability from v to w, with the property

w∈V p(w|v) = 1. A play is an infinite sequence v 0 v 1 • • • ∈ V ω of vertices such that if v n ∈ (V Max ∪ V Min ) then (v n , v n+1 ) ∈ E and if v n ∈ V R then p(v n+1 |v n ) > 0.
A play is won by Max if it visits the target vertex; otherwise the play is won by Min. A finite play is a finite prefix of a play.

A strategy for player Max is a mapping σ :

V * V Max → V such that for each finite play h = v 0 . . . v n such that v n ∈ V Max , we have (v n , σ(h)) ∈ E. A play v 0 v 1 • • • is consistent with σ if for every n, if v n ∈ V Max then v n+1 is σ(v 0 • • • v n ).
A strategy for player Min is defined similarly, and is generally denoted τ .

Once the initial vertex v and two strategies σ, τ for player Max and Min are fixed, we can measure the probability that a given set of plays occurs. This probability measure is denoted P σ,τ v . For every n ∈ N, we denote by V n the random variable defined by

V n (v 0 v 1 • • • ) = v n ,
the set of plays is equipped with the σalgebra generated by random variables (V n ) n∈N . Then there exists a probability measure P σ,τ v with the following properties:

P σ,τ v (V 0 = v) = 1 (1) P σ,τ v (V n+1 = σ(V 0 • • • V n ) | V n ∈ V Max ) = 1 , (2)
P σ,τ v (V n+1 = τ (V 0 • • • V n ) | V n ∈ V Min ) = 1 , (3)
P σ,τ v (V n+1 | V n ∈ V R ) = p(V n+1 |V n ) . (4)
Expectation of a real-valued, measurable and bounded function

φ under P σ,τ v is denoted E σ,τ v [φ]
. We will often use implicitely the following formula, which gives the expectation of φ once a finite prefix

h = v 0 v 1 • • • v n of the play is fixed: E σ,τ v [ φ | V 0 • • • V n = h] = E σ[h],τ [h] vn [ φ[h] ] , (5)
where

σ[h](w 0 w 1 w 2 • • • ) = σ(v 0 • • • v n w 1 w 2 • • • ) and τ [h] and φ[h] are defined similarly.
Values and positional optimal strategies. The goal of player Max is to reach the target vertex t with the highest probability possible, whereas player Min has the opposite goal. Given a starting vertex v and a strategy σ for player Max, whatever strategy τ is chosen by Min, the target vertex t will be reached with probability at least:

inf τ P σ,τ v (Reach(t))
, where Reach(t) is the event {∃n ∈ N, V n = t}. Thus, starting from v, player Max can ensure to win the game with probability arbitrarily close to:

val * (v) = sup σ inf τ P σ,τ v (Reach(t)) ,
and symmetrically, player Min can ensure that player Max cannot win with a probability much higher than:

val * (v) = inf τ sup σ P σ,τ v (Reach(t)) .
Clearly val * (v) ≤ val * (v). In fact these values are equal, and this common value is called the value of vertex v and denoted val(v). A much stronger result is known about SSGs: the infimum and supremum used in the definition of val(v) are attained for some strategies called optimal strategies. Moreover, there exists optimal strategies of a simple kind, called positional strategies. A strategy σ is said to be positional if it depends only on the current vertex, i.e. for every finite play

v 0 • • • v n σ(v 0 • • • v n ) = σ(v n ).
The following results are wellknown [START_REF] Shapley | Stochastic games[END_REF][START_REF] Condon | The complexity of stochastic games[END_REF].

Theorem 1. In any SSG, for every vertex v ∈ V , the values val * (v) and val * (v) are equal. This common value is called the value of vertex v and denoted val(v).

There exists strategies σ # and τ # that are optimal i.e. for every vertex v and every strategies σ, τ :

P σ,τ # v (Reach(t)) ≤ val(v) ≤ P σ # ,τ v (Reach(t)) .
Moreover there exists strategies that are both optimal and positional.

2 Playing with f-strategies

Existence of positional optimal strategies is a key property of SSGs, used for designing all known algorithms solving SSGs. The algorithm we propose relies on a refinement of this result, we will prove that optimal strategies can be looked for in a strict subset of positional strategies called the set of f -strategies.

In this section, we describe what are f -strategies.

Informal description of f -strategies

With every permutation f = (r 0 , . . . , r m ) of random vertices V R , we associate a couple σ f , τ f of positional strategies, called the f -strategies. We give intuition about what are f -strategies, before giving their formal construction.

A permutation f = (r 0 , . . . , r m ) of V R intuitively represents preferences of Max and Min over the random vertices: player Max prefers the play to start from a random vertex of index as high as possible, i.e. starting from vertex r l+1 is better for player Max than starting from vertex r l , whereas the opposite holds for player Min.

When both players agree on the preferences given by f , the f -strategies σ f , τ f are natural behaviours of player Max and Min. Indeed, strategy σ f for player Max consists in attracting the pebble either in the target vertex or in a random vertex of index as high as possible in f . By opposite, strategy τ f for player Min consists in keeping the pebble away from the target and from random vertices of high index in f . The f -strategies can be described more precisely, introducing a non-stochastic game. In this non-stochastic game, plays can be either of finite or infinite duration, and after a play, players Max and Min have to give coins to each other. This game is played on the game graph (V, V Max , V Min , E), where all random vertices are terminal vertices. When the play reaches a random vertex r l ∈ V R , the play immediately stops and player Min has to give l coins to Max, where l is the index of the random vertex r l in the permutation f = (r 0 , . . . , r m ). Of course player Min wants to give as few coins as possible to player Max, whereas the goal of player Max is the opposite. The worst for player Min is when the play does not reach a random vertex but reaches the target vertex instead, in that case player Min has to give m + 1 coins to Max. The best for player Min is the remaining case, when the play never reaches any random vertex nor the target, then instead of giving coins to Max player Min receives 1 coin from player Max. In this game there exist positional optimal strategies σ f and τ f for both players. These strategies are precisely the f -strategies. This intuitive interpretation of f -strategies is depicted on Figure 2.1, for the permutation (1, 2, 3, 4, 5).

In the rest of this section, we define formally the notion of f -strategies. For this we need to introduce in the next subsection the notion of deterministic attractor. Fig. 2. The permutation is f = (1, 2, 3, 4, 5). Edges consistent with f -strategies are black, other edges are dotted. For example from vertex a, player Min prefers moving the pebble on vertex b than on the target vertex t. Indeed in the former case player Min has to pay 5 coins to Max whereas in the latter case he would have to pay 6 coins.

Deterministic attractors

Let W ⊆ V be a subset of vertices. The deterministic attractor in W is the set of vertices Att(W ) ⊆ V from which Max has a strategy for attracting the play in W and avoiding at the same time any visit to a random vertex before the first visit to W . An attraction strategy in W is a positional strategy σ # for Max which guarantees that every play starting from Att(W ) has this property.

A trapping strategy out of W is a positional strategy τ # for player Min which guarantees than any play starting outside Att(W ) will avoid a visit to W before the first visit to a random vertex. These notions are formalized in the following proposition.

Proposition 1. Let W ⊆ V be a subset of vertices. There exists a subset Att(W ) called the deterministic attractor in W , a positional strategy σ # for Max called the attraction strategy in W and a positional strategy τ # for Min called the trapping strategy out of W such that:

1. For every v 0 ∈ Att(W ), for every play

v 0 v 1 • • • ∈ V ω consistent with σ # , there exists n ∈ N such that v n ∈ W and for every 0 ≤ k < n, v k ∈ V R . 2. For every v 0 ∈ Att(W ), for every play v 0 v 1 • • • ∈ V ω consistent with τ # , for every n ∈ N, if v n ∈ Att(W ) then there exists 0 ≤ k < n such that v k ∈ V R .
There exists an algorithm that computes Att(W ), σ # and τ # in time O(|E|•|V |).

Computing the f -strategies

We now describe formally how to compute the f -strategies σ f , τ f associated with a permutation f = (r 0 , . . . , r m ) of random vertices. Intuitively, the strategy σ f for Max consists in attracting the play in the target vertex t or in a random vertex whose index is as high as possible in f , while the strategy τ f for Min aims at the opposite.

We start with defining a sequence W -, W 0 , . . . , W m+1 of subsets of V :

W m+1 = Att({t}) , for all 0 ≤ l ≤ m, W l = Att({r l , r l+1 , . . . , r m , t}) , (6)
W -= V \ W 0 .
An example is given on Figure 2, where relative frontiers of the sets W -, W 0 , . . . , W m+1 are delimited by gray lines. On this example, the set W m+1 only contains the target vertex t, the set W 5 is {a, b, 5, t}, the set W -is the singleton {c}.

The f -strategies are constructed by combining different positional strategies together. Let σ m+1 be the attraction strategy in {t}, then on W m+1 σ f coincides with σ m+1 and τ f is any positional strategy. For 0 ≤ l ≤ m, let σ l be the attraction strategy in {r l , r l+1 , . . . , r m , t} and let τ l be the trapping strategy out of {r l+1 , . . . , t}, then on W l \ W l+1 σ f coincides with σ l and τ f coincides with τ l . Let τ -be the trapping strategy out of {r 0 , . . . , r m , t}, then on W -= V \ W 0 , τ f coincides with τ -and σ f is any positional strategy.

We will use the following properties of f -strategies:

Lemma 1. Let f = (r 0 , . . . , r m ) a permutation of random vertices. Every play consistent with σ f and starting from W m+1 stays in W m+1 and reaches the target vertex t. Every play consistent with τ f and starting from W -stays in W -and never reaches t. Let φ : V → R defined by φ(v) = P σ f ,τ f v (Reach(t)). For every 0 ≤ l ≤ m, for every v ∈ W l \ W l+1 , φ(v) = φ(r l ).

Optimality of f-strategies

A key property of f -strategies is given in the following theorem.

Theorem 2. In every SSG, there exists a permutation f of random vertices such that the f -strategies σ f and τ f are optimal. This theorem suggests the following algorithm for solving SSGs. It consists in testing, for each possible permutation f of random vertices, whether the fstrategies are optimal. Since f -strategies are positional, their optimality can be tested in polynomial time using linear programming [START_REF] Derman | Finite State Markov Decision Processes[END_REF][START_REF] Condon | The complexity of stochastic games[END_REF]. Finally, the corresponding algorithm can find values and optimal strategies solving at most |V R |! linear programs.

Testing optimality of f -strategies can be done in a more elegant and efficient way, without making use of linear programming. Indeed, Theorem 3 shows that it is sufficient to test whether the f -strategies are self-consistent and progressive, in the following sense.

Definition 1 (Self-consistent and progressive permutations). Let f = (r 0 , . . . , r m ) be a permutation of random vertices and σ f and τ f the f -strategies.

For v ∈ V , let φ(v) = P σ f ,τ f v (Reach(t)). Permutation f is self-consistent if φ(r 0 ) ≤ φ(r 1 ) ≤ . . . ≤ φ(r m ) . ( 7
)
Permutation f is progressive if for every 0 ≤ i ≤ j ≤ m, if φ(r i ) > 0 then there exists w ∈ Att({r j+1 , . . . , r m , t}) such that p(w|r j ) > 0.

Both properties can be reformulated in term of the Markov chain induced by σ f and τ f , see Proposition 2.

Intuitively, both players use their f -strategies when they both agree on the preference order given by f and play consistently with this preference order. Self-consistency states that plays starting from random vertices of higher rank in f have greater probabilities of reaching the target. The progressive property states that if some random vertex r i gives non-zero probability to reach the target, then, from every random vertex r j of higher rank in f , also with non-zero probability either the target vertex or a random vertex of higher rank than r j will be reached prior to any visit to a random vertex.

Next theorem states that together with self-consistency, the progressive property ensures optimality of the f -strategies.

Theorem 3. Let f be a permutation of random vertices. If f is self-consistent and progressive then the f -strategies σ f and τ f are optimal. Moreover there exists a permutation f of random vertices which is self-consistent and progressive.

Notice that self-consistency alone is not sufficient for ensuring that f -strategies are optimal, a counter-example is given on Figure 3.

The progressive property forces any wrong guess about preferences of the players to propagate among random vertices and to lead to a violation of selfconsistency. Somehow, the progressive property plays a role similar to the halting hypothesis used in [START_REF] Condon | The complexity of stochastic games[END_REF]. The halting hypothesis states that any play of the SSG should reach a sink vertex, which ensures uniqueness of a solution to the local optimality equations, see [START_REF] Condon | The complexity of stochastic games[END_REF] for more details.

An algorithm for solving SSGs and based on Theorem 3 is described in the next section. The rest of this section is dedicated to the proof of Theorem 3, which relies on a few preliminary lemmas.

Under the hypothesis that f is self-consistent, first lemma states that during a play consistent with σ f , the values of vertices relatively to f -strategies is a super-martingale, and symmetrically for player Min.

Lemma 2. Let f a permutation of V R and σ f , τ f the f -strategies. Let φ : V → R defined by φ(v) = P σ f ,τ f v (Reach(t)). Suppose f is self-consistent.
Then for every strategies σ, τ for Max and Min, for every v ∈ V and n ∈ N,

E σ f ,τ v [ φ(V n+1 ) | V 0 • • • V n ] ≥ φ(V n ) , (8)
E σ,τ f v [ φ(V n+1 ) | V 0 • • • V n ] ≤ φ(V n ) . (9) r 2 v r 1 t - r 2 r 1 t 1 2 1 2 1 2 1 2 1 1 1 2 1 2 1 2 1 2
Fig. 3. On the left is depicted an SSG with two random vertices {r1, r2}, a Min vertex v and the target vertex t. Player Min has only one optimal strategy: moving the pebble to vertex r1 whenever it is on v, this way the play never reaches the target vertex t. This is exactly the f -strategy τ f associated with the permutation f = (r1, r2). Suppose now the permutation is f = (r2, r1), then following its f -strategy τ f , player Min will go to vertex r2 from v. In that case, t is reached from both r1 and r2 with probability 1, hence permutation (r2, r1) is self-consistent, although strategy τ f is not optimal. However f is not progressive since from r1 the play reaches r2 before reaching t. On the right is depicted the Markov chain M f associated with f = (r2, r1).

Under the hypothesis that f is progressive, next lemma gives a necessary and sufficient condition for a play consistent with σ f to reach the target vertex.

Lemma 3. Let f be a permutation of V R and σ f , τ f the f -strategies. Let φ : V → R defined by φ(v) = P σ f ,τ f v (Reach(t)). Suppose f is progressive. Then for every vertex v ∈ V and every strategy τ for Min:

P σ f ,τ v Reach(t)   φ(Vn) > 0 for infinitely many n ∈ N = 1 . ( 10
)
Next lemma is the main ingredient for constructing iteratively a self-consistent and progressive permutation.

Lemma 4. Let X ⊆ V be a subset of vertices of an SSG and let W = Att(X). Suppose W contains the target vertex. Then either all vertices v ∈ V \ W have value 0 in the SSG or there exists a random vertex r ∈

V R ∩ (V \ W ) such that val(r) = max{val(v) | v ∈ V \ W } and v∈W p(v|r) > 0.
We now give a proof of Theorem 3.

Proof (of Theorem 3).

We start with proving that if f is self-consistent and progressive then σ f and τ f are optimal. Let v ∈ V and σ, τ be some strategies for Max and Min.

We first prove that starting from v, σ f ensures to reach t with probability at least P σ f ,τ f v (Reach(t)):

P σ f ,τ v (Reach(t)) ≥ P σ f ,τ v (φ(V n ) > 0 for infinitely many n ∈ N) ≥ E σ f ,τ v lim sup n∈N φ(V n ) ≥ lim sup n∈N E σ f ,τ v [φ(V n )] ≥ E σ f ,τ v [φ(V 0 )] = φ(v) = P σ f ,τ f v (Reach(t)) , (11)
where the first inequality comes from Lemma 3, the second because values of φ are between 0 and 1, the third is a property of expectations, the fourth comes from Lemma 2 and the last two equalities hold because V 0 is equal to the starting vertex v and by definition of φ.

We now prove that starting from v, τ f ensures to reach t with probability no more than P σ f ,τ f v (Reach(t)):

P σ,τ f v (Reach(t)) ≤ P σ,τ f v lim inf n∈N φ(V n ) = 1 ≤ E σ,τ f v lim inf n∈N φ(V n ) ≤ lim inf n∈N E σ,τ f v [φ(V n )] ≤ E σ,τ f v [φ(V 0 )] = φ(v) = P σ f ,τ f v (Reach(t)) , (12)
where the first inequality holds because t is an absorbing state and φ(t) = 1, the second holds because values of φ are between 0 and 1, the third is a property of expectations, the fourth comes from Lemma 2 and the two last equalities hold because V 0 is equal to the starting vertex v and by definition of φ.

Finally, (11) and (12) together prove that σ f and τ f are optimal.

We now prove the existence of a permutation f which is self-consistent and progressive. For a set W and a random vertex r ∈ V R we denote p(W |r) = w∈W p(w|r) the probability of going to W from r. We build a self-consistent and progressive permutation f = (r 0 , r 1 , . . . , r m ) by iteration of the following iterative step.

Let 0 ≤ l ≤ m, suppose that vertices (r l+1 , . . . , r m ) have already been chosen, let X l+1 = {r l+1 , . . . , r m , t} and let W l+1 = Att(X l+1 ). If l > 0 and all vertices in V \ W l+1 have value 0, choose r l to be any random vertex in V R \ X l+1 . Otherwise, according to Lemma 4, there exists a random vertex r l in V \ W l+1 whose value is maximal in V \ W l+1 and such that p(W l+1 |r l ) > 0 .

(

) 13
This achieves the inductive step. Let f = (r 0 , r 1 , . . . , r m ) be a permutation built according to this iterative procedure, we now prove that f is self-consistent and progressive.

By construction of f ,

val(r 0 ) ≤ . . . ≤ val(r n ) . ( 14
)
By definition of the f -strategies, for any 0 ≤ l ≤ m: (A) σ f coincides on W l \ W l+1 with an attraction strategy in {r l , . . . , r m , t}, (B) τ f coincides on W l \ W l+1 with a trapping strategy out of {r l+1 , . . . , r m , t}, (C) σ f coincides on W m+1 with an attraction strategy in {t}, (D) τ f coincides on W -= V \ W 0 with a trapping strategy out of W 0 , (E) any play consistent with τ f starting form a vertex of value 0 stays in the set of vertices of value 0.

We start with proving that f is progressive. Let 0 ≤ k ≤ m such that P σ f ,τ f r k (Reach(t)) > 0. According to (E), val(r k ) > 0, hence according to (14), for every k ≤ l ≤ m, val(r l ) > 0. Hence, for every k ≤ l ≤ m, eq. ( 13) holds, which proves that f is progressive. Now we prove that f is self-consistent. According to (14), for proving that f is self-consistent it is enough to prove that for any 0 ≤ l ≤ m,

P σ f ,τ f r l (Reach(t)) = val(r l ) . ( 15
)
We start with proving for every 0 ≤ l ≤ m,

val is constant equal to val(r l ) on W l \ W l+1 . (16)
Let 0 ≤ l ≤ m and v ∈ W l \ W l+1 . According to (A), σ f guarantees any play starting from v to reach set {r l , . . . , r m , t} hence val(v) ≥ min{val(r l ), . . . , val(r m ), val(t)}, and together with (14) we get val(v) ≥ val(r l ). The converse inequality holds because according to (B), strategy τ f guarantees any play starting from v to either stay forever in V \W l+1 and never reach t or to reach a random vertex in {r 0 , . . . , r l }, hence val(v) ≤ max{val(r 0 ), . . . , val(r l )} = val(r l ). This achieves to prove (16). Now we prove that for every v, w ∈ V ,

E σ f ,τ f v [val(V n+1 ) | V n = w] = val(w) . (17)
According to (C), val is constant equal to 1 on W m+1 and W m+1 is stable under σ f and τ f hence (17) holds for w ∈ W m+1 . According to (D), val is constant equal to 0 on W -and W -is stable under σ f and τ f hence (17) holds for w ∈ W -. Let 0 ≤ l ≤ m and w ∈ W l \ W l+1 . According to (16), val is constant on W l \ W l+1 and according to (A) and (B), W l \ W l+1 is stable under σ f and τ f , hence (17 17) also holds because w = t hence according to (5), val(w) = v∈V p(v|w) • val(v). Now we prove that for any v ∈ V ,

) holds if w ∈ V Max ∪ V Min . If w ∈ V R then (
(P σ f ,τ f v (Reach(t)) = 0) =⇒ (val(v) = 0) . ( 18
) For every v ∈ V let φ(v) = P σ f ,τ f v (Reach(t)). Let Z = {v ∈ V | φ(v) = 0}.
We start with proving that Z = V \ W l for some l. According to Lemma 1, for each 0 ≤ l ≤ m, the value of φ is constant equal to φ(w l ) on the set W l \ W l+1 . Since φ has value 0 on V \ W 0 , and since W 0 ⊆ W 1 ⊆ . . . ⊆ W m+1 , there exists 0 ≤ l ≤ m such that Z = V \ W l . Now we prove that Z is stable under random moves. Indeed, let r ∈ V R ∩ Z then since φ(r) = v∈V p(v|r)φ(v) and since r ∈ Z, φ(r) = 0, hence all successors of r have value 0 and are in Z. Now we prove that τ f guarantees that every play starting from Z never leaves Z. Indeed according to (B), strategy τ f traps the play in V \ W l+1 = Z until it reaches a random vertex, but Z is stable under random moves. Finally, since Z does not contain the target, any play consistent with strategy τ f and starting from Z will never reach the target. This proves that vertices in Z have value 0 and achieves the proof of (18). Now we can achieve the proof that f is self-consistent. We already proved that f is progressive hence according to Lemma 3, there are two types of play consistent with σ f : those reaching the target and those staying ultimately in the set where φ has value 0. In the former case, since t is absorbing, lim n val(V n ) = 1 and in the latter case according to (18), lim n val(V n ) = 0. Hence:

P σ f ,τ f v (Reach(t)) = E σ f ,τ f v lim n n ) = lim n E σ f ,τ f v [val(V n )] = val(v) ,
where the second equality holds because val is bounded and the third comes from (17). This proves (15) and achieves the proof that f is self-consistent.

An algorithm for computing values of SSGs

In this section, we give an algorithm that computes values and optimal strategies of an SSG. This algorithm, based on Theorem 3, looks for a permutation f which is self-consistent and progressive.

Testing whether a permutation is self-consistent and progressive

For testing whether a permutation f is self-consistent and progressive, it is enough to compute some reachability probabilities in the following Markov chain.

Definition 2 (Markov chain associated with f ). Let f = (r 0 , . . . , r m ) a permutation of V R , and W -, W 0 , . . . , W m+1 the subsets of V defined by (6). Let M f be the Markov chain with states S = {-, 0, . . . , m, m + 1} such that both states -and m + 1 are absorbing and for every i ∈ {0, . . . , m} and j ∈ S, the transition probability from i to j in M f is given by:

x i,j = v∈Wj p(v|r i ) .
The Markov chain M f is designed to mimic behaviour of the play when the players use their f -strategies: it is obtained by removing edges which are not consistent with f -strategies and shrinking each set W l to the vertex r l .

The following proposition gives an effective procedure for testing self-consistency and progressiveness of a permutation. Proposition 2. Let f = (r 0 , . . . , r m ) be a permutation of random vertices, with |V R | = m + 1. Let M f the Markov chain associated with f , with transition probabilities (x i,j ) i,j∈S . For 0 ≤ i ≤ m, let x * i the probability of eventually reaching state m + 1 starting from state i in the Markov chain M f . Then f is selfconsistent iff for every 0 ≤ i, j ≤ m,

(i ≤ j) =⇒ (x * i ≤ x * j ) , (19)
and f is progressive iff for every 0 ≤ i ≤ j ≤ m, (x * i > 0) =⇒ (there exists j < k ≤ m + 1 such that x j,k > 0) .

Let I ⊆ S the set of states from which m + 1 is reachable in M f i.e. such that x * i > 0. Then (x * i ) i∈I is the unique solution of the following linear system:

x * i = j∈I x i,j • x * j , (i ∈ I \ {m + 1}) x * m+1 = 1 . ( 21
)
Proof. Uniqueness of a solution of the linear system (21) is proven for example in [START_REF] Condon | The complexity of stochastic games[END_REF], Lemma 1. Bringing together results about optimality of f -strategies and characterization of self-consistent and progressive permutations given by Proposition 2, we obtain an algorithm for solving SSG: This algorithm enumerates all possible permutations f of V R . For each permutation, the algorithm tests whether f is self-consistent and progressive. This is done by computing the sets W -, W 0 , . . . , W m , W m+1 defined by (6), computing the transition probabilities (x i,j ) i,j∈S of the Markov chain M f associated with f , solving the linear system (21) and testing conditions (19) and (20). If the permutation fails the test then the algorithm proceeds to the next permutation. If the permutation passes the test, then the algorithm outputs the f -strategies and the mapping val : V → [0, 1] which associates 0 to the vertices in W -, 1 to the vertices in W m+1 and x * l to the vertices in W l , 0 ≤ l ≤ m. The correction of the algorithm comes from Theorem 3, which ensures the existence of a self-consistent and progressive permutation f and the optimality of f -strategies associated with any such permutation. Proposition 2 validates the procedure used for testing self-consistency and progressiveness.

The

Conclusion

We presented an algorithm computing values and optimal strategies of an SSG in time O( |V R |!•(|V ||E|+|p|) ). Our algorithm is particularly efficient for the SSGs with few random vertices and does not rely on quadratic or linear programming solvers.

A natural way of improving our algorithm would be to design a smart way of updating a permutation f in case it is not self-consistent or progressive, this way one would obtain a new kind of strategy improvement algorithm for solving SSGs.

Fig. 1 .

 1 Fig. 1. A Simple Stochastic Game.

  known so far run in sub-exponential expected time e O( √ n) . Our results. In this paper we present an algorithm that computes values and optimal strategies of an SSG in time O( |V R |! • (|V ||E| + |p|) ), where |V R | is the number of random vertices, |V | is the number of vertices and |p| is the maximal bit-length of transition probabilities.

4. 2

 2 Solving SSGs in time O( |V R |! • (|V ||E| + |p|) )

Theorem 4 .

 4 Values and optimal strategies of a simple stochastic gameG = (V, V Max , V Min , V R , E, t, p) are computable in time O( |V R |!•(|V ||E|+|p|) ), where |p| is the maximal bit-length of a transition probability in p.

  complexity of the algorithm is O( |V R |! • (|V ||E| + |p|) ). Indeed, there are exactly |V R |! permutations of random vertices. For each permutation f , the algorithm builds the Markov chain M f . This is done by computing the deterministic attractors W m+1 , . . . , W -, which according to Proposition 1 takes time O(|E||V |). Then the algorithms solves the linear system (21), which can be done in time |V R | 3 |p|, see [Dix82]. The two tests (19) and (20) can be performed in time O(|V R |).

⋆ This research was partially supported by french project ANR "DOTS".