LARA

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

\begin{equation*} 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.

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

\begin{equation*} 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$.

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 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

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 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

\begin{equation*} \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:

\begin{equation*} \alpha(succ0) = \{ (\{w\},\{w0\}) \mid w \in \Sigma^* \} \end{equation*}

and where $succ1$ takes a tree node and finds its right child:

\begin{equation*} \alpha(succ1) = \{ (\{w\},\{w1\}) \mid w \in \Sigma^* \} \end{equation*}

The meaning of formulas is then given by standard 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:

References