\begin{slide}{Beschränkte Rekursion}
  beliebige Rekursion kann zu unendlichen Zustandsgraphen
  und nicht-regulären (Spur-)Sprachen führen.

  Falls das nicht gewünscht ist, dann Syntax einschränken:
  \begin{itemize}
  \item 
    $\mu P . (( a \to P ; c ) \Box b)$

    Spursprache: \dots

    Folgerung: Einschränken auf rechts-lineare Ausdrücke
    ($P$ darf niemals links von \verb|;| stehen)
  \item
    Simulation von \verb|;| durch $\|_S$:

    $\mu P . ((a \to P \|_{a} ac) \Box b)$

    Folgerung: $P$ darf gar nicht in $\|_S$ vorkommen
  \end{itemize}

\end{slide}
