- English only

# Lab for Automated Reasoning and Analysis LARA

# 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] (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]]. |