\begin{slide}{Baum-Automaten (I)}

\emph{Literatur:} Gecseg/Steinby: Tree Automata (1984),
Comon et al.: TATA (Tree automata Techniques and Applications) (2000--),
\url{http://www.grappa.univ-lille3.fr/tata/}

\emph{Definition:} Ein Baumautomat $A=(\Sigma, Q,F,R)$ besteht aus
\begin{itemize}\itemsep 0pt\parskip 2pt
\item
  Alphabet $A$,
$\bullet$
  Zustandsmenge $Q$
\item
  Menge der akzeptierenden Zustände $F \subseteq Q$
\item
  Regelmenge $R$ mit Regeln der Form
  \( f(q_1,\ldots,q_k)\to q \)
  mit $f\in \Sigma, k\ge 0, q_1,\ldots,q_k\in Q, q\in Q$.
\end{itemize}
Beispiel: $\Sigma=\{F,T,\vee,\wedge\}, Q=\{0,1\}, F=\{1\},$

$R=\{F\to 0,T\to 1,0
\vee 0\to 0,0\vee 1\to 1,1\vee 0\to 1,1\vee 1\to 1,
0\wedge 0\to 0,0\wedge 1\to 0,1\wedge 0\to 0,1\wedge 1\to 1\}$.

\end{slide}

\begin{slide}{Baum-Automaten (II)}

Eine \emph{Rechnung} von $A$ mit Eingabeterm $t$
ist eine Folge von Regelanwendungen.

Beispiel: Eingabe $t=F\vee(T\wedge F)$, 
Rechnung $F\vee(T\wedge F)\to 0\vee(T\wedge F) 
\to 0 \vee(1\wedge F) \to 0 \vee(1\wedge 0) \to 0 \vee 0 \to 0$.

Eine \emph{akzeptierende} Rechnung endet mit einem $q\in F$.
Wir schreiben $t\to_R^* q\in F$.

Die Sprache des Automaten ist $L(A)=\{t \mid \exists q\in F: t\to_R^*q \}$.

Die Sprache des Beispiel-Automaten 
sind genau die Formeln mit Wahrheitswert 1.

Übung: warum gibt es in Baum-Automaten keine Startzustände?

Übung: geben Sie einen Baumautomaten
für die Menge  aller allgemeingültigen aussagenlogischen Formeln
über dem Alphabet $\{x,T,F,\neg,\vee,\wedge\}$
mit einer Variablen $x$ an (Beispiel:  $x \vee \neg x$ gehört dazu.)
Hinweis: der Automat hat 4 Zustände.

\end{slide}
