\newcommand{\Pow}{\operatorname{Pow}}
\newcommand{\trace}{\operatorname{trace}}

\begin{slide}{Plan}

betrachten Zustandsübergangssysteme allgemein
(Beispiele: endliche Automaten, Petri-Netze, CSP)

\bigskip

Semantiken und durch sie definierte Äquivalenzen:
\begin{itemize}\itemsep 2pt \parskip 2pt
\item Spur-Semantik $\trace (S) \subseteq \Sigma^*$ 

  $S_1$ spur-äquivalent zu $S_2$, falls $\trace(S_1)=\trace(S_2)$.

\item Ablehnungs-Semantik $\rej(S) \subseteq \Sigma^* \times \Pow(\Sigma)$

  $S_1$ ablehnungs-äquivalent zu $S_2$, falls $\rej(S_1)=\rej(S_2)$.
\item Bisimulation:
  $S_1$ \emph{bisimilar} zu $S_2$, falls eine Relation (\emph{Bisimulation})
  $R \subseteq \states(S_1)\times \states(S_2)$ 
  mit bestimmten Eigenschaften existiert
\end{itemize}

\end{slide}

