{"id":551,"date":"2015-10-13T15:51:59","date_gmt":"2015-10-13T13:51:59","guid":{"rendered":"http:\/\/www.mimuw.edu.pl\/~bojan\/?page_id=551"},"modified":"2015-10-14T10:52:40","modified_gmt":"2015-10-14T08:52:40","slug":"finding-an-accepting-path-in-trees","status":"publish","type":"page","link":"https:\/\/www.mimuw.edu.pl\/~bojan\/20152016-2\/jezyki-automaty-i-obliczenia-2\/mcnaughtons-theorem\/finding-an-accepting-path-in-trees","title":{"rendered":"Solving Trees"},"content":{"rendered":"

The goal of this page is proving the following lemma.<\/p>\n

Lemma 2.<\/strong>\u00a0There exists a deterministic\u00a0Muller\u00a0automaton such that for every tree \u00a0\"t \in [Q]^\omega\", the automaton accepts \"t\" if and only if \"t\" contains a path with infinitely many accepting edges.<\/p>\n

Consider a tree\u00a0\"t \in [Q]^\omega\", and let \"n \in \Nat\" be some depth. Define a node to be important for depth \"n\"<\/em>\u00a0if it is either: the root, a node at depth \"n\", or a node which is a closest common ancestor of two nodes at depth \"n\". This\u00a0definition is\u00a0illustrated below (with solid lines representing accepting edges, and dotted lines representing non-accepting edges):
\n<\/a>
\n<\/a><\/p>\n

\"3-tree-paths\"<\/a><\/p>\n

 <\/p>\n

\n

 <\/p>\n

Definition of the Muller automaton.<\/strong> We now describe the Muller automaton for Lemma 2. After reading the first \"n\" letters of an input tree (i.e. after reading the input tree up to depth \"n\"), the automaton keeps in its state a tree, where the nodes correspond to nodes of the\u00a0input\u00a0tree that are important for depth \"n\", and the edges corresponds to paths in the input tree that connect these nodes.\u00a0This tree\u00a0stored by the automaton is a tree with at most \"|Q|\" leaves, and therefore it has less than \"2|Q|\" edges. The automaton also keeps track of a colouring of the edges, with each edge being marked as accepting or not, where “accepting” means that the corresponding path in the input tree contains at least one accepting edge. Finally, the automaton remembers for each edge an\u00a0identifiers from the set \"\set{1,\ldots,2|Q|-1}\", with the identifier policy being described below. A typical memory state looks like this:<\/p>\n

\"summary-identifiers\"<\/a><\/p>\n

The big black dots correspond to important nodes for the current depth, black edges are accepting, dotted edges are non-accepting, while the numbers are the identifiers. Note that at any given moment, all identifiers are distinct. It might be the case (which is not true for the picture above), that the identifiers used at a given moment have holes, e.g. identifier 4 is used but not 3.<\/p>\n

The initial state of the automaton is a tree which has one node, which is the root and a leaf at the same time, and no edges. We now explain how the state is updated. Suppose the automaton reads a new letter, which looks something like this:<\/p>\n

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

To define the new state, we perform the following four steps.<\/p>\n

Step 1. We first append\u00a0the new\u00a0letter to the tree in the state of the automaton. In the example of the tree and letter illustrated above, the result looks like this:<\/p>\n

\"summary-extended\"<\/a><\/p>\n

Step 2. We then eliminate paths that do die out before reaching the new maximal depth. In the above picture, this means eliminating the path with identifier 4:<\/p>\n

\"summary-extended-pruned\"<\/a><\/p>\n

Step 3. We eliminate unary nodes, thus joining several edges into a single edge. This means that a path which only passes through nodes of degree one gets collapsed to a single edge, the identifier for such a path is inherited from the first edge on the path.\u00a0In the above picture, this means\u00a0eliminating\u00a0the unary nodes that are the targets of edges with identifiers 1 and 5:<\/p>\n

\"summary-extended-pruned-unary\"<\/a><\/p>\n

Step 4. Finally, if there are edges that do not have identifiers, these edges get assigned arbitrary identifiers that are not currently used. In the above picture, there are two such edges, and the final result looks like this:<\/p>\n

\"summary-extended-pruned-unary-final\"<\/a><\/p>\n

This completes the definition of the state update function. We now define the acceptance condition.<\/p>\n

\n

 <\/p>\n

The acceptance condition.\u00a0<\/strong>When executing a transition, the automaton described above goes from one tree with edges labelled by identifiers to another tree with edges labelled by identifiers. For each identifier, a transition can have three possible effects, described\u00a0below:<\/p>\n

    \n
  1. Delete. <\/strong>An edge can be deleted in\u00a0\u00a0step 2 (it dies out) or in step 3 (it is merged with a path to the left). The identifier of such an edge is said to be deleted<\/em> in the transition. Since we reuse identifiers, an identifier can still be present after a transition that deletes it, because it has been added again in step 4, \u00a0e.g. this happens to identifier 4 in the above example.<\/li>\n
  2. Refresh. <\/strong>In step 3,\u00a0a whole path \"e_1 e_2 \cdots e_n\" is\u00a0folded into its first edge \"e_1\". If the part \"e_2 \cdots e_n\" contains at least one accepting edge, then we say that the identifier of edge \"e_1\" is refreshed.<\/em><\/li>\n
  3. Nothing. <\/strong>An identifier might be neither deleted nor refreshed,\u00a0e.g. this is the case for identifier 2 in the example.<\/li>\n<\/ol>\n

    The following fact describes the key property of the above data structure.<\/p>\n

    Fact.\u00a0<\/strong>For every tree\u00a0in \"[Q]^\omega\", the following are equivalent:
    \na)\u00a0the tree contains a path with infinitely many accepting edges;
    \nb) some identifier is deleted finitely often but refreshed infinitely often.<\/p>\n

    Before proving the above fact, we show how it completes the proof of Lemma 2 at the beginning of this page. We claim that condition b) can be expressed as a Muller condition on transitions. The accepting family\u00a0of subsets of transitions is <\/p>\n

      <\/span>   <\/span>\"\[\bigcup_i \Ff_i\]\"<\/p>\n

    where \"i\" ranges over possible identifiers, and the family \"\Ff_i\" contains a set \"X\" of transitions if
    \n\u2022 some transition in \"X\" refreshed identifier \"i\";
    \n\u2022 none of the transitions in \"X\" delete identifier \"i\".<\/p>\n

    Identifier \"i\" is deleted finitely often but refreshed infinitely often if and only if the set of transitions seen infinitely often belongs to \"\Ff_i\", and therefore, thanks to the fact above, the automaton defined above recognises the language in the statement of Lemma 2. The rest of this page is devoted to proving the fact.<\/p>\n

    \n

    Proof of the fact.\u00a0<\/strong>\u00a0The implication from b) to a) is straightforward. An identifier in the state of the automaton\u00a0corresponds to a finite path in the input tree. If the identifier is not deleted, then this path stays the same or grows to the right (i.e. something is appended to the path). When the identifier is refreshed, the path grows by at least one accepting state. Therefore, if the identifier is deleted finitely often and refreshed infinitely often, there is some path that keeps on growing with more and more accepting states, and its limit is a path with infinitely many accepting edges.<\/p>\n

    Let us now focus on the implication from a) to b). Suppose that the tree \"t\" contains some infinite path \"\pi\" that has infinitely many accepting edges. Call an identifier\u00a0active in\u00a0step \"n\"\u00a0<\/em>if the path described by this identifier in the \"n\"-th state of the run corresponds to a prefix of the path \"\pi\". Let \"I\" be the set of identifiers that are active in all but finitely many steps, and which are deleted finitely often. This set is nonempty, e.g. the first edge of the path \"\pi\" has corresponds always to the same identifier. In particular, there is some step \"n\", such that identifiers from \"I\" are not deleted after step \"n\". Let \"i \in I\" be the identifier that is last on the path \"\pi\", i.e. all other identifiers in \"I\" describe finite paths that are earlier on \"\pi\". It is not difficult to see that the identifier \"i\" must be refreshed infinitely often by prefixes of the path \"\pi\".<\/p>\n","protected":false},"excerpt":{"rendered":"

    The goal of this page is proving the following lemma. Lemma 2.\u00a0There exists a deterministic\u00a0Muller\u00a0automaton such that for every tree \u00a0, the automaton accepts if and only if contains a path with infinitely many accepting edges. Consider a tree\u00a0, and let be some depth. Define a node to be important for depth \u00a0if it is […]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":539,"menu_order":1,"comment_status":"open","ping_status":"closed","template":"","meta":{"_acf_changed":false,"inline_featured_image":false,"footnotes":""},"class_list":["post-551","page","type-page","status-publish","hentry"],"acf":[],"_links":{"self":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/551"}],"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=551"}],"version-history":[{"count":12,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/551\/revisions"}],"predecessor-version":[{"id":576,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/551\/revisions\/576"}],"up":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/539"}],"wp:attachment":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/media?parent=551"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}