{"id":1171,"date":"2016-11-16T19:25:27","date_gmt":"2016-11-16T18:25:27","guid":{"rendered":"http:\/\/www.mimuw.edu.pl\/~bojan\/?page_id=1171"},"modified":"2016-12-28T15:30:33","modified_gmt":"2016-12-28T14:30:33","slug":"tree-automata-and-interpretations","status":"publish","type":"page","link":"https:\/\/www.mimuw.edu.pl\/~bojan\/20152016-2\/jezyki-automaty-i-obliczenia-2\/monadic-second-order-logic-and-courcelles-theorem\/tree-automata-and-interpretations","title":{"rendered":"Mso and automata on finite trees"},"content":{"rendered":"

Finite trees and their automata.<\/b><\/p>\n

Apart from graphs, we will also use mso to define properties of trees (and their special case, words). Define a\u00a0ranked alphabet\u00a0<\/em>to be a finite set \"\Sigma\" where every element \"a \in \Sigma\" has an associated arity in \"\set{0,1,\ldots}\". Here is a picture of a ranked alphabet:<\/p>\n

\"mso-courcelle\"<\/a><\/p>\n

A tree over a ranked alphabet<\/em> \"\Sigma\" is defined to be a (rooted) tree where every node has a label from \"\Sigma\". Furthermore, for each node the number of children is the same as the rank of the label, and we assume that these children are ordered, i.e. one can speak of the first child, second child, etc. Here is a picture of a tree over the alphabet from the example above:<\/p>\n

\"mso-courcelle-02\"<\/a><\/p>\n

A tree \"t\" \u00a0over an alphabet \"\Sigma\" can be viewed as a logical structure, call it \"\underline t\". The universe of \"\underline t\" is the nodes. For every \"i \in \set{0,1,\ldots}\" there is a binary predicate \"child_i(x,y)\" which says that \"y\" is the \"i\"-th child of \"x\", and for every \"a \in \Sigma\" there is a predicate \"a(x)\" which says that \"x\" has label \"a\". Using mso, one can define a descendant predicate: a node \"y\" is a descendant of \"x\" if and only if every \"y\" belongs to every set \"X\" that contains \"x\" and is closed under children.<\/p>\n

We say that a set of trees \"L\" over a ranked alphabet \"\Sigma\" is mso definable<\/em> if there is an mso formula \"\varphi\" such that <\/p>\n

  <\/span>   <\/span>\"\[\underline t \models \varphi \quad \mbox{iff} \quad t \in L \qquad \mbox{for every tree $t$ over $\Sigma$}\]\"<\/p>\n

Examples of mso definable sets of trees include: “the number of nodes is divisible by 3” or “some root-to-leaf path has even length”.<\/p>\n

\n

Tree automata<\/strong><\/p>\n

Apart from mso, another mechanism of defining sets of trees (also known as tree languages) is to use automata. There also exist regular expressions for trees, but we do not discuss those here.<\/p>\n

A (nondeterministic)\u00a0tree automaton\u00a0<\/em>consists of:<\/p>\n

    \n
  • an input alphabet<\/em> \"\Sigma\", which is a ranked alphabet<\/li>\n
  • a finite set of states<\/em> \"Q\" with a distinguished accepting subset \"F \subseteq Q\"<\/li>\n
  • for every letter \"a \in \Sigma\" of rank \"n\", a transition\u00a0relation<\/em> \"\delta_a \subseteq Q^n \times Q\".<\/li>\n<\/ul>\n

    An automaton is called deterministic<\/em> if every transition relation is actually a function \"Q^n \to Q\". A run of the automaton over an input tree \"t\" is a labelling of tree nodes by states which is consistent with the transition relation in the following sense: if a node \"x\" has label \"a\" and its children have states \"q_1,\ldots,q_n\" then the state in node \"x\" satisfies <\/p>\n

      <\/span>   <\/span>\"\[ (q_1,\ldots,q_n,q) \in \delta_a.\]\"<\/p>\n

    Note that that this definition covers the special case of leaves; if a leaf has label \"a\" then the transition relation \"\delta_a \subseteq Q\" indicates what are the states allowed in leaves with state \"a\". Therefore, the transition relations for labels of rank zero can be viewed as initial states in the automaton. A tree is accepted<\/em> by the automaton if there is some run which has an accepting state in the root. Therefore, one can view the run of the automaton as a bottom-up pass through the tree, which is considered accepting if the last state (the root) has an accepting state. That is why the\u00a0automaton model described above is sometimes called a\u00a0bottom-up automaton;<\/em>\u00a0although the distinction between top-down or bottom-up makes most sense\u00a0when talking about deterministic automata.<\/p>\n

    The same proof as for automata on words, i.e. the subset construction, shows that tree automata can be determinised. The proof of the following theorem is skipped, it is a straightforward induction on the size of an mso formula. The\u00a0proof uses the fact that tree automata have all the closure properties that correspond to operators in mso formulas, such as Boolean combinations and projections (guessing).<\/p>\n

    Theorem<\/strong>. If a tree language \"L \subseteq \mathsf{trees}\Sigma\" is definable in mso, then it is recognised by some tree automaton.<\/p>\n

    The converse of the above theorem is also true, i.e. every language definable by a tree automaton can be defined in mso.<\/p>\n

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

    Finite trees and their automata. Apart from graphs, we will also use mso to define properties of trees (and their special case, words). Define a\u00a0ranked alphabet\u00a0to be a finite set where every element has an associated arity in . Here is a picture of a ranked alphabet: A tree over a ranked alphabet is defined […]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":1140,"menu_order":4,"comment_status":"open","ping_status":"closed","template":"","meta":{"_acf_changed":false,"inline_featured_image":false,"footnotes":""},"class_list":["post-1171","page","type-page","status-publish","hentry"],"acf":[],"_links":{"self":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/1171"}],"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=1171"}],"version-history":[{"count":5,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/1171\/revisions"}],"predecessor-version":[{"id":1210,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/1171\/revisions\/1210"}],"up":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/1140"}],"wp:attachment":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/media?parent=1171"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}