BRICS RS-00-48 Jurdziński & Vöge: A Discrete Stratety Improvement Algorithm for Solving Parity Games BRICS

Basic Research in Computer Science

A Discrete Stratety Improvement Algorithm for Solving Parity Games

Marcin Jurdziński Jens Vöge BRICS Report Series RS-00-48 ISSN 0909-0878 December 2000 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000, Marcin Jurdziński & Jens Vöge.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/00/48/

A Discrete Strategy Improvement Algorithm for Solving Parity Games^{∗}

Marcin Jurdziński^{†} BRICS^{‡}

Dept. of Computer Sci.

University of Aarhus Denmark

Jens Vöge^{§} Lehrstuhl für Informatik VII Fachgruppe Informatik RWTH Aachen Germany

December 2000

Abstract

A discrete strategy improvement algorithm is given for constructing winning strategies in parity games, thereby providing also a new solution of the model-checking problem for the modal μ-calculus. Known strategy improvement algorithms, as proposed for stochastic games by Hoffman and Karp in 1966, and for discounted payoff games and parity games by Puri in 1995, work with real numbers and require solving linear programming instances involving high precision arithmetic. In the present algorithm for parity games these difficulties are avoided by the use of discrete

∗A preliminary version of this paper [21] was published in: Computer Aided Verification, 12th International Conference, CAV 2000, Proceedings, volume 1855 of Lecture Notes in Computer Science, pages 202–215, Chicago, IL, USA, July 2000, Springer-Verlag.

†Address: BRICS, Department of Computer Science, University of Aarhus, Ny Munkegade Building 540, DK-8000 Aarhus C, Denmark. Email: mju@brics.dk. A part of the work reported here was done while the author was a research assistant at Lehrstuhl für Informatik VII, RWTH Aachen, Germany.

‡Basic Research in Computer Science, Centre of Danish Science Foundation.

§Address: RWTH Aachen, Lehrstuhl für Informatik VII, D-52056 Aachen, Germany. Email: voege@informatik.rwth-aachen.de. Supported by the Deutsche Forschungsgemeinschaft (DFG), project Th 352/5-3.

vertex valuations in which information about the relevance of vertices and certain distances is coded. An efficient implementation is given for a strategy improvement step. Another advantage of the present approach is that it provides a better conceptual understanding and easier analysis of strategy improvement algorithms for parity games. However, so far it is not known whether the present algorithm works in polynomial time. The long standing problem whether parity games can be solved in polynomial time remains open.

1 Introduction

The study of the computational complexity of solving parity games has two main motivations. One is that the problem is polynomial time equivalent to the modal μ-calculus model checking [8, 19], and hence better algorithms for parity games may lead to better model checkers, which is a major objective in computer aided verification.

The other motivation is the intriguing status of the problem from the point of view of structural complexity theory. It is one of the few natural problems which is in NP ∩ co-NP [8] (and even in UP ∩ co-UP [10]), and is not known to have a polynomial time algorithm, despite substantial effort of the community (see [8, 1, 18, 11] and references there). Other notable examples of such problems include simple stochastic games [3, 4], mean payoff games [6, 23], and discounted payoff games [23]. There are polynomial time reductions of parity to mean payoff games [16, 10], mean payoff to discounted payoff games [23], and discounted payoff to simple stochastic games [23]. Parity games, as the simplest of them all, seem to be the most plausible candidate for trying to find a polynomial time algorithm.

A strategy improvement algorithm has been proposed for solving stochastic games by Hoffman and Karp [9] in 1966. Puri in his PhD thesis [16] has adapted the algorithm for discounted payoff games. Puri also provided a polynomial time reduction of parity games to mean payoff games, and advocated the use of the algorithm for solving parity games, and hence for the modal μ-calculus model checking.

In our opinion Puri’s strategy improvement algorithm for solving parity games has two drawbacks.

• The algorithm uses high precision arithmetic, and needs to solve linear programming instances: both are typically costly operations.

An implementation (by the first author) of Puri’s algorithm, using a linear programming algorithm of Meggido [13], proved to be prohibitively slow.

• Solving parity games is a discrete, graph theoretic problem, but the crux of the algorithm is manipulation of real numbers, and its analysis is crucially based on continuous methods, such as Banach’s fixed point theorem.

The first one makes the algorithm inefficient in practice, the other one obscures understanding of the algorithm.

Our discrete strategy improvement algorithm remedies both shortcomings of Puri’s algorithm mentioned above, while preserving the overall structure of the generic strategy improvement algorithm. We introduce discrete values (such as tuples of: vertices, sets of vertices and natural numbers denoting lengths of paths in the game graph) which are being manipulated by the algorithm, instead of their encodings into real numbers. (One can show a precise relationship between behaviour of Puri’s and our algorithms; we will treat this issue elsewhere.)

The first advantage of our approach is that we avoid solving linear programming instances involving high precision arithmetic. Instead, a shortest paths instance needs to be solved in every strategy improvement step of the algorithm. The shortest paths instances occurring in this context have discrete weights recording relevance of vertices and distances in the game graph. We develop an algorithm exploiting the special structure of these instances instead of using standard shortest paths algorithms. Our algorithm gives an efficient implementation of a single improvement step of the strategy improvement algorithm. Its running time is O(n · m), where n is the number of vertices, and m is the number of edges in the game graph. In comparison, a naive application of Bellman-Ford algorithm [5] gives O(n^{2} · m) running time.

The other advantage is more subjective: we believe that it is easier to analyze the discrete data maintained by our algorithm, rather than its subtle encodings into real numbers involving infinite geometric series [16]. The classical continuous reasoning involving Banach fixed point theorem gives an elegant proof of correctness of the algorithm in a more general case of discounted payoff games [16], but we think that in the case of parity games it blurs an intuitive understanding of the underlying discrete structure. However, the long standing open question whether a strategy improvement algorithm works in polynomial time [4] remains unanswered. Nevertheless, we hope that our discrete analysis of the algorithm may help either to find a proof of polynomial time termination, or to come up with a family of examples on which the algorithm requires exponential number of steps. Any of those results would mark a substantial progress in understanding the computational complexity of parity games.

So far, for all families of examples we have considered the strategy improvement algorithm needs only linear number of strategy improvement steps. Notably, a linear number of strategy improvements suffices for several families of difficult examples for which other known algorithms need exponential time.

The rest of this chapter is organized as follows. In section 2 we define the infinite parity games and we establish their equivalence to finite cycledomination games. In section 3 we sketch the idea of a generic strategy improvement algorithm and we state general postulates which guarantee correctness of the algorithm. Then in section 4 we give a specific proposal for the ingredients of a generic strategy improvement algorithm. In section 5 we prove that these ingredients satisfy the postulates of section 3. In this way we get a purely discrete strategy improvement algorithm for solving parity games. In section 6 we give a specialized shortest paths algorithm for the shortest paths instances occurring in our strategy improvement algorithm. In this way we obtain an efficient O(n · m) implementation of a strategy improvement step, where n is the number of vertices, and m is the number of edges in the game graph. Finally, in section 7 we discuss partial results and open questions concerning the time complexity of strategy improvement algorithms.

2 Parity games

2.1 Infinite parity games

A game graph G = (V, E, (M_{Even}, M_{Odd}), p) of a parity game consists of a directed graph (V, E), a partition (M_{Even}, M_{Odd}) of the set of vertices V, and a priority function p : V → {0, 1, …, k} for some k ∈ ℕ. We restrict ourselves to finite parity game graphs and for technical convenience we assume that every vertex has at least one out-going edge.

An infinite parity game G^{∞} is a two-person infinite duration pathforming game played on graph G. The two players, Even and Odd, keep moving a token along edges of the game graph: player Even moves the token from vertices in M_{Even}, and player Odd moves the token from vertices in M_{Odd}. A play of G^{∞} is an infinite path ⟨v_{0}, v_{1}, v_{2}, …⟩ in the game graph G arising in this way. A play P = ⟨v_{0}, v_{1}, v_{2}, …⟩ is winning for player Even if the biggest priority occurring infinitely often in P (i.e., the biggest number occurring infinitely often in ⟨p(v_{0}), p(v_{1}), p(v_{2}), …⟩) is even; otherwise P is winning for player Odd.

A memoryless strategy for player Even is a function σ : M_{Even} → V such that (v, σ(v)) ∈ E for all v ∈ M_{Even}. (We consider only memoryless strategies here so for brevity we just write strategies to denote memoryless strategies throughout the paper.) A play ⟨v_{0}, v_{1}, v_{2}, …⟩ is consistent with a strategy σ for player Even if v_{ℓ+1} = σ(v_{ℓ}) for all ℓ ∈ ℕ, such that v_{ℓ} ∈ M_{Even}. Strategies for player Odd are defined analogously. If σ is a strategy for player Even (Odd) then we write G_{σ} to denote the game graph obtained from G by removing all the edges (v, w), such that v ∈ M_{Even} (v ∈ M_{Odd}) and σ(v) ≠ w; we write E_{σ} for the set of edges of G_{σ}. If σ is a strategy for player Even and τ is a strategy for player Odd then we write G_{στ} for (G_{σ})_{τ}; we write E_{στ} for its set of edges.

Note that if σ is a strategy for player Even and τ is a strategy for player Odd then for every vertex v, there is a unique play P_{στ}(v) starting from v and consistent with both σ and τ. We say that a strategy σ for player Even is a winning strategy from a vertex v if for every strategy τ for player Odd, the unique play P_{στ}(v) starting from v and consistent with both σ and τ is winning for player Even. A strategy σ is a winning strategy from a set of vertices W if it is winning from every vertex in W. Winning strategies for player Odd are defined analogously.

Remark. In literature on parity games (see for example [20, 22, 10]) a different definition of a winning strategy is used; here we call it “a strategy winning against arbitrary strategies.” We say that a strategy σ for player Even (Odd) is a strategy winning against arbitrary strategies from a vertex v if every play starting from v and consistent with σ is winning for player Even (Odd). We argue that the two definitions are equivalent for parity games.

Proposition 2.1 A strategy σ for player Even (Odd) is a winning strategy from a vertex v if and only if σ is a strategy winning against arbitrary strategies from v.

Proof. The “if” part is obvious.

We prove the “only if” part for player Even; the proof for player Odd is analogous. Suppose that σ is a winning strategy for player Even from v. Then the biggest priority on every cycle in G_{σ} reachable from v in G_{σ} is even. Let P be an infinite play consistent with σ. We argue that the biggest priority occurring infinitely often on P is even. Using a simple stacking technique (see for example [23], page 347, or [10], page 122) we can decompose play P into a finite path and an infinite number of simple cycles in G_{σ}. (The decomposition may be different if the game graph is infinite, but the proposition can be proved in a very similar way also for parity games with infinite game graphs.) Note that biggest priorities in all simple cycles in the decomposition are even because all the cycles are cycles in G_{σ} reachable from v in G_{σ}. Hence the maximal priority occurring infinitely often in P is even, i.e., P is a winning play for player Even. [Proposition 2.1] [Remark] □

Theorem 2.2 (Memoryless Determinacy [7, 15]) For every parity game graph G, there is a unique partition (W_{Even}, W_{Odd}) of the set of vertices of G, such that there is a winning strategy for player Even from W_{Even} in G^{∞} and a winning strategy for player Odd from W_{Odd} in G^{∞}.

We call sets W_{Even} and W_{Odd} the winning sets of player Even and player Odd, respectively. The problem of deciding the winner in parity games is, given a parity game graph and a vertex of the graph, to determine whose winning set the vertex belongs to. By solving a parity game we mean finding the partition (W_{Even}, W_{Odd}).

2.2 Finite cycle-domination games

For the purpose of development and reasoning about our discrete strategy improvement algorithm for solving parity games it is technically convenient to reformulate a bit the standard definition of parity games outlined above. Below we define finite cycle-domination games and we give a simple translation of every parity game into an equivalent cycle-domination game.

A game graph G = (V, E, (M_{⊕}, M_{⊖}), (R_{+}, R_{−})) of a cycle-domination game consists of a directed graph (V, E), where V = {1, 2, …, n} for some n ∈ ℕ, and of two partitions (R_{+}, R_{−}) and (M_{⊕}, M_{⊖}) of the set of vertices V. We sometimes refer to the numbers identifying vertices as their priorities, and we use the standard ≤ order on natural numbers to compare them.

A finite cycle-domination game G^{ω} is a two-person finite path-forming game played on graph G. The two players, player ⊕ and player ⊖, play similarly to players Even and Odd in infinite parity games by moving a token along edges of the game graph G: player ⊕ moves the token from vertices in M_{⊕}, and player ⊖ moves the token from vertices in M_{⊖}. The difference from infinite parity games is that a play is finished as soon as the path constructed so far by the players contains a cycle. In other words, a play in G^{ω} is a finite path P = ⟨v_{0}, v_{1}, …, v_{ℓ}⟩ in the game graph G, such that v_{i} ≠ v_{j} for all 1 ≤ i < j < ℓ, and there is a k < ℓ, such that v_{k} = v_{ℓ}. It follows that ⟨v_{k}, v_{k+1}, …, v_{ℓ}⟩ is the only cycle in play P; we write Cycle(P) to denote this unique cycle, and we call it the cycle of P. We define the cycle dominating value λ(P) of play P to be max^{≤} (Cycle(P)) = max^{≤}{v_{k}, v_{k+1}, …, v_{ℓ}}, i.e., the vertex with biggest priority in the cycle of P. We say that a play P in G^{ω} is winning for player ⊕ if λ(P) ∈ R_{+}, otherwise λ(P) ∈ R_{−} and play P is winning for player ⊖. Strategies and winning strategies for both players in G^{ω} are defined similarly as in infinite parity games.

Given a parity game graph G = (V, E, p, (M_{Even}, M_{Odd})) we construct a cycle-domination game graph \overline{G} = (V, E, (R_{+}, R_{−}), (M_{⊕}, M_{⊖})), such that the games G^{∞} and \overline{G}^{ω} are equivalent in the following sense.

Proposition 2.3 A strategy σ is a winning strategy for player Even (player Odd) from a vertex v in G^{∞} if and only if σ is a winning strategy for player ⊕ (player ⊖) from v in \overline{G}^{ω}.

Construction of \overline{G}: Let M_{⊕} = M_{Even}, M_{⊖} = M_{Odd}, and

R_{+} = { v ∈ V : p(v) is even }, and R_{−} = { v ∈ V : p(v) is odd }.

We introduce a total order relation ≤ on V called the relevance order. Let the relevance order ≤ be an arbitrary total order extending the preorder induced by priorities, i.e., such that p(v) ≤ p(w) implies v ≤ w for all v, w ∈ V. Note that we use the same symbol “≤” for the standard order on natural numbers and for the relevance order; in fact we identify vertices in V with integers in the set {1, 2, …, |V |} via the unique orderisomorphism between the total orders (V, ≤) and ({1, 2, …, |V |}, ≤ ).

Proof (of Proposition 2.3). The first condition, i.e., that σ is a winning strategy for player Even (player Odd) in G^{∞} is equivalent to saying that for every cycle in G_{σ} reachable from v in G_{σ}, the biggest priority occurring on the cycle is even (odd). The other condition, i.e., that σ is a winning strategy for player ⊕ (player ⊖) in \overline{G}^{ω} is equivalent to saying that for every cycle in \overline{G}_{σ}, the most relevant vertex in the cycle belongs to R_{+} (R_{−}). It follows immediately from the construction of \overline{G} that the biggest priority occurring on a cycle in G_{σ} is even (odd), if and only if the most relevant vertex in the same cycle in \overline{G}_{σ} belongs to R_{+} (R_{−}), and so we are done. [Proposition 2.3]

3 Generic strategy improvement algorithm

In order to develop a strategy improvement algorithm for solving cycledomination games we define the problem of solving cycle-domination games as an “optimization problem.” Suppose we have a pre-order ⊑ on the set Strategies_{⊕} ⊆ (M_{⊕} → V) of strategies for player ⊕, satisfying the following two postulates.

P1. There is a maximum element in the pre-order (Strategies_{⊕}, ⊑), i.e., there is a strategy σ ∈ Strategies_{⊕}, such that κ ⊑ σ for all

     κ ∈ Strategies_{⊕}.

P2. If σ is a maximum element in the pre-order (Strategies_{⊕}, ⊑) then σ is a winning strategy for player ⊕ from every vertex of her winning set.

The problem of solving a cycle-domination game with respect to ⊑ is, given a cycle-domination game, to find a strategy for player ⊕ which is a maximum element in the pre-order (Strategies_{⊕}, ⊑).

Suppose we also have an operator

            Improve : Strategies_{⊕} → Strategies_{⊕},

satisfying the following two postulates:

I1. If σ is not a maximum element in the pre-order (Strategies_{⊕}, ⊑) then σ ⊑ Improve(σ) and Improve(σ) ⋢ σ.

I2. If σ is a maximum element in the pre-order (Strategies_{⊕}, ⊑) then we have Improve(σ) = σ.

A generic strategy improvement algorithm is the following procedure.

Strategy improvement algorithm

     pick a strategy σ for player ⊕

while σ ≠ Improve(σ) do σ := Improve(σ)

Note that postulate I1. guarantees that the algorithm terminates, because there are only finitely many strategies for player ⊕. Postulate I2. implies that when the algorithm terminates then the strategy σ is a maximum element in the pre-order (Strategies_{⊕}, ⊑). Altogether, we get the following.

Theorem 3.1 If a pre-order (Strategies_{⊕}, ⊑) satisfies postulates P1. and P2., and an Improve operator satisfies postulates I1. and I2. then strategy improvement algorithm is a correct algorithm for solving cycle-domination games with respect to ⊑.

4 Discrete strategy improvement algorithm

Below we give a particular proposal for a pre-order (Strategies_{⊕}, ⊑) satisfying postulates P1. and P2., and an Improve operator satisfying postulates I1. and I2. These definitions are based on discrete valuations assigned to strategies and hence give rise to a purely discrete strategy improvement algorithm for solving cycle-domination games.

4.1 Play values

For every w ∈ V, we define V_{>w} = { v ∈ V : v > w }, and V_{<w} = { v ∈ V : v < w }.

Let P = ⟨v_{1}, v_{2}, …, v_{ℓ}⟩ be a play, and let v_{k} = λ(P), i.e., the cycle value of P is the k-th element of P. Let Prefix(P) = {v_{1}, v_{2}, …, v_{k−1}}, i.e., Prefix(P) is the set of vertices in play P occurring before the loop value of P. We define the primary path value π(P) of play P to be Prefix(P) ∩ V_{>λ(P)}, i.e., the set of vertices occurring in P with priorities bigger than λ(P). We define the secondary path value #(P) of play P to be |Prefix(P)|, i.e., the length of the path from the initial vertex of P to λ(P). The path value of play P is defined to be the ordered pair (π(P), #(P)) ∈ ℘(V) × ℕ. The play value Θ(P) of play P is defined

to be the ordered pair (λ(P), (π(P), #(P))) ∈ V × (℘(V) × ℕ). We write PlayValues to denote the image of the function Θ : Plays → V × (℘(V) × ℕ). Note that

PlayValues ⊆ { (v, (B, k)) : B ⊆ V_{>v} }.  (1)

4.2 Linear order ⊴ on PlayValues

For all v ∈ V, we define

Reward(v) = \begin{cases}−v & if v ∈ R_{−}, \\ v & if v ∈ R_{+}. \end{cases}

For all v, w ∈ V, we define v ⪯ w to hold if and only if Reward(v) ≤ Reward(w). We write v ≺ w if v ⪯ w and v ≠ w. Note that ⪯ is a linear order on V, and m ≺ p for all m ∈ R_{−} and p ∈ R_{+}.

For B, C ∈ ℘(V), such that B ≠ C, we define

MaxDiff(B, C) = max^{≤}((B \ C) ∪ (C \ B)).

We define B ≺ C to hold if and only if either

• MaxDiff(B, C) ∈ (B \ C) ∩ R_{−}, or

• MaxDiff(B, C) ∈ (C \ B) ∩ R_{+}.

We write B ⪯ C if B ≺ C or B = C. For ℓ ∈ V, we write B ⪯_{ℓ} C if B ∩ V_{>ℓ} ⪯ C ∩ V_{>ℓ}. We write B =_{ℓ} C if B ⪯_{ℓ} C and C ⪯_{ℓ} B. We write B ≺_{ℓ} C if B ⪯_{ℓ} C and C ⪯̸_{ℓ} B.

For all ℓ ∈ V, and (B, k), (B′, k′) ∈ ℘(V) × ℕ, we define the relation (B, k) ⊴_{ℓ} (B′, k′) to hold if and only if either

• B ≺_{ℓ} B′, or

• B =_{ℓ} B′ and either

– ℓ ∈ R_{−} and k ≤ k′, or – ℓ ∈ R_{+} and k′ ≤ k.

We write (B, k) ◁_{ℓ} (B′, k′) if (B, k) ⊴_{ℓ} (B′, k′) and (B′, k′) ⋬_{ℓ} (B, k).

For all (ℓ, (B, k)), (ℓ′, (B′, k′)) ∈ V × (℘(V) × ℕ), we define the relation (ℓ, (B, k)) ⊴ (ℓ′, (B′, k′)) to hold if and only if either

• ℓ ≺ ℓ′, or

• ℓ = ℓ′ and (B, k) ⊴_{ℓ} (B′, k′).

For ξ, ξ′ ∈ V × (℘(V) × ℕ), we write ξ ◁ ξ′ if ξ ⊴ ξ′ and ξ′ ⋬ ξ.

Note that (1) guarantees that ⊴ is a linear order on PlayValues. It is a linear pre-order on V × (℘(V) × ℕ).

Example. Note that ξ_{1} = (3, {1}, 2) and ξ_{2} = (3, {2}, 2) are not play values, because {1} ⊈ V_{>3} and {2} ⊈ V_{>3}, respectively. We have ξ_{1} ⊴ ξ_{2} and ξ_{2} ⊴ ξ_{1}, even though ξ_{1} ≠ ξ_{2}. [Example] □

4.3 Pre-order ⊑ on Strategies_{⊕}

We write Valuations to denote the set (V → PlayValues) of functions assigning a play value to every vertex of the game graph. We extend the ⊴ order to a partial order on Valuations by defining it point-wise, i.e., for Ξ, Ξ′ ∈ Valuations we define Ξ ⊴ Ξ′ to hold if Ξ(v) ⊴ Ξ′(v) for all v ∈ V. We write Ξ ◁ Ξ′ if Ξ ⊴ Ξ′ and Ξ ≠ Ξ′.

Valuation Ω_{σ}. For every strategy σ ∈ Strategies_{⊕} we define Ω_{σ} ∈ Valuations in the following way:

Ω_{σ}(v) = min^{⊴}{ Θ(P) : P ∈ Plays_{σ}(v) },

where Plays_{σ}(v) is the set of plays starting from vertex v and consistent with σ. Finally, for σ, σ′ ∈ Strategies_{⊕} we define σ ⊑ σ′ to hold if and only if Ω_{σ} ⊴ Ω_{σ′}. We write σ ⊏ σ′ if Ω_{σ} ◁ Ω_{σ′}.

4.4 An Improve operator

We say that a set I ⊆ E is unambiguous if (v, w) ∈ I and (v, u) ∈ I imply that w = u. For every unambiguous set of edges I, we define an

operator Switch_{I} : Strategies_{⊕} → Strategies_{⊕} as follows:

[Switch_{I}(σ)](v) = \begin{cases}w & if (v, w) ∈ I for some w ∈ V, \\ σ(v) & otherwise. \end{cases}

We say that an edge (v, w) ∈ E is an improvement for a strategy σ if

Ω_{σ}(σ(v)) ◁ Ω_{σ}(w).  (2)

We define a (non-deterministic) operator Improve : Strategies_{⊕} → Strategies_{⊕} as follows:

Improve(σ) = \begin{cases}Switch_{I}(σ) & for some set I ≠ ∅ of improvements for σ, \\ σ & if there are no improvements for σ. \end{cases}

Let I_{1}, I_{2}, …, I_{t} ⊆ E, and let σ be a strategy for player ⊕. Define σ_{0} = σ, and σ_{k} = Switch_{I_{k}}(σ_{k−1}) for k > 0. We say that P = ⟨I_{1}, I_{2}, …, I_{t}⟩ is a strategy improvement policy for σ if:

• for all k ≤ t, we have that I_{k} ≠ ∅ is an unambiguous set of improvements for σ_{k−1}, and

• there are no improvements for σ_{t}.

4.5 A few technical definitions

Pre-orders ⊴_{ℓ} on M(V) × ℕ. For technical reasons, for every ℓ ∈ V, we extend the pre-order ⊴_{ℓ} on ℘(V) × ℕ to M(V) × ℕ, where M(V) is the set of multi-sets of elements of V. The definitions of ⪯_{ℓ}, and ⊴_{ℓ} are the same as for ℘(V) × ℕ; the only difference is that MaxDiff for B, C ∈ M(V) is defined by

MaxDiff(B, C) = max^{≤}((B \_{M} C) ∪ (C \_{M} B)),

where \_{M} is the multiset difference, and B ≺ C is defined to holds if and only if either

• MaxDiff(B, C) ∈ (B \_{M} C) ∩ R_{−}, or

• MaxDiff(B, C) ∈ (C \_{M} B) ∩ R_{+}.

Example. If 3 ∈ R_{−} then we have {1, 3, 3} ⪯ {1, 2, 3} because

MaxDiff({1, 3, 3}, {1, 2, 3}) = 3

and 3 ∈ ({1, 3, 3} \_{M} {1, 2, 3}) ∩ R_{−}. [Example] □

Pre-orders ˜⊴_{ℓ} on M(V) × ℕ. We define the following weakening of the ⊴_{ℓ} pre-order. For ℓ ∈ V and (B, k), (B′, k′) ∈ M(V) × ℕ, we define (B, k)˜⊴_{ℓ}(B′, k′) to hold if and only if B ⪯_{ℓ} B′. We write (B, k) ≅_{ℓ} (B′, k′) if (B, k)˜⊴_{ℓ}(B′, k′) and (B′, k′)˜⊴_{ℓ}(B, k). Note that ˜⊴_{ℓ} is a preorder on M(V)×ℕ, and that ˜⊴_{ℓ} is coarser than ⊴_{ℓ}, i.e., (B, k) ⊴_{ℓ} (B′, k′) implies (B, k)˜⊴_{ℓ}(B′, k′). Note, for example, that if 2 ∈ R_{+} then we have ({2, 3}, 1) ≅_{2} ({1, 3}, 2), but ({2, 3}, 1) ⋬_{2} ({1, 3}, 2).

Operation ⊞ on M(V) × ℕ. For (B, k), (B′, k′) ∈ M(V) × ℕ, we define (B, k)⊞(B′, k′) = (B∪_{M}B′, k+k′), where ∪_{M} is the multi-set union. We also use the following shorthand: if C ∈ ℘(V) then (B, k) ⊞ C is defined to be equal to (B, k) ⊞ (C, |C|), i.e., we have that (B, k) ⊞ C = (B ∪_{M} C, k + |C|). Moreover, if v ∈ V then we often write (B, k) ⊞ v instead of (B, k)⊞{v}. In other words, we have that (B, k)⊞v = (B ∪_{M} {v}, k+1).

5 Correctness of the algorithm

In order to prove correctness of our discrete strategy improvement algorithm, i.e., to establish Theorem 3.1, it suffices to argue that the definitions of subsection 4 satisfy postulates P1., P2., I1., and I2.

5.1 Valuation Ω_{σ} and shortest paths

Let Ω_{σ} = (Λ_{σ}, Π_{σ}) : V → V × (℘(V) × ℕ). We establish the following characterization of Ω_{σ}.

1. Let T_{σ} = {t ∈ V : there is a cycle C in G_{σ}, such that max^{≤}(C) = t}. Then for all v ∈ V, we have that

Λ_{σ}(v) = min^{⪯}{ t ∈ T_{σ} : there is a path from v to t in G_{σ} }. (3)

2. For v, t ∈ V, we define Path_{σ}(v, t) to be the set of sets of vertices S ∈ ℘(V), such that S ∪ {t} is the set of vertices occurring on a (simple) path from v to t in G_{σ}. Let v ∈ V and let ℓ = Λ_{σ}(v). Then we have

Π_{σ}(v) = min^{⊴_{ℓ}}{ (S ∩ V_{>ℓ}, |S|) : S ∈ Path_{σ}(v, ℓ) }. (4)

Clause 1. is straightforward. Note that for all (v, w) ∈ E_{σ} we have

Λ_{σ}(v) ⪯ Λ_{σ}(w).  (5)

We argue that clause 2. holds. Let P ∈ Plays_{σ}(v), such that Θ(P) = Ω_{σ}(v). Let R = Prefix(P) and let C = Cycle(P). Then Λ_{σ}(v) = λ(P) and

Π_{σ}(v) = (π(P), #(P)) = ((R ∪ C) ∩ V_{>ℓ}, |R|),

i.e., Π_{σ}(v) = (R ∩ V_{>ℓ}, |R|); the last equality holds because max^{≤}(C) = λ(P). Therefore, we have that

Π_{σ}(v) = min^{⊴_{ℓ}}{ (π(P), #(P)) : P ∈ Plays_{σ}(v) and λ(P) = ℓ }
= min^{⊴_{ℓ}}{ (S ∩ V_{>ℓ}, |S|) : S ∈ Path_{σ}(v, ℓ) }.

As a result of the above we get a characterization of Π_{σ}(v) as a solution of the following shortest paths problem instance. For ℓ ∈ T_{σ} consider the subgraph G_{σ}^{ℓ} = (V^{ℓ}, E_{σ}^{ℓ}) of G_{σ} induced by V^{ℓ} = {v ∈ V : Λ_{σ}(v) = ℓ}. With every edge (v, w) ∈ E_{σ}^{ℓ} we associate the weight ({v} ∩ V_{>ℓ}, 1) ∈ M(V) × ℕ. The set of weights of paths in G_{σ}^{ℓ} is M(V) × ℕ with ⊞ as the operation of adding weights. Shortest paths are taken with respect to the ⊴_{ℓ} pre-order on M(V) × ℕ.

Remark. Section 26.4 of the book by Cormen et al. [5] describes an algebraic structure called a closed semi-ring that allows to define a shortest paths problem and devise algorithms for finding shortest paths. We leave it as an exercise to the reader to verify that for every ℓ ∈ V, the set M(V) × ℕ with the extension operator ⊞ and the summation operator max^{⊴_{ℓ}} forms a closed semi-ring. [Remark] □

Note that from Λ_{σ}(v) = ℓ for all v ∈ V^{ℓ}, it follows that all cycles in G_{σ}^{ℓ} have “non-negative” weight, i.e., they have weight ⊴_{ℓ}-bigger than (∅, 0) if ℓ ∈ R_{−}, and ⊴_{ℓ}-bigger than (∅, +∞) if ℓ ∈ R_{+}. Therefore, shortest paths to ℓ exist from each vertex v ∈ V^{ℓ}, they are simple paths, and Π_{σ}(v) is the weight of the shortest path from v to ℓ in G_{σ}^{ℓ}.

Observe, that for v ≠ ℓ, the characterization of Π_{σ}(v) as the weight of a shortest path from v to ℓ implies, that if w ∈ V^{ℓ} is a successor of v on a shortest path from v to ℓ in G_{σ}^{ℓ} then

Π_{σ}(v) =_{ℓ} Π_{σ}(w) ⊞ v,  (6)

and for all (v, u) ∈ E_{σ}^{ℓ} we have

Π_{σ}(v) ⊴_{ℓ} Π_{σ}(u) ⊞ v.  (7)

Note that we have

Π_{σ}(ℓ) = (∅, 0).  (8)

Moreover, observe that by definition of ℓ ∈ T_{σ}, there is a cycle C in G_{σ}^{ℓ}, such that max^{≤}(C) = ℓ, and there are no cycles with “negative” weight. Therefore, if w is the successor of ℓ with a shortest path to ℓ then Π_{σ}(w) = (∅, k) for some k ∈ ℕ, and hence we have

Π_{σ}(ℓ) ≅_{ℓ} Π_{σ}(w) ⊞ ℓ,  (9)

and for all (ℓ, u) ∈ E_{σ}^{ℓ} we have

Π_{σ}(ℓ) ˜⊴_{ℓ} Π_{σ}(u) ⊞ ℓ.  (10)

5.2 Locally progressive valuations

Strategy \overline{σ} for player ⊖. Let σ be a strategy for player ⊕. We define a strategy \overline{σ} for player ⊖ in the following way. For every v ∈ M_{⊖}, we set:

\overline{σ}(v) = w, such that Ω_{σ}(w) ⊴ Ω_{σ}(u) for all u ∈ succ(v),

i.e., \overline{σ}(v) is defined to be a successor of v which minimizes the value of Ω_{σ} with respect to ⊴. Note that from the characterization of Ω_{σ} from the previous subsection it follows that for all (v, w) ∈ E_{σ\overline{σ}}, we have Λ_{σ}(v) = Λ_{σ}(w). Moreover, claims (6) and (9) hold, respectively, for all (v, w) ∈ E_{σ\overline{σ}}, depending on whether Λ_{σ}(v) ≠ v or Λ_{σ}(v) = v, respectively. These observations together with claim (8) motivate the following notion of a locally progressive valuation.

Locally progressive valuation. Let Ξ = (Λ, Π) : V → V × (℘(V) × ℕ) be a valuation. We define Prog(Ξ, e) to hold for e = (v, w) ∈ E, if and only if:

1. Λ(v) = Λ(w), and

2. if Λ(v) ≠ v then Π(v) =_{Λ(v)} Π(w) ⊞ v, and

3. if Λ(v) = v then Π(v) ≅_{Λ(v)} Π(w) ⊞ v and Π(v) = (∅, 0).

We say that Ξ is a locally progressive valuation for strategies σ and τ if and only if Prog(Ξ, e) holds, for all e ∈ E_{στ}.

The following fact follows immediately from the definition of strategy \overline{σ} and from (3), (6), (8), and (9).

Proposition 5.1 Valuation Ω_{σ} is a locally progressive valuation for σ and \overline{σ}.

Valuation Θ_{στ}. Note that if σ and τ are strategies for player ⊕ and for player ⊖, respectively, then for every vertex v ∈ V, there is a unique play P_{στ}(v) starting from v and consistent with σ and τ. We write Θ_{στ} for a valuation defined by Θ_{στ}(v) = Θ(P_{στ}(v)).

In the following lemma we establish that a locally progressive valuation for σ and τ is a local characterization of the valuation Θ_{στ}.

Lemma 5.2 A valuation Ξ is a locally progressive valuation for σ and τ if and only if Ξ = Θ_{στ}.

Proof. Let v ∈ V and let P_{στ}(v) = ⟨v_{1}, v_{2}, …, v_{ℓ}⟩ be the unique play starting from v and consistent with σ and τ. It is easy to verify that Θ_{στ} is a locally progressive valuation for σ and τ. We show that if Ξ is a locally progressive valuation for σ and τ then Ξ(v) = Θ(P_{στ}(v)).

Let C = {v_{k}, v_{k+1}, …, v_{ℓ−1}} be the cycle of P_{στ}(v), i.e., let v_{k} = v_{ℓ} and k < ℓ. Let Ξ = (Λ, Π), where Λ : V → V and Π : V → (M(V) × ℕ). By definition of a locally progressive valuation we get that Λ(v_{1}) = Λ(v_{2}) = ⋯ = Λ(v_{ℓ}). Let ℓ = Λ(v). We claim that λ(P_{στ}(v)) = Λ(v), i.e., that max^{≤}(C) = ℓ.

By definition of a locally progressive valuation we get that Π(v_{i}) ≅_{ℓ} Π(v_{i+1}) ⊞ v_{i} for all i ∈ {k, k + 1, …, ℓ − 1}. This implies that

Π(v_{k}) ≅_{ℓ} Π(v_{ℓ}) ⊞ {v_{k}, v_{k+1}, …, v_{ℓ−1}} = Π(v_{k}) ⊞ C.

It follows that max^{≤}(C) ≤ ℓ. Note that max^{≤}(C) < ℓ implies that Π(v_{i}) =_{ℓ} Π(v_{i+1}) ⊞ v_{i} for all i ∈ {k, k + 1, …, ℓ − 1}, i.e., that Π(v_{k}) =_{ℓ} Π(v_{k})⊞C holds. This, however, is impossible because |C| > 0. Therefore, we get that max^{≤}(C) = ℓ.

Now we argue that Π(v) is equal to the path value of P_{στ}(v). By definition of a locally progressive valuation we get that Π(v_{i}) =_{ℓ} Π(v_{i+1})⊞ v_{i} for all i ∈ {1, 2, …, k − 1}, and that Π(v_{k}) = (∅, 0). Therefore, we get that

Π(v) =_{ℓ} (∅, 0) ⊞ Prefix(P_{στ}(v)) =_{ℓ} (π(P_{στ}(v)), #(P_{στ}(v))).

[Lemma 5.2]

A best counter-strategy against σ. Note that by Proposition 5.1, an immediate corollary of Lemma 5.2 is that

Ω_{σ} = Θ_{σ\overline{σ}}.  (11)

Hence by definition of Ω_{σ} we get that Θ_{σ\overline{σ}} ⊴ Θ_{στ}, for all strategies τ for player ⊖. In other words, \overline{σ} is a best counter-strategy against σ.

5.3 Locally under-progressive valuations

Motivated by conditions (5), (7), (8), and (10) satisfied by Ω_{σ}, we introduce a relaxation of the notion of a locally progressive valuation called a locally under-progressive valuation.

Locally under-progressive valuation. Let Ξ = (Λ, Π) : V → V × (℘(V) × ℕ) be a valuation. We define UnderProg(Ξ, e) to hold for e = (v, w) ∈ E, if and only if:

1. Λ(v) ⪯ Λ(w), and

if Λ(v) = Λ(w) then:

2. if Λ(v) ≠ v then Π(v) ⊴_{Λ(v)} Π(w) ⊞ v, and

3. if Λ(v) = v then Π(v) ˜⊴_{Λ(v)} Π(w) ⊞ v and Π(v) = (∅, 0).

We say that Ξ is a locally under-progressive valuation for strategy σ if and only if UnderProg(Ξ, e) holds, for all e ∈ E_{σ}.

The following fact follows immediately from (5), (7), (8), and (10).

Proposition 5.3 Valuation Ω_{σ} is a locally under-progressive valuation for strategy σ.

In the following proposition we collect a couple of simple facts about locally under-progressive valuations and relations ⊴ and ˜⊴_{ℓ}.

Proposition 5.4 Let Ξ = (Λ, Π) : V → V × (℘(V) × ℕ) be a valuation.

1. If UnderProg(Ξ, (v, w)) holds and Λ(v) = Λ(w) then we have that Π(v) ˜⊴_{Λ(v)} Π(w) ⊞ v holds.

2. If UnderProg(Ξ, (v, w)) holds and Ξ(w) ⊴ Ξ(u) then we have that UnderProg(Ξ, (v, u)) holds.

In the next lemma we establish that a locally under-progressive valuation Ξ for a strategy σ is a witness that all plays starting from a vertex v and consistent with σ, have value at least as big as Ξ(v) with respect to the ⊴ order.

Lemma 5.5 If Ξ is a locally under-progressive valuation for a strategy σ then Ξ ⊴ Ω_{σ}.

Before we prove Lemma 5.5 we collect the following important properties of relations ⊴_{ℓ} and ˜⊴_{ℓ}.

Proposition 5.6 Let ℓ ∈ V, and B, C ∈ M(V), and k ∈ ℕ.

1. If max^{≤}(C) ≥ ℓ then

max^{≤}(C) ⪰ ℓ if and only if (B, k) ˜⊴_{ℓ} (B, k) ⊞ C.

2. If max^{≤}(C) ≠ ℓ then

max^{≤}(C) ≻ ℓ if and only if (B, k) ◁_{ℓ} (B, k) ⊞ C.

Proof. Assume first that max^{≤}(C) > ℓ. Then (B, k)˜◁_{ℓ} (B, k) ⊞ C holds if and only if B ≺_{ℓ} B ∪_{M} C holds, if and only if max^{≤}(C) ∈ R_{+} holds, if and only if max^{≤}(C) ≻ ℓ holds. Observe also, that (B, k) ◁_{ℓ} (B, k) ⊞ C holds if and only if B ≺_{ℓ} B ∪_{M} C holds, if and only if (B, k)˜◁_{ℓ} (B, k) ⊞ C holds.

Assume that max^{≤}(C) = ℓ. Then (B, k) ˜⊴_{ℓ} (B, k) ⊞ C holds because B =_{ℓ} B ∪_{M} C; and max^{≤}(C) ⪰ ℓ obviously holds.

Assume finally that max^{≤}(C) < ℓ. Then B =_{ℓ} B ∪_{M} C and therefore by definition of ⊴_{ℓ} we have that (B, k) ◁_{ℓ} (B, k) ⊞ C holds if and only if ℓ ∈ R_{−}, if and only if max^{≤}(C) ≻ ℓ. [Proposition 5.6]

Proof (of Lemma 5.5). Let v ∈ V, and let P be a play starting from v and consistent with σ. It suffices to show that Ξ(v) ⊴ Θ(P).

Let Ξ = (Λ, Π) : V → V × (M(V) × ℕ). First we show that Λ(v) ⪯ λ(P). From definition of a locally under-progressive valuation it follows that the values of Λ on vertices in play P are non-decreasing with respect to ⪯ order, so they are all equal on the cycle Cycle(P) of P. Hence, if we define ℓ to be the value of Λ on vertices in Cycle(P) then we have Λ(v) ⪯ ℓ. Therefore, it suffices to prove that ℓ ⪯ λ(P).

If ℓ ∉ Cycle(P) then applying the definition of a locally underprogressive valuation around the cycle of P we get that

Π(w) ⊴_{ℓ} Π(w) ⊞ Cycle(P),

for some vertex w ∈ Cycle(P). Note that from ℓ ∉ Cycle(P) it follows that λ(P) ≠ ℓ, and therefore clause 2. of Proposition 5.6, with C = Cycle(P), implies that λ(P) = max^{≤} (Cycle(P)) ⪰ ℓ.

If ℓ ∈ Cycle(P) then applying the definition of a locally underprogressive valuation around the cycle of P, together with clause 1. of Proposition 5.4, we get that

Π(w) ˜⊴_{ℓ} Π(w) ⊞ Cycle(P),

for some vertex w ∈ Cycle(P). Note that from ℓ ∈ Cycle(P) it follows that λ(P) ≥ ℓ, and therefore clause 1. of Proposition 5.6 implies that λ(P) = max^{≤} (Cycle(P)) ⪰ ℓ.

If Λ(v) ≺ λ(P) then we have Ξ(v) ◁ Θ(P) and we are done. Assume then that ℓ = Λ(v) = λ(P). We show that in this case Π(v) ◁_{ℓ} (π(P), #(P)), which immediately implies that Ξ(v) ⊴ Θ(P). By applying the definition of a locally under-progressive valuation along Prefix(P) we get

Π(v) ⊴_{ℓ} Π(ℓ) ⊞ Prefix(P),

and we also have Π(ℓ) = (∅, 0) because Λ(ℓ) = ℓ, and hence

Π(v) ⊴_{ℓ} (Prefix(P), |Prefix(P)|) =_{ℓ} (π(P), #(P)).

[Lemma 5.5]

5.4 Strategy improvement

Lemma 5.7 For every strategy σ for player ⊕, we have σ ⊑ Improve(σ).

Proof. It suffices to show that Ω_{σ} is a locally under-progressive valuation for Improve(σ). Then by Lemma 5.5 we get that Ω_{σ} ⊴ Ω_{Improve(σ)}, i.e., that σ ⊑ Improve(σ).

We argue that Ω_{σ} is a locally under-progressive valuation for the strategy Improve(σ). By Proposition 5.3 we have that Ω_{σ} is a locally under-progressive valuation for σ. Therefore, it suffices to check that for all v ∈ M_{⊕}, the predicate UnderProg holds for Ω_{σ} along the edge (v, [Improve(σ)](v)). Note that by definition of the Improve operator we have

Ω_{σ}([Improve(σ)](v)) ⊵ Ω_{σ}(σ(v)),

for all v ∈ M_{⊕}. Note that the UnderProg predicate holds for Ω_{σ} along the edges (v, σ(v)), for all v ∈ M_{⊕}, because Ω_{σ} is a locally progressive valuation for σ. It then follows from clause 2. of Proposition 5.4 that the UnderProg predicate for Ω_{σ} holds along every edge (v, [Improve(σ)](v)), for all v ∈ M_{⊕}. [Lemma 5.7]

5.5 Maximum strategies

Lemma 5.8 For every strategy σ for player ⊕, the following are equivalent:

1. strategy σ is not a maximum element in (Strategies_{⊕}, ⊑),

2. Improve(σ) ≠ σ,

3. Improve(σ) ⋢ σ.

Locally over-progressive valuation. Let Ξ = (Λ, Π) : V → V ×(℘(V)×ℕ) be a valuation. We define OverProg(Ξ, e) to hold for e = (v, w) ∈ E if and only if:

1. Λ(v) ⪰ Λ(w), and

if Λ(v) = Λ(w) then:

2. if Λ(v) ≠ v then Π(v) ⊵_{Λ(v)} Π(w) ⊞ v, and

3. if Λ(v) = v then Π(v) ˜⊵_{Λ(v)} Π(w) ⊞ v and Π(v) = (∅, 0).

We say that Ξ is a locally over-progressive valuation for strategy τ for player ⊖ if and only if OverProg(Ξ, e) holds for all e ∈ E_{τ}.

Valuation ℧_{σ}. For every strategy τ ∈ Strategies_{⊖} we define ℧_{τ} ∈ Valuations in the following way:

℧_{τ}(v) = max^{⊴}{ Θ(P) : P ∈ Plays_{τ}(v) },

where Plays_{τ}(v) is the set of plays starting from vertex v and consistent with τ.

In the following lemma we show that a locally over-progressive valuation Ξ for a strategy τ is a witness that all plays starting from vertex v and consistent with τ have value at most as big as Ξ(v) with respect to the ⊴ order on valuations.

Lemma 5.9 If Ξ is a locally over-progressive valuation for a strategy τ then ℧_{τ} ⊴ Ξ.

The above lemma is proved similarly to Lemma 5.5, using the following simple facts instead of Proposition 5.4.

Proposition 5.10 Let Ξ = (Λ, Π) : V → V ×(℘(V)×ℕ) be a valuation.

1. If OverProg(Ξ, (v, w)) holds and Λ(v) = Λ(w) then we have that Π(v) ˜⊵_{Λ(v)} Π(w) ⊞ v holds.

2. If OverProg(Ξ, (v, w)) holds and Ξ(w) ⊵ Ξ(u) then we have that OverProg(Ξ, (v, u)) holds.

Proof (of Lemma 5.8). 1 ⇒ 2. We claim that it suffices to argue that if Improve(σ) = σ then Ω_{σ} is a locally over-progressive valuation for \overline{σ}. By Lemma 5.9 we then have

℧\overline{σ} ⊴ Ω_{σ}.  (12)

This, however, implies that κ ⊑ σ for all strategies κ for player ⊕. It is so because Ω_{κ} ⊴ ℧_{τ} holds for all strategies κ and τ, hence in particular Ω_{κ} ⊴ ℧\overline{σ} holds, so altogether we get Ω_{κ} ⊴ ℧\overline{σ} ⊴ Ω_{σ}.

We argue that Ω_{σ} is a locally over-progressive valuation for \overline{σ}. By Proposition 5.1 we know that Prog predicate for Ω_{σ} holds along all edges (v, w) ∈ E, such that σ(v) = w or \overline{σ}(v) = w. Therefore, it suffices to check that the OverProg predicate for Ω_{σ} holds along all edges (v, w) ∈ E, such that v ∈ M_{⊕}. Note that from Improve(σ) = σ it follows that

Ω_{σ}(σ(v)) ⊵ Ω_{σ}(w),

for all v ∈ M_{⊕} and w ∈ succ(v), and hence by clause 2. of Proposition 5.10 we get that OverProg(Ω_{σ}, (v, w)) holds.

2 ⇒ 3. Note that if Improve(σ) ≠ σ then for some v ∈ M_{⊕}, the predicate Prog does not hold for Ω_{σ} along the edge (v, [Improve(σ)](v)). Therefore, by Lemma 5.2 we have that Ω_{σ} ≠ Θ_{Improve(σ)\overline{Improve(σ)}}, i.e., by (11) we have that Ω_{σ} ≠ Ω_{Improve(σ)}. Recall that ⊴ is a partial order on the set of valuations, hence it must be the case that Ω_{Improve(σ)} ⋬ Ω_{σ} because by Lemma 5.7 we have Ω_{σ} ⊴ Ω_{Improve(σ)}.

3 ⇒ 1. Straightforward. [Lemma 5.8]

5.6 Proving the postulates P1., P2., I1., and I2.

P1. Lemmas 5.7 and 5.8 imply that after a finite number of iterations of the strategy improvement algorithm it must be the case that Improve(σ) = σ. By Lemma 5.8 such a strategy σ is a maximum element in the pre-order (Strategies_{⊕}, ⊑).

P2. Let σ be a maximum element in (Strategies_{⊕}, ⊑). Then from Lemma 5.8 it follows that Improve(σ) = σ. By definition of Ω_{σ}, strategy σ is a winning strategy for player ⊕ from the set

W_{⊕}^{σ} = { v ∈ V : Ω_{σ}(v) = (ℓ, (B, k)) and ℓ ∈ R_{+} }.

We claim that W_{⊕}^{σ} is the winning set for player ⊕. It suffices to argue that player ⊖ has a winning strategy from the set V \ W_{⊕}^{σ}. Note that

V \ W_{⊕}^{σ} = { v ∈ V : Ω_{σ}(v) = (ℓ, (B, k)) and ℓ ∈ R_{−} },

and by (12) we have ℧\overline{σ} ⊴ Ω_{σ}. This means, however, that \overline{σ} is a winning strategy for player ⊖ from V \ W_{⊕}^{σ}.

I1. Immediate from Lemmas 5.7 and 5.8.

I2. Immediate from Lemma 5.8.

6 Efficient implementation

We are given a graph G = (V, E) with a linear order ≤ on vertices, and a vertex t ∈ V, such that:

for every v ∈ V, there is a path from v to t in G,  (13)

and

for every cycle C in G, we have that max^{≤}(C) ⪰ t.  (14)

Every edge (v, w) ∈ E has the weight ({v} ∩ V_{>t}, 1) ∈ ℘(V_{>t}) × ℕ. The weights are ordered by ⊴_{t} and added to each other with ⊞. The task is for all vertices v ∈ V, to determine (the weight of) a shortest path from v to t in G. For all v ∈ V, let Σ(v) ⊆ ℘(V_{>t}) be the set of vertices with priority bigger than t occurring in a shortest path from v to t in G.

We use the following algorithm to compute the shortest paths.

Shortest paths

1. E := E \ ({t} × V )

  2. for all r ∈ V_{>t} in ≤-descending order

3. if r ∈ R_{+} then

  4.  W := { w ∈ V : there is a path from w to t in (V \ r, E) }

5. E := E \ ((W ∪ {r}) × (V \ W))

6. if r ∈ R_{−} then

  7.  U := { u ∈ V : there is a path from u to r in (V, E) }

8. E := E \ ((U \ {r}) × (V \ U))

  9. if t ∈ R_{+} then find longest distances from every vertex to t
  10. if t ∈ R_{−} then find shortest distances from every vertex to t

The algorithm works as follows. First we remove edges going out of t since we are only interested in paths from all vertices to t (line 1.). Then in every iteration of the for all loop (lines 2.–8.) we remove edges that cannot possibly belong to a shortest path from a vertex v to t. After the for all loop has been executed, from every vertex there are only paths to t containing the same set of vertices in V_{>t} as a shortest path. Therefore, in order to find shortest paths from every vertex to t it suffices to find longest distances to t if t ∈ R_{+}, and shortest distances to t if r ∈ R_{−} (lines 9. or 10.). Finding longest distances in the case when t ∈ R_{+} can be done efficiently because in this case the graph is acyclic.

Let us analyze the first iteration of the for all loop, i.e., let r = max^{≤}(V) and let r > t. There are two cases to consider: r ∈ R_{+} and r ∈ R_{−}.

Suppose that r ∈ R_{+}. Then for all v ∈ V, by the definition of ⊴_{t} and by the maximality of r with respect to ≤, a shortest path from v to t should avoid visiting r if possible. More formally, for every v ∈ V, we have that:

r ∉ Σ(v) if and only if there is a path from v to t in G in which r does not occur.

(15)

Therefore, the set W computed in line 4. contains all vertices v ∈ V, such that r does not occur on a shortest path from v to t. On the other hand, the set V \W consists of vertices from which a visit to r is “unavoidable” on a shortest path to t. It is then not hard to see that by removing in line 5. all the edges leading from W to V \ W we only disconnect paths which cannot be shortest paths to t. Let G′ be the graph after removing edges in line 5. Therefore, for every v ∈ V, we have that:

G′ contains a shortest path from v to t in G.  (16)

Moreover, after performing the deletion of edges in line 5., no path from W to t contains r, and all the paths from V \ W to t contain r. In other words, we have that:

if r ∈ Σ(v) then r occurs on every path from v to t in G′,  (17)

and

if r ∉ Σ(v) then r does not occur on any path from v to t

in G′. (18)

Observe also, that by performing the deletion in line 5. we disconnect all cycles containing r, because then r can only be reached from vertices in V \ W, and only vertices in W are reachable form r, i.e., we have:

there is no cycle in G′ containing r.  (19)

We omit considering the other case, i.e., r = max^{≤}(V_{>t}) ∈ R_{−}. Instead, motivated by claims (16), (17), (18), and (19), established above for r = max^{≤}(V_{>t}) ∈ R_{+}, we argue that the following invariant is maintained by all iterations of the for all loop.

For x ∈ V_{>t}, let G(x) be the graph after the body of for all loop has been performed for all r ∈ V_{>t}, such that r > x.

Proposition 6.1 Let r ∈ V_{>t}. For all s ∈ V_{>t}, such that s > r, and for all v ∈ V, we have:

1. G(r) contains a shortest path from v to t in G,

2. if s ∈ Σ(v) then s occurs on every path from v to t in G(r),

3. if s ∉ Σ(v) then s does not occur on any path from v to t in G(r),

4. there is no cycle in G(r) containing s.

Proof. We prove the proposition by induction on r. Claims 1.–4. hold trivially for r = max^{≤}(V). Assume as the induction hypothesis that clauses 1.–4. hold for some r ∈ V_{>t}. We show then, that clauses 1.–4. hold for r′ = max^{≤}(V_{<r}), by analyzing what happens when the body of the for all loop is performed. We consider two cases.

• r ∈ R_{+}.

Note that by clauses 1.-3. of the induction hypothesis, and by definition of ⊴_{t}, we have:

r ∈ Σ(v) if and only if r occurs on every path from v to t in G(r).

With this analogue of claim (15), the arguments needed to prove clauses 1.–4. for r′ are the same as the ones we have used to establish claims (16)–(19).

• r ∈ R_{−}.

Note that by clauses 1.-3. of the induction hypothesis, and by definition of ⊴_{t}, we have:

r ∈ Σ(v) if and only if r occurs on some path from v to t in

G(r). (20)

We argue that:

there is no cycle in G(r) containing r.  (21)

Suppose the contrary is the case, i.e., that there is a cycle C containing r in G(r). Then by clause 4. of the induction hypothesis we have that max^{≤}(C) = r, which together with r ∈ R_{−} implies that max^{≤}(C) ≺ t, a contradiction with (14). Note that (21) establishes clause 4. for r′.

A corollary of (21) is that if r ∈ Σ(v) then all paths from v to t and containing r are simple paths. Moreover, by clause 1. of the induction hypothesis there is a path from r to t in G(r), and hence, claim (20) implies the following:

r ∈ Σ(v) if and only if there is a path from v to r in

G(r). (22)

Therefore, the set U computed in line 7. contains all vertices v ∈ V, such that r occurs on a shortest path from v to t, and the set V \U contains all vertices from which a visit to r is not possible on a shortest path to t. Observe, that by removing edges leading from U \{r} to V \U we only disconnect paths which cannot be shortest paths to t. This establishes clause 1. for r′.

Note also, that by definition of U no path from V \ U to t contains r, and after deletions of edges in line 8. we have that all paths from U to t contain r. This establishes clauses 3. and 2. for r′.

[Proposition 6.1]

Theorem 6.2 An improvement step of our discrete strategy improvement algorithm can be performed in time O(n · m).

7 Time complexity

In the analysis of the running time of a strategy improvement algorithm there are two parameters of major interest:

1. the time needed to perform a single strategy improvement step,

2. the number of strategy improvement steps needed.

By Theorem 6.2 our discrete strategy improvement algorithm achieves a satisfactory bound on the former parameter.

A satisfactory analysis of the latter parameter is missing in our work. Despite the long history of strategy improvement algorithms for stochastic and payoff games [9, 4, 16] very little is known about the number of strategy improvement steps needed. The best upper bounds are exponential [4, 16] but to our best knowledge no examples are known which require more than linear number of improvement steps. We believe that our purely discrete description of strategy improvement gives new insights into the behaviour of the algorithm in the special case of parity games. The two long standing questions: whether there is a polynomial time algorithm for solving parity games [8], and, more concretely, whether a strategy improvement algorithm for parity games terminates in polynomial time [4, 16], remain open. Below we discuss some disjoint observations we have come up with so far, and some questions which we believe are worth pursuing.

Proposition 7.1 For every initial strategy, there is a strategy improvement policy of length at most n. Moreover, there is such a policy switching exactly one edge in every improvement step.

Proof. Let us fix a strategy κ which is a maximum element in the partial order (Strategies_{⊕}, ⊑). Note that it suffices to show that for every strategy σ which is not a maximum element in (Strategies_{⊕}, ⊑), there is an improvement (v, w) ∈ E for σ, such that w = κ(v).

Claim 7.2 If I ⊆ E contains no improvement for σ then Switch_{I}(σ) ⊑ σ.

We argue how the proposition follows from the claim. Suppose for the sake of contradiction that for all v ∈ M_{⊕}, such that σ(v) ≠ κ(v), we have Ω_{σ}(κ(v)) ⊴ Ω_{σ}(σ(v)). Let I = { (v, κ(v)) : v ∈ M_{⊕} and σ(v) ≠ κ(v) }. Note that Switch_{I}(σ) = κ. Hence by Claim 7.2 we get that κ ⊑ σ which contradicts the assumption that κ is a maximum element in (Strategies_{⊕}, ⊑) and that σ is not.

Proof (of Claim 7.2). Note that for all (v, w) ∈ I we have that

Ω_{σ}(w) ⊴ Ω_{σ}(σ(v)).  (23)

By Proposition 5.1 we have that Prog(Ω_{σ}, e) holds for all edges e in the graph of strategies σ and \overline{σ}. From (23) and from clause 2. of Proposition 5.10 it follows that OverProg(Ω_{σ}, e) holds for all edges e in the graph of strategies Switch_{I}(σ) and \overline{σ}. Let σ′ = Switch_{I}(σ). Note that in the (one-player) game G_{σ′} we have ℧\overline{σ} = Θ_{σ′\overline{σ}}. Therefore, by applying Lemma 5.9 to G_{σ′} we get that Θ_{σ′\overline{σ}} ⊴ Ω_{σ}. Note that by definition of Ω_{σ′} we have that Ω_{σ′} ⊴ Θ_{σ′\overline{σ}}, and hence we get Ω_{σ′} ⊴ Ω_{σ} which concludes the proof. [Claim 7.2] [Proposition 7.1]

This contrasts with an algorithm for solving parity games based on progress measures [11], for which there are families of examples on which every policy requires an exponential number of steps.

Melekopoglou and Condon [14] exhibit families of examples of simple stochastic games for which several natural strategy improvement policies switching only one switchable vertex in every strategy improvement step have exponential length.

Problem 7.3 Are there families of examples of parity games for which there exist strategy improvement policies of super-polynomial length?

Examples of Melekopoglou and Condon [14] are Markov decision processes, i.e., one-player simple stochastic games [3]. It is an open question whether the strategy improvement algorithm using the standard policy, i.e., switching all switchable vertices in every strategy improvement step, works in polynomial time for one-player simple stochastic games [14]. In contrast, our discrete strategy improvement algorithm terminates in polynomial time for one-player parity games.

Proposition 7.4 The discrete strategy improvement algorithm terminates after O(n^{3}) strategy improvement steps for one-player parity games.

Most algorithms for solving parity games studied in literature have roughly O((n/d)^{d}) or O((n/d)^{d/2}) worst-case running time bounds, where d is the number of different priorities assigned to vertices. The best upper bound we can give at the moment for the number of strategy improvement steps needed by our discrete strategy improvement algorithm is the trivial one, i.e., the number of different strategies for player 0, which can be 2^{Ω(n)}.

Proposition 7.5 The discrete strategy improvement algorithm terminates after ∏_{v∈V_{0}} out-deg(v) many strategy improvement steps.

There is, however, a variation of the strategy improvement algorithm for parity games, for which the number of strategy improvement steps is bounded by O((n/d)^{d}).

Proposition 7.6 There is a strategy improvement algorithm for parity games for which all policies have length O((n/d)^{d}), and every strategy improvement step can be performed in n^{O(1)} time.

Note that in every strategy improvement step the current valuation Ω_{σ} strictly improves with respect to ⊴ in at least one vertex. We say that a strategy improvement step is substantial if in the current valuation the loop value for some vertex strictly improves. Observe that there can be at most O(n^{2}) substantial strategy improvement steps. It follows that in search for superpolynomial examples one has to manufacture gadgets allowing long sequences of non-substantial strategy improvement steps.

We have collected a little experimental evidence that in practice most improvement steps are non-substantial. There are few interesting scalable families of hard examples of parity games known in literature. Using an implementation of our discrete strategy improvement algorithm by Schmitz and Vöge [17] we have run some experiments on families of examples taken from [2] and from [11], and on a family of examples mentioned in [11] which make Zielonka’s version [22] of the McNaughton’s algorithm [12] work in exponential time. For all these families only linear number of strategy improvement steps were needed and, interestingly, the number of non-substantial strategy improvement steps was in all cases constant, i.e., not dependent of the size of the game graph.

We conclude with a number of questions to pursue.

Problem 7.7 Does our discrete algorithm, with a policy switching in every strategy improvement step a maximal set of improvements (i.e., switching all switchable vertices), terminate in polynomial time? If not, exhibit families of examples for which there are policies of exponential length.

Problem 7.8 Are there polynomial time computable heuristics for constructing policies of polynomial length?

Problem 7.9 Define and study other partial orders on the set of strategies and other strategy improvement operators.

Problem 7.10 Develop other algorithms than a strategy improvement algorithm for solving the optimization problem of solving cycle-domination games with respect to a partial order on the set of strategies.

References

[1] A. Browne, E. M. Clarke, S. Jha, D. E. Long, and W. Marrero. An improved algorithm for the evaluation of fixpoint expressions. Theoretical Computer Science, 178(1–2):237–255, May 1997. A preliminary version appeared in Proceedings of CAV’94, volume 818 of LNCS, Springer-Verlag.

[2] Nils Buhrke, Helmut Lescow, and Jens Vöge. Strategy construction in infinite games with Streett and Rabin chain winning conditions. In Tiziana Margaria and Bernhard Steffen, editors, Tools and Algorithms for Construction and Analysis of Systems, Second International Workshop, TACAS ’96, volume 1055 of LNCS, pages 207–224, Passau, Germany, 27–29 March 1996. Springer-Verlag.

[3] Anne Condon. The complexity of stochastic games. Information and Computation, 96:203–224, 1992.

[4] Anne Condon. On algorithms for simple stochastic games. In Jin-Yi Cai, editor, Advances in Computational Complexity Theory, volume 13 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 51–73. American Mathematical Society, 1993.

[5] Thomas H. Cormen, Charles E. Leiserson, and Ronald L. Rivest. Introduction to Algorithms. MIT Press/McGraw-Hill, 1990.

[6] A. Ehrenfeucht and J. Mycielski. Positional strategies for mean payoff games. Int. Journal of Game Theory, 8(2):109–113, 1979.

[7] E. A. Emerson and C. S. Jutla. Tree automata, mu-calculus and determinacy (Extended abstract). In 32nd Annual Symposium on Foundations of Computer Science, pages 368–377, San Juan, Puerto Rico, 1–4 October 1991. IEEE Computer Society Press.

[8] E. A. Emerson, C. S. Jutla, and A. P. Sistla. On model-checking for fragments of μ-calculus. In Costas Courcoubetis, editor, Computer Aided Verification, 5th International Conference, CAV’93, volume 697 of LNCS, pages 385–396, Elounda, Greece, June/July 1993. Springer-Verlag.

[9] A. Hoffman and R. Karp. On nonterminating stochastic games. Management Science, 12:359–370, 1966.

[10] Marcin Jurdziński. Deciding the winner in parity games is in UP ∩ co-UP. Information Processing Letters, 68(3):119–124, November 1998.

[11] Marcin Jurdziński. Small progress measures for solving parity games. In Horst Reichel and Sophie Tison, editors, STACS 2000, 17th Annual Symposium on Theoretical Aspects of Computer Science, Proceedings, volume 1770 of Lecture Notes in Computer Science, pages 290–301, Lille, France, February 2000. Springer-Verlag.

[12] Robert McNaughton. Infinite games played on finite graphs. Annals of Pure and Applied Logic, 65(2):149–184, 1993.

[13] Nimrod Megiddo. Towards a genuinely polynomial algorithm for linear programming. SIAM Journal on Computing, 12:347–353, 1983.

[14] Mary Melekopoglou and Anne Condon. On the complexity of the policy improvement algorithm for Markov decision processes. ORSA Journal of Computing, 6(2):188–192, 1994. Operations Research Society of America.

[15] A. W. Mostowski. Games with forbidden positions. Technical Report 78, University of Gdańsk, 1991.

[16] Anuj Puri. Theory of Hybrid Systems and Discrete Event Systems. PhD thesis, Electronics Research Laboratory, College of Engineering, University of California, Berkeley, December 1995. Memorandum No. UCB/ERL M95/113.

[17] Dominik Schmitz and Jens Vöge. Implementation of a strategy improvement algorithm for finite-state parity games (Extended abstract). Fifth International Conference on Implementation and Application of Automata, CIAA 2000, Proceedings, London, Ontario, Canada, July 2000. Available at

http://www-i7.informatik.rwth-aachen.de/~voege/omega/.

[18] Helmut Seidl. Fast and simple nested fixpoints. Information Processing Letters, 59(6):303–308, September 1996.

[19] Colin Stirling. Local model checking games (Extended abstract). In Insup Lee and Scott A. Smolka, editors, CONCUR’95: Concurrency Theory, 6th International Conference, volume 962 of LNCS, pages 1– 11, Philadelphia, Pennsylvania, 21–24 August 1995. Springer-Verlag.

[20] Wolfgang Thomas. On the synthesis of strategies in infinite games. In 12th Annual Symposium on Theoretical Aspects of Computer Science, volume 900 of LNCS, pages 1–13, Munich, Germany, 2– 4 March 1995. Springer-Verlag.

[21] Jens Vöge and Marcin Jurdziński. A discrete strategy improvement algorithm for solving parity games (Extended abstract). In E. A. Emerson and A. P. Sistla, editors, Computer Aided Verification, 12th International Conference, CAV 2000, Proceedings, volume 1855 of Lecture Notes in Computer Science, pages 202–215, Chicago, IL, USA, July 2000. Springer-Verlag.

[22] Wiesław Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200:135–183, 1998.

[23] Uri Zwick and Mike Paterson. The complexity of mean payoff games on graphs. Theoretical Computer Science, 158:343–359, 1996.

Recent BRICS Report Series Publications

RS-00-48 Marcin Jurdziński and Jens Vöge. A Discrete Stratety Improvement Algorithm for Solving Parity Games. December 2000. 31 pp. Extended abstract appears in Emerson and Sistla, editors, Computer-Aided Verification: 11th International Conference, CAV ’00 Proceedings, LNCS 1855, 2000, pages 202–215.

RS-00-47 Lasse R. Nielsen. A Denotational Investigation of Defunctionalization. December 2000. 50 pp. Presented at 16th Workshop on the Mathematical Foundations of Programming Semantics, MFPS ’00 (Hoboken, New Jersey, USA, April 13–16, 2000).

RS-00-46 Zhe Yang. Reasoning About Code-Generation in Two-Level Languages. December 2000.

RS-00-45 Ivan B. Damgård and Mads J. Jurik. A Generalisation, a Simplification and some Applications of Paillier’s Probabilistic Public-Key System. December 2000. 18 pp. Appears in Kim, editor, Fourth International Workshop on Practice and Theory in Public Key Cryptography, PKC ’01 Proceedings, LNCS 1992, 2001, pages 119–136. This revised and extended report supersedes the earlier BRICS report RS-00-5.

RS-00-44 Bernd Grobauer and Zhe Yang. The Second Futamura Projection for Type-Directed Partial Evaluation. December 2000. To appear in Higher-Order and Symbolic Computation. This revised and extended report supersedes the earlier BRICS report RS-99-40 which in turn was an extended version of Lawall, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’00 Proceedings, 2000, pages 22–32.

RS-00-43 Claus Brabrand, Anders Møller, Mikkel Ricky Christensen, and Michael I. Schwartzbach. PowerForms: Declarative Client-Side Form Field Validation. December 2000. 21 pp. Appears in World Wide Web Journal, 4(3), 2000.

RS-00-42 Claus Brabrand, Anders Møller, and Michael I. Schwartzbach. The <bigwig> Project. December 2000. 25 pp.