{"id":214,"date":"2015-04-23T12:27:34","date_gmt":"2015-04-23T10:27:34","guid":{"rendered":"http:\/\/duch.mimuw.edu.pl\/~bojan\/podpunkt\/?page_id=214"},"modified":"2017-10-31T12:58:37","modified_gmt":"2017-10-31T11:58:37","slug":"safety-games","status":"publish","type":"page","link":"https:\/\/www.mimuw.edu.pl\/~bojan\/20142015-2\/alg\/5-piecewise-testable-languages\/safety-games","title":{"rendered":"Safety Games"},"content":{"rendered":"

A safety game.\u00a0<\/b>A\u00a0safety game\u00a0<\/em>is a kind of game of infinite duration and perfect information, played by two players. The game is defined by an arena<\/em>, which is a directed graph plus a function which says for each vertex (which is called a position<\/em> of the game) which of the two players own this vertex. Here is a picture of an arena, with the players being called \"0\" and \"1\":<\/p>\n

\"safety-game\"<\/a><\/p>\n

Given an initial position, the game is played as follows: at each step the player who owns the current position chooses an outgoing edge, and so on until either an infinite path is created (in which case the player \"0\" wins), or a position is reached which does not have outgoing edges (in which the player who cannot make a move loses, i.e. the player who does not own the last position wins).<\/p>\n

Theorem.\u00a0<\/strong>Given a safety game with a finite arena and an initial position, one can decide in polynomial time which of the two players has a winning strategy. Furthermore, the player who has a winning strategy also has a memoryless winning strategy, which means that the choice of next position depends only on the current position and not on the history of the game before reaching that position.<\/p>\n

Proof. <\/strong>We define a sequence of sets of positions where player \"1\" can force a victory in a finite number of positions.\u00a0Define \"V_0\" to be the empty set, and define \"V_{n}\" to be \"V_{n-1}\" plus those positions \"v\" such that either:
\n\u2022 \"v\" is owned by player \"0\", and all outgoing edges from \"v\" go into \"V_{n-1}\"; or
\n\u2022 \"v\" is owned by player \"1\", and some outgoing edge from \"v\" goes into \"V_{n-1}\".<\/p>\n

For example, \"V_1\" consists of positions owned by player \"0\" which have no outgoing edges.\u00a0It is easy to see that for positions in \"V_n\", player \"1\"\u00a0has a memoryless strategy which guarantees victory in at most \"n\" steps, i.e. in at most \"n\" steps player \"0\" will end up in a position without outgoing edges. If the arena is finite, the sequence \"V_n\" must stabilize at some set, call it \"V_*\". As mentioned above, player \"1\" has a winning strategy that guarantees winning on all positions from \"V_*\". We claim\u00a0that\u00a0player \"0\" has a memoryless winning strategy in positions outside \"V_*\". This is because\u00a0by definition, if a position is not in \"V_*\", then either it belongs to player \"0\" and has at least one outgoing edge that stays outside \"V_*\", or it belongs to player \"1\" and has all outgoing edges that stay outside \"V_*\". The strategy of player \"0\" is to use the edge the stays outside \"V_*\". \"\Box\"<\/span><\/p>\n

In future lectures, we will also consider safety games with possibly infinite arenas. Of course the part of the above theorem about polynomial time no longer makes sense, but the part about memoryless strategies continues to be true. Consider the proof of the above theorem, and apply it to an infinite arena. Instead of indexing the sets \"V_n\" by natural numbers, one can index them by ordinal numbers. For ordinal numbers, instead of \"V_{n-1}\" one talks about the union of \"V_m\" ranging over ordinal numbers \"m < n\". The set \"V_n\" is\u00a0guaranteed to stabilize for some ordinal.<\/p>\n","protected":false},"excerpt":{"rendered":"

A safety game.\u00a0A\u00a0safety game\u00a0is a kind of game of infinite duration and perfect information, played by two players. The game is defined by an arena, which is a directed graph plus a function which says for each vertex (which is called a position of the game) which of the two players own this vertex. Here […]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":212,"menu_order":2,"comment_status":"open","ping_status":"open","template":"","meta":{"_acf_changed":false,"inline_featured_image":false,"footnotes":""},"class_list":["post-214","page","type-page","status-publish","hentry"],"acf":[],"_links":{"self":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/214"}],"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=214"}],"version-history":[{"count":6,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/214\/revisions"}],"predecessor-version":[{"id":469,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/214\/revisions\/469"}],"up":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/212"}],"wp:attachment":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/media?parent=214"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}