Differences

This shows you the differences between two versions of the page.

--- tree_automata [2010/05/27 18:10]
vkuncak
+++ tree_automata [2015/04/21 17:32]
@@ Line 1: / Line 1: @@
-====== Tree automata ======
-===== Finite Automata as Automata in Unary Language =====
-Consider a finite alphabet $\Sigma$.  A word $w \in \Sigma^*$ is a finite sequence of symbols from $\Sigma$.
-We can represent such a sequence as a term, as follows
-  * treat elements of $\Sigma$ as unary function symbols
-  * let $\epsilon$ be a constant symbol
-Represent $a_1 a_2 \ldots a_{n-1} a_n$ as a ground term
-\[
-   a_n(a_{n-1}(\ldots a_2(a_1(\epsilon))\ldots))
-\]
-We define the notion of [[finite state machine]] as accepting a set of such terms.
-===== Bottom up tree automata =====
-**Definition:**Given an alphabet ${\cal L}$, a non-deterministic bottom-up tree automaton in language ${\cal L}$ is $A = ({\cal L},Q,\Delta,F)$ where
-  * $Q$ is a set of states
-  * $F$ is the set of final states
-  * $\Delta$ is a set of rewrite rules
-\[
-    f(q_1,\ldots,q_n) \to q
-\]
-where $f$ is a function symbol of arity $n$ and where $q_1,\ldots,q_n,q \in Q$.
-Note: In the case of constant $a \in {\cal L}$ the transition has the form $a \to q$ and specifies possible initial states.
-A ground term in language ${\cal L}$ is accepted by the automaton iff it is possible to reach $q \in F$ by apply rewrite rules in $\Delta$ to term $t$.
-This rewriting process is a sequence of transitions $t \to t_1 \to \ldots \to t_k$ where $t_1,\ldots,t_k$ are terms in language ${\cal L} \cup Q$ with $Q$ being treated as constants of arity zero.
-**Definition:** A regular tree language is a set of terms accepted by a non-deterministic bottom-up tree automaton.
-Example:
-  * bottom up tree automaton checking the parity of the number of nodes in the tree
-Non-deterministic top-down tree automaton: reverse a bottom-up tree automaton
-Deterministic top-down tree automaton: more restrictive. Is there deterministic automaton to check the parity of the number of nodes?
-===== Closure Properties of Tree Automata ======
-**Definition:** We say bottom-up tree automaton is //deterministic// iff for every $f$ of arity $n$ and $q_1,\ldots,q_n \in Q$ there exists exactly one $q \in Q$ such that $f(q_1,\ldots,q_n) \in \Delta$.
-**Lemma:** For every bottom up tree automaton there exists a deterministic bottom up tree automaton accepting the same language.
-Closure under:
-  * union
-  * negation
-  * intersection
-Comparison to context-free grammars: closure under intersection and complement. Parser trees are regular, their yield is not.
-Projection.
-===== Weak Monadic Logic of Two Successors (WS2S) =====
-We generalize [[sav09:Weak Monadic Logic of One Successor]] to logic that allows quantification over finite subsets of an infinite binary tree.
-  * a finite subset $S$ of nodes in an infinite binary tree can be specified by listing, for each node in $S$, a path in the binary that leads to this node
-  * a path in a binary tree is a finite sequence of "left" and "right" moves from the root
-  * we encode each node as a string $w \in \{0,1\}^*$
-The domain $D$ of WS2S is the set of all finite subsets  $S \subseteq \{0,1\}^*$.
-Minimalistic syntax:
-\begin{equation*}
-  F ::= v \subseteq v \mid succ0(v,v) \mid succ1(v,v) \mid F \lor F \mid \lnot F \mid \exists v.F
-\end{equation*}
-We consider interpretations $(D,\alpha)$ where
-\[
-   \alpha({\subseteq}) = \{ (S_1,S_2) \mid S_1 \subseteq S_2 \}
-\]
-where $succ0$ takes a tree node and finds its left child:
-\[
-   \alpha(succ0) = \{ (\{w\},\{w0\}) \mid w \in \Sigma^* \}
-\]
-and where $succ1$ takes a tree node and finds its right child:
-\[
-   \alpha(succ1) = \{ (\{w\},\{w1\}) \mid w \in \Sigma^* \}
-\]
-The meaning of formulas is then given by standard [[sav08:First-order logic semantics]].
-===== Deciding WS2S =====
-A construction is similar to one for WS1S and is possible thanks to closure properties of finite automata.
-Examples:
-  * subset
-  * successor
-===== Verification of Trees =====
-[[TreeInsertion.java]]
-===== Infinite Trees =====
-S2S (without restriction to finite sets) is also decidable.  The proofs are much more complex:
-  * cannot use bottom-up automata
-  * complementation is difficult
-Key reference:
-  * {{sav08:rabin69s2s.pdf|Decidability of Second-Order Theories and Automata on Infinite Trees, by Michael O. Rabin}}
-===== References =====
-  * [[http://gforge.inria.fr/frs/download.php/3251/tata.pdf|Tree Automata Techniques and Applications]]
-  * [[http://richmodels.epfl.ch/lat|Logic and Automata Theory course]]