%From rvg@Sunburn.Stanford.EDU Mon Oct 26 17:14:04 1992
%Updates by sas@cs.sunysb.edu to abstract, intro, concl. on 10/23/92 
%Updates by bus@zeus.informatik.rwth-aachen.de on 10/25/92
%Updates by sas@cs.sunysb.edu performed on 7/3/94-7/22/94
%Updates by rvg@cs.stanford.edu performed on 7/7/94-7/21/94
\documentstyle[11pt]{article}
\oddsidemargin  0pt
\evensidemargin 0pt             % 1 inch margin comes for free
\topmargin      0pt             % 4 margins of 1in each
\headheight     0pt             % default 12pt = 0.42cm       
\headsep        0pt             % default 25pt = 0.88cm       
\textwidth    6.5in             % paper = 8.5x11in
\textheight   8.58in            %  + foot 30pt = 9.00in
\parskip      0.075in           % distance between the paragraphs
\unitlength   0.8cm             % this is used in pictures
\linethickness{.4mm}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%	     On A4 paper the right margin is 6 mm smaller,	   %%%%
%%%%	     whereas the bottom margin is 17.6 mm longer.	   %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newlength{\shiftside}			 \newlength{\shifttop}
\setlength{\shiftside}{-3mm}		 \setlength{\shifttop}{8.8mm}
\typeout{On what kind of paper are you going to print this?}
\typein[\paper]{Enter 0 for American paper or 1 for A4.}
\addtolength\oddsidemargin{\paper\shiftside}
\addtolength\evensidemargin{\paper\shiftside}
\addtolength\topmargin{\paper\shifttop}

%%%%%%%%%%%%%%%%%%%%%%%\input{drawtexmacros.tex}%%%%%%%%%%%%%%%%%%%%%%%
%----------------------------------------------------------------------
% podar@sbcs (Sunil Podar) Nov 26, 1985.
% Dept. of Computer Science, SUNY at Stony Brook.
% You may use this file in whatever way you wish. You are requested to 
% leave this notice intact, and report any bugs, enhancements, etc. back
% to:
% CSNET: podar@sbcs.csnet
% ARPA: podar%suny-sb.csnet@csnet-relay.arpa
% UUCP: {allegra, hocsd, philabs, ogcvax}!sbcs!podar
%----------------------------------------------------------------------
% to include this file,type:
% \input{/users/podar/Latex/macros/picture}
%
% This file contains implementation of:
% \multiputlist
% \grid
% \hdashline
% \vdashline
% \thindots
% \thickdots
% \dotdashline
% \dottedline
% \drawline
% dottedjoin environment
% dotdashjoin environment
% linejoin environment
% \joinput
%
% For documentation, see the accompanying manual.
%----------------------------------------------------------------------
\makeatletter
%----------------------------------------------------------------------
% usage: \multiputlist(x,y)(delta-x,delta-y)[tbrl]{item1,item2,item3,.....}
%
\def\lop#1\to#2{\expandafter\lopoff#1\lopoff#1#2}
\long\def\lopoff,#1,#2\lopoff#3#4{\def#4{#1}\def#3{,#2}}
\def\@@mlistempty{,}
\newif\iflistnonempty
\def\multiputlist(#1,#2)(#3,#4){\@ifnextchar
[{\@imultiputlist(#1,#2)(#3,#4)}{\@imultiputlist(#1,#2)(#3,#4)[]}}

\long\def\@imultiputlist(#1,#2)(#3,#4)[#5]#6{%
\@xdim=#1\unitlength
\@ydim=#2\unitlength
\listnonemptytrue \def\@@mlist{,#6,} % need this for end condition
\loop
\lop\@@mlist\to\@@firstoflist
\@killglue\raise\@ydim\hbox to\z@{\hskip
\@xdim\@imakepicbox(0,0)[#5]{\@@firstoflist}\hss}
\advance\@xdim #3\unitlength\advance\@ydim #4\unitlength
\ifx\@@mlist\@@mlistempty \listnonemptyfalse\fi
\iflistnonempty
\repeat\relax
\ignorespaces}
%----------------------------------------------------------------------
%\grid(width,height)(delta-width,delta-height)[initial-X-integer,initial-Y-integer]
% usage: 1. \put(0,0){\grid(95,100)(9.5,10)}
%        2. \put(0,0){\grid(100,100)(10,5)[-10,0]}
%        or \put(0,0){\tiny \grid(100,100)[0,0]} % the numbers in \tiny font.
\newcount\delta
\newdimen\@delta
\newdimen\@@delta
\newcount\@gridcnt
\def\grid(#1,#2)(#3,#4){\@ifnextchar [%
{\@igrid(#1,#2)(#3,#4)}%
{\@igrid(#1,#2)(#3,#4)[@,@]}}

\long\def\@igrid(#1,#2)(#3,#4)[#5,#6]{%
\makebox(#1,#2){%
\@delta=#1pt\@@delta=#3pt\divide\@delta by\@@delta\delta=\@delta%
\advance\delta by 1\relax\message{grid=\the\delta\space x}%
\multiput(0,0)(#3,0){\delta}{\line(0,1){#2}}%
\ifx#5@\relax\else%
\global\@gridcnt=#5%
\multiput(0,0)(#3,0){\delta}{%
\makebox(0,-2)[t]{\number\@gridcnt\global\advance\@gridcnt by #3}}%
\global\@gridcnt=#5%
\multiput(0,#2)(#3,0){\delta}{%
\makebox(0,0)[b]{\number\@gridcnt\vspace{2mm}\global\advance\@gridcnt by #3}}%
\fi%
\@delta=#2pt\@@delta=#4pt\divide\@delta by\@@delta\delta=\@delta%
\advance\delta by 1\relax\message{\the\delta . }%
\multiput(0,0)(0,#4){\delta}{\line(1,0){#1}}%
\ifx#6@\relax\else
\global\@gridcnt=#6%
\multiput(0,0)(0,#4){\delta}{%
\makebox(0,0)[r]{\number\@gridcnt\ \global\advance\@gridcnt by #4}}%
\global\@gridcnt=#6%
\multiput(#1,0)(0,#4){\delta}{%
\makebox(0,0)[l]{\ \number\@gridcnt\global\advance\@gridcnt by #4}}%
\fi
}}
%----------------------------------------------------------------------
% These two macros make dashed lines of specified length (second arguement)
% with dashes of specified length (first arguement) just like the \line
% command. e.g.:
% \put(10,10){\hdashline{2}{50.4}} 	%--> put a horizontal dashed line
%					%with individual dashes of length=
%					%2 units & total length=50.4 units
% 					%starting at (10,10).
% and likewise \vdashline will put a vertical dashed line.
%
\def\hdashline#1#2{\@hvdashline{#1}{#2}{h}}
\def\vdashline#1#2{\@hvdashline{#1}{#2}{v}}
\def\@hvdashline#1#2#3{\leavevmode\hbox to \z@{\baselineskip \z@%
\lineskip \z@%
\@linelen=#2\unitlength%
\@dashcnt=\@linelen \advance\@dashcnt 200 %to prevent roundoff errors
\@dashdim=#1\unitlength\divide\@dashcnt \@dashdim
\advance\@dashcnt \@ne \divide\@dashcnt \tw@
\multiply\@dashdim \@dashcnt
\advance\@linelen by -\@dashdim
\advance\@dashcnt \m@ne
\divide\@linelen \@dashcnt %\@linelen now = width/height of 'emptydash'
\advance\@dashcnt \@ne
\ifx#3h% its a hdashline
\setbox\@dashbox=\hbox{\vrule \@height \@halfwidth \@depth \@halfwidth
\@width #1\unitlength\hskip \@linelen}\@tempcnta=0
\put(0,0){\@whilenum \@tempcnta <\@dashcnt
\do{\copy\@dashbox\advance\@tempcnta \@ne }}
\else% its a vdashline
\setbox\@dashbox\hbox{\vrule \@width \@wholewidth
\@height #1\unitlength}\@tempcnta=0
\put(0,0){\hskip -\@halfwidth \vbox{\@whilenum \@tempcnta <\@dashcnt
\do{\vskip \@linelen\copy\@dashbox\advance\@tempcnta \@ne }}}%
\fi
}}
%----------------------------------------------------------------------
% following macros are provided here:
% \drawline(X1,Y1)(X2,Y2)[optional percentage]
% \dottedline(X1,Y1)(X2,Y2){dotgap in units}[optional dotcharacter]
% \dotdashline(X1,Y1)(X2,Y2){dash-length}{interdotgap in each dash}[opt. char]
% \dotcharacter{#1}
% \thindots
% \thickdots
% \begin{dottedjoin}{interdot-gap in units}
% .....			
% \end{dottedjoin}
% \begin{dotdashjoin}{dash-length in units}{interdotgap in each dash}
% .....			
% \end{dotdashjoin}
% \begin{linejoin}
% .....
% \end{linejoin}
% \joinput(X1,Y1){character}
%----------------------------------------------------------------------
\newif\ifjointhem \global\jointhemfalse
\newif\iffirstpoint \global\firstpointtrue
\newcount\@joinkind
\newenvironment{dottedjoin}[1]%
{\global\jointhemtrue \gdef\dotgapunits{#1}\global\@joinkind=0\relax}%
{\global\jointhemfalse \global\firstpointtrue}
%
\newenvironment{dotdashjoin}[2]%
{\global\jointhemtrue \gdef\dotgapunits{#1}\gdef\dotindashgap{#2}%
\global\@joinkind=1\relax}%
{\global\jointhemfalse \global\firstpointtrue}
%
\newenvironment{linejoin}%
{\global\jointhemtrue \global\@joinkind=2\relax}%
{\global\jointhemfalse \global\firstpointtrue}
%----------------------------------------------------------------------
%% this is equiv to \put(x,y){#1} when not in {dot*join} environment.
\long\def\joinput(#1,#2)#3{{\@killglue\raise#2\unitlength\hbox to \z@{\hskip
#1\unitlength #3\hss}\ignorespaces}
\ifjointhem
 \iffirstpoint \gdef\xone{#1} \gdef\yone{#2} \global\firstpointfalse
 \else\ifcase\@joinkind
       \dottedline(\xone,\yone)(#1,#2){\dotgapunits}
    \or\dotdashline(\xone,\yone)(#1,#2){\dotgapunits}{\dotindashgap}
    \else\drawline(\xone,\yone)(#1,#2)\fi
    \gdef\xone{#1} \gdef\yone{#2}
 \fi
\fi
}
%----------------------------------------------------------------------
\newdimen\dotgap
\newcount\@xdiff
\newcount\@ydiff
\newcount\numsegments
\newif\ifsqrtdone
%% from sqrtandstuff func basically need \numsegments.
%% given a deltax, deltay and dotgap, it calculates \numsegments = number of
%% segments along the hypotenuse. used by \dottedline & \dotdashline.
\def\sqrtandstuff#1#2#3{
\ifdim #1 <0pt \@xdiff= -#1 \else \@xdiff=#1\fi
\ifdim #2 <0pt \@ydiff= -#2 \else \@ydiff=#2\fi
%% @diff's will be positive and diff's will retain their sign.
\dotgap=#3 \divide\dotgap by 2
\advance\@xdiff by\dotgap \advance\@ydiff by\dotgap% for round-off errors
\dotgap=#3
\divide\@xdiff by\dotgap
\divide\@ydiff by\dotgap
\sqrtdonefalse
\ifnum\@xdiff < 2
   \ifnum\@ydiff < 2 \numsegments=\@xdiff \advance\numsegments by\@ydiff
		      \sqrtdonetrue
        \else\numsegments=\@ydiff \sqrtdonetrue\fi
   \else\ifnum\@ydiff < 2 \numsegments=\@xdiff \sqrtdonetrue\fi
\fi
\ifsqrtdone \ifnum\numsegments=\z@ \numsegments=\@ne\fi\relax
 \else
  \ifnum\@ydiff >\@xdiff \@tempcnta=\@xdiff \@xdiff=\@ydiff \@ydiff=\@tempcnta
  \fi    		%exchange @xdiff & @ydiff, so now @xdiff > @ydiff
  \numsegments=\@ydiff
  \multiply\numsegments by\numsegments
  \multiply\numsegments by 457
  \divide\numsegments by\@xdiff
  \divide\numsegments by\@m
  \advance\numsegments by\@xdiff
		%numsegments = @xdiff + (0.457*sqr(@ydiff)/@xdiff)
\fi
%\typeout{numsegments=\the\numsegments}
}
%----------------------------------------------------------------------
%%this is essentially same as \multiput except that I have removed the
%%\unitlengths, thus all arguments to \multiput@abs are absolute!. Also for
%%some reason that I do not understand, it needed another \unskip in the
%%loop -- without it everything comes shifted horizontally, maybe \@killglue
%%is incorrect and does one less \unskip than it should?.
\long\def\multiput@abs(#1,#2)(#3,#4)#5#6{\@killglue\@multicnt=#5\relax
\@xdim=#1\relax
\@ydim=#2\relax
\@whilenum \@multicnt > 0\do
{\unskip\raise\@ydim\hbox to \z@{\hskip%
\@xdim #6\hss}\advance\@multicnt \m@ne\advance\@xdim
#3\relax\advance\@ydim #4}\ignorespaces}
%----------------------------------------------------------------------
%
% \dottedline(X1,Y1)(X2,Y2){interdot gap in units}[opt. char]
%
\newdimen\xdiff
\newdimen\ydiff
\newdimen\xstart
\newdimen\ystart
\newbox\@dotbox
\def\make@dotbox#1{\setbox\@dotbox\hbox{#1}}
%% I used the following construction earlier but that results in box memory
%% full much too soon although it works perfectly.
%%\setbox\@dotbox\vbox to\z@{\vss \hbox to\z@{\hss #1\hss}\vss}\relax}
\def\thindots{\def\dotcharacter{\fivrm .}}
\def\thickdots{\def\dotcharacter{\twltt .}}
\thindots % default is thindots.

\def\dottedline(#1,#2)(#3,#4)#5{\@ifnextchar [%
{\@idottedline(#1\unitlength,#2\unitlength)(#3\unitlength,#4\unitlength)%
{#5\unitlength}}%
{\@idottedline(#1\unitlength,#2\unitlength)(#3\unitlength,#4\unitlength)%
{#5\unitlength}[\dotcharacter]}}

%% user is not supposed to use this directly.
%% the arguments here are absolute dimensions.
\long\def\@idottedline(#1,#2)(#3,#4)#5[#6]{{%
\xdiff=#3\relax\advance\xdiff by -#1\relax
\ydiff=#4\relax\advance\ydiff by -#2\relax
\sqrtandstuff{\xdiff}{\ydiff}{#5}
\divide\xdiff by\numsegments
\divide\ydiff by\numsegments
\advance\numsegments by\@ne     % to put the last point at destination.
%
%% I could simply multiput a box of wd=ht=0 but that involves glues and eats
%% up memory so instead I subtract half the width of box containg the char and
%% subtract half the ht and then multiput it. Now it so happens that \circle
%% gives a box of ht=0 & wd=diam of circle so in that case I cannot do this
%% subtraction; moreover the put statement put's the circle on the specified
%% coordinate wheres all other things it puts the thing with its bottom-left
%% coord at the specfd coord. So, now I simply put the character rather than
%% the box.It results in almost 30-40% savings in memory => we can put more
%% stuff.
\make@dotbox{#6}
\xstart=#1 \ystart=#2
\ifdim\ht\@dotbox >\z@% otherwise its a circle.
  \advance\xstart by -0.5\wd\@dotbox
  \advance\ystart by -0.5\ht\@dotbox
  \advance\ystart by .5\dp\@dotbox\fi
\multiput@abs(\xstart,\ystart)(\xdiff,\ydiff){\numsegments}{#6}
%%  circle's have a ht=0, this is one way I could think of to catch circles.
\relax}}
%----------------------------------------------------------------------
% \dotdashline(X1,Y1)(X2,Y2){dash-length}{interdotgap in each dash}[opt. char]
%
% for small line length, I indulge in some approximations. In order not to
% give ugly lines in such a case,the minimum # of dashes I put is 2, one at
% either end point and thus accordingly reduce the dash-length. Also have to
% some dirty work to account for stretch & shrink.
%----------------------------------------------------------------------
%
\def\dotdashlinestretch{0}
\def\dotdashline(#1,#2)(#3,#4)#5#6{\@ifnextchar [%
{\@idotdashline(#1\unitlength,#2\unitlength)(#3\unitlength,#4\unitlength)%
{#5\unitlength}{#6\unitlength}}%
{\@idotdashline(#1\unitlength,#2\unitlength)(#3\unitlength,#4\unitlength)%
{#5\unitlength}{#6\unitlength}[\dotdashlinestretch]}}

%% user is not supposed to use this directly.
%% the arguments here are absolute dimensions.
\long\def\@idotdashline(#1,#2)(#3,#4)#5#6[#7]{{%
\xdiff=#3 \advance\xdiff by -#1\relax
\ydiff=#4 \advance\ydiff by -#2\relax
\sqrtandstuff{\xdiff}{\ydiff}{#5}
%%\typeout{after sqrt numsegments= \the\numsegments}
\ifnum\numsegments <3 \numsegments=3\fi%minimum number of dashes, I can plot
% is 2, 1 at either end, thus min numsegments is 3 (including 'empty dash').
\@tempdima=\xdiff \@tempdimb=\ydiff
\divide\@tempdimb by\numsegments
\divide\@tempdima by\numsegments
\setbox\@dotbox\hbox{%
\@idottedline(0pt,0pt)(\@tempdima,\@tempdimb){#6}[\dotcharacter]}
\advance\xdiff by -\@tempdima % both have same sign
\advance\ydiff by -\@tempdimb
%
\ifnum #7=0 \relax\else\ifnum #7 < -100
  \typeout{***dotdashline: reduction > -100 percent implies blankness!***}
\else\numsegmentsi=#7 \advance\numsegmentsi by 100
     \multiply\numsegments by\numsegmentsi
     \divide\numsegments by 100
\fi\fi
%
\divide\numsegments by 2 % earlier numsegments included 'empty dashes' too.
\ifnum\numsegments >0 %      %   if =0 then don't divide => \xdiff & \ydiff
 \divide\xdiff by\numsegments%   remain same.
 \divide\ydiff by\numsegments
 \advance\numsegments by\@ne %for the last segment for which I subtracted
	 		     %\@tempdima & \@tempdimb from \xdiff & \ydiff
 \else\numsegments=2 % one at each end.
\fi
%%\typeout{numsegments finally = \the\numsegments}
\multiput@abs(#1,#2)(\xdiff,\ydiff){\numsegments}{\copy\@dotbox}
\relax}}
%
%----------------------------------------------------------------------
%%1.00   .833333  .80  .75  .66666   .60  .50  .40  .33333    .25  .20  .16666
%% .916666 .816666 .775 .708333 .633333 .55 .45 .366666 .291666 .225 .183333
%% 0.0
%%0.083333
%% the first line has absolute slopes corresponding to various permissible
%% integer combinations representing slopes. The second line is the midpoint
%% of all those slopes (attempted to show them in the middle of two entries).
%%
%% \lineslope(xdiff dimen, ydiff dimen)
%% Given base (xdiff) and height (ydiff) in dimensions, determines the
%% closest available slope and returns the two required integers in \@xarg and
%% \@yarg. The given base and height can be ANYTHING, -ve or +ve, or even 0pt.
%% \lineslope knows about (0,1) and (1,0) slopes too and returns correct
%% values if the conditions regarding xdiff & ydiff are obeyed. (see NOTE).
%% Used by \drawline. This is the simplest and only way I could figure out
%% to accomplish it!.
%% NOTE: For accuracy of calculations, both the dimensions (xdiff & ydiff)
%% must be in SAME units and the larger of the two dimensions must be
%% atleast 1pt (i.e. 65536 sp). To avoid dividing by 0, I make the larger
%% dimension = 1pt if it is < 1pt.
%% will need a similar one for vectors, or maybe this can be used. For
%% vectors the range is -4, 4 unlike lines where it is -6, 6.
\newif\if@flippedargs
\def\lineslope(#1,#2){%
\ifdim #1 <0pt \@xdim= -#1 \else\@xdim=#1\fi
\ifdim #2 <0pt \@ydim= -#2 \else\@ydim=#2\fi
%%\typeout{xdim,ydim= \the\@xdim, \the\@ydim}
\ifdim\@xdim >\@ydim \@tempdima=\@xdim \@xdim=\@ydim \@ydim=\@tempdima
\@flippedargstrue\else\@flippedargsfalse\fi% x < y
\ifdim\@ydim >1pt \@tempcnta=\@ydim
            \divide\@tempcnta by 65536% now \@tempcnta=integral part of #1.
            \divide\@xdim by\@tempcnta\fi
\ifdim\@xdim <.083333pt \@xarg=1 \@yarg=0
 \else\ifdim\@xdim <.183333pt \@xarg=6 \@yarg=1
 \else\ifdim\@xdim <.225pt \@xarg=5 \@yarg=1
 \else\ifdim\@xdim <.291666pt \@xarg=4 \@yarg=1
 \else\ifdim\@xdim <.366666pt \@xarg=3 \@yarg=1
 \else\ifdim\@xdim <.45pt \@xarg=5 \@yarg=2
 \else\ifdim\@xdim <.55pt \@xarg=2 \@yarg=1
 \else\ifdim\@xdim <.633333pt \@xarg=5 \@yarg=3
 \else\ifdim\@xdim <.708333pt \@xarg=3 \@yarg=2
 \else\ifdim\@xdim <.775pt \@xarg=4 \@yarg=3
 \else\ifdim\@xdim <.816666pt \@xarg=5 \@yarg=4
 \else\ifdim\@xdim <.916666pt \@xarg=6 \@yarg=5
       \else\@xarg=1 \@yarg=1%
\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi
\if@flippedargs\relax\else\@tempcnta=\@xarg \@xarg=\@yarg \@yarg=\@tempcnta\fi
\ifdim #1 <0pt \@xarg= -\@xarg\fi
\ifdim #2 <0pt \@yarg= -\@yarg\fi
%%\typeout{closest slope integers = \the\@xarg, \the\@yarg}
}
%----------------------------------------------------------------------
% usage: \drawline(X1,Y1)(X2,Y2)
%        \drawline(X1,Y1)(X2,Y2)[#] % # is an integer between -100 & infinity.
% \renewcommand{\drawlinestretch}{-50}  %ONLY INTEGERS PERMITTED.
% \renewcommand{\toosmalldrawline}{false}
%----------------------------------------------------------------------
%% \renewcommand{\toosmalldrawline}{false}
\def\toosmalldrawline{true}
\newcount\numsegmentsi
\newif\if@toosmall
\newif\if@toosmalldrawline
\def\drawlinestretch{0} %well, could have used a counter.
\def\drawline(#1,#2)(#3,#4){\@ifnextchar [%
{\@idrawline(#1,#2)(#3,#4)}{\@idrawline(#1,#2)(#3,#4)[\drawlinestretch]}}

\def\@idrawline(#1,#2)(#3,#4)[#5]{%
\xdiff=#3\unitlength \advance\xdiff by -#1\unitlength
\ydiff=#4\unitlength \advance\ydiff by -#2\unitlength
\lineslope(\xdiff,\ydiff)
%% \lineslope returns the two integers in \@xarg & \@yarg
\ifnum\@xarg< 0 \@negargtrue\else\@negargfalse\fi
\ifnum\@xarg =0 \setbox\@linechar%
\hbox{\hskip -\@halfwidth \vrule \@width \@wholewidth \@height 10.2pt \@depth \z@}
\else \ifnum\@yarg =0 \setbox\@linechar%
\hbox{\vrule \@height \@halfwidth \@depth \@halfwidth \@width 10.2pt}
\else \if@negarg \@xarg -\@xarg \@yyarg -\@yarg
        \else \@yyarg \@yarg\fi
\ifnum\@yyarg >0 \@tempcnta\@yyarg \else \@tempcnta -\@yyarg\fi
\ifnum\@tempcnta>6 \@badlinearg\@tempcnta0\fi
\setbox\@linechar\hbox{\@linefnt\@getlinechar(\@xarg,\@yyarg)}%
\fi\fi
%%
%% following is neat. The last segment takes \wd\@linechar & \ht\@linechar
%% so plot the line as though it were from (#1,#2) to
%% (#3-\wd\@linechar,#4-\ht\@linechar) (i.e. for positive slope, of course,
%% signs are reversed for other slopes). Also for horizontal & vertical
%% dashes we don't have to subtract the ht & wd resp. since they are already
%% centered.
\global\@toosmallfalse
\csname @toosmalldrawline\toosmalldrawline\endcsname % sets it true or false
{\ifdim\xdiff <\z@ \xdiff=-\xdiff\fi
 \ifdim\ydiff <\z@ \ydiff=-\ydiff\fi
 \ifdim\xdiff <\wd\@linechar \global\@toosmalltrue\fi
 \ifdim\ydiff <\ht\@linechar \global\@toosmalltrue\fi}
\if@toosmall
 \if@toosmalldrawline
   \ifdim\@wholewidth <0.5pt
    \@idottedline(#1\unitlength,#2\unitlength)(#3\unitlength,#4\unitlength)%
{0.75pt}[\fivrm .]
    \else
    \@idottedline(#1\unitlength,#2\unitlength)(#3\unitlength,#4\unitlength)%
{1pt}[\twltt .]
    \fi
\else\typeout{**\string\drawline(#1,#2)(#3,#4)... \@spaces line too small to
   draw; leaving it blank.^^J\@spaces do a
   \string\renewcomand{\string\toosmalldrawline}{true} to draw it.}
 \fi
\else
\ifnum\@xarg=0\relax\else\ifdim\xdiff >\z@ \advance\xdiff by -\wd\@linechar
  \else\advance\xdiff by\wd\@linechar\fi\fi
\ifnum\@yarg=0\relax\else\ifdim\ydiff >\z@\advance\ydiff by -\ht\@linechar
  \else\advance\ydiff by\ht\@linechar\fi\fi
\ifdim\xdiff <\z@ \@xdiff=-\xdiff \else\@xdiff=\xdiff\fi
\ifdim\ydiff <\z@ \@ydiff=-\ydiff \else\@ydiff=\ydiff\fi
%%\typeout{xdiff,ydiff=\the\xdiff , \the\ydiff}
\numsegments=0 \numsegmentsi=0
\ifdim\wd\@linechar >1pt
 \numsegmentsi=\@xdiff \divide\numsegmentsi by\wd\@linechar\fi
\ifdim\ht\@linechar >1pt
 \numsegments=\@ydiff \divide\numsegments by\ht\@linechar\fi
\ifnum\numsegmentsi >\numsegments \numsegments=\numsegmentsi\fi
\advance\numsegments by\@ne %to account for round-off error
%
\ifnum #5=0 \relax \else\ifnum #5 < -100
  \typeout{***drawline: reduction > -100 percent implies blankness!***}
\else\numsegmentsi=#5 \advance\numsegmentsi by 100
     \multiply\numsegments by\numsegmentsi
     \divide\numsegments by 100
\fi\fi
%%\typeout{numsegments after = \the\numsegments}
%
\divide\xdiff by\numsegments
\divide\ydiff by\numsegments
\advance\numsegments by\@ne %for the last segment for which I subtracted
			    %\wd & \ht of \@linechar from \@xdiff & \@ydiff.
%%\typeout{numseg,xdiff,ydiff= \the\numsegments, \the\xdiff, \the\ydiff}
%
\xstart=#1\unitlength \ystart=#2\unitlength
\if@negarg \advance\xstart by -\wd\@linechar\fi
\ifnum\@yarg <0 \advance\ystart by -\ht\@linechar\fi
\multiput@abs(\xstart,\ystart)(\xdiff,\ydiff){\numsegments}{\copy\@linechar}
\fi} %the if of @toosmall
%---------------------------------------------------------------------
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\PCCSR} {{\rm PCCS}_{R}}
\newcommand{\PrR} {Pr_{R}}
\newcommand{\Nequiv}{\stackrel{N}{\sim}}
\newcommand{\Requiv}{\stackrel{R}{\sim}}
\newcommand{\Gequiv}{\stackrel{G}{\sim}}
\newcommand{\Sequiv}{\stackrel{S}{\sim}}
\newcommand{\Mequiv}{\stackrel{M}{\sim}}
\newcommand{\phiN} {\varphi_{N}}
\newcommand{\phiR} {\varphi_{R}}
\newcommand{\phiG} {\varphi_{G}}
\newcommand{\phiS} {\varphi_{S}}
\newcommand{\phiSG} {\varphi_{SG}}
\newcommand{\phiGR} {\varphi_{GR}}
\newcommand{\phiRN} {\varphi_{RN}}
\newcommand{\phiSR} {\varphi_{SR}}
\newcommand{\phiSN} {\varphi_{SN}}
\newcommand{\phiGN} {\varphi_{GN}}
\newcommand{\IMARGR} {\mbox{IMAR}_{GR}}
\newcommand{\IMARSG} {\mbox{IMAR}_{SG}}
\newcommand{\IMARSR} {\mbox{IMAR}_{SR}}
\newcommand{\IMARSN} {\mbox{IMAR}_{SN}}
\newcommand{\IMARGN} {\mbox{IMAR}_{GN}}
\newcommand{\IMARRN} {\mbox{IMAR}_{RN}}
 
\newcommand{\multisetl}{\displaystyle{ \{ \hspace{-.038in} | }}
\newcommand{\multisetr}{\displaystyle{ | \hspace{-.04in} \} }}
\newcommand{\sht}{\vspace{-.6em}}
\newcommand{\zero}{\mbox{\large \bf 0}}
\newcommand{\ie}{{i.e.\ }}
\newcommand{\dcup}{\stackrel{\mbox{\huge .}}{\cup}}	% disjoint union
\newcommand{\fix}{\mbox{\it fix}}			% recursion operator
\newcommand{\dl}[1]{\mbox{\rm I\hspace{-0.75mm}#1}}	% openface letter
\newcommand{\dc}[1]{\mbox{\rm {\raisebox{.4ex}{\makebox	% openface character
	[0pt][l]{\hspace{.2em}\scriptsize $\mid$}}}#1}}
\newcommand{\IN}{\dl{N}}			        % natural numbers
\newcommand{\IG}{\dc{G}}			   	% graphs

\newcommand{\Rarrow}[4]{\mbox{${#1} \; \stackrel{#2} {  
{\mbox{\raisebox{4.9pt}{$_\subset$}}}  
\!\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!\rightarrow}_{#4} \, {#3}$}}
\newcommand{\rarrow}[4]{\mbox{${#1} \; \stackrel{#2} {  
{\mbox{\raisebox{4.9pt}{$_\subset$}}}  
\!\!\!\!-\!\!\!-\!\!\!\rightarrow}_{#4} \, {#3}$}}

\newcommand{\Garrow}[4]{\mbox{${#1}\ \ \stackrel{#2 \ }
{\!\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!\rightarrow}_{#4}
\ {#3}$}}
\newcommand{\garrow}[4]{\mbox{${#1}\ \ \stackrel{#2 \ }
{\!\!\!\!-\!\!\!-\!\!\!\rightarrow}_{#4}\ {#3}$}}

\newcommand{\midlongmapsto}{\mbox{{{\raisebox{1.5pt}{$_\vdash$}}
$\!\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!\rightarrow$}}}
\newcommand{\Sarrow}[4]{\mbox{${#1}\ \stackrel{#2 \ } 
\midlongmapsto_{#4}\ {#3}$}} 
\newcommand{\sarrow}[4]{\mbox{${#1}\ \stackrel{#2}\longmapsto_{#4}\ {#3}$}}

\newcommand{\rsigma}{\mbox{\parbox{4ex}{\[ \sum_{i \in I}\]}
$[p_{i}] \, \alpha_{i}\,.\, E_{i}$}}

\newcommand{\gsigma}{\mbox{\parbox{4ex}{\[ \sum_{i \in I}\]}
$[p_{i}] \, E_{i}$}}

%\newcommand{\ssigma}[1]{\mbox{\begin{picture}(0.5,0.4)
%     \put(0,0.05){$\sum$} \put(0.01,-0.24){\tiny $_{i \in I}$} \end{picture}
%   $\! #1$}}

\newcommand{\rstr}{   % restriction operator (made by cjou)
        \begin{picture}(0.27,0.4)
        \thinlines
        \put(0.14,-0.06){\line(0,1){0.44}}
        \drawline(0.144,0.39)(0.24,0.25)
%       \put(0.15,-0.06){\line(0,1){0.44}}
%       \drawline(0.145,0.397)(0.245,0.257)
        \end{picture} }

\newcommand{\Ffix}{\raisebox{0pt}[0pt][0pt]{\tiny $
\begin{array}{@{}c@{}}\mbox{\footnotesize $[F]$}\\ \mbox{fix}\!_X\end{array}$}}
\newcommand{\Enfix}{\raisebox{0pt}[0pt][0pt]{\tiny $
\begin{array}{@{}c@{}}\mbox{\footnotesize $[E]$}\\ \neg\mbox{fix}\!_X\!\end{array}$}}

% left over sums from cjou - not sure needed
% \newcommand{\probsum}[2]{\mbox{$ \; {}_{#1} \! +_{#2} \;$} }
% \newcommand{\longsum}[2]{\mbox{\begin{picture}(1.2,0.4)
%                                       \put(0.4,0.05){$\sum$}
%                                       \put(0.0,-0.25){\tiny $_{#1}$}
%                                \end{picture}
%                                $\! #2$}}
%
% \newcommand{\shortsum}[2]{\mbox{\begin{picture}(0.5,0.4)
%                                       \put(0,0.05){$\sum$}
%                                       \put(0.17,-0.24){\tiny $_{#1}$}
%                                \end{picture}
%                                $\! #2$}}
%
% \newcommand{\psigmanew}[3]{\mbox{$\displaystyle \sum_{#1}^{#2} \! \!
%      \! \! \! \! (#3)$ }} 
%
%\newcommand{\gsigma}{\mbox{\begin{picture}(0.5,0.4)
%      \put(0,0.05){$\sum$} \put(0.01,-0.24){\tiny $_{i \in I}$} \end{picture}
%    $\! [p_{i}]E_{i}$}}
%
%\newcommand{\rsigma}{\mbox{\begin{picture}(0.5,0.4)
%      \put(0,0.05){$\sum$} \put(0.01,-0.24){\tiny $_{i \in I}$} \end{picture}
%    $\! [p_{i}] \, \alpha{i}\,.\,E_{i}$}}
%
% added by Bernhard 17Mar90
% \newcommand{\unioni}{\mbox{\begin{picture}(0.5,0.4)
%                                       \put(0,0.05){$\bigcup$}
%                                       \put(0.17,-0.24){\tiny $_{i}$}
%                                \end{picture}
%                                }}
%
% \newcommand{\musigma}{\mbox{\parbox{4ex}{\[ \sum_{i \in I}\]}
% $p_{i}$}}
%
\newtheorem{definition}{Definition}
\newtheorem{theorem}{Theorem}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newcommand\qed{\hfill$\Box$\vspace{1ex}}
\renewenvironment{abstract}{\begin{list}{\hspace{\labelsep}}
			{\rightmargin\leftmargin
			\listparindent 1.5em
			\parsep 0pt plus 1pt}
			\small\item}{\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{\bf Reactive, Generative and Stratified Models\\ 
of Probabilistic Processes}

\author{
{\sf Rob J. van Glabbeek}\thanks{Research supported in part by ONR
Grant N00014-92-J-1974.}\\
{\small \sl Computer Science Department, Stanford University}\vspace{-.2em} \\
{\small \sl Stanford, CA 94305-2140, USA}\vspace{-.2em} \\ 
{\small \tt rvg@cs.stanford.edu}\vspace{1em} \\
\and 
{\sf Scott A. Smolka}\thanks{Research supported in part by NSF Grants
CCR-8704309, CCR--9120995, and CCR--9208585; and AFOSR Grant F49620-93-1-0250.}\\
{\small \sl Department of Computer Science, SUNY at Stony Brook}\vspace{-.2em}
\\{\small \sl Stony Brook, NY 11794-4400, USA}\vspace{-.2em} \\
{\small \tt sas@cs.sunysb.edu}\vspace{1em} \\
\and
{\sf Bernhard Steffen}\\
{\small \sl Institut f\"{u}r Mathematik und Informatik, Universit\"{a}t Passau}\vspace{-.2em} \\
{\small \sl 94040 Passau, Germany}\vspace{-.2em} \\
{\small \tt bus@fmi.uni-passau.de}\\
        }
\date{}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
\bibliographystyle{alpha}
\maketitle
\begin{abstract}
We introduce three models of probabilistic processes, namely, reactive,
generative and stratified.  These models are investigated within the context
of PCCS, an extension of Milner's SCCS in which each summand of a process
summation expression is guarded by a probability and the sum of these
probabilities is 1.  For each model we present a structural operational
semantics of PCCS and a notion of bisimulation equivalence which we prove to be
a congruence.  We also show that the models form a hierarchy:  the reactive
model is derivable from the generative model by abstraction from the relative
probabilities of different actions, and the generative model is derivable from
the stratified model by abstraction from the purely probabilistic branching
structure. Moreover the classical nonprobabilistic model is derivable
 from each of these models by abstraction from all probabilities.
\end{abstract}
%\input{intro}
%\input{syntax}
%\input{reactive}
%\input{generative}
%\input{stratified}
%\input{interrelate}
%\input{conclusion}

% Received: from daimi.dk by sbcs.sunysb.edu; Sun, 18 Mar 90 14:36:19 -0500
\section{Introduction}
\label{sec-intro}

In the {\em reactive model} \cite{pnueli-reactive-systems} of classical 
concurrency theory, a
process reacts to stimuli presented by its environment.
A mechanistic view of the reactive model has been given by Milner
\cite{milner80} in terms of {\em button pushing experiments}. The environment
or {\em observer} experiments on a process by attempting to depress one of
several buttons that the process possesses as its interface to the outside
world.  The experiment {\em succeeds} if the button is unlocked and therefore
goes down; otherwise the experiment {\em fails}.  
In response to a successful experiment, the process makes an internal state
transition and is then ready for further experimentation.

The reactive model has been adopted by Larsen and Skou 
\cite{larsen-skou-prob-bisim} for {\em probabilistic processes}\,:  
a button-pressing experiment succeeds, with probability 1, or else fails.
If successful, the process makes an internal state transition according to a
probability distribution associated with the depressed button and the
current state of the process.

In the probabilistic case, it is interesting to consider a more
``probabilistic'' form of experimentation we call the {\em generative model}.
In this setting, an observer may attempt to depress {\em more than one button
at a time}.
Now the process is more or less on equal footing with its environment, and will
decide, according to a prescribed probability distribution, which button if any
will go down.
In response to a successful outcome,
this same probability distribution, conditioned by the process's choice of
button, will govern the internal state transition made by the process.

%\input{fig-PQ}
\begin{figure*}
\begin{picture}(20.000000,4.000000)
\thicklines
\thinlines
\put(4.579206,3.336801){\circle{0.20}}
\put(4.556847,1.980293){\circle{0.20}}
\put(1.658681,1.86235){\circle{0.20}}
\put(7.478143,1.986235){\circle{0.20}}
\put(6.028676,0.612108){\circle{0.20}}
\put(3.107378,0.617845){\circle{0.20}}
\drawline(1.747345,1.90)(4.490541,3.295210)
\put(4.579206,3.283532){\line(0,-1){1.261853}}
\drawline(4.713359,3.301152)(7.322402,2.010001)
\drawline(4.468183,1.938908)(3.174455,0.653494)
\drawline(4.623924,1.932966)(5.939239,0.653494)
\put(7.499731,0.623991){\circle{0.20}}
\put(7.455784,1.927025){\line(0,-1){1.249970}}
\put(15.482601,3.330859){\circle{0.20}}
\drawline(12.650740,1.90)(15.393936,3.289268)
\put(12.562077,1.89){\circle{0.20}}
\put(15.482601,3.277591){\line(0,-1){1.261853}}
\put(15.460243,1.974352){\circle{0.20}}
\drawline(15.616755,3.295211)(18.225798,2.004059)
\put(18.381538,1.980294){\circle{0.20}}
\drawline(15.393938,1.927025)(14.100209,0.641611)
\put(14.033133,0.605962){\circle{0.20}}
\put(16.954430,0.600225){\circle{0.20}}
\drawline(15.549679,1.921083)(16.864992,0.641611)
\put(18.425486,0.623991){\circle{0.20}}
\put(18.381538,1.927025){\line(0,-1){1.249970}}
\put(3.375684,3.324918){\small \rm $P$}
\put(14.568974,3.324918){\small \rm $Q$}
\put(1.859139,2.70){\small \rm $a[\frac{1}{4}]$}
\put(3.70,2.359321){\small \rm $a[\frac{3}{4}]$}
\put(6.430362,2.572600){\small \rm $b[1]$}
\put(2.862203,1.204415){\small \rm $a[1]$}
\put(5.515964,1.204415){\small \rm $b[1]$}
\put(7.678602,1.210152){\small \rm $c[1]$}
\put(12.606794,2.560717){\small \rm $a[\frac{1}{6}]$}
\put(14.560,2.353379){\small \rm $a[\frac{1}{2}]$}
\put(17.356115,2.554776){\small \rm $b[\frac{1}{3}]$}
\put(13.699292,1.222034){\small \rm $a[\frac{1}{2}]$}
\put(16.464077,1.204415){\small \rm $b[\frac{1}{2}]$}
\put(18.649075,1.210152){\small \rm $c[1]$}
\end{picture}
\caption{Reactive process $P$ and generative process $Q$.}
\label{fig-PQ}
\end{figure*}

For example,
consider the reactive process $P$ and the generative process $Q$ given by:
$$\textstyle P = \frac{1}{4}a + \frac{3}{4}a\,.\,(a + b) + \, b\,.\,c
\hspace{1.5in}
Q = \frac{1}{6}a + \frac{1}{2}a\,.\,(\frac{1}{2}a + \frac{1}{2}b) + 
                        \frac{1}{3}b\,.\,c$$
$P$ and $Q$ have as semantics the {\em probabilistic labeled transition 
systems} depicted in Figure~\ref{fig-PQ}. 
For $P$, an $a$- or $b$-experiment
will succeed with probability 1, whereas a $c$-experiment will fail.
In the case of an $a$-experiment, $P$ will branch left with 
probability $\frac{1}{4}$ and right with
probability $\frac{3}{4}$.  Note that no information is given about the
relative probability of performing an $a$-action versus a $b$-action in $P$'s
initial state. 

For the generative process $Q$, if the observer simultaneously attempts to
depress the $a$ and $b$ buttons, $Q$ will unlock its $a$-button with
probability $\frac{2}{3}$ and its $b$-button with probability $\frac{1}{3}$.
In the former case, $Q$ will branch left with probability $\frac{1}{4}$ and
right with probability $\frac{3}{4}$, which is precisely $P$'s reaction to an
$a$-experiment.
In fact, for any {\em single-button experiment}, $P$ and $Q$ behave the same.
Thus $Q$ contains strictly more information than $P$, and, in
a broader sense, the reactive model is an {\em abstraction} of the
generative model.

In this paper we also consider the {\em stratified model} of probabilistic
processes, which captures the branching structure of the {\em purely
probabilistic choices} made by a process.
For example, consider an operating system in which there are $n$ processes to 
be multiprogrammed.  One
of these is the garbage collector which performs optimally if given one third
of the CPU cycles.  The other $n-1$ processes are user processes and
should equally share the remaining two thirds of the CPU.  For the case $n=3$,
a plausible specification of a scheduler for these processes would be
$$\textstyle Sc = \fix_{X}(\frac{1}{3}a.X+\frac{1}{3}b.X+\frac{1}{3}c.X)$$
where the action $a$ identifies the garbage collector, and $b$ and $c$ the user
processes.  But consider the {\em restriction context} in which user $c$ is
denied further access to the machine.  What would happen to its share of the
CPU?  Because of the symmetry in the above specification, we would naturally
arrive at the expression
$$\textstyle \fix_{X}(\frac{1}{2}a.X + \frac{1}{2}b.X)$$
Now, however, the garbage collector is granted one half of the CPU which is
{\em different} from our original intent.
An exact specification of the scheduler can be obtained through the use of 
{\em nested} expressions of probabilistic choice:
$$\textstyle Sc'=\fix_{X}(\frac{1}{3}a.X+\frac{2}{3}(\frac{1}{2}b.X+\frac{1}{2}c.X))$$
which, in the stratified model, yields the leftmost probabilistic labeled
transition system of Figure~\ref{fig-Sc}.
If user $c$ were now denied access we would obtain
$$\textstyle \fix_{X}(\frac{1}{3}a.X +\frac{2}{3}b.X)$$
as desired.  Thus, in the stratified model, the intended relative frequencies
are preserved in a level-wise fashion in the presence of restriction.

%\input{fig-Sc}
\begin{figure*}
\begin{picture}(20.000000,4.000000)
\thicklines
\thinlines
\put(1.993292,2.140305){\small \rm $a$}
\put(4.958535,1.322835){\small \rm $b$}
\put(8.347824,1.334718){\small \rm $c$}
\put(2.82,3.3287){\small \rm $\frac{1}{3}$}
\put(5.933,3.304){\small \rm $\frac{2}{3}$}
\put(5.50,2.398){\small \rm $\frac{1}{2}$}
\put(7.68036,2.398){\small \rm $\frac{1}{2}$}
\put(12.962993,2.39){\small \rm $a[\frac{1}{3}]$}
\put(14.69432,1.986235){\small \rm $b[\frac{1}{3}]$}
\put(17.17,2.42){\small \rm $c[\frac{1}{3}]$}
\put(6.741843,2.667254){\circle{0.180444}}
\drawline(6.630821,2.625869)(5.337864,1.830000)
\drawline(6.875998,2.625869)(8.080289,1.850000)
\put(2.416568,2.631810){\line(0,-1){0.746376}}
\put(2.394209,2.667254){\circle{0.180443}}
\put(5.293146,1.844049){\line(0,-1){0.728551}}
\put(5.270016,1.885435){\circle{0.180443}}
\put(8.191311,1.885435){\circle{0.180443}}
\put(8.191312,1.838107){\line(0,-1){0.728552}}
\put(1.993292,2.140305){\small \rm $a$}
\put(4.958535,1.322835){\small \rm $b$}
\put(8.347824,1.334718){\small \rm $c$}
\put(4.512129,3.608489){\circle{0.180442}}
\drawline(2.438927,2.602000)(4.423465,3.598700)
\drawline(4.601565,3.578700)(6.653180,2.700000)
\drawline(2.371850,1.861873)(1.636322,1.020638)[50]
\drawline(2.416568,1.855932)(3.129737,1.014696)
\put(1.636322,1.008755){\line(1,0){1.515774}}
\put(15.461014,2.744494){\circle{0.180443}}
\drawline(5.315505,1.085995)(6.028674,0.244759)
\put(4.535259,0.238818){\line(1,0){1.515773}}
\drawline(5.270787,1.091936)(4.535259,0.250701)[50]
\drawline(8.168953,1.097878)(7.433425,0.256642)[50]
\drawline(8.213670,1.091936)(8.926840,0.250701)
\put(7.433425,0.244759){\line(1,0){1.515774}}
\put(15.482601,2.679343){\line(0,-1){0.906387}}
\drawline(15.371578,2.714787)(12.562077,1.784838)
\drawline(15.549679,2.720728)(18.359180,1.778897)
\drawline(12.495001,1.761277)(11.759472,0.920042)[50]
\drawline(12.539717,1.755336)(13.252887,0.914101)
\put(11.759472,0.908159){\line(1,0){1.515775}}
\drawline(15.460243,1.755336)(14.724714,0.914101)[50]
\drawline(15.504959,1.749395)(16.218130,0.908159)
\put(14.724714,0.902218){\line(1,0){1.515774}}
\drawline(18.359180,1.767219)(17.623652,0.925984)[50]
\drawline(18.403896,1.761278)(19.117067,0.920042)
\put(17.623652,0.914101){\line(1,0){1.515776}}
\put(2.17033,1.168766){\small \rm $X$}
\put(5.114275,0.457238){\small \rm $X$}
\put(8.035571,0.3821){\small \rm $X$}
\put(12.294542,1.074111){\small \rm $X$}
\put(15.27425,1.0821){\small \rm $X$}
\put(18.211,1.074111){\small \rm $X$}
\end{picture}
\caption{Stratified and generative transition systems of $Sc'$.}
\label{fig-Sc}
\end{figure*}

Note that the probabilistic labeled transition system of $Sc'$ in the 
generative model is simply the right one of Figure~\ref{fig-Sc}. 
Thus, in the generative model, $Sc$ is (unfortunately) equivalent to $Sc'$.
We shall see that, in a broader sense, the generative model is an abstraction
of the stratified model, in which the branching structure
of probabilistic choices has been ``flattened.''

The extremal case of nested probabilistic choice in the stratified model, in
which zero probabilities are permitted, yields a general notion of {\em process priority}.  For example, the expression
$$1P + 0(1Q + 0R)$$
gives priority to process $P$ over $Q$ and $R$, and priority to $Q$ over $R$.
Thus process $R$ can only be executed in a restriction context that excludes
$P$ and $Q$.  Zero probabilities are not considered in this paper, but
their role in modeling priority is examined carefully in \cite{SS90}.

\subsubsection*{\large \bf Summary of Technical Results}

We will be working within the framework of PCCS,  a
specification language for probabilistic processes introduced in
\cite{gjs90}. 
PCCS is derived from  Milner's SCCS \cite{milner83} by replacing the operator
of nondeterministic process summation with a probabilistic counterpart.
Several PCCS expressions have appeared above, which should give the flavor of
the language.

\pagebreak[3]
For each of the three probabilistic models, and, for comparison purposes,
the classical nonprobabilistic model, we present the following:
\sht
\begin{itemize}
   \item a {\em structural operational semantics} of PCCS, given as a set of
   inference rules in the style of Plotkin \cite{plotkin-sos} and Milner
   \cite{milner89}. 
   For each model, these inference rules determine a {\em semantic mapping}
   from the set of PCCS expressions to a particular domain of
   probabilistic labeled transition systems.
   We denote these mappings as $\phiN$, $\phiR$, $\phiG$, and
   $\phiS$, respectively. 
   (As discussed in Section~\ref{sec-react}, the relabeling operator of PCCS
   is not compatible with the reactive model, and also the combination of
   summation and unguarded recursion may be problematic. Therefore, 
   $\phiR$ applies only to a sublanguage $\PCCSR$ of PCCS in which relabeling
   and unguarded recursion are excluded.) 
   
   \item a notion of {\em bisimulation semantics}.
   In \cite{larsen-skou-prob-bisim}, Larsen and Skou introduced 
   {\em probabilistic
   bisimulation}, a natural and elegant extension of strong bisimulation
   \cite{park-concurrency,milner83} for reactive processes.
   We likewise define probabilistic bisimulation on generative and 
   stratified processes.
   In each model, the largest bisimulation (under set inclusion),
   denoted $\Nequiv$, $\Requiv$, $\Gequiv$, and $\Sequiv$, respectively,
   determines the model's bisimulation semantics. 
   
   \item We prove that $\Requiv$ is a congruence with respect to $\PCCSR$, and 
   $\Nequiv$, $\Gequiv$ and $\Sequiv$ are congruences with respect to PCCS.
\end{itemize}   

We then inter-relate the models, ultimately showing that they
form a hierarchy:  
the generative model is an abstraction of the stratified
model, the reactive model is an abstraction of the generative model,
and the nonprobabilistic model is an abstraction of the reactive model.
This reflects the stepwise reduction of ``observational power'';
\ie starting from the
stratified model, we first abstract from the probabilistic branching
structure, then from the relative probabilities among different
actions, and finally from all probabilities. We proceed as follows:\sht

\begin{itemize}

\item We add to the stratified, generative and reactive operational
semantics {\em inter-model abstraction rules}, which respectively allow the
inference of generative probabilistic transitions from stratified ones,
reactive probabilistic transitions from generative ones, and nonprobabilistic
transitions from reactive ones.  These rules determine mappings between domains
of probabilistic labeled transition systems, which are denoted as $\phiSG$,
$\phiGR$ and $\phiRN$, respectively. Similarly we define ``shortcuts''
$\phiSR$, $\phiGN$ and $\phiSN$, and establish $\phiGN \circ \phiSG =
\phiRN \circ \phiSR = \phiSN$, $\phiRN \circ \phiGR = \phiGN$ and
$\phiGR \circ \phiSG = \phiSR$. The last result however only holds for
stratified transition systems specified by closed PCCS expressions in
which each summation is probability- {\em and} action-guarded. We
refer to such expressions as {\em summation-guarded\/} PCCS expressions.

\item We obtain the following {\em inter-model abstraction results\/}.
$$\begin{array}{llll}
\mbox{For any two stratified transition systems $G$ and $H$:} &
G \Sequiv H & \Longrightarrow & \phiSG(G) \Gequiv \phiSG(H)\\
\mbox{For any two generative transition systems $G$ and $H$:} &
G \Gequiv H & \Longrightarrow & \phiGR(G) \Requiv \phiGR(H)\\
\mbox{For any two reactive transition systems $G$ and $H$:} &
G \Requiv H & \Longrightarrow & \phiRN(G) \Nequiv \phiRN(H)\\
\mbox{For any two stratified transition systems $G$ and $H$:} &
G \Sequiv H & \Longrightarrow & \phiSR(G) \Requiv \phiSR(H)
\end{array}$$

Note that our last abstraction result holds for all stratified transition
systems and is therefore not directly obtainable from the first two via the
$\phiSR$ shortcut (which applies only to summation-guarded stratified
transition systems).

\item For $P$ a closed PCCS expression we prove the following {\em
commutativity results\/}, which, in addition to the abstraction results,
establish the hierarchy among the models.
$$\begin{array}{ll}
\phiG(P) \; = \; \phiSG(\phiS(P)) & \mbox{if $P$ is summation-guarded
or restriction-free}\\
\phiR(P) \; = \; \phiGR(\phiG(P)) & \mbox{if $P$ is a summation-guarded
$\PCCSR$ expression}\\
\phiR(P) \; = \; \phiSR(\phiS(P)) & \mbox{if $P$ is a
$\PCCSR$ expression}\\
\phiN(P) \; = \; \phiRN(\phiR(P)) & \mbox{if $P$ is a
$\PCCSR$ expression}\\
\phiN(P) \; = \; \phiSN(\phiS(P)) & \!\! = \; \phiGN(\phiG(P))
\end{array}$$
In the presence of restriction and general summation the first commutativity
result does not hold. This is to be expected, as the stratified model is
motivated by its different treatment of restriction with respect to nested
summations.  Additionally, we show that the second commutativity result does
not hold in the presence of general summation. In fact, our counterexample
suggests that the reactive summation has a stratified flavor that is not
present in the generative case. This impression is supported by the third
commutativity result, that holds without restrictions on summation or
restriction. It is not possible to define in a compositional way a more
generatively flavored summation in the reactive model, that would allow a
generalization of the second commutativity result.
%However, by introducing a ``semi-stratified''
%interpretation of restriction in the stratified model, the first result can be
%extended to arbitrary PCCS expressions.

\begin{figure*}
\setlength{\unitlength}{0.0125in}%
\begin{picture}(442,184)(0,545)
\thicklines
\multiput(190,620)(-22.36017,-11.18008){4}{\line(-2,-1){ 12.920}}
\put(110,580){\vector(-2,-1){0}}
\multiput(315,620)(-22.36017,-11.18008){4}{\line(-2,-1){ 12.920}}
\put(235,580){\vector(-2,-1){0}}
\multiput(440,620)(-22.36017,-11.18008){4}{\line(-2,-1){ 12.920}}
\put(360,580){\vector(-2,-1){0}}
\put(425,640){\vector(-1, 0){ 40}}
\put(295,640){\vector(-1, 0){ 40}}
\put(180,640){\vector(-1, 0){ 40}}
\put(460,615){\vector( 0,-1){ 35}}
\put(340,615){\vector( 0,-1){ 35}}
\put(215,615){\vector( 0,-1){ 35}}
\put( 90,615){\vector( 0,-1){ 35}}
\put(280,715){\vector( 1,-1){ 60}}
\put(275,715){\vector(-1,-1){ 60}}
\put(285,715){\vector( 3,-1){180}}
\put(270,715){\vector(-3,-1){180}}
\put(150,650){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvrm $\varphi_{RN}$}}}
\put(270,650){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvrm $\varphi_{GR}$}}}
\put(395,650){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvrm $\varphi_{SG}$}}}
\put(165,695){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvrm $\varphi_{N}$}}}
\put(250,675){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvrm $\varphi_{R}$}}}
\put(330,675){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvrm $\varphi_{G}$}}}
\put(380,695){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvrm $\varphi_{S}$}}}
\put(405,555){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm $\Longleftarrow$}}}
\put(275,555){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm $\Longleftarrow$}}}
\put(155,555){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm $\Longleftarrow$}}}
\put(460,545){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Bisimulation}}}
\put(460,560){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Stratified}}}
\put(340,545){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Bisimulation}}}
\put(340,560){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Generative}}}
\put(215,545){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Bisimulation}}}
\put(215,560){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Reactive}}}
\put( 90,545){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Bisimulation}}}
\put( 90,560){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Nonprobabilistic}}}
\put(465,625){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Model}}}
\put(465,640){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Stratified}}}
\put(340,625){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Model}}}
\put(340,640){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Generative}}}
\put(215,625){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Model}}}
\put(215,640){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Reactive}}}
\put( 90,625){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Model}}}
\put( 90,640){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\elvrm Nonprobabilistic}}}
\put(260,720){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvrm PCCS}}}
\end{picture}
\caption{Interdependencies between the models.}
\label{fig-sum}
\end{figure*}

\item 
We then show that the equivalence induced on the stratified
(generative) model via abstraction to the generative (reactive) model is 
{\em not} a congruence with respect to PCCS.
This demonstrates the need for refining the bisimulation semantics when moving
to a less abstract model.  More precisely, we exhibit a pair of PCCS processes
$P$, $Q$ and a context ${\cal C}[ \; ]$ such that
\begin{center}
$\phiSG(\phiS(P)) \Gequiv \phiSG(\phiS(Q))$ \ \ and \ \
$\phiSG(\phiS({\cal C}[P])) \not\Gequiv \phiSG(\phiS({\cal C}[Q]))$
\end{center}
Similarly for the generative-to-reactive and stratified-to-reactive
abstractions.

\item
On the other hand, the equivalence induced on the stratified model via
abstraction to the reactive model {\em is\/} a congruence with respect to
$\PCCSR$.  Likewise, the equivalences induced on the stratified and generative
models via abstraction to the nonprobabilistic model are congruences with
respect to PCCS; and the equivalence induced on the reactive model via
abstraction to the nonprobabilistic model is a congruence with respect to
$\PCCSR$.  These congruence results can be seen as consequences of the fact
that the corresponding commutativity results hold without side conditions, and
that $\Requiv$, $\Gequiv$, and $\Sequiv$ are congruences.
\end{itemize}
The interdependencies between the different models are summarized in
Figure~\ref{fig-sum}. 
Here the upper part reflects the commutativity results,
the double arrows below reflect the abstraction results,
and the dashed arrows indicate the bisimulations that are induced on the
stratified, generative, and reactive models via abstraction to the generative,
reactive, and nonprobabilistic models, respectively. 

We conclude the paper with
an interesting open problem concerning an equivalence relation $\Mequiv$ ({\em
mixed bisimulation}) that, in terms of its distinguishing strength, falls
strictly between $\Gequiv$ and $\Sequiv$, and is still a congruence in the
stratified model.  We conjecture that $\Mequiv$ is the largest
congruence contained in $\Gequiv$.

\subsubsection*{\large \bf Related Work}

This paper is an extended version of~\cite{vGSST}, which was written in
cooperation with Chris Tofts.  The main contributions of the current paper
and~\cite{vGSST} are:
\begin{list}{\bf --}{\leftmargin 15pt}\sht
\item
The reactive operational semantics of summation-guarded $\PCCSR$ was first
given in~\cite{vGSST}.
The reactive semantics of general summation, not present in~\cite{vGSST}, was
developed in~\cite{LS92}. The generative operational semantics of PCCS
stems from~\cite{gjs90}.\sht
\item
The stratified model and its operational and bisimulation semantics first
appeared in~\cite{vGSST}.\sht
\item
All congruence results and the interrelations between the various models
were indicated, in part, in~\cite{vGSST}.  Their detailed proofs are given here
for the first time.\sht
\end{list}
Pointers to earlier, mostly logic-oriented approaches to probabilistic
processes (e.g. probabilistic temporal and dynamic logic) can be found
in~\cite{gjs90}.  Recent work on probabilistic process
algebra includes~\cite{LS92} (in a reactive setting), \cite{JS90,JL91,BBS92}
(in a generative setting) and \cite{SS90,Tof90b} (in a stratified setting).
All these papers consider probabilistic bisimulation, except for~\cite{JS90},
where also probabilistic versions of trace, failure and readiness equivalences
and congruences are studied. The interplay between time and probability has
been investigated in~\cite{HJ90,Lowe91}.

Larsen and Skou~\cite{larsen-skou-prob-bisim} have examined
the reactive model in the setting of {\em testing}.
They exhibit a testing algorithm that, with probability
$1 - \epsilon$, where $\epsilon$ is arbitrarily small, can distinguish
processes that are not probabilistically bisimilar.
Bloom and Meyer \cite{bloom-meyer} further show that if nondeterministic
bounded-branching processes $P$ and $Q$
are bisimilar, then there is an assignment of probabilities to the edges
of $P$ and $Q$, yielding reactive processes $P'$ and $Q'$
such that $P'$ and $Q'$ are probabilistically bisimilar.

Christoff~\cite{christoff90} also considers the testing of probabilistic
processes.  He proposes three probabilistic trace-based testing equivalences
for generative processes using nondeterministic tests.  Cleaveland et
al.~\cite{CSZ92} investigate the testing of generative processes as
well (but with
generative tests); close connections to the classical testing theory of
De Nicola and Hennessy are demonstrated.  Similar connections are made by Yi
and Larsen in~\cite{YiLarsen92} for a model of probabilistic processes based
on~\cite{HJ90}.

Jones and Plotkin~\cite{jones-plotkin} investigate a probabilistic
powerdomain of evaluations, which they use to give the semantics of a language
with a probabilistic parallel construct.  Finally, Seidel~\cite{Seidel92} uses
conditional probability measures to give a semantics to a probabilistic
extension of CSP.

% From bus@daimi.dk Sun Mar 18 14:36:36 1990
\section{Syntax of PCCS}

As in SCCS, the {\em atomic actions} of PCCS form a multiplicative structure
$(Act, \cdot)$ that is generated freely from the set $\Lambda$ of {\em
particulate actions}.
Unlike SCCS, where $Act$ is an abelian monoid, we assume neither commutativity
nor associativity for action product ($\cdot$).
Thus all elements of $Act$ are of the form $a$ or $(\alpha, \beta)$, where 
$a \in \Lambda$ and $\alpha,\beta \in Act$.
One can think of the atomic action $(\alpha, \beta)$ as the {\em simultaneous
ordered occurrence} of actions $\alpha$ and $\beta$.

As discussed in Section~\ref{sec-react}, the free structure
of our action algebra is necessary to be able to define synchronous product in
the reactive model.  For any SCCS-like action monoid or group, the
corresponding synchronization merge can be expressed in our calculus by a
combination of product and relabeling.  For example, the group structure of
SCCS can be obtained through relabelings of the form
$(\alpha, \overline{\alpha}) \mapsto 1$ and
$(\overline{\alpha}, \alpha) \mapsto 1$\,,
where 1 is the unit or idle action of SCCS.
As a consequence relabeling, which is a derived operator in SCCS in
the sense that it can be expressed in terms of the other operators,
has to be introduced as a first-class operator in PCCS.
 
Let $X$ be a variable, $A$ a subset of $Act$, and $f: Act 
\rightarrow Act$. The syntax of PCCS is given by:\vspace{-.2in}
\[E ::= \zero \; \; | \; \; X \; \; | \; \; \alpha . E \; \; | \; \;  
%{\displaystyle \sum} \; [p_{i}] \, E_{i},
\gsigma \; \mbox{ where }p_i \in (0,1], \ {\displaystyle \sum_{i \in I} p_{i} =
1} \; \; | \; \; E \!\times \! F \; \; | \; \; E
\rstr A \; \; | \; \; E [f] \; \; | \; \; \fix_{X} E\]

\vspace{-.2in}
Intuitively, $\zero$ is the {\em zero process}
having no transitions, while $\alpha\, . \,E$ performs action $\alpha$ with
probability 1 and then behaves like $E$.  The expression $\sum [p_{i}] \,
E_{i}$ offers a probabilistic choice among its constituent behaviors $E_{i}$.
$E \times
F$ represents synchronized product, and the restricted expression $E \rstr A$
can perform actions only from the set $A$. Finally, $E [ f ] $ specifies a
relabeling of actions, and $\fix_{X} E$ defines a recursive process.

A PCCS expression is {\em guarded} if in its syntactic tree, every
path from a recursion operator $\fix_X$ to an occurrence of the
corresponding variable $X$ passes through an action operator $\alpha .$.
In this paper we require expressions to be {\em restriction-guarded},
a much weaker requirement that ensures that the restriction operators
in the generative and stratified models are well-defined.
A PCCS expression is restriction-guarded if in its syntactic
tree, every path from a recursion operator $\fix_X$ to an occurrence of
the corresponding variable $X$ either passes through an action
operator $\alpha .$, or doesn't pass through a restriction operator.
This excludes expressions like
$\fix_{X}(\frac{1}{3}a.X+\frac{1}{3}b.X+\frac{1}{3}X\rstr \{a\})$ but
permits non-guarded expressions like $\fix_{X}(X[f]+(a.X)\rstr\{ b \})$.
We write $E\in\mbox{PCCS}$ to indicate that $E$ is a
restriction-guarded PCCS expression. 
An expression having no free variables is called a {\it process}, and $Pr$ is
the set of all restriction-guarded PCCS processes.

For this paper, all summation expressions are required to be finite.
It will be convenient to assume that all indices used in summation
expressions come from a given set $I_0$ not containing $0$. Also,
we write the binary version of process summation as $[p]\, E + [1 - p ] \, F$,
assuming an index set \{1,2\}, and often omit the square brackets around
the probabilities. 

\section{The Nonprobabilistic Model}
\label{sec-nonprob}

%This definition is from rosemary. Rob
\def\aRa{\buildrel\alpha\over\longrightarrow}

We start with the nonprobabilistic model of PCCS based on Milner's
model of SCCS \cite{milner83}. In this model all probabilities are
neglected and the only difference between PCCS and SCCS is the different
communication format.  The reasons for including this section are to
facilitate comparison between the probabilistic models and the
classical one, and to present some proofs pertaining to classical
bisimulation in such a way that they can be recycled in the
probabilistic case.

\subsection{Nonprobabilistic Operational Semantics of PCCS}
\label{sec-nonprob-operational}

The nonprobabilistic operational semantics of PCCS is given by
the inference rules of Figure~\ref{fig-nos}.
\begin{figure}
\centering
$\begin{array} {lll}
\hline \\
   &   &
\garrow{\alpha \,.\, E\ }{\alpha}{E}{} \\[0.2cm]

\garrow{E_{j}\ }{\alpha}{E'}{}, \;\; j \in I & \Longrightarrow &
\garrow{\gsigma \ }{\alpha}{E'}{} \\[0.2cm]

\garrow{E\ }{\alpha}{E'}{}, \; \garrow{F\ }{\beta}{F'}{} & \Longrightarrow &
\Garrow{E \times F\,}{\alpha\beta}{E' \times F'}{} \\[0.2cm]

\garrow{E\ }{\alpha}{E'}{}, \;\; \alpha \in A & \Longrightarrow &
\garrow{E \rstr A \ }{\alpha}{E' \rstr A}{} \\[0.2cm]

\garrow{E\ }{\alpha}{E'}{} & \Longrightarrow &
\Garrow{E[f]\,}{f(\alpha)}{E' [f]}{} \\[0.2cm]

\garrow{E \{\fix_X E / X \} \ }{\alpha}{E'}{} & \Longrightarrow &
\garrow{\fix_{X} E\ }{\alpha}{E'}{}

\\[0.2cm] \hline
\end{array}$
\caption{Nonprobabilistic operational semantics of PCCS.}
\label{fig-nos}
\end{figure}
We write $N \vdash P \aRa P'$ or just $P\aRa P'$ 
if $P \aRa P'$ can be derived from these rules.
We refer to $P \aRa P'$ as a {\em transition\/} and its intuitive meaning is
that $P$ can perform action $\alpha$ to become $P'$.
The rules of Figure~\ref{fig-nos} induce a mapping $\phiN$ from $Pr$
to a domain of nonprobabilistic labeled transition systems.

\begin{definition}
A {\em (nonprobabilistic) transition system} is a triple (S,T,I) with
\vspace{-.6em}
\begin{itemize}
\item[\bf --] S a set of {\em states},
\vspace{-.3em}
\item[\bf --] $T \subseteq S \times Act \times S$ a set of {\em transitions},
\vspace{-.3em}
\item[\bf --] and $I \in S$ the {\em initial} state.
\end{itemize}
\end{definition}
In a transition system all parts that are not reachable from the root as well
as the identity of the states are often considered irrelevant. Therefore an
isomorphism between two transition systems can be defined as a bijective
relation between their reachable states, preserving transitions and the
initial state. Isomorphic transition systems are conceptually identified. Now
$\phiN(P)$ for $P \in Pr$ is defined to be the transition system $(S,T,I)$
with $S=Pr$, $I=P$ and $T$ the set of transitions
$\{ (P,\alpha,P') \;|\; N \vdash P \aRa P' \}$.

Let $\IG_N$ be the domain of transition systems (or {\em process graphs}).
To extend the mapping $\phiN : Pr \rightarrow \IG_N$
to an interpretation of the open (restriction-guarded) PCCS expressions in
$\IG_N$, let PCCS-$\IG_N$ be the language PCCS to which all transition
systems $G\in\IG_N$ have been added as constants. We introduce an
operational rule $G\aRa G_s$ for each initial transition $(I,\alpha,s)$ in
each transition system $G=(S,T,I)$.  Here $G_s$ denotes the transition
system with the same states and transitions as $G$, but with $s$ as the initial
state. Let $\phiN'$ be the extension of $\phiN$ to closed PCCS-$\IG_N$
expressions. Now let $E$ be an open PCCS expression and $\xi$ a valuation
of the free variables of $E$ in $\IG_N$.  Then denoting by $E^{\xi}$ the
result of substituting the constant $\xi(X)$ for $X$ in $E$, for all
occurrences of free variables $X$ in $E$, allows us finally to define
$\phiN(E)(\xi)=\phiN'(E^\xi)$.

Note that the extended $\phiN$ in particular defines an interpretation of
the PCCS operators in $\IG_N$, thereby making $\IG_N$ into a PCCS-algebra.

\subsection{Bisimulation}

In this section we reformulate strong bisimulation~\cite{milner83} as
bisimulation in the nonprobabilistic model, which we explicitly call
{\em nonprobabilistic bisimulation\/}.
A nonprobabilistic bisimulation will be presented as an equivalence relation
over $Pr$. For this purpose we need a predicate that indicates whether or not
from a given process it is possible to reach (a member of) a set of
processes by means of an $\alpha$-step.
Using $\cal P$ for the powerset operator we have:

\begin{definition}
\label{def-ncPDF}
The function $\mu_N :\, (Pr\times Act\times {\cal P} (Pr))\longrightarrow
\{0,1\}$ is given by: $\forall\alpha\in Act,\
\forall P\in Pr,\ \forall S\subseteq Pr,$
\[\mu_N (P,\,\alpha ,\,S)=\left\{
\begin{array}{cl}1 & \mbox{if } \exists Q\in S~with~P\aRa Q\\ 0 & otherwise
\end{array} \right. \]
\end{definition}

For an equivalence relation $\cal R$ over $Pr$, we write $Pr/\cal R$ 
to denote the set of equivalence classes induced by $\cal R$, and
$\lbrack P\rbrack _{\cal R}$ to denote the
equivalence class of which $P$ is a member. 
Nonprobabilistic bisimulation can now be defined as follows:

\begin{definition}\label{def-Nequiv}
An equivalence relation ${\cal R}\subseteq Pr\times
Pr$ is a {\em nonprobabilistic bisimulation} if $(P,Q)\in \cal R$ implies:
$\forall S\in Pr/{\cal R},\ \forall\alpha\in Act$,
\[\mu_N (P,\alpha,S) = \mu_N (Q,\alpha,S)\]
Two processes $P,Q\in Pr$ are {\em nonprobabilistic bisimulation equivalent}
(written $P \Nequiv Q$) if there exists a nonprobabilistic bisimulation
${\cal R}$ such that $(P,Q)\in {\cal R}$.
Two open PCCS expressions $E,F\in {\rm PCCS}$ are
{\em nonprobabilistic bisimulation equivalent} iff they are
nonprobabilistic bisimulation equivalent after any
substitution of closed terms for their free variables.
\end{definition}

This definition can easily be transformed into a definition of
bisimulation on transition systems (a bisimulation between two
transition systems is a relation on the disjoint union of their
states), such that, for $E,F \in {\rm PCCS}$, $E\Nequiv F \iff
\forall \mbox{ valuations }\xi,~\phiN(E)(\xi)\Nequiv \phiN(F)(\xi)$.

\begin{proposition}
If ${\cal R}_i \ (i\in I)$ is a collection of bisimulations, then
also their reflexive and transitive closure $(\bigcup_i {\cal
R}_i)^\ast$ is a bisimulation.
\label{propo-union}
\end{proposition}

\noindent
{\bf Proof:} Since each of the relations ${\cal R}_i$ is symmetric,
$(\bigcup_i {\cal R}_i)^\ast$ is also symmetric, and hence an
equivalence relation. Now suppose $(P,Q)\in (\bigcup_i {\cal
R}_i)^\ast$. Then there are $P_j \ (j=0,\ldots ,n)$ for certain $n \in
\mbox{\rm I\hspace{-0.75mm}N}$, such that $P=P_o$, $Q=P_n$ and (for
$j=1,\ldots ,n$) $(P_{j-1},P_j)\in {\cal R}_k$ for certain $k\in I$.
Suppose $S\in Pr/(\bigcup_i {\cal R}_i)^\ast$ and $\alpha\in Act$.
Let $1 \leq j \leq n$ and $(P_{j-1},P_j)\in {\cal R}_k$.
Since $S$ is the union of a number of equivalence classes $T\in
Pr/{\cal R}_k$ and $\mu_N (P_{j-1},\,\alpha,\,T)=\mu_N
(P_j,\,\alpha,\,T)$ for any $T\in Pr/{\cal R}_k$, it follows that
$\mu_N (P_{j-1},\,\alpha,\,S)=\mu_N (P_j,\,\alpha,\,S)$.  This is true
for all $j=1,\ldots ,n$; thus $\mu_N (P,\,\alpha,\,S)=\mu_N
(Q,\,\alpha,\,S)$. Hence $(\bigcup_i {\cal R}_i )^\ast$ is a
bisimulation.\hfill $\Box$

\begin{corollary} $(${\bf Equivalence}$)$
Bisimulation equivalence is an equivalence relation on $Pr$.
\end{corollary}

\noindent
{\bf Proof:} From the definition of $\Nequiv$ it
follows that on $Pr$ we have \[\Nequiv\ =\; \bigcup\,\{ \; {\cal R} \;
| \; {\cal R} \mbox{ is nonprobabilistic bisimulation}\,\}\]
Thus by Proposition \ref{propo-union}, $\Nequiv$ is itself a
bisimulation and hence an equivalence relation.\hfill $\Box$

It is not difficult to see that a nonprobabilistic bisimulation is
just a strong bisimulation \cite{milner83,milner89} that happens to be an
equivalence relation. Since strong bisimulation equivalence, defined as
the union of all strong bisimulations, is an equivalence relation itself
\cite{milner83,milner89}, this is not a limiting restriction and nonprobabilistic
bisimulation equivalence (being the union of all nonprobabilistic
bisimulations) coincides with strong bisimulation equivalence.

The following congruence theorem stems from Milner \cite{milner83,milner89}.
Our proof is a bit different from Milner's because we insist that
bisimulations should be equivalences and reason in terms of the
function $\mu_N$ rather than using the underlying transitions. This
pays off when we add the probabilities.

In the proof of the theorem, we lift the PCCS operators to {\em sets\/} of
expressions, which is done in the natural way.  For example, for $S \subseteq
Pr$, $A \subseteq Act$, $S \rstr A$ designates the set $\{ P \rstr A \;|\; P
\in S \}$.

A PCCS {\em context} is defined as a PCCS expression that may contain a
special constant $\Omega$. If ${\cal C}$ is a PCCS context and $E$
a PCCS expression, then ${\cal C}[E]$ is the result of substituting
$E$ for all occurrences of $\Omega$ in ${\cal C}$, and ${\cal C}
{\raisebox{0pt}[0pt][0pt]{\tiny $\begin{array}{@{}c@{}} 
\mbox{\footnotesize $[E]$}\\ \mbox{fix}\!_X\!\end{array}$}}$
(${\cal C}\Enfix$) is the result of substituting $E$ for all occurrences of
$\Omega$ in ${\cal C}$ that are (not) in the scope of an operator $\fix_X$.
Although we are only interested in contexts with exactly one ``hole'', \ie one
occurrence of $\Omega$, it is technically advantageous (in the congruence
proofs) to also allow contexts without holes or with more than one hole.
In ${\cal C}[E]$, though, all our holes are instantiated with the same
expression $E$. The set of all restriction-guarded PCCS
contexts is denoted $\mbox{PCCS}[\ ]$.
\bigskip

\begin{theorem} $(${\bf Congruence}$)$ For ${E},{F} \in
{\rm PCCS}$, ${\cal C} \in \mbox{\rm PCCS}[\ ]$: \ \
${E}\Nequiv {F}$ \ implies \ ${\cal C}[{E}]\Nequiv
{\cal C}[{F}]$
\label{thm-ncon}
\end{theorem}

\noindent
{\bf Proof:} 
The case of open PCCS expressions ${\cal C}[{E}],\ {\cal C}[{F}]$
can be reduced to the closed case, by considering ${\cal C}[{E}]$,
${\cal C}[{F}]$ under all possible substitutions. 
Note that for an expression ${\cal C}[E]$ any variable in $E$ is either bound
within $E$, free in $E$ but bound within ${\cal C}[E]$, or free even in 
${\cal C}[E]$.  Due to the definition of bisimulation equivalence on open
terms, we can eliminate from further consideration variables of the last
kind, as well as free variables occurring in $\cal C$.
Now, adopting the convention that ``$C \in \mbox{PCCS}[\ ]^*$'' should be read
as ``$C \in \mbox{PCCS}[\ ]$ such that
${\cal C}[{E}],\ {\cal C}[{F}] \in Pr$'', it is enough to show that
the equivalence (\ie reflexive, symmetric, and transitive) closure ${\cal R}$
of ${\cal R}'=\{({\cal C}[{E}], {\cal C}[{F}])\mid$ $E\Nequiv
F,~{\cal C} \in \mbox{PCCS}[\ ]^*\}$ is a 
bisimulation. This can be established by showing that for all 
$(P,Q) \in {\cal R}$, $S\in Pr/{\cal R}$ and $\alpha\in Act$, $$\mu_N
(P,\alpha,\,S)=\mu_N (Q,\alpha,\,S)$$ 
We may assume $(P,Q)\in {\cal R}'$, because the extension to 
the equivalence closure is straightforward. Thus we have to show that
for all $E,F\in {\rm PCCS}$ with \raisebox{0pt}[0pt][0pt]{$E\Nequiv F$},
\begin{equation}
\forall {\cal C} \in \mbox{PCCS}[\ ]^*,\ \forall S\in Pr/{\cal R},\ \forall
\alpha\in Act,\ \ \mu_N ({\cal C}[{E}],\,\alpha,\,S) = \mu_N ({\cal
C}[{F}],\,\alpha,\,S)
\label{eqn-congr-nonprob}
\end{equation}
We proceed by induction on the number of free variables in $E$ and
$F$.  Let $E,F\in\mbox{PCCS}$ such that $E\Nequiv F$, and suppose
(\ref{eqn-congr-nonprob}) is established for pairs $E',F'\in{\rm
PCCS}$ with fewer free variables. Then it is enough to establish only
one direction of (\ref{eqn-congr-nonprob}), with $\leq$ substituted
for $=$, as the converse direction, $\geq$, follows by symmetry.
Write $N \vdash_n P \aRa P'$ if the transition $P \aRa P'$ can be
derived by a proof-tree of depth $n$ or less, and define $\mu_N^n :
(Pr \times Act \times {\cal P} (Pr)) \longrightarrow \{0,1\}$ by:
\[\mu_N^n (P,\,\alpha ,\,S)=\left\{\begin{array}{cl}1 & \mbox{if }
\exists Q\in S \mbox{ with } N \vdash_n P\aRa Q\\ 0 & \mbox{otherwise} 
\end{array} \right. \]
Now $\mu_N (P,\alpha,\,S)={\displaystyle\lim_{n \rightarrow \infty}}
\mu_N^n (P,\alpha,\,S)$, so we only have to show that for all $n\geq 0$,
\begin{equation}
\forall {\cal C} \in \mbox{PCCS}[\ ]^*,\ \forall S\in Pr/{\cal R},\ \forall
\alpha\in Act,\ \ \mu_N^n ({\cal C}[{E}],\,\alpha,\,S) \leq \mu_N ({\cal
C}[{F}],\,\alpha,\,S)
\label{eqn-congr}
\end{equation}
This will be done by induction to $n$.

The case $n=0$ is trivial, so we may assume (\ref{eqn-congr}) for a certain
$n \geq 0$. In proving (\ref{eqn-congr}) for $n+1$ we distinguish seven cases,
depending on the topmost operator (or lack thereof) of ${\cal C}$. From
here onwards we drop the subscripts $N$. 
\begin{description}
\item [Empty context:] We have to show that for all 
$S\in Pr/{\cal R}$ and $\alpha\in Act$,
\begin{equation}
\mu^{n+1} (E,\,\alpha,\,S)\leq\mu(F,\,\alpha,\,S)
\label{eqn-congr-empty}
\end{equation}
 $\Nequiv$ is contained in the equivalence relation ${\cal R}$. Thus
$S$ is the disjoint union of one or more $T \in Pr/\Nequiv$, and it
suffices to prove (\ref{eqn-congr-empty}) for these $T$ instead of
$S$.
This follows immediately from $E \Nequiv F$:
$$\mu^{n+1} (E,\,\alpha,\,T)\leq\mu(E,\,\alpha,\,T)=\mu(F,\,\alpha,\,T)$$
Note that at this point we cannot obtain (\ref{eqn-congr}) with the superscript
$n$ at both sides of the inequality.
\item [Action prefixing:] We have to show that for all
${\cal C} \in \mbox{PCCS}[\ ]^*$, $S\in Pr/{\cal R}$ and $\beta\in Act$,
\begin{equation}
\mu^{n+1} (\alpha\,.\,{\cal C}[{E}],\,\beta,\,S)\leq\mu(\alpha\,.\,{\cal
C}[{F}],\,\beta,\,S)
\label{eqn-congr-act}
\end{equation}
$$\mbox{For any }E \in~\mbox{\rm PCCS},~ \mu^{n+1}
(\alpha\,.\,E,\,\beta,\,S)=\mu(\alpha\,.\,E,\,\beta,\,S)\ =\ \left\{ 
\begin{array}{cl}1 & \mbox{if } \alpha = \beta \mbox{ and } E \in S\\
0 & \mbox{otherwise} \end{array} \right.$$
Thus, if $\alpha \not= \beta$ requirement (\ref{eqn-congr-act}) is
fulfilled trivially, 
and if $\alpha = \beta$ it follows since ${\cal C}[{E}]$ and ${\cal C}[{F}]$
are in the same equivalence class $S'\in Pr/{\cal R}$.
\item [Summation:] We have to show that for all ${\cal
C}_i  \in \mbox{PCCS}[\ ]^*$, $S\in Pr/{\cal R}$ and $\alpha \in Act$,
\begin{equation}
\mu^{n+1} (\sum_{i\in I} \lbrack p_i\rbrack\, {\cal C}_i
[{E}],\,\alpha,\,S)\leq
\mu(\sum_{i\in I} \lbrack p_i\rbrack\, {\cal C}_i [{F}],\,\alpha,\,S)
\label{eqn-congr-sum}
\end{equation}
Indeed, using LHS and RHS to denote the left- and right-hand sides of
(\ref{eqn-congr-sum}), we infer
$$\mbox{LHS}= \max_{i\in I} (\mu^n ({\cal C}_i[{E}],\,\alpha,\,S))
\begin{array}[b]{c} \mbox{\footnotesize induction}\\ \leq\end{array}
\max_{i\in I} (\mu ({\cal C}_i [{F}],\,\alpha,\,S))=\mbox{RHS}$$
\item [Product:] We have to show that for all ${\cal
C}_i  \in \mbox{PCCS}[\ ]^*$ ($i=1,2$), $S\in Pr/{\cal R}$ and $\gamma \in Act$,
\begin{equation}
\mu^{n+1} ({\cal C}_1 [{E}]\times {\cal C}_2 [{E}],\,\gamma,\,S)\leq
\mu ({\cal C}_1 [{F}]\times {\cal C}_2 [{F}],\,\gamma,\,S)
\label{eqn-congr-prod}
\end{equation}
Since $\mu^{n+1} ({\cal C}_1 [{E}]\times {\cal C}_2 [{E}],\,\gamma,\,S-
(Pr\times Pr))=0$, we may in (\ref{eqn-congr-prod}) replace $S$ by $S
\cap (Pr \times Pr)$. By the definition of ${\cal R}$ we have $(P_1,P_2)
\in {\cal R} \wedge (Q_1,Q_2) \in {\cal R} \Rightarrow (P_1 \times Q_1
, P_2 \times Q_2) \in {\cal R}$. Hence $S \cap (Pr \times Pr)$ is the
disjoint union of a collection of sets of the form $S_1 \times S_2$ with
$S_1,S_2\in Pr/{\cal R}$, and it suffices to prove (\ref{eqn-congr-prod}) for
such sets $S_1 \times S_2$ instead of $S \cap (Pr \times Pr)$. Moreover we may
assume that $\gamma$ is of the form $(\alpha,\beta)$, since otherwise
$\mu^{n+1} ({\cal C}_1 [{E}]\times {\cal C}_2 [{E}],\,\gamma,\,S)=0$ and
we are done. Thus we have to show that for all ${\cal
C}_i  \in \mbox{PCCS}[\ ]^*$, $S_i\in Pr/{\cal R}$ ($i=1,2$) and
$\alpha,\beta \in Act$, $$\mu^{n+1} ({\cal C}_1 [{E}]\times {\cal C}_2
[{E}],\,(\alpha,\beta),\,S_1 \times S_2) \leq \mu ({\cal C}_1
[{F}]\times {\cal C}_2 [{F}],\,(\alpha,\beta),\,S_1 \times S_2)$$
$$\mbox{LHS}=\mu^n ({\cal C}_1 [{E}],\,\alpha,\,S_1)\cdot\mu^n ({\cal
C}_2 [{E}],\,\beta,\,S_2) \begin{array}[b]{c}
\mbox{\footnotesize induction}\\ \leq\end{array} \mu ({\cal C}_1
[{F}],\,\alpha,\,S_1)\cdot\mu ({\cal C}_2 [{F}],\,\beta,\,S_2)
=\mbox{RHS}$$
\item [Restriction:] We have to show that for all ${\cal
C}  \in \mbox{PCCS}[\ ]^*$, $A \subseteq Act$, $S\in Pr/{\cal R}$ and $\alpha
\in Act$, 
\begin{equation}
\mu^{n+1} ({\cal C} [{E}]\rstr A,\,\alpha,\,S)\leq
\mu ({\cal C} [{F}]\rstr A,\,\alpha,\,S)
\label{eqn-congr-rstr}
\end{equation}
Since $\mu^{n+1} ({\cal C} [{E}]\rstr A,\,\alpha,\,S- Pr\rstr A)=0$, we
may in (\ref{eqn-congr-rstr}) replace $S$ by $S
\cap (Pr \rstr A)$. By the definition of ${\cal R}$ we have $(P_1,P_2)
\in {\cal R} \Rightarrow (P_1 \rstr A, P_2 \rstr A) \in {\cal R}$.
Hence $S \cap (Pr \rstr A)$ is the disjoint union of a collection of
sets of the form $S' \rstr A$ with $S'\in Pr/{\cal
R}$, and it suffices to prove (\ref{eqn-congr-rstr}) for such sets
$S'\rstr A$ instead of $S \cap (Pr \rstr A)$. Moreover we may
assume that $\alpha \in A$, since otherwise
$\mu^{n+1} ({\cal C} [{E}]\rstr A,\,\alpha,\,S)=0$ and
we are done. Thus we have to show that for all ${\cal
C}  \in \mbox{PCCS}[\ ]^*$, $A \subseteq Act$, $S'\in Pr/{\cal R}$ and
$\alpha \in A$, $$\mu^{n+1} ({\cal C} [{E}]\rstr A,
\,\alpha,\,S'\rstr A) \leq \mu ({\cal C} [{F}]\rstr A,\,\alpha,\,S'\rstr A)$$
$$\mbox{LHS}=\mu^n ({\cal C} [{E}],\,\alpha,\,S') \begin{array}[b]{c}
\mbox{\footnotesize induction}\\ \leq\end{array} \mu ({\cal C}
[{F}],\,\alpha,\,S')=\mbox{RHS}$$
\item [Relabeling:] We have to show that for all ${\cal
C}  \in \mbox{PCCS}[\ ]^*$, $f:Act \rightarrow Act$, $S\in Pr/{\cal R}$ and
$\beta \in Act$, 
\begin{equation}
\mu^{n+1} ({\cal C} [{E}][f],\,\beta,\,S)\leq
\mu ({\cal C} [{F}][f],\,\beta,\,S)
\label{eqn-congr-relab}
\end{equation}
Since $\mu^{n+1} ({\cal C} [{E}][f],\,\beta,\,S- Pr[f])=0$, we
may in (\ref{eqn-congr-relab}) replace $S$ by $S
\cap Pr[f]$. By the definition of ${\cal R}$ we have $(P_1,P_2)
\in {\cal R} \Rightarrow (P_1 [f], P_2 [f]) \in {\cal R}$.
Hence $S \cap Pr[f]$ is the disjoint union of a collection of
sets of the form $S'[f]$ with $S'\in Pr/{\cal
R}$, and it suffices to prove (\ref{eqn-congr-relab}) for such sets
$S'[f]$ instead of $S \cap Pr[f]$.
Thus we have to show that for all ${\cal
C}  \in \mbox{PCCS}[\ ]^*$, $f:Act \rightarrow Act$, $S'\in Pr/{\cal R}$ and
$\beta \in Act$, $$\mu^{n+1} ({\cal C} [{E}][f],
\,\beta,\,S'[f]) \leq \mu ({\cal C} [{F}][f],\,\beta,\,S'[f])$$
$$\mbox{LHS}=\max_{f(\alpha)=\beta} (\mu^n ({\cal C}
[{E}],\,\alpha,\,S')) \begin{array}[b]{c} \mbox{\footnotesize
induction}\\ \leq\end{array} \max_{f(\alpha)=\beta} (\mu ({\cal C} 
[{F}],\,\alpha,\,S'))=\mbox{RHS}$$
\item [Recursion:] We have to show that for all ${\cal C} \in \mbox{PCCS}[\ ]$
with $\fix_X{\cal C} \in \mbox{PCCS}[\ ]^*$,
$S\in Pr/{\cal R}$ and $\alpha\in Act$,
$$\mu^{n+1} (\fix_X {\cal C}[{E}],\,\alpha,\,S)\leq\mu(\fix_X {\cal
C}[{F}],\,\alpha,\,S)$$
In case $X$ does not occur free in $E$ or $F$ this follows since\sht
$$\mbox{LHS}= \mu^n ({\cal C}[{E}]\{\fix_X {\cal
C}[{E}]/X\},\,\alpha,\,S) = \mu^n ({\cal C}\{\fix_X {\cal
C}/X\}[{E}],\,\alpha,\,S) \begin{array}[b]{c} \mbox{\footnotesize
induction}\\ \leq\end{array}$$ $$\mu ({\cal C}\{\fix_X {\cal
C}/X\}[{F}],\,\alpha,\,S) = \mu ({\cal C}[{F}]\{\fix_X {\cal
C}[{F}]/X\},\,\alpha,\,S)=\vspace{1ex}\mbox{RHS}$$
In case $X$ does occur free in $E$ or $F$ we have
$E\{\fix_X {\cal C}[F]/X\} \Nequiv F\{\fix_X {\cal C}[F]/X\}$
by Definition~\ref{def-Nequiv}, and since these expressions have fewer
free variables than $E$ and $F$ it follows that
\begin{equation}\label{eqn-rec}
\mu({\cal C}\{\fix_X{\cal C}/X\}\Ffix[E\{\fix_X {\cal C}[F]/X\}],\,\alpha,\,S)=
\mu({\cal C}\{\fix_X{\cal C}/X\}\Ffix[F\{\fix_X {\cal C}[F]/X\}],\,\alpha,\,S)
\end{equation}
$$\mbox{Hence\ \ LHS}=\mu^n({\cal C}[{E}]\{\fix_X{\cal C}[{E}]/X\},
\,\alpha,\,S)= \mu^n({\cal C}\Enfix\{\fix_X{\cal C}/X\}[E],\,\alpha,\,S)
\begin{array}[b]{c} \mbox{\footnotesize induction}\\ \leq\end{array}$$
$$\mu({\cal C}\Enfix\{\fix_X{\cal C}/X\}[F],\,\alpha,\,S)
%=\mu({\cal C}[E]\{\fix_X{\cal C}[F]/X\},\,\alpha,\,S)
\begin{array}[b]{c} \mbox{\footnotesize (\ref{eqn-rec})}\\ = \end{array}
\mu({\cal C}[F]\{\fix_X{\cal C}[F]/X\},\,\alpha,\,S)
=\mbox{RHS}$$
This argument is illustrated in Figure~\ref{fig-congruence}.\qed
\end{description}

\begin{figure}[htb]
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
    \graphtemp=.5ex\advance\graphtemp by 3.125in
    \rlap{\kern 0.875in\lower\graphtemp\hbox to 0pt{\hss $\cal C$\hss}}%
    \special{pn 8}%
    \special{pa 875 2500}%
    \special{pa 250 3750}%
    \special{fp}%
    \special{pa 875 2500}%
    \special{pa 1500 3750}%
    \special{fp}%
    \special{pa 250 3750}%
    \special{pa 437 3750}%
    \special{fp}%
    \special{pa 563 3750}%
    \special{pa 875 3750}%
    \special{fp}%
    \special{pa 1000 3750}%
    \special{pa 1187 3750}%
    \special{fp}%
    \special{pa 1313 3750}%
    \special{pa 1500 3750}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 3.750in
    \rlap{\kern 0.500in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 3.438in
    \rlap{\kern 0.938in\lower\graphtemp\hbox to 0pt{\hss $\fix_X$\hss}}%
    \special{pa 938 3500}%
    \special{pa 938 3656}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 3.750in
    \rlap{\kern 0.938in\lower\graphtemp\hbox to 0pt{\hss $\Omega$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 3.750in
    \rlap{\kern 1.250in\lower\graphtemp\hbox to 0pt{\hss $\Omega$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 4.562in
    \rlap{\kern 0.875in\lower\graphtemp\hbox to 0pt{\hss \begin{tabular}{c}and a context $\cal C$ with\\ one free occurrence of $X$,\\ one hole in the scope\\ of an operator $\fix_X$\\ and one hole outside\\ such a scope\end{tabular}\hss}}%
    \special{sh 0.100}%
    \special{pa 375 938}%
    \special{pa 625 938}%
    \special{pa 625 313}%
    \special{pa 375 313}%
    \special{pa 375 938}%
    \special{ip}%
    \graphtemp=.5ex\advance\graphtemp by 0.312in
    \rlap{\kern 0.500in\lower\graphtemp\hbox to 0pt{\hss $E$\hss}}%
    \special{pa 375 313}%
    \special{pa 375 938}%
    \special{fp}%
    \special{pa 625 313}%
    \special{pa 625 938}%
    \special{fp}%
    \special{pa 375 938}%
    \special{pa 437 938}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.938in
    \rlap{\kern 0.500in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \special{pa 562 938}%
    \special{pa 625 938}%
    \special{fp}%
    \special{sh 0.300}%
    \special{pa 1125 938}%
    \special{pa 1375 938}%
    \special{pa 1375 313}%
    \special{pa 1125 313}%
    \special{pa 1125 938}%
    \special{ip}%
    \graphtemp=.5ex\advance\graphtemp by 0.312in
    \rlap{\kern 1.250in\lower\graphtemp\hbox to 0pt{\hss $F$\hss}}%
    \special{pa 1125 313}%
    \special{pa 1125 938}%
    \special{fp}%
    \special{pa 1375 313}%
    \special{pa 1375 938}%
    \special{fp}%
    \special{pa 1125 938}%
    \special{pa 1187 938}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.938in
    \rlap{\kern 1.250in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \special{pa 1313 938}%
    \special{pa 1375 938}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.562in
    \rlap{\kern 0.875in\lower\graphtemp\hbox to 0pt{\hss \begin{tabular}{c}Two terms $E$ and $F$,\\ each with one free\\ occurrence of\\ a variable $X$\end{tabular}\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.625in
    \rlap{\kern 2.750in\lower\graphtemp\hbox to 0pt{\hss $\cal C$\hss}}%
    \special{pa 2750 0}%
    \special{pa 1812 1875}%
    \special{fp}%
    \special{pa 2750 0}%
    \special{pa 3688 1875}%
    \special{fp}%
    \special{pa 1812 1875}%
    \special{pa 2062 1875}%
    \special{fp}%
    \special{pa 2312 1875}%
    \special{pa 2781 1875}%
    \special{fp}%
    \special{pa 2906 1875}%
    \special{pa 3250 1875}%
    \special{fp}%
    \special{pa 3375 1875}%
    \special{pa 3688 1875}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.875in
    \rlap{\kern 2.188in\lower\graphtemp\hbox to 0pt{\hss $\fix_X$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 1.500in
    \rlap{\kern 2.844in\lower\graphtemp\hbox to 0pt{\hss $\fix_X$\hss}}%
    \special{pa 2844 1563}%
    \special{pa 2844 1781}%
    \special{fp}%
    \special{sh 0.100}%
    \special{pa 2656 2750}%
    \special{pa 3031 2750}%
    \special{pa 3031 1875}%
    \special{pa 2656 1875}%
    \special{pa 2656 2750}%
    \special{ip}%
    \graphtemp=.5ex\advance\graphtemp by 1.875in
    \rlap{\kern 2.844in\lower\graphtemp\hbox to 0pt{\hss $E$\hss}}%
    \special{pa 2656 1875}%
    \special{pa 2656 2750}%
    \special{fp}%
    \special{pa 3031 1875}%
    \special{pa 3031 2750}%
    \special{fp}%
    \special{pa 2656 2750}%
    \special{pa 2781 2750}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 2.750in
    \rlap{\kern 2.844in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \special{pa 2906 2750}%
    \special{pa 3031 2750}%
    \special{fp}%
    \special{sh 0.100}%
    \special{pa 3125 2750}%
    \special{pa 3500 2750}%
    \special{pa 3500 1875}%
    \special{pa 3125 1875}%
    \special{pa 3125 2750}%
    \special{ip}%
    \graphtemp=.5ex\advance\graphtemp by 1.875in
    \rlap{\kern 3.313in\lower\graphtemp\hbox to 0pt{\hss $E$\hss}}%
    \special{pa 3125 1875}%
    \special{pa 3125 2750}%
    \special{fp}%
    \special{pa 3500 1875}%
    \special{pa 3500 2750}%
    \special{fp}%
    \special{pa 3125 2750}%
    \special{pa 3188 2750}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 2.750in
    \rlap{\kern 3.313in\lower\graphtemp\hbox to 0pt{\hss $\fix_X$\hss}}%
    \special{pa 3438 2750}%
    \special{pa 3500 2750}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 2.562in
    \rlap{\kern 2.188in\lower\graphtemp\hbox to 0pt{\hss $\cal C$\hss}}%
    \special{pa 2188 1938}%
    \special{pa 1563 3187}%
    \special{fp}%
    \special{pa 2188 1938}%
    \special{pa 2813 3187}%
    \special{fp}%
    \special{pa 1563 3187}%
    \special{pa 1750 3187}%
    \special{fp}%
    \special{pa 1875 3187}%
    \special{pa 2188 3187}%
    \special{fp}%
    \special{pa 2313 3187}%
    \special{pa 2500 3187}%
    \special{fp}%
    \special{pa 2625 3187}%
    \special{pa 2813 3187}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 3.187in
    \rlap{\kern 1.812in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 2.875in
    \rlap{\kern 2.250in\lower\graphtemp\hbox to 0pt{\hss $\fix_X$\hss}}%
    \special{pa 2250 2938}%
    \special{pa 2250 3094}%
    \special{fp}%
    \special{sh 0.100}%
    \special{pa 2125 3812}%
    \special{pa 2375 3812}%
    \special{pa 2375 3187}%
    \special{pa 2125 3187}%
    \special{pa 2125 3812}%
    \special{ip}%
    \graphtemp=.5ex\advance\graphtemp by 3.187in
    \rlap{\kern 2.250in\lower\graphtemp\hbox to 0pt{\hss $E$\hss}}%
    \special{pa 2125 3187}%
    \special{pa 2125 3812}%
    \special{fp}%
    \special{pa 2375 3187}%
    \special{pa 2375 3812}%
    \special{fp}%
    \special{pa 2125 3812}%
    \special{pa 2188 3812}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 3.812in
    \rlap{\kern 2.250in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \special{pa 2313 3812}%
    \special{pa 2375 3812}%
    \special{fp}%
    \special{sh 0.100}%
    \special{pa 2438 3812}%
    \special{pa 2688 3812}%
    \special{pa 2688 3187}%
    \special{pa 2438 3187}%
    \special{pa 2438 3812}%
    \special{ip}%
    \graphtemp=.5ex\advance\graphtemp by 3.187in
    \rlap{\kern 2.562in\lower\graphtemp\hbox to 0pt{\hss $E$\hss}}%
    \special{pa 2438 3187}%
    \special{pa 2438 3812}%
    \special{fp}%
    \special{pa 2688 3187}%
    \special{pa 2688 3812}%
    \special{fp}%
    \special{pa 2438 3812}%
    \special{pa 2500 3812}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 3.812in
    \rlap{\kern 2.562in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \special{pa 2625 3812}%
    \special{pa 2688 3812}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 3.438in
    \rlap{\kern 3.313in\lower\graphtemp\hbox to 0pt{\hss $\cal C$\hss}}%
    \special{pa 3313 2813}%
    \special{pa 2688 4063}%
    \special{fp}%
    \special{pa 3313 2813}%
    \special{pa 3938 4063}%
    \special{fp}%
    \special{pa 2688 4063}%
    \special{pa 2875 4063}%
    \special{fp}%
    \special{pa 3000 4063}%
    \special{pa 3313 4063}%
    \special{fp}%
    \special{pa 3438 4063}%
    \special{pa 3625 4063}%
    \special{fp}%
    \special{pa 3750 4063}%
    \special{pa 3938 4063}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 4.062in
    \rlap{\kern 2.938in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 3.750in
    \rlap{\kern 3.375in\lower\graphtemp\hbox to 0pt{\hss $\fix_X$\hss}}%
    \special{pa 3375 3812}%
    \special{pa 3375 3969}%
    \special{fp}%
    \special{sh 0.100}%
    \special{pa 3250 4688}%
    \special{pa 3500 4688}%
    \special{pa 3500 4063}%
    \special{pa 3250 4063}%
    \special{pa 3250 4688}%
    \special{ip}%
    \graphtemp=.5ex\advance\graphtemp by 4.062in
    \rlap{\kern 3.375in\lower\graphtemp\hbox to 0pt{\hss $E$\hss}}%
    \special{pa 3250 4063}%
    \special{pa 3250 4688}%
    \special{fp}%
    \special{pa 3500 4063}%
    \special{pa 3500 4688}%
    \special{fp}%
    \special{pa 3250 4688}%
    \special{pa 3313 4688}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 4.688in
    \rlap{\kern 3.375in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \special{pa 3438 4688}%
    \special{pa 3500 4688}%
    \special{fp}%
    \special{sh 0.100}%
    \special{pa 3563 4688}%
    \special{pa 3813 4688}%
    \special{pa 3813 4063}%
    \special{pa 3563 4063}%
    \special{pa 3563 4688}%
    \special{ip}%
    \graphtemp=.5ex\advance\graphtemp by 4.062in
    \rlap{\kern 3.688in\lower\graphtemp\hbox to 0pt{\hss $E$\hss}}%
    \special{pa 3563 4063}%
    \special{pa 3563 4688}%
    \special{fp}%
    \special{pa 3813 4063}%
    \special{pa 3813 4688}%
    \special{fp}%
    \special{pa 3563 4688}%
    \special{pa 3625 4688}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 4.688in
    \rlap{\kern 3.688in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \special{pa 3750 4688}%
    \special{pa 3813 4688}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 5.188in
    \rlap{\kern 2.750in\lower\graphtemp\hbox to 0pt{\hss $\begin{array}{c}{\cal C}[{E}]\{\fix_X{\cal C}[{E}]/X\}\\[5pt] ={\cal C}\Enfix\{\fix_X{\cal C}/X\}[E]\end{array}$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.625in
    \rlap{\kern 5.250in\lower\graphtemp\hbox to 0pt{\hss $\cal C$\hss}}%
    \special{pa 5250 0}%
    \special{pa 4313 1875}%
    \special{fp}%
    \special{pa 5250 0}%
    \special{pa 6188 1875}%
    \special{fp}%
    \special{pa 4313 1875}%
    \special{pa 4563 1875}%
    \special{fp}%
    \special{pa 4813 1875}%
    \special{pa 5281 1875}%
    \special{fp}%
    \special{pa 5406 1875}%
    \special{pa 5750 1875}%
    \special{fp}%
    \special{pa 5875 1875}%
    \special{pa 6188 1875}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.875in
    \rlap{\kern 4.688in\lower\graphtemp\hbox to 0pt{\hss $\fix_X$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 1.500in
    \rlap{\kern 5.344in\lower\graphtemp\hbox to 0pt{\hss $\fix_X$\hss}}%
    \special{pa 5344 1563}%
    \special{pa 5344 1781}%
    \special{fp}%
    \special{sh 0.300}%
    \special{pa 5156 2750}%
    \special{pa 5531 2750}%
    \special{pa 5531 1875}%
    \special{pa 5156 1875}%
    \special{pa 5156 2750}%
    \special{ip}%
    \graphtemp=.5ex\advance\graphtemp by 1.875in
    \rlap{\kern 5.344in\lower\graphtemp\hbox to 0pt{\hss $F$\hss}}%
    \special{pa 5156 1875}%
    \special{pa 5156 2750}%
    \special{fp}%
    \special{pa 5531 1875}%
    \special{pa 5531 2750}%
    \special{fp}%
    \special{pa 5156 2750}%
    \special{pa 5281 2750}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 2.750in
    \rlap{\kern 5.344in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \special{pa 5406 2750}%
    \special{pa 5531 2750}%
    \special{fp}%
    \special{sh 0.100}%
    \special{pa 5625 2750}%
    \special{pa 6000 2750}%
    \special{pa 6000 1875}%
    \special{pa 5625 1875}%
    \special{pa 5625 2750}%
    \special{ip}%
    \graphtemp=.5ex\advance\graphtemp by 1.875in
    \rlap{\kern 5.812in\lower\graphtemp\hbox to 0pt{\hss $E$\hss}}%
    \special{pa 5625 1875}%
    \special{pa 5625 2750}%
    \special{fp}%
    \special{pa 6000 1875}%
    \special{pa 6000 2750}%
    \special{fp}%
    \special{pa 5625 2750}%
    \special{pa 5688 2750}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 2.750in
    \rlap{\kern 5.812in\lower\graphtemp\hbox to 0pt{\hss $\fix_X$\hss}}%
    \special{pa 5938 2750}%
    \special{pa 6000 2750}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 2.562in
    \rlap{\kern 4.688in\lower\graphtemp\hbox to 0pt{\hss $\cal C$\hss}}%
    \special{pa 4688 1938}%
    \special{pa 4063 3187}%
    \special{fp}%
    \special{pa 4688 1938}%
    \special{pa 5313 3187}%
    \special{fp}%
    \special{pa 4063 3187}%
    \special{pa 4250 3187}%
    \special{fp}%
    \special{pa 4375 3187}%
    \special{pa 4688 3187}%
    \special{fp}%
    \special{pa 4813 3187}%
    \special{pa 5000 3187}%
    \special{fp}%
    \special{pa 5125 3187}%
    \special{pa 5313 3187}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 3.187in
    \rlap{\kern 4.312in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 2.875in
    \rlap{\kern 4.750in\lower\graphtemp\hbox to 0pt{\hss $\fix_X$\hss}}%
    \special{pa 4750 2938}%
    \special{pa 4750 3094}%
    \special{fp}%
    \special{sh 0.300}%
    \special{pa 4625 3812}%
    \special{pa 4875 3812}%
    \special{pa 4875 3187}%
    \special{pa 4625 3187}%
    \special{pa 4625 3812}%
    \special{ip}%
    \graphtemp=.5ex\advance\graphtemp by 3.187in
    \rlap{\kern 4.750in\lower\graphtemp\hbox to 0pt{\hss $F$\hss}}%
    \special{pa 4625 3187}%
    \special{pa 4625 3812}%
    \special{fp}%
    \special{pa 4875 3187}%
    \special{pa 4875 3812}%
    \special{fp}%
    \special{pa 4625 3812}%
    \special{pa 4688 3812}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 3.812in
    \rlap{\kern 4.750in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \special{pa 4812 3812}%
    \special{pa 4875 3812}%
    \special{fp}%
    \special{sh 0.300}%
    \special{pa 4937 3812}%
    \special{pa 5187 3812}%
    \special{pa 5187 3187}%
    \special{pa 4937 3187}%
    \special{pa 4937 3812}%
    \special{ip}%
    \graphtemp=.5ex\advance\graphtemp by 3.187in
    \rlap{\kern 5.062in\lower\graphtemp\hbox to 0pt{\hss $F$\hss}}%
    \special{pa 4937 3187}%
    \special{pa 4937 3812}%
    \special{fp}%
    \special{pa 5187 3187}%
    \special{pa 5187 3812}%
    \special{fp}%
    \special{pa 4937 3812}%
    \special{pa 5000 3812}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 3.812in
    \rlap{\kern 5.062in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \special{pa 5125 3812}%
    \special{pa 5187 3812}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 3.438in
    \rlap{\kern 5.812in\lower\graphtemp\hbox to 0pt{\hss $\cal C$\hss}}%
    \special{pa 5813 2813}%
    \special{pa 5188 4063}%
    \special{fp}%
    \special{pa 5813 2813}%
    \special{pa 6438 4063}%
    \special{fp}%
    \special{pa 5188 4063}%
    \special{pa 5375 4063}%
    \special{fp}%
    \special{pa 5500 4063}%
    \special{pa 5813 4063}%
    \special{fp}%
    \special{pa 5938 4063}%
    \special{pa 6125 4063}%
    \special{fp}%
    \special{pa 6250 4063}%
    \special{pa 6438 4063}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 4.062in
    \rlap{\kern 5.438in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 3.750in
    \rlap{\kern 5.875in\lower\graphtemp\hbox to 0pt{\hss $\fix_X$\hss}}%
    \special{pa 5875 3812}%
    \special{pa 5875 3969}%
    \special{fp}%
    \special{sh 0.300}%
    \special{pa 5750 4688}%
    \special{pa 6000 4688}%
    \special{pa 6000 4063}%
    \special{pa 5750 4063}%
    \special{pa 5750 4688}%
    \special{ip}%
    \graphtemp=.5ex\advance\graphtemp by 4.062in
    \rlap{\kern 5.875in\lower\graphtemp\hbox to 0pt{\hss $F$\hss}}%
    \special{pa 5750 4063}%
    \special{pa 5750 4688}%
    \special{fp}%
    \special{pa 6000 4063}%
    \special{pa 6000 4688}%
    \special{fp}%
    \special{pa 5750 4688}%
    \special{pa 5813 4688}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 4.688in
    \rlap{\kern 5.875in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \special{pa 5938 4688}%
    \special{pa 6000 4688}%
    \special{fp}%
    \special{sh 0.300}%
    \special{pa 6063 4688}%
    \special{pa 6312 4688}%
    \special{pa 6312 4063}%
    \special{pa 6063 4063}%
    \special{pa 6063 4688}%
    \special{ip}%
    \graphtemp=.5ex\advance\graphtemp by 4.062in
    \rlap{\kern 6.188in\lower\graphtemp\hbox to 0pt{\hss $F$\hss}}%
    \special{pa 6063 4063}%
    \special{pa 6063 4688}%
    \special{fp}%
    \special{pa 6312 4063}%
    \special{pa 6312 4688}%
    \special{fp}%
    \special{pa 6063 4688}%
    \special{pa 6125 4688}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 4.688in
    \rlap{\kern 6.188in\lower\graphtemp\hbox to 0pt{\hss $X$\hss}}%
    \special{pa 6250 4688}%
    \special{pa 6312 4688}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 5.188in
    \rlap{\kern 5.250in\lower\graphtemp\hbox to 0pt{\hss $\begin{array}{c}{\cal C}\Enfix\{\fix_X{\cal C}/X\}[F]=\\[5pt]{\cal C}\{\fix_X{\cal C}/X\}\Ffix[E\{\fix_X {\cal C}[F]/X\}]\end{array}$\hss}}%
    \hbox{\vrule depth5.188in width0pt height 0pt}%
    \kern 6.438in
  }%
}%
\centerline{\raise 1em\box\graph}
\caption{The last steps in the congruence proof.}
\label{fig-congruence}
\end{figure}

% From bus@daimi.dk Sun Mar 18 14:37:26 1990
\newcommand{\doublersigma}{\mbox{\parbox{8ex}{\[ \sum_{i \in I} 
\sum_{j \in J}\]}$[p_{ij}] \, \alpha_{i}\,.\, E_{}$}}

\section{The Reactive Model}
\label{sec-react}

The reactive model of probabilistic processes was introduced by Larsen and
Skou in \cite{larsen-skou-prob-bisim}.  In this section, we consider the
reactive model within the context of $\PCCSR$, the sublanguage of PCCS with
guarded recursion and without relabeling.  We begin by presenting the
reactive operational semantics for $\PCCSR$ that defines a probabilistic
transition system for every $\PCCSR$ process.  We then
equip the model with a notion of probabilistic bisimulation, also due to
Larsen and Skou, and show that the resulting equivalence relation is a
congruence with respect to $\PCCSR$.

We restrict ourselves to guarded recursion in order to ensure that the
reactive summation operator is well-defined.
That we do not give a reactive semantics to the relabeling operator is
due to an inherent incompatibility between this operation and the
reactive viewpoint.  For example, consider process $P = \frac{1}{2}
a.X + \frac{1}{2} b.Y$.  $P$ has a probability-1 $a$-transition to $X$
and a probability-1 $b$-transition to $Y$.  However, if the relabeling
that maps $a$ to itself and $b$ to $a$ is applied to $P$, then we may
end up with a ``nonsensical'' object having two probability-1
$a$-transitions.  Some form of relabeling could be defined in the
reactive model if an appropriate normalization procedure were applied.
Here three normalization procedures come to mind. Let $Q =
\frac{1}{3} a.X + \frac{1}{3} a.X + \frac{1}{6} b.Y +\frac{1}{6} c.Z$
and again rename $b$ into $a$. Now a ``syntactic'' normalization
procedure would yield a probability-$\frac{1}{5}$ $a$-transition to
$Y$. This is also the solution obtained by abstracting from the
generative or stratified model (\ie by applying $\phiGR \circ \phiG$
or $\phiSR \circ \phiS$), and from the counterexample in Section
\ref{sec-inter-GR} it follows that this solution is not compositional.
An intermediate normalization procedure would yield a
probability-$\frac{1}{3}$ $a$-transition to $Y$ (by counting the
number of summands that can do an $a$-step). But then $Q$ and $Q'=
\frac{2}{3} a.X + \frac{1}{6} b.Y + \frac{1}{6} c.Z$ would behave
differently after relabeling, and bisimulation equivalence would not
be a congruence. Finally a ``semantic'' normalization procedure would
give the $a$-transition to $Y$ probability $\frac{1}{2}$ (by counting
the number of actions that are renamed into $a$), but here the
disadvantage is that first renaming $b$ in $a$ and then $c$ in $a$
yields a different outcome than doing this in the reverse order.  Of
course, injective relabelings can be added without problem.

A solution to the problem of defining relabeling in the
reactive model has recently been found by Larsen and Skou [personal
communication]. They propose to equip a relabeling that renames
actions $a_1, \dots ,a_n$ into $a$ with a probability distribution
that associates a probability $p_i$ to each of the $a_i$'s. These
probabilities then determine the normalization factor.
As such a probabilistic relabeling is meaningless in the generative
and stratified models, we will not consider this solution in the
present paper.

The same problems encountered in defining renaming in the reactive
model apply to the SCCS product, as relabeling can be expressed in
terms of product and the other SCCS operators. For this reason, we
have ``split'' the SCCS product in the PCCS product and relabeling, only
the latter of which has to be sacrificed in the reactive model.

%reactive model defined only on the sublanguage $\PCCSR$
%general summation not compatible with reactive model for several reasons:  The
%most obvious is that almost by definition a reactive process is very
%specified:  for any potential action there should be a clear probability
%distribution.  Also what does it mean to sum in a process like $\zero$?
%On the technical side, there are two candidates for defining the reactive
%operational semantics of general summation: 1) structurally - but
%commutativity result with generative model fails to hold in this case.
%2) flattening probability structure to get action-guarded sum and work from
%there - but reactive bisimulation not a congruence in this case.

\subsection{Reactive Operational Semantics of ${\bf PCCS_{R}}$}

The reactive operational semantics of $\PCCSR$ is given in Figure~\ref{fig-ros}
as a set of inference rules.  
Reactive transitions are of the form
\sht
\begin{center}
$\rarrow {P}{\alpha[p]}{P'}{i}$ 
\end{center}
\vspace{-.15in}
meaning that $P$, with probability $p$, can perform an $\alpha$-transition to
become $P'$.  The index $i$ is explained just below.

%\input{fig-ros}
\begin{figure*}
\centering
$\begin{array}{llll}
\hline \\
          &             & \rarrow{\alpha . E}{\alpha[1]}{E}{0} & \\[0.2cm]

\rarrow{E_{j}}{\alpha[q]}{\!E'}{k} & \Longrightarrow &
\Rarrow{\gsigma}{\alpha[p_{j} \cdot q/r]}{E'}{j.k} 
&\mbox{\scriptsize $(j\in I,\ r = \displaystyle \sum_{i\in I} 
\displaystyle{ \{ \hspace{-.032in} | } p_i \mid {E_i}\stackrel{\alpha[s]}{  
\mbox{\raisebox{3.6pt}{$_\subset$}}
\!\!\!\!-\!\!\!-\!\!\!\rightarrow}_{l}{E''}
\displaystyle{ | \hspace{-.034in} \} } )$}\\[0.2cm]

\rarrow{E}{\alpha[p]}{E'}{i}, \; \rarrow{F}{\beta [q]}{F'}{j} &
\Longrightarrow & \Rarrow{E \times F}{\alpha \beta\, [p \cdot q]}
{E' \times F'}{(i,j)} \\[0.2cm]

\rarrow{E}{\alpha[p]}{E'}{i} & \Longrightarrow &
\rarrow{E \rstr A}{\alpha[p]}{E'\rstr A}{i} &(\alpha \in A) \\[0.2cm]

\rarrow{E \{\fix_X E / X\}}{\alpha[p]}{E'}{i} &  \Longrightarrow &
\rarrow{\fix_{X} E}{\alpha[p]}{E'}{i}
\\[0.2cm] \hline
\end{array}$
\caption{Reactive operational semantics of $\PCCSR$.}
\label{fig-ros}
\end{figure*}

In the second rule, in which $\multisetl,\multisetr$ denote multiset brackets,
$r$ is the normalization factor used to compute the
{\em conditional probabilities} of the sum under the assumption $\alpha$.
The rest of the rules
are straightforward adaptations of their nonprobabilistic counterparts.

Unlike in the nonprobabilistic case, all probabilistic transitions are
indexed.  The set $I_R$ of reactive indices is the smallest set such
that $0\in I_R$, \ $j \in I_0, k\in I_R \Rightarrow j.k \in I_R$, and $i,j\in
I_R \Rightarrow (i,j)\in I_R$. The purpose of the  
indices is to distinguish different {\em occurrences} of the same probabilistic
transition. They are constructed so that every outgoing probabilistic
transition of an expression has a unique index. (The indices will be used in
the next section to define {\em cumulative} probability distributions.)
The following example is illustrative:
$$\rarrow {([\frac{1}{2}]a\,.\,\zero + [\frac{1}{2}]a\,.\,\zero)}
{a[\frac{1}{2}]} {\zero} {1.0}
\hspace{1in}
\rarrow {([\frac{1}{2}]a\,.\,\zero + [\frac{1}{2}]a\,.\,\zero)}
{a[\frac{1}{2}]} {\zero} {2.0}$$

As in the nonprobabilistic case, the reactive operational rules collectively
define the semantic mapping $\phiR$ from $\PrR$, the closed expressions
of $\PCCSR$, and even from the open $\PCCSR$ expressions, to the domain of
reactive probabilistic labeled transition systems. 

\begin{definition}
A {\em reactive (probabilistic) transition system} is a triple (S,T,I) with
\vspace{-.6em}
\begin{itemize}
\item[\bf --] S a set of {\em states},
\vspace{-.3em}
\item[\bf --] $T \subseteq S \times Act \times (0,1] \times I_R \times S$
a set of {\em transitions}, such that
\begin{enumerate}
\item $((s,\alpha,p,i,t)\in T \wedge (s,\beta,q,i,r)\in T) \Rightarrow
(\alpha =\beta \wedge p=q \wedge t=r)$
\item $\forall s\in S,\ \forall \alpha\in Act,\ \sum \multisetl p
\,|\, \exists i\in I_R,\ t\in S:\ (s,\alpha,p,i,t)\in T \multisetr \in \{0,1\}$
\end{enumerate}
\vspace{-.3em}
\item[\bf --] and $I \in S$ the {\em initial} state.
\end{itemize}
\end{definition}

The first requirement of T says that all outgoing transitions of a
given state have different indices. The second one says that for each
state the probabilities of the outgoing $\alpha$-transitions, if there
are any, sum up to 1, for any action $\alpha$ separately. An
isomorphism between two reactive transition systems is a bijective
mapping $f$ between their reachable states {\em and} transitions,
satisfying $f(s,\alpha,p,i,t) = (f(s),\alpha,p,j,f(t))$, where $i$ and
$j$ may be different indices, and $f(I)=I'$, where $I$ and $I'$ are
the initial states of the two systems.  The mapping $\phiR$ is defined
just as $\phiN$ in the previous section. It is not difficult to see
that $\phiR (P)$ meets the requirements for reactive transition
systems.

\subsection{Reactive Bisimulation}
\label{sec-rbisim}

We now consider {\em reactive bisimulation}, a notion of probabilistic
bisimulation for reactive processes due
to Larsen and Skou \cite{larsen-skou-prob-bisim}.  By definition, all
reactive bisimulations are equivalence relations.  Intuitively, two
processes $P$,$Q$ are probabilistically bisimilar in the reactive model if, for
each action symbol, they derive reactive bisimulation classes with equal
cumulative probability.
 
To define reactive bisimulation, we first need to define the {\em cumulative
probability distribution function} (cPDF) which computes the total probability
by which a process derives a set of processes.
Adopting the convention that the empty sum of probabilities is 0, we have:

\begin{definition} $(${\bf Reactive cPDF}$)$ $\mu_{R}$: $
(\PrR \times Act \times {\cal P}(\PrR) ) \longrightarrow [0, 1]$ is the total function 
given by\,: $\forall \alpha \in Act$, $\forall \, P \in \PrR$,
$\forall \, S \subseteq \PrR$,
\[
\mu_{R} (P, \alpha, S) = \sum_{i\in I_R}
\multisetl \; p_{i} \, | \rarrow{P}{\alpha [ p_{i} ]}{Q}{i} \mbox{ and } 
Q \in S \multisetr \]
\label{def-rcPDF}
\end{definition}

Reactive bisimulation can now be defined as follows:

\begin{definition} {\bf (\cite{larsen-skou-prob-bisim})}
\label{def-rbisim}
An equivalence relation ${\cal R}$ $\subseteq \PrR \times \PrR$ is a {\em
reactive bisimulation} if $(P, Q) \in {\cal R}$ implies\,: $\forall
S \in \PrR/{\cal R}, \ \forall \alpha \in Act$,
\[ \mu_{R} (P, \alpha, S ) =  \mu_{R} (Q, \alpha, S ) \]
Two processes $P, Q$ are {\em  reactive bisimulation equivalent} (written
$P \, \Requiv \, Q$) if there exists a reactive bisimulation ${\cal R}$
such that $(P, Q) \in {\cal R}$.
\end{definition}

By the same proof as was used for nonprobabilistic bisimulation,
reactive bisimulation equivalence can be shown to be an equivalence
relation indeed.
Furthermore, reactive bisimulation equivalence is the largest reactive
bisimulation and can be found by a straightforward
adaptation of the fixed-point iteration technique of \cite{milner89}.

Like strong bisimulation does for SCCS or CCS, reactive bisimulation
equivalence provides a compositional semantics for $\PCCSR$ that
is consistent with the operational semantics defined in the last section. 
Specifically:

\pagebreak[3]
\vspace{1.5ex}
\begin{theorem} $(${\bf Congruence}$)$ For ${E}, {F} \in
{\rm PCCS}_R$, ${\cal C} \in \PCCSR [\ ]$: \ \ ${E}
\Requiv {F}$ \ implies \ ${\cal C}[{E}] \Requiv {\cal
C}[{F}]$
\label{thm-rcon}  
\end{theorem}
{\bf Proof:} Following the previous congruence proof, we 
define $\cal R$ as the equivalence closure of ${\cal R}'=\{({\cal C}[{E}],
{\cal C}[{F}])\mid E\Requiv F,~{\cal C}\in\PCCSR[\ ]^*\}$. 
The {\em top\/} of a context ${\cal C}\in\PCCSR[\ ]$ is the part that remains
after first removing every subcontext of the form $\alpha.E$ and subsequently
every subcontext not containing $\Omega$.
Now let $\PCCSR^k [\ ]$ be the set of all
$\PCCSR$ contexts with at most $k$ nested summation
operators in their top. This time we have to show that
for all $E,F\in \PCCSR$ with \raisebox{0pt}[0pt][0pt]{$E\Requiv F$},
and for all $k\in \mbox{\rm I\hspace{-0.75mm}N}$,
\begin{equation}
\forall {\cal C} \in \PCCSR^k [\ ]^*,\ \forall S\in \PrR/{\cal R},\ \forall
\alpha\in Act,\ \ \mu_R ({\cal C}[{E}],\,\alpha,\,S) = \mu_R ({\cal
C}[{F}],\,\alpha,\,S)
\label{eqn-congr-react}
\end{equation}
This will be done by three nested inductions. First we apply induction on the
number of free variables in $E$ and $F$ and choose $E,F\in\PCCSR$ with
$E\Requiv F$ for the induction step. Then we apply induction on $k$ and
suppose (\ref{eqn-congr-react}) holds for $k<l$. Finally the proof of
(\ref{eqn-congr-react}) for $k=l$ continues exactly like the one
for $\Nequiv$ (\ie with induction on the depth of derivations), substituting
$R$ for $N$ and $\PCCSR^l [\ ]$ for ${\rm PCCS} 
[\ ]$, except that the function $\mu_{R}^n$: $
(\PrR \times Act \times {\cal P}(\PrR) ) \longrightarrow [0, 1]$ is
given by\,: $\forall \alpha \in Act$, $\forall \, P \in \PrR$,
$\forall \, S \subseteq \PrR$,
\[\mu_{R}^n (P, \alpha, S) = \sum_{i\in I_R}
\multisetl \; p_{i} \, |\, R \vdash_n \rarrow{P}{\alpha [ p_{i}
]}{Q}{i} \mbox{ and }  Q \in S \multisetr \]
and every time we invoke the induction hypothesis, we check
that it is applied to contexts in $\PCCSR^l [\ ]^*$ only (in the case
of recursion this follows by guardedness of $\PCCSR$ expressions). Moreover
the case of relabeling is dropped---the congruence proof
would break down where the operation~~max~~is applied---and
the last line in the case of summation is replaced by:
$$\mbox{LHS}=\frac{\sum_{i\in I} p_i\cdot \mu_R^n ({\cal C}_i[{E}],\,\alpha,\,S)}
{\sum_{i\in I} \multisetl p_i \mid \mu_R ({\cal C}_i[{E}],\alpha,\PrR)
\neq 0 \multisetr }
\begin{array}{c} \mbox{\footnotesize induction}\\ \leq \\
\mbox{\footnotesize (\ref{eqn-congr-react})} \end{array}
\frac{\sum_{i\in I} p_i\cdot \mu_R ({\cal C}_i [{F}],\,\alpha,\,S)}
{\sum_{i\in I} \multisetl p_i \mid \mu_R ({\cal C}_i[{F}],\alpha,\PrR)
\neq 0 \multisetr } =\mbox{RHS}$$
Here (\ref{eqn-congr-react}) may be applied since ${\cal C}_i \in
\PCCSR^{l-1}[\ ]^*$. \hfill $\Box$ 


% From bus@daimi.dk Sun Mar 18 14:37:45 1990
\section{The Generative Model}

In contrast to the reactive model, which is defined only over the sublanguage
$\PCCSR$ of PCCS, the generative model is defined over full PCCS.  In this
section, we provide PCCS with a generative operational semantics.  We then
extend the notion of reactive bisimulation to the generative case and show that
the resulting equivalence is a congruence with respect to PCCS.

\subsection{Generative Operational Semantics of PCCS}

The generative operational semantics of PCCS is
given in Figure~\ref{fig-gos}.  We use a different kind of arrow (non-hooked)
to distinguish generative transitions from reactive ones. 
As in the reactive case, generative transitions are
indexed to distinguish multiple occurrences of the same probabilistic
transition.  The set $I_G$ of generative indices is equal to $I_R$.

%\input{fig-gos}
\begin{figure*}
\centering
$\begin{array}{llll}
\hline \\
          &             & \garrow{\alpha . E}{\alpha[1]}{E}{0} & \\[0.2cm]

\garrow{E_{j}}{\alpha[q]}{\!E'}{k} & \Longrightarrow &
\Garrow{\gsigma}{\alpha[p_{j} \cdot q]}{E'}{j.k} 
& (j \in I) \\[0.2cm]

\garrow{E}{\alpha[p]}{E'}{i}, \; \garrow{F}{\beta [q]}{F'}{j} &
\Longrightarrow & \Garrow{E \times F}{\alpha \beta\, [p \cdot q]}
{E' \times F'}{(i,j)} & \\[0.2cm]

\garrow{E}{\alpha[p]}{E'}{i} & \Longrightarrow &
\Garrow{E \rstr A}{\alpha[p/r]}{E'\rstr A}{i} & 
${\small $(\alpha \in A\,, \ r = \nu_{G}(E,A))$}$ \\[0.2cm]

\garrow{E}{\alpha[p]}{E'}{i} & \Longrightarrow &
\Garrow{E[f]}{f(\alpha) [p]}{E'[f]}{i} & \\[0.2cm]

\garrow{E \{\fix_X E / X\}}{\alpha[p]}{E'}{i} &  \Longrightarrow &
\garrow{\fix_{X} E}{\alpha[p]}{E'}{i} &
\\[0.2cm] \hline
\end{array}$
\caption{Generative operational semantics of PCCS.}
\label{fig-gos}
\end{figure*}

With the exception of restriction, all rules are straightforward adaptations of
their nonprobabilistic counterparts.  The restriction rule defines the 
probabilistic transitions of 
$E \rstr A $ in terms of the {\em conditional probabilities} of $E$ under the
assumption $A$. In
this rule, the function $\nu_{G}$ computes the {\em generative normalization 
factor} such that $\nu_{G} ( E, A )$ is the sum of the probabilities
of the transitions of $E$ labeled by symbols from $A$. 
The formal definition of $\nu_{G}$ is given by
\[ \nu_{G} ( E, A ) = 
\sum_{i \in I_{G}} \multisetl \,  p_{i} \; | \; \garrow{E}{\alpha
[p_i]}{E_{i}}{i} \ ,\ \alpha \in A \multisetr \]
Note that under the assumptions $\garrow{E}{\alpha [p]}{E'}{i}$ and
$\alpha \in A$, $\nu_{G}(E,A) > 0$.
As we consider restriction-guarded recursion only, it will follow from
the proof of Theorem \ref{thm-gcon} that $\nu_{G}$ is well-defined.

To illustrate the generative operational semantics, consider the expression
\sht
\begin{center}
$E = (a\,.\,\zero) \times 
([\frac{1}{3}]b\,.\,X + [\frac{1}{3}]c\,.\,Y + [\frac{1}{3}]\zero)$
\sht
\end{center}
We have:
\sht
\begin{center}
\Garrow{E}{(a,b)[\frac{1}{3}]}{\zero \times X}{(0,1.0)} \hspace{.4in}
\Garrow{E}{(a,c)[\frac{1}{3}]}{\zero \times Y}{(0,2.0)} 
\end{center}
As $\nu_{G}(E,\{(a,b)\}) = \frac{1}{3}$, we also have:
\begin{center}
$\Garrow{E \rstr \{(a,b)\}}  {(a,b)[1]}  {(\zero \times X)\rstr \{(a,b)\}}
{(0,1.0)}$
\end{center}

A generative process is said to be {\em stochastic} if the sum of the
probabilities of its derivations is 1. Otherwise, when this sum is
strictly less than 1, the process is said to be {\em substochastic},
and therefore possesses a non-zero probability of deadlock.  PCCS
expressions (contexts) without \zero, unguarded recursion and restriction
{\em preserve stochasticity\/}: if stochastic processes are
substituted for their free variables, then the obtained processes are
stochastic as well.  In the case of restriction, the obtained process
may have no derivations at all.

The normalization factor $\nu_{G}(E,A)$ used in the restriction rule
of Figure~\ref{fig-gos} is such that a substochastic process placed in
a restriction context becomes stochastic or deadlocks completely.
Alternatively, the relative probability of deadlock in a substochastic
process can be preserved by normalizing by the quantity $r =
\nu_{G}(E,A)+1-\nu_{G}(E,Act)$.  The term $1 - \nu_{G}(E,Act)$
represents the probability of deadlock in $E$.  To illustrate, we
would have in the above example that $\nu_{G}(E,Act) = \frac{2}{3}$,
$r = \frac{2}{3}$, and thus:
\sht
\begin{center}
$\Garrow {E \rstr \{(a,b)\}}  {(a,b)[\frac{1}{2}]}  
{(\zero \times X) \rstr \{(a,b)\}}  {(0,1.0)}$
\end{center} 
In fact, deadlock preserving and eliminating restriction operators can
be combined in one language by introducing an operator $\rstr A$ for
$A \subseteq Act \cup \{\zero\}$.  From here on all results apply to
this extended language.  In Figure~\ref{fig-gos} the generative
normalization factor is now extended by
$$\nu_G (E,A\dcup 0) = \nu_{G}(E,A)+1-\nu_{G}(E,Act)$$
for $A \subseteq Act$. In the reactive and nonprobabilistic models
$\rstr(A\dcup 0)$ is defined exactly as $\rstr A$.

A generative process is called {\em semistochastic} if the sum of the
probabilities of its derivations is 0 or 1. PCCS expressions
(contexts) without summation preserve semistochasticity, but a
summation context, or an unguarded recursion context with summation,
may introduce non-semistochastic behavior. Each of the expressions
\begin{center}
$\frac{1}{2} a.\zero + \frac{1}{2} \zero\ \ \ \ \ \mbox{and}\ \ \ \ \ 
\fix_X (\frac{2}{3} (X[(a,b)\rightarrow a]\times X[(a,b)\rightarrow
b]) + \frac{1}{3} (a,b).X)$
\end{center}
for instance has a deadlock probability of $\frac{1}{2}$. PCCS may be
turned into a semistochastic language by replacing the summation
operator by a semistochastic variant,\sht\ which can be expressed
in our language as $( \gsigma ) \rstr Act$\sht\ (using our
deadlock eliminating restriction operator), and adapting the definition
of restriction-guardedness. In this language there will be
no difference between the deadlock preserving and deadlock eliminating
restriction operator, and $[p]\,X+[1-p]\,\zero \equiv X$.

A generative transition system is defined as a reactive transition
system, except that the second requirement of $T$ is changed into
$$\forall s\in S,\ \sum \multisetl p \,|\, \exists \alpha\in Act,\
i\in I_G,\ t\in S:\ (s,\alpha,p,i,t)\in T \multisetr \leq 1$$
Also, the semantic mapping $\phiG$ from PCCS to the domain of generative
transition systems is defined exactly as $\phiN$ and $\phiR$.

\subsection{Generative Bisimulation}
\label{sec-gbisim}

The extension of reactive bisimulation to the generative model is
straightforward.  The definition of the generative cPDF $\mu_{G}$ is the same 
as
Definition~\ref{def-rcPDF} except that it is defined over $Pr$ and in terms of
indexed generative transitions.  Likewise, the definition of a generative
bisimulation and of $\Gequiv$ are the same as in Definition~\ref{def-rbisim},
except that they are defined over $Pr$ and in terms of $\mu_{G}$.
Similar to the reactive case, $\Gequiv$ is substitutive in PCCS.

\vspace{1.5ex}
\begin{theorem} $(${\bf Congruence}$)$ For ${E}, {F} \in
{\rm PCCS}$, ${\cal C} \in \mbox{\rm PCCS}[\ ]$: \ \
${E} \Gequiv {F}$ \ implies \ ${\cal C}[{E}] \Gequiv
{\cal C}[{F}]$
\label{thm-gcon}  
\end{theorem}
{\bf Proof:} We follow the reactive congruence proof, but this time
with ${\rm PCCS}^k[\ ]$ the set of PCCS contexts with at most $k$
nested {\em restriction} operators in their top, until we have to show,
for $k \in \mbox{\rm I\hspace{-0.75mm}N}$,
\begin{equation}
\forall {\cal C} \in {\rm PCCS}^k [\ ]^*,\ \forall S\in Pr/{\cal R},\ \forall
\alpha\in Act,\ \ \mu_G ({\cal C}[{E}],\,\alpha,\,S) = \mu_G ({\cal
C}[{F}],\,\alpha,\,S)
\label{eqn-congr-gen}
\end{equation}
Again, this will be done by induction on $k$. Suppose (\ref{eqn-congr-gen})
holds for $k<l$. It then follows that 
\begin{equation}
\forall k<l,\
\forall {\cal C} \in {\rm PCCS}^k[\ ]^*,\ \forall A\subseteq Act\dcup\{0\},\ \ 
\nu_G ({\cal C}[{E}],A) = \nu_G ({\cal C}[{F}],A)
\label{eqn-nu}
\end{equation}
because (restricting w.l.o.g.\ to the case $A \subseteq Act$)
$$\nu_G (P,A) = \sum_{\stackrel{\alpha
\in A}{S \in Pr/{\cal R}}} \mu_G (P,\,\alpha,\,S)$$
Now the proof of (\ref{eqn-congr-gen}) for $k=l$ continues just like
the one for $\Nequiv$, defining $\mu_G^n$ similar to $\mu_R^n$ and
substituting ${\rm PCCS}^l [\ ]$ for ${\rm PCCS} [\ ]$, except that
the occurrences of \ max \ in the cases of summation and relabeling
are replaced by $\sum$ (in the case of summation followed by
$p_i\cdot$), and every time we invoke the induction hypothesis, we
check that it is applied to contexts in ${\rm PCCS}^l [\ ]^*$ only (in
the case of recursion this follows by restriction-guardedness of PCCS
expressions). Moreover the last line in the case of restriction is
replaced by: $$\mbox{LHS}=\frac{\mu^n ({\cal C}
[{E}],\,\alpha,\,S')}{\nu ({\cal C}[{E}],A)}
\begin{array}{c} \mbox{\footnotesize induction}\\ \leq \\
\mbox{\footnotesize (\ref{eqn-nu})} \end{array} \frac{\mu ({\cal C}
[{F}],\,\alpha,\,S')}{\nu ({\cal C}[{F}],A)}=\mbox{RHS}$$
Here (\ref{eqn-nu}) may be applied since ${\cal C} \in {\rm PCCS}^{l-1}[\ ]^*$.
\hfill $\Box$

% From bus@daimi.dk Sun Mar 18 14:38:25 1990
\section{The Stratified Model}

The treatments of the nonprobabilistic, reactive and generative models
are extended here to the stratified case.

\subsection{Stratified Operational Semantics of PCCS}

The stratified operational semantics of PCCS is comprised of two types of
transition relations: {\em action transitions} (as in the nonprobabilistic
model) and {\em probability transitions}. Action transitions are of the form
$\garrow{P\,}{\alpha}{Q}{}$. Probability transitions are of the form
$\sarrow{P}{p}{Q}{i}$, meaning that $P$, with probability $p$, can behave as
the process $Q$. Here $i$ is an index from the set $I_{S} = I_{S}^{0}-\{0\}$,
where $I_{S}^{0}$ is the smallest set such that $0\in I_S^0$, $I_0 \subseteq
I_{S}^{0}$ and $i,j \in I_{S}^{0} \Rightarrow (i,j) \in I_{S}^{0}$.
This separation of action and probability in the stratified model
permits the branching structure of the purely probabilistic choices to be
captured explicitly.  The inference rules for probability transitions appear in
Figure~\ref{fig-sos}; the rules for action transitions are the same as
in the nonprobabilistic case, except that there is no rule for process
summation, since in the stratified model the only choice mechanism is
probabilistic. Only the probability transitions need to be indexed.
This bi-structured approach to operational semantics was (to our knowledge)
first presented in \cite{tofts90} to give a semantics for a timed version of 
CCS.
Note that no PCCS expression admits both action and probability
transitions. Thus the set of PCCS processes is partitioned into {\em
action processes} (admitting action transitions), {\em probability
processes} (admitting probability transitions), and {\em deadlock
processes} (admitting neither).

\begin{figure}
\centering
$\begin{array} {llll}
\hline
   &   &
\sarrow{\gsigma}{p_{j}}{E_j}{j} & (j \in I) \\[0.2cm]

%\garrow{E\ }{\alpha}{E'}{}      &  \Longrightarrow  &
%\sarrow{E}{1}{E}{1} \\[0.2cm]

\sarrow{E}{p}{E'}{i}, \; \sarrow{F}{q}{F'}{j} & \Longrightarrow &
\sarrow{E \times F}{p \cdot q}{ E' \times F'}{(i,j)} \\[0.2cm]

\sarrow{E}{p}{E'}{i}, \; \garrow{F\ }{\alpha}{F'}{} & \Longrightarrow &
\sarrow{E \times F}{p}{E' \times F}{(i,0)} \\[0.2cm]

\garrow{E\ }{\alpha}{E'}{}, \; \sarrow{F}{p}{F'}{i} & \Longrightarrow &
\sarrow{E \times F}{p}{E \times F'}{(0,i)} \\[0.2cm]

\sarrow{E}{p}{E'}{i}, \; E'\stackrel{A}{\longrightarrow} & \Longrightarrow & 
\Sarrow{E \rstr A}{p/\nu_{S}(E,A)}{E'\rstr A}{i} \\[0.2cm]

\sarrow{E}{p}{E'}{i} & \Longrightarrow & \sarrow{E[f]}{p}{E' [f]}{i} \\[0.2cm]

\sarrow{E \{\fix_X E / X\}}{p}{E'}{i} & \Longrightarrow &
\sarrow{\fix_{X} E}{p}{E'}{i}
\\[0.2cm] \hline
\end{array}$
\caption{Stratified operational semantics of PCCS.}
\label{fig-sos}
\end{figure}

Except for the rules for product and restriction, all of the
inferences rules for probability transitions are straightforward
adaptations of their nonprobabilistic counterparts.  The third and
fourth rules say that the product of an action process and a
probability process is a probability process.
They are needed to avoid deadlock in a synchronous product
that is caused by a difference in depth of the purely probabilistic
branching structures of the argument processes. For example, we do not
want \,$(\frac{1}{2}\, a.\zero + \frac{1}{2}\, b.\zero) \times c.\zero$\, to 
deadlock simply because there does not exist a probability transition in the
right hand argument.

As in the generative operational semantics, the restriction rule
expresses the probability transitions of $E \rstr A$ in terms of the
conditional probabilities of $E$ under the assumption $A$.
Intuitively, $E \rstr A$\, behaves like $E$, where all probability
transitions to subexpressions that necessarily require the execution
of a restricted action are eliminated. The probabilities associated
with these transition are evenly distributed among the remaining
probability transitions.

\noindent
The predicate $\stackrel{A}{\longrightarrow}$ for $A \subseteq Act$ is
defined by $E\stackrel{A}{\longrightarrow}$ if
$E=\sarrow{E_0}{p_1}{}{i_1}\hspace{-.5em}
\sarrow{E_1}{p_2}{}{i_2}\hspace{-.3em} \cdots
\sarrow{}{p_n}{}{i_n}\hspace{-.5em} \garrow{E_n}{\alpha}{\!E'}{}$
for certain $n \in \mbox{\rm I\hspace{-0.75mm}N}$ and $\alpha \in A$.
It is extended to $A \subseteq Act\dcup\{0\}$ by
$E\stackrel{A\dcup\{0\}}{\longrightarrow}$ iff
$(E\stackrel{A}{\longrightarrow} \vee
\garrow{E\!}{Act}{}{} \hspace{-2em}/\hspace{1.15em} )$.
Thus the condition $E'\stackrel{A}{\longrightarrow}$
in the rule premise requires that derivative $E'$ of $E$ is capable 
of performing an action transition from the set $A$ of permitted
actions (or, in case $0\in A$, deadlocks).
The function $\nu_{S}$ calculates the {\em stratified normalization 
factor} and is defined by
\[ \nu_{S} ( E, A ) = 
\sum_{i \in I_{S}} \multisetl \,  p_{i} \; | \; \sarrow{E}{p_i}{E_{i}}{i}
\ ,\ \garrow{E_i}{A}{}{} \multisetr \]
As in the generative case, it will follow from the proof of Theorem
\ref{thm-scon} that $\stackrel{A}{\longrightarrow}$ and $\nu_{S}$ are
well-defined. 

%\[ \nu_{S} ( E, A) = \left\{ \begin{array}{l}
%%1 & \mbox{if} \ E \ \not \hspace{-.04in} \longmapsto \mbox{~and~} E \ \not 
%%\hspace{-.04in} \longrightarrow \\
%1 \ \ \ \mbox{if}\  \garrow{E}{\alpha}{}{}, \; \alpha \in A \\
%0 \ \ \  \mbox{if}\  \garrow{E}{\beta}{}{}, \; \beta \not \in A; 
%                  \ \ \ \ \ \mbox{else} \\
%\sum_{i} \multisetl \,  p_{i} \; | \; \sarrow{E}{p_{i}}{E_{i}}{i}  
% \ ,\ \nu_{S} ( E_{i}, A) \neq 0 \multisetr
%\end{array} \right. \]

To illustrate the inference rule for restriction,
consider the process 
\sht
\begin{center}
$P \; = \; \frac{1}{3}\,
a.\zero\, + \,\frac{2}{3}\, (\frac{1}{2}\, b.\zero\, + \,\frac{1}{2}\, 
c.\zero)$ 
\sht
\end{center}
In the following, $P$ is placed in some relevant
restriction contexts, resulting in the restriction-free processes on the
right-hand side.
\[
\begin{array}{lcl}
P \, \rstr \{b,c \} & \equiv & 1\, (\frac{1}{2}\, b.\zero\, +
\,\frac{1}{2}\, c.\zero) \\
P \, \rstr \{a,c \} & \equiv &  \frac{1}{3}\, a.\zero\, +
\,\frac{2}{3}\, 1\, c.\zero\\
P \, \rstr \{c \} & \equiv &  1\, (1\, c.\zero )\\
\end{array}
\]
Here $\equiv$ denotes isomorphism of the associated labeled transition
systems.

% As in the generative case, the inference rule for restriction can be adapted
% in order to preserve the relative probability of deadlock in a substochastic
% process.  This is accomplished by replacing, both in Figure
% \ref{fig-sos} and in the definition of $\nu_S$, the clause
% $\garrow{E}{A}{}{}$ by $(\garrow{E}{A}{}{} \vee \garrow{E}{Act}{}{}
% \hspace{-2em}/\hspace{1.15em} )$.  Again, the reader may verify that our
% theorems continue to hold.

The inference rules for action and probability transitions define the
semantic mapping $\phiS$ from PCCS to the domain of stratified
probabilistic labeled transition systems. Such transition systems have
{\em action states}, having exactly one outgoing action transition,
{\em probability states}, having only outgoing probability
transitions, all with a different index, and {\em deadlock states},
having no outgoing transitions. Stratified transition systems are {\em
semistochastic} in the sense that for each probability state the sum of
the probabilities of its outgoing transitions is 1. A state with a
sequence of probability transition to a deadlocked state corresponds
to a substochastic state in the generative model.


\subsection{Stratified Bisimulation}

Stratified bisimulation is similar to reactive and generative bisimulation in
that processes are required to derive stratified bisimulation equivalence
classes with equal cumulative probability. However, the separation of
probability and action in the stratified operational semantics is reflected in
the definition of stratified bisimulation.

To define stratified bisimulation, we need to: (1) define a function that
computes the total probability by which a process can behave the same as
any process in a set of processes (the technique is analogous to the one in
Definition~\ref{def-rcPDF}, and thus the details are omitted); (2) lift,
as in Definition~\ref{def-ncPDF}, the action relations to {\em
sets} of derivative processes.  The {\em stratified cumulative PDF}
$\mu_{S}$ incorporates both (1) and (2) in an integrated fashion.  In
particular, $\mu_{S}$ is of the form
\[ \mu_{S}: (Pr \times
(Act \ \cup \ \{\, * \, \} ) \times {\cal P}(Pr) ) \longrightarrow [ 0, 1] \]
where $*$ is a dummy symbol used to mark probability transitions.
That is, for 
$\alpha \!\in \!Act, \,\mu_{S} (P, \alpha , S) \in \{\, 0, 1 \, \}$
indicates whether or not $P$ has an $\alpha$--transition to some process 
in $S$. 
\hspace{-0.44308pt}Otherwise,
$\mu_{S} (P, * , S) \in [ 0, 1]$ specifies the total probability by which
$P$ may behave the same as any process in $S$.

\begin{definition} 
An equivalence relation ${\cal R}$ $\subseteq Pr \times Pr$ is a {\em
stratified bisimulation} if $(P, Q) \in {\cal R}$ implies $\forall
S \in Pr/{\cal R}, \ \forall \alpha \in Act \cup \{ * \}$,
\[ \mu_{S} (P, \alpha, S ) =  \mu_{S} (Q, \alpha, S ) \]
Two processes $P, Q$ are {\em  stratified  bisimulation equivalent} (written 
$P \, \Sequiv \, Q$) if there exists a stratified bisimulation ${\cal R}$
such that $(P, Q) \in {\cal R}$.
\end{definition}

\vspace{1.5ex}
\begin{theorem} $(${\bf Congruence}$)$ For ${E}, {F} \in {\rm
PCCS}$, ${\cal C} \in \mbox{\rm PCCS}[\ ]$: \ \ ${E} \Sequiv {F}$ \
implies \ ${\cal C}[{E}] \Sequiv {\cal C}[{F}]$
\label{thm-scon}  
\end{theorem}
{\bf Proof:} By induction on $k$ (as in the generative case) we establish
\begin{equation}
\forall {\cal C} \in {\rm PCCS}^k [\ ]^*,\ \forall S\in Pr/{\cal R},\ \forall
\alpha\in Act \cup \{ * \},\ \ \mu_S ({\cal C}[{E}],\,\alpha,\,S) =
\mu_S ({\cal C}[{F}],\,\alpha,\,S)
\label{eqn-congr-strat}
\end{equation}
where ${\cal R}$ is defined as usual. Suppose (\ref{eqn-congr-strat})
holds for $k<l$. It then follows that 
\begin{equation}
\forall k<l,\
\forall {\cal C} \in {\rm PCCS}^k [\ ]^*,\ \forall A \subseteq Act\dcup\{0\},\ \ 
\garrow{{\cal C}[{E}]}{A}{}{} \mbox{iff \ } \garrow{{\cal C}[{F}]}{A}{}{}
\label{eqn-congr-A}
\end{equation}
As a consequence we may write $\garrow{S}{A}{}{}$ for $S \in Pr/{\cal R}$
when $\garrow{P}{A}{}{}$ for an arbitrary representative $P \in S$.
Now, if ${\cal C}[{E}]$ is not an action process,
$$\nu_S ({\cal C}[{E}],A) = \sum_{S\stackrel{A}{\longrightarrow}} \mu_S
({\cal C}[{E}],\,*,\,S)$$ 
\noindent
and therefore
\begin{equation}
\forall k<l,\
\forall {\cal C} \in {\rm PCCS}^k [\ ]^*,\ \forall A \subseteq Act\dcup\{0\},\ \ 
\nu_S ({\cal C}[{E}],A) = \nu_S ({\cal C}[{F}],A)
\label{eqn-nuS}
\end{equation}

The proof of (\ref{eqn-congr-strat}) for $k=l$ is split into two
cases. The case of an action transition $\alpha \in Act$ proceeds as
the congruence proof for $\Nequiv$, except that we check that the
induction hypothesis is applied to contexts in ${\rm PCCS}^l [\ ]$ only, and
in the case of summation we conclude with ${\rm LHS} = 0 = {\rm RHS}$.

The case of a probability transition $\alpha = *$ also follows the proof
for $\Nequiv$, defining $\mu_S^n$ similar to $\mu_R^n$, but with the
following modifications.
\begin{description}
\item[Action prefixing:] The proof of (\ref{eqn-congr-act}) (with $\beta = *$)
trivializes as $\mu^{n+1} (\alpha\,.\,{\cal C}[{E}],\,*,\,S) = 0$.
\item[Summation:] The proof of (\ref{eqn-congr-sum}) is replaced by
$$\mu^{n+1} (\sum_{i\in I} \lbrack p_i\rbrack\, {\cal C}_i [{E}],\,*,\,S)
= \sum_{i\in I} \multisetl p_i \mid {\cal C}_i [{E}] \in S \multisetr
= \sum_{i\in I} \multisetl p_i \mid {\cal C}_i [{F}] \in S \multisetr
= \mu(\sum_{i\in I} \lbrack p_i\rbrack\, {\cal C}_i [{F}],\,*,\,S)$$
since, for $i \in I$, ${\cal C}_i [{E}]$ and ${\cal C}_i [{F}]$
are in the same equivalence class $S'\in Pr/{\cal R}$.
\item[Product:] The proof of (\ref{eqn-congr-prod}) (with $\gamma = *$)
is unchanged until ``Moreover''. Then we have to show that for all
${\cal C}_i  \in {\rm PCCS}^l [\ ]^*$ and $S_i\in Pr/{\cal R}$
($i=1,2$),
\begin{equation}
\mu^{n+1} ({\cal C}_1 [{E}]\times {\cal C}_2
[{E}],\,*,\,S_1 \times S_2) \leq \mu ({\cal C}_1
[{F}]\times {\cal C}_2 [{F}],\,*,\,S_1 \times S_2)
\label{eqn-congr-prod-prob}
\end{equation}
For this we distinguish 4 cases, depending on whether or not ${\cal
C}_1 [{E}]$ and ${\cal C}_2 [{E}]$ are probability processes. If neither
of them are, (\ref{eqn-congr-prod-prob}) follows since LHS=0. 
If both of them are, we have
$$\mbox{LHS}=\mu^n ({\cal C}_1 [{E}],\,*,\,S_1)\cdot\mu^n ({\cal
C}_2 [{E}],\,*,\,S_2) \begin{array}[b]{c}
\mbox{\footnotesize induction}\\ \leq\end{array} \mu ({\cal C}_1
[{F}],\,*,\,S_1)\cdot\mu ({\cal C}_2 [{F}],\,*,\,S_2) =\mbox{RHS}$$
And if just one of them (say ${\cal C}_1 [{E}]$) is a probability
process, (\ref{eqn-congr-prod-prob}) follows since 
$$\mbox{LHS}=\mu^n ({\cal C}_1 [{E}],*,S_1)\cdot
\!\! \sum_{\beta\in Act}
\mu^n ({\cal C}_2 [{E}],\beta,S_2) \hspace{-7pt}\begin{array}[b]{c}
\mbox{\footnotesize induction}\\ \leq\end{array}\hspace{-7pt}
\mu ({\cal C}_1 [{F}],*,S_1)\cdot
\!\! \sum_{\beta\in Act} \mu ({\cal C}_2 [{F}],\beta,S_2) =\mbox{RHS}$$
\item[Restriction:] The proof of (\ref{eqn-congr-rstr}) is unchanged
until ``Moreover''. Then we have to show that for all
${\cal C}  \in {\rm PCCS}^l [\ ]^*$, $A \subseteq Act\cup \{0\}$ and $S'\in Pr/{\cal R}$,
\begin{equation}
\mu^{n+1} ({\cal C} [{E}]\rstr A,
\,*,\,S'\rstr A) \leq \mu ({\cal C} [{F}]\rstr A,\,*,\,S'\rstr A)
\label{eqn-congr-rstr-prob}
\end{equation}
Now the proof of (\ref{eqn-congr-rstr-prob}) proceeds with a case
distinction. In case $\garrow{S'}{A}{}{}$\hspace{-1.85em}/\hspace{1em} we
have LHS=0=RHS. In case $\garrow{S'}{A}{}{}$ it concludes as in
the generative case.
\item[Relabeling:] This case (with $\beta=*$) concludes with $$\mbox{LHS}
=\mu^n ({\cal C}[{E}],\,*,\,S') \begin{array}[b]{c} \mbox{\footnotesize
induction}\\ \leq\end{array} \mu ({\cal C} [{F}],\,*,\,S')= \mbox{RHS}
\makebox[0pt][l]{\ \ $\Box$}$$ 
\end{description}

\section{Interrelating the Models}

In this section we establish the results announced in the
introduction, showing that the models discussed before form a
hierarchy. We start with investigating the abstraction from the
generative to the reactive model in Section~\ref{sec-inter-GR},
followed by an analogous treatment of the more intricate
abstraction from the stratified to the generative model in
Section~\ref{sec-inter-SG}.  Subsequently, we give a direct
abstraction from the stratified to the reactive model in
Section~\ref{sec-inter-SR}. Finally, we briefly sketch the simpler
abstraction steps leading from probabilistic to nonprobabilistic
models.

\subsection{The Generative to Reactive Abstraction}
\label{sec-inter-GR}

Let $E,E'$ be PCCS expressions.  The {\em inter-model abstraction rule}
$\IMARGR$ is defined by
$$\garrow {E} {\alpha[p]} {E'} {i} \;\;\; \Longrightarrow \;\;\;
 \Rarrow {E} {\alpha[p/\nu_{G}(E, \{\alpha\})]} {E'} {i}$$
This rule uses the generative normalization function to convert generative
probabilities to reactive ones, thereby abstracting away from the relative
probabilities between different actions. We can now define $\phiGR(\phiG(P))$
as the reactive transition system that can be inferred from $P$'s generative
transition system via $\IMARGR$. By the same procedure as described at the end
of Section \ref{sec-nonprob-operational}, $\phiGR$ can be extended to a mapping
$\phiGR : \IG_G \rightarrow \IG_R$.

Write $P \stackrel{GR}{\sim} Q$ if $P,Q\in Pr$ are reactive bisimulation
equivalent with respect to the transitions derivable from $G+\IMARGR$, \ie the
theory obtained by adding $\IMARGR$ to the rules of Figure~\ref{fig-gos}.
The equivalence $\stackrel{GR}{\sim}$ is defined just like $\Requiv$ but
using the cPDF $\mu_{GR}$ instead of $\mu_R$.  $\mu_{GR}$ is defined by
$$\mu_{GR} (P, \alpha, S) = \sum_{i\in I_{R} (=I_G)} \multisetl \; p_{i} \mid
G+\IMARGR \vdash \rarrow{P}{\alpha [ p_{i} ]}{Q}{i} \mbox{ and } 
Q \in S \multisetr$$
%Note that $I_{GR}=I_G=I_R$.

\begin{theorem} {\bf(Abstraction)} \label{thm-abstrGR} 
Let $G,H\in \IG_G$.  Then $G\Gequiv H ~\Rightarrow~ \phiGR(G)\Requiv\phiGR(H)$.
\end{theorem} 
{\bf Proof:} We prove this theorem for the case that $G$ and $H$ are of the
form $\phiG(P)$ and $\phiG(Q)$ with $P,Q\in Pr$ and use that
$\phiG(P)\Gequiv\phiG(Q) \Leftrightarrow P\Gequiv Q$ and
$\phiGR(\phiG(P))\Requiv\phiGR(\phiG(Q))\Leftrightarrow P\stackrel{GR}{\sim}Q$.
The proof of the general case is not essentially different, but would involve
defining the reactive and generative bisimulation equivalences formally on
transition systems.

Let $\cal R$ be a generative bisimulation on $Pr$.
We prove that $\cal R$ is also a reactive bisimulation on $Pr$ with
respect to the transitions derivable from $G+\IMARGR$.
So let $(P,Q)\in {\cal R}$, $S\in Pr/{\cal R}$ and $\alpha\in Act$.
Then $$\nu_G (P,\{\alpha\}) = \sum_{S \in Pr/{\cal R}}\mu_G
(P,\,\alpha,\,S) = \sum_{S \in Pr/{\cal R}} \mu_G (Q,\,\alpha,\,S) =  
\nu_G (P,\{\alpha\}), ~~\mbox{so}$$ 
$$\mu_{GR} (P,\alpha,S) = \frac{\mu_G (P,\alpha,S)}{\nu_G (P,\{\alpha\})} =
\frac{\mu_G (Q,\alpha,S)}{\nu_G (Q,\{\alpha\})} = \mu_{GR}(Q,\alpha,S)~~~\Box$$
\vspace{1ex}
        
We will now investigate to what extent $\phiGR$ commutes with the
semantic mappings $\phiG$ and $\phiR$.\linebreak[3] This\sht\sht\ turns out
to be the case for $\PCCSR$ processes in which all summations are of the
form $\rsigma$\sht\sht. We say that such an expression is {\em
summation-guarded}.

\begin{lemma} {\bf(Soundness and Completeness of $\IMARGR$)}
For $E,E'$ summation-guarded $\PCCSR\!$ expressions, $\alpha\in Act$, $p \in
(0,1]$ and $i \in I_R$, $$R \vdash \rarrow{E}{\alpha[p]}{E'}{i} \
\Longleftrightarrow \ G+\IMARGR \vdash \rarrow{E}{\alpha[p]}{E'}{i}$$\sht
\label{imarGR}
\end{lemma}
{\bf Proof:} As in the congruence proofs, we use induction on the depth
of derivation trees, and write $R \vdash_n \rarrow{E}{\alpha[p]}{E'}{i}$ if
the transition $\rarrow{E}{\alpha[p]}{E'}{i}$ can be derived by a proof-tree of
depth $n$. In the similar definition of $G+\IMARGR \vdash_n$ we don't count the
single application of $\IMARGR$ though. We distinguish several cases, depending
on the topmost operator of $E$. The case of action prefixing is trivial.
\sht\sht
\begin{description}
\item[Guarded summation:]
$R \vdash_{2} \Rarrow{\rsigma}{\alpha_j [q]}{E_j}{j}$\\
iff $~j\in I~$ and \raisebox{1pt}[0pt][0pt]{\parbox{9cm}{\[q~=~p_j
\raisebox{-4pt}[0pt][0pt]{\huge /}\!\!\!\! 
\sum_{k\in I,~\alpha_k = \alpha_j}\!\!\!\! p_k ~=~ p_j
\raisebox{-4pt}[0pt][0pt]{\huge /}\nu_G (\rsigma, \{\alpha_j\})\]}}\\
iff $~G+\IMARGR \vdash_{2} \Rarrow{\rsigma}{\alpha_j [q]}{E_j}{j}$.\sht
\item[Product:]
$R \vdash_{n+1} \Rarrow{E\times F}{(\alpha,\beta)[r]}{E'\times F'}{(i,j)}$\\
iff $~R \vdash_{n} \Rarrow{E}{\alpha[p]}{E'}{i},~~
\Rarrow{F}{\beta[q]}{F'}{j}~$ and $~p\cdot q = r$\\
iff $~G+\IMARGR \vdash_{n} \Rarrow{E}{\alpha[p]}{E'}{i},~~
\Rarrow{F}{\beta[q]}{F'}{j}~$ and $~p\cdot q = r~$ (by induction)\\
iff $~G \vdash_{n} \Garrow{E}{\alpha[p\cdot \nu_G
(E,\{\alpha\})]}{E'}{\!\!\!\!\!\!\!\!i},~~ 
\Garrow{F}{\beta[q\cdot \nu_G
(F,\{\beta\})]}{F'}{\!\!\!\!\!\!\!\!j}~$ and $~p\cdot q = r$\\ 
iff $~G \vdash_{\!\!n+1} \Garrow{E\!\times\! F}{(\alpha,\beta)[r\cdot s]}{\!\!E'\!\times\!
F'}{(i,j)}$ and $s=\nu_G (E,\{\alpha\})\cdot\nu_G (F,\{\beta\})=
\nu_G (E\!\times\! F,\{(\alpha,\beta)\})\!\!\!\!\!$\\iff
$~G+\IMARGR\vdash_{n+1}\Rarrow{E\times F}{(\alpha,\beta)[r]}{E'\times F'}{(i,j)}$.
\item[Restriction:]
$R \vdash_{n+1} \Rarrow{E\rstr A}{\alpha[p]}{E'\rstr A}{i}$\\
iff $~R \vdash_{n} \Rarrow{E}{\alpha[p]}{E'}{i}~$ and $~\alpha\in A$\\
iff $~G+\IMARGR \vdash_{n} \Rarrow{E}{\alpha[p]}{E'}{i}~$ and
$~\alpha\in A~$ (by induction)\\
iff $~G \vdash_{n} \Garrow{E}{\alpha[p\cdot \nu_G
(E,\{\alpha\})]}{E'}{\!\!\!\!\!\!\!\!i}~$ and $~\alpha\in A$\\
iff $~G \vdash_{n+1} \Garrow{E\rstr A}{\alpha[p\cdot r]}{E'\rstr A}{i}~$
where $~r=\frac{\nu_G (E,\{\alpha\})}{\nu_G (E,A)}= 
\nu_G (E\rstr A,\{\alpha\})$\\
iff $~G+\IMARGR\vdash_{n+1}\Rarrow{E\rstr A}{\alpha[p]}{E'\rstr A}{i}$.
\item[Recursion:]
$R \vdash_{n+1} \Rarrow{\fix_X E}{\alpha[p]}{E'}{i}$\\
iff $~R \vdash_{n} \Rarrow{E\{\fix_X E/X\}}{\alpha[p]}{E'}{i}$\\
iff $~G+\IMARGR \vdash_{n} \Rarrow{E\{\fix_X E/X\}}{\alpha[p]}{E'}{i}~$
(by induction)\\ 
iff $~G \vdash_{\!\!n} \Garrow{E\{\fix_X E/X\}}{\alpha[p\cdot r]}{\!\!E'}{i}~$
where $~r=\nu_G(E\{\fix_X E/X\},\{\alpha\})= \nu_G (\fix_X E,\{\alpha\})$\\ 
iff $~G \vdash_{\!\!n+1\,} \Garrow{\fix_X E\!\!\!\!}{\alpha[p\cdot \nu_G
(\fix_X E,\{\alpha\})]}{E'}{\!\!\!\!\!\!\!\!\!\!\!\!i}$\\
iff $~G+\IMARGR\vdash_{n+1}\Rarrow{\fix_X E}{\alpha[p]}{E'}{i}$.
\qed
\end{description}
As an immediate consequence of Lemma~\ref{imarGR} we have:

\begin{theorem} {\bf(Commutativity)} \label{thm-comGR}
Let $P\!\in\! \PrR$ be summation-guarded. Then $\phiGR(\phiG(P))\!=\!\phiR(P)$.
\end{theorem} 

\begin{corollary} Let $P,Q\in\PrR$ be summation-guarded. Then $P\Gequiv Q
\Rightarrow P\Requiv Q$.
\label{cor-GR}
\end{corollary}
{\bf Proof:} Theorem \ref{thm-abstrGR} says that $P\Gequiv Q \Rightarrow
P\stackrel{GR}{\sim} Q$ for $P,Q\in Pr$. Theorem \ref{thm-comGR} (or Lemma
\ref{imarGR}) implies $\mu_{R} (P, \alpha, S) = \mu_{GR} (P, \alpha, S)$ and
hence $P\Requiv Q \Leftrightarrow P\stackrel{GR}{\sim} Q$ for
summation-guarded $P,Q\in \PrR$.\qed

Theorem \ref{thm-comGR} does not hold in the presence of general summation.
Consider the process
$$\textstyle P = \frac{1}{3}a\,.\,X + \frac{2}{3}(\frac{1}{2}a\,.\,Y + 
        \frac{1}{2}b\,.\,Z)$$
In $\phiGR(\phiG(P))$ the probabilities of $a.X$ and $a.Y$ are equal,
while in $\phiR(P)$ executing $a.Y$ is twice as likely as $a.X$.
This counterexample can be easily extended so to apply to Corollary
\ref{cor-GR} as well.
One may wonder whether relabeling could be added to, or summation redefined on
the reactive model such that reactive bisimulation remains a congruence, but
Theorem \ref{thm-comGR} can be extended. This is not possible as it would
imply that $\stackrel{GR}{\sim}$ is a congruence, which will be refuted
below.

The equivalence $\stackrel{GR}{\sim}$ (which was previously defined only on
closed PCCS expressions) can be extended to arbitrary generative labeled
transition systems by $G\stackrel{GR}{\sim}H \Leftrightarrow
\phiGR(G)\stackrel{R}{\sim} \phiGR(H)$, and $P\stackrel{GR}{\sim}Q
\Leftrightarrow \phiG(P)\stackrel{GR}{\sim}\phiG(Q)$. 
We show that this equivalence is not a congruence, thus demonstrating the need
for refining the bisimulation semantics when moving from the reactive to the
generative model.  Consider the PCCS processes
\sht
\begin{center}
$P = \frac{1}{3}a\,.\,\zero + \frac{2}{3}b\,.\,c\,.\,\zero \hspace{1.5in}
Q = \frac{1}{2}a\,.\,\zero + \frac{1}{2}b\,.\,c\,.\,\zero$
\sht
\end{center}
For $P$,$Q$ we have $P\stackrel{GR}{\sim}Q$, \ie
$$\phiGR(\phiG(P)) \Requiv \phiGR(\phiG(Q))$$
However, the same is not true for ${\cal C}[P]$ and ${\cal C}[Q]$, where
${\cal C}$ is the relabeling $[a \rightarrow a, b \rightarrow a, c \rightarrow
c]$.  In particular, 
$\mu_{GR}({\cal C}[P], a, [c\,.\,\zero]_{\Requiv}) = \frac{2}{3}$
and
$\mu_{GR}({\cal C}[Q], a, [c\,.\,\zero]_{\Requiv}) = \frac{1}{2}$.

A similar counterexample is obtained by placing $P$ and $Q$ in the
summation context ${\cal C} = \frac{1}{2} [\ ] + \frac{1}{2}
b\,.\,\zero$. In this case
$\mu_{GR}({\cal C}[P], b, [c\,.\,\zero]_{\Requiv}) = \frac{2}{5}$
and
$\mu_{GR}({\cal C}[Q], b, [c\,.\,\zero]_{\Requiv}) = \frac{2}{3}$.

\subsection{The Stratified to Generative Abstraction}
\label{sec-inter-SG}

Let $E,E'$ be PCCS expressions.  Then $\IMARSG$ 
is given by
$$\garrow{E}{\alpha}{E'}{\!}\;\;\Longrightarrow\;\;\garrow{E}{\alpha[1]}{E'}{0}$$
$$\sarrow{E}{p}{E'}{i}\garrow{\!}{\alpha[q]}{E''}{j}\;\;
\Longrightarrow \;\; \Garrow{E}{\alpha[p\cdot q]}{E''}{i.j}$$
where $i.j$ (as in the generative case) denotes the concatenation of two
indices.  Thus the elements of $I_{SG}$, the set of indices generated by
$S+\IMARSG$, are sequences, and we let $|i|$ denote the length of such a
sequence.

Write $P \stackrel{SG}{\sim} Q$ if $P,Q\in Pr$ are generative bisimulation
equivalent with respect to the transitions derivable from $G+\IMARSG$.
The equivalence $\stackrel{SG}{\sim}$ is defined just like $\Gequiv$, but
using the cPDF $\mu_{SG}$ instead of $\mu_G$.  $\mu_{SG}$ is defined by
$$\mu_{SG} (P, \alpha, S) = \sum_{i\in I_{SG}} \multisetl \; p_{i} \mid
G+\IMARSG \vdash \garrow{P}{\alpha [ p_{i} ]}{Q}{i} \mbox{ and } 
Q \in S \multisetr$$

\begin{theorem} {\bf(Abstraction)} \label{thm-abstrSG}
Let $G,H\in \IG_S$.  Then $G\Sequiv H ~\Rightarrow~ \phiSG(G)\Gequiv\phiSG(H)$.
\end{theorem} 
{\bf Proof:} As before, we prove this theorem for the case that $G$ and $H$
are of the form $\phiS(P)$ and $\phiS(Q)$. Thus we show that for $P,Q\in
Pr$, $P\Sequiv Q ~\Rightarrow~ P\stackrel{SG}{\sim}Q$.

We now define
\[ \mu_{SG}^n (P, \alpha, S) = \sum_{i\in I_{SG}}
\multisetl \; p_{i} \mid S+\IMARSG \vdash \garrow{P}{\alpha [ p_{i} ]}{Q}{i},~
Q \in S \mbox{ and } |i|=n \multisetr \] 
Let $\cal R$ be a stratified bisimulation on $Pr$.  We prove that $\cal R$ is
also a generative bisimulation on $Pr$ with respect to the transitions
derivable from $S+\IMARSG$, \ie that for $(P,Q)\in {\cal R}$, $S\in Pr/{\cal
R}$ and $\alpha\in Act$, $$\mu_{SG} (P,\alpha,S) = \mu_{SG} (Q,\alpha,S)$$
As $\mu_{SG} (P, \alpha, S) = \sum_{n\in \mbox{\scriptsize \rm
I\hspace{-0.55mm}N}} \mu_{SG}^n (P, \alpha, S)$, it suffices to prove this for
every $\mu_{SG}^n$, which we will do by induction on $n$.
$$\mu_{SG}^1 (P,\alpha,S) = \mu_{S} (P,\alpha,S) = \mu_{S} (Q,\alpha,S) =
\mu_{SG}^1 (Q,\alpha,S)$$\sht\sht\sht

$$\mu_{SG}^{n+1}(P, \alpha, S) = \sum_{i\in I_{S}, j\in I_{SG}} \multisetl \;
p_{i}\cdot q_j \mid S+\IMARSG\vdash\sarrow{P}{p_i}{R}{i}\garrow{\!}
{q_j}{Q}{j},~R \in Pr,~Q \in S \mbox{ and } |j|=n \multisetr$$\sht
$$=  \sum_{R\in Pr} \mu_S (P,*,\{R\})\cdot\mu_{SG}^n (R,\alpha,S)$$
$$=\!\! \sum_{[R]_{\cal R} \in Pr/{\cal R}}\!\!
\mu_{S} (P,*,[R]_{\cal R})\cdot\mu_{SG}^n (R^{\raisebox{5pt}[0pt][0pt]
{\makebox[0pt][l]{$\swarrow^{\raisebox{3pt}{\small independent of choice of
$R\in [R]_{\cal R}$}}$}}},\alpha,S)$$
$$=\!\! \sum_{[R]_{\cal R} \in Pr/{\cal R}}\!\!
\mu_{S}(Q,*,[R]_{\cal R})\cdot\mu_{SG}^n (R,\alpha,S) = 
\mu_{SG}^{n+1} (Q,\alpha,S)~~~\Box$$\sht

$\IMARSG$ has the effect of ``flattening'' trees of probability transitions
with action transitions at the leaves, into a single-level structure of
generative transitions. Indeed, we show that the generative transition system
of a restriction-free PCCS process $P$ is isomorphic to the generative
transition system that can be inferred from $P$'s stratified transition system
via $\IMARSG$. For example, let $P =
\frac{1}{3}a\,.\,\zero + \frac{2}{3}(\frac{1}{2}b\,.\,\zero + 
\frac{1}{2}c\,.\,\zero)$.  Then, by $\IMARSG$
\sht
\begin{center}
$\garrow{P}{a [ \frac{1}{3}]}{\zero}{1.0} \;\;\;\;\;\;\;\; \garrow{P}{b [
\frac{1}{3}]}{\zero}{2.1.0} \;\;\;\;\;\;\;\; 
\garrow{P}{c[\frac{1}{3}]}{\zero}{2.2.0}$  
\sht
\end{center}
Except for the transition indices, these are precisely the
transitions of $P$ in the generative model.

\begin{lemma} {\bf(Soundness and Completeness of $\IMARSG$)}
There is a surjection $f: I_G \rightarrow I_{SG}$ such that for
$E,E'$ restriction-free PCCS expressions, $\alpha\in Act$, $p \in
(0,1]$ and $i \in I_G$, 
$$G \vdash \garrow{E}{\alpha[p]}{E'}{i} \ \Longleftrightarrow \ 
S+\IMARSG \vdash \garrow{E}{\alpha[p]}{E'}{f(i)}$$
Moreover $G \vdash \garrow{E}{\alpha[p]}{E'}{i},~~\garrow{E}{\beta[q]}{E''}{j},
~~i\neq j\ \Longrightarrow \ f(i)\neq f(j)$.
\label{imarSG}
\end{lemma}
{\bf Proof:} In Lemma \ref{imarGR} $f$ happened to be the identity function and
was therefore not mentioned. Unfortunately, $f$ can not be chosen bijective
this time. In order to get rid of this complication in an early stage, we split
the proof in two parts by considering an intermediate operational semantics
$G'$. The inference rules of $G'$ are exactly the same as the ones of $G$,
except that in the rule for product when $i$ and $j$ are both $0$ the resulting
index is also $0$ instead of $(0,0)$. Let $f': I_G \rightarrow I_{G'}$ be the
function that exhaustively replaces all occurrences of $(0,0)$ in an index by
$0$. Then
$$G \vdash \garrow{E}{\alpha[p]}{E'}{i} \ \Longleftrightarrow \ G' \vdash
\garrow{E}{\alpha[p]}{E'}{f'(i)}$$ Now let $G \vdash
\garrow{E}{\alpha[p]}{E'}{i},~~\garrow{E}{\beta[q]}{E''}{j}$ and $f'(i)=f'(j)$.
If $E$ is summation-free, it has only one outgoing transition and therefore
$i=j$. Otherwise $i=j$ is established by a straightforward induction on the
length of derivations.
We refer to this property of $f'$ as ``limited injectivity''
since $f'$ is injective only with respect to the transition indices of a given
$E$. 

The second part of the proof consist of establishing Lemma \ref{imarSG} with
$G'$ instead of $G$ and \mbox{$f: I_{G'}\rightarrow I_{SG}$}. This function
can be chosen bijective.

Recall that $I_S^0 = I_S \cup\{0\}$ and let $I_{SG}^0$ be the largest set of
sequences over $I_S^0$ such that an index $(i,j)$ can only be followed by
either $0$ or an index $(k,l)$ such that $i.k, j.l \in I_{SG}^0$, and an index
$0$ can only be followed by an index $0$.  Then $I_{SG} = I_{SG}^0 \cap (I_S)^*
0$. This follows from the fact that product is a static operator, \ie the
syntactic subtree of occurrences of product in a PCCS expression is preserved
under stratified derivations.
Define $head: I_{G'} \rightarrow I_S^0$, $~tail: I_{G'}
\rightarrow I_{G'}$ and the partial function $\bullet: I_S^0 \times I_{G'}
\rightarrow I_{G'}$ by
$$\begin{array}{@{}lll@{}}
head(0)=0                   &tail(0)=0     &0\bullet 0=0\\
head(i.j)=i                 &tail(i.j)=j   &i\bullet j=i.j  \hfill (i\in I_0)\\
head(i,j)\!=\!(head(i),head(j)) &tail(i,j)=\left\{ {\arraycolsep 0pt
\begin{array}{@{}ll@{}} (tail(i),tail(j)) & \mbox{~if}\neq (0,0)\\0 &
\mbox{~otherwise}\end{array}}\right. 
&\begin{array}{@{}l@{}}(i,j)\bullet (k,l)=(i\bullet k,j\bullet l)\\
(i,j)\bullet 0 = (i\bullet 0,j\bullet 0)\end{array}
\end{array}$$
With structural induction on $j$ for ``$\Rightarrow$'' and on $i$ for
``$\Leftarrow$'' it follows that
\begin{equation}
i=j\bullet k ~~\Leftrightarrow~~ j=head(i)\wedge k=tail(i)
\label{uniquely}
\end{equation}
Moreover, if $i\neq 0$, $head(i)\in I_S$ and $tail(i)$ is a shorter index than
$i$. Define $f:I_{G'}\rightarrow I_{SG}$ by
$$f(i)= \left\{ \begin{array}{ll} 0 & \mbox{if~} i=0 \\ head(i)\,.\,f(tail(i))
& \mbox{otherwise} \end{array} \right. $$
and $g:I_{SG}\rightarrow I_{G'}$ by
$$g(i_0. \cdots .i_n)=(i_0 \bullet ( \cdots (i_{n-1} \bullet i_n) \cdots ))$$
Note that $f$ transforms pairs of sequences into sequences of pairs.
Clearly $f(i)\in I_{SG}$ for $i\in I_{G'}$ and $g(i)\in I_{G'}$ for $i\in
I_{SG}$. Further $g$ is the inverse of $f$ by (\ref{uniquely}), and hence $f$
is bijective. The bijectivity\linebreak[2] of $f$ together with the limited injectivity of
$f'$ establishes the ``moreover'' part of the lemma.

We now proceed to prove
$$G' \vdash \garrow{E}{\alpha[p]}{E'}{i} \ \Longleftrightarrow \ 
S+\IMARSG \vdash \garrow{E}{\alpha[p]}{E'}{f(i)}$$
by structural induction on $i$. In case $i=0$ (the induction base) $E$ must
be summation-free and there is almost no difference between the generative and
stratified (=nonprobabilistic) inference rules, and the statement holds.
In case $i\neq 0$ we again use induction on the depth of derivation trees,
albeit modified ones. Here the modification of a $G'$ derivation tree consists
of removing all
ancestors of transitions from summation expressions, and the modification of an
$S+\IMARSG$ derivation tree consists of erasing any subtree ending with a
clause that is used as the second argument in an application of $\IMARSG$.
Moreover, the remaining application of $\IMARSG$ doesn't count. We now use the
notation $\vdash_n$ to refer to the depth of modified derivations, and prove
$$G' \vdash_n \garrow{E}{\alpha[p]}{E'}{i} \ \Longleftrightarrow \ 
S+\IMARSG \vdash_n \garrow{E}{\alpha[p]}{E'}{f(i)}$$ by induction on $n$.
We distinguish several cases, depending on the topmost operator of $E$.
As $i\neq 0$ this operator cannot be action prefixing.\sht
\begin{description}
\item[Summation:]
$G' \vdash_{1} \Garrow{\gsigma}{\alpha[p]}{E'}{j.k}~~$
iff $~~G' \vdash \Garrow{E_j}{\alpha[q]}{E'}{k}~$ and $~p=p_j\cdot q$\sht\sht\\
iff $~S+\IMARSG \vdash \Garrow{E_j}{\alpha[q]}{E'}{f(k)}~$ and $~p=p_j\cdot q~$
(by induction ($k<j.k$))\sht\\
iff $~S+\IMARSG \vdash_{1} \Garrow{\gsigma}{\alpha[p]}{E'}{f(j.k)}~$
(since $~S \vdash_{1} \Sarrow{\gsigma}{p_j}{E_j}{j}$).\sht
\item[Product:] In case $i\neq 0\neq j$:
$G' \vdash_{n+1} \Garrow{E\times F}{(\alpha,\beta)[r]}{E''\times F''}{(i,j)}$\\
iff $~G' \vdash_{n} \Garrow{E}{\alpha[p]}{E''}{i},~~
    \Garrow{F}{\beta[q]}{F''}{j}~$ and $~p\cdot q = r$\\
iff $~S+\IMARSG \vdash_{n} \Garrow{E}{\alpha[p]}{E''}{f(i)},~~
    \Garrow{F}{\beta[q]}{F''}{f(j)}~$ and $~p\cdot q =r~$ (by induction)\\[1ex]
iff $~S\vdash_{n}\Sarrow{E}{p_1}{E'}{head(i)},~~\Sarrow{F}{q_1}{F'}{head(j)}
    $,\\ \hspace*{1.2em}
    $S+\IMARSG \vdash \garrow{E'}{\alpha[p_2]}{E''}{f(tail(i))},~~ 
    \garrow{F'}{\beta[q_2]}{F''}{f(tail(j))}~$ and
    $~p_1\cdot p_2\cdot q_1\cdot q_2 =r$\\[1ex]
iff $~S\vdash_{n}\Sarrow{E}{p_1}{E'}{head(i)},~~\Sarrow{F}{q_1}{F'}{head(j)}
    $,\\ \hspace*{1.2em}
    $G' \vdash \garrow{E'}{\alpha[p_2]}{E''}{tail(i)},~~
    \garrow{F'}{\beta[q_2]}{F''}{tail(j)}~$ and
    $~p_1\cdot p_2\cdot q_1\cdot q_2 =r~$ (by induction)\\[1ex]
iff $~S \vdash_{n+1} \Sarrow{E\times F}{r_1}{E'\times F'}{(head(i),head(j))}$,
    \\ \hspace*{1.2em}
    $G' \vdash \Garrow{E'\times F'}{(\alpha,\beta)[r_2]}{E''\times F''}
    {tail(i,j)}~$ and $~r_1\cdot r_2 =r$\\
iff $~S \vdash_{n+1} \Sarrow{E\times F}{r_1}{E'\times F'}{head(i,j)}$,
    \\ \hspace*{1.2em}
    $S+\IMARSG \vdash\Garrow{E'\times F'}{(\alpha,\beta)[r_2]}
    {E''\times F''}{f(tail(i,j))}~$ and $~r_1\cdot r_2 =r~$ (by induction)\\
iff $~S+\IMARSG\vdash_{n+1}\Garrow{E\times F}{(\alpha,\beta)[r]}
    {E''\times F''}{f(i,j)}$. 
\item
\rm In case $i\neq 0 = j$:
$G' \vdash_{n+1} \Garrow{E\times F}{(\alpha,\beta)[r]}{E''\times F''}{(i,0)}$\\
iff $~G' \vdash_{n} \Garrow{E}{\alpha[r]}{E''}{i},~~
    \Garrow{F}{\beta[1]}{F''}{0}$\\
iff $~S+\IMARSG \vdash_{n} \Garrow{E}{\alpha[r]}{E''}{f(i)},~~
    \Garrow{F}{\beta[1]}{F''}{0}~$ (by induction)\\[1ex]
iff $~S \vdash_{n}\Sarrow{E}{r_1}{E'}{head(i)},~~\Garrow{F}{\beta}{F''}{}$,
    \\ \hspace*{1.2em}
    $S+\IMARSG \vdash \Garrow{E'}{\alpha[r_2]}{E''}{f(tail(i))},~~ 
    \Garrow{F}{\beta[1]}{F''}{0}~$ and $~r_1\cdot r_2 =r$\\[1ex]
iff $~S \vdash_{n}\Sarrow{E}{r_1}{E'}{head(i)},~~\Garrow{F}{\beta}{F''}{}$,
    \\ \hspace*{1.2em}
    $G' \vdash \Garrow{E'}{\alpha[r_2]}{E''}{tail(i)},~~
    \Garrow{F}{\beta[1]}{F''}{0}~$ and $~r_1\cdot r_2=r~$ (by induction)\\[1ex]
iff $~S \vdash_{n+1} \Sarrow{E\times F}{r_1}{E'\times F}{(head(i),0)}$,
    \\ \hspace*{1.2em}
    $G' \vdash \Garrow{E'\times F}{(\alpha,\beta)[r_2]}{E''\times F''}
    {tail(i,0)}~$ and $~r_1\cdot r_2 =r$\\
iff $~S \vdash_{n+1} \Sarrow{E\times F}{r_1}{E'\times F}{head(i,0)}$,
    \\ \hspace*{1.2em}
    $S+\IMARSG \vdash\Garrow{E'\times F}{(\alpha,\beta)[r_2]}
    {E''\times F''}{f(tail(i,0))}~$ and $~r_1\cdot r_2 =r~$ (by induction)\\
iff $~S+\IMARSG\vdash_{n+1}\Garrow{E\times F}{(\alpha,\beta)[r]}
    {E''\times F''}{f(i,0)}$. 
\item
The case $i=0\neq j$ is symmetric.
\item[Relabeling:]
$G' \vdash_{n+1} \Garrow{E[f]}{\alpha[p]}{E''[f]}{i}$\\
iff $~G' \vdash_{n} \Garrow{E}{\beta[p]}{E''}{i}~$ and $~f(\beta)=\alpha$\\
iff $~S+\IMARSG \vdash_{n} \Garrow{E}{\beta[p]}{E''}{f(i)}~$ and
    $~f(\beta)=\alpha~$ (by induction)\\ 
iff $~S \vdash_{n} \sarrow{E}{p_1}{\!E'}{head(i)}$,
    $~S+\IMARSG \vdash\garrow{E'\!\!}{\beta[p_2]}{\!\!E''}{f(tail(i))}$,
    $~p_1\cdot p_2 = p~$ and $~f(\beta)=\alpha$\\
iff $~S \vdash_{n} \sarrow{E}{p_1}{\!E'}{head(i)}$,
    $~G' \vdash \garrow{E'\!\!}{\beta[p_2]}{\!\!E''}{tail(i)}$,
    $~p_1\cdot p_2 = p~$ and $~f(\beta)=\alpha~$ (by induction)\\
iff $~S \vdash_{n+1} \sarrow{E[f]\!\!}{p_1}{\!\!\!E'[f]}{head(i)}$,
    $~G' \vdash \garrow{E'[f]\!\!}{\alpha[p_2]}{\!\!\!E''[f]}{tail(i)}$,
    $~p_1\cdot p_2 = p$\\
iff $~S \vdash_{n+1} \sarrow{E[f]\!\!}{p_1}{\!\!\!E'[f]}{head(i)}$,
    $~S+\IMARSG \vdash \garrow{E'[f]\!\!}{\alpha[p_2]}{\!\!\!E''[f]}
    {f(tail(i))}$, $~p_1\cdot p_2 = p~$ (ind.)\\
iff $~S+\IMARSG \vdash_{n+1} \Garrow{E[f]}{\alpha[p]}{E''[f]}{f(i)}$.
\item[Recursion:]
$G' \vdash_{n+1} \Garrow{\fix_X E}{\alpha[p]}{E''}{i}$\\
iff $~G' \vdash_{n} \Garrow{E\{\fix_X E/X\}}{\alpha[p]}{E''}{i}$\\
iff $~S+\IMARSG \vdash_{n} \Garrow{E\{\fix_X E/X\}}{\alpha[p]}{E''}{f(i)}~$
(by induction)\\ 
iff $~S \vdash_{n} \sarrow{E\{\fix_X E/X\}}{p_1}{E'}{head(i)},
    ~~S+\IMARSG \vdash \Garrow{E'}{\alpha[p_2]}{E''}{f(tail(i))}~$ and 
    $~p_1 \cdot p_2 = p$\\
iff $~S \vdash_{n+1} \sarrow{\fix_X E}{p_1}{E'}{head(i)},
    ~~S+\IMARSG \vdash \Garrow{E'}{\alpha[p_2]}{E''}{f(tail(i))}~$ and 
    $~p_1 \cdot p_2 = p$\\
iff $~S+\IMARSG \vdash_{n+1} \Garrow{\fix_X E}{\alpha[p]}{E''}{f(i)}$.
\qed
\end{description}
As an immediate consequence of this lemma, we obtain the following commutativity result:

\vspace{1.5ex}
\begin{theorem} {\bf(Commutativity)}
Let $P \in Pr$ be restriction-free.  Then 
$ \phiSG(\phiS(P)) \; = \; \phiG(P) $.
\label{thm-comSG}
\end{theorem} 

\begin{corollary} Let $P,Q\in Pr$ be restriction-free PCCS processes.
Then $P\Sequiv Q \Rightarrow P\Gequiv Q$.
\label{cor-SG}\end{corollary}
{\bf Proof:} Theorem \ref{thm-abstrSG} says that $P\Sequiv Q \Rightarrow
P\stackrel{SG}{\sim} Q$ for $P,Q\in Pr$. Theorem \ref{thm-comSG} (or Lemma
\ref{imarSG}) implies $\mu_{G} (P, \alpha, S) = \mu_{SG} (P, \alpha, S)$ and
hence $P\Gequiv Q \Leftrightarrow P\stackrel{SG}{\sim} Q$ for
restriction-free $P,Q\in Pr$.\qed

Theorem~\ref{thm-comSG} does not hold for arbitrary PCCS processes.
Consider the process 
\sht
\begin{center}
$P = \frac{1}{3}a\,.\,\zero + \frac{2}{3}(\frac{1}{2}b\,.\,\zero + 
        \frac{1}{2}c\,.\,\zero)\rstr\{ a,b \}$
\sht
\end{center}
$\phiG(P)$ is equal to $\frac{1}{2}a\,.\,\zero + \frac{1}{2}b\,.\,\zero$
while $\phiSG(\phiS(P))$ is equal to 
$\frac{1}{3}a\,.\,\zero + \frac{2}{3}b\,.\,\zero$.\\
This counterexample can be easily extended so to apply to Corollary
\ref{cor-SG} as well.

However, Theorem~\ref{thm-comSG} and Corollary~\ref{cor-SG} do hold for
summation-guarded PCCS processes with restriction. The reason is that for
those processes there is hardly any difference between the generative and
stratified models. It suffices to extend Lemma~\ref{imarSG} to this case.

\pagebreak[3]
\begin{lemma} Lemma~\ref{imarSG} also holds for summation-guarded PCCS
expressions.
\label{imarSGR}\end{lemma}
{\bf Proof:} It suffices to add the case for restriction to the proof of
Lemma~\ref{imarSG}. Check that the remark concerning the induction base still
holds. For the induction
step we use that in the stratified model, if $E$ is summation-guarded and
$\sarrow{E}{p}{E'}{i}$, then $E'$ is an action process. This can be inferred by
a straightforward induction on stratified derivations. It follows that
$\nu_G(E,A) = \nu_S(E,A)$.\sht
\begin{description}
\item[Restriction:]
$G' \vdash_{n+1} \Garrow{E\rstr A}{\alpha[p]}{E''\rstr A}{i}$\\
iff $~G' \vdash_{n} \Garrow{E}{\alpha[p\cdot\nu_G(E,A)]}{E''}{\!\!\!i}~$ and
$~\alpha\in A$\\
iff $~S+\IMARSG \vdash_{n} \Garrow{E}{\alpha[p\cdot\nu_G(E,A)]}{E''}
{\!\!\!f(i)}~$ and $~\alpha\in A~$ (by induction)\\
iff $~S \vdash_{n} \Sarrow{E}{p\cdot\nu_S(E,A)}{E'}{head(i)},~~f(tail(i))=0,
    ~~S \vdash \garrow{E'}{\alpha}{E''}{\!}~$ and $~\alpha\in A$\\
iff $~S \vdash_{n+1} \sarrow{E\rstr A}{p}{E'\rstr A}{head(i)},
    ~~S+\IMARSG \vdash \garrow{E'}{\alpha[1]}{E''}{f(tail(i))}~$ and
$~\alpha\in A$\\
iff $~S+\IMARSG \vdash_{n+1} \Garrow{E\rstr A}{\alpha[p]}{E''\rstr A}{f(i)}$.
\qed
\end{description}

Finally, we show that the equivalence induced on the stratified model by
generative bisimulation is not a congruence for restriction.  Consider
processes $Sc$ and 
$Sc'$ of Section~\ref{sec-intro} (the scheduler specifications). We have
$\varphi_{SG}(\phiS(Sc)) \Gequiv \varphi_{SG}(\phiS(Sc'))$
but, as discussed in Section~\ref{sec-intro}, 
$\varphi_{SG}(\phiS(Sc\rstr \{ a, b \})) 
\not\Gequiv \varphi_{SG}(\phiS(Sc'\rstr \{ a, b \}))$.

\subsection{The Stratified to Reactive Abstraction}
\label{sec-inter-SR}

Let $E,E'$ be PCCS expressions.  Then $\IMARSR$ is given by $$\garrow{E}
{\alpha}{E'}{\!\!}\;\;\Longrightarrow\;\;\rarrow{E}{\alpha[1]}{E'}{0}$$ 
$$\sarrow{E}{p}{E'}{i}\rarrow{\!}{\alpha[q]}{E''}{j}\;\;\Longrightarrow \;\;
\Rarrow{E}{\alpha[\frac{p\cdot q}{\nu_S (E,\{\alpha\})}]}{E''}{i.j}$$

This inter-model abstraction rule defines a mapping $\phiSR: \IG_S \rightarrow
\IG_R$. Like the composed mapping $\phiGR \circ \phiSG: \IG_S \rightarrow
\IG_R$, $\phiSR$ flattens trees of probability transitions with action
transitions at the leaves into a single-level structure, and normalizes the
probabilities to yield a reactive transition system. However, whereas $\phiGR
\circ \phiSG$ first flattens and then normalizes, $\phiSR$ performs these
operations interactively. From the proof of Lemma~\ref{imarSGR} it follows that
for summation-guarded PCCS expressions there is no difference between both
approaches. But in general the two mappings are different, as will be
demonstrated at the end of this section.

\begin{theorem} {\bf(Abstraction)} \label{thm-abstrSR}
Let $G,H\in \IG_S$.  Then $G\Sequiv H ~\Rightarrow~ \phiSR(G)\Requiv\phiSR(H)$.
\end{theorem}
{\bf Proof:} Combine the proofs of Theorems~\ref{thm-abstrSG}
and~\ref{thm-abstrGR}. (It doesn't suffice to combine just the
theorems themselves since $\phiGR \circ \phiSG(G) \not= \phiSR(G)$ for an
arbitrary stratified transition system $G$).\qed

\begin{theorem} {\bf(Commutativity)} \label{thm-comSR}
Let $P \in \PrR$. Then $ \phiSR(\phiS(P)) \; = \; \phiR(P) $.
\end{theorem}
{\bf Proof:} We proceed along the lines of the proof
of Theorem~\ref{thm-comSG} (\ie Lemma~\ref{imarSG}), substituting
$R$'s for $G$'s, but with the following modifications in the cases for
the topmost operator of $E$.\sht\sht
\begin{description}
\item[Summation:] $p=p_j \cdot q / r$ where $r= \displaystyle \sum_{i\in I}
\multisetl p_i \mid \rarrow{E_i}{\alpha[s]}{E''}{l} \multisetr = \nu_S
(\gsigma,\{\alpha\})$.\sht
\item[Product:] In case $i\neq 0\neq j$:
$~p_1\cdot p_2\cdot q_1\cdot q_2 =r \cdot \nu_S(E,\{\alpha\}) \cdot
\nu_S(F,\{\beta\}) = r \cdot \nu_S(E\times F,\{(\alpha,\beta)\})$
and $~r_1\cdot r_2 = r \cdot \nu_S(E\times F,\{(\alpha,\beta)\})$.

In case $i\neq 0 = j$:
$~r_1\cdot r_2 = r \cdot \nu_S(E,\{\alpha\}) = r \cdot
\nu_S(E\times F,\{(\alpha,\beta)\})$.
\item[Restriction:]
$R' \vdash_{n+1} \Rarrow{E\rstr A}{\alpha[p]}{E''\rstr A}{i}$\\
iff $~R' \vdash_{n} \Rarrow{E}{\alpha[p]}{E''}{i}~$ and $~\alpha\in A$\\
iff $~S+\IMARSR \vdash_{n} \Rarrow{E}{\alpha[p]}{E''}{f(i)}~$ and
    $~\alpha\in A~$ (by induction)\\ 
iff $~S \vdash_{n} \sarrow{E\!\!}{p_1}{\!\!\!E'}{head(i)}$,
    $~S+\IMARSR \vdash\!\rarrow{E'\!\!}{\alpha[p_2]}{\!\!E''}{f(tail(i))}$,
    $~p_1\!\cdot p_2 = p\cdot\nu_S(E,\{\alpha\})$ and $\alpha\!\in\! A$\\
iff $~S \vdash_{n} \sarrow{E\!\!}{p_1}{\!\!\!E'}{head(i)}$,
    $~R \vdash\!\rarrow{E'\!\!}{\alpha[p_2]}{\!\!E''}{tail(i)}$,
    $~p_1\!\cdot p_2 = p\cdot\nu_S (E,\{\alpha\})~$ and $~\alpha\!\in\! A~$
    (induction)\\ 
iff $~S \vdash_{\!\!n+1} \sarrow{E\rstr A\!\!}{r_1}{\!\!\!E'\rstr A}{head(i)}$,
    $~R \vdash\!\rarrow{E'\rstr A\!\!}{\alpha[p_2]}{\!\!E''\rstr A}{tail(i)}~$
    and $~r_1 \cdot p_2 = p\cdot\frac{\nu_S (E,\{\alpha\})}{\nu_S (E,A)}$\\
iff $~S \vdash_{\!\!n+1} \sarrow{E\rstr A\!\!}{r_1}{\!\!\!E'\rstr A}{head(i)}$,
    {\footnotesize$~S$+IMAR$_{SR}$}$\vdash\!\rarrow{E'\rstr A\!\!}{\alpha[p_2]}
    {\!\!E''\rstr A}{f(tail(i))}$,
    $~r_1\!\cdot p_2 \!=\! p\cdot${\small $\nu_S (E\rstr A,\{\alpha\})$}\\
iff $~S+\IMARSR \vdash_{n+1} \Rarrow{E\rstr A}{\alpha[p]}{E''\rstr A}{f(i)}$.
\item[Relabeling:] This case does not apply as $E$ is a $\PCCSR$ expression.
\item[Recursion:] $~p_1 \cdot p_2 = p \cdot \nu_S(E\{\fix_X E/X\},\{\alpha\}) =
p \cdot \nu_S(\fix_X E,\{\alpha\})$.\qed
\end{description}

\begin{corollary} Let $P,Q\in \PrR$. Then $P\Sequiv Q \Rightarrow P\Requiv Q$.
\label{cor-SR}\end{corollary}

By means of the same counterexample that we used at the end of
Section~\ref{sec-inter-GR}, one shows that the equivalence induced on the
stratified model by reactive bisimulation through $\phiSR$ is not a congruence
for relabeling.  As a consequence, no compositional definition of relabeling in
the reactive model is possible that allows a generalization of
Theorem~\ref{thm-comSR}.

The corresponding counterexample for summation is also valid for $\phiGR\circ
\phiSG$, but not for $\phiSR$ (in fact, it couldn't be, by
Theorems~\ref{thm-comSR} and~\ref{thm-rcon}). Hence these two mappings are
different. It appears that $\phiSR$ preserves some of the stratified flavor
of nested PCCS summations, which is lost by $\phiGR \circ \phiSG$.

\subsection{The Probabilistic to Nonprobabilistic Abstraction}

Let $E,E'$ be PCCS expressions.  Then $\IMARSN$ is given by
$$\sarrow{E}{p}{E'}{i}\garrow{\!}{\alpha}{E''}{\!}\;\;\Longrightarrow \;\;
\garrow{E}{\alpha}{E''}{\!}$$
Similarly $\IMARGN$ and $\IMARRN$ are given by
$$\garrow {E} {\alpha[p]} {E'} {i} \;\;\; \Longrightarrow \;\;\;
\garrow {E} {\alpha} {E'} {\!}$$
$$\rarrow {E} {\alpha[p]} {E'} {i} \;\;\; \Longrightarrow \;\;\;
\garrow {E} {\alpha} {E'} {\!}$$

These inter-model abstraction rules simply throw away all probabilities.
It is comparatively straightforward to establish the remaining commutativity
results announced in the introduction.

\begin{theorem} {\bf(Abstraction)}
Let $G,H\in \IG_R$.  Then $G\Requiv H ~\Rightarrow~ \phiRN(G)\Nequiv\phiRN(H)$.
\end{theorem}
{\bf Proof:} Following the idea of the previous abstraction proofs, we show
that a reactive bisimulation on $\PrR$ is also a nonprobabilistic bisimulation
(with respect to the transitions derivable from $R+\IMARRN$, but by
commutativity these are the same as the ones derivable from $N$).
This follows as $\mu_N$ is completely determined by $\mu_R$, namely
$$\mu_N(P,\alpha,S)=\left\{ \begin{array}{lll}0&\mbox{if}&\mu_R(P,\alpha,S)=0\\
1&\mbox{if}&\mu_R(P,\alpha,S)>0\end{array} \right.~~~\Box$$

As before, the general (semantic) case can be obtained in the same way, after
defining the involved bisimulations on the (semantic) transition system
domains.  Generative or stratified to nonprobabilistic abstraction results can
also be proved likewise, but these follow already by combination with the
previous abstraction results.

\section{Conclusions and Open Problem}

In this paper we have presented a variety of congruence, commutativity, and
abstraction results that carefully interrelate the reactive, generative, and
stratified models of probabilistic processes.  In so doing, we have
seen that generative bisimulation ($\Gequiv$) is not a congruence in the 
stratified model, while stratified bisimulation ($\Sequiv$) is.
However, $\Sequiv$ is not the {\em largest} congruence contained in 
$\Gequiv$ (it is too fine). For example, consider $P=[1][1]a\,.\,\zero$ and
$Q=[1]a\,.\,\zero$. We have $\phiS(P) \not\Sequiv \phiS(Q)$ yet 
$\varphi_{SG}(\phiS({\cal C}[P])) \Gequiv \varphi_{SG}(\phiS({\cal C}[Q]))$,
for any context ${\cal C}[\,]$.

It is interesting, therefore, to ask what is the largest congruence 
contained in  $\Gequiv$. We can show that, in terms of its distinguishing
strength, the following equivalence relation falls strictly between
$\Gequiv$ and $\Sequiv$, and is still a congruence in the
stratified model. 

\begin{definition} 
An equivalence relation ${\cal R}$ $\subseteq Pr \times Pr$ is a {\em
mixed bisimulation} if $(P, Q) \in {\cal R}$ implies $\forall
S \in Pr/{\cal R}$,
\begin{itemize}
\item
$\mu_{S} (P, *, S ) =  \mu_{S} (Q, *, S )$ if both $P$ and $Q$ are probability
processes
\item
and $\forall \alpha \in Act,~ \mu_{SG} (P, \alpha, S ) =  \mu_{SG} (Q, \alpha,
S )$
\end{itemize}
Two processes $P, Q$ are {\em  mixed bisimulation equivalent} (written 
$P \, \Mequiv \, Q$) if there exists a mixed bisimulation ${\cal R}$
such that $(P, Q) \in {\cal R}$.
\end{definition}

Mixed bisimulation essentially allows an $\alpha$-transition in one
process to be matched by an $\alpha$-transition preceded by a number
of probability-1 transitions in the other process (the second clause).
At the same time, probability-1 transitions at other places may be
significant in a product context, and must therefore be taken into
account (the first clause).  We close with the following:

\noindent
{\bf Conjecture} {\bf (Full Abstraction)} In the stratified model, $\Mequiv$ 
is the largest congruence contained in $\Gequiv$.

\vspace{0.5cm}
\noindent {\large\bf Acknowledgements:}  We would like to thank 
Chris Tofts for his collaboration in \cite{vGSST}, from which the
current paper evolved, and Kim Larsen and Robin Milner
for valuable discussions on models of probabilistic processes.  We are also
indebted to the anonymous referees for their helpful comments.

\begin{thebibliography}{vGSST90}

\bibitem[BBS92]{BBS92}
{\sc J.~C.~M. Baeten, J.~A. Bergstra \& S.~A. Smolka} (1992):
\newblock {\em Axiomatizing probabilistic processes: {ACP} with generative probabilities.}
\newblock Technical report, Dept. of Math and Computing Science, Technical University of Eindhoven, Eindhoven, The Netherlands.
\newblock Extended abstract in W. R. Cleaveland, editor: {\sl Proceedings of CONCUR~'92}, LNCS 630, Springer-Verlag, Berlin, pp. 472--485, 1992.

\bibitem[BM89]{bloom-meyer}
{\sc B.~Bloom \& A.~R. Meyer} (1989):
\newblock {\em A remark on bisimulation between probabilistic processes.}
\newblock In Meyer \& Tsailin, editors: {\sl Logik at Botik}, {\sl {\rm LNCS}} 363, Springer-Verlag, Berlin, pp. 26--40.

\bibitem[Chr90]{christoff90}
{\sc I.~Christoff} (1990):
\newblock {\em Testing equivalences for probabilistic processes.}
\newblock Technical Report DoCS 90/22, Ph.D. Thesis, Department of Computer Science, Uppsala University, Uppsala, Sweden.
\newblock See also {\it Testing equivalences and fully abstract models for probabilistic processes}. In J. C. M. Baeten \& J. W. Klop, editors: {\sl Proceedings of CONCUR'90}, {\rm LNCS 458}, Springer-Verlag, Berlin, pp. 126--140, 1990.

\bibitem[CSZ92]{CSZ92}
{\sc R.~Cleaveland, S.~A. Smolka \& A.~E. Zwarico} (1992):
\newblock {\em Testing preorders for probabilistic processes.}
\newblock In W.~Kuich, editor: {\sl Proceedings of the 19th ICALP}, {\sl
{\rm LNCS}} 623, Springer-Verlag, Berlin.

\bibitem[GJS90]{gjs90}
{\sc A.~Giacalone, C.-C. Jou \& S.~A. Smolka} (1990):
\newblock {\em Algebraic reasoning for probabilistic concurrent systems.}
\newblock In M.~Broy \& C.B. Jones, editors: {\sl Proceedings Working Conference on Programming Concepts and Methods}, IFIP TC 2, Sea of Gallilee, Israel, pp. 443--458.

\bibitem[vGSST90]{vGSST}
{\sc R.~J. van Glabbeek, S.~A. Smolka, B.~Steffen \& C.~M.~N. Tofts} (1990):
\newblock {\em Reactive, generative, and stratified models of probabilistic processes.}
\newblock In {\sl Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science}, Philadelphia, PA, pp. 130--141.

\bibitem[HJ90]{HJ90}
{\sc H.~Hansson \& B.~Jonsson} (1990):
\newblock {\em A calculus for communicating systems with time and probabilities.}
\newblock In {\sl Proceedings of the 11th IEEE Symposium on Real-Time Systems}, Orlando, Florida.

\bibitem[JP89]{jones-plotkin}
{\sc C.~Jones \& G.~D. Plotkin} (1989):
\newblock {\em A probabilistic powerdomain of evaluations.}
\newblock In {\sl Proceedings of the 4th Annual IEEE Symposium on Logic in Computer Science}.

\bibitem[JL91]{JL91}
{\sc B.~Jonsson \& K.~G. Larsen} (1991):
\newblock {\em Specification and refinement of probabilistic processes.}
\newblock In {\sl Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science}, Amsterdam.

\bibitem[JS90]{JS90}
{\sc C.-C. Jou \& S.~A. Smolka} (1990):
\newblock {\em Equivalences, congruences, and complete axiomatizations for probabilistic processes.}
\newblock In J.~C.~M. Baeten \& J.~W. Klop, editors: {\sl Proceedings of CONCUR '90}, {\sl {\rm LNCS}} 458, Springer-Verlag, Berlin, pp. 367--383.

\bibitem[Low91]{Lowe91}
{\sc G.~Lowe} (1991):
\newblock {\em Prioritized and probabilistic models of timed CSP.}
\newblock Technical Report PRG-TR-24-91, Oxford University Computing
Laboratory, Programming Research Group, 11 Keble Road, Oxford OX1 3QD, England.

\bibitem[LS91]{larsen-skou-prob-bisim}
{\sc K.~G. Larsen \& A.~Skou} (1991):
\newblock {\em Bisimulation through probabilistic testing.}
\newblock {\sl Information and Computation} 94(1), pp. 1--28.
\newblock Preliminary report in {\sl Proceedings of the 16th Annual ACM Symposium on Principles of Programming Languages}, 1989.

\bibitem[LS92]{LS92}
{\sc K.~G. Larsen \& A.~Skou} (1992):
\newblock {\em Compositional verification of probabilistic processes.}
\newblock In W.~R. Cleaveland, editor: {\sl Proceedings of CONCUR~'92}, {\sl {\rm LNCS}} 630, Springer-Verlag, Berlin, pp. 456--471.

\bibitem[Mil80]{milner80}
{\sc R.~Milner} (1980):
\newblock {\em A Calculus of Communicating Systems}, {\sl {\rm LNCS}} 92.
\newblock Springer-Verlag, Berlin.

\bibitem[Mil83]{milner83}
{\sc R.~Milner} (1983):
\newblock {\em Calculi for synchrony and asynchrony.}
\newblock {\sl Theoretical Computer Science} 25, pp. 267--310.

\bibitem[Mil89]{milner89}
{\sc R.~Milner} (1989):
\newblock {\em Communication and Concurrency}.
\newblock International Series in Computer Science. Prentice Hall.

\bibitem[Par81]{park-concurrency}
{\sc D.~M.~R. Park} (1981):
\newblock {\em Concurrency and automata on infinite sequences.}
\newblock In P.~Deussen, editor: {\sl Proceedings of the 5th G.I. Conference on Theoretical Computer Science}, {\sl {\rm LNCS}} 104, Springer-Verlag, Berlin, pp. 167--183.

\bibitem[Plo81]{plotkin-sos}
{\sc G.~D. Plotkin} (1981):
\newblock {\em A structural approach to operational semantics.}
\newblock Technical Report DAIMI FN-19, Computer Science Department, Aarhus University.

\bibitem[Pnu85]{pnueli-reactive-systems}
{\sc A.~Pnueli} (1985):
\newblock {\em Linear and branching structures in the semantics and logics of reactive systems.}
\newblock In W.~Brauer, editor: {\sl Proceedings of the 12th ICALP, {\rm Nafplion}}, {\sl {\rm LNCS}} 194, Springer Verlag, Berlin, pp. 15--32.

\bibitem[Sei92]{Seidel92}
{\sc K.~Seidel} (1992):
\newblock {\em Probabilistic communicating processes.}
\newblock Technical Report PRG-102, Oxford University Computing Laboratory,
Programming Research Group, 11 Keble Road, Oxford OX1 3QD, England.

\bibitem[SS90]{SS90}
{\sc S.~A. Smolka \& B.~U. Steffen} (1990):
\newblock {\em Priority as extremal probability.}
\newblock In J.~C.~M. Baeten \& J.~W. Klop, editors: {\sl Proceedings of CONCUR '90}, {\rm LNCS 458}, Springer-Verlag, Berlin, pp. 456--466.

\bibitem[Tof90a]{tofts90}
{\sc C.~M.~N. Tofts} (1990):
\newblock {\em Proof Methods and Pragmatics for Parallel Programming}.
\newblock PhD thesis, LFCS, University of Edinburgh.

\bibitem[Tof90b]{Tof90b}
{\sc C.~M.~N. Tofts} (1990):
\newblock {\em A synchronous calculus of relative frequency.}
\newblock In J.~C.~M. Baeten \& J.~W. Klop, editors: {\sl Proceedings of CONCUR '90}, {\sl {\rm LNCS}} 458, Springer-Verlag, Berlin, pp. 467--480.

\bibitem[YL92]{YiLarsen92}
{\sc W. Yi \& K.~G. Larsen} (1992):
\newblock {\em Testing probabilistic and nondeterministic processes.}
\newblock In {\sl Proceedings of Protocol Specification, Testing and
Verification XII}, pp. 47--61.

\end{thebibliography}
\end{document}
