\begin{slide}{Nebenläufige Komposition}

\dots mit Synchronisation

\begin{itemize}
\item Syntax: $(P_1 \|_S P_2)$ für $S\subseteq \Sigma$
\item Semantik
  \begin{itemize}
  \item informal: Ereignisse aus $S$ \\ sollen in 
    $P_1$ und $P_2$ synchron ausgeführt werden,

    Ereignisse $\notin S$ beliebig (asynchron)
  \item formal (Inferenzregeln): \dots
  \end{itemize}
\end{itemize}
beachte Spezialfälle $S=\emptyset, S=\Sigma$.


\end{slide}
