
%\documentstyle[11pt,zed]{csart}
\documentstyle{csart}

\begin{document}

\sloppy

\def\dotdot{\mathinner{\ldotp\ldotp}}

\def\parallel{\mathinner{\,\|\,}}

\def\cho#1#2#3{{\vcenter{\vbox{\hrule height.#3pt
		\hbox{\vrule width.#3pt height#2pt \kern#1pt
		\vrule width.#3pt}
		\hrule height.#3pt}}}}
\def\choi{\mathchoice\cho5{15}{48}\cho4{12}{45}\cho39{25}\cho26{21}}
\def\Choice{\mathop{\smash\choi\vphantom\sum}}

\def\choice{{\scriptstyle \Choice }}

\def\righti#1#2{{\mathclose>\llap{$#2\kern#1pt$}}}
\def\rightif{\mathchoice\righti{3}{\displaystyle|}\righti3{\textstyle|}\righti{2}{\scriptstyle|}\righti{2}{\scriptscriptstyle|}}
\def\lefti#1#2{{\mathopen<\llap{$#2\kern#1pt$}}}
\def\leftif{\mathchoice\lefti{2}{\displaystyle|}\lefti{2}{\textstyle|}\lefti{2}{\scriptstyle|}\lefti{1.5}{\scriptscriptstyle|}}


%\section{Problem}


``Handler'' process
\begin{eqnarray*}
\lefteqn{\mbox{{\bf H}}_i^P(Q_k, m) =} \\
   & & \left( \Choice_{j = 0}^\infty P_i.r.Q_j^I \rightarrow
   \left( \mbox{{\bf H}}_i^P(Q_j, m) \, \leftif Q_k = \mbox{NULL} \rightif \,
   Q_j.c.P_i^O \rightarrow \mbox{{\bf H}}_i^P(Q_k, m) \right) \right) \quad \choice \\
   & & \quad \left( Q_k.c.P_{i + 1}^O \rightarrow
		    \mbox{{\bf H}}_i^P(Q_k, \mbox{T}) \right) \quad \choice \\
   & & \left( \Choice_{j = 0}^\infty P_i.c.Q_j^I \rightarrow
       \left( \left (P_{i + 1}.r.Q_j^O \rightarrow \mbox{{\bf STOP}} \right)
       \, \leftif m \rightif  \,
       \vphantom{\mbox{{\bf H}}_i^P} \right. \right. \\
   & & \hspace{7em} \left. \vphantom{\Choice_{j = 0}^\infty} \left.
       \left( \mbox{{\bf H}}_i^P(Q_j, m) \, \leftif Q_k = \mbox{NULL} \rightif \,
       Q_k.c.P_i^O \rightarrow \mbox{{\bf H}}_i^P(Q_j, m) \right) \right) \right) \\
\end{eqnarray*}

``Supervisor'' process
\begin{displaymath}
\mbox{{\bf U}}_i^P = \Choice_{j = 0}^\infty P_i.r.Q_j^I \rightarrow
  \left( \Choice_{k = 0}^\infty Q_k.c.P_{i + 1}^O \rightarrow \mbox{{\bf STOP}}
  \right)
\end{displaymath}

An instance of a channel
\begin{displaymath}
\mbox{{\bf P}}_i = \mbox{{\bf U}}_i^P \parallel
  \mbox{{\bf H}}_i^P (\mbox{NULL}, \mbox{F})
\end{displaymath}

Define
\begin{eqnarray*}
\mbox{{\bf P}}_i^R (Q_k) & = &
  \left( \Choice_{l = 0}^\infty Q_l.c.P_{i + 1}^O \rightarrow
    \mbox{{\bf STOP}}_{\alpha (\mbox{{\bf U}}_i^P)} \right) \parallel
  \mbox{{\bf H}}_i^P (Q_k, \mbox{F}) \\
\mbox{{\bf P}}_i^C (Q_k) & = &
  \mbox{{\bf U}}_i^P \parallel \mbox{{\bf H}}_i^P (Q_k, \mbox{F}) \\
%\mbox{{\bf P}}_i^S       & = &
%   \Choice_{j = 0}^\infty P_i.c.Q_j^I \rightarrow
%			  P_{i + 1}.r.Q_j^O \rightarrow \mbox{{\bf STOP}}
\mbox{\bf P}_i^M (Q_k) & = & 
   Q_k.c.P_{i + 1}^O \rightarrow
  \left( \mbox{{\bf STOP}}_{\alpha (\mbox{{\bf U}}_i^P)} \parallel
  \mbox{{\bf H}}_i^P (Q_k, \mbox{T}) \right) \\
\end{eqnarray*}

The $\mbox{\bf P}_i$s can be expanded to
\begin{eqnarray*}
\mbox{\bf P}_i & = &
      \left( \Choice_{j = 0}^\infty P_i.r.Q_j^I \rightarrow
	     \mbox{\bf P}_i^R (Q_j) \right) \choice
      \left( \Choice_{j = 0}^\infty P_i.c.Q_j^I \rightarrow
	     \mbox{\bf P}_i^C (Q_j) \right) \\
\mbox{\bf P}_i^R (Q_k) & = & 
       \mbox{\bf P}_i^M (Q_k) \, \choice
       \left( \Choice_{j = 0}^\infty P_i.c.Q_j^I \rightarrow
	      Q_k.c.P_i^O \rightarrow \mbox{\bf P}_i^R (Q_j) \right) \\
\mbox{\bf P}_i^C (Q_k) & = & 
       \left( \Choice_{j = 0}^\infty P_i.r.Q_j^I \rightarrow
	      Q_j.c.P_i^O \rightarrow
	      \mbox{\bf P}_i^R (Q_k) \right) \choice
       \left( \Choice_{j = 0}^\infty P_i.c.Q_j^I \rightarrow
	      Q_k.c.P_i^O \rightarrow \mbox{\bf P}_i^C (Q_j) \right) \\
\mbox{\bf P}_i^M (Q_k) & = & 
       Q_k.c.P_{i + 1}^O \rightarrow
       \left( \Choice_{j = 0}^\infty P_i.c.Q_j^I \rightarrow
	P_{i + 1}.r.Q_j^O \rightarrow \mbox{\bf STOP} \right)
\end{eqnarray*}
\end{document}
