Finite Automata as Automata in Unary Language
Consider a finite alphabet . A word is a finite sequence of symbols from .
We can represent such a sequence as a term, as follows
- treat elements of as unary function symbols
- let be a constant symbol
Represent as a ground term
We define the notion of finite state machine as accepting a set of such terms.
Bottom up tree automata
Definition:Given an alphabet , a non-deterministic bottom-up tree automaton in language is where
- is a set of states
- is the set of final states
- is a set of rewrite rules
where is a function symbol of arity and where .
Note: In the case of constant the transition has the form and specifies possible initial states.
A ground term in language is accepted by the automaton iff it is possible to reach by apply rewrite rules in to term .
This rewriting process is a sequence of transitions where are terms in language with 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.
- 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 of arity and there exists exactly one such that .
Lemma: For every bottom up tree automaton there exists a deterministic bottom up tree automaton accepting the same language.
Comparison to context-free grammars: closure under intersection and complement. Parser trees are regular, their yield is not.
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 of nodes in an infinite binary tree can be specified by listing, for each node in , 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
The domain of WS2S is the set of all finite subsets .
We consider interpretations where
where takes a tree node and finds its left child:
and where takes a tree node and finds its right child:
The meaning of formulas is then given by standard First-order logic semantics.
A construction is similar to one for WS1S and is possible thanks to closure properties of finite automata.
Verification of Trees
S2S (without restriction to finite sets) is also decidable. The proofs are much more complex:
- cannot use bottom-up automata
- complementation is difficult