Differences
This shows you the differences between two versions of the page.
tree_automata [2010/05/25 15:33] 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(succ) = \{ (\{w\},\{w0\}) \mid w \in \Sigma^* \} | ||
- | \] | ||
- | and where $succ1$ takes a tree node and finds its right child: | ||
- | \[ | ||
- | \alpha(succ) = \{ (\{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]] | ||