\begin{slide}{Bestimmung einer Bisimulation (Plan)}

\begin{itemize}\itemsep 2pt \parskip 2pt
\item Eingabe: Systeme $(S_1, S_2)$
\item berechne Folge von Relationen $R_0, R_1 \ldots \subseteq Q_1\times Q_2$

  wobei $(p_1, p_2)\in R_k \iff$ $p_1$ in $S_1$ und $p_2$ in $S_2$
  verhalten sich für Transitionsfolgen der Länge $\le k$ \glqq gleich\grqq
\item Folge ist monoton fallend bzgl. Inklusion: 
  $Q_1\times Q_2 = R_0 \supseteq R_1
  \supseteq R_2 \supseteq \ldots$
\item falls diese Folge schließlich stationär ist ($\exists n: R_n=R_{n+1}$),
  dann teste, ob dieses $R_n$ eine Bisimulation für $(S_1, S_2)$ ist.
\end{itemize}
Sätze: Korrektheit, Vollständigkeit,

Termination für endliche $Q_1, Q_2$.

\bigskip

vergleiche: Verfahren zur Minimierung von Automaten
(Tabelle zur Markierung nicht äquivalenter Zustände)

\end{slide}

\begin{slide}{Bestimmung einer Bisimulation (Impl.)}

aus Definition \glqq $R$ ist Bisimulation\grqq:
\begin{itemize}
\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 und symmetrisch ($1 \leftrightarrow 2$)
\end{itemize}

leite Verfeinerungsverfahren ab: 

gegeben $R_k$, definiere $R_{k+1}$ durch:
 
$(p_1, p_2)\in R_{k+1}$, falls $(p_1,p_2)\in R_k$ und
\begin{itemize}
\item 
$ \forall (p_1,a,q_1)\in T_1:
\exists q_2:  (p_2, a, q_2)\in T_2 \wedge (q_1, q_2)\in R_k$
\item und symmetrische Bedingung (tausche $1 \leftrightarrow 2$)
\end{itemize}







\end{slide}
