\begin{slide}{Spur-Semantiken}

bis jetzt: Zustandsübergangssystem
\begin{itemize}
\item Zustände $=$ Prozeß-Terme, 
\item Übergänge $\stackrel{a}{\to}$ 
  und $\stackrel{\tau}{\to}$ 
\end{itemize}
entspricht: (endlicher) Automat mit Epsilon-Übergängen

jetzt: Vergleich solcher Systeme (Automaten)
durch Beobachtungen.
\begin{itemize}
\item (bekannt) Aktionen sind beobachtbar

  denotationale Semantik des System ist Spur-Sematik:
  Menge aller möglichen Aktionsfolgen
\item (neu) Deadlocks sind beobachtbar,
  Verfeinerung der Spur-Semantik
\end{itemize}

\end{slide}

\newcommand{\rej}{\operatorname{rej}}

\begin{slide}{Spur/Ablehnungs-Semantik}

Spur:
  \begin{itemize}
  \item Ein-Schritt-Relation: \dots
  \item Mehr-Schritt-Relation: \dots
  \end{itemize}

Ablehnung:
  \begin{itemize}
  \item $P \in \Proc(\Sigma)$ heißt \emph{stabil},
    wenn $\neg\exists Q \in \Proc(\Sigma): 
    P\stackrel{\tau}{\to} Q$
\item stabiler $P \in \Proc(\Sigma)$ 
  \emph{lehnt} $A\subseteq \Sigma$ \emph{ab},

  wenn $\neg\exists a\in A, Q\in \Proc(\Sigma): 
  P\stackrel{a}{\to} Q$
  \end{itemize}

Ablehnungs-Semantik $\rej(P)$
Menge aller Paare von Spur und Ablehnungsmenge
am Ende der jeweiligen Spur.

\end{slide}
