Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
tree_automata [2010/05/27 18:10]
vkuncak
tree_automata [2015/04/21 17:32] (current)
Line 10: Line 10:
  
 Represent $a_1 a_2 \ldots a_{n-1} a_n$ as a ground term Represent $a_1 a_2 \ldots a_{n-1} a_n$ as a ground term
-\[+\begin{equation*}
    ​a_n(a_{n-1}(\ldots a_2(a_1(\epsilon))\ldots))    ​a_n(a_{n-1}(\ldots a_2(a_1(\epsilon))\ldots))
-\]+\end{equation*}
  
 We define the notion of [[finite state machine]] as accepting a set of such terms. We define the notion of [[finite state machine]] as accepting a set of such terms.
Line 23: Line 23:
   * $F$ is the set of final states   * $F$ is the set of final states
   * $\Delta$ is a set of rewrite rules   * $\Delta$ is a set of rewrite rules
-\[+\begin{equation*}
     f(q_1,​\ldots,​q_n) \to q     f(q_1,​\ldots,​q_n) \to q
-\]+\end{equation*}
 where $f$ is a function symbol of arity $n$ and where $q_1,​\ldots,​q_n,​q \in Q$. where $f$ is a function symbol of arity $n$ and where $q_1,​\ldots,​q_n,​q \in Q$.
  
Line 37: Line 37:
  
 Example: Example:
-  * bottom up tree automaton ​checking the parity of the number of nodes in the tree+  * bottom up tree automaton ​accepting trees with an even number of nodes in the tree, in alphabet with constant '​a',​ binary function '​f'​. 
 +  * bottom up tree automaton accepting expressions with complement, union, intersection;​ accepting only expressions that are monotonic in each variable
  
 Non-deterministic top-down tree automaton: reverse a bottom-up tree automaton 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? 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 ====== ===== Closure Properties of Tree Automata ======
Line 77: Line 75:
  
 We consider interpretations $(D,​\alpha)$ where We consider interpretations $(D,​\alpha)$ where
-\[+\begin{equation*}
    ​\alpha({\subseteq}) = \{ (S_1,S_2) \mid S_1 \subseteq S_2 \}    ​\alpha({\subseteq}) = \{ (S_1,S_2) \mid S_1 \subseteq S_2 \}
-\]+\end{equation*}
 where $succ0$ takes a tree node and finds its left child: where $succ0$ takes a tree node and finds its left child:
-\[+\begin{equation*}
    ​\alpha(succ0) = \{ (\{w\},​\{w0\}) \mid w \in \Sigma^* \}    ​\alpha(succ0) = \{ (\{w\},​\{w0\}) \mid w \in \Sigma^* \}
-\]+\end{equation*}
 and where $succ1$ takes a tree node and finds its right child: and where $succ1$ takes a tree node and finds its right child:
-\[+\begin{equation*}
    ​\alpha(succ1) = \{ (\{w\},​\{w1\}) \mid w \in \Sigma^* \}    ​\alpha(succ1) = \{ (\{w\},​\{w1\}) \mid w \in \Sigma^* \}
-\]+\end{equation*}
  
 The meaning of formulas is then given by standard [[sav08:​First-order logic semantics]]. The meaning of formulas is then given by standard [[sav08:​First-order logic semantics]].
 
tree_automata.txt · Last modified: 2015/04/21 17:32 (external edit)
 
© EPFL 2018 - Legal notice