Introduction to Infinite Games and Winning Strategies

Introduction to Infinite Games Chapter 2 in Automata, Logic and infinite games Jonathan Cederbaum

Infinite Games - Intro 2 Players Game board is a (possibly infinite) directed Graph We Define: How the games is played Who wins Determinacy, Winning Strategies, Forgetful Strategies, Memoryless Strategies Fundamental Results

Games Game: Arena: Successors of v in V: vE := { v V | (v, v ) E } May be infinite 2 Players: Player 0, Player 1 Notation: Player , Player where {0, 1} Note: (V, E) not necessarily bipartite Arena + Winning Conditions (V0, V1, E) (V = V0 U V1, E contained in VxV)

A Play Informal Explanation The token is placed on some Initial vertex v. If v is a 0-Vertex, its Player 0 s turn. Otherwise, it s a 1-Vertex, and Player 1 s turn. On each turn, the player moves the token to some successor v in vE. Note: a player may play mutiple turns in concession. The game goes on infinitely or until reaching a vertex without successors, a Dead End. vE = .

A Play Formal Definition A Prefix of a Play defined as expected

Arena - Example Player 0 Player 1

Games & Winning Sets A Game G is a pair: (A, Win) A is the arena Win V is the Winning Set. Player 0 is the winner of a play in the game G iff: is a finite play: = v0v1 vrand vris a 1-vertex where Player 1 can t move anymore (Dead end). is an infinite play and Win Note: Player 1 wins if Player 0 doesn t. In an Initialized Game (G, vI) all plays start in vI

Winning Conditions How do we define the winning set ( Win ) ? Use acceptance conditions of w-automata, to define a winning play. Problem: the graph may be infinite, might not even have recurring states.. Solution: color each vertex (Finite set of colors), Apply acceptance conditions on the color sequence induced by the play.

Winning Conditions - Cont A Coloring Function: : V C C is some finite set of colors Given a play: = v0v1v2 Define the play s coloring: ( )= (v0) (v1) (v2) C (the color set) is viewed as the state set of a finite w- automaton. Acc is the acceptance condition for this automaton. (As defined in the previous lecture) buchi, muller, Rabin, Street, etc. W (Acc) : Defines the winning set to be all plays where ( ) is accepted according to Acc. note dependence on

Acceptance Conditions Buchi: (acc=F P(C)) W (Acc) iff Inf( ( )) F Muller: (acc=F 2C). W (Acc) iff Inf( ( )) F Max-Parity: C is some set of integers. W (Acc) iff Max(Inf( ( ))) is Even Additional Acceptance Conditions: Rabin, Rabin Chain Condition, Street etc. A game is a regular game if its winning set equals W (Acc) for some , and some Acc from above. Notation: we write (A, , Acc) instead of (A,W (Acc))

Arena - Example A = (V0, V1,E, ) (colored arena) C = {1, 2, 3, 4} Player 0 Player 1 - No dead ends -Choose Mullner accepting conditions given by: - F = {{1, 2}, {1, 2, 3, 4}}. -Example play 1: - = z6z3z2z4z2z4z6z5(z2z4) - ( ) = 23121224(12) -Inf( ( )) = {1, 2} F -So is a winning play for player 0 - ' = (z2z4z6z3) - ( ) = (1223) -Inf( ( )) = {1, 2, 3} F -So is a winning play for player 1

Fundamental Questions I Given an initialized game can one player win regardless of what the other does? In this case we say the game is determined. We will formalize this question by introducing the notions of a strategy, and a winning strategy. The answer is yes, every (regular) game is determined (this result will be proved in chapter 6).

Fundamental Questions II Given a final graph, can we compute who the winner is? Can compute it efficiently? This and more in chapter 7, stay tuned. Complexity of determining the winner depends on the type of the game (The winning condition).

Fundamental Questions III What does the winning strategy look like? A general strategy tells the player the next move to make given all previous moves . When might we have a winning strategy that requires remembering a bounded number of moves - a Forgetful Strategy. When can we decide the next move given just the current vertex - a Memoryless Strategy. Answer: regular games have Forgetful winning strategies. Parity games have Memoryless winning strategies.

Strategies A is an arena. {0, 1}. f : V*V V - a partial function. A prefix of a play = v0v1 vrconforms with f if for every i, where 0 i r-1 and vi V , the function f is defined at v0 viand: vi+1= f (v0 vi). A Play conforms with f if all its prefixes conform with f . f is a strategy for Player on U V if it is defined for every prefix of a play which starts in U, conform with it, and doesn t end in a Dead End of Player . When U is a singleton {v} we say f is a strategy for Player on v. f is a Winning Startegy for Player on U if all plays which conform to f and start in U are wins for Player .

Strategies - Cont Player wins a game G on U V if he has a winning strategy on U. When (G, vI) is an initialized game, we say Player wins it if he wins G on the singleton set {v}. Given a game G, we define the winning region for Player , denoted W (G), or W for short, to be the set of all vertices v such that Player 0 wins (G, v). Remark: For any game G, Player wins G on W (G). Since if Player wins on each group A T, then Player wins on U A.

Strategy - Example A = (V0, V1,E, ) (colored arena) C = {1, 2, 3, 4} Mullner accepting conditions given by: - F = {{1, 2}, {1, 2, 3, 4}}. Player 0 Player 1 -f1(yz0) = z0 f1(yz4) = z6 f1(yz3) = z2 is a winning strategy for Player 1 on W1= {z0, z1}. (or = z1) (or = z1) -Player 0 must move z2to z4 -so z2, z4 appear infinite times. -player 1 should not always choose z4->z2 -Player 1 then should choose z4->z6occasionally. -Player 0 wins iff on z6he alternates between z3and z5.

Strategy - Example A = (V0, V1,E, ) (colored arena) C = {1, 2, 3, 4} Mullner accepting conditions given by: - F = {{1, 2}, {1, 2, 3, 4}}. Player 0 Player 1 -To summarize, the following is a winning strategy for Player 0, on W0 = {z2, z3, z4, z5, z6}. -z4if V z2 -z3if V z5z2z4(z2z4) z6 -z5if V z3z2z4(z2z4) z6 -z3 if (V \ {z3, z5}) z6

Reduction of Muller Games to Parity Games Note: For every regular game (A, , Acc) there exists a Muller winning condition Acc such that (A, , Acc) and (A, , Acc ) have the same winning regions. e.g for Buchi games define: F := {G 2C| G F = }. Result: For every Muller game G=(A, , F) there exists a (max) parity game G =(A , , Acc ) and an injection r : V V such that every (unique) play in G starting in v V induces a (unique) play in G starting in r(v), and Player wins in G iff he wins in G . this result explains why we focus on Parity Games in chapter 6 & 7 Remainder: Muller: (acc=F 2C). W (Acc) iff Inf( ( )) F Max-Parity: C is some set of integers. W (Acc) iff Max(Inf( ( ))) is Even

The Construction - Vertices V = Vx

The Construction - Edges Connect vertex (v, q) to vertex (v , q ) if: 1. v vE 2. q = (v', q) q is the updated qafter seeing color c = (v ) is the memory update function. 3 cases for updating q: Case #1: (color c appears before ): q = xcy z q = x yzc Case #2: (c appears after ): q = x ycz q = xy zc Case #3: (c not in q): (q = q) q = qc

The Construction Initial Vertex r(v) := (v, (v))

The Construction Coloring Function Given F, that defines the Muller condition in A: otherwise If y F F = {{b}}

Muller to Parity Full Example For every play in A, there is a corresponding play in A , for example: = z1z2z0z1z2 ( ) = abaab (winning for Player 0) = (z1, a)(z2, ab)(z0, ba)(z1, b a)(z2, ab)(z2, a b) ( ) = 133132 (winning for Player 0) Player 0 Player 1 F = {{b}}

Correctness of Construction Theorem: For every Muller game (A, , F) there exists a (max) parity game (A , , Acc ) and a function r : V V such that for every v V, Player wins ((A, , F), v) if and only if Player wins ((A , , Acc ), r(v)). = v0v1 V infinite play in A. the corresponding play in A p1( ) = p2( ) = q0q1. . . F := Inf( ( )) Argument 1: from some point only c F appear on the right of the . From some i colors not in F do not appear in . at some j > i we have seen again all colors in F. at that point colors in F appear on the right side of the string. from step j+1 only colors in F appear right of the . conclusion: |yi| |F| from some i Argument 2: There are infinite times where all colors in F are right of the . since the left most color in F must appear at some point conclusion: there are infinite times k where | yk| = |F| and Thus the largest length of y that appears infinitely often is |F| and y=F > the highest color that appears infinite times is: 2*|F| if y F (even) 2*|F| - 1 if not (odd) Summary: is winning for player 0 in A iff is winning for him in A . So Player 0 Wins (A, v) iff he wins (A , r(v)) where qi= xi yiis defined by: q0:= (v0) and qi+1:= (vi+1, qi) for i .

Determinacy In all examples so far, the Winning regions for Player 0 and Player 1 partition V. When a game has this property we say it is determined. Theorem: Every parity game is determined. proven in chapter 6. Corollary: Every regular game is determined (by the equivalence result provenearlier).

Forgetfull & Memoryless Strategies Player 0 Player 1 A = (V0, V1,E, ) (colored arena) C = {1, 2, 3, 4} Mullner accepting conditions given by: - F = {{1, 2}, {1, 2, 3, 4}}. To win, if the token is placed in z6, Player 0 must alternate between choosing z3and z5 Player 0 has to remember 1 bit. We saw that this is enough. We showed a Forgetfull strategy for Player 0. Player 1 just moves z0to zo. This is a Memoryless strategy.

Forgetful Strategies - Definition A Strategy f is said to be forgetful (finite memory) if there exists: A finite set M An element mI M (the initial memory value) A function : V M M (memory update function) A function g: V M V (next move function) such that when = v0v1 vris a prefix of a play, in the domain of f , and the sequence: m0,m1,...,mris determined by m0=mIand mi+1= (vi+1,mi), then f ( )=g(vr, mr). A forgetful strategy where |M|=1 is called Memoryless. notation: f :V V

Memoryless & Forgetful Strategy Example Player 1 memoryless Strategy: M = {m} g(z0,m) = z0 g(z3,m) = g(z4,m) = z2 is winning on {z0, z1} A = (V0, V1,E, ) (colored arena) C = {1, 2, 3, 4} Mullner accepting conditions given by: - F = {{1, 2}, {1, 2, 3, 4}}. Player 0 forgetfull Strategy: M = {3, 4} mI= 3 Player 0 Player 1 Winning On {z2, z3, z4, z5, z6}.

Forgetful Strategies Cont. Player wins a game G forgetful when he has a (maybe different) forgetful winning strategy for each point in his winning region. winning a game G memoryless is defined accordingly. Exercise: Give an example for a game G such that Player 0 wins forgetful on each {v} for v W0, but he has no (single) forgetful winning strategy on W0. this is in contrast to the result on regular strategies. The Lemma following shows that the statement is true for memoryless strategies (under certain conditions).

Lemma Let G=(A, Win) by any game such that: 1. V (vertex set) is countable 2. V*Win Win (adding a finite prefix) 3. Win/V* Win (removing a finite prefix) Win/V := { V | w V with w Win } Let U be a set of vertices that Player has a memoryless winning strategy on each u U. Then Player has a memoryless winning strategy on (all) U. Condition 2 & 3 are satisfied for every regular game since Inf(X( )) is unaffected.

Lemma Proof (construction) goal: construct a memoryless winning strategy on U. for every u U, Let f u: V V be a memoryless winning strategy for Player on u. wlog assume the domain of f u , denoted Duis minimal. Let < be a well ordering on U (V is countable) Define For each v D, let u(v) be the minimal vertex in U s.t the strategy for u is defined for v. Define strategy: f (v) := f u(v)(v) choose the minimal strategy defined for v D = u D u = min ( ) u v v D u u

Lemma Proof (correctness) Need to show that f (v) := f u(v)(v) is a winning strategy on U. Let = v0v1 be a play, starting in U and conforms with f . In each -vertex vj in , Player chooses f u(vj) Let Then from i on, f = f u(vi) vivi+1 is a suffix of a play that starts in u(vi), visits vi, and conforms to f u(vi) by minimality of Du(vi) Then V (Win/V ) And so, by condition 2 & 3 Win i = min j ( ) u v j

Example Max Parity Game Player 0 Wins (memoryless) on each v in {z1, z2}, eg: f0z1wins on z1: f0z1(z1) = z2 f0z2wins on z2: f0z2(z2) = z1 Strategy f0(z)= (f0z1if z=z1or f0z2if z=z2) is not winning. But if z1<z2we get according to the construction: f0 =f0z1 which is indeed a winning strategy on {z1, z2} for Player 0. f0z1(z2) = z3 f0z2(z1) = z0 Player 0 Player 1

Forgetful Determinacy of Regular Games We prove: In every Regular Game both Players win forgetful. Forgetfull determinacy of Regular games We use the following theorem: In every Parity game, both players win memoryless. (proven in chapter 6) memoryless determinacy of parity games

Forgetful Determinacy of Regular Games Proof Let (A, ,F) be a Muller game remainder: a regular game (A, , acc) has the same winning regions as some muller game (A, ,F) Let A be the equivalent Max-Parity game V = V Let f 0, f 1be memoryless winning strategies on W0 , W1 by memoryless determinacy of parity games idea: use finite memory to simulate playing on A when playing on A. Winning regions are: W = { v V | (v, r(v)) W }

Forgetful Determinacy of Regular Games Proof set memory M= set mI=r(v)= (v) set = update memory according to the update rule of 2.7 g (v, q) := f ( (v, q) )0 (v , q )0= v f generates a winning play in A , then by previous theorem, the sequence of the first components is a winning play win A. Thus g is a winning strategy for Player .

Ilustration of Forgetfull Strategy (same example from before) Player 0 Player 1 F = {{b}} - = z1z2z0z1z2 is winning for Player 0 - Winning regions: W0= {z2} and W1= {z0, z1}. - = (z1, a)(z2, ab)(z0, ba)(z1, b a)(z2, ab)(z2, a b) - ( ) = 133132 (winning for Player 0)

Some (unproven) Results regarding memoryless determinacy Parity games enjoy memoryless determinacy In some Muller games both player need memory to win. Rabin and Street are in between: one of the two players always has a memoryless winning strategy, specifically: In Rabin games Player 0 has a memoryless strat. In Streett games Player 1 has a memoryless strat.

Reachability Games & Attractors A new kind of games, given: Arena A = (V0, V1, E) X V Reachability Game R(A, X): is a winning play for Player 0 if: some v X occurs in , or: A dead end of Player 1 occurs in . Different then former games: dead end of player 0 isn t necessarily a loss for him strategies for player 0 aren t required to be defined on plays ending in some v X.

Ordinals and Transfinite Induction A Short Digression Motivation: we want to prove some property using induction Problem: dealing with non countable sets Well Ordered sets: A Totally ordered set, s.t each (non emtpy) subset has a least element. equivalently (AOIC) every strictly descending series is finite canonical example: Ordinals: we think of them as the position of an element in an ordered set. An ordinal that is no a successor (other then 0) is called a limit ordrinal. Example: 0,1, , , +1, +2 , *2, , * Theorem: every set can be well ordered (using AOC)

Transfinte induction (and recursion) Induction: prove P(0) (base case) successor step: assuming P(a) prove P(a+1) Limit step: for every limit ordinal assume P(a) for all ordinals <a to prove P( ) Recursion: Define S0 for every ordinal a define Sa+1using definition Sa Limit step: for every limit ordinal define S using the definition of safor all ordinals a< .

Theorem: Reachability Games Enjoy Memoryless Determinacy A is an arena, X V The winning region and the winning strategy for player 0 in R(A, X) are defined inductively: X0= X For ordinals v: X +1= Xv pre(Xv) pre(Y ) = { v V0| vE Y = } { v V1 | vE Y } vertices in V0who have a neighbour in Y verticesi in V1where all neighbours are in Y. v v X for each limit ordinal : Idea: A W0 A pre(A) W0 Let be the smallest ordinal such that X = X +1 Claim: W:= X is Player 0 s winning region (W=W0).

Illustration X0=X X1=X0UPre(X0) X2=X1UPre(X1) X3=X2UPre(X2) X =UiXi X +1=X U Pre(X )

Reachability games enjoy memoryless determinacy First Direction. First direction, show W W0: For every v W\X there exists a unique ordinal v < such that v X v+1\ X v Further, if v V0(v W V0\X) then by Pre there is a neigbour of v, v s.t v X v Choose (memoryless) strategy: f0(v) = v Claim: f0 is winning on W. Show by transfinite induction: f0 is winning on X for every .

Illustration v V1 v V0 f0 X v+1 =X vU Pre(X v) V X v

Reachability games enjoy memoryless determinacy Second direction. Define W = V\W . Second direction: show W W1 Let v W v X If v is a dead end: It is a dead end of Player 0 Since all dead ends of player 1 are in X1 (by Pre) Then player 1 win on v If v is not a dead end and v V0: then for every v vE v W (v W ) If v is not a dead end v V1: there exists v vE such that v W (v W ) Set f1(v) = v (memoryless strategy for Player 1) Every play conform with f1and starting in W is contained in W Since W doesn t contain vertices from X or dead ends of Player 1, every such play is winning for Player 1. Finally: W=W0 and W =W1

Reachability Games-definitions The winning region of Player 0 in the reachability game R(A, X) is denoted Attr0(A, X) and called 0-attractor of the set X in the arena A. The winning strategy (denoted f0 in the proof) is called the a corresponding attractor strategy for Player 0. 1-attractor and strategy are symmetrically defined by exchanging V0and V1in the arena.

-trap - Definition A -trap is a subset Y V such that vE Y for every v Y V and vE Y for every v Y V A function which picks for every v Y V a vertex v vE Y is called a trapping strategy for Player . The complement of a -attractor is a -trap in last proof W =V\W is a 0-trap.

Conclusion WLOGarenas have no dead ends (no proof) Let (A, Acc) be an arbitrary game A = (V0, V1,E) set U = Attr (A, ) Player wins on U Memoryless (by forcing the player to a dead end) Arena A : remove vertices from which you can force the other player to a dead end: V0 := V0\ (U0 U1) V1 := V1\ (U0 U1) V = V0 V1 E = E (V xV ) A = (v0 , v1 , E ) Claim: for every for every v V , Player wins (A , Acc, v) iff he wins (A, Acc, v) Winning strategies for (A , Acc) can be used in (A, Acc). use: the complement of a -attractor is a -trap hw..