Thomas Brihaye
email: thomas.brihaye@umons.ac.be

Gilles Geeraerts
email: gilles.geeraerts@ulb.ac.be

Axel Haddad
email: axel.haddad@umons.ac.be

Benjamin Monmege
email: benjamin.monmege@lif.univ-mrs.fr

Pseudopolynomial Iterative Algorithm to Solve Total-Payoff Games and Min-Cost Reachability Games

Introduction

Games played on graphs are nowadays a well-studied and well-established model for the computer-aided design of computer systems, as they enable automatic synthesis of systems that are correct-by-construction. Of particular interest are quantitative games, that allow one to model precisely quantitative parameters of the system, such as energy consumption. In this setting, the game is played by two players on a directed weighted graph, where the edge weights model, for instance, a cost or a reward associated with the moves of the players. Each vertex of the graph belongs to one of the two players who compete by moving a token along the graph edges, thereby forming an infinite path called a play. With each play is associated a real-valued payoff computed from the sequence of edge weights along the play. The traditional payoffs that have been considered in the literature include total-payoff [START_REF] Gimbert | When can you play positionally?[END_REF], mean-payoff [START_REF] Ehrenfeucht | Positional strategies for mean payoff games[END_REF]) and discounted-payoff [START_REF] Zwick | The complexity of mean payoff games[END_REF]. In this quantitative setting, one player aims at maximising the payoff while the other tries to minimise it. So one wants to compute, for each player, the best payoff that he can guarantee from each vertex, and the associated optimal strategies (i.e. that guarantee the optimal payoff no matter how the adversary is playing).

Such quantitative games have been extensively studied in the literature. Their associated decision problems (is the value of a given vertex above a given threshold? ) are known to be in NP∩co-NP. Mean-payoff games have arguably been best studied from the algorithmic point of view. A landmark is Zwick and Paterson's pseudopolynomial time (i.e. polynomial in the weighted graph when weights are encoded in unary) algorithm [START_REF] Zwick | The complexity of mean payoff games[END_REF], using the value iteration paradigm that consists in computing a sequence of vectors of values that converges towards the optimal values of the vertices. After a fixed, pseudo-polynomial, number of steps, the computed values are precise enough to deduce the actual values of all vertices. Better pseudo-polynomial time algorithms have later been proposed, e.g., by Björklund and Vorobyov (2007); [START_REF] Brim | Faster algorithms for mean-payoff games[END_REF]; [START_REF] Comin | An improved pseudo-polynomial upper bound for the value problem and optimal strategy synthesis in mean payoff games[END_REF], also achieving sub-exponential expected running time by means of randomisation.

In this paper, we focus on total-payoff games 1 . Given an infinite play π, we denote by π[k] the prefix of π of length k, and by TP(π[k]) the (finite) sum of all edge weights along this prefix. The total-payoff of π, TP(π), is the inferior limit of all those sums, i.e. TP(π) = lim inf k→∞ TP(π[k]). Compared to mean-payoff (and discounted-payoff) games, the literature on total-payoff games is less extensive. [START_REF] Gimbert | When can you play positionally?[END_REF] have shown that optimal memoryless strategies always exist for both players and the best algorithm to compute the values runs in exponential time [START_REF] Gawlitza | Games through nested fixpoints[END_REF], and consists in iteratively improving strategies. Other related works include energy games where one player tries to optimise its energy consumption (computed again as a sum), keeping the energy level always above 0. Note that it differs in essence from total-payoff games where no condition on the energy level is required: in particular, the optimal total-payoff could be negative, and even -∞, and it is a priori not possible to simply lift all the weights by a constant to solve total-payoff games by solving a related energy games. Moreover, this difference makes difficult to apply techniques solving energy games in the case of total-payoff games. Probabilistic variants of total-payoff games have also been studied, but the weights are restricted to be non-negative [START_REF] Chen | Automatic verification of competitive stochastic systems[END_REF].

We argue that the total-payoff objective is interesting as a refinement of the mean-payoff. Indeed, recall first that the total-payoff is finite if and only if the mean-payoff is null. Then, the computation of the total-payoff enables a finer, two-stage analysis of a game G: (i) compute the mean payoff MP(G); (ii) subtract MP(G) from all edge weights, and scale the resulting weights if necessary to obtain integers. At that point, one has obtained a new game G with null mean-payoff; (iii) compute TP(G ) to quantify the amount of fluctuation around the mean-payoff of the original game. Unfortunately, so far, no efficient (i.e. pseudo-polynomial time) algorithms for total-payoff games have been proposed, and straightforward adaptations of Zwick and Paterson's value iteration algorithm for mean-payoff do not work, as we demonstrate at the end of Section 2. In the present article, we fill in this gap by introducing the first pseudo-polynomial time algorithm for computing the values in total-payoff games.

Our solution is a non-trivial value iteration algorithm that proceeds through nested fixed points (see Algorithm 2). A play of a total-payoff game is infinite by essence. We transform the game so that one of the players (the minimiser) must ensure a reachability objective: we assume that the game ends once this reachability objective has been met. The intuition behind this transformation, that stems from the use of an inferior limit in the definition of the total-payoff, is as follows: in each play π whose total-payoff is finite, there is a position in the play after which all the partial sums TP(π[i]) (with i

) will be larger than or equal to the total-payoff TP(π) of π, and infinitely often both will be equal. For example, consider the game depicted in Fig. 1(a), where the maximiser player (henceforth called Max) plays with the round vertices and the minimiser (Min) with the square vertices. For both players, the optimal value when playing from v 1 is 2, and the play π = v 1 v 2 v 3 v 4 v 5 v 4 v 3 (v 4 v 5 ) ω reaches this value (i.e. TP(π) = 2). Moreover, for all k 7: TP(π[k]) TP(π), and infinitely many prefixes (π[8], π[10], π[12], . . .) have a total-payoff of 2, as shown in Fig. 1(b).

Based on this observation, we transform a total-payoff game G, into a new game that has the same value as the original total-payoff game but incorporates a reachability objective for Min. Intuitively, in this new game, we allow a new action for Min: after each play prefix π[k], he can ask to stop the game, in which case the payoff of the play is the payoff TP(π[k]) of the prefix. However, allowing Min to stop the game at every moment would not allow us to obtain the same value as in the original total-payoff game: for instance, in the example of Fig. 1(a), Min could secure value 1 by asking to stop after π[2], which is strictly smaller that the actual total-payoff (2) of the whole play π. So, we allow Max to veto to stop the game, in which case both must go on playing. Again, allowing Max to turn down all of Min's requests would be unfair, so we parametrise the game with a natural number K, which is the maximal number of vetoes that Max can play (and we denote by G K the resulting game). For the play depicted in Fig. 1(b), letting K = 3 is sufficient: trying to obtain a better payoff than the optimal, Min could request to stop after π [START_REF]By definition of σ Min , t = argmin v ∈E(in,v) ω (in, v), v + Val G Val G (v ) . In particular, for v = v, as ω (in, v), v = 0[END_REF], π [2] and π[6], and Max can veto these three requests. After that, Max can safely accept the next request of Min, since the total payoff of all prefixes π[k] with k 6 are larger than or equal to TP(π) = 2. Our key technical contribution is to show that for all total-payoff games, there exists a finite, pseudo-polynomial, value of K such that the values in G K and G coincide (assuming all values are finite in G: we treat the +∞ and -∞ values separately). Now, assume that, when Max accepts to stop the game (possibly because he has exhausted the maximal number K of vetoes), the game moves to a target vertex, and stops. By doing so, we effectively reduce the computation of the values in the total-payoff game G to the computation of the values in the total-payoff game G K with an additional reachability objective (the target vertex) for Min.

In the following, such refined total-payoff games-where Min must reach a designated target vertex-will be called min-cost reachability games. Failing to reach the target vertices is the worst situation for Min, so the payoff of all plays that do not reach the target is +∞, irrespective of the weights along the play. Otherwise, the payoff of a play is the sum of the weights up to the first occurrence of the target. As such, this problem nicely generalises the classical shortest path problem in a weighted graph. In the one-player setting (considering the point of view of Min for instance), this problem can be solved in polynomial time by Dijkstra's and Floyd-Warshall's algorithms when the weights are non-negative and arbitrary, respectively. [START_REF] Khachiyan | On short paths interdiction problems: Total and node-wise limited interdiction[END_REF] propose an extension of Dijkstra's algorithm to handle the two-player, non-negative weights case. However, in our more general setting (two players, arbitrary weights), this problem has, as far as we know, not been studied as such, except that the associated decision problem is known to be in NP ∩ co-NP [START_REF] Filiot | Quantitative languages defined by functional automata[END_REF]. A pseudo-polynomial time algorithm to solve a very close problem, called the longest shortest path problem has been introduced by Björklund and Vorobyov (2007) to eventually solve mean-payoff games. However, because of this peculiar context of mean-payoff games, their definition of the length of a path differs from our definition of the payoff and their algorithm can not be easily adapted to solve our min-cost reachability problem. Thus, as a second contribution, we show that a value iteration algorithm enables us to compute in pseudo-polynomial time the values of a min-cost reachability game. We believe that min-cost reachability games bear their own potential theoretical and practical applications2 . Those games are discussed in Section 3. In addition to the pseudo-polynomial time algorithm to compute the values, we show how to compute optimal strategies for both players and characterise them: there is always a memoryless strategy for the maximiser player, but we exhibit an example (see Fig. 2) where the minimiser player needs (finite) memory. Those results on mincost reachability games are exploited in Section 4 where we introduce and prove correct our efficient algorithm for total-payoff games.

v 4 v 3 v 5 v 2 v 1 -2 -1 2 1 2 -1 -1 (
Finally, we briefly present our implementation in Section 5, using as a core the numerical model-checker PRISM. This allows us to describe some heuristics able to improve the practical performances of our algorithms for total-payoff games and min-cost reachability games on certain subclasses of graphs.

Quantitative games with arbitrary weights

In this section, we formally introduce the game model we consider throughout the article.

We denote by Z the set of integers, and Z∞ = Z∪{-∞, +∞}. The set of vectors indexed by V with values in S is denoted by S V . We let be the pointwise order over Z V ∞ , where x y if and only if x(v) y(v) for all v ∈ V .

Games played on graphs

We consider two-player turn-based games played on weighted graphs and denote the two players by Max and Min. A weighted graph is a tuple V, E, ω where V = V Max V Min is a finite set of vertices partitioned into the sets V Max and V Min of Max and Min respectively, E ⊆ V × V is a set of directed edges, ω : E → Z is the weight function, associating an integer weight with each edge. In our drawings, Max vertices are depicted by circles; Min vertices by rectangles. For every vertex v ∈ V , the set of successors of v with respect to E is denoted by

E(v) = {v ∈ V | (v, v ) ∈ E}.
= v 0 v 1 • • • v k ∈ V * such that for all 0 i < k, (v i , v i+1 ) ∈ E. A play is an infinite sequence of vertices π = v 0 v 1 • • • such that every finite prefix v 0 • • • v k , denoted by π[k], is a finite play. The total-payoff of a finite play π = v 0 v 1 • • • v k is obtained by summing up the weights along π, i.e. TP(π) = k-1 i=0 ω(v i , v i+1 ).
In the following, we sometimes rely on the mean-payoff to obtain information about total-payoff objectives. The meanpayoff computes the average weight of

π, i.e. if k 1, MP(π) = 1 k k-1 i=0 ω(v i , v i+1 ),
and MP(π) = 0 when k = 0. These definitions are lifted to infinite plays as follows. The total-payoff of a play π is given by TP(π) = lim inf k→∞ TP(π[k]). 3 Similarly, the mean-payoff of a play π is given by MP(π) = lim inf k→∞ MP(π[k]). Tuples V, E, ω, TP and V, E, ω, MP , where V, E, ω is a weighted graph, are called total-payoff and mean-payoff games respectively.

Strategies and values

A strategy for Max (respectively, Min) in a game G = V, E, ω, P (with P one of the previous payoffs), is a mapping σ :

V * V Max → V (σ : V * V Min → V ) such that for all sequences π = v 0 • • • v k with v k ∈ V Max (v k ∈ V Min ), it holds that (v k , σ(π)) ∈ E. A play or finite play π = v 0 v 1 • • • conforms to a strategy σ of Max (respectively, Min) if for all k such that v k ∈ V Max (v k ∈ V Min ), we have that v k+1 = σ(π[k]). A strategy σ is memoryless if for all finite plays π, π , we have that σ(πv) = σ(π v) for all v ∈ V .
A strategy σ is said to be finite-memory if it can be encoded in a deterministic Moore machine, M, m 0 , up, dec , where M is a finite set representing the memory of the strategy, with an initial memory content m 0 ∈ M , up : M × V → M is a memory-update function, and dec : M × V → V a decision function such that for every finite play π and vertex v, σ(πv) = dec(mem(πv), v) where mem(π) is defined by induction on the length of the finite play π as follows: mem(v 0 ) = m 0 , and mem(πv) = up(mem(π), v). In this case, we say that |M | is the size of the strategy.

For all strategies σ Max and σ Min , for all vertices v, we let Play(v, σ Max , σ Min ) be the outcome of σ Max and σ Min , defined as the unique play conforming to σ Max and σ Min and starting in v. Naturally, the objective of Max is to maximise its payoff. In this model of zero-sum game, Min then wants to minimise the payoff of Max. Formally, we let Val G (v, σ Max ) and Val G (v, σ Min ) be the respective values of the strategies, defined as (recall that P is either TP or MP):

Val G (v, σ Max ) = infσ Min P(Play(v, σ Max , σ Min )) and Val G (v, σ Min ) = sup σ Max P(Play(v, σ Max , σ Min )). Fi- nally, for all vertices v, we let Val G (v) = sup σ Max Val G (v, σ Max ) and Val G (v) = infσ Min Val G (v,
v: Val G (v, σ Max ) = Val G (v) and Val G (v, σ Min ) = Val G (v)
respectively. We say that a game G is determined if for all vertices v, its lower and upper values are equal. In that case, we write

Val G (v) = Val G (v) = Val G (v)
, and refer to it as the value of v in G. If the game is clear from the context, we may drop the index G from all previous notations. Mean-payoff and total-payoff games are known to be determined, with the existence of optimal memoryless strategies [START_REF] Zwick | The complexity of mean payoff games[END_REF][START_REF] Gimbert | When can you play positionally?[END_REF].

Previous works and contribution

Total-payoff games have been mainly considered as a refinement of mean-payoff games [START_REF] Gimbert | When can you play positionally?[END_REF]. Indeed, if the mean-payoff value of a game is positive (respectively, negative), its total-payoff value is necessarily +∞ (-∞). When the mean-payoff value is 0 however, the total-payoff is necessarily different from +∞ and -∞, hence total-payoff games are particularly useful in this case, to refine the analysis of the game. Deciding whether the total-payoff value of a vertex is positive can be achieved in NP ∩ co-NP. [START_REF] Gawlitza | Games through nested fixpoints[END_REF] refined the complexity to UP ∩ co-UP, and values are shown to be effectively computable solving nested fixed point equations with a strategy iteration algorithm working in exponential time in the worst case. Because of this strong relationship between mean-payoff games and total-payoff games, we can show that total-payoff games are, in some sense, as hard as mean-payoff games, for which the existence of a (strongly) polynomial time algorithm is a long-standing open question.

In this article, we improve on this state-of-the-art and introduce the first (to the best of our knowledge) pseudo-polynomial time algorithm for total-payoff games. In many cases, (e.g., mean-payoff games), a successful way to obtain such an efficient algorithm is the value iteration paradigm. Intuitively, value iteration algorithms compute successive approximations x 0 , x 1 , . . . , x i , . . . of the game value by restricting the number of turns that the players are allowed to play: x i is the vector of optimal values achievable when the players play at most i turns. The sequence of values is computed by means of an operator F, letting x i+1 = F(x i ) for all i. Good properties (Scott-continuity and monotonicity) of F ensure convergence towards its smallest or greatest fixed point (depending on the value of x 0 ), which, in some cases, is the value of the game.

Let us briefly explain why, unfortunately, a straightforward application of this approach fails with total-payoff games. In our case, the most natural operator F is such that

F(x)(v) = max v ∈E(v) ω(v, v ) + x(v ) for all v ∈ V Max and F(x)(v) = min v ∈E(v) ω(v, v ) + x(v ) for all v ∈ V Min .
Indeed, this definition matches the intuition that x N is the optimal value after N turns. Then, consider the example of Fig. 1(a), limited to vertices {v 3 , v 4 , v 5 } for simplicity. Observe that there are two simple cycles with weight 0, hence the total-payoff value of this game is finite. Max has the choice between cycling into one of these two cycles. It is easy to check that Max's optimal choice is to enforce the cycle between v 4 and v 5 , securing a payoff of -1 from v 4 (because of the lim inf definition of TP). Hence, the values of v 3 , v 4 and v 5 are respectively 1, -1 and 0. In this game, we have

F(x) = 2 + x(v 4 ), max(-2 + x(v 3 ), -1 + x(v 5 )), 1 + x(v 4
) , and the vector (1, -1, 0) is indeed a fixed point of F. However, it is neither the greatest nor the smallest fixed point of F. Indeed, it is easy to check that, if x is a fixed point of F, then x + (a, a, a) is also a fixed point, for all constant a ∈ Z ∪ {-∞, +∞}. If we try to initialise the value iteration algorithm with value (0, 0, 0), which could seem a reasonable choice, the sequence of computed vectors is: (0, 0, 0), (2, -1, 1), (1, 0, 0), (2, -1, 1), (1, 0, 0), . . . that is not stationary, and does not even contain (1, -1, 0). Notice that (-∞, -∞, -∞) and (+∞, +∞, +∞) are fixed points, so that they do not allow us to find the correct answer too. Thus, it seems difficult to compute the actual game values with an iterative algorithm relying on the operator F, as in the case of mean-payoff games.4 Notice that, in the previous example, the Zwick and Paterson's algorithm (Zwick and Paterson, 1996) to solve mean-payoff games would easily conclude from the sequence above, since the vectors of interest are then (0, 0, 0), (1, -0.5, 0.5), (0.33, 0, 0), (0.5, -0.25, 0.25), (0.2, 0, 0), . . . indeed converging towards (0, 0, 0), the mean-payoff values of this game.

Instead, as explained in the introduction, we propose a different approach that consists in reducing total-payoff games to min-cost reachability games where Min must enforce a reachability objective on top of his optimisation objective. The aim of the next section is to study these games, and we reduce total-payoff games to them in Section 4.

Min-cost reachability games

In this section, we consider min-cost reachability games (MCR games for short), a variant of total-payoff games where one player has a reachability objective that he must fulfil first, before minimising his quantitative objective (hence the name mincost reachability). Without loss of generality, we assign the reachability objective to player Min, as this will make our reduction from total-payoff games easier to explain. Hence, when the target is not reached along a path, the payoff of this path shall be the worst possible for Min, i.e. +∞. Formally, an MCR game is played on a weighted graph V, E, ω equipped with a target set of vertices

T ⊆ V . The payoff T -MCR(π) of a play π = v 0 v 1 . . . is given by T -MCR(π) = +∞ if the play avoids v 1 v 2 v 3 -W -1 0 0 0 (a)
Fig. 2 An MCR game (with W a positive integer and, v 3 the target) where Min needs memory to achieve its optimal strategy. T , i.e. if for all k 0, v k / ∈ T , and T -MCR(π) = TP(π[k]) if k is the least position in π such that v k ∈ T . Lower and upper values are then defined as in Section 2.

Using an indirect consequence of Martin's theorem [START_REF] Martin | Borel determinacy[END_REF], we can show that MCR games are determined, i.e. that the upper and lower valus always coincide:

Theorem 1 MCR games are determined.

Proof Consider a quantitative game G = V, E, ω, P and a vertex v ∈ V . We will prove the determinacy result by using the Borel determinacy result of [START_REF] Martin | Borel determinacy[END_REF]. First, notice that the payoff mapping T -MCR is Borel measurable since the set of plays with finite T -MCR payoff is a countable union of cylinders. Then, for an integer M , consider Win M to be the set of plays with a payoff less than or equal to M . It is a Borel set, so that the qualitative game defined over the graph V, E, ω with winning condition Win M is determined. We now use this preliminary result to show our determinacy result.

We fix an MCR game and one of its vertices v, and first consider cases where either the lower or the upper values is infinite. Suppose first that Val(v) = -∞. We have to show that Val(v) = -∞ too. Let M be an integer. Since Val(v) < M , we know that for all strategies σ Max of Max, there exists a strategy σ Min for Min, such that P(Play(v, σ Max , σ Min )) M . In particular, Max has no winning strategy in the qualitative game equipped with Win M as a winning condition, hence, by determinacy, Min has a winning strategy, i.e. a strategy σ Min such that every strategy σ Max of Max verifies P(Play(v, σ Max , σ Min ))

M . This exactly means that Val(v) M . Since this holds for every value M , we get that Val(v) = -∞. The proof goes exactly in a symmetrical way to show that Val(v) = +∞ implies Val(v) = +∞.

Consider then the case where both Val(v) and Val(v) are finite values. For the sake of contradiction, assume that Val(v) < Val(v) and consider a real number r strictly in-between those two values. From r < Val(v), we deduce that Min has no winning strategy from v in the qualitative game with winning condition Winr. Identically, from Val(v) < r, we deduce that Max has no winning strategy from v in the same game. This contradicts the determinacy of this qualitative game. Hence,

Val(v) = Val(v).
Example 2 As an example, consider the MCR game played on the weighted graph of Fig. 2, where W is a positive integer and v 3 is the target. We claim that the values of vertices v 1 and v 2 are both -W . Indeed, consider the following strategy for Min: during each of the first W visits to v 2 (if any), go to v 1 ; else, go to v 3 . Clearly, this strategy ensures that the target will eventually be reached, and that either (i) edge (v 1 , v 3 ) (with weight -W ) will eventually be traversed; or (ii) edge (v 1 , v 2 ) (with weight -1) will be traversed at least W times. Hence, in all plays following this strategy, the payoff will be at most -W . This strategy allows Min to secure -W , but he can not ensure a lower payoff, since Max always has the opportunity to take the edge (v 1 , v 3 ) (with weight -W ) instead of cycling between v 1 and v 2 . Hence, Max's optimal choice is to follow the edge (v 1 , v 3 ) as soon as v 1 is reached, securing a payoff of -W . The Min strategy we have just given is optimal, and there is no optimal memoryless strategy for Min. Indeed, always playing (v 2 , v 3 ) does not ensure a payoff -W ; and, always playing (v 2 , v 1 ) does not guarantee to reach the target, and this strategy has thus value +∞.

A remark on related work Let us note that Björklund and Vorobyov (2007) introduce the longest shortest path problem (LSP for short) and propose a pseudopolynomial time algorithm to solve it. However, their definition has several subtle but important differences to ours, such as in the definition of the payoff of a play (equivalently, the length of a path). As an example, in the game of Fig. 2, the play π = (v 1 v 2 ) ω (that never reaches the target) has length -∞ in their setting, while, in our setting, {v 3 }-MCR(π) = +∞. A more detailed comparison of the two definitions is given in Appendix A. Moreover, even if a preprocessing would hypothetically allow one to use the LSP algorithm to solve MCR games, our solution (that has the same worst-case complexity as theirs) is simpler to implement, and we also introduce (see Section 5) heuristics that are only applicable to our value iteration solution.

As explained in the introduction of this section, we show how to solve those games, i.e. how to compute Val(v) for all vertices v in pseudo-polynomial time. This procedure will be instrumental to solving total-payoff games. Our contributions are summarised in the following theorem:

Theorem 3 Let G = V, E, ω, T -MCR be an MCR game.
1. For all v ∈ V , deciding whether Val(v) = +∞ can be done in polynomial time. 2. For v ∈ V , deciding whether Val(v) = -∞ is as hard as solving mean-payoff games, in NP ∩ co-NP and can be achieved in pseudo-polynomial time. 3. If Val(v) = -∞ for all vertices v ∈ V , then both players have optimal strategies. Moreover, Max always has a memoryless optimal strategy, while Min may require finite (pseudo-polynomial) memory in his optimal strategy. 4. Computing all values Val(v) (for v ∈ V ), as well as optimal strategies (if they exist) for both players, can be done in (pseudo-polynomial) time O(|V | 2 |E|W ).

Finding vertices with value +∞

To prove the first item of Theorem 3, it suffices to notice that vertices with value +∞ are exactly those from which Min can not reach the target. Therefore the problem reduces to deciding the winner in a classical reachability game, that can be solved in polynomial time [START_REF] Thomas | On the synthesis of strategies in infinite games[END_REF], using the classical attractor construction.

More precisely, let G = V, E, ω, T -MCR be an MCR game. Notice that for all plays

π = v 0 v 1 • • • , T -MCR(π) = +∞ if and only if v k /
∈ T for all k 0, i.e. π avoids the target. Then, let us show that the classical attractor technique [START_REF] Thomas | On the synthesis of strategies in infinite games[END_REF] allows us to compute the set

V +∞ = {v ∈ V | Val(v) = +∞}.
Recall that the attractor of a set T of vertices is obtained thanks to the sequence Attr 0 (T ), . . . , Attr i (T ), . . . where: Attr 0 (T ) = T ; and for all i 0:

Attr i+1 (T ) = Attr i (T ) ∪ {v ∈ V Min | E(v) ∩ Attr i (T ) = ∅} ∪ {v ∈ V Max | E(v) ⊆ Attr i (T )} .
It is well-known that this sequence converges after at most |V | steps to the set Attr(T ) of all vertices from which Min has a memoryless strategy to ensure reaching T . Hence, under our hypothesis, V +∞ = V \ Attr(T ). This proves the first item of Theorem 3. Observe that we can safely remove from the game graph all vertices v such that Val(v) = +∞, without changing the values of the other vertices. Hence, we can, when need be, assume that the MCR games we consider contain no vertex with value +∞, as they can be removed by this polynomial-time preprocessing.

In those games, one can construct in polynomial time a memoryless strategy, called an attractor strategy, ensuring to reach the target in less than |V | steps from every vertex.

In the following, we assume that all vertices have a value different from +∞. Indeed as described above one can detect in polynomial time the vertices with value +∞ and remove them without changing the values of the other vertices.

Finding vertices with value -∞

To prove the second item, we notice that vertices with value -∞ are exactly those with a value < 0 in the mean-payoff game played on the same graph. On the other hand, we can show that every mean-payoff game can be transformed (in polynomial time) into an MCR game such that a vertex has value < 0 in the mean-payoff game if and only if the value of its corresponding vertex in the MCR game is -∞. More precisely:

Proposition 4 1. For all MCR games G = V, E, ω, T -MCR where Val G (v) = +∞ for all v, for all vertices v of G, Val G (v) = -∞ if and only if Val G (v) < 0,
where G is the mean-payoff game V, E, ω, MP .

2. Conversely, given a mean-payoff game G = V, E, ω, MP , we can build, in polynomial time, an MCR game G such that for all vertices v of G:

Val G (v) < 0 if and only if Val G (v) = -∞.
Proof To prove the first item, consider an MCR game G = V, E, ω, T -MCR such that Val G (v) = +∞ for all v ∈ V , and G = V, E, ω, MP the same weighted graph equipped with a mean-payoff objective. If Val G (v) < 0, we know that there is a profile of optimal memoryless strategies (σ Max , σ Min ) such that the outcome starting in v and following this profile necessarily starts with a finite prefix and then loops in a cycle with a total weight less than 0. For every M > 0, we construct a strategy σ M Min that ensures in G a cost less than or equal to -M : this will prove that Val G (v) = -∞. Since we have assumed that Val G (v) = +∞ for all v, we know that Min has a strategy to reach the target from all v (for instance, take the attractor strategy described above), by a path of length at most |V |. Thus, there exists a bound w and a strategy allowing Min to reach the target from every vertex of G with a cost at most w. The strategy σ M Min of Min is then to follow σ Min until the accumulated cost is less than -M -w, at which point it follows his strategy to reach the target. Clearly, for all M , σ M Min guarantees that Min reaches the target with a cost at most -M .

Reciprocally

, if Val G (v) = -∞, consider M = |V |W and a strategy σ M Min of Min ensuring a cost less than -M , i.e. such that Val G (v, σ M Min ) < -M .
Consider the finitely-branching tree built from G by unfolding the game from vertex v and resolving the choices of Min with strategy σ M Min . Each branch of this tree corresponds to a possible strategy of Max. Since this strategy generates a finite cost, we are certain that every such branch leads to a vertex of T . If we trim the tree at those vertices, we finally obtain a finite tree. Now, for a contradiction, consider an optimal memoryless strategy σ Max of Max securing a non-negative mean-payoff, that is,

Val G (v, σ Max ) 0.
Consider the branch of the previous tree where Max follows strategy σ Max . Since this finite branch has cost less than -M = -|V |W < 0 (W is positive, otherwise the mean-payoff value would be 0), we know for sure that there are two occurrences of the same vertex v with an in-between weight less than 0: otherwise, by removing all non-negative cycles, we obtain a play without repetition of vertices, henceforth of length bounded by |V |, and therefore of cost at least -M . Suppose that v ∈ V Max . Then, Min has a strategy σ Min to ensure a negative mean-payoff Val G (v, σ Min ) < 0: indeed, he simply modifies5 his strategy so that he always stays in the negative cycle starting in v (he can do that since σ Max plays a memoryless strategy, so that he can not change his decisions in the cycle), ensuring that, against the optimal strategy σ Max of Max, he gets a mean-payoff being the cost of the cycle. This is a contradiction since Max is supposed to have a strategy ensuring a non-negative mean-payoff from v. Hence, v ∈ V Min . But the same contradiction appears in that case since Min can force that it always stays in the negative cycle by modifying his strategy. Finally, we have proved that Max can not have a memoryless strategy securing a non-negative mean-payoff from v. By memoryless determinacy of the mean-payoff games, this ensures that Min has a memoryless strategy securing a negative mean-payoff from v.

Hence, we have shown that Val G (v) = -∞ if and only if Val G (v) < 0, which concludes the first claim of Proposition 4.

To prove the second item, we reduce mean-payoff games to MCR games as follows. Let G = V, E, ω, MP be a mean-payoff game. Without loss of generality, we may suppose that the graph of the game is bipartite, in the sense that

E ⊆ V Max × V Min ∪ V Min × V Max . 6
The problem we are interested in is to decide whether Val G (v) < 0 for a given vertex v. We now construct an MCR game G = V , E , ω , T -MCR from G. The only difference is the presence of a fresh target vertex t on top of vertices of

V : V = V {t} with T = {t}. Edges of G are given by E = E ∪ {(v, t) | v ∈ V Min } ∪ {(t, t)}. Weights of edges are given by: ω (v, v ) = ω(v, v ) if (v, v ) ∈ E, and ω (v, t) = ω (t, t) = 0. We show that Val G (v) < 0 if and only if Val G (v) = -∞.
Algorithm 1: Value iteration for MCR games. Gray lines correspond to the computation of optimal strategy for both players (see Section 3.4)

Input: MCR game V, E, ω, MCR , W greatest weight in absolute value 1 X(t) := 0 2 foreach v ∈ V \ {t} do X(v) := +∞ 3 repeat 4 Xpre := X 5 foreach v ∈ V Max \ {t} do 6 X(v) := max v ∈E(v) ω(v, v ) + Xpre(v ) 7 σ Max (v) := argmax v ∈E(v) ω(v, v ) + Xpre(v ) 8 foreach v ∈ V Min \ {t} do 9 X(v) := min v ∈E(v) ω(v, v ) + Xpre(v ) 10 if X(v) = Xpre(v) then 11 σ Min (v) := argmin v ∈E(v) ω(v, v ) + Xpre(v ) 12 if Xpre(v) = +∞ then σ † Min (v) = σ Min (v) 13 foreach v ∈ V \ {t} do 14 if X(v) < -(|V | -1)W then X(v) := -∞ 15 until X = Xpre 16 return X
In G , all values are different from +∞, since Min plays at least every two steps, and has the capability to go to the target vertex with weight 0. Hence, letting G = V , E , ω , MP the mean-payoff game on the weighted graph of G , by the previous direction, we have that for every vertex

v ∈ V , Val G (v) = -∞ if and only if Val G (v) < 0.
To conclude, we prove that for all vertices

v ∈ V , Val G (v) < 0 if and only if Val G (v) < 0. If Val G (v) < 0, by mapping the memoryless optimal strategies of G into G , we directly obtain that Val G (v) Val G (v) < 0,
since Max has no possibility to go by himself to the target. Reciprocally, if Val G (v) < 0, we can project a profile of memoryless optimal strategies over vertices of G, since the target can not be visited in this case (otherwise the optimal play would have mean-payoff 0): the play obtained from v in G is then the projection of the play obtained from v in G , with the same cost. Hence,

Val G (v) Val G (v) < 0.

Computing all values

Now that we have discussed the case of vertices with value in {-∞, +∞}, let us present our core contribution on MCR games, which is a pseudo-polynomial time, value iteration algorithm to compute the values of those games. Note that this algorithm is correct even when some vertices have value in {-∞, +∞}, as we will argue later.

In all that follows, we assume that there is exactly one target vertex denoted by t, and the only outgoing edge from t is a self loop with weight 0: this is reflected by denoting MCR the payoff mapping {t}-MCR. This is without loss of generality since everything that happens after the first occurrence of a target vertex in a play does not matter for the payoff.

Our value iteration algorithm for MCR games is given in Algorithm 1. As it can be seen, this algorithm consists in computing a sequence of vectors X. Initially (line 2), X(v) = +∞ for all vertices but the target t where X(t) = 0. Then, a new value of X is obtained by optimising locally the value of each node, and changing to -∞ the value X(v) of all vertices v such that the computed value X(v) has gone below a given threshold -(|V | -1)W (line 14). The following proposition states the correctness of Algorithm 1.

Proposition 5 If an MCR game G = V, E, ω, MCR is given as input (possibly with values +∞ or -∞), Algorithm 1 outputs Val G , after at most (2|V | -1)W |V | + 2|V | iterations.
To establish this proposition, we consider the sequence of values (x i ) i 0 that vector X takes along the execution of the algorithm. More formally, we can define this sequence thanks to the operator F, which denotes the function

Z V ∞ → Z V ∞ mapping every vector x ∈ Z V ∞ to F(x)
defined, for all vertices v, by:

F(x)(v) =          0 if v = t max v ∈E(v) ω(v, v ) + x(v ) if v ∈ V Max \ {t} min v ∈E(v) ω(v, v ) + x(v ) if v ∈ V Min \ {t} .
Then, for all vertices v we let x 0 (t) = 0, and x 0 (v) = +∞ for all v = t. Moreover, for all i 1, we let

x i = F(x i-1 ).
The intuition behind this sequence is that x i is the value of the game if we impose that Min must reach the target within i steps (and get a payoff of +∞ if he fails to do so). Notice that operator F is monotonic (i.e. F(x) F(y) for all x y), and that x 1 = F(x 0 ) x 0 , so that we know that the sequence (x i ) i 0 is non-increasing:

∀i 0 x i+1 x i .
(1)

In order to formalise the intuition that x i is the value of the game if we impose that Min must reach the target within i steps, we define, for a play

π = v 0 v 1 • • • v i • • • : MCR i (π) = MCR(π) if v k = t for some k i +∞ otherwise .
We further let Observe first that for all v ∈ V , for all i 0, and for all strategies σ Max and σ Min :

MCR i (Play(v, σ Max , σ Min )) MCR(Play(v, σ Max , σ Min )) .
Indeed, if the target vertex t is reached within i steps, then payoffs are equal. Otherwise, MCR i (Play(v, σ Min , σ Max )) = +∞. Thus, for all i 1 and v ∈ V :

Val i (v) Val(v) = Val(v)
which can be rewritten as

Val i Val = Val .
Let us now consider the sequence (Val i ) i 0 . We first give an alternative definition of this sequence permitting to show its convergence.

Lemma 6 For all i 1, for all v ∈ V :

Val i (v) =          0 if v = t max v ∈E(v) ω v, v + Val i-1 v if v ∈ V Max \ {t} min v ∈E(v) ω v, v + Val i-1 v if v ∈ V Min \ {t} .
Proof The lemma can be established by showing that Val i (v) is the value in a game played on a finite tree of depth i (i.e. by applying a backward induction). We adopt the following notation for labeled unordered trees. A leaf is denoted by (v), where v ∈ V is the label of the leaf. A tree with root labeled by v and subtrees A 1 , . . . , An is denoted by (v, {A 1 , . . . , An}). Then, for each v ∈ V and i 0, we define A i (v) as follows:

A 0 (v) = (v) for all i 1 : A i (v) = (v, {A i-1 (v ) | (v, v ) ∈ E}) .
Now, let us further label those trees by a value in Z∪{+∞} thanks to the function λ (thereby formalising the backward induction). For all trees of the form A 0 (v) = (v), we let:

λ(A 0 (v)) = 0 if v = t +∞ if v = t .

For all trees of the form

A i (v) = (v, {A i-1 (v 1 ), . . . , A i-1 (vm)}) (for some i
1), we let:

λ A i (v) =          0 if v = t max 1 j m ω(v, v j ) + λ(A i-1 (v j )) if v ∈ V Max \ {t} min 1 j m ω(v, v j ) + λ(A i-1 (v j )) if v ∈ V Min \ {t} .
(2)

Clearly, for all v ∈ V , for all i 0, the branches of A i (v) correspond to all the possible finite plays Play(v, σ Max , σ Min )[i], i.e. there is a branch for each possible strategy profile (σ Max , σ Min ). Thus, λ(A i (v)) = Val i (v) for all i 0, which permits us to conclude from (2).

We have just shown that for all i 1, Val i = F(Val i-1 ), and since

x 0 = Val 0 ,
we obtain (as expected)

x i = Val i for all i 0.
The main question is now to characterise the limit of the sequence (x i ) i 0 , and more precisely, to prove that it is the value Val of the game. Indeed, at this point, it would not be too difficult to show that Val is a fixed point of operator F, but it would be more difficult to show that it is the greatest fixed point of F, that is indeed the limit of sequence (x i ) i 0 (by Kleene's theorem, applicable since F is Scott-continuous). Instead, we study refined properties of the sequence (Val i ) i 0 , namely its stationarity and the speed of its convergence, and deduce that Val is the greatest fixed point as a corollary (see Corollary 11).

We start by characterising how where k is the step at which v has been added to the attractor, and each value a i is finite and bounded:

Lemma 7 Let v ∈ V be a vertex and let 0 k |V | be such that v ∈ Attr k ({t}) \ Attr k-1 ({t}) (assuming Attr -1 ({t}) = ∅). Then, for all 0 j |V |: (i) j < k implies Val j (v) = +∞ and (ii) j k implies Val j (v) jW .
Proof We prove the property for all vertices v, by induction on j.

Base case: j = 0. We consider two cases. Either v = t. In this case, k = 0, and we must show that Inductive case: j = 1. Let us assume that the lemma holds for all v, for all values of j up to -1, and let us show that it holds for all v, and for j = . Let us fix a vertex v, and its associated index k such that v ∈ Attr k ({t}) \ Attr k-1 ({t}). We consider two cases.

1. First, assume k > . In this case, we must show that Val (v) = +∞. We consider again two cases: (a) If v ∈ V Min , then none of its successors belong to Attr -1 ({t}), otherwise, v would be in Attr ({t}), by definition of the attractor, and we would have k . Hence, by induction hypothesis, Val -1 (v ) = +∞ for all v such that (v, v ) ∈ E. Thus:

Val (v) = min (v,v )∈E ω(v, v ) + Val -1 (v ) (Lemma 6) = +∞ . (b) If v ∈ V Max
, then at least one successor of v does not belong to Attr -1 ({t}), otherwise, v would be in Attr ({t}), by definition of the attractor, and we would have k . Hence, by induction hypothesis, there exists v such that (v, v ) ∈ E and Val -1 (v ) = +∞. Thus:

Val (v) = max (v,v )∈E ω(v, v ) + Val -1 (v ) (Lemma 6) = +∞ .
2. Second, assume k . In this case, we must show that Val (v) W . As in the previous item, we consider two cases:

(a) In the case where v ∈ V Min , we let v be a vertex such that v ∈ Attr k-1 ({t}) and (v, v) ∈ E. Such a vertex exists by definition of the attractor. By induction hypothesis, Val -1 (v) W . Then:

Val (v) = min (v,v )∈E ω(v, v ) + Val -1 (v ) (Lemma 6) ω(v, v) + Val -1 (v) ((v, v) ∈ E) ω(v, v) + ( -1)W (Ind. Hyp.) W + ( -1)W = W .
(b) In the case where v ∈ V Max , we know that all successors v of v belong to

Attr k-1 ({t}) by definition of the attractor. By induction hypothesis, for all successors v of v: Val -1 (v ) W .Hence:

Val (v) = max (v,v )∈E ω(v, v ) + Val -1 (v ) (Lemma 6) max (v,v )∈E (W + ( -1)W ) (Ind. Hyp.) = W .
In particular, this allows us to conclude that, after |V | steps, all values are bounded by |V |W :

Corollary 8 For all v ∈ V , Val |V | (v) |V |W .
The next step is to show that the sequence (x i ) i 0 stabilises after a bounded number of steps, when all values are finite:

(v) = Val(v) is indeed reached.
Let us build a tree Aσ Min unfolding all possible plays from v against σ Min . Aσ Min has a root labeled by v. If a tree node is labeled by a vertex v of Min, this tree node has a unique child labeled by σ Min (v). If a tree node is labeled by a vertex v of Max, this tree node has one child per successor v of v in the graph, labeled by v . We proceed this way until we encounter a node labeled by a vertex from t in which case this node is a leaf. Aσ Min is necessarily finite. Otherwise, by König's Lemma, it has one infinite branch that never reaches t. From that infinite branch, one can extract a strategy σ Max for Max such that MCR(Play(v, σ Max , σ Min )) = +∞, hence Val(v) = +∞, which contradicts the hypothesis. Assume the tree has depth m. Then, Aσ Min is a subtree of the tree A obtained by unfolding all possible plays up to length m (as in the proof of Lemma 6). In this case, it is easy to check that the value labeling the root of Aσ Min after applying backward induction is larger than or equal to the value labeling the root of A after applying backward induction. The latter is Val(v) while the former is Val m (v), by Lemma 6, so that

Val(v) Val m (v).
Since the sequence is non-increasing, we finally obtain Val(v) Val (v).

As a corollary of this lemma, we obtain:

Corollary 11 In all MCR games where all values are finite, Val is the greatest fixed point of F.

We are finally able to establish the correctness of Algorithm 1.

Proof (of Proposition 5) Let us first suppose that the values of all vertices are finite. Then, x j = Val j is the value of X at the beginning of the jth step of the loop, and the condition of line 13 can never be fulfilled. Hence, by Lemma 9, after at most (2|V | -1)W |V | + |V | iterations, all values are computed correctly (by Lemma 10) in that case. Suppose now that there are vertices with value +∞. Those vertices will remain at their initial value +∞ during the whole computation, and hence do not interfere with the rest of the computation.

Finally, consider that the game contains vertices with value -∞. By the proof of Lemma 9, we know that optimal values of vertices of values different from -∞ are at least -(|V | -1)W + 1 so that, if the value of a vertex reaches an integer below -(|V | -1)W , we are sure that its value is indeed -∞, which proves correct the line 13 of the algorithm. This update may cost at most one step per vertex, which in total adds at most |V | iterations. Moreover, dropping the value to -∞ does not harm the correction for the other vertices (it may only speed up the convergence of their values). This is due to the fact that, if the Kleene sequence (F i (x 0 )) i 0 is initiated with a vector of values x 0 that is greater or equal to the optimal value vector Val, then the sequence converges at least as fast as before towards the optimal value vector.

Example 12 We close this discussion on the computation of the values by an example of execution of Algorithm 1. Consider the MCR game in Fig. 2. The successive values for vertices (v 1 , v 2 ) (value of the target v 3 is always 0) computed by the value iteration algorithm are the following: (+∞, +∞), (+∞, 0), (-1, 0), (-1, -1), (-2, -1), (-2, -2), . . . , (-W, -W + 1), (-W, -W ). This requires 2W steps to converge (hence a pseudo-polynomial time).

Computing optimal strategies for both players

As we have seen earlier, Min does not always have optimal memoryless strategies. However, we will see that one can always construct so-called negative cycle strategies (NC-strategies), which are memoryless strategies that have a meaningful structure for Min, in the sense that they allow him either: (i) to reach the target by means of a play whose value is lower that the value of the game; or (ii) to decrease arbitrarily the partial sums along the play, when it does not reach the target (in other words, the partial sums tend to -∞ as the play goes on). So, NC-strategies are, in general, not optimal, as they do not guarantee to reach the target (but in this case, they guarantee that Min will play consistently with his objective, by decreasing the value of the play prefixes).

Formally, an NC-strategy is a memoryless strategy σ Min for player Min such that, for all cycles

v 0 • • • v k-1 v k (with v k = v 0 ) conforming to σ Min (i.e. where each v i ∈ V Min satisfies σ(v i ) = v i+1 ), ω(v 0 , v 1 ) + • • • + ω(v k-1 , v k ) < 0 .
We define the fake value, fake(v, σ Min ), of an NC-strategy σ Min as the supremum of the costs of the finite plays that conform with it and start in v:

fake(v, σ Min ) = sup MCR(v 1 • • • v k ) | v 1 = v, v k = t, ∀v i ∈ V Min : σ Min (v i ) = v i+1 .
Notice that the fake value is not necessarily equal to the value of σ Min , since, in the definition of the fake value, we only consider plays that do reach the target, and ignore those that don't (in the computation of the actual value of σ Min , these plays would yield +∞). However, a strategy's fake value is always smaller than or equal to its value. We say that an NC-strategy is fake-optimal if its fake value is smaller than or equal to the optimal value of the game from all vertices. In particular, if the optimal value of a vertex v is -∞, the set

{MCR(v 1 • • • v k ) | v 1 = v, v k = t, ∀v i ∈ V Min σ Min (v i ) = v i+1
is empty for all fake-optimal strategies σ Min , hence the supremum of this set is indeed -∞.

Example 13 On the game of Fig. 2, the memoryless strategy σ Min mapping v 2 to v 1 is an NC-strategy as the only two possible cycles

v 1 v 2 v 1 and v 2 v 1 v 2 both have weight -1. The value of σ Min from v 2 is +∞ as the play v 2 v 1 v 2 v 1 v 2 • • •
agrees with it and does not reach the target, but the fake value of σ Min is -W , since the play v 2 v 1 v 3 is the finite play that agrees with σ Min with the biggest cost possible. Since we know that the actual optimal value is -W , the strategy σ Min is fake-optimal.

The following proposition reveals the interest of NC-strategies, by explaining how one can, in some cases, construct an optimal finite-memory strategy from a fake-optimal NC-strategy.

Proposition 14 If Min has a strategy σ † Min to reach a target vertex (from every possible initial vertex), and has a fake-optimal NC-strategy σ Min , then for all n ∈ Z one can construct a finite-memory strategy σ n Min such that for all vertices v, it holds that

Val(v, σ n Min ) max(n, Val(v)).
Remark 15 In particular, if the value of all vertices is finite, then one can construct an optimal finite-memory strategy. If the value of a vertex is -∞, this proposition also says that there is an infinite family a strategies that allows one to secure a value which is arbitrarily low (remember that, by definition, -∞ can not be the value that corresponds to a single strategy).

Proof First let us show that for all partial plays π = v 1 • • • v of size at least k|V |+1 (for some k) that conforms with σ Min , TP(π) W (|V | -1) -k. We establish this proof by induction on k. For the base case, we consider the case where

|V |.
Then, the play visits at most |V | -1 edges, and thus its total cost is at most W (|V | -1). Now, for the induction, we assume that k|V | + 1 for some k 1. Then, let i and j be two indices such that i < j, v i = v j and j i + |V | (those indices necessarily exist since

|V | + 1). Since σ Min is an NC-strategy, the total cost of v i • • • v j is at most -1. As π = v 1 • • • v i v j+1 • • • v is
also a play that conforms with σ Min with size greater than (k -1)|V | + 1, we have (by induction hypothesis)

TP(π ) W (|V |-1)-k +1, thus TP(π) = TP(v i • • • v j )+TP(π ) W (|V |-1)-k.
In the following, let σ † Min be a memoryless strategy ensuring to reach the target (obtained by the attractor technique for instance), and let k = max(2W (|V | -1)n, 0). The strategy σ n Min consists in playing σ Min , until switching to σ † Min when the length of the play is greater than k|V | + 1: formally

σ n Min (π) = σ Min (π) if |π| < k|V | + 1 and σ n Min (π) = σ † Min (π) otherwise.
It is clear that this strategy can be implemented by a finite deterministic Moore machine, storing the size of the current play until it is greater than k|V | + 1.

Let us now check that Val(v, σ n

Min ) max(n, Val(v)) for all vertices. Let π be a play conforming to σ n Min starting in a vertex v and reaching t. If |π| k|V | + 1 then π is a play that reaches the target conforming to σ Min and therefore

MCR(π) fake(v, σ Min )
π is a finite play reaching t

Val(v)

σ Min is fake-optimal max(n, Val(v)) .

If |π| > k|V | + 1, then let π 1 be its prefix of size k|V | + 1, and π 2 be the rest of the play (π = π 1 • π 2 ). As π 2 is a play that conforms with σ † Min , a memoryless strategy ensuring to reach the target, we know that it reaches the target in at most |V | steps. Therefore, TP(π 2 ) W (|V | -1). As π 1 is a play that conforms with σ Min of size k|V | + 1, from the reasoning above, TP(π

1 ) W (|V | -1) -k n -W (|V | -1), therefore TP(π) = TP(π 1 ) + TP(π 2 ) n max(n, Val(v)).
In practice, rather than using a Moore machine, we can simulate the strategy σ n Min (of the proof above) quite easily: one just has to handle two memoryless strategies and a counter keeping track of the length of the current play. Since σ † Min can easily be obtained by the classical attractor algorithm, we turn our attention to the construction of a fake-optimal NC-strategy σ Min . Without loss of generality, we suppose that no vertex has optimal value +∞, since for these vertices, all strategies are equivalent.

For vertices of value -∞, we can obtain σ Min as an optimal strategy for Min in the mean-payoff game of the first item in Proposition 4. Since the mean-payoff value is negative, this strategy guarantees that it does not reach target, thus generating a fake value -∞, equal to the optimal value of the vertex. Moreover, since it is a memoryless strategy, we know that, as soon as Max plays a memoryless strategy that necessarily reaches a cycle, this cycle must have a negative weight (at most the optimal value of the initial vertex) : this strategy is thus a fake-optimal NC-strategy.

From now on, we thus concentrate our study on the vertices of finite value, thus considering that no vertices have value +∞ or -∞ in the MCR game. Let X i denote the value of variable X after i iterations of the loop of Algorithm 1, and let X 0 (v) = +∞ for all v ∈ V . We have seen that the sequence X 0 X 1 X 2 • • • is stationary at some point, equal to Val. Let us now define σ Min (v) for all vertices v ∈ V Min \ {t}. We let iv > 0 be the smallest index such that X iv (v) = Val(v). Fix a vertex v such that X iv (v) = ω(v, v ) + X iv-1 (v ) (such a v exists by definition) and define σ Min (v) = v . Notice that it is exactly what is achieved in line 11 of Algorithm 1. Note also that strategy σ † Min is correctly computed in line 12 of Algorithm 1.

Let us prove that this construction indeed yields a fake-optimal NC strategy σ Min . We first prove the following lemma, that states that the vertex σ Min (v) has already reached its final value at step iv -1 of the algorithm, for all vertices v.

Lemma 16 For all vertices

v ∈ V Min \ {t}, X iv-1 (σ Min (v)) = Val(σ Min (v)).
Proof Let v = σ Min (v). Since (X i (v )) i 0 is non-increasing and converges towards the value of v , we know that X iv-1 (v ) Val(v ). By contradiction assume that X iv-1 (v ) > Val(v ). Note that there exists j > iv such that X j-1 (v ) = Val(v ). Therefore:

Val(v) X j (v) (since (X k (v)) k∈N is non-increasing) ω(v, v ) + X j-1 (v ) (by definition of X j ) = ω(v, v ) + Val(v ) (by choice of j) < ω(v, v ) + X iv-1 (v ) (by the contradiction hypothesis) = X iv (v) = Val(v) (by definition of X iv )
which raises a contradiction.

We can now prove that our definition of σ Min has the announced properties:

Proposition 17 σ Min is an NC-strategy, and fake(v, σ Min ) Val(v) for all vertices v.

Proof Equivalently, we want to prove that for all vertices v, and for all plays

π = v 1 v 2 • • • starting in v and conforming to σ Min ,
(1) if there exists i < j such that

v i = v j , then TP(v i • • • v j ) < 0, (2) if π reaches t then MCR(π) Val(v).
For (1), consider a cycle

v i • • • v j with v j = v i .
Notice that at least one vertex of this cycle belongs to Min, since, otherwise, Max would have a strategy to obtain a value +∞ for vertex v i , which contradicts the hypothesis that every vertex has value different from +∞. Hence, for the sake of the explanation, we suppose that v i ∈ V Min , and that the index iv i where vertex v i stabilises in the sequence (X k (v i )) k 0 is maximal among all possible vertices of {v i , . . . , v j } ∩ V Min . The following extends easily to the general case.

We prove by induction over i < j that

X iv i (v i ) TP(v i • • • v ) + X iv i -1 (v ) . (3)
The base case = i + 1 comes from the fact that, since v i ∈ V Min , we have

σ Min (v i ) = v i+1 . Therefore, X iv i (v i ) = ω(v i , v i+1 )+X iv i -1 (v i+1
), and by definition

TP(v i v i+1 ) = ω(v i , v i+1 ).
For the inductive case, let us consider i < < j such that (3) holds and let us prove it for + 1. If v ∈ V Max , by definition of X iv i , we have

X iv i (v ) = max (v ,v )∈E ω(v , v ) + X iv i -1 (v ) ω(v , v +1 ) + X iv i -1 (v +1 ) .
If v ∈ V Min , by maximality of iv i , we have

X iv i (v ) = X iv (v ) = ω(v , v +1 ) + X iv -1 (v +1 ) ω(v , v +1 ) + X iv i -1 (v +1 )
using that the sequence X 0 , X 1 , X 2 , . . . is non-increasing. In all cases, we have

X iv i (v ) ω(v , v +1 ) + X iv i -1 (v +1 ) .
Using again that X 0 , X 1 , X 2 , . . . is non-increasing, we obtain

X iv i -1 (v ) X iv i (v ) ω(v , v +1 ) + X iv i -1 (v +1 ) .
Injecting this into the induction hypothesis, we have

X iv i (v i ) TP(v i • • • v ) + ω(v , v +1 ) + X iv i -1 (v +1 ) = TP(v i • • • v +1 ) + X iv i -1 (v +1 )
which concludes the proof by induction.

In particular, for = j, as v i = v j we obtain that

X iv i (v i ) X iv i -1 (v i ) + TP(v i • • • v j ) .
and as, by definition of iv i , we have

X iv i (v i ) < X iv i -1 (v i ), we necessarily have TP(v i • • • v j ) < 0.
We now prove (2). We decompose

π as π = v 1 • • • v k t ω with for all i, v i = t. We prove by decreasing induction on i that MCR(v i • • • v k t ω ) Val(v i ). If i = k + 1, MCR(t ω ) = 0 = Val(t). If i k, by induction we have MCR(v i+1 • • • v k t ω ) Val(v i+1 ). Thus MCR(v i • • • v k t ω ) ω(v i , v i+1 ) + Val(v i+1 ). If v i ∈ V Min , then v i+1 = σ Min (v i )
, and by Lemma 16,

Val(v i+1 ) = X iv i -1 (v i+1 ) = X iv i (v i ) -ω(v i , v i+1 ) by definition of σ Min . Since X iv i (v i ) = Val(v i ), this can be rewritten as Val(v i ) = ω(v i , v i+1 ) + Val(v i+1 ) MCR(v i • • • v k t ω ), which proves the inequality for i. If v i ∈ V Max , then MCR(v i • • • v k t ω ) ω(v i , v i+1 ) + Val(v i+1 ) max (vi,v )∈E ω(v i , v ) + Val(v ) = Val(v i )
the last equality coming from Corollary 11.

As a corollary, we obtain the existence of finite memory strategies (obtained from σ Min and σ † Min as described above) when all values are finite:

Corollary 18 When the values of all vertices of an MCR game are finite, one can construct an optimal finite-memory strategy for player Min.

Strategies of Max

Let us now show that Max always has a memoryless optimal strategy. This asymmetry stems directly from the asymmetric definition of the gamewhile Min has the double objective of reaching t and minimising its cost, Max aims at avoiding t, and if not possible, maximising the cost.

Proposition 19 In all MCR games, Max has a memoryless optimal strategy.

Proof For vertices with value +∞, we already know a memoryless optimal strategy for Max, namely every strategy that remains outside the attractor of the target vertices. For vertices with value -∞, all strategies are equally bad for Max.

We now explain how to define a memoryless optimal strategy σ Max for Max in case of a graph containing only finite values. For every finite play π ending in a vertex v ∈ V Max of Max, we let

σ Max (π) = argmax v ∈E(v) ω(v, v ) + Val(v ) .
This is clearly a memoryless strategy. Let us prove that it is optimal for Max, that is, for every vertex v ∈ V , and every strategy σ Min of Min MCR(Play(v, σ Max , σ Min )) Val(v) .

In case Play(v, σ Max , σ Min ) does not reach the target set of vertices, the inequality holds trivially. Otherwise, we let

Play(v, σ Max , σ Min ) = v 0 v 1 • • • v • • • with the least position such that v = t. If = 0, i.e. v = v 0 = t, we have MCR(Play(v, σ Max , σ Min )) = 0 = Val(v) .
Otherwise, let us prove by induction on 0 i that

MCR(v -i • • • v ) Val(v -i ) .
This will permit to conclude since

MCR(Play(v, σ Max , σ Min )) = MCR(v 0 v 1 • • • v ) Val(v 0 ) = Val(v) .
The base case i = 0 corresponds to the previous case where the starting vertex is t. Supposing that the property holds for index i, let us prove it for i + 1. We have

MCR(v -i-1 • • • v ) = ω(v -i-1 , v -i ) + MCR(v -i • • • v ) .
By induction hypothesis, we have

MCR(v -i-1 • • • v ) ω(v -i-1 , v -i ) + Val(v -i ) . (4)
We now consider two cases:

-If v -i-1 ∈ V Max \ {t}, then v -i = σ Max (v 0 v 1 • • • v -i-1
), so that by definition of σ Max :

ω(v -i-1 , v -i ) + Val(v -i ) = max v ∈V |(v -i-1 ,v )∈E ω(v -i-1 , v ) + Val(v ) .
Using Corollary 11 and (4), we obtain

MCR(v -i-1 • • • v ) Val(v -i-1 ) . -If v -i-1 ∈ V Min \ {t}, then ω(v -i-1 , v -i ) + Val(v -i ) min v ∈V |(v -i-1 ,v )∈E ω(v -i-1 , v ) + Val(v ) .
Once again using Corollary 11 and (4), we obtain

MCR(v -i-1 • • • v ) Val(v -i-1 ) .
This concludes the proof.

v 1 v 2 t 0 0 0 0 v 1 v 2 v 3 v 4 t -1 -1 0 0 -1 0 Fig. 3 Importance of the if condition of Algorithm 1
Notice that strategy σ Max can be computed directly, along the execution of the value iteration algorithm. This corresponds to line 7 of Algorithm 1.

Notice further that the presence of the if condition in line 11, and the absence of a similar condition at line 7, are crucial. Indeed, removing the if from line 11 would amount to computing σ Min from the vector of values obtained at the end of the value iteration, when the vector X has stabilised. Let us show that, in this case, the algorithm might fail to compute a fake-optimal NC-strategy, by considering the MCR game in the left part of Fig. 3. Clearly, the values of both v 1 and v 2 are 0. However, if we extract σ Min from Xpre at that point of the execution of the algorithm (i.e. we let σ Min (v) = argmin v ∈E(v) (ω(v, v ) + Xpre(v ))), then we could end up with σ Min (v 1 ) = v 2 and σ Min (v 2 ) = v 1 . In this case, σ Min is no longer an NC-strategy because the cycle v 1 v 2 v 1 does not have negative weight. Similarly, let us consider the MCR game in the right part of Fig. 3 to explain why line 7 is not under the range of an if (X(v) = Xpre(v)) condition. After two iterations, X reaches the optimal values (-1, 0, -1, 0) but a Max strategy σ Max such that σ Max (v 1 ) = v 3 can still be chosen since Xpre(v 3 ) = 0 at that point. However, on the next iteration, X(v 3 ) = Xpre(v 3 ) = -1 (indeed, X has now stabilised on all nodes), and it is crucial that σ Max (v 1 ) = v 2 gets computed, otherwise the strategy would not be optimal for Max.

An efficient algorithm to solve total-payoff games

We now turn our attention back to total-payoff games (without reachability objective), and discuss our main contribution. Building on the results of the previous section, we introduce the first (as far as we know) pseudo-polynomial time algorithm for solving those games in the presence of arbitrary weights, thanks to a reduction from total-payoff games to MCR games. The MCR game produced by the reduction has size pseudo-polynomial in the size of the original total-payoff game. Then, we show how to compute the values of the total-payoff game without building the entire MCR game, and explain how to deduce memoryless optimal strategies from the computation of our algorithm.

Reduction to MCR games

We provide a transformation from a total-payoff game G = V, E, ω, TP to an MCR game G K (where K is a parameter in N) such that the values of G can be extracted from the values in G K (as formalised below). Intuitively, G K simulates the game where players play in G; Min may propose to stop playing and reach a 4 MCR game G 3 associated with the total-payoff game of Fig. 2 fresh vertex t acting as the target; Max can then accept, in which case we reach the target, or refuse at most K times, in which case the game continues. Structurally, G K consists of a sequence of copies of G along with some new states that we now describe formally. We let t be a fresh vertex, and, for all n 1, we define the MCR game G n = V n , E n , ω n , {t}-MCR where V n Max (respectively, V n Min ) consists of n copies (v, j), with 1 j n, of each vertex v ∈ V Max (respectively, v ∈ V Min ) and some exterior vertices (ex, v, j) for all v ∈ V and 1 j n (respectively, interior vertices (in, v, j) for all v ∈ V and 1 j n). Moreover, V n Max contains the fresh target vertex t. Edges are given by

v1, 3 in, v1, 3 v2, 3 in, v2, 3 v3, 3 in, v3, 3 -1 -W ex, v1, 3 ex, v2, 3 ex, v3, 3 v1, 2 in, v1, 2 v2, 2 in, v2, 2 v3, 2 in, v3, 2 -1 -W ex, v1, 2 ex, v2, 2 ex, v3, 2 v1, 1 in, v1, 1 v2, 1 in, v2, 1 v3, 1 in, v3, 1 -1 -W ex, v1, 1 ex, v2, 1 ex, v3, 1 t Fig.
E n = {(t, t)} (v, j), (in, v , j) | (v, v ) ∈ E, 1 j n (in, v, j), (v, j) | v ∈ V, 1 j n (ex, v, j), t | v ∈ V, 1 j n (in, v, j), (ex, v, j) | v ∈ V, 1 j n (ex, v, j), (v, j -1) | v ∈ V, 1 < j n .
All edge weights are zero, except edges (v, j), (in, v , j) that have weight ω(v, v ).

Example 20 For example, considering the weighted graph of Fig. 2, the corresponding reachability total-payoff game G 3 is depicted in Fig. 4 (where weights 0 have been removed).

The next proposition formalises the relationship between the two games, and is proved in the rest of this subsection.

Proposition 21 Let K = |V |(2(|V | -1)W + 1). For all v ∈ V and k K, -Val G (v) = +∞ if and only if Val G (v) = Val G k ((v, k)); -Val G (v) = +∞ if and only if Val G k ((v, k)) (|V | -1)W + 1.
The bound K will be found by using the fact (informally described in the previous section) that if not infinite, the value of a min-cost reachability game belongs in [-

(|V | -1) × W + 1, |V | × W ],
and that after enough visits of the same vertex, an adequate loop ensures that G k verifies the above properties.

To prove Proposition 21, we must relate paths in games G and G n : with each finite path in G n , we associate a finite path in G, obtained by looking at the sequence of vertices of V appearing inside the vertices of the finite play. Formally, the projection of a finite path π is the sequence proj(π) of vertices of G inductively defined by proj(ε) = ε and for all finite path π, v ∈ V and 1 j n:

proj((in, v, j)π) = proj(π) , proj((ex, v, j)tπ) = v , proj((ex, v, j)) = ε , proj((ex, v, j + 1)(v, j)π) = proj((v, j)π) = v proj(π) .
In particular, notice that in the case of a play with prefix (ex, v, j)t, the rest of the play is entirely composed of target vertices t, since t is a sink state. For instance, the projection of the finite play

(v 1 , 3)(in, v 2 , 3)(ex, v 2 , 3)(v 2 , 2)(in, v 3 , 2)(v 3 , 2)(in, v 3 , 2)(ex, v 3 , 2)t of the game G 3 of Fig. 4 is given by v 1 v 2 v 3 v 3 .
The following lemma relates plays of G n with their projection in G, comparing their total-payoff.

Lemma 22 The projection mapping satisfies the following properties.

1. If π is a finite play in G n then proj(π) is a finite play in G. 2. If π is a play in G n that does not reach the target, then proj(π) is a play in G.

3. For all finite play π, TP(π) = TP(proj(π)).

Proof The proof of 2 is a direct consequence of 1. With each vertex w ∈ V n \ {t}, we naturally associate a vertex f (w) as follows:

f (v, j) = f (in, v, j) = f (ex, v, j) = v .
Then notice that if (w, w ) ∈ E n with w, w = t, then either f (w) = f (w ) or (f (w), f (w )) ∈ E. We now prove 1 and 3 inductively on the size of the finite play

π = w 1 • • • w k of G n ,
along with the fact that 4. if proj(π) = ∅ and w 1 = t then the first vertex of proj(π) is f (w 1 ).

If k = 0, then π = proj(π) = ε are finite plays with the same total-payoff. If k = 1, either proj(π) = ε or π = (v, j) and proj(π) = v: in both cases, the properties hold trivially. Otherwise, k 2 and we distinguish several possible prefixes:

-If π = (in, v, j)π , then proj(π) = proj(π ). Hence, 1 holds by induction hypothesis. If proj(π) is non-empty, so is proj(π ). Moreover, the first vertex of π is either (v, j) or (ex, v, j), so that we have 4 by induction hypothesis. Finally, the previous remark shows that the first edge of π has necessarily weight 0, so that, TP(π) = TP(π ), and 3 also holds by induction hypothesis.

-If π = (v, j)π , then proj(π) = v proj(π ) so that 4 holds directly. Moreover, π is a non-empty finite play so that π = (in, v , j)π with (v, v ) ∈ E, and proj(π ) = proj(π ). By induction, proj(π ) is a finite play in G, and it starts with v (by 4). Since (v, v ) ∈ E, this shows that proj(π) is a finite play. Moreover,

TP(π) = ω n ((v, j), (in, v , j)) + TP(π ) = ω(v, v ) + TP(π ). By induction hypothesis, we have TP(π ) = MCR(proj(π )). Moreover, MCR(proj(π)) = ω(v, v ) + MCR(proj(π )) which concludes the proof of 3. -If π = (ex, v, j)(v, j -1)π then proj(π) = v proj(π ) = proj((v, j -1)π ): this
allows us to conclude directly by using the previous case.

-Otherwise, π = (ex, v, j)tπ , and then proj(π) = v is a finite play with totalpayoff 0, like π, and 4 holds trivially.

The next lemma states that when playing memoryless strategies, one can bound the total-payoff of all finite plays. Proof We prove the part for Min, the other case is similar. The proof proceeds by induction on the size of a partial play

π = v 1 • • • v k with v 1 = v. If k |V | then TP(π) = k-1 i=1 ω(v i , v i+1 ) (k -1)W (|V |-1)W . If k |V |+1 then there exists i < j such that v i = v j . Assume by contradiction that TP(v i • • • v j ) > 0. Then the play π = v 1 • • • v i • • • v j (v i+1 • • • v j ) ω conforms to σ Min and TP(π ) = +∞ which contradicts Val(v, σ Min ) = +∞. Therefore TP(v i • • • v j ) 0. We have TP(π) = TP(v 1 • • • v i ) + TP(v i • • • v j ) + TP(v j+1 • • • v k ), and since v i = v j , v 1 • • • v i v j+1 • • • v k
is a finite play starting from v that conforms to σ Min , and by induction hypothesis

TP(v 1 • • • v i v j+1 • • • v k ) (|V | -1)W . Then TP(π) = TP(v 1 • • • v i v j+1 • • • v k ) + TP(v i • • • v j ) TP(v 1 • • • v i v j+1 • • • v k ) (|V | -1)W .
This permits to bound the finite values Val(v) of vertices v of the game:

Corollary 24 For all v ∈ V , Val(v) ∈ -(|V | -1)W, (|V | -1)W {-∞, +∞}.
Proof From the result of [START_REF] Gimbert | When can you play positionally?[END_REF], we know that total-payoff games are memorylessly determined, i.e. there exists two memoryless strategies σ Max , σ Min such that for all v, We now compare values in both games. A first lemma shows, in particular, that

Val(v) = Val(v, σ Max ) = Val(v, σ Min ). Assume that Val(v) / ∈ {-∞, +∞}. Then since Val(v, σ Min ) = Val(v) = -∞, Lemma
Val G n (v, n) Val G (v), in case Val G (v) = +∞. Lemma 25 For all m ∈ Z, v ∈ V , and n 1, if Val G (v) m then Val G n (v, n) m.
Proof By hypothesis and using the memoryless determinacy of total-payoff games [START_REF] Gimbert | When can you play positionally?[END_REF], there exists a memoryless strategy

σ Min for Min in G such that Val G (v, σ Min ) m. Let σ m
Min be the strategy in G n defined, for all finite play π, vertex v and 1 j n, by

σ m Min (π(v , j)) = (in, σ Min (proj(π)v ), j) , σ m Min (π(in, v , j)) = (v , j) if TP(π(in, v , j)) m + 1 , (ex, v , j) if TP(π(in, v , j)) m .

Intuitively σ m

Min simulates σ Min , and asks to leave the copy when the current totalpayoff is less than or equal to m. Notice that, by construction of σ m Min , proj(π) conforms to σ Min , if π conforms to σ m Min .

As a first step, if a play π starting in (v, n) and conforming to σ m Min encounters the target then its value is at most m. Indeed, it is of the form π = π (in, v , j)(ex, v , j)t ω , and since it conforms to σ m Min we have

MCR(π) = TP(π (in, v , j)(ex, v , j)t) = TP(π (in, v , j)) m.
Then, assume, by contradiction, that there exists a play π starting in (v, n) and conforming to σ m Min , that does not encounter the target. Then, this means that Min does not ask n +1 times the ability to exit in π (since on the (n+1)th time that we jump in an exterior vertex, Max is forced to go to the target). In particular, there exists 0 j n such that π is of the form

π (v 1 , j)(in, v 2 , j)(v 2 , j)(in, v 3 , j) • • • (v k , j) (in, v k , j) • • • . Since for all i, σ m Min (π (v 1 , j)(in, v 2 , j) • • • (in, v i , j)) = (v i , j), we have that TP(π (v 1 , j)(in, v 2 , j) • • • (in, v i , j)) m + 1.
Therefore, since every prefix of proj(π) is the projection of a prefix of π, Lemma 22 shows that TP(proj(π)) m + 1 > m, which raises a contradiction since proj(π) conforms to σ Min and Val(v, σ Min ) m. Hence every play that conforms to σ m Min encounters the target, and, hence, has value at most m. This implies that Val G n (v, n) m.

We now turn to the other comparison between Val G n (v, n) and Val G (v). Since Val G (v) can be infinite in case the target is not reachable, we have to be more careful. In particular, we show that

Val G n (v, n) min Val G (v), (|V | -1)W + 1 holds for large values of n. In the following, we let K = |V |(2(|V | -1)W + 1). Lemma 26 For all m (|V | -1)W + 1, k K, and vertex v, if Val G (v) m then Val G k (v, k) m.
Proof By hypothesis and using the memoryless determinacy proved by [START_REF] Gimbert | When can you play positionally?[END_REF], there exists a memoryless strategy

σ Max for Max in G such that Val G (v, σ Max ) m. Let σ m
Max be the strategy in G K defined, for all finite play π, vertex v and 1 j n, by:

σ m Max (π(v, j)) = (in, σ Max (proj(π)v), j) , σ m Max (π(ex, v, j)) = (v, j -1) if TP(π) m -1 and j > 1 , t otherwise .

Intuitively σ m

Max simulates σ Max , and accepts to go to the target when the current total-payoff is greater than or equal to m.

By construction of σ m Max , if π conforms to σ m Max , then proj(π) conforms to σ Max . From the structure of the weighted graph, we know that for every play π of G k , there exists 1

j k such that π is of the form π k (ex, v k , k)π k-1 (ex, v k-1 , k - 1) • • • π j (ex, v j , j
)π verifying that: there are no occurrences of exterior vertices in π k , . . . , π j , π ; for all j, all vertices in π belong to the -th copy of G; either π = t ω or all vertices of π belong to the (j + 1)th copy of G (in which case, j < k).

We now show that, in G k , MCR(π) m for all play π starting in (v, k) and conforming to σ m Max . There are three cases to consider. 1. If π does not reach the target, then

MCR(π) = +∞ m. 2. If π = π k (ex, v k , k) • • • π j (ex, v j , j)t ω and j > 1 then, σ m Max (π k (ex, v 0 , k) • • • π j (ex, v j , j)) = t .
Thus, using Lemma 22,

MCR(π) = TP(π k (ex, v k , k) • • • π j (ex, v j , j)t) = TP(proj(π k (ex, v k , k) • • • π j (ex, v j , j)t)) Val G (v, σ Max ) m . 3. If π = π k (ex, v k , k) • • • π 1 (ex, v 1 , 1)t ω , assume by contradiction that TP(π k (ex, v k , k) • • • π 1 ) m -1 .
Otherwise, we directly obtain MCR(π) m. Let v be a vertex that occurs at least

N = K/|V | = 2(|V | -1)W + 1 times in the sequence v 1 , . . . , v k : such a vertex exists, since otherwise K k (N -1)|V | which contradicts the fact that (N -1)|V | < K. Let j 1 > • • • > j N be a sequence of indices such that v ji = v for all i. We give a new decomposition of π: π = π 1 (ex, v j1 , j 1 ) • • • π N (ex, v j N , j N )π N +1 .
Since π conforms to σ m Max and according to the assumption, we have that for all i,

TP(π 1 (ex, v j1 , j 1 ) • • • π i ) m -1 .
We consider two cases. (a) If there exists

π i such that TP(π i ) 0 then, let proj(π i ) = u 1 • • • u with u 1 = u = v , Since π i conforms to σ m Max , proj(π i ) conforms to σ Max . There- fore the play π = proj(π 1 (ex, v j1 , j 1 ) • • • π i (ex, v ji , j i ))(u 1 • • • u -1 ) ω
conforms to σ Max . Furthermore, using again Lemma 22,

TP( π) = lim inf n→+∞ TP π 1 (ex, v j1 , i 1 ) • • • π i (ex, v ji , j i ) + nTP(u 1 • • • u ) and since TP(u 1 • • • u ) = TP(π i ) 0, we have TP( π) TP(π 1 (ex, v j1 , i 1 ) • • • π i (ex, v ji , j i )) m -1.
Thus π is a play starting from v that conforms to σ Max but whose totalpayoff is strictly less than m, which raises a contradiction. (b) If for all π i , TP(π i ) 1 (notice that it is implied by

TP(π i ) > 0). From Lemma 23, since Val G (v, σ Max ) m = -∞, we know that TP(proj(π 0 )) -(|V | -1)W . From Lemma 22, TP(π 0 ) -(|V | -1)W . Therefore TP(π 1 (ex, v j1 , i 1 ) • • • π N ) -(|V | -1)W + N = (|V | -1)W + 1 m
which contradicts the assumption that

TP(π 1 (ex, v j1 , i 1 ) • • • π N ) < m.
We have shown that MCR(π) m for all play π starting in (v, k) and conforming to σ m Max , which implies

Val G K ((v, k), σ m Max ) m. v1 in, v1 v2 in, v2 t v3 in, v3 -1 -W max(0, Y (v2)) max(0, Y (v1)) max(0, Y (v3))
Fig. 5 MCR game G Y associated with the total-payoff game of Fig. 2 Using the two last lemmas, we can now prove Proposition 21 by relating precisely values in G and G k .

Proof (of Proposition 21) Let v ∈ V be a vertex. We consider three cases:

-If Val G (v) = -∞, then for all m, Val G (v) m. By Lemma 25, Val G K (v, K) m. Therefore Val G K (v, K) = -∞. -If Val G (v) = m ∈ [-(|V | -1)W, (|V | -1)W ]. Then, m Val G (v) m. Thus, by
Lemmas 25 and 26, m

Val G K (v, K) m. Therefore Val G K (v, K) = m. -If Val G (v) = +∞, then Val G (v) (|V | -1)W + 1. By Lemma 26, Val G K (v, K) (|V | -1)W + 1.

Value iteration algorithm for total-payoff games

By Proposition 21, an immediate way to obtain a value iteration algorithm for total-payoff games is to build game G K , run Algorithm 1 on it, and map the computed values back to G. We take advantage of the structure of G K to provide a better algorithm that avoids building G K . Intuitively, we first compute the values of the vertices in the last copy of the game (vertices of the form (v, 1), (in, v, 1) and (ex, v, 1)), then of those in the penultimate (vertices of the form (v, 2), (in, v, 2) and (ex, v, 2)), and so on. We first sketch the intuitions that lead to the formalisation of these ideas. Let Z j be a vector mapping each vertex v of G to the value Z j (v) of vertex (v, j) in G K . Then, we define an operator H such that Z j+1 = H(Z j ). Thus, assuming that we have computed the values of all vertices in the jth copy, H returns the value of the vertices in the j +1st copy. In other words, the definition of H(Y ) for some vector Y is to extract from G K one copy of the game (that we call G Y ), and make Y appear in the weights of some edges as illustrated in Fig. 5. This game, G Y , simulates a play in G in which Min can opt for 'leaving the game' at each round (by moving to the target), obtaining max(0, Y (v)), if v is the current vertex. Then, we can define H(Y )(v) as the value of v in G Y . By construction, it is easy to see that Z j+1 = H(Z j ) holds for all j 1, i.e. that H indeed corresponds to computing the values of the vertices in the j + 1st copy, given the values in the jth copy. Furthermore, letting Z 0 (v) = -∞ for all v, and Z 1 = H(Z 0 ), we will prove that: (i) H is monotonic, but may not be Scott-continuous; (ii) the sequence (Z j ) j 0 converges towards Val G . These arguments are the main ideas justifying Algorithm 2 to solve total-payoff games. Intuitively, the outer loop computes, in variable Y, a Algorithm 2: A value iteration algorithm for total-payoff games Input: Total-payoff game G = V, E, ω, TP , W largest weight in absolute value

1 foreach v ∈ V do Y(v) := -∞ 2 repeat 3 foreach v ∈ V do Ypre(v) := Y(v); Y(v) := max(0, Y(v)); X(v) := +∞ 4 repeat 5 Xpre := X 6 foreach v ∈ V Max do X(v) := max v ∈E(v) ω(v, v ) + min(Xpre(v ), Y(v )) 7 foreach v ∈ V Min do X(v) := min v ∈E(v) ω(v, v ) + min(Xpre(v ), Y(v )) 8 foreach v ∈ V such that X(v) < -(|V | -1)W do X(v) := -∞ 9 until X = Xpre 10 Y := X 11 foreach v ∈ V such that Y(v) > (|V | -1)W do Y(v) := +∞ 12 until Y = Ypre 13 return Y
non-decreasing sequence of vectors whose limit is Val G , and that is stationary (this is not necessarily the case for the sequence (Z j ) j 0 ). Line 1 initialises Y to Z 0 . Each iteration of the outer loop amounts to running Algorithm 1 to compute H(Ypre) (lines 3 to 10), then detecting if some vertices have value +∞, updating Y accordingly (line 11, following the second item of Proposition 21). We will show that, for all j > 0, if we let Y j be the value of Y after the j-th iteration of the main loop, then Z j Y j Val G , which ensures the correctness of the algorithm.

Formal proof of the correctness of Algorithm 2 Let us now formalise the arguments sketched above to establish the correctness of Algorithm 2. We first define formally the game G Y described informally above. With the original total-payoff game G = V, E, ω, TP and with every vector Y ∈ Z V ∞ , we associate the MCR game G Y = V , E Y , ω Y , {t}-MCR as follows. The sets of vertices are given by

V Max = V Max {t} and V Min = V Min {(in, v) | v ∈ V } .
As in game G j , vertices of the form (in, v) are called interior vertices. Edges are defined by

E Y = v, (in, v ) | (v, v ) ∈ E (in, v), v | v ∈ V (in, v), t | v ∈ V ∧ Y (v) = +∞ {(t, t)}
while weights of edges are defined, for all (v, v ) ∈ E, by

ω Y v, (in, v ) = ω(v, v ) , ω Y (in, v), t = max 0, Y (v) , ω Y (in, v), v = 0.
It is easy to see that lines 3 to 10 are a rewriting of Algorithm 1 in the special case of game G Y : in particular, neither the target vertex nor interior vertices are explicit, but their behaviour is taken into account by the transformation performed in line 3 and the operators min used in the inner computation of lines 6 and 7. Hence, if we define H(Y )(v) = Val G Y (v) for all v ∈ V , we can say that if inside the main loop, at line 3 the variable Y has value Y , then after line 10, it has value H(Y ).

Notice that the game G Y resembles a copy of G in the game G j of the previous section. More, precisely, from the values (Val G j (v, j)) v∈V in the jth copy, we can deduce the values in the (j + 1)th copy by an application of operator H:

Val G j+1 (v, j + 1) v∈V = H (Val G j (v, j)) v∈V .
(5)

Although the 0th copy is not defined, we abuse the notation and set Val G 0 (v, 0) = -∞, which still conforms to the above equality. Furthermore, due to the structure of the game G j notice that for all j j ,

Val G j (v, j) = Val G j (v, j).
Notice the absence of exterior vertices (ex, v , j) in game G Y , replaced by the computation of the maximum between 0 and X(v ) on the edge towards the target. Before proving the correctness of Algorithm 2, we prove several interesting properties of operator H.

Proposition 28 H is a monotonic operator.

Proof For every vector Y ∈ Z V ∞ , let F Y be the operator associated with the MCR game as defined in Section 3, i.e. for all X ∈ Z V ∞ , and for all

v 1 ∈ V F Y (X)(v 1 ) =          max v2∈E Y (v1) ω Y (v 1 , v 2 ) + X(v 2 ) if v ∈ V Max \ {t} min v2∈E Y (v1) ω Y (v 1 , v 2 ) + X(v 2 ) if v ∈ V Min 0 if v 1 = t .
We know from Corollary 11 that

Val G Y is the greatest fixed point of F Y . Consider now two vectors Y, Y ∈ Z V ∞ such that Y Y . First, notice that for all X ∈ Z V ∞ : F Y (X) F Y (X) . (6)
Indeed, to get the result it suffices to notice that for all

v 1 , v 2 ∈ V , ω Y (v 1 , v 2 ) ω Y (v 1 , v
2 ) (the only differences are on the edges ((in, v), t)).

Consider then the vector X 0 defined by X 0 (v 1 ) = +∞ for all v 1 ∈ V . Given Y Y , from (6), we have that F Y (X 0 ) F Y (X 0 ), then a simple induction shows that for all i,

F i Y (X 0 ) F i Y (X 0 ). Thus, since Val G Y (respectively, Val G Y ) is the greatest fixed point of F Y (respectively, F Y ), we have Val G Y Val G Y . As a consequence H(Y ) H(Y ).
Notice that H may not be Scott-continuous, as shown in the following example.

Example 29 Recall that, in our setting, a Scott-continuous operator is a mapping

F : Z V ∞ → Z V
∞ such that for every sequence of vectors (x i ) i 0 having a limit xω, the sequence (F (x i )) i 0 has a limit equal to F (xω).

We present a total-payoff game whose associated operator H is not continuous. Let G be the total-payoff game containing one vertex v of Min and a self loop of weight -1 (as depicted in Fig. 6). For all

Y ∈ Z, in the MCR game G Y , v v -1 G v in, v t -1 0 Y 0 G Y Fig. 6
An example where the operator H is not Scott-continuous.

has value -∞, indeed one can take the loop an arbitrary number of times before reaching the target, ensuring a value arbitrary low. Therefore, if we take an increasing sequence (Y i ) i 0 of integers, H(Y i )(v) = -∞ for all i, thus the limit of the sequence (H(Y i )) i 0 is -∞. However, the limit of the sequence (Y i ) i 0 is +∞ and H(+∞)(v) = +∞, since the target is not reachable anymore (in case the weight of an edge would be +∞, it is removed in the definition of E Y ). Thus, H is not Scott-continuous.

In particular, we may not use the Kleene sequence, as we have done for MCR games, to conclude to the correctness of our algorithm. Anyhow, we will show that the sequence (Y j ) j 0 indeed converges towards the vector of values of the total-payoff game. We first show that this vector is a pre-fixed point of H starting with a technical lemma that is useful in the subsequent proof.

Lemma 30 Let σ Min be a strategy for Min in G, and π = v 1 • • • v i a finite play that conforms to σ Min . Then:

TP(v 1 • • • v i ) + Val G (v i ) Val G (v 1 , σ Min ) .
Proof Let σ Max be an optimal strategy for Max and

v i v i+1 v i+2 • • • be the play Play(v i , σ Max , σ Min ). Since σ Max is optimal, TP(v i v i+1 v i+2 • • • ) Val G (v i ). Further- more notice that v 1 • • • v i v i+1 • • • conforms to the strategy σ Min , therefore we have TP(v 1 v 1 • • • v i v i+1 • • • ) Val G (v 1 , σ Min ). Thus: TP(v 1 • • • v i ) + Val G (v i ) TP(v 1 • • • v i ) + TP(v i v i+1 • • • ) TP(v 1 v 1 • • • v i v i+1 • • • ) Val G (v 1 , σ Min ) . Lemma 31 Val G is a pre-fixed point of H, i.e. H(Val G ) Val G .
Proof To ease the notations, we denote Val G by Y in this proof. To prove this lemma, we just have to show that for all v 1 ∈ V , the value of v 1 in the MCR game G Y is at most its value in the original total-payoff game G, i.e.

H(Y )(v 1 ) = Val G Y (v 1 ) Y (v 1 ) . Let σ Min be a memoryless strategy in G such that Val G (v 1 , σ Min ) m for some m ∈ Z {+∞}. And let σ m
Min be a strategy in G X defined for all finite play πv with v ∈ V Min by σ m Min (πv ) = (in, σ Min (v )) and for all finite play π(in, v ),

σ m Min (π(in, v )) = t if TP(π(in, v )t) m v otherwise .
Notice that, by construction, all plays starting in v 1 , conforming to σ m Min and that reach the target have value at most m. Assume by contradiction that there exists a play

v 1 (in, v 2 )v 2 (in, v 3 ) • • • ∈ Play(v 1 , σ m
Min ) that never reaches t. In particular, for all i,

TP(v 1 (in, v 2 ) • • • (in, v i )t) > m.
Again by construction, v 1 v 2 • • • is a play in G that conforms to σ Min and for all i,

TP(v 1 (in, v 2 ) • • • (in, v i )) = TP(v 1 • • • v i ).
-If there exists i 2 such that Y (v i ) = Val G (v i ) 0, then

TP(v 1 (in, v 2 ) • • • (in, v i )t) = TP(v 1 (in, v 2 ) • • • (in, v i )) + ω X ((in, v i ), t) = TP(v 1 • • • v i ) + max(0, Y (v i )) = TP(v 1 • • • v i ) + Y (v i ) Val(v 1 , σ Min ) (from Lemma 30) m which raises a contradiction. -If for all i 2, Y (v i ) = Val G (v i ) < 0 then for all i 2, TP(v 1 (in, v 2 ) • • • (in, v i )t) = TP(v 1 (in, v 2 ) • • • (in, v i )) = TP(v 1 • • • v i ) > m . Thus TP(v 1 v 2 • • • ) > m, which contradicts the fact that v 1 v 2 • • • conforms to σ Min and Val G (v 1 , σ Min ) m. Thus Val G Y (v 1 , σ Min ) m. As a consequence, Val G Y (v 1 ) Val G (v 1 ).
Remark 32 Even if it is not necessary for the proof of Theorem 27, we can show that Val G is the least pre-fixed point of H. Notice that, by monotonicity of H, this directly implies that Val G is the least fixed point of H. The proof that Val G is the least pre-fixed point of H amounts to better understand the convergence of the sequence (Val G j (v, j)) j 0 (remember that we set Val G 0 (v, 0) = -∞ for all v). Indeed, Proposition 21 already shows that for vertices v such that Val G (v) < +∞, (Val G j (v, j)) j 1 converges towards Val G (v). It is also the case for vertices v such that Val G (v) = +∞ as we show in Lemma 33 below. Then, consider a pre-fixed point Y of H, i.e. H(Y ) Y . Since Val G 0 (v, 0) = -∞ Y (v) and H is monotonous, we prove by immediate induction that Val G j (v, j) Y (v) for all v and j 0: indeed, if Val G j (v, j) Y (v) for all v, we have

(Val G j+1 (v, j + 1)) v∈V = H((Val G j (v, j)) v∈V ) H(Y ) Y .
This implies that Val G Y , showing that Val G is indeed the least pre-fixed point of H, and hence the least fixed point of H, by the above reasoning.

Before continuing the proof of Theorem 27, we show the result used in the previous remark. that Val G (v) > (|V | -1)W . By Corollary 24, we know that Val G (v) = +∞, so that Y j+1 (v) = +∞ = Val G (v). In the overall, we have proved

(i) For every finite play v 1 • • • v k conforming to σ Max starting in v 1 = v, if there exists i < j such that v i = v j then TP(v i • • • v j ) 1. (ii) For every m ∈ N, k m|V | + 1 and v 1 • • • v k a finite play conforming to σ Max and starting in v 1 = v, TP(v 1 • • • v k ) m -(|V | -1)W . v 1 v 2 v 3 -W 1 W 0 (b)
Val G j+1 (v, j + 1) Y j+1 (v) Val G (v)
We are now able to prove the correctness and termination of the algorithm.

Proof (of Theorem 27) For j = K (remember that K was defined in the previous section), the invariant of Lemma 34 becomes

Val G K (v, K) Y K (v) Val G (v)
for all vertices v ∈ V . Notice that the iteration may have stopped before iteration K, in which case the sequence (Y j ) j 0 may be considered as stationary. In case

Val G (v) = +∞, Proposition 21 proves that Val G K (v, K) = Val G (v), so that we have Y K (v) = Val G (v). In case Val G (v) = +∞, Proposition 21 shows that Val G K (v, K) > (|V | -1)W : by the operation performed at line 11, we obtain that Y K (v) = +∞ = Val G (v). Hence, K = |V |(2(|V | -1)W + 1
) is an upper bound on the number of iterations before convergence of Algorithm 2, and moreover, at the convergence, the algorithm outputs the vector of optimal values of the total-payoff game.

Convergence speed of the algorithm Observe that the number of iterations in each internal loop is controlled by Theorem 3. On the example of Fig. 2, only 2 external iterations are necessary, but the number of iterations of each internal loop would be 2W . By contrast, for the total-payoff game depicted in Fig. 7, each internal loop requires 2 iterations to converge, but the external loop takes W iterations to stabilise. A combination of both examples would experience a pseudo-polynomial number of iterations to converge in both the internal and external loops, matching the W 2 term of the above complexity: this gives rise to the parametric example of Fig. 8.

Optimal strategies

In Section 3, we have shown, for all MCR games, the existence of a fake-optimal NC-strategy permitting to reconstruct an optimal finite-memory strategy for Min (if every vertex has value different from -∞, or a strategy ensuring every possible threshold for vertices with value -∞). Given a total-payoff game G, if we apply this construction to the game G Val G , we obtain an NC-strategy σ Min . Consider the strategy σ Min , obtained by projecting σ Min on V as follows: for all finite plays π and vertices σ Min is optimal for Min in G. Notice that σ Min , and hence σ Min , can be computed during the last iteration of the value iteration algorithm, as explained in the case of MCR games in Section 3.4. A similar construction can be done to compute an optimal strategy for Max.

v ∈ V Min , we let σ Min (πv) = v if σ Min (v) = (in, v ). We show thereafter that v 1 v 2 v 3 v 4 v 5 v 6 v 7 . . . v 3(n-1) v 3n-2 v 3n-1 v 3n t -W -1 0 0 1 W -W -1 0 0 1 W W -W -1 0
Theorem 35 The memoryless strategy σ Min is optimal in G.

Proof We start by showing that for all v, exist a vertex v that appears infinitely often in this play. As σ Min is an NC-strategy, the accumulated cost of the chunk of the play between two occurrences of v has weight at most -1, thus the total payoff of

v 0 (in, v 1 )v 1 (in, v 2 ) • • • is -∞.
As the total-payoff of this play is equal to the total payoff of π, we have that TP(π) = -∞.

Otherwise, Min asks at some point to go to the target: let iπ be the first index such that σ Min (in, v iπ ) = t. As the strategy σ Min is a fake-optimal NCstrategy, we know that the accumulated cost of π until the target verifies TP(π) = MCR(π)

Val G Val G (v 0 ). As Val G is a fixed point of H (see Remark 32), we have that for all v, Val G Val G (v) = H(Val G (v)) = Val G (v), thus TP(π) Val G (v 0 ). We have TP(v 0 • • • v iπ ) = TP v 0 (in, v 1 )v 1 • • • v iπ-1 (in, v iπ ) = TP(π)-ω (in, v iπ ), t . From (1), we have ω (in, v iπ ), t = Val G (v iπ ), thus TP(v 0 • • • v iπ ) Val G (v 0 ) -Val G (v iπ ), which proves (2). Now let us prove the theorem. Let v be a vertex in G. If Val G (v) = +∞ then trivially Val G (v, σ Min ) +∞ = Val G (v). Otherwise let π = v 0 v 1 • • • be a play in G that conforms with σ Min such that v = v 0 . If TP(π) = -∞ then TP(π) Val G (v).
Otherwise we construct inductively an increasing sequence of indices i

0 , i 1 , . . . such that TP(v ij • • • v ij+1 ) Val G (v ij ) -Val G (v ij+1
) (for all j) as follows. First, we let i 0 = 0. Then, for all j, let π

= v ij v ij +1 • • • be the current suffix of π: since TP(π) = -∞, we have TP(π ) = -∞, thus (2) shows that by letting i j+1 = i j + i π , we obtain TP(v ij • • • v ij+1 ) Val G (v ij ) -Val G (v ij+1
), and we know that σ Min (in, v ij+1 ) = t.

We can then show, by a direct induction, that for all j 1, TP

(v 0 • • • v ij ) Val G (v) -Val G (v ij ). From (1), we know that Val G (v ij ) 0, thus TP(v 0 • • • v ij ) Val G (v). Hence TP(π) = lim inf n→∞ TP(v 0 • • • vn) lim inf j→∞ TP(v 0 • • • v ij ) Val G (v) .

Implementation and heuristics

In this section, we report on a prototype implementation of our algorithms.7 For convenience reasons, we have implemented them as an add-on to PRISM-games [START_REF] Chen | Automatic verification of competitive stochastic systems[END_REF], although we could have chosen to extend another model-checker as we do not rely on the probabilistic features of PRISM models (i.e. we use the PRISM syntax of stochastic multi-player games, allowing arbitrary rewards, and forbidding probability distributions different of Dirac ones). We then use rPATL specifications of the form C R min / max=? [F ∞ ϕ] and C R min / max=? [F c ⊥] to model respectively MCR games and total-payoff games, where C represents a coalition of players that want to minimise/maximise the payoff, and ϕ is another rPATL formula describing the target set of vertices (for total-payoff games, such a formula is not necessary). We have tested our implementation on toy examples. On the parametric one Fig. 8, results obtained by applying our algorithm for total-payoff games are summarised in Table 1, where for each pair (W, n), we give the time t in seconds, the number ke of iterations in the external loop, and the total number k i of iterations in the internal loop. Notice that due to the very little memory consumption of the algorithm, there is no risk of running out of memory. However, the execution time can become very large. For instance, in case W = 500 and n = 1000, the execution time becomes 536s whereas the total number of iterations in the internal loop is greater than a million.

Acceleration techniques

We close this section by sketching two techniques that can be used to speed up the computation of the fixed point in Algorithms 1 and 2. We fix a weighted graph V, E, ω . Both accelerations rely on a topological order of the strongly connected components (SCC for short) of the graph, given as a function c : V → N, mapping each vertex to its component, verifying that (i) c(V ) = {0, . . . , p} for some p 0, (ii) c -1 (q) is a maximal SCC for all q, (iii) and c(v) c(v ) for all (v, v ) ∈ E. 8 In case of an MRC game with t the unique target, c -1 (0) = {t}. Intuitively, c induces a directed acyclic graph whose vertices are the sets c -1 (q) for all q ∈ c(V ), and with an edge (S 1 , S 2 ) if and only if there are

v 1 ∈ S 1 , v 2 ∈ S 2 such that (v 1 , v 2 ) ∈ E.
The first acceleration heuristic is a divide-and-conquer technique that consists in applying Algorithm 1 (or the inner loop of Algorithm 2) iteratively on each c -1 (q) for q = 0, 1, 2, . . . , p, using at each step the information computed during steps j < q (since the value of a vertex v depends only on the values of the vertices v such that c(v ) c(v)).

The second acceleration heuristic consists in studying more precisely each component c -1 (q). Having already computed the optimal values Val(v) of vertices v ∈ c -1 ({0, . . . , q -1}), we ask an oracle to precompute a finite set Sv ⊆ Z∞ of possible optimal values for each vertex v ∈ c -1 (q). For MCR games and the inner iteration of the algorithm for total-payoff games, one way to construct such a set Sv is to consider that possible optimal values are the one of non-looping paths inside the component exiting it, since, in MCR games, there exist optimal strategies for both players whose outcome is a non-looping path (see Section 3).

Algorithm 3 and 4 are enhanced versions of Algorithm 1 and 2 respectively, that apply these acceleration heuristics.

Finally, we note that we can identify classes of weighted graphs for which there exists an oracle that runs in polynomial time and returns, for all vertices v, a set Sv of polynomial size. On such classes, Algorithms 1 and 2, enhanced with our two acceleration techniques, run in polynomial time. For instance, for all fixed positive integers L, the class of weighted graphs where every component c -1 (q) uses at Algorithm 3: Accelerated value iteration algorithm for min-cost reachability games Input: MCR game V, E, ω, {t}-MCR , SCC-decomposition c : V → {0, 1, . . . , p} and an oracle O(q, v) outputting sets (Sv) v∈c -1 (q)

1 X(t) := 0 2 for q = 1 to p do Input: Total-payoff game G = V, E, ω, TP , SCC-decomposition c : V → {0, 1, . . . , p} and an oracle O(q, v) outputting sets (Sv) v∈c -1 (q)

1 foreach v ∈ V do Y(v) := -∞ 2 for q = 0 to p do most L distinct weights (that can be arbitrarily large in absolute value) satisfies this criterion. Table 1 contains the results obtained with the heuristics on the parametric example presented before. Observe that the acceleration technique permits here to decrease drastically the execution time, the number of iterations in both loops depending not even anymore on W . Even though the number of iterations in the external loop increases with heuristics, due to the decomposition, less computation is required in each internal loop since we only apply the computation for the active component.

Conclusion

In this work, we have provided the first (to the best of our knowledge) pseudopolynomial time algorithm to solve total-payoff games with arbitrary (positive and negative) weights. This algorithm is a variation on the classical value iteration technique. To obtain this algorithm, we have reduced the problem of solving totalpayoff games to that of solving min-cost reachability (MCR) games, a variant of the former where the game stops as soon as a target vertex is reached (in which case the payoff of the plays is the total accumulated weight of the play up to the target). We believe that those MCR games are interesting by themselves, as they can be used to model problems where, for instance, a target configuration must be reached while ensuring a minimal energy spending. Notice also that they have been used as a building block for the resolution of priced timed games in [START_REF] Brihaye | Adding negative prices to priced timed games[END_REF]Brihaye et al ( , 2015a)). We have characterised the optimal strategies that one can extract in those total-payoff and MCR games. Finally, we have implemented our algorithms and proposed some heuristics that take into account the structure of the games to speed up the computation. As future works, we would like to push further the MCR games in a context of non-zero sum games where each player wants to optimise its accumulated cost until reaching its own target. As a possible direction, the search for Nash equilibria in this context will most likely benefit from our better understanding of optimal strategies for both players in the underlying zero-sum games. This bridge from zero-sum to non-zero-sum games has already been investigated for concurrent priced games by [START_REF] Klimoš | Nash equilibria in concurrent priced games[END_REF], and by [START_REF] Brihaye | Multiplayer cost games with simple nash equilibria[END_REF] to find simple Nash equilibria for large classes of multiplayer cost games.

A Comparison with the longest shortest path problem of Björklund and Vorobyov

Björklund and Vorobyov have studied games related to our min-cost reachability games, as the longest shortest path problem (LSP for short) in (Björklund and Vorobyov, 2007). To clarify the following discussion, let us recall the definition of LSP, adapted to our syntax.

The LSP problem considers a weighted graph G, whose vertices are partitioned into two players, and equipped with a single target vertex t. The problem asks to find a memoryless strategy σ Max of Max such that in the graph Gσ Max , obtained from G by deleting all outgoing edges from vertices of V Max except those selected in σ Max , the length of the shortest path from every vertex to the target t is as large as possible (over all memoryless strategies). The definition of paths from a vertex v to the target is, however, very different from ours: such a path may indeed be a finite play, without cycle, from v to the target t (in which case its length is the sum of the weights of edges). However, every cycle containing v (even if it can not reach the target) is also considered as a path to the target. The length of such cycle is defined as follows: Vorobyov, 2007) proves that the decision version of the LSP (i.e. deciding if the LSP of a vertex is positive or not in a given graph) is in NP ∩ co-NP, and they claim (without formal proof) that their pseudo-polynomial time algorithm permits to decide this problem. This requires a first transformation of the problem, so that no zero weight cycles remain in the weighted graph. This transformation, explained above Proposition 9.1, is correct but does not preserve the LSP of the vertices, so that their algorithm do not compute the LSP distance of vertices, but only study their positivity.

Hence, the comparison between our definition of min-cost reachability and the definition of LSP can be summarised as follows:

1. Either one relies on the first definition of LSP given in the article. In this case, Björklund and Vorobyov propose a pseudo-polynomial time algorithm to compute the LSP, but these values do not match our definition of the min-cost reachability payoff, as demonstrated by the above example. 2. Or one relies on the second definition. In this case, we believe that the LSP values may match our definition of min-cost reachability but the article does not explain formally how to compute those new values.

It is plausible that the pseudo-polynomial time algorithm of Björklund and Vorobyov could be adapted to compute the LSP value according to the second definition. Yet, even in this case, there are several points of comparison worth mentioning:

1. The worst-case complexity of the algorithm proposed by Björklund and Vorobyov is O(|V | 2 |E|W ), which matches ours (see Proposition 5). Nevertheless, our solution is much easier to describe and to implement: while they must make repeated calls to a modified version of the Bellman-Ford algorithm (the modification is crucial to obtain their complexity), we have a simple fixed point algorithm. 2. Our algorithm exploits the value iteration paradigm (that can be seen as a backward induction), while theirs is a strategy iteration algorithm. Because of that, there are examples on which our algorithm is more efficient that theirs (although the worst-case complexity is the same). As an example, the LSP instance presented in Fig. 2 of (Björklund and Vorobyov, 2007), with 2n + 1 vertices but a biggest weight W exponential in n, requires an exponential number 2 n of iterations for the strategy iteration algorithm, but our value iteration algorithm (based on backward induction) would solve it in linear time with respect to n. More precisely, with our tool, we are able to compute the values of this game in less than a millisecond for constant n = 15 (i.e. a game with 32 vertices and largest weight W ≈ 2.68 • 10 8 ): the value of the initial state obtained is 4.74 • 10 9 , and as aforementioned, the number of iterations that our value iteration requires is 16, linear in n. Our tool being an add-on of the PRISM model-checker, relying on the use of integer rewards, we have not been able to build the game for a value n greater than 15. 3. We propose several acceleration heuristics that perform well on several examples we have tried. These accelerations cannot easily be incorporated in their algorithm (because it is a strategy iteration algorithm). 4. Finally, from the theoretical point of view, Björklund and Vorobyov do not study the strategies of the opponent player Min. In contrast, our study allows us to produce optimal strategies for both players, and in particular, show that memoryless strategies may not be sufficient for Min, whereas they are enough for Max.

Fig. 1

 1 Fig. 1 (a) A total-payoff game, and (b) the evolution of the partial sums in π.

Lemma 23

 23 Let v ∈ V , and σ Min (respectively, σ Max ) be a memoryless strategy for Min (respectively, Max) in the total-payoff game G, such that Val(v, σ Min ) = +∞ (respectively, Val(v, σ Max ) = -∞). Then for all finite play π conforming to σ Min (respectively, to σ Max ), TP(π) (|V | -1)W (respectively, TP(π) -(|V | -1)W ).

  23 shows that all finite play π that conforms to σ Min verifies TP(π) -(|V | -1)W , therefore Val(v) -(|V | -1)W . One can similarly prove that TP(v) (|V | -1)W .

Theorem 27

 27 If a total-payoff game G = V, E, ω, TP is given as input, Algorithm 2 outputs the vector Val G of optimal values, after at most K = |V |(2(|V | -1)W + 1) iterations of the external loop. The complexity of the algorithm is O(|V | 4 |E|W 2 ).

Lemma 33

 33 Let v ∈ V such that Val G (v) = +∞, and σ Max a memoryless strategy for Max in G such that Val G (v, σ Max ) = +∞.Then the following holds:

Fig. 7

 7 Fig.7An example total-payoff game where each execution of the inner loop requires two iterations while the outer loop takes W iterations to stabilise.

0 Fig. 8

 08 Fig. 8 Parametric weighted graph

3 (

 3 Sv) v∈c -1 (q) := O(q, X) /* Use of the oracle */4 foreach v ∈ c -1 (q) do X(v) := max Sv c -1 (q) ∩ V Max do 8 X(v) := max v ∈E(v) ω(v, v ) + Xpre(v ) 9 foreach v ∈ c -1 (q) ∩ V Min do 10 X(v) := min v ∈E(v) ω(v, v ) + Xpre(v ) 11 foreach v ∈ c -1 (q) do X(v) := max Sv ∩ [-∞, X(v)] 12 until X = Xpre 13 return XAlgorithm 4: Accelerated value iteration algorithm for total-payoff games

3 (

 3 Sv) v∈c -1 (q) := O(q, Y) /* Use of the oracle */ 4 repeat 5 foreach v ∈ c -1 (q) do 6 Ypre(v) := Y(v); Y(v) := max(0, Y(v)); X(v) := max Sv V Max ∩ c -1 (q) do 10 X(v) := max v ∈E(v) ω(v, v ) + min(Xpre(v ), Y(v )) 11 foreach v ∈ V Min ∩ c -1 (q) do 12 X(v) := min v ∈E(v) ω(v, v ) + min(Xpre(v ), Y(v )) 13 foreach v ∈ c -1 (q) do X(v) := max Sv ∩ [-∞, X(v)] 14 until X = Xpre 15 Y := X 16 foreach v ∈ V such that Y(v) > (|V | -1)W do Y(v) := +∞ 17 until Y = Ypre 18 return Y

Fig. 9

 9 Fig. 9 An instance of the longest shortest path problem

  σ Min ) be respectively the lower and upper values of v. We may easily show that Val G Val G . We say that strategies σ Max of Max and σ Min of Min are optimal if, for all vertices

  Val

i (v) = infσ Min sup σ Max MCR i (Play(v, σ Max , σ Min )) (

where σ Max and σ Min are respectively strategies of Max and Min).

  Val i evolves over the first |V | + 1 steps. The next lemma states that, for each node v, the sequence Val 0 (v), Val 1 (v), . . . ,

	Val	i (v), . . . , Val	|V | (v) is of the form
			+∞, +∞, . . . , +∞ , a k , a k+1 , . . . , a |V |
			k times

  Val

0 (v) 0 × W = 0, which is true by definition of Val 0 . Or v = t. In this case, k > 0, and we must show that Val 0 (v) = +∞, which is true again by definition of Val 0 .

  Lemma 9 In an MCR game where all values are finite, the sequence(Val Min ): otherwise, we could iteratively remove every possible non-negative cycle of the finite play before reaching t (hence reducing the cost of the play) and obtain a play without cycles before reaching t with a cost less than -(|V | -1)W , which is impossible (since it should be of length at most |V | -1 to cross at most one occurrence of each vertex). Consider the first negative cycle in the play. After the first occurrence of the cycle, we let Min choose its actions like in the cycle. By this way, we can construct another strategy σ Min for Min, verifying that for every memoryless strategy σ Max of Max (this would not be true for general strategies of Max), we have MP(Play(v, σ Max , σ Min )) being the weight of the negative cycle in which the play finishes. Since for mean-payoff games, memoryless strategies are sufficient for Max, we deduce that Val G (v) < 0.This reasoning permits to prove that at every step i, Val i (v) -(|V | -1)W + 1 for all vertices v. Recall from Corollary 8 that, after |V | steps in the sequence, all vertices are assigned a value smaller that |V |W . Moreover, we know that the sequence is non-increasing (see (1)). In summary, for all k 0 and for all vertices v: Val |V |+k (v) |V |W Hence, in the worst case a strictly decreasing sequence will need (2|V | -1)W |V | steps to reach the lowest possible value where all vertices are assigned -(|V | -1)W + 1 from the highest possible value where all vertices are assigned |V |W . Thus, taking into account the |V | steps to reach a finite value on all vertices, the sequence stabilises in at most (2|V | -1)W |V | + |V | steps. Let us thus denote by Val the value obtained when the sequence (Val Val Val. Let us show that Val Val. Let v ∈ V be a vertex. Since Val(v) is a finite integer, there exists a strategy σ Min for Min that realises this value, i.e. Val(v) = sup σ Max MCR(Play(v, σ Max , σ Min )). Notice that this holds because the values are integers, inducing that the infimum in the definition of Val

	Val(v)
	-(|V | -1)W + 1

i ) i 0 stabilises after at most (2|V | -1)W |V | + |V | steps.

Proof We first show that if Min can secure, from some vertex v, a payoff less than -(|V | -1)W , i.e.

Val(v)

< -(|V | -1)W , then it can secure an arbitrarily small payoff from that vertex, i.e.

Val(v)

= -∞, which contradicts our hypothesis that the value is finite. Hence, let us suppose that there exists a strategy σ Min for Min such that Val(v, σ Min ) < -(|V | -1)W . Let G be the mean-payoff game studied in Proposition 4. We will show that Val G (v) < 0, which permits to conclude that Val G (v) = -∞. Let σ Max be a memoryless strategy of Max. By hypothesis, we know that MCR(Play(v, σ Max , σ Min )) < -(|V |-1)W . This ensures the existence of a cycle with negative cost in the play Play(v, σ Max , σ i ) i 0 stabilises. We are now ready to prove that this value is the actual value of the game:

Lemma 10 For all MCR games where all values are finite: Val = Val .

Proof We already know that

Table 1

 1 Results of value iteration on a parametric example

			without heuristics		with heuristics
	W	n	t	ke	k i	t	ke	k i
	50	100	0.52s	151	12,603	0.01s 402	1,404
	50	500	9.83s	551	53,003	0.42s 2,002 7,004
	200 100	2.96s	301	80,103	0.02s 402	1,404
	200 500	45.64s 701	240,503	0.47s 2,002 7,004
	500 1,000	536s 1,501 1,251,003 2.37s 4,002 14,004

An example of practical application would be to perform controller synthesis taking into account energy consumption. On the other hand, the problem of computing the values in certain classes of priced timed games has recently been reduced to computing the values in min-cost reachability games[START_REF] Brihaye | Adding negative prices to priced timed games[END_REF].

Our results can easily be extended by substituting a lim sup for the lim inf. The lim inf is more natural since we adopt the point of view of the maximiser Max, where the lim inf is the worst partial sum seen infinitely often.

In the context of stochastic models like Markov decision processes,[START_REF] Strauch | Negative dynamic programming[END_REF] already noticed that in the presence of arbitrary weights, the value iteration algorithm does not necessarily converge towards the accurate value:[START_REF] Puterman | Markov Decision Processes[END_REF] gives a more detailed explanation inEx. 7.3.3.

This is not needed in the proof, but notice that Min necessarily modifies its strategy here, i.e. owns at least one vertex of the cycle. Otherwise, the value in the MCR game G would not be -∞.

It suffices to add a vertex of the opponent in-between two vertices of the same player related by a transition in G: in this vertex, the opponent has no choice but to follow the transition chosen by the first player.

Source and binary files, as well as some examples, can be downloaded from http://www. ulb.ac.be/di/verif/monmege/tool/TP-MCR/.

Such a mapping is computable in linear time, e.g., by Tarjan's algorithm[START_REF] Tarjan | Depth first search and linear graph algorithms[END_REF].

Acknowledgements The authors are indebted to Jean-François Raskin for enlightening discussions, and, in particular, for suggesting the example in Fig. 2. They also want to thank reviewers of this version, as well as the short version Brihaye et al (2015b), that helped greatly improving its content.

was sponsored by EU FP7 project Cassting.

(iii) For all m ∈ N and k (m

(iv) lim j→∞ Val G j (v, j) = +∞.

Proof We prove (i) by contradiction. Therefore, assume that TP(

We prove (ii) by induction on m. The base case is straightforward. For the inductive case, let m > 0, k m|V | + 1 and v 1 • • • v k a finite play conforming to σ Max and starting in v 1 = v. Since k m|V |+1 |V |+1 there exists i < j |V |+1 such that v i = v j . Thus:

Let π be a play starting in (v, k) and conforming to σ Max . If π does not reach t, then

Item (iv) is then a direct consequence of (iii).

We are now ready to state and prove the inductive invariant allowing us to show the correctness of Algorithm 2.

Lemma 34 Before the j-th iteration of the external loop of Algorithm 2, we have

) for all vertex v ∈ V . Suppose then that the invariant holds for j 0. We know (see ( 5)) that Val G j+1 (v, j + 1) = H((Val G j (v , j)) v ∈V ). Moreover, after the assignment of line 10, by definition of H, variable Y contains H(Y j ). The operation performed on line 11 only increases the values of vector Y, so that at the end of the jth iteration, we have H(Y j ) Y j+1 . Since H is monotonous, and by the invariant at step j, we obtain

Moreover, using again the monotony of H and Lemma 31, we have

A closer look at line 11 shows that H(Y j ) and Y j+1 coincide over vertices v such that H(Y j )(v) (|V | -1)W , and otherwise Y j+1 (v) = +∞. Hence, if H(Y j )(v) (|V |-1)W , we directly obtain Y j+1 (v) = H(Y j )(v) Val G (v). Otherwise, we know