\begin{slide}{Endliche Systeme}

für $P\in\Proc(\Sigma)$:
Menge der von $P$ aus
durch Folgen von $a$-- und $\tau$--Schritten
erreichbaren Prozesse (Terme) ist endlich,


\begin{itemize}
\item die meisten Inferenzeregeln erzeugen 
  nur echte Teilterme 
\item beachte: Komposition $\|_S$
\item beachte: Fixpunkt-Operator (Rekursion)

  $\mu P. (\ldots P \ldots)$
\end{itemize}

  
einfache Lösung: Einschränkung auf End-Rekursion

$\mu P . (\dots P)$

vergleiche: rechtslineare Grammatiken

\end{slide}
