arXiv:1503.04426v7 [cs.DS] 24 Apr 2016

An Improved Pseudo-Polynomial Upper Bound for the
Value Problem and Optimal Strategy Synthesis
in Mean Payoff Games
Carlo Comin ∗

Romeo Rizzi †

Abstract
In this work we offer an O(|V |2 |E|W ) pseudo-polynomial time deterministic algorithm for
solving the Value Problem and Optimal Strategy Synthesis in Mean Payoff Games. This improves by a factor log(|V |W ) the best previously known pseudo-polynomial time upper bound
due to Brim, et al. The improvement hinges on a suitable characterization of values, and a
description of optimal positional strategies, in terms of reweighted Energy Games and Small
Energy-Progress Measures.

Keywords: Mean Payoff Games, Value Problem, Optimal Strategy Synthesis, Energy Games,
Small Energy-Progress Measures, Pseudo-Polynomial Time.

1

Introduction

A Mean Payoff Game (MPG) is a two-player infinite game Γ := (V, E, w, hV0 ,V1 i), which is played
on a finite weighted directed graph, denoted GΓ := (V, E, w), the vertices of which are partitioned
into two classes, V0 and V1 , according to the player to which they belong. It is assumed that GΓ has
no sink vertex and that the weights of the arcs are integers, i.e., w : E → {−W, . . . , 0, . . . ,W } for
some W ∈ N.
At the beginning of the game a pebble is placed on some vertex vs ∈ V , and then the two players,
named Player 0 and Player 1, move the pebble ad infinitum along the arcs. Assuming the pebble
is currently on Player 0’s vertex v, then he chooses an arc (v, v0 ) ∈ E going out of v and moves
the pebble to the destination vertex v0 . Similarly, assuming the pebble is currently on Player 1’s
vertex, then it is her turn to choose an outgoing arc. The infinite sequence vs , v, v0 . . . of all the encountered vertices is a play. In order to play well, Player 0 wants to maximize the limit inferior of
n−1
w(vi , vi+1 ),
the long-run average weight of the traversed arcs, i.e., to maximize lim infn→∞ n1 ∑i=0
1 n−1
whereas Player 1 wants to minimize the lim supn→∞ n ∑i=0 w(vi , vi+1 ). Ehrenfeucht and Mycielski [5] proved that each vertex v admits a value, denoted valΓ (v), which each player can secure
by means of a memoryless (or positional) strategy, i.e., a strategy that depends only on the current
vertex position and not on the previous choices.
∗ Department of Mathematics, University of Trento, Trento, Italy; LIGM, Université Paris-Est, Marne-la-Vallée, Paris,
France. (carlo.comin@unitn.it)
† Department of Computer Science, University of Verona, Verona, Italy. (romeo.rizzi@univr.it)

1

Solving an MPG consists in computing the values of all vertices (Value Problem) and, for
each player, a positional strategy that secures such values to that player (Optimal Strategy Synthesis). The corresponding decision problem lies in NP ∩ coNP [11] and it was later shown by
Jurdziński [8] to be recognizable with unambiguous polynomial time non-deterministic Turing
Machines, thus falling within the UP ∩ coUP complexity class.
The problem of devising efficient algorithms for solving MPGs has been studied extensively
in the literature. The first milestone was that of Gurvich, Karzanov and Khachiyan [7], in which
they offered an exponential time algorithm for solving a slightly wider class of MPGs called Cyclic
Games. Afterwards, Zwick and Paterson [11] devised the first deterministic procedure for computing values in MPGs, and optimal strategies securing them, within a pseudo-polynomial time and
polynomial space. In particular, Zwick and Paterson established an O(|V |3 |E|W ) upper bound for
the time complexity of the Value Problem, as well as an upper bound of O(|V |4 |E|W log(|E|/|V |))
for that of Optimal Strategy Synthesis [11].
Recently, several research efforts have been spent in studying quantitative extensions of infinite games for modeling quantitative aspects of reactive systems [2–4]. In this context quantities
may represent, for example, the power usage of an embedded component, or the buffer size of
a networking element. These studies have brought to light interesting connections with MPGs.
Remarkably, they have recently led to the design of faster procedures for solving them. In particular, Brim, et al. [3] devised faster deterministic algorithms for solving the Value Problem and
Optimal Strategy Synthesis in MPGs within O(|V |2 |E|W log(|V |W )) pseudo-polynomial time and
polynomial space.
To the best of our knowledge, this is the tightest pseudo-polynomial upper bound on the time
complexity of MPGs which is currently known.
Indeed, a wide spectrum of different approaches have been investigated in the literature. For instance, Andersson and Vorobyov [1] provided a fast sub-exponential time randomized
algorithm for
q
p
2
solving MPGs, whose time complexity can be bounded as O(|V | |E| exp(2 |V | ln(|E|/ |V |) +
p
O( |V | + ln |E|))). Furthermore, Lifshits and Pavlov [9] devised an O(2|V | |V | |E| logW ) singlyexponential time deterministic procedure by considering the potential theory of MPGs.
These results are summarized in Table 1.
Table 1: Complexity of the main Algorithms for solving MPGs.

Algorithm

Value Problem

Optimal
Strategy
Synthesis

Note

This work

O(|V |2 |E|W )

O(|V |2 |E|W )

Determ.

[3]

O(|V |2 |E|W

[11]
[9]
[1]

log(|V |W ))

Θ(|V |3 |E|W )

log(|V |W ))

Θ(|V |4 |E|W

O(2|V | |V | |E| logW )
r
 √
|E|
2 |V | ln √
+O( |V |+ln |E|) 


O |V |2 |E| e

O(|V |2 |E|W

|V |

log

|E|
|V | )

Determ.
Determ.

n/a

Determ.

same complexity

Random.

Contribution. The main contribution of this work is that to provide an O(|V |2 |E|W ) pseudopolynomial time and O(|V |) space deterministic algorithm for solving the Value Problem and Op2

timal Strategy Synthesis in MPGs. As already mentioned in the introduction, the best previously
known procedure has a deterministic time complexity of O(|V |2 |E|W log(|V |W )), which is due to
Brim, et al. [3]. In this way we improve the best previously known pseudo-polynomial time upper
bound by a factor log(|V |W ). This result is summarized in the following theorem.
Theorem 1. There exists a deterministic algorithm for solving the Value Problem and Optimal
Strategy Synthesis of MPGs within O(|V |2 |E|W ) time and O(|V |) space, on any input MPG Γ =
(V, E, w, hV0 ,V1 i). Here, W = maxe∈E |we |.
In order to prove Theorem 1, this work points out a novel and suitable characterization of
values, and a description of optimal positional strategies, in terms of certain reweighting operations
that we will introduce later on in Section 2.
In particular, we will show that the optimal value valΓ (v) of any vertex v is the unique rational
number ν for which v “transits” from the winning region of Player 0 to that of Player 1, with
respect to reweightings of the form w − ν. This intuition will be clarified later on in Section 3,
where Theorem 3 is formally proved.
Concerning strategies, we will show that an optimal positional strategy for each vertex v ∈ V0
is given by any arc (v, v0 ) ∈ E which is compatible with certain Small Energy-Progress Measures
(SEPMs) of the above mentioned reweighted arenas. This fact is formally proved in Theorem 4 of
Section 3.
These novel observations are smooth, simple, and their proofs rely on elementary arguments.
We believe that they contribute to clarifying the interesting relationship between values, optimal
strategies and reweighting operations (with respect to some previous literature, see e.g. [3, 9]).
Indeed, they will allow us to prove Theorem 1.
Organization. This manuscript is organized as follows. In Section 2, we introduce some notation
and provide the required background on infinite two-player games and related algorithmic results.
In Section 3, a suitable relation between values, optimal strategies, and certain reweighting operations is investigated. In Section 4, an O(|V |2 |E|W ) pseudo-polynomial time and O(|V |) space
algorithm, for solving the Value Problem and Optimal Strategies Synthesis in MPGs, is designed
and analyzed by relying on the results presented in Section 3. In this manner, Section 4 actually
provides a proof of Theorem 1 which is our main result in this work.

2

Notation and Preliminaries

We denote by N, Z, Q the set of natural, integer, and rational numbers (respectively). It will be
sufficient to consider integral intervals, e.g., [a, b] := {z ∈ Z | a ≤ z ≤ b} and [a, b) := {z ∈ Z | a ≤
z < b} for any a, b ∈ Z.
Weighted Graphs. Our graphs are directed and weighted on the arcs. Thus, if G = (V, E, w) is a
graph, then every arc e ∈ E is a triplet e = (u, v, we ), where we = w(u, v) ∈ Z is the weight of e. The
maximum absolute weight is W := maxe∈E |we |. Given a vertex u ∈ V , the set of its successors is
post(u) = {v ∈ V | (u, v) ∈ E}, whereas the set of its predecessors is pre(u) = {v ∈ V | (v, u) ∈ E}.
A path is a sequence of vertices v0 v1 . . . vn . . . such that (vi , vi+1 ) ∈ E for every i. We denote by V ∗
the set of all (possibly empty) finite paths. A simple path is a finite path v0 v1 . . . vn having no
repetitions, i.e., for any i, j ∈ [0, n] it holds vi 6= v j whenever i 6= j. The length of a simple path
ρ = v0 v1 . . . vn equals n and it is denoted by |ρ|. A cycle is a path v0 v1 . . . vn−1 vn such that v0 . . . vn−1
3

is simple and vn = v0 . The length of a cycle C = v0 v1 . . . vn equals n and it is denoted by |C|. The
average weight of a cycle v0 . . . vn is 1n ∑n−1
i=0 w(vi , vi+1 ). A cycle C = v0 v1 . . . vn is reachable from v
in G if there exists a simple path p = vu1 . . . um in G such that p ∩C 6= 0.
/
Arenas. An arena is a tuple Γ = (V, E, w, hV0 ,V1 i) where GΓ := (V, E, w) is a finite weighted
directed graph and (V0 ,V1 ) is a partition of V into the set V0 of vertices owned by Player 0, and the
set V1 of vertices owned by Player 1. It is assumed that GΓ has no sink, i.e., post(v) 6= 0/ for every
v ∈ V ; still, we remark that GΓ is not required to be a bipartite graph on colour classes V0 and V1 .
Fig. 1 depicts an example.
−1
A

+2

+2

−1 −9
D

−1

B

+1

−2

C

+1
Figure 1: An arena Γ.
A game on Γ is played for infinitely many rounds by two players moving a pebble along the
arcs of GΓ . At the beginning of the game we find the pebble on some vertex vs ∈ V , which is called
the starting position of the game. At each turn, assuming the pebble is currently on a vertex v ∈ Vi
(for i = 0, 1), Player i chooses an arc (v, v0 ) ∈ E and then the next turn starts with the pebble on v0 .
A play is any infinite path v0 v1 . . . vn . . . ∈ V ∗ in Γ. For any i ∈ {0, 1}, a strategy of Player i
is any function σi : V ∗ × Vi → V such that for every finite path p0 v in GΓ , where p0 ∈ V ∗ and
v ∈ Vi , it holds that (v, σi (p0 , v)) ∈ E. A strategy σi of Player i is positional (or memoryless) if
σi (p, vn ) = σi (p0 , v0m ) for every finite paths pvn = v0 . . . vn−1 vn and p0 v0m = v00 . . . v0m−1 v0m in GΓ such
that vn = v0m ∈ Vi . The set of all the positional strategies of Player i is denoted by ΣM
i . A play
v0 v1 . . . vn . . . is consistent with a strategy σ ∈ Σi if v j+1 = σ (v0 v1 . . . v j ) whenever v j ∈ Vi .
Given a starting position vs ∈ V , the outcome of strategies σ0 ∈ Σ0 and σ1 ∈ Σ1 , denoted
outcomeΓ (vs , σ0 , σ1 ), is the unique play that starts at vs and is consistent with both σ0 and σ1 .
Γ
Given a memoryless strategy σi ∈ ΣM
i of Player i in Γ, then Gσi = (V, Eσi , w) is the graph
obtained from GΓ by removing all the arcs (v, v0 ) ∈ E such that v ∈ Vi and v0 6= σi (v); we say that
GΓσi is obtained from GΓ by projection w.r.t. σi .
Concluding this subsection, the notion of reweighting is recalled. For any weight function
0
w, w0 : E → Z, the reweighting of Γ = (V, E, w, hV0 ,V1 i) w.r.t. w0 is the arena Γw = (V, E, w0 , hV0 ,V1 i).
Also, for w : E → Z and any ν ∈ Z, we denote by w + ν the weight function w0 defined as
w0e := we + ν for every e ∈ E. Indeed, we shall consider reweighted games of the form Γw−q ,
for some q ∈ Q. Notice that the corresponding weight function w0 : E → Q : e 7→ we − q is rational,
while we required the weights of the arcs to be always integers. To overcome this issue, it is sufficient to re-define Γw−q by scaling all the weights by a factor equal to the denominator of q ∈ Q,
namely, to re-define: Γw−q := ΓD·w−N , where N, D ∈ N are such that q = N/D and gcd(N, D) = 1.
This re-scaling will not change the winning regions of the corresponding games, and it has the
significant advantage of allowing for a discussion (and an algorithmics) which is strictly based on
integer weights.

4

Mean Payoff Games. A Mean Payoff Game (MPG) [3, 5, 11] is a game played on some arena
Γ for infinitely many rounds by two opponents, Player 0 gains a payoff defined as the long-run
average weight of the play, whereas Player 1 loses that value. Formally, the Player 0’s payoff of a
play v0 v1 . . . vn . . . in Γ is defined as follows:
MP0 (v0 v1 . . . vn . . .) := lim inf
n→∞

1 n−1
∑ w(vi , vi+1 ).
n i=0

The value secured by a strategy σ0 ∈ Σ0 in a vertex v is defined as:

valσ0 (v) := inf MP0 outcomeΓ (v, σ0 , σ1 ) ,
σ1 ∈Σ1

Notice that payoffs and secured values can be defined symmetrically for the Player 1 (i.e., by
interchanging the symbol 0 with 1 and inf with sup).
Ehrenfeucht and Mycielski [5] proved that each vertex v ∈ V admits a unique value, denoted
valΓ (v), which each player can secure by means of a memoryless (or positional) strategy. Moreover, uniform positional optimal strategies do exist for both players, in the sense that for each player
there exist at least one positional strategy which can be used to secure all the optimal values, independently with respect to the starting position vs . Thus, for every MPG Γ, there exists a strategy
σ0
Γ
M
σ0 ∈ ΣM
0 such that val (v) ≥ val (v) for every v ∈ V , and there exists a strategy σ1 ∈ Σ1 such
σ
Γ
1
that val (v) ≤ val (v) for every v ∈ V . Indeed, the (optimal) value of a vertex v ∈ V in the MPG
Γ is given by:
valΓ (v) = sup valσ0 (v) = inf valσ1 (v).
σ1 ∈Σ1

σ0 ∈Σ0

Thus, a strategy σ0 ∈ Σ0 is optimal if
for all v ∈ V . A strategy σ0 ∈ Σ0 is said
to be winning for Player 0 if valσ0 (v) ≥ 0, and σ1 ∈ Σ1 is winning for Player 1 if valσ1 (v) < 0.
Correspondingly, a vertex v ∈ V is a winning starting position for Player 0 if valΓ (v) ≥ 0, otherwise
it is winning for Player 1. The set of all winning starting positions of Player i is denoted by Wi for
i ∈ {0, 1}.
valσ0 (v) = valΓ (v)

start
A

+2

−1
+2

−1 −9
D

−1
+1

B

+1
C

A

−2 +2

−1
+2

−1 −9
D

−1
+1

A

B

+1

−2 +2

−1 −9
D

C

−1
+2

−1
+1

B

+1
C

A

−2 +2

−1
+2

−1 −9
D

Figure 2: An MPG on Γ, played from left to right, whose payoff equals

+1

−1
+1

−1+1
2

B

−2

C

= 0.

A finite variant of MPGs is well-known in the literature [3, 5, 11]. Here, the game stops as
soon as a cyclic sequence of vertices is traversed (i.e., as soon as one of the two players moves
the pebble into a previously visited vertex). It turns out that this finite variant is equivalent to the
infinite one [5]. Specifically, the values of an MPG are in relationship with the average weights of
its cycles, as stated in the next lemma.
Lemma 1 (Brim, et al. [3]). Let Γ = (V, E, w, hV0 ,V1 i) be an MPG. For all ν ∈ Q, for all positional
σ0
strategies σ0 ∈ ΣM
0 of Player 0, and for all vertices v ∈ V , the value val (v) is greater than ν if
Γ
and only if all cycles C reachable from v in the projection graph Gσ0 have an average weight
w(C)/|C| greater than ν.
5

The proof of Lemma 1 follows from the memoryless determinacy of MPGs. We remark that
a proposition which is symmetric to Lemma 1 holds for Player 1 as well: for all ν ∈ Q, for all
σ1
positional strategies σ1 ∈ ΣM
1 of Player 1, and for all vertices v ∈ V , the value val (v) is less than
Γ
ν if and only if all cycles reachable from v in the projection graph Gσ1 have an average weight less
than ν.
Also, it is well-known [3, 5] that each value valΓ (v) is contained within the following set of
rational numbers:


N
D ∈ [1, |V |], N ∈ [−DW, DW ] .
SΓ =
D
Notice that |SΓ | ≤ |V |2W .
The present work tackles on the algorithmics of the following two classical problems:
• Value Problem. Compute for each vertex v ∈ V the (rational) optimal value valΓ (v).
• Optimal Strategy Synthesis. Compute an optimal positional strategy σ0 ∈ ΣM
0 .
Currently, the asymptotically fastest pseudo-polynomial time algorithm for solving both problems is a deterministic procedure whose time complexity is O(|V |2 |E|W log(|V |W )) [3]. This
result has been achieved by devising a binary-search procedure that ultimately reduces the Value
Problem and Optimal Strategy Synthesis to the resolution of yet another family of games known as
the Energy Games. Even though we do not rely on binary-search in the present work, and thus we
will introduce some truly novel ideas that diverge from the previous solutions, still, we will reduce
to solving multiple instances of Energy Games. For this reason, the Energy Games are recalled in
the next paragraph.
Energy Games and Small Energy-Progress Measures. An Energy Game (EG) is a game that
is played on an arena Γ for infinitely many rounds by two opponents, where the goal of Player 0 is
to construct an infinite play v0 v1 . . . vn . . . such that for some initial credit c ∈ N the following holds:
j

c + ∑ w(vi , vi+1 ) ≥ 0 , for all j ≥ 0.

(1)

i=0

Given a credit c ∈ N, a play v0 v1 . . . vn . . . is winning for Player 0 if it satisfies (1), otherwise
it is winning for Player 1. A vertex v ∈ V is a winning starting position for Player 0 if there
exists an initial credit c ∈ N and a strategy σ0 ∈ Σ0 such that, for every strategy σ1 ∈ Σ1 , the play
outcomeΓ (v, σ0 , σ1 ) is winning for Player 0. As in the case of MPGs, the EGs are memoryless
determined [3], i.e., for every v ∈ V , either v is winning for Player 0 or v is winning for Player 1,
and (uniform) memoryless strategies are sufficient to win the game. In fact, as shown in the next
lemma, the decision problems of MPGs and EGs are intimately related.
Lemma 2 (Brim, et al. [3]). Let Γ = (V, E, w, hV0 ,V1 i) be an arena. For all threshold ν ∈ Q, for
all vertices v ∈ V , Player 0 has a strategy in the MPG Γ that secures value at least ν from v if and
only if, for some initial credit c ∈ N, Player 0 has a winning strategy from v in the reweighted EG
Γw−ν .
In this work we are especially interested in the Minimum Credit Problem (MCP) for EGs: for
each winning starting position v, compute the minimum initial credit c∗ = c∗ (v) such that there
exists a winning strategy σ0 ∈ ΣM
0 for Player 0 starting from v. A fast pseudo-polynomial time
deterministic procedure for solving MCPs comes from [3].
6

Theorem 2 (Brim, et al. [3]). There exists a deterministic algorithm for solving the MCP within
O(|V | |E|W ) pseudo-polynomial time, on any input EG (V, E, w, hV0 ,V1 i).
The algorithm mentioned in Theorem 2 is the Value-Iteration algorithm analyzed by Brim, et
al. in [3]. Its rationale relies on the notion of Small Energy-Progress Measures (SEPMs). These are
bounded, non-negative and integer-valued functions that impose local conditions to ensure global
properties on the arena, in particular, witnessing that Player 0 has a way to enforce conservativity
(i.e., non-negativity of cycles) in the resulting game’s graph. Recovering standard notation, see
e.g. [3], let us denote CΓ = {n ∈ N | n ≤ |V |W } ∪ {>} and let  be the total order on CΓ defined
as x  y if and only if either y = > or x, y ∈ N and x ≤ y.
In order to cast the minus operation to range over CΓ , let us consider an operator : CΓ × Z →
CΓ defined as follows:

max(0, a − b) , if a 6= > and a − b ≤ |V |W ;
a b :=
a b=>
, otherwise.
Given an EG Γ on vertex set V = V0 ∪ V1 , a function f : V → CΓ is a Small Energy-Progress
Measure (SEPM) for Γ if and only if the following two conditions are met:
1. if v ∈ V0 , then f (v)  f (v0 )

w(v, v0 ) for some (v, v0 ) ∈ E;

2. if v ∈ V1 , then f (v)  f (v0 )

w(v, v0 ) for all (v, v0 ) ∈ E.

The values of a SEPM, i.e., the elements of the image f (V ), are called the energy levels of f .
It is worth to denote by V f = {v ∈ V | f (v) 6= >} the set of vertices having finite energy. Given a
SEPM f and a vertex v ∈ V0 , an arc (v, v0 ) ∈ E is said to be compatible with f whenever f (v) 
f (v0 ) w(v, v0 ); moreover, a positional strategy σ0f ∈ ΣM
0 is said to be compatible with f whenever
f
0
0
for all v ∈ V0 , if σ0 (v) = v then (v, v ) ∈ E is compatible with f . Notice that, as mentioned in [3], if
f and g are SEPMs, then so is the minimum function defined as: h(v) = min{ f (v), g(v)} for every
v ∈ V . This fact allows one to consider the least SEPM, namely, the unique SEPM f ∗ : V → CΓ
such that, for any other SEPM g : V → CΓ , the following holds: f ∗ (v)  g(v) for every v ∈ V . Also
concerning SEPMs, we shall rely on the following lemmata. The first one relates SEPMs to the
winning region W0 of Player 0 in EGs.
Lemma 3 (Brim, et al. [3]). Let Γ = (V, E, w, hV0 ,V1 i) be an EG.
1. If f is any SEPM of the EG Γ and v ∈ V f , then v is a winning starting position for Player 0
in the EG Γ. Stated otherwise, V f ⊆ W0 ;
2. If f ∗ is the least SEPM of the EG Γ, and v is a winning starting position for Player 0 in the
EG Γ, then v ∈ V f ∗ . Thus, V f ∗ = W0 .
Also notice that the following bound holds on the energy levels of any SEPM (actually by
definition of CΓ ).
Lemma 4. Let Γ = (V, E, w, hV0 ,V1 i) be an EG. Let f be any SEPM of Γ. Then, for every v ∈ V
either f (v) = > or 0 ≤ f (v) ≤ |V |W .

7

Value-Iteration Algorithm. The algorithm devised by Brim, et al. for solving the MCP in EGs
is known as Value-Iteration [3]. Given an EG Γ as input, the Value-Iteration aims to compute the
least SEPM f ∗ of Γ. This simple procedure basically relies on a lifting operator δ . Given v ∈ V ,
the lifting operator δ (·, v) : [V → CΓ ] → [V → CΓ ] is defined by δ ( f , v) = g, where:

if u 6= v
 f (u)
min{ f (v0 ) w(v, v0 ) | v0 ∈ post(v)} if u = v ∈ V0
g(u) =

max{ f (v0 ) w(v, v0 ) | v0 ∈ post(v)} if u = v ∈ V1
We also need the following definition. Given a function f : V → CΓ , we say that f is inconsistent in v whenever one of the following two holds:
1. v ∈ V0 and for all v0 ∈ post(v) it holds f (v) ≺ f (v0 )

w(v, v0 );

2. v ∈ V1 and there exists v0 ∈ post(v) such that f (v) ≺ f (v0 )

w(v, v0 ).

To start with, the Value-Iteration algorithm initializes f to the constant zero function, i.e.,
f (v) = 0 for every v ∈ V . Furthermore, the procedure maintains a list L of vertices in order to
witness the inconsistencies of f . Initially, v ∈ V0 ∩ L if and only if all arcs going out of v are
negative, while v ∈ V1 ∩ L if and only if v is the source of at least one negative arc. Notice that
checking the above conditions takes time O(|E|).
As long as the list L is nonempty, the algorithm picks a vertex v from L and performs the
following:
1. Apply the lifting operator δ ( f , v) to f in order to resolve the inconsistency of f in v;
2. Insert into L all vertices u ∈ pre(v) \ L witnessing a new inconsistency due to the increase of
f (v).
(The same vertex can’t occur twice in L, i.e., there are no duplicate vertices in L.)
The algorithm terminates when L is empty. This concludes the description of the Value-Iteration
algorithm.
As shown in [3], the update of L following an application of the lifting operator δ ( f , v) requires
O(|pre(v)|) time. Moreover, a single application of the lifting operator δ (·, v) takes O(|post(v)|)
time at most. This implies that the algorithm can be implemented so that it will always halt within
O(|V | |E|W ) time (the reader is referred to [3] in order to grasp all the details of the proof of
correctness and complexity).
Remark. The Value-Iteration procedure lends itself to the following basic generalization, which
turns out to be of a pivotal importance in order to best suit our technical needs. Let f ∗ be the least
SEPM of the EG Γ. Recall that, as a first step, the Value-Iteration algorithm initializes f to be
the constant zero function. Here, we remark that it is not necessary to do that really. Indeed, it is
sufficient to initialize f to be any function f0 which bounds f ∗ from below, that is to say, to initialize
f to any f0 : V → CΓ such that f0 (v)  f ∗ (v) for every v ∈ V . Soon after, L can be initialized in a
natural way: just insert v into L if and only if f0 is inconsistent at v. This initialization still requires
O(|E|) time and it doesn’t affect the correctness of the procedure.
So, we shall assume to have at our disposal a procedure named Value-Iteration(), which
takes as input an EG Γ = (V, E, w, hV0 ,V1 i) and an initial function f0 that bounds from below the
least SEPM f ∗ of the EG Γ (i.e., s.t. f0 (v)  f ∗ (v) for every v ∈ V ). Then, Value-Iteration()
outputs the least SEPM f ∗ of the EG Γ within O(|V | |E|W ) time and working with O(|V |) space.
8

3

Values and Optimal Positional Strategies from Reweightings

This section aims to show that values and optimal positional strategies of MPGs admit a suitable
description in terms of reweighted arenas. This fact will be the crux for solving the Value Problem
and Optimal Strategy Synthesis in O(|V |2 |E|W ) time.

3.1

On optimal values

A simple representation of values in terms of Farey sequences is now observed, then, a characterization of values in terms of reweighted arenas is provided.
Optimal values and Farey sequences. Recall that each value valΓ (v) is contained within the
following set of rational numbers:


N
D ∈ [1, |V |], N ∈ [−DW, DW ] .
SΓ =
D
Let us introduce some notation in order to handle SΓ in a way that is suitable for our purposes.
Firstly, we write every ν ∈ SΓ as ν = i + F, where i = iν = bνc is the integral and F = Fν = {ν} =
ν − i is the fractional part. Notice that i ∈ [−W,W ] and that F is a non-negative rational number
having denominator at most |V |.
As a consequence, it is worthwhile to consider the Farey sequence Fn of order n = |V |. This is
the increasing sequence of all irreducible fractions from the (rational) interval [0, 1] with denominators less than or equal to n. In the rest of this paper, Fn denotes the following sorted set:


N
Fn =
0 ≤ N ≤ D ≤ n, gcd(N, D) = 1 .
D
Farey sequences have numerous and interesting properties, in particular, many algorithms for
generating the entire sequence Fn in time O(n2 ) are known in the literature [6], and these rely on
Stern-Brocot trees and mediant properties. Notice that the above mentioned quadratic running time
2
is optimal, as it is well-known that the sequence Fn has s(n) = 3πn2 + O(n ln n) = Θ(n2 ) terms.
Throughout the article, we shall assume that F0 , . . . , Fs−1 is an increasing ordering of Fn , so
that Fn = {Fj }s−1
j=0 and Fj < Fj+1 for every j.
Also notice that F0 = 0 and Fs−1 = 1.
For example, F5 = {0, 51 , 14 , 31 , 25 , 21 , 35 , 32 , 34 , 54 , 1}.
At this point, SΓ can be represented as follows:

SΓ = [−W,W ) + F|V | = i + Fj i ∈ [−W,W ), j ∈ [0, s − 1] .
The above representation of SΓ will be convenient in a while.
Optimal values and reweightings. Two introductory lemmata are shown below, then, a characterization of optimal values in terms of reweightings is provided.
Lemma 5. Let Γ = (V, E, w, hV0 ,V1 i) be an MPG and let q ∈ Q be a rational number having
w+q
denominator D ∈ N. Then, valΓ (v) = D1 valΓ (v) − q holds for every v ∈ V .

9

w+q

Proof. Let us consider the play outcomeΓ (v, σ0 , σ1 ) = v0 v1 . . . vn . . . By the definition of valΓ (v),
and by that of reweighting Γw+q (= ΓD·w+N ), the following holds:
valΓ

w+q

w+q

(v) = supσ0 ∈Σ0 infσ1 ∈Σ1 MP0 (outcomeΓ

(v, σ0 , σ1 ))

= supσ0 ∈Σ0 infσ1 ∈Σ1 lim infn→∞ n1 ∑n−1
i=0 (D · w(vi , vi+1 ) + N) (if q = N/D)
= D · supσ0 ∈Σ0 infσ1 ∈Σ1 MP0 (outcomeΓ (v, σ0 , σ1 )) + N
= D · valΓ (v) + N.
w+q

Then, valΓ (v) = D1 valΓ

w+q

(v) − ND = D1 valΓ

(v) − q holds for every v ∈ V .
2

Lemma 6. Given an MPG Γ = (V, E, w, hV0 ,V1 i), let us consider the reweightings:
Γi, j = Γw−i−Fj , for any i ∈ [−W,W ] and j ∈ [0, s − 1],
where s = |F|V | | and Fj is the j-th term of the Farey sequence F|V | .
Then, the following propositions hold:
1. For any i ∈ [−W,W ] and j ∈ [0, s − 1], we have:
v ∈ W0 (Γi, j ) if and only if valΓ (v) ≥ i + Fj ;
2. For any i ∈ [−W,W ] and j ∈ [1, s − 1], we have:
v ∈ W1 (Γi, j ) if and only if valΓ (v) ≤ i + Fj−1 .
Proof.
1. Let us fix arbitrarily some i ∈ [−W,W ] and j ∈ [0, s − 1].
Assume that Fj = N j /D j for some N j , D j ∈ N.
Since
Γi, j = (V, E, D j (w − i) − N j , hV0 ,V1 i),
then by Lemma 5 (applyed to q = −i − Fj ) we have:
valΓ (v) =

1
valΓi, j (v) + i + Fj .
Dj

Recall that v ∈ W0 (Γi, j ) if and only if valΓi, j (v) ≥ 0.
Hence, we have v ∈ W0 (Γi, j ) if and only if the following inequality holds:
valΓ (v) =

1
valΓi, j (v) + i + Fj
Dj

≥ i + Fj .
This proves Item 1.
10

2. The argument is symmetric to that of Item 1, but with some further observations.
Let us fix arbitrarily some i ∈ [−W,W ] and j ∈ [1, s − 1]. Assume that Fj = N j /D j for
some N j , D j ∈ N. Since Γi, j = (V, E, D j (w − i) − N j , hV0 ,V1 i), then by Lemma 5 we have
valΓ (v) = D1j valΓi, j (v) + i + Fj . Recall that v ∈ W1 (Γi, j ) if and only if valΓi, j (v) < 0.
Hence, we have v ∈ W1 (Γi, j ) if and only if the following inequality holds:
valΓ (v) =

1
valΓi, j (v) + i + Fj
Dj

< i + Fj .
Now, recall from Section 2 that valΓ (v) ∈ SΓ , where
SΓ = {i + Fj | i ∈ [−W,W ), j ∈ [0, s − 1]}.
By hypothesis we have:
j ≥ 1 and 0 ≤ Fj−1 < Fj ,
thus, at this point, v ∈ W1 (Γi, j ) if and only if valΓ (v) ≤ i + Fj−1 .
This proves Item 2.
2
We are now in the position to provide a simple characterization of values in terms of reweightings.
Theorem 3. Given an MPG Γ = (V, E, w, hV0 ,V1 i), let us consider the reweightings:
Γi, j = Γw−i−Fj , for any i ∈ [−W,W ] and j ∈ [1, s − 1],
where s = |F|V | | and Fj is the j-th term of the Farey sequence F|V | .
Then, the following holds:
valΓ (v) = i + Fj−1 if and only if v ∈ W0 (Γi, j−1 ) ∩ W1 (Γi, j ).
Proof. Let us fix arbitrarily some i ∈ [−W,W ] and j ∈ [1, s − 1].
By Item 1 of Lemma 6, we have v ∈ W0 (Γi, j−1 ) if and only if valΓ (v) ≥ i + Fj−1 . Symmetrically, by Item 2 of Lemma 6, we have v ∈ W1 (Γi, j ) if and only if valΓ (v) ≤ i + Fj−1 . Whence, by
composition, v ∈ W0 (Γi, j−1 ) ∩ W1 (Γi, j ) if and only if valΓ (v) = i + Fj−1 .
2

3.2

On optimal positional strategies

The present subsections aims to provide a suitable description of optimal positional strategies in
terms of reweighted arenas. An introductory lemma is shown next.
Lemma 7. Let Γ = (V, E, w, hV0 ,V1 i) be an MPG, the following hold:
1. If v ∈ V0 , let v0 ∈ post(v). Then valΓ (v0 ) ≤ valΓ (v) holds.

11

2. If v ∈ V1 , let v0 ∈ post(v). Then valΓ (v0 ) ≥ valΓ (v) holds.
Γ (v)

3. Given any v ∈ V0 , consider the reweighted EG Γv = Γw−val

.

Let fv : V → CΓv be any SEPM of the EG Γv such that v ∈ V fv (i.e., fv (v) 6= >). Let v0fv ∈ V
be any vertex out of v such that (v, v0fv ) ∈ E is compatible with fv in Γv .
Then, valΓ (v0fv ) = valΓ (v).
Proof.

1. It is sufficient to construct a strategy σ0v ∈ ΣM
0 securing to Player 0 a payoff at least
0
Γ
0
v
M
val (v ) from v in the MPG Γ. Let σ0 ∈ Σ0 be a strategy securing payoff at least valΓ (v0 )
from v0 in Γ. Then, let σ0v be defined as follows:

0

σ v (u) , if u ∈ V0 \ {v};

 0v0
σ0 (v) , if u = v and v is reachable from v0 in GΓ v0 ;
σ0v (u) =
σ0


 v0
, if u = v and v is not reachable from v0 in GΓ 0 .
σ0v

We argue that σ0v secures payoff at least valΓ (v0 ) from v in Γ. First notice that, by Lemma 1
(applied to v0 ), all cycles C that are reachable from v0 in Γ satisfy:
w(C)
≥ valΓ (v0 ).
|C|
The fact is that any cycle reachable from v in GΓσ v is also reachable from v0 in GΓ v0 (by
0

σ0

definition of σ0v ), therefore, the same inequality holds for all cycles reachable from v. At
this point, the thesis follows again by Lemma 1 (applied to v, in the inverse direction). This
proves Item 1.
2. The proof of Item 2 is symmetric to that of Item 1.
3. Firstly, notice that valΓ (v0fv ) ≤ valΓ (v) holds by Item 1. To conclude the proof it is sufficient to show valΓ (v0fv ) ≥ valΓ (v). Recall that (v, v0fv ) ∈ E is compatible with fv in Γv by
hypothesis, that is:

fv (v)  fv (v0fv )
w(v, v0fv ) − valΓ (v) .
This, together with the fact that v ∈ V fv (i.e., fv (v) 6= >) also holds by hypothesis, implies that
v0fv ∈ V f (i.e., fv (v0fv ) 6= >). Thus, by Item 1 of Lemma 3, v0fv is a winning starting position
of Player 0 in the EG Γv . Whence, by Lemma 2, it holds that valΓ (v0fv ) ≥ valΓ (v). This
proves Item 3.
2
We are now in position to provide a sufficient condition, for a positional strategy to be optimal,
which is expressed in terms of reweighted EGs and their SEPMs.
Theorem 4. Let Γ = (V, E, w, hV0 ,V1 i) be an MPG. For each v ∈ V , consider the reweighted EG
Γ
Γv = Γw−val (v) . Let fv : V → CΓv be any SEPM of Γv such that v ∈ V fv (i.e., fv (v) 6= >). Moreover,
assume: fv1 = fv2 whenever valΓ (v1 ) = valΓ (v2 ).

12

When v ∈ V0 , let v0fv ∈ V be any vertex such that (v, v0fv ) ∈ E is compatible with fv in the EG Γv ,
and consider the positional strategy σ0∗ ∈ ΣM
0 defined as follows:
σ0∗ (v) = v0fv for every v ∈ V0 .
Then, σ0∗ is an optimal positional strategy for Player 0 in the MPG Γ.
Proof. Let us consider the projection graph GΓσ ∗ = (V, Eσ0∗ , w). Let v ∈ V be any vertex. In order to
0
prove that σ0∗ is optimal, it is sufficient (by Lemma 1) to show that every cycle C that is reachable
Γ
from v in GΓσ ∗ satisfies w(C)
|C| ≥ val (v).
0

• Preliminaries. Let v ∈ V and let C be any cycle of length |C| ≥ 1 that is reachable from v
in GΓσ ∗ . Then, there exists a path ρ of length |ρ| ≥ 1 in GΓσ ∗ and such that: if |ρ| = 1, then
0
0
ρ = ρ0 ρ1 = vv; otherwise, if |ρ| > 1, then:
ρ = ρ0 . . . ρ|ρ| = vv1 v2 . . . vk u1 u2 . . . u|C| u1 ,
where vv1 . . . vk is a simple path, for some k ≥ 0 and u1 . . . u|C| u1 = C.
u|C|
u4
u1

v
v1

C

vk
u3

GΓσ ∗
0

u2

Figure 3: A cycle C that is reachable from v through v1 · · · vk in GΓσ ∗ .
0

• Fact 1. It holds valΓ (ρi ) ≤ valΓ (ρi+1 ) for every i ∈ [0, |ρ|).
of Fact 1. If ρi ∈ V0 then valΓ (ρi ) = valΓ (ρi+1 ) by Item 3 of Lemma 7; otherwise, if
ρi ∈ V1 , then valΓ (ρi ) ≤ valΓ (ρi+1 ) by Item 2 of Lemma 7. This proves Fact 1. In particular, notice that valΓ (v) ≤ valΓ (u1 ) when |ρ| > 1.
2
• Fact 2. Assume C = u1 . . . u|C| u1 , then valΓ (ui ) = valΓ (u1 ) for every i ∈ [0, |C|].
of Fact 2. By Fact 1, valΓ (ui−1 ) ≤ valΓ (ui ) for every i ∈ [2, |C|], as well as valΓ (u|C| ) ≤
valΓ (u1 ). Then, the following chain of inequalities holds:
valΓ (u1 ) ≤ valΓ (u2 ) ≤ . . . ≤ valΓ (u|C| ) ≤ valΓ (u1 ).
Since the first and the last value of the chain are actually the same, i.e., valΓ (u1 ), then, all
these inequalities are indeed equalities. This proves Fact 2.
2

13

• Fact 3. The following holds for every i ∈ [0, |ρ|):
fρi (ρi ), fρi (ρi+1 ) 6= > and fρi (ρi ) ≥ fρi (ρi+1 ) − w(ρi , ρi+1 ) + valΓ (ρi ).
of Fact 3. Firstly, we argue that any arc (ρi , ρi+1 ) ∈ E is compatible with fρi in Γρi . Indeed,
if ρi ∈ V0 , then (ρi , ρi+1 ) is compatible with fρi in Γρi because ρi+1 = σ0∗ (ρi ) by hypothesis;
otherwise, if ρi ∈ V1 , then (ρi , x) is compatible with fρi in Γρi for every x ∈ post(ρi ), in
particular for x = ρi+1 , by definition of SEPM.
At this point, since (ρi , ρi+1 ) is compatible with fρi in Γρi , then:

w(ρi , ρi+1 ) − valΓ (ρi ) .

fρi (ρi )  fρi (ρi+1 )

Now, recall that ρi ∈ V fρi (i.e., fρi (ρi ) 6= >) holds for every ρi by hypothesis. Since fρi (ρi ) 6=
> and the above inequality holds, then we have fρi (ρi+1 ) 6= >. Thus, we can safely write:
fρi (ρi ) ≥ fρi (ρi+1 ) − w(ρi , ρi+1 ) + valΓ (ρi ).
2

This proves Fact 3.
• Fact 4. Assume that the cycle C = u1 . . . u|C| u1 is such that:
valΓ (ui ) = valΓ (u1 ) ≥ valΓ (v), for every i ∈ [1, |C|].
Then, provided that u|C|+1 = u1 , the following holds for every i ∈ [1, |C|]:
i

fu1 (u1 ), fui+1 (ui+1 ) 6= > and fu1 (u1 ) ≥ fui+1 (ui+1 ) − ∑ w(u j , u j+1 ) + i · valΓ (v).
j=1

of Fact 4. Firstly, notice that fu1 (u1 ), fui+1 (ui+1 ) 6= > holds by hypothesis.
The proof proceeds by induction on i ∈ [1, |C|].
– Base Case. Assume that |C| = 1, so that C = u1 u1 . Then fu1 (u1 ) ≥ fu1 (u1 )−w(u1 , u1 )+
valΓ (u1 ) follows by Fact 3. Since valΓ (u1 ) ≥ valΓ (v) by hypothesis, then the thesis
follows.
– Inductive Step. Assume by induction hypothesis that the following holds:
i−1

fu1 (u1 ) ≥ fui (ui ) − ∑ w(u j , u j+1 ) + (i − 1) · valΓ (v).
j=1

By Fact 3, we have:
fui (ui ) ≥ fui (ui+1 ) − w(ui , ui+1 ) + valΓ (ui ).
Since valΓ (ui+1 ) = valΓ (ui ) holds by hypothesis, then we have fui+1 = fui . Recall
that valΓ (ui ) ≥ valΓ (v) also holds by hypothesis.
Thus, we obtain the following:
i

fu1 (u1 ) ≥ fui+1 (ui+1 ) − ∑ w(u j , u j+1 ) + i · valΓ (v).
j=1

This proves Fact 4.
14

2
• We are now in position to show that every cycle C that is reachable from v in GΓσ ∗ satisfies
0

w(C)/|C| ≥ valΓ (v). By Fact 1 and Fact 2, we have valΓ (v) ≤ valΓ (u1 ) = valΓ (ui ) for
every i ∈ [1, |C|]. At this point, we apply Fact 4. Consider the specialization of Fact 4 when
i = |C| and also recall that u|C|+1 = u1 . Then, we have the following:
|C|

fu1 (u1 ) ≥ fu1 (u1 ) − ∑ w(u j , u j+1 ) + |C| · valΓ (v).
j=1

As a consequence, the following lower bound holds on the average weight of C:
1
w(C)
=
|C|
|C|

|C|

∑ w(u j , u j+1 ) ≥ valΓ (v),

j=1

which concludes the proof.
2
Remark 1. Notice that Theorem 4 holds, in particular, when fv is the least SEPM fv∗ of the
reweighted EG Γv . This follows because v ∈ V fv∗ always holds for the least SEPM fv∗ of the EG
Γv , as shown next: by Lemma 2 and by definition of Γv , then v is a winning starting position for
Player 0 in the EG Γv (for some initial credit); now, since fv∗ is the least SEPM of the EG Γv , then
v ∈ V fv∗ follows by Item 2 of Lemma 3.

4

An O(|V |2 |E|W ) time Algorithm for solving the Value Problem and Optimal Strategy Synthesis in MPGs

This section offers a deterministic algorithm for solving the Value Problem and Optimal Strategy Synthesis of MPGs within O(|V |2 |E|W ) time and O(|V |) space, on any input MPG Γ =
(V, E, w, hV0 ,V1 i).
Let us now recall some notation in order describe the algorithm in a suitable way.
Given an MPG Γ = (V, E, w, hV0 ,V1 i), consider again the following reweightings:
Γi, j = Γw−i−Fj , for any i ∈ [−W,W ] and j ∈ [0, s − 1],
where s = |F|V | | and Fj is the j-th term of F|V | .
Assuming Fj = N j /D j for some N j , D j ∈ N, we focus on the following weights:
wi, j =w − i − Fj = w − i −

Nj
;
Dj

w0i, j =D j wi, j = D j (w − i) − N j .
0

Recall that Γi, j is defined as Γi, j := Γwi, j , which is an arena having integer weights. Also notice
that, since F0 < . . . < Fs−1 is monotone increasing, then the corresponding weight functions wi, j
15

can be ordered in a natural way, i.e., w−W,1 > w−W,2 > . . . > wW −1,s−1 > . . . > wW,s−1 . In the rest
of this section, we denote by fw∗0 : V → CΓi, j the least SEPM of the reweighted EG Γi, j . Moreover,
i, j

the function fi,∗ j : V → Q, defined as fi,∗ j (v) :=
scaling of

4.1

fw∗0 .
i, j

1 ∗
D j f w0i, j (v)

for every v ∈ V , is called the rational

Description of the Algorithm

In this section we shall describe a procedure whose pseudo-code is given below in Algorithm 1.
It takes as input an arena Γ = (V, E, w, hV0 ,V1 i), and it aims to return a tuple (W0 , W1 , ν, σ0∗ ) such
that: W0 and W1 are the winning regions of Player 0 and Player 1 in the MPG Γ (respectively),
ν : V → SΓ is a map sending each starting position v ∈ V to its optimal value, i.e., ν(v) = valΓ (v),
and finally, σ0∗ : V0 → V is an optimal positional strategy for Player 0 in the MPG Γ.
The intuition underlying Algorithm 1 is that of considering the following sequence of weights:
w−W,1 > w−W,2 > . . . > w−W,s−1 > w−W +1,1 > w−W +1,2 > . . . > wW −1,s−1 > . . . > wW,s−1
where the key idea is that to rely on Theorem 3 at each one of these steps, testing whether a
transition of winning regions has occurred. Stated otherwise, the idea is to check, for each vertex
?

v ∈ W0 (Γprev(i, j) ) ∩ W1 (Γi, j )
···

start
w−W,1 w−W,2 w−W,3

· · · wprev(i, j) wi, j

···

wW −1,s−1 wW,1

Figure 4: An illustration of Algorithm 1.
v ∈ V , whether v is winning for Player 1 with respect to the current weight wi, j , meanwhile recalling
whether v was winning for Player 0 with respect to the immediately preceding element wprev(i, j) in
the weight sequence above.
If such a transition occurs, say for some v̂ ∈ W0 (Γprev(i, j) ) ∩ W1 (Γi, j ), then one can easily
compute valΓ (v̂) by relying on Theorem 3; Also, at that point, it is easy to compute an optimal
positional strategy, provided that v̂ ∈ V0 , by relying on Theorem 4 and Remark 1 in that case.
Each one of these phases, in which one looks at transitions of winning regions, is named Scan
Phase. A graphical intuition of Algorithm 1 is given in Fig. 4.

16

An in-depth description of the algorithm and of its pseudo-code now follows.
Algorithm 1: Solving the Value Problem and Strategy Synthesis in MPGs.

1
2
3
4

5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

27

Procedure solve MPG(Γ)
input : an MPG Γ = (V, E, w, hV0 ,V1 i).
output: a tuple (W0 , W1 , ν, σ0∗ ) such that: W0 and W1 are the winning regions of Player 0 and
Player 1 (respectively) in the MPG Γ; ν : V → SΓ is a map sending each starting position
v ∈ V to its corresponding optimal value, i.e., ν(v) = valΓ (v); and σ0∗ : V0 → V is an
optimal positional strategy for Player 0 in the MPG Γ.
// Init Phase
W0 ← 0;
/ W1 ← 0;
/
f (v) ← 0, ∀ v ∈ V ;
W ← maxe∈E |we |; w0 ← w +W ; D ← 1;
s ← compute the size |F|V | | of F|V | ; // with the algorithm of [10]
// Scan Phases
for i = −W to W do
F ← 0;
for j = 1 to s − 1 do
prev f ← f ;
prev w ← D1 w0 ;
prev F ← F;
F ← generate the j-th term of F|V | ; // with the algorithm of [10]
N ← numerator of F;
D ← denominator of F;
w0 ← D (w − i) − N;
0
f ← D1 Value-Iteration(Γw , dD prev f e);
for v ∈ V do
if prev f (v) 6= > and f (v) = > then
ν(v) ← i + prev F; // set optimal value ν
if ν(v) ≥ 0 then
W0 ← W0 ∪ {v}; // v is winning for Player 0
else
W1 ← W1 ∪ {v}; // v is winning for Player 1
if v ∈ V0 then
for u ∈ post(v) do
if prev f (v)  prev f (u)
σ0∗ (v) ← u; break;

prev w(v, u) then

return (W0 , W1 , ν, σ0∗ )

• Initialization Phase. To start with, the algorithm performs an initialization phase. At line 1,
Algorithm 1 initializes the output variables W0 and W1 to be empty sets. Notice that, within
the pseudo-code, the variables W0 and W1 represent the winning regions of Player 0 and
Player 1, respectively; also, the variable ν represents the optimal values of the input MPG Γ,
and σ0∗ represents an optimal positional strategy for Player 0 in the input MPG Γ. Secondly,
at line 2, an array variable f : V → CΓ is initialized to f (v) = 0 for every v ∈ V ; throughout the
computation, the variable f represents a SEPM. Next, at line 3, the greatest absolute weight
W is assigned as W = maxe∈E |we |, an auxiliary weight function w0 is initialized as w0 =
17

w + W , and a “denominator” variable is initialized as D = 1. Concluding the initialization
phase, at line 4 the size (i.e., the total number of terms) of F|V | is computed and assigned
to the variable s. This size can be computed very efficiently with the algorithm devised by
Pawlewicz and Pătraşcu [10].
• Scan Phases. After initialization, the procedure performs multiple Scan Phases. Each one
of these is indexed by a pair of integers (i, j), where i ∈ [−W,W ] (at line 5) and j ∈ [1, s − 1]
(at line 7). Thus, the index i goes from −W to W , and for each i, the index j goes from 1 to
s − 1.
At each step, we say that the algorithm goes through the (i, j)-th scan phase. For each scan
phase, we also need to consider the previous scan phase, so that the previous index prev(i, j)
shall be defined as follows: the predecessor of the first index is prev(−W, 1) := (−W, 0); if
j > 1, then prev(i, j) := (i, j − 1); finally, if j = 1 and i > −W , then prev(i, j) := (i − 1, s −
1).
At the (i, j)-th scan phase, the algorithm considers the rational number zi, j ∈ SΓ defined as:
zi, j := i + F[ j],
where F[ j] = N j /D j is the j-th term of F|V | . For each j, F[ j] can be computed very efficiently, on the fly, with the algorithm of Pawlewicz and Pătraşcu [10]. Notice that, since
F[0] < . . . < F[s − 1] is monotonically increasing, then the values zi, j are scanned in increasing order as well. At this point, the procedure aims to compute the rational scaling fi,∗ j of the
least SEPM fw∗0 , i.e.,
i, j

f := fi,∗ j =

1 ∗
f 0 .
D j wi, j

This computation is really at the heart of the algorithm and it goes from line 8 to line 15. To
∗
start with, at line 8 and line 9, the previous rational scaling fprev
(i, j) and the previous weight
function wprev(i, j) (i.e., those considered during the previous scan phase) are saved into the
auxiliary variables prev f and prev w.
Remark. Since the values zi, j are scanned in increasing order of magnitude, then prev f =
∗
∗
fprev
(i, j) bounds from below f i, j . That is, it holds for every v ∈ V that:
∗
∗
prev f (v) = fprev
(i, j) (v)  f i, j .

The underlying intuition, at this point, is that of computing the energy levels of f = fi,∗ j
firstly by initializing them to the energy levels of the previous scan phase, i.e., to prev f =
∗
fprev
(i, j) , and then to update them monotonically upwards by executing the Value-Iteration
algorithm for EGs.
Further details of this pivotal step now follow. Firstly, since the Value-Iteration has been
designed to work with integer numerical weights only [3], then the weights wi, j = w − zi, j
have to be scaled from Q to Z: this is performed in the standard way, from line 12 to line 15,
by considering the numerator N j and the denominator D j of F[ j], and then by setting:

w0i, j (e) := D j w(e) − i − N j , for every e ∈ E.
The initial energy levels are also scaled up from Q to Z by considering the values: dD j prev f (v)e,
0
for every v ∈ V (line 15). At this point the least SEPM of Γwi, j is computed, at line 15, by
18

0

0

invoking Value-Iteration(Γwi, j , dD j prev f e), that is, by executing on input Γwi, j the
Value-Iteration with initial energy levels given by: dD j prev f (v)e for every v ∈ V . Soon
after that, the energy levels have to be scaled back from Z to Q, so that, in summary, at
line 15 they becomes:
f = fi,∗ j =

0
1
Value-Iteration(Γwi, j , dD j prev f e).
Dj

The correctness of lines 14-15 will be proved in Lemma 8.
Here, let us provide a sketch of the argument:
1. Since F0 < . . . < Fs−1 is monotone increasing, then the sequence {w0i, j }(i, j) is monotone
decreasing, i.e., for every i, j and e ∈ E, w0prev(i, j) (e) > w0i, j (e). Whence, the sequence
∗
of rational scalings { fi,∗ j }i, j is monotone increasing, i.e., fi,∗ j  fprev
(i, j) holds at the
(i, j)-th step. The proof is in Lemma 8.
∗
2. At the (i, j)-th iteration of line 8, it holds that prev f = fprev
(i, j) .
This invariant property is also proved as part of Lemma 8.
∗
∗
3. Since prev f = fprev
(i, j) , then prev f  f i, j .

Thus, one can prove that D j prev f  fw∗0 .
i, j

4. Since w0i, j (e) ∈ Z for every e ∈ E, then fw∗0 (v) ∈ Z for every v ∈ V , so that dD j prev f(v)e 
fw∗0 (v) holds for every v ∈ V as well.

i, j

i, j

0

5. This implies that it is correct to execute the Value-Iteration, on input Γwi, j , with initial
energy levels given by: dD j prev f (v)e for every v ∈ V .
Back to us, once f = fi,∗ j has been determined, then for each v ∈ V the condition:
?

v ∈ W0 (Γprev(i, j) ) ∩ W1 (Γi, j ),
is checked at line 17: it is not difficult to show that, for this, it is sufficient to test whether
both prev f(v) 6= > and f (v) = > hold on v (it follows by Lemma 8).
If v ∈ W0 (Γprev(i, j) ) ∩ W1 (Γi, j ) holds, then the algorithm relies on Theorem 3 in order to
assign the optimal value as follows: ν(v) := valΓ (v) = zprev(i, j) (line 18). If ν(v) ≥ 0, then
v is added to the winning region W0 at line 20. Otherwise, ν(v) < 0 and v is added to W1 at
line 22.
To conclude, from line 23 to line 27, the algorithm proceeds as follows: if v ∈ V0 , then it
computes an optimal positional strategy σ0∗ (v) for Player 0 in Γ: this is done by testing for
each u ∈ post(v) whether (v, u) ∈ E is an arc compatible with prev f in Γprev(i, j) ; namely,
whether the following holds for some u ∈ post(v):
?

prev f (v)  prev f (u)

prev w(v, u).

If (v, u) ∈ E is found to be compatible with prev f at that point, then σ0∗ (v) := u gets assigned and the arc (v, u) becomes part of the optimal positional strategy returned to output.
Indeed, the correctness of such an assignment relies on Theorem 4 and Remark 1.
This concludes the description of the scan phases and also that of Algorithm 1.
19

4.2

Proof of Correctness

Now we formally prove the correctness of Algorithm 1. The following lemma shows some basic
invariants that are maintained throughout the computation.
Lemma 8. Algorithm 1 keeps the following invariants throughout the computation:
1. For every i ∈ [−W,W ] and every j ∈ [1, s − 1], it holds that:
∗
∗
fprev
(i, j) (v)  f i, j (v), for every v ∈ V ;
∗
2. At the (i, j)-th iteration of line 8, it holds that: prev f = fprev
(i, j) ;

3. At the (i, j)-th iteration of line 8, it holds that: dD j prev f e  fw∗0 ;
i, j

4. At the (i, j)-th iteration of line 15, it holds that:
0
1
Value-Iteration(Γwi, j , dD j prev f e) = fi,∗ j .
Dj

Proof.
• Proof (of Item 1). Recall that wi, j := w−i−Fj . Since F0 < . . . < Fs−1 is monotone increasing,
then: wi, j (e) < wprev(i, j) (e) holds for every e ∈ E.
In order to prove the thesis, consider the following function:

∗
∗
g : V → Q ∪ {>} : v 7→ min fprev
(i, j) (v), f i, j (v) .
w0

We show that Dprev(i, j) g is a SEPM of Γ prev(i, j) . There are four cases, according to whether
∗
∗
v ∈ V0 or v ∈ V1 , and g(v) = fprev
(i, j) (v) or g(v) = f i, j (v).
– Case: v ∈ V0 . Then, the following holds for some u ∈ post(v):
∗
∗ Case: g(v) = fprev
(i, j) (v):
∗
Dprev(i, j) g(v) = Dprev(i, j) fprev
(i, j) (v)

= fw∗0

(v)

 fw∗0

(v)

∗
[by g(v) = fprev
(i, j) (v)]
∗
∗
[by Dprev(i, j) fprev
(i, j) = f w0

prev(i, j)

]

prev(i, j)

prev(i, j)

w0prev(i, j) (v, u)

∗
= Dprev(i, j) fprev
(i, j) (u)

 Dprev(i, j) g(u)

is SEPM of Γ

w0prev(i, j)

]

prev(i, j)

w0prev(i, j) (v, u) [by fw∗0

w0prev(i, j) (v, u)

20

[ fw∗0

prev(i, j)

∗
= Dprev(i, j) fprev
(i, j) ]

[by definition of g(u)]

∗ Case: g(v) = fi,∗ j (v):
Dprev(i, j) g(v) = Dprev(i, j) fi,∗ j (v)
Dprev(i, j) ∗
fw0 (v)
=
i, j
Di, j
Dprev(i, j) ∗

fw0 (u)
i, j
Di, j
= Dprev(i, j) fi,∗ j (u)
= Dprev(i, j) fi,∗ j (u)
 Dprev(i, j) fi,∗ j (u)
= Dprev(i, j) fi,∗ j (u)
 Dprev(i, j) g(u)

[by g(v) = fi,∗ j (v)]
[by fi,∗ j = fw∗0 /Di, j ]
i, j

Dprev(i, j) 0
wi, j (v, u)
Di, j
Dprev(i, j) 0
wi, j (v, u)
Di, j

[ fw∗0 is SEPM of Γwi, j ]

Dprev(i, j) wi, j (v, u)

[by wi, j (v, u) = w0i, j (v, u)/Di, j ]

0

i, j

[by fi,∗ j = fw∗0 /Di, j ]
i, j

Dprev(i, j) wprev(i, j) (v, u) [by wi, j < wprev(i, j) ]
w0prev(i, j) (v, u)

[by Dprev(i, j) wprev(i, j) = w0prev(i, j) ]

w0prev(i, j) (v, u)

[by definition of g(u)]

This means that (v, u) is an arc compatible with Dprev(i, j) g in Γ

w0prev(i, j)

.

– Case: v ∈ V1 . The same argument shows that (v, u) ∈ E is compatible with Dprev(i, j) g
in Γ

w0prev(i, j)

, but it holds for all u ∈ post(v) in this case.
w0prev(i, j)

This proves that Dprev(i, j) g is a SEPM of Γ
Since fw∗0

w0prev(i, j)

is the least SEPM of Γ

.

, then:

prev(i, j)

fw∗0

prev(i, j)

Since fw∗0

prev(i, j)

(v)  Dprev(i, j) g(v), for every v ∈ V .

∗
∗
∗
= Dprev(i, j) fprev
(i, j) and g = min( f prev(i, j) , f i, j ), then:
∗
∗
∗
Dprev(i, j) fprev
(i, j)  Dprev(i, j) min( f prev(i, j) , f i, j ).

∗
∗
∗
Whence fprev
(i, j) = min( f prev(i, j) , f i, j ).
∗
∗
This proves that fprev
(i, j) (v)  f i, j (v) holds for every v ∈ V .

• Fact 1. Next, we prove that if Item 2 holds at the (i, j)-th scan phase, then both Item 3 and
Item 4 hold at the (i, j)-th scan phase as well.
∗
∗
of Fact 1. Assume that Item 2 holds. Let us prove Item 3 first. Since fprev
(i, j)  f i, j holds
∗
∗
by Item 1, and since prev f = fprev
(i, j) holds by hypothesis, then prev f (v)  f i, j (v) holds
0
∗
∗
∗
for every v ∈ V . Since wi, j = D j wi, j and fw0 = D j fi, j , then D j prev f(v)  fw0 (v) holds
i, j

i, j

for every v ∈ V . Since w0i, j (e) ∈ Z for every e ∈ E, then fw∗0 (v) ∈ Z for every v ∈ V , so that
i, j

dD j prev f(v)e  fw∗0 (v) holds for every v ∈ V as well. This proves Item 3.
i, j

We show Item 4 now. Since Item 3 holds, at line 15 it is correct to initialize the starting energy
levels of Value-Iteration() to dD j prev f (v)e for every v ∈ V , in order to execute the
0
Value-Iteration on input Γwi, j .
21

This implies the following:
0

Value-Iteration(Γwi, j , dD j prev f e) = fw∗0 .
i, j

We know that

1
Dj

fw∗0 = fi,∗ j .
i, j

This proves that Item 4 holds and concludes the proof of Fact 1.

2

• Fact 2. We now prove that Item 2 holds at each iteration of line 8.
of Fact 2. The proof proceeds by induction on (i, j).
Base Case. Let us consider the first iteration of line 8; i.e., the iteration indexed by i = −W
and j = 1. Recall that, at line 2 of Algorithm 1, the function f is initialized as f (v) = 0 for
∗
every v ∈ V . Notice that f is really the least SEPM f−W,0
of Γ−W,0 = Γw+W , because every
arc e ∈ E has a non-negative weight in Γw+W , i.e., we +W ≥ 0 for every e ∈ E.
Hence, at the first iteration of line 8, the following holds:
∗
∗
= fprev
prev f = 0 = f−W,0
(−W,1) .

Inductive Step. Let us assume that Item 2 holds for the prev(i, j)-th iteration, and let us
prove it for the (i, j)-th one. Hereafter, let us denote (i p , j p ) = prev(i, j) for convenience.
Since Item 2 holds for the (i p , j p )-th iteration by induction hypothesis, then, by Fact 1, the
following holds at the (i p , j p )-th iteration of line 15:
1
w0
Value-Iteration(Γ i p , j p , dD j p prev f e) = f = fi∗p , j p .
D jp
Thus, at the (i, j)-th iteration of line 8:
∗
prev f = f = fi∗p , j p = fprev
(i, j) .

2

This concludes the proof of Fact 2.

At this point, by Fact 1 and Fact 2, Lemma 8 follows.

2

We are now in the position to show that Algorithm 1 is correct.
Proposition 1. Assume that Algorithm 1 is invoked on input Γ = (V, E, w, hV0 ,V1 i) and, whence,
that it returns (W0 , W1 , ν, σ0 ) as output.
Then, W0 and W1 are the winning sets of Player 0 and Player 1 in Γ (respectively), ν : V → S
is such that ν(v) = valΓ (v) for every v ∈ V , and σ0 : V0 → V is an optimal positional strategy for
Player 0 in the MPG Γ.

22

Proof. At the (i, j)-th iteration of line 17, the following holds by Lemma 8:
∗
∗
prev f = fprev
(i, j) and f = f i, j .

Our aim now is that to apply Theorem 3. For this, firstly observe that one can safely write prev f =
fi,∗ j−1 . In fact, since F0 = 0 and Fs−1 = 1, then:
wprev(i,1) = wi−1,s−1 = w − i = wi,0 , for every i ∈ [−W,W ].
This implies that wprev(i, j) = wi, j−1 for every i ∈ [−W,W ] and j ∈ [1, s − 1].
∗
∗
Whence, prev f = fprev
(i, j) = f i, j−1 .
So, at the (i, j)-th iteration of line 17, the following holds for every v ∈ V :
prev f (v) 6= > and f (v) = > iff fi,∗ j−1 (v) 6= > and fi,∗ j (v) = > [by Lemma 8]
iff v ∈ W0 (Γi, j−1 ) ∩ W1 (Γi, j ) [by Item 1-2 of Lemma 3]
iff valΓ (v) = i + Fj−1 [by Theorem 3]
This implies that, at the (i, j)-th iteration of line 18, Algorithm 1 correctly assigns the value ν(v) =
i + F[ j − 1] = i + Fj−1 to the vertex v.
Γ
Since for every
 vertex v ∈ V we have val (v) ∈ SΓ (recall that SΓ admits the following representation SΓ = i + Fj i ∈ [−W,W ), j ∈ [0, s − 1] ), then, as soon as Algorithm 1 halts, ν(v) =
valΓ (v) correctly holds for every v ∈ V . In turn, at line 20 and at line 22, the winning sets W0 and
W1 are correctly assigned as well.
Now, let us assume that ν(v) = i + Fj−1 holds at the (i, j)-th iteration of line 18, for some v ∈ V .
Then, the following holds on prev w at line 9:
prev w = wprev(i, j) = wi, j−1 = w − i − Fj−1 = w − ν(v) = w − valΓ (v).
Thus, at the (i, j)-th iteration of line 25, for every v ∈ V0 and u ∈ post(v):
prev f (v)  prev f (u)

∗
∗
prev w(v, u) iff fprev
(i, j) (v)  f prev(i, j) (u)


w − valΓ (v)
Γ (v)

∗
w−val
iff (v, u) is compatible with fprev
(i, j) in Γ
Γ (v)

∗
w−val
Recall that fprev
(i, j) is the least SEPM of Γ

f∗

, thus by Theorem 4 the following implication

Γ
Γw−val (v) ,

holds: if (v, u) is compatible with prev(i, j) in
then σ0 (v) = u is an optimal positional
strategy for Player 0, at v, in the MPG Γ.
This implies that line 26 of Algorithm 1 is correct and concludes the proof.
2

4.3

Complexity Analysis

The present section aims to show that Algorithm 1 always halts in O(|V |2 |E|W ) time. This upper
bound is established in the next proposition.
Proposition 2. Algorithm 1 always halts within O(|V |2 |E|W ) time and it works with O(|V |) space,
on any input MPG Γ = (V, E, w, hV0 ,V1 i). Here, W = maxe∈E |we |.

23

Proof. (Time Complexity of the Init Phase) The initialization of W0 , W1 , ν, σ0 (at line 1) and that
of f (at line 2) takes time O(|V |). The initialization of W at line 3 takes O(|E|) time. To conclude,
the size s = |F|V | | of the Farey sequence (i.e., its total number of terms) can be computed in
O(n2/3 log1/3 n) time as shown by Pawlewicz and Pătraşcu in [10]. Whence, the Init phase of
Algorithm 1 takes O(|E|) time overall.
(Time Complexity of the Scan Phases) To begin, notice that there are O(|V |2W ) scan phases
overall. In fact, at line 5 the index i goes from −W to W , while at line 7 the index j goes from
0 to s − 1 where s = |F|V | | = Θ(|V |2 ). Observe that, at each iteration, it takes O(|E|) time to go
from line 8 to line 14 and then from line 16 to line 27. In particular, at line 11, the j-th term Fj
of the Farey sequence F|V | can be computed in O(n2/3 log4/3 n) time as shown by Pawlewicz and
Pătraşcu in [10].
Now, let us denote by Ti,15j the time taken by the (i, j)-th iteration of line 15, that is the
0

time it takes to execute the Value-Iteration algorithm on input Γwi, j with initial energy levels:
∗
dD j fprev
(i, j) e. Then, the (i, j)-th scan phase always completes within the following time bound:
O(|E|) + Ti,15j .
We now focus on Ti,15j and argue that the (aggregate) total cost ∑i, j Ti,15j of executing the ValueIteration algorithm for EGs at line 15 (throughout all scan phases) is only O(|V |2 |E|W ). Stated
otherwise, we aim to show that the amortized cost of executing the (i, j)-th scan phase is only
O(|E|).
Recall that the Value-Iteration algorithm for EGs consists, as a first step, into an initialization
(which takes O(|E|) time) and, then, in the continuous iteration of the following two operations: (1)
the application of the lifting operator δ ( f , v) (which takes O(|post(v)|) time) in order to resolve
the inconsistency of f in v, where f (v) represents the current energy level and v ∈ V is any vertex
at which f is inconsistent; and (2) the update of the list L (which takes O(|pre(v)|) time), in order
to keep track of all the vertices that witness an inconsistency. Recall that L contains no duplicates.
At this point, since at the (i, j)-th iteration of line 15 the Value-Iteration is executed on input
w0i, j
Γ , then a scaling factor on the maximum absolute weight W must be taken into account. Indeed,
it holds that:
n
o
W 0 := max |w0i, j (e)| e ∈ E, i ∈ [−W,W ], j ∈ [0, s − 1] = O(|V |W ).
Remark. Actually, since w0i, j := D j (w − i) − N j (where N j /D j = Fj ∈ F|V | ), then the scaling factor
D j changes from iteration to iteration. Still, D j ≤ |V | holds for every j.
At each application of the lifting operator δ ( f , v) the energy level f (v) increases by at least
one unit with respect to the scaled-up maximum absolute weight W 0 . Stated otherwise, at each
application of δ ( f , v), the energy level f (v) increases by at least 1/|V | units with respect to the
original weight W .
Throughout the whole computation, the rational scalings of the energy levels never decrease by
Lemma 8: in fact, at the (i, j)-th scan phase, Algorithm 1 executes the Value-Iteration with initial
∗
energy levels: dD j fprev
(i, j) e. Whence, at line 15, the (i, j)-th execution of the Value-Iteration
starts from the (carefully scaled-up) energy levels of the prev(i, j)-th execution; roughly speaking,
no energy gets ever lost during this process. Then, by Lemma 4, each energy level f (v) can be
lifted-up at most |V |W 0 = O(|V |2 W ) times.
The above observations imply that the (aggregate) total cost of executing the Value-Iteration at

24

line 15 (throughout all scan phases) can be bounded as follows:

 

∑

−W ≤i≤W
1≤ j≤s−1





 
O(|E|) +  ∑ O |post(v)| + |pre(v)| O(|V |W 0 )
|
|
|
{z
}
|
{z
}
{z
}
{z
}
−W ≤i≤W
v∈V


Ti,15j = 

∑

1≤ j≤s−1 init cost
2

lifting δ

update L

Lemma 4

2


= O(|V | |E|W ) + O(|V | W ) ∑ O |post(v)| + |pre(v)|
v∈V

2

= O(|V | |E|W )
Whence, Algorithm 1 always halts within the following time bound:




T IME solve MPG Γ = ∑
O(E) + Ti,15j = O(|V |2 |E|W ).
−W ≤i≤W
1≤ j≤s−1

This concludes the proof of the time complexity bound.
We now turn our attention to the space complexity.
(Space Complexity) First of all, although the Farey sequence F|V | has |F|V | | = Θ(|V |2 ) many
elements, still, Algorithm 1 works fine assuming that every next element of the sequence is generated on the fly at line 11. This computation can be computed in O(|V |2/3 log4/3 |V |) sub-linear
time and space as shown by Pawlewicz and Pătraşcu [10]. Secondly, given i and j, it is not necessary to actually store all weights w0i, j (e) := D j (w(e) − i) − N j for every e ∈ E, as one can compute
them on the fly provided that N j , D j , w and e are given. Finally, Algorithm 1 needs to store in
memory the two SEPMs f and old f , but this requires only O(|V |) space. Finally, at line 15, the
Value-Iteration algorithm employs only O(|V |) space. In fact the list L, which it maintains in order
to keep track of inconsistencies, doesn’t contain duplicate vertices and, therefore, its length is at
most |L| ≤ |V |. These facts imply altogether that Algorithm 1 works with O(|V |) space.
2

5

Conclusions

In this work we proved an O(|V |2 |E|W ) pseudo-polynomial time upper bound for the Value Problem and Optimal Strategy Synthesis in Mean Payoff Games. The result was achieved by providing
a suitable description of values and positional strategies in terms of reweighted Energy Games and
Small Energy-Progress Measures.
On this way we ask whether further improvements are not too far away.
Acknowledgements. This work was supported by Department of Computer Science, University
of Verona, Verona, Italy, under PhD grant “Computational Mathematics and Biology”, on a cotutelle agreement with LIGM, Université Paris-Est in Marne-la-Vallée, Paris, France.

References
[1] Andersson, D., Vorobyov, S.: Fast algorithms for monotonic discounted linear programs with
two variables per inequality. Tech. rep., Preprint NI06019-LAA, Isaac Netwon Institute for
Mathematical Sciences, Cambridge, UK (2006)

25

[2] Bouyer, P., Fahrenberg, U., Larsen, K., Markey, N., Srba, J.: Infinite runs in weighted timed
automata with energy constraints. In: F. Cassez, C. Jard (eds.) Formal Modeling and Analysis
of Timed Systems, Lecture Notes in Computer Science, vol. 5215, pp. 33–47. Springer Berlin
Heidelberg (2008)
[3] Brim, L., Chaloupka, J., Doyen, L., Gentilini, R., Raskin, J.: Faster algorithms for meanpayoff games. Formal Methods in System Design 38(2), 97–118 (2011)
[4] Chakrabarti, A., de Alfaro, L., Henzinger, T., Stoelinga, M.: Resource interfaces. In: R. Alur,
I. Lee (eds.) Embedded Software, Lecture Notes in Computer Science, vol. 2855, pp. 117–
133. Springer Berlin Heidelberg (2003)
[5] Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. International
Journal of Game Theory 8(2), 109–113 (1979)
[6] Graham, R., Knuth, D., Patashnik, O.: Concrete Mathematics: A Foundation for Computer
Science, 2nd edn. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA (1994)
[7] Gurvich, V., Karzanov, A., Khachiyan, L.: Cyclic games and an algorithm to find minimax cycle means in directed graphs. USSR Computational Mathematics and Mathematical Physics
28(5), 85 – 91 (1988)
[8] Jurdziński, M.: Deciding the winner in parity games is in UP∩co-UP. Information Processing
Letters 68(3), 119 – 124 (1998)
[9] Lifshits, Y., Pavlov, D.: Potential theory for mean payoff games. Journal of Mathematical
Sciences 145(3), 4967–4974 (2007)
[10] Pawlewicz, J., Pătraşcu, M.: Order statistics in the farey sequences in sublinear time and
counting primitive lattice points in polygons. Algorithmica 55(2), 271–282 (2009)
[11] Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theoretical
Computer Science 158, 343–359 (1996)

26

