{"id":615,"date":"2015-10-15T15:15:55","date_gmt":"2015-10-15T13:15:55","guid":{"rendered":"http:\/\/www.mimuw.edu.pl\/~bojan\/?page_id=615"},"modified":"2015-10-26T15:08:30","modified_gmt":"2015-10-26T14:08:30","slug":"games-with-%cf%89-regular-winning-conditions","status":"publish","type":"page","link":"https:\/\/www.mimuw.edu.pl\/~bojan\/20152016-2\/jezyki-automaty-i-obliczenia-2\/games-with-%cf%89-regular-winning-conditions","title":{"rendered":"2. Games with \u03c9-regular winning conditions"},"content":{"rendered":"

In this lecture, we consider games played by two players\u00a0(called 0 and 1), which are zero-sum, perfect information, and most importantly, of potentially infinite duration. Suppose that \"W \subseteq \Sigma^\omega\" is a set of \"\omega\"-words. Define a\u00a0game with winning condition \"W\"\u00a0<\/em>to be:<\/p>\n

\u2022 a directed graph, not necessarily finite, whose vertices will be called\u00a0positions of the game;<\/em>
\n\u2022 a\u00a0distinguished\u00a0initial position<\/em>;
\n\u2022 partition of the positions<\/em>\u00a0into\u00a0positions\u00a0controlled by player 0 \u00a0<\/em>and\u00a0positions\u00a0controlled by player 1;
\n\u2022<\/em>\u00a0a labelling function<\/em>\u00a0that maps each position\u00a0to a label from \"\Sigma\".
\n<\/em><\/p>\n

The game is played as follows. The game begins in the initial position. The player who controls\u00a0the initial position\u00a0chooses an outgoing edge, leading to a new position. The player who controls\u00a0the new position\u00a0chooses an outgoing edge, leading to a new position, and so on. If the play reaches a position\u00a0with no outgoing edges, then the player who controls\u00a0the position\u00a0loses immediately. Otherwise, the play continues forever, and yields an infinite path. By applying the labelling function\u00a0to the path, we get an word in \"\Sigma^\omega\"; if this word belongs to \"W\" then player 0 wins, otherwise player 1 wins.<\/p>\n

When formalizing the notions of the above paragraph, one uses the concept of a strategy. <\/em>A strategy\u00a0for player \"i \in \set{0,1}\" is a function which inputs a history of the play so far (a path from the initial position\u00a0to some position\u00a0controlled by player \"i\"), and outputs the new position\u00a0(consistent with the edge relation in the graph). Given strategies for both players, call these \"\sigma_0\" and \"\sigma_1\", a unique play is determined, which is either a finite path ending in a terminal\u00a0position\u00a0(no outgoing edges), or an infinite path. This play is called winning for player \"0\"<\/em> if it is finite and ends in a terminal\u00a0position\u00a0controlled by\u00a0the opposing player\u00a0\"1\"; or if it is infinite and satisfies the winning condition after applying the labelling function. Otherwise, the play is winning for player \"1\". A winning<\/em> strategy for player \"i\" is defined to be a strategy \"\sigma_i\" such that for every possible strategy \"\sigma_{1-i}\" of the opponent, the resulting play is winning for player \"i\".<\/p>\n

\n

 <\/p>\n

Determinacy.\u00a0<\/strong>A game is called determined<\/em> if one of the players has a winning strategy. Clearly it cannot be the case that both players have winning strategies. One could be tempted to think that, because of the perfect information, one of the players must have a winning strategy. However, because of the infinite duration, one can come up with strange games (e.g. using the axiom of choice) which are not determined because none\u00a0of the players has a winning strategy.<\/p>\n

The goal of this lecture is to show a theorem by B\u00fcchi and Landweber: if the winning condition of the game is recognised by an automaton, then the game is determined, and furthermore the winning player has a finite memory winning strategy, in the following sense.<\/p>\n

Finite memory\u00a0strategy.\u00a0<\/strong>Consider a game where the positions\u00a0are \"V\". Let \"i\" be one of the players. A strategy for player \"i\" with memory<\/em>\u00a0\"M\" is given by:
\n\u2022 a\u00a0deterministic automaton with states \"M\" and input alphabet \"V\"; and
\n\u2022 for every\u00a0position\u00a0\"v\" controlled by \"i\", a function \"f_v\" from \"M\" to the neighbors of \"v\".
\nThe two ingredients above define a strategy for player \"i\" in the following way: the next move chosen by player \"i\" in a position\u00a0\"v\" is obtained by applying the function \"f_{v}\" to the state of the automaton after reading the history of the play, including \"v\". We will apply this definition also to games with infinitely many\u00a0positions, but we will only care about finite memory sets \"M\".<\/p>\n

An important special case is when the set \"M\" has only one element, in which case the strategy is called \u00a0memoryless<\/em>. In this case, the new position\u00a0chosen by the player only depends on the current position, and not on the history of the game before that.<\/p>\n

Theorem. (B\u00fcchi-Landweber)\u00a0<\/strong>For every \"\omega\"-regular language \"W\" there exists a finite set \"M\" such that for every game with winning condition \"W\", one of the players has a winning strategy that uses memory \"M\".<\/p>\n

The proof of the above theorem has two parts. The first part is to identify a special case of games with \"\omega\"-regular winning conditions, called\u00a0parity conditions.\u00a0<\/em>Define the\u00a0\"n\"-rank parity condition\u00a0<\/em>to be\u00a0the set of \"\omega\"-words over the alphabet \"\set{1,\ldots,n}\" where the smallest number appearing infinitely often is even.\u00a0A\u00a0parity game\u00a0<\/em>is a game where the winning condition is the \"n\"-rank parity language for some \"n\".<\/p>\n

Parity games are important because not only can they be won using finite memory strategies, but even memoryless strategies are enough:<\/p>\n

Theorem 1.\u00a0<\/strong>For every parity game, one of the players has a memoryless winning strategy.<\/span><\/p>\n

Theorem 1\u00a0is proved here<\/a>.\u00a0The second step of the B\u00fcchi-Landweber theorem is the reduction to parity games. This essentially boils down to transforming deterministic Muller automata into something called deterministic parity automata.<\/em>\u00a0In a parity automaton, there is a ranking function from states to numbers, and a run is considered accepting if the minimal rank appearing infinitely often is even. This is a special case of the Muller condition, but it turns out to be expressively complete in the following sense:<\/p>\n

Theorem 2.\u00a0<\/strong>For every deterministic Muller automaton, there exists an equivalent deterministic parity automaton.<\/p>\n

Theorem 2 is\u00a0proved\u00a0here<\/a>. Let us now combine the two theorems to get the B\u00fcchi-Landweber theorem. Consider a game with an \"\omega\"-regular winning condition \"L \subseteq \Sigma^\omega\". By Theorem 2, there is a deterministic parity automaton which recognises the language \"L\". Consider a new game, call it the product game, <\/em>\u00a0where the positions are pairs (position of the original game, state of the deterministic parity automaton). This is a parity game, with the ranks inherited from the automaton. In a position \"(v,q)\", the player controlling position \"v\" chooses an edge in the original game, and the state is updated deterministically according to the transition function of the automaton. It is not difficult to see that the following conditions are equivalent for every position \"v\" of the original game and every player \"i \in \set{0,1}\":
\n1. player \"i\" wins from position \"v\" in the original game;
\n2. player \"i\" wins from position \"(v,q)\" in the product game, where \"q\" is the initial state of the automaton.<\/p>\n

The implication from 1 to 2 crucially uses determinism of the automaton and would fail if a nondeterministic automaton were used (under an appropriate definition of a product game).\u00a0Since the product game is a parity game, for every position \"v\", condition 2 must hold for either player 0 or 1; furthermore, a positional strategy in the product game corresponds to a finite memory strategy in the original game, where the memory is the states of the automaton.<\/p>\n

 <\/p>\n","protected":false},"excerpt":{"rendered":"

In this lecture, we consider games played by two players\u00a0(called 0 and 1), which are zero-sum, perfect information, and most importantly, of potentially infinite duration. Suppose that is a set of -words. Define a\u00a0game with winning condition \u00a0to be: \u2022 a directed graph, not necessarily finite, whose vertices will be called\u00a0positions of the game; \u2022 […]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":535,"menu_order":2,"comment_status":"open","ping_status":"closed","template":"","meta":{"_acf_changed":false,"inline_featured_image":false,"footnotes":""},"class_list":["post-615","page","type-page","status-publish","hentry"],"acf":[],"_links":{"self":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/615"}],"collection":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/comments?post=615"}],"version-history":[{"count":13,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/615\/revisions"}],"predecessor-version":[{"id":715,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/615\/revisions\/715"}],"up":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/535"}],"wp:attachment":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/media?parent=615"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}