Memoryless Determinacy of Parity Games - Tel Aviv University

Memoryless Determinacy of Parity Games - Tel Aviv University

Memoryless Determinacy of Parity Games C H A P T E R 6 I N A U T O M ATA , L O G I C A N D I N F I N I T E G A M E S , E D I T E D BY G R A D E L , T H O M A S AND WILKE G A M E S , L O G I C A N D A U T O M ATA S E M I N A R 19/4/2017 LIOR ZILBERSTEIN

In the Previous Lecture Game an arena and a winning condition. Arena - the directed graph where the game is played on. Winning condition a winning set that can be described using the acceptances conditions that were introduced in lecture 2, using a coloring function . Successors the successors of is defined by Plays a path starting from the initial vertex , that is consistent with the graph. A play might be infinite or finite if it reaches a dead end.

In the Previous Lecture Parity games a game where the winning condition is: iff is even. Remark For every regular game there exists a Muller winning condition such that and have the same winning regions. Theorem for every Muller game there exists a parity game and a function such that for every , player wins if and only if player wins . In This Lecture Theorem Every parity game is determined, meaning that the winning regions for

player 0 and player 1 partition the set of vertices of the game. We will also see that the winning player have a memoryless winning strategy for the game. From this we get Every regular game is determined. But First: Some Useful Notations

Subgames Definition let be any subset of . The subgraph of induced by is denoted , where and is the restriction of to . The graph is a subgame of if every dead end in is also a dead end in . In other words, in a subgame no new dead ends may be introduced. New dead ends might change the winning regions. Subgames

For example, lets look at the game, , to the right. The subgraph is a subgame. The subgraph is not a subgame, because is a dead end in the sub graph but not in the original graph. Subgames Lemma let and be subsets of such that and is a subgame of and is a subgame of . Then, is a subgame of .

Proof Let be a dead end in , this means has no successors in , so is a dead end in as well. We know that is a dead end in , because is a subgame of . And because is a subgame of , is a dead end in also. We showed every dead end in is a dead end in , hence, is a subgame of . -traps If the token is in a -trap , then player can play a strategy consisting in choosing always successors

inside of . On the other hand, since all successors of -vertices in belong to , player has no possibility to force the token outside of . In the example the set is a 1-trap and the set is a 0-trap. -traps Lemma (1) For every -trap in , is a sub game. (2) For every family of -traps , the union is a -trap as well.

(3) If is a -trap in and is a subset of , then is a -trap in iff is a -trap in . Note the converse of (1) is not true. For example, the set from the example is a subgame in , but it is neither a 0-trap nor a 1-trap. Also, the equivalence in (3) does not hold for nested traps of different types: if is a -trap and is -trap in , then, in general, is not a trap of any kind in . Attractors and Attractor Sets The attractor set for player and set , is the set of vertices from which player has a strategy to

attract the token to or a dead end in in a finite number of steps. As proven in the last lecture the attraction strategy is a memoryless strategy. In the example Attractors and Attractor Sets Lemma (1) The set is a -trap in .

(2) If is a -trap in , then so is . (3) is a -trap in iff . (4) where is the greatest (w.r.t. set inclusion) -trap contained in . exists since is a -trap, and by the previous lemma, the union of -traps is a -trap. Attractors and Attractor Sets (1) The set is a -trap in .

Proof let If and then player can move the token from to a vertex in , hence has a memoryless strategy that gets the token from to in a finite number of moves, so , A contradiction. If and , every step player takes from will lead into , so , A contradiction. Attractors and Attractor Sets (2) If is a -trap in , then so is . Proof Let be a -trap. From every vertex in, player has a strategy to force the token into

or a dead end in . In either case, from then on there is no way for to choose a vertex outside of . Note that all dead ends in belong to s attractor set. Attractors and Attractor Sets (3) is a -trap in iff . Proof Assume that is a -trap. This means that, starting from some vertex in , has a strategy to keep the token inside and that does not contain a dead end in . Thus, , for otherwise would have a way to force the token from some vertex in into . The

inclusion in the other direction is trivial. Conversely, assume . By (1), is a -trap. Then, shows that is a -trap. Attractors and Attractor Sets (4) where is the greatest (w.r.t. set inclusion) -trap contained in . Proof By definition of , . Hence, . Because is a -trap, (3) implies . For the converse inclusion, we show that . By (1), is a -trap. Moreover, implies . Since is the biggest -trap with , it follows

-Paradise A -paradise in game is a region (a set of vertices) from which cannot escape and wins from all vertices of this region using a memoryless strategy. Its important to note that, -paradise is a subset of s winning region . -Paradise Formally, a set is a -paradise if is a -trap

There exists a memoryless winning strategy for on such that - is a total mapping from into such that, for all , - For every and every play in that conforms with , is winning for .

. -Paradise Lemma (1) If is a -paradise, then so is . (2) Let be a family of -paradises. Then is a -paradise. Proof (1) By the last lemma, is a -trap. A memoryless winning strategy for will be: For vertices , has a memoryless strategy to force the token to or to a dead end in , in the

latter case, wins. In the former case, once in , plays according to the memoryless winning strategy for and wins as well. -Paradise (2) first, as a union of -traps, is also a -trap. Let be a finite play. The dead end, , in belongs to some . Since all vertices of are winning for , we can conclude that . Thus, wins . For an infinite play, Let denote the memoryless winning strategy on for . A memoryless winning strategy on for is constructed in the following way: Fix a wellordering relation on I (Axiom of choice guarantees the existence of such relation).

Then for , we set , where is the least element of I (w.r.t. ) such that . We need to show that is a winning strategy on . -Paradise Let be an infinite play that conforms with and let, for all , . Obviously, . More importantly, the successor vertex belongs to as well (either is a vertex and then all

of its successors, in particular , belong to the -trap , or is -vertex and then ). Moreover, implies that . Since an infinite non-increasing sequence of elements of wellorder set is ultimately constant, we conclude that some suffix of is conform with one of the strategies . Thus, wins . Determinacy Determinacy Now, we can show that parity games are determined and that the winner of a parity game has a memoryless winning strategy. Formally, we prove the main theorem of this lecture:

Theorem The set of vertices of a parity game is partitioned into a 0paradise and a 1-paradise We will provide two proofs of this theorem, a non-constructive one, and a constructive one. For finite parity games, the second proof can even be turned into a recursive algorithm for computing the winning regions and the memoryless winning strategies. Three Lemmas Lemma If the maximum parity of is 0, then is partitioned into a 0-paradise and a 1paradise. Proof Since the maximum parity of is 0, player 1 can only win on dead ends in or

vertices from which he can force the token to such a dead end. That is, the 1-paradise is the set with an obvious winning strategy. Since is a 1-trap and the maximum parity of is 0, it is easy to see that is a 0-paradise. Three Lemmas We will now assume that the maximum parity of is at least 1. by induction and the first lemma, we may assume that our theorem holds for every parity game with maximum parity less than . Let , this means player wins if the token visits infinitely often the maximum parity. Let be

a -paradise such that is a -trap. Finally, let and . Note that as a complement of an attractor, is a -trap in , and thus, is a subgame of , so is a subgame of . Three Lemmas The colors in are elements of , thus, by the induction hypothesis, is partitioned into a 0paradise, , and 1-paradise, , say with a memoryless winning strategies .

Three Lemmas Lemma The union is a -paradise. Proof The set is a -paradise in and is a -trap in , thus, according to a lemma weve proven, is a -trap in . Consequently, is a -trap in : Once inside , cant move the token outside this set. Although from , may be able to move the token inside , cant move it outside in .

Three Lemmas Let be the memoryless winning strategy of in . When playing according to in and according to in , two cases can occur: (1) At some moment in a play the token hits the set . Then, from this moment on, plays according to and wins the play. (2) The token stays forever in . Since in this set, plays according to , wins the play. We have shown is a -trap, and have a memoryless winning strategy inside this set, so is a -paradise.

Three Lemmas Lemma If , then is a -paradise Proof If , wins everywhere on with . To win on , Player plays as follows on : If the token visits a vertex , then moves it to any successor vertex inside of his winning region , such successor vertex exists since is a -trap. If the token visits , then attracts it in a finite number of steps to or a dead end in . If the token is in , then plays according to the winning strategy on .

Three Lemmas ( ) Formally, the winning strategy for on is defined as follows for : ( )= ( [ ] , ) ( ) ( [ ] , )

{

Let be any play that conforms with starting from some vertex in . Then, three cases can occur. First, from some moment on, the token stays forever inside of and in this case some suffix of conforms with . Second, the token is moved to a dead end in . Third, the token visits infinitely often the maximal parity (i.e. the set ). In all of the three cases, wins. Hence, is a -paradise.

A Non-constructive Proof for Our Theorem Let be the maximum parity occurring in . If , the first lemma is enough to prove the theorem. Suppose , and let . Let be the family of all -paradises. We have proven that is the greatest among these -paradises, say with a memoryless winning strategy . If we show that is a -paradise, we are done. A Non-constructive Proof for Our Theorem First, we need to show is a -trap.

We know that is a -paradise, and that , because is the greatest -paradise, we get. Hence, as a complement of an attractor set, is a -trap. With and we can apply the second lemma and obtain that is a -paradise. However since is the greatest -paradise, it follows that . By the third lemma, we conclude that is a -paradise. This concludes that the set of vertices of a parity game is partitioned into a 0-paradise and a 1-paradise. A Constructive Proof for Our Theorem

In this proof, we will define the winning region constructively using transfinite induction. We construct an increasing sequences of -paradises , and a corresponding winning strategy . For , will be an extension of . The construction will be mainly based on the second lemma, allowing us to expand paradises using union. The set will be specified as before. A Constructive Proof for Our Theorem Our base case, , again follows the first lemma. For the induction step, we assume and define as before.

Initially, . For a limit ordinal we set . By the lemma we have proven about paradises, is a paradise. Since, by the induction hypothesis, for every the strategy is an extension of we can define to be the union of the strategies with . Now, some suffix of any play that conforms with conforms with one , which is a winning strategy, hence, so is . A Constructive Proof for Our Theorem For a non limit ordinal , we define using the second lemma. First we set ) to be the

attractor set for on . We have proven that this is a -paradise, moreover, the memoryless winning strategy on , call it , extends on . Since is a -attractor set, is a -trap and we can apply the second lemma and define . The set is a -paradise, and has a winning strategy as defined in the proof of the second lemma, and it extends . A Constructive Proof for Our Theorem Let be the smallest ordinal such that .

Let . We claim that is a -paradise. Since is a -paradise, this would complete our constructive proof. We know , implying that . Thus, is a -trap, as a complement of a -paradise. With and we can apply the second lemma and obtain that is a -paradise. By construction of , it follow , and since these sets are disjoint, we obtain that . By the third lemma, we conclude that is a -paradise. Algorithmic Result

The Winning-Regions Algorithm We now present a (nave) deterministic algorithm, called winning-regions, for computing the winning regions and corresponding winning strategies of the two players of a finite parity game. This algorithm is derived in a straightforward manner from the constructive proof we saw. Its correctness follows immediately. There are better known deterministic algorithms for computing winning regions, that unlike this algorithm require polynomial space.

Since we work with finite graphs, natural induction suffices. winning-regions() if return win-opponent() winning-regions()

: return win-opponent() repeat: :

=winning-regions() Until Return The Winning-Regions Algorithm Corollary Computing the winning region of finite parity games and the corresponding memoryless winning strategies can be carried out in time , where m is the number of edges, l it the number of vertices and n is the maximum parity.

Proof Note that w.l.o.g., we may assume . All assignments except for those involving recursive function calls, can be carried out in time where c is some fixed, big enough, constant. Attractor set can be computed in time . The Winning-Regions Algorithm We denote by the worst case runtime of winning-regions on all inputs with those parameters. And similarly, by the worst case runtime of win-opponent. We obtain the following inequalities:

Note that the recursive call for winning-regions() is not necessary in winning-regions, because we compute it in the last iteration step of win-opponent. So when we can omit its runtime in the inequality for . The Winning-Regions Algorithm Solving the above inequality system, yields that

Complexity Result A Simple Complexity Result Let be the problem of deciding whether, given an initialized finite parity game, player 0 wins. Corollary

A Simple Complexity Result Proof first we show The following is a nondeterministic polynomial time algorithm for deciding : (1) Given , guess a memoryless strategy for player 0. (2) Check whether is a winning strategy. We need to show that the second step can be carried out in polynomial time. The strategy can be represented by a subgraph of , this subgraph coincides with except that all edges where and are eliminated. i.e. for a 0-vertex we only keep the outgoing edge referred by .

A Simple Complexity Result Given , we need to check whether there is a dead end in reachable from . We also need to check whether there exists a vertex reachable from in such that is odd and lies on a cycle in containing only vertices of parity less or equal to . If one of this conditions is true, player 0 loses the game. Checking this can be carried out in polynomial time, thus . A Simple Complexity Result

We now show . By our theorem, deciding means deciding whether is a winning positon for player 1. To do so, we construct - a game where 0-vertices and 1-vertices are switched, and all parities are increased by 1. Applying the algorithm on will give us . ?Questions

Recently Viewed Presentations

  • A ABC is similar to . Find x

    A ABC is similar to . Find x

    100. ITriangle BCD is similar to triangle EFG.Find x _____ 10. J∆ ??? ~∆???Find x
  • For by grace you have been saved through

    For by grace you have been saved through

    "Oh God, grant what you command and command what you desire." Heretic. 8 For by grace you have been saved through faith. And this is not your own doing; it is the gift of God, 9 not a result of...
  • Building quality assurance and quality improvement systems at ...

    Building quality assurance and quality improvement systems at ...

    the mental process required for successful paraphrasing helps you to grasp the full meaning of the original. Overview. Paraphrasing. Changes the original text into your own words. ... Simply substituting synonyms is usually not enough! Activity. Referencing - before you...
  • Formas de energía alternativas - vecinadelpicasso

    Formas de energía alternativas - vecinadelpicasso

    Medgaz es un gaseoducto submarino que está proyectado entre Argelia y España. En Almería se conectará con el existente gaseoducto Almería-Albacete. El gas fluye desde el 2011. El gasoducto tiene una longitud de 210 km y cuenta con una capacidad...
  • Globalization: What it is and what it isn't?

    Globalization: What it is and what it isn't?

    Globalization: What it is and what it isn't Trade and movement of infected cattle and poultry across national borders have contributed to recent outbreaks of mad cow disease in the northern hemisphere and avian influenza in Asia.
  • Random Acts of Kindness Bulletin Board: - Reslife.Net

    Random Acts of Kindness Bulletin Board: - Reslife.Net

    Random Acts of Kindness Bulletin Board:An example of taking an idea from ResLife.net and expanding it a bit Cheyenne Harrington, RA. Submitted By Beth Hill, Associate Director of Residence Life. Western New England College
  • S608 Developing Guidelines for Determining When to Use

    S608 Developing Guidelines for Determining When to Use

    Deke Smith, FAIA, Executive Director, buildingSMART alliance. December 11, 2008 . S608. Developing Guidelines for Determining When to Use . ISO 16739 and ISO 15926. National Institute of Building Sciences. 1974 - Public Law 93-383, Sect. 809 .
  • B. Water Bodies - act as heat sink/source

    B. Water Bodies - act as heat sink/source

    Manaus, Brazil Tropical Dry Forest Savannah The Temperate Zone: BIOMES Differences in temperate zone biomes are driven by a combination of temp and rainfall. Deserts Alpine Tundra Lotic Systems - Moving Waters Lentic Systems: Ponds and Lakes Marine Systems