Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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