\newcommand{\STOP}{\operatorname{STOP}}
\newcommand{\Proc}{\operatorname{Proc}}
\newcommand{\ec}{\operatorname{\Box}}
\newcommand{\ic}{\operatorname{\sqcap}}

\begin{slide}{Die Prozeß-Algebra (Syntax)}

Terme zur Beschreibung von Prozessen

(vgl. reguläre Ausdrücke 
zur Beschreibung von Sprachen)


Menge $\Proc(\Sigma)$ der
Prozeß-Terme über einem Alphabet $\Sigma$
von atomaren Aktionen:
\begin{itemize}\itemsep 0pt
\item $\STOP \in \Proc(\Sigma) $ 
\item Präfix: $a\in \Sigma \wedge P\in \Proc 
  \Rightarrow (a\to P)\in\Proc$
\item external choice: 
  $P_i\in\Proc(\Sigma) \Rightarrow ( P_1 \ec P_2) \in \Proc(\Sigma)$
\item internal choice: 
  $P_i\in\Proc(\Sigma) \Rightarrow ( P_1 \ic P_2) \in \Proc(\Sigma)$
\end{itemize}
und weitere Operatoren (später)
\begin{itemize}
\item Fixpunkt (für Iteration)
\item Verschränkung (für nebenläufige Ausführung)
\end{itemize}


\end{slide}

\begin{slide}{Die Prozeß-Algebra (operationale Semantik)}

durch Inferenz-System ($=$ Axiome, Schlußregeln) \\
für die Übergangsrelation zwischen Prozessen

\bigskip

$P_1 \stackrel{a}{\to} P_2$ bedeutet für $a\in\Sigma$: 
Prozeß $P_1$ führt $a$ aus (sichtbar)
und verhält sich danach wie  Prozeß $P_2$

\bigskip

$P_1 \stackrel{\tau}{\to} P_2$ bedeutet (mit $\tau \notin\Sigma$)
Prozeß $P_1$ führt eine nicht sichtbare Aktion aus
und verhält sich danach wie  Prozeß $P_2$


\begin{itemize}
\item Axiom $(a \to P)\stackrel{a}{\to} P$
\item Axiome $(P_1\ic P_2)\stackrel{\tau}{\to} P_1$
  und  $(P_1\ic P_2)\stackrel{\tau}{\to} P_2$
\item Schlußregel: 

wenn $P\stackrel{a}{\to} Q$,
  dann $(P \ec P') \stackrel{a}{\to} Q$
  und $(P' \ec P)  \stackrel{a}{\to} Q$
\end{itemize}

\end{slide}

