\begin{slide}{Ersetzungssysteme und Programmanalyse}

\begin{itemize}
\item
  $R$ ein Ersetzungssystem, $L$ eine Sprache (Menge) von Bäumen,
  \[ R^*(L) = \{ t \mid \exists s\in L: s\to_R^* t \} \]
  alle Mehr-Schritt-Nachfolger von $L$. 
\item
  modelliert: $R$ ein Programm, $L$ eine Menge von (möglichen) Eingaben,
  dann $R^*(L)$ Menge von erreichbaren Zuständen (Zwischenergebnissen)
\item
  $E$ eine Menge von verbotenen Zuständen.
  Kein verbotener Zustand erreichbar: $R^*(L) \cap E = \emptyset$
\item
  Beispiel: durch XSLT-Transformation soll immer
  Schema-konformes Dokument entstehen
\end{itemize}

\end{slide}

\begin{slide}{Ersetzung und Automaten (Regularität)}

\begin{itemize}
\item  Normalformen
  \begin{itemize}
  \item
    Normalformen für $\{fgfg \to \dots\}$?
  \item
    Normalformen für $\{ A(A(D,x),y)\to\dots \}$?
  \item
    Ist Menge der Normalformen immer regulär? (Nein.)
  \end{itemize}
\item Nachfolgermengen
  \begin{itemize}
  \item
    $L$ und $E$ durch endliche (Baum-)Automaten beschrieben.
    Wie kann man $R^*(L) \cap E = \emptyset$ entscheiden?
  \item
    im Allgemeinen gar nicht, wg. Halteproblem
  \item in Einzelfällen doch

    $\Sigma=\{a,b\}, R=\{aa\to aba\}, L=a^*, E = \Sigma^* bb \Sigma^*$
  \end{itemize}
\end{itemize}


\end{slide}
