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

\begin{document}

\sloppy

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

\def\parallel{\mathinner{\,\|\,}}
\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|}}

\newcommand{\proc}[1]{\mbox{\bf {#1}}}
\newcommand{\symbol}[1]{\mbox{\it {#1}}}
\newcommand{\function}[1]{\mbox{\it {#1}} \,}

\def\satisfies{\, \, \mbox {\bf sat}\, \,}

\def\lbag{[[}
\def\rbag{]]}

\def\ndchoice{\sqcap}
\def\suchthat{\, | \,}
\def\concat{\hat{\mbox{ }}}

\def\bif{\mbox{\bf if}\, \,}
\def\bthen{\, \, \mbox{\bf then}\, \,}
\def\belse{\, \, \mbox{\bf else}\, \,}

\def\powset{\mbox{P}}

\section{Static Channel System}

     Introduce the $n$-ary relation on natural numbers
\begin{eqnarray*}
     \function{prog} (a_0, \ldots , a_{n-1}) & = &
       a_{n-1} + 1 \geq a_0 \geq \ldots \geq a_{n - 1}
\end{eqnarray*}
$\symbol{prog}$ is short for {\em progression}.  Now, if $s$ is a
sequence of events of length $n$, introduce the predicate
\begin{eqnarray*}
  \function{cycle} (s) (\symbol{tr}, \symbol{ref}) & = &
    \function{prog} (\symbol{tr} \downarrow s_0, \ldots,
		     \symbol{tr} \downarrow s_{n - 1}) \land \\ & &
    ( ((\symbol{tr} \downarrow s_0 = \symbol{tr} \downarrow s_{n - 1})
      \land s_0 \not\in \symbol{ref}) \lor \\ & &
    \exists i : 1 \dotdot n - 1 \cdot 
          ((\symbol{tr} \downarrow s_i < \symbol{tr} \downarrow s_{i - 1})
	  \land s_i \not\in \symbol{ref}) )
\end{eqnarray*}
(A process with this specification has the implementation
\begin{eqnarray*}
& \mu \proc{X} \cdot
  s_0 \rightarrow \ldots \rightarrow s_{n - 1} \rightarrow \proc{X})
\end{eqnarray*}
For the purposes of this section, a ``channel'', $\proc{C}$,
is a process with alphabet
\begin{displaymath}
  \{ C.d^O, C.d^I, C.a^O, C.a^I \}
\end{displaymath}
satisfying the specification
$\function{channel} (C) (\symbol{tr}, \symbol{ref})$ where
\begin{eqnarray*}
\function{channel} (C) & = &
  \function{cycle} (\langle C.d^O, C.d^I, C.a^O, C.a^I \rangle )
\end{eqnarray*}
A system of channels with disjoint alphabets satisfy
\begin{eqnarray*}
\left( \Parallel_{C \in S} \proc{C} \right) & \satisfies &
  \forall C : S \cdot \function{channel} (C) (\symbol{tr}, \symbol{ref})
\end{eqnarray*}
Introduce the specifications
\begin{eqnarray*}
  \function{out-buf} (C) & = &
    \function{cycle} (\langle C.d^O, C'.d^O, C'.a^I, C.a^I \rangle ) \\
  \function{in-buf} (C) & = &
    \function{cycle} (\langle C'.d^I, C.d^I, C.a^O, C'.a^O \rangle )
\end{eqnarray*}
and suppose that $\proc{T}$ is a message delivery system with
$M = \bigcup_{C \in S} \{C'.d, C'.a\}$.
A distributed channel system is defined by
\begin{eqnarray*}
  \proc{D} = \left( \Parallel_{C \in S}
		    \proc{C}^{out} \parallel \proc{C}^{in} \right) \parallel
             \proc{T}
\end{eqnarray*}
where
\begin{eqnarray*}
\proc{C}^{out} & \satisfies & \function{out-buf} (C) (tr, ref) \\
\proc{C}^{in}  & \satisfies & \function{in-buf}  (C) (tr, ref)
\end{eqnarray*}

\subsection*{Theorem:}

If the set of primed events
$\alpha \proc{T} = \bigcup_{C \in S} \{C'.d^O, C'.d^I, C'.a^O, C'.a^I\}$
is concealed, $\proc{D}$ implements a channel system, ie
\begin{eqnarray*}
\proc{D} \backslash \alpha \proc{T} & \satisfies &
  \forall C : S \cdot \function{channel} (C) (\symbol{tr}, \symbol{ref})
\end{eqnarray*}

\subsection*{Proof:}

From the properties of alphabet-disjoint cycles and the parallel
composition rule
\begin{eqnarray*}
\proc{D} & \satisfies & \function{dist-chan} (\symbol{tr}, \symbol{ref})
\end{eqnarray*}
where
\begin{eqnarray*}
\function{dist-chan} (\symbol{tr}, \symbol{ref}) & = &
  \exists X:\powset \alpha \proc{D} \cdot
  \exists Y:\powset \alpha \proc{T} \cdot
			\symbol{ref} = X \cup Y \land \\ & &
  \function{buffers} (\symbol{tr}, X)  \land
  \function{router} (\symbol{tr}, Y)
\end{eqnarray*}
and
\begin{eqnarray*}
  \function{buffers} (\symbol{tr}, \symbol{ref}) & = &
  \left( \forall C:S \cdot
    \function{out-buf} (C) (\symbol{tr}, \symbol{ref}) \land
    \function{in-buf}  (C) (\symbol{tr}, \symbol{ref}) \right) \\
  \function{router} (\symbol{tr}, \symbol{ref}) & = &
		     (M^O \cap \symbol{ref}) = \emptyset \land \\ & &
   \left( (\function{pending-ins}  (tr) \neq \emptyset ) \Rightarrow
   (\function{pending-ins}  (tr) \not\subset \symbol{ref}) \right) \land \\ & &
		      \function{pending-outs} (tr) = \emptyset
\end{eqnarray*}
The combined trace restrictions in $\symbol{buffers}$ and
$\symbol{router}$ imply
\begin{displaymath}
    \function{prog} (\symbol{tr} \downarrow C.d^O,
                     \symbol{tr} \downarrow C'.d^O,
                     \symbol{tr} \downarrow C'.d^I,
                     \symbol{tr} \downarrow C.d^I,
                     \symbol{tr} \downarrow C.a^O,
                     \symbol{tr} \downarrow C'.a^O,
                     \symbol{tr} \downarrow C'.a^I,
                     \symbol{tr} \downarrow C.a^I)
\end{displaymath}
for any $C$, because
\begin{displaymath}
    \function{prog} (\symbol{tr} \downarrow C.d^O,
                     \symbol{tr} \downarrow C'.d^O,
                     \symbol{tr} \downarrow C'.a^I,
                     \symbol{tr} \downarrow C.a^I)
\end{displaymath}
and
\begin{displaymath}
    \function{prog} (\symbol{tr} \downarrow C'.d^I,
                     \symbol{tr} \downarrow C.d^I,
                     \symbol{tr} \downarrow C.a^O,
                     \symbol{tr} \downarrow C'.a^O)
\end{displaymath}
and $\function{pending-outs} (tr) = \emptyset$ implies
\begin{displaymath}
    (\symbol{tr} \downarrow C'.d^O \geq \symbol{tr} \downarrow C'.d^I) \land
    (\symbol{tr} \downarrow C'.a^O \geq \symbol{tr} \downarrow C'.a^I)
\end{displaymath}
so that the second progression can be inserted into the first.
Combining the long progression with the specification of the
buffers (and using some elementary properties of progressions) we get
\begin{eqnarray*}
  \forall C:S & \cdot &
     ((\symbol{tr} \downarrow C.d^O = \symbol{tr} \downarrow C.a^I) \land
       C.d^O \not\in X \land C'.d^I \not\in X) \lor \\ & &
     ((\symbol{tr} \downarrow C'.d^O < \symbol{tr} \downarrow C.d^O) \land
       C'.d^O \not\in X \land C'.d^I \not\in X) \lor \\ & &
     ((\symbol{tr} \downarrow C'.d^I < \symbol{tr} \downarrow C'.d^O) \land
       C'.a^I \not\in X \land C'.d^I \not\in X) \lor \\ & &
     ((\symbol{tr} \downarrow C.d^I < \symbol{tr} \downarrow C'.d^I) \land
       C'.a^I \not\in X \land C.d^I \not\in X) \lor \\ & &
     ((\symbol{tr} \downarrow C.a^O < \symbol{tr} \downarrow C.d^I) \land
       C'.a^I \not\in X \land C.a^O \not\in X) \lor \\ & &
     ((\symbol{tr} \downarrow C'.a^O < \symbol{tr} \downarrow C.a^O) \land
       C'.a^I \not\in X \land C'.a^O \not\in X) \lor \\ & &
     ((\symbol{tr} \downarrow C'.a^I < \symbol{tr} \downarrow C'.a^O) \land
       C'.a^I \not\in X \land C'.d^I \not\in X) \lor \\ & &
     ((\symbol{tr} \downarrow C.a^I < \symbol{tr} \downarrow C'.a^I) \land
       C.a^I \not\in X \land C'.d^I \not\in X)
\end{eqnarray*}
When the events in $\alpha \proc{T}$ are concealed, we will be interested
in $X$ and $Y$ for which $\alpha \proc{T} \subset (X \cup Y)$.
Since $(M^O \cap Y) = \emptyset $ this means that $M^I \subset X$.
This eliminates the second and sixth terms in the disjunction above.
Now consider the subset $s$ of $S$ whose elements satisfy
\begin{displaymath}
     (\symbol{tr} \downarrow C'.d^I < \symbol{tr} \downarrow C'.d^O) \lor
     (\symbol{tr} \downarrow C'.a^I < \symbol{tr} \downarrow C'.a^O)
\end{displaymath}
For these channels $C'.a^I \not\in X \land C'.d^I \not\in X$.  So
$\bigcup_{C \in s} \{C'.d, C'.a\}$ includes all messages
in transit, and the corresponding set of input events don't
intersect $X$, so it must be contained in $Y$.
If $s$ is non-empty this is a contradiction with
$(\function{pending-ins} (tr) \neq \emptyset ) \Rightarrow
 (\function{pending-ins} (tr) \not\subset \symbol{Y})$,
so $s$ must be empty.
This eliminates the third and seventh terms in the disjunction,
leaving just
\begin{eqnarray*}
  \forall C:S & \cdot &
     ((\symbol{tr} \downarrow C.d^O = \symbol{tr} \downarrow C.a^I) \land
       C.d^O \not\in X \land C'.d^I \not\in X) \lor \\ & &
     ((\symbol{tr} \downarrow C.d^I < \symbol{tr} \downarrow C.d^O) \land
       C'.a^I \not\in X \land C.d^I \not\in X) \lor \\ & &
     ((\symbol{tr} \downarrow C.a^O < \symbol{tr} \downarrow C.d^I) \land
       C'.a^I \not\in X \land C.a^O \not\in X) \lor \\ & &
     ((\symbol{tr} \downarrow C.a^I < \symbol{tr} \downarrow C.a^O) \land
       C.a^I \not\in X \land C'.d^I \not\in X)
\end{eqnarray*}
which implies
\begin{displaymath}
  \forall C : S \cdot \function{channel} (C) (\symbol{tr}, X),
\end{displaymath}
so if $(\symbol{ref} \cap \alpha \proc{T}) = \emptyset $
\begin{eqnarray*}
  \function{dist-chan} (\symbol{tr},
			\symbol{ref} \cup \alpha \proc{T}) & \Rightarrow &
  \exists X:\powset \alpha \proc{D} \cdot
  \exists Y:\powset \alpha \proc{T} \cdot
			\symbol{ref} = X \cup Y \land \\ & &
  \forall C:S \cdot \function{channel} (C) (\symbol{tr}, X) \\
  & \Rightarrow &
  \forall C:S \cdot \function{channel} (C) (\symbol{tr}, \symbol{ref}) \\
\end{eqnarray*}
This establishes the theorem by application of the rule for
hiding (divergence freedom follows from the
interleaving of ``primed'' and ``unprimed'' events).
\end{document}

