\newcommand{\range}{\operatorname{range}}
\newcommand{\domain}{\operatorname{domain}}

\begin{slide}{Definition}

Zustandsübergangssystem $S=(\Sigma, Q, T, i)$ 

(Alphabet $\Sigma$, Zustandsmenge $Q$, \\
Transitionen $T\subseteq Q\times \Sigma\times Q$, 
Startzustand $i\in Q$)

\bigskip

Relation $R\subseteq Q_1\times Q_2$ ist Bisimulation
zwischen $S_1$ und $S_2$, falls:

\begin{itemize}\itemsep 3pt\parskip 3pt
\item Vor- und Nachbereich groß genug: $\domain R = Q_1, \range R = Q_2$
\item Startzustände sind bisimilar: $(i_1, i_2)\in R$
\item $S_1$-Transitionen durch $S_2$-Transitionen simuliert:
  
  $\forall (p_1, p_2)\in R: \forall (p_1,a,q_1)\in T_1:$ \\
  \qquad $ \exists q_2:  (p_2, a, q_2)\in T_2 \wedge (q_1, q_2)\in R$
\item $S_2$-Transitionen durch $S_1$-Transitionen simuliert 

  Ü: Diagramm zeichnen, Formel hinschreiben
\end{itemize}


\end{slide}
