{"id":765,"date":"2015-10-27T11:25:59","date_gmt":"2015-10-27T10:25:59","guid":{"rendered":"http:\/\/www.mimuw.edu.pl\/~bojan\/?page_id=765"},"modified":"2015-10-27T16:15:07","modified_gmt":"2015-10-27T15:15:07","slug":"distance-automata","status":"publish","type":"page","link":"https:\/\/www.mimuw.edu.pl\/~bojan\/20152016-2\/jezyki-automaty-i-obliczenia-2\/distance-automata","title":{"rendered":"4. Distance automata"},"content":{"rendered":"

The syntax of a\u00a0distance automaton\u00a0<\/em>is the same as for a nondeterministic finite automaton, except that it has a distinguished subset of transitions, called the costly\u00a0<\/em>transitions. The cost of a run is defined to be the number of costly transitions that it uses. In this lecture, we prove the following theorem.<\/p>\n

Theorem.\u00a0<\/strong>The following problem is decidable:
\n\u2022 Input.<\/strong>\u00a0A\u00a0distance automaton.
\n\u2022 Question.\u00a0<\/strong>Is the automaton bounded\u00a0<\/em>in the following sense:\u00a0there is some \"m \in \Nat\" such \u00a0that every input word admits an accepting run of cost at most \"m\".<\/p>\n

The problem in the above theorem is called the\u00a0limitedness\u00a0<\/em>problem for distance automata. The goal of this lecture is to show how limitedness can be decided using the B\u00fcchi-Landweber theorem.<\/a><\/p>\n

\n

 <\/p>\n

The limitedness game.<\/strong><\/p>\n

Let us fix a distance automaton. For a number \"m \in \Nat \cup \set \omega\", consider the following game, call it the limitedness\u00a0game with bound \"m\".\u00a0<\/em>The game is played in infinitely many rounds \"1,2,3,\ldots\", by two players called Input<\/em>\u00a0and Automaton<\/em>. In each round:
\n\u2022 player Input chooses a letter of the input alphabet;
\n\u2022 player Automaton responds with a set of transitions over this letter.<\/p>\n

A set of move of player Automaton in a given round, which is a set of transitions, can be visualised as a bipartite graph, which says how the letter can take a state to a new state, with costly transitions being\u00a0solid edges and non-costly transitions\u00a0being\u00a0dashed edges, like below:<\/p>\n

\"set<\/a><\/p>\n

For the definition of the game, it is important that player Automaton does not need to choose all possible transitions over the letter played by player Input, only a subset. After all\u00a0rounds have been played, the situation looks like this:<\/p>\n

\"s\"<\/p>\n

The winning condition for player Automaton is the following:<\/p>\n

    \n
  1. in every column, an accepting state must be reachable from an initial state in the first column; and<\/li>\n
  2. every path contains \u00a0\"<m\" solid edges.<\/li>\n<\/ol>\n

    In case of \"m = \omega\", the second condition says that every path contains finitely many solid edges.<\/p>\n

     <\/p>\n

    The following lemma implies the decidability of the limitedness problem.<\/p>\n

    Lemma.\u00a0<\/strong>For a distance automaton, the following conditions are equivalent, and furthermore one can decide if they hold:<\/p>\n

      \n
    1. the automaton is limited;<\/li>\n
    2. there is some \"m\" such that player Automaton wins the limitedness game with bound \"m\";<\/li>\n
    3. player Automaton wins the limitedness game with bound \"\omega\"<\/li>\n<\/ol>\n

       <\/p>\n

      It remains to prove the lemma. The implications from 2 to 1 and from 2 to 3 are immediate. For the other implications and the decidability part, the key is the observation that for every choice of \"m \in \Nat \cup \set{\omega}\", \u00a0the limitedness game is a special case of a game with a finite arena and an \"\omega\"-regular condition. \u00a0In particular, one can apply the B\u00fcchi-Landweber theorem<\/a>, yielding that a) the winner can be decided; b) the winner needs finite memory. Condition a) is used to get the decidability in the lemma, while condition b) will be used in the implication from 3 to 2.<\/p>\n

       <\/p>\n

      \n

       <\/p>\n

      Implication from 1 to 2.<\/strong><\/p>\n

      We want to prove that if the automaton is limited, then player Automaton has a winning strategy for some finite \"m\", which will turn out to be the same \"m\" as in the definition of limitedness. Here is the strategy of player automaton.\u00a0Define a run \"\rho\" of the distance automaton over an input word \"w\" to be\u00a0optimal\u00a0<\/em>if it has minimal cost among runs that have the same input word, same source state and same target state. The strategy of player Automaton is as follows: if the input word is \"a_1 \cdots a_i\", then in the \"i\"-th round, player Automaton responds with those transitions that participate in some optimal run of cost \"<m\" over the word \"a_1 \cdots a_i\". An important observation is that optimal runs are closed under prefixes, and therefore the graph produced by player Automaton in the first \"i\"\u00a0rounds\u00a0consists of all optimal runs over the first \"i\" letters of the input. \u00a0This guarantees that the strategy is winning.<\/p>\n

       <\/p>\n

      \n

       <\/p>\n

      Implication from 3 to 2.<\/strong><\/p>\n

      Suppose that player Automaton wins the limitedness game with bound \"\omega\". We will prove that player Automaton can also win the limitedness game with a finite bound.<\/p>\n

      By the B\u00fcchi-Landweber theorem, if player Automaton can win the game with bound \"\omega\", then he can also\u00a0win the game with a finite memory strategy. We will show that this finite memory strategy is actually winning for a finite bound.<\/p>\n

      By unfolding the definition of a finite memory strategy in the limitedness game, there is a deterministic automaton, call it the strategy automaton,<\/em>\u00a0over the input alphabet of the original distance automaton, and a function \"f\" from the states of\u00a0the strategy automaton\u00a0to sets of transitions in the origial distance automaton, such that if in the first \"i\" rounds the letters produced by player Input were \"a_1 \cdots a_i\", then the response of player Automaton in the \"i\"-th round is obtained by applying \"f\" to the state of the strategy automaton\u00a0after reading \"a_1 \cdots a_i\".<\/p>\n

      We claim that this same winning strategy produces runs where the cost is at most (number of states in the distance automaton) times (number of states in the automaton for the strategy), thus proving the implication from 3 to 2 in the lemma.\u00a0To prove the claim, suppose that the strategy produces a run exceeding the above bound. This means that there is some input word \"a_1 \cdots a_i\" such that the strategy maps it to a sequence of transitions \"\delta_1 \cdots \delta_i\" and there exists a run \"\rho\" in \"\delta_1 \cdots \delta_i\" which exceeds the above bound. By a pumping argument, there must be some \"k < l \le i\" such that:
      \na)\u00a0the state of the strategy automaton is the same after \"k\" and \"l\" steps;
      \nb) the state of the run \"\rho\" is the same after \"k\" and \"l\" steps;
      \nc) there is a costly transition in \"\rho\" between steps \"k\" and \"l\".
      \nCondition a) implies that if player Input plays the word<\/p>\n

        <\/span>   <\/span>\"\[a_1 \cdots a_k (a_{k+1} \cdots a_l)^\omega\]\"<\/p>\n

      then player Output will respond with the word<\/p>\n

        <\/span>   <\/span>\"\[\delta_1 \cdots \delta_k (\delta_{k+1} \cdots \delta_l)^\omega\]\"<\/p>\n

      Conditions b) and c) imply that the infinite sequence of transitions above will contain a run with infinite cost, thus contradicting the assumption that the strategy is winning.<\/p>\n

       <\/p>\n

      \n

       <\/p>\n

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

      The syntax of a\u00a0distance automaton\u00a0is the same as for a nondeterministic finite automaton, except that it has a distinguished subset of transitions, called the costly\u00a0transitions. The cost of a run is defined to be the number of costly transitions that it uses. In this lecture, we prove the following theorem. Theorem.\u00a0The following problem is decidable: […]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":535,"menu_order":4,"comment_status":"open","ping_status":"open","template":"","meta":{"_acf_changed":false,"inline_featured_image":false,"footnotes":""},"class_list":["post-765","page","type-page","status-publish","hentry"],"acf":[],"_links":{"self":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/765"}],"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=765"}],"version-history":[{"count":16,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/765\/revisions"}],"predecessor-version":[{"id":785,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/765\/revisions\/785"}],"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=765"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}