\documentclass{entcs} 
\usepackage{amsmath}
\usepackage{xspace}
\usepackage{enumerate}
\usepackage{pstricks,pst-node,pst-tree}
\usepackage{stmaryrd}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Macro file for Electronic Notes in Theoretical Computer Science.
% Adopted from document-style for journals published by Elsevier Science. 
% To be used with LaTeX version 2.09 of 14 January 1992 (or later) 
%
% Version: 1.10
% Date:    13 February 1998
%
% Copyright (C) 1998. All rights reserved.
%
% IMPORTANT NOTICE:
%
% You are not allowed to change this file. You may however copy this file 
% to a file with a different name and then change the copy. 
% 
% You are NOT ALLOWED to distribute this file alone. You are NOT ALLOWED 
% to take money for the distribution or use of this file (or a changed 
% version) except for a nominal charge for copying etc. 
% 
% You are allowed to distribute this file under the condition that it is 
% distributed together with all files mentioned in readme.els. 
% 
% If you receive only some of these files from someone, complain! 
% 
%

\headheight 10pt
\headsep 20pt
\footskip 20pt
\setlength{\topmargin}{-30pt}
%\addtolength{\textheight}{-20pt} 

\def\labelenumi{\rm\normalshape (\theenumi)}     
\def\labelenumii{\rm\normalshape (\theenumii)}

\font\eightrm=cmr8 scaled\magstep1
\font\eightbf=cmbx8 scaled\magstep1
\font\eighttt=cmtt8 scaled\magstep1
\font\eightit=cmsl10
\font\sixrm=cmr6 scaled\magstep1
\font\bfone=cmbx10 scaled\magstep2
\font\smc=cmcsc10 scaled\magstep1
\font\sc=cmcsc10 

\def\date{\ifcase\month\or January\or February \or March\or April\or May
\or June\or July\or August\or September\or October\or November
\or December\fi\space\number\day, \number\year}

\volume{GDP Fest}
\def\volu{GDP Fest}
\journal{Electronic Notes in Theoretical Computer Science}
\def\jour{Electronic Notes in Theoretical Computer Science}
\def\vol{GDP Fest}

\def\rightheadline{\firstheadline}
%\def\rightheadline{\ifnum\value{page}=1%\hypergetpageref{FirstPage}
%      \firstheadline \else\hfill{\scriptsize \emph{\lastname.\ $|$
%      Electronic Notes in Theoretical Computer Science \vol\ 
%      (\annum)}}\hfill\fi} 
\def\leftheadline{test}

%\def\firstheadline{\vbox{\baselineskip=10pt \parindent 0pt \obeylines
%    \eightrm\hfill INFINITY 2003\ {\eighttt Preliminary
%      Version}\hfill\break}}
%\def\firstfootline{\vbox{\baselineskip=10pt \parindent 0pt \obeylines
%    \vspace{.1in}\centerline{\eightit This is a preliminary version.
%      The final version will be published in} \centerline{\eightit
%      Electronic Notes in Theoretical Computer Science}
%    \centerline{\eightit URL: {\eighttt
%        www.elsevier.nl/locate/entcs}}}}

\def\firstheadline{GDP Festschrift\hfill ENTCS, \emph{to appear}\\}
\def\firstfootline{\hfill}

\pagestyle{headings}

% THE NEXT LINES GIVE DEFINITIONS FOR THE THEOREM ENVIRONMENTS.
% EACH IS VIEWED AS A theorem environment IN THE SENSE OF LaTeX.
% THEIR NAMES ARE: Theorem, Proposition, Lemma, Corollary, Proposition,
% Criterion, Definition, Conjecture, Example, Problem, Remark, 
% Summary, and Acknowledgement.  ALSO INCLUDED WITHIN encs.sty ARE THE
% ENVIRONMENTS Note, Claim and Case UNDER THEIR OWN NAMES, AND THE
% ENVIRONMENT Algorithm UNDER THE NAME alg; FOR THIS USE 
% \begin{alg} text \end{alg}.
% TYPE \begin{name} text \end{name} AS USUAL FOR ENVIRONMENTS IN LaTeX.
% THE ENVIRONMENT name IS NUMBERED WITHIN section. E.G. THE FIRST 'Name' 
% IN SECTION 1 IS NUMBERED 'Name 1.1'

\newenvironment{theorem}{\vspace{-\lastskip}\par\addvspace{.6pc plus
    .2pc minus .1pc}\begin{thm}}{\end{thm}\par\addvspace{.6pc plus
    .2pc minus .1pc}} \newenvironment{lemma}{\vspace{-\lastskip}\par
  \addvspace{.6pc plus .2pc minus .1pc}\begin{lem}}
  {\end{lem}\par\addvspace{.6pc plus .2pc minus .1pc}}
\newenvironment{corollary}{\vspace{-\lastskip}\par \addvspace{.6pc
    plus .2pc minus .1pc}\begin{cor}}{\end{cor}\par\addvspace{.6pc
    plus .2pc minus .1pc}}
\newenvironment{proposition}{\vspace{-\lastskip}\par \addvspace{.6pc
    plus .2pc minus .1pc}\begin{prop}}{\end{prop}\par\addvspace{.6pc
    plus .2pc minus .1pc}}
\newenvironment{criterion}{\vspace{-\lastskip}\par \addvspace{.6pc
    plus .2pc minus .1pc} \begin{crit}}{\end{crit}\par\addvspace{.6pc
    plus .2pc minus .1pc}}
\newenvironment{definition}{\vspace{-\lastskip}\par \addvspace{.6pc
    plus .2pc minus
    .1pc}\begin{defn}\rm}{\end{defn}\par\addvspace{.6pc plus .2pc
    minus .1pc}}
\newenvironment{conjecture}{\vspace{-\lastskip}\par \addvspace{.6pc
    plus .2pc minus .1pc}\begin{conj}}{\end{conj}\par\addvspace{.6pc
    plus .2pc minus .1pc}}
\newenvironment{example}{\vspace{-\lastskip}\par \addvspace{.6pc plus
    .2pc minus .1pc}\begin{exmp}\rm}{\end{exmp}\par\addvspace{.6pc
    plus .2pc minus .1pc}}
\newenvironment{problem}{\vspace{-\lastskip}\par \addvspace{.6pc plus
    .2pc minus .1pc}\begin{prob}}{\end{prob}\par\addvspace{.6pc plus
    .2pc minus .1pc}} \newenvironment{remark}{\vspace{-\lastskip}\par
  \addvspace{.6pc plus .2pc minus .1pc}\begin{rem}\rm}
{\end{rem}\par\addvspace{.6pc plus .2pc minus .1pc}}
\newenvironment{summary}{\vspace{-\lastskip}\par \addvspace{.6pc plus
    .2pc minus .1pc}\begin{summ}}{\end{summ}\par\addvspace{.6pc plus
    .2pc minus .1pc}}
\newenvironment{acknowledgement}{\vspace{-\lastskip}\par\addvspace{.6pc
    plus .2pc minus .1pc}\begin{ack}}{\end{ack}\par\addvspace{.6pc
    plus .2pc minus .1pc}}

\newenvironment{exercise}{\begin{trivlist}\item[\hskip%
    \labelsep{\bf Exercise.}]}% 
    {\end{trivlist}}

%% THE ENVIRONMENT \begin{proof} ... \end{proof} PRODUCES AN
%% END-OF-PROOF SIGN.

\newenvironment{proof}{\begin{pf}}{\qed\end{pf}}

%% THE ENVIRONMENT \begin{proof*} ... \end{proof*} SUPPORTS ADDING
%% INFORMATION SUCH AS  'Proof (Sketch)' AS THE LABEL FOR THE PROOF.

\newenvironment{proof*}{\begin{pf*}}{\qed\end{pf*}}

%% END OF `entcsmacro.sty'
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Fonts
\newfont{\fsc}{eusm10 scaled 1100}      % frenchscript letters
\newfont{\bbb}{bbm10 scaled 1100}       % blackboard bold

\newcommand{\inp}{\mathop\in}                           % takes less space
\newcommand{\ocdot}{\cdot}                              % optionally invisible \cdot
\renewcommand{\mu}{\alpha}                              % actions in Act_\tau
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{#1}}     % no vertical space
\newcommand{\dcup}{\stackrel{\mbox{\huge .}}{\cup}}	% disjoint union

%%%%%%%%%%%%%%%%%%%%%%%
%%  CSP
\newcommand{\BNFsep}{\;\;|\;\;}
\newcommand{\intc}{\mathrel{\sqcap}}
\newcommand{\extc}{\mathrel{\Box}}
\newcommand{\probc}[1]{\mathrel{\!_{\scriptscriptstyle #1}\oplus}}
\newcommand{\Par}[1]{\mathrel{|_{#1}}}
\newcommand{\parT}{\Par{\Act}}
\newcommand{\Cnil}{\mathop{\textbf{\textsf{0}}}}

\newcommand{\Act}{\ensuremath{\mathsf{Act}}\xspace}
\newcommand{\pCSP}{\ensuremath{\mathsf{pCSP}}\xspace}
\newcommand{\CSP}{\ensuremath{\mathsf{CSP}}\xspace}
\newcommand{\Op}[1]{\mbox{\bbb [}#1\mbox{\bbb ]}}

\newcommand{\standf}[1]{\operatorname{sf}(#1)}
\newcommand{\standP}{\ensuremath{\text{standardP}}\xspace}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Testing
\newcommand{\Proc}{\ensuremath{\mathcal Proc}\xspace}
\newcommand{\Tests}{\ensuremath{\mathcal T}\xspace}
\newcommand{\Outcomes}{\ensuremath{\mathcal O}\xspace}
\newcommand{\Apply}{\ensuremath{\mathcal Apply}\xspace}
\newcommand{\results}[1]{\ensuremath{\mathcal Results}(#1)}
\newcommand{\resultsN}{\ensuremath{\mathcal Results}\xspace}
\newcommand{\Fsubs}[1]{\mathop{\mbox{\fsc P}^{\mbox{\tiny\kern .1em$+$}}_{\it \kern -.2em fin}(#1)}}
\newcommand{\eureka}{\ensuremath{\omega}\xspace}
\newcommand{\maxlive}[1]{\mathop{\mathit{maxlive}(#1)}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% preorders
\newcommand{\Hleq}{\sqsubseteq_{\rm Ho}}
\newcommand{\Sleq}{\sqsubseteq_{\rm Sm}}
\newcommand{\Mustleq}{\sqsubseteq_{\text{must}}}
\newcommand{\Mayleq}{\sqsubseteq_{\text{may}}}
\newcommand{\Musteq}{\simeq_{\text{must}}}
\newcommand{\Mayeq}{\simeq_{\text{may}}}

\newcommand{\pMustleq}{\sqsubseteq_{\text{pmust}}}
\newcommand{\pMayleq}{\sqsubseteq_{\text{pmay}}}
\newcommand{\pMusteq}{\simeq_{\text{pmust}}}
\newcommand{\pMayeq}{\simeq_{\text{pmay}}}
\newcommand{\notpMustleq}{\mathrel{\not\sqsubseteq}_{\text{pmust}}}
\newcommand{\notpMayleq}{\mathrel{\not\sqsubseteq}_{\text{pmay}}}
\newcommand{\notpMusteq}{\mathrel{\not\simeq}_{\text{pmust}}}
\newcommand{\notpMayeq}{\mathrel{\not\simeq}_{\text{pmay}}}

\newcommand{\forsim}{\mathrel{\rhd\kern -.3em_{\raisebox{-.1em}{\tiny$S$}}}}
\newcommand{\liftforsim}{\mathrel{\lift{\rhd\kern-.3em_{\raisebox{-.1em}{\tiny$S$}}}}}
\newcommand{\simpreo}{\sqsubseteq_{S}}
\newcommand{\simequiv}{\simeq_{S}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% distributions
\newcommand{\dist}[1]{\mathop{\mbox{$\cal D$}} ({#1})   } % distributions
%CCM060810 The \mbox stops the D hanging below the baseline.
\newcommand{\pdist}[1]{\overline{#1}  } % distributions
\newcommand{\pS}{S_p} % states in plts for \pCSP
\newcommand{\support}[1]{\lceil{#1}\rceil}
\newcommand{\lift}[1]{\mathrel{\overline{#1}}}
\newcommand{\aRel}{\ensuremath{\mathrel{{\cal R }}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% maths
\renewcommand{\min}{\mathop{\mathit{min}}}
\renewcommand{\max}{\mathop{\mathit{max}}}
\newcommand{\setof}[2]{\{ \, #1 \, \mid \, #2 \, \}}% set comprehension
\newcommand{\sset}[1]{\{ {#1}  \}  } % singleton set
\newcommand{\cfun}[1]{\inp_{#1}} % singleton set

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%% Inference rule names
\DeclareSymbolFont{smallcaps}{\encodingdefault}{\rmdefault}{m}{sc}
\DeclareSymbolFontAlphabet\mathsc{smallcaps}
\newcommand{\Rulef}[1]{{\mathsc{#1}}}   %%font for rules 
\newcommand{\Rlts}[1]{\ensuremath{\Rulef{(#1)}}}%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%equation names
\newcommand{\Ename}[1]{\ensuremath{\mathbf{(#1)}}}%%%%

\makeatletter
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%% Inferences %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\nowidth}[2][l]{\makebox[0cm][#1]{#2}}%
\newcommand{\mnowidth}[2][l]{\makebox[0cm][#1]{$#2$}}%

\RequirePackage{ifthen}   % provides \ifthenelse
\newcommand{\ifemptyelse}[3]{\ifx\@@bullshit#1\@@bullshit#2\else#3\fi}
\newcommand{\ifnotempty}[2]{\ifx\@@bullshit#1\@@bullshit\else#2\fi}
\newenvironment{scope}
  {\bgroup\ignorespaces}
  {\egroup\global\@ignoretrue}

\newbox\@topbox
\newbox\@botbox
\newcommand{\linfer}[3][{}]{%
  \ifemptyelse{#1}{
    \setbox\@topbox\hbox{%
      \renewcommand{\arraystretch}{1}%
      $\begin{array}{l}#2\end{array}$}%
    }{
    \ifemptyelse{#2}{
      \setbox\@topbox\hbox{%
        \renewcommand{\arraystretch}{1}%
        $\begin{array}{l}\mnowidth[l]{\scriptstyle#1}\\\ \end{array}$}%
      }{
      \setbox\@topbox\hbox{%
        \renewcommand{\arraystretch}{1}%
        $\begin{array}{l}\mnowidth[l]{\scriptstyle#1}\\#2\end{array}$}%
      }
    }
  \setbox\@botbox\hbox{%
    \def\tilde##1{\widetilde{##1}}%
    \renewcommand{\arraystretch}{1}%
    $\begin{array}{l}#3\end{array}$}%
  \ifdim\wd\@botbox<\wd\@topbox% which is bigger?  set the other to match
    \setbox\@botbox\hbox to \wd\@topbox{\box\@botbox\hfil}
  \else
    \setbox\@topbox\hbox to \wd\@botbox{\box\@topbox\hfil}
  \fi
  \frac{\box\@topbox}{\box\@botbox}
  }
\newcommand{\linferSIDE}[4][{}]{%
  \ifemptyelse{#1}{
    \setbox\@topbox\hbox{%
      \renewcommand{\arraystretch}{1}%
      $\begin{array}{l}#2\end{array}$}%
    }{
    \ifemptyelse{#2}{
      \setbox\@topbox\hbox{%
        \renewcommand{\arraystretch}{1}%
        $\begin{array}{l}\mnowidth[l]{\scriptstyle#1}\\\ \end{array}$}%
      }{
      \setbox\@topbox\hbox{%
        \renewcommand{\arraystretch}{1}%
        $\begin{array}{l}\mnowidth[l]{\scriptstyle#1}\\#2\end{array}$}%
      }
    }
  \setbox\@botbox\hbox{%
    \def\tilde##1{\widetilde{##1}}%
    \renewcommand{\arraystretch}{1}%
    $\begin{array}{l}#3\end{array}$}%
  \ifdim\wd\@botbox<\wd\@topbox% which is bigger?  set the other to match
    \setbox\@botbox\hbox to \wd\@topbox{\box\@botbox\hfil}
  \else
    \setbox\@topbox\hbox to \wd\@botbox{\box\@topbox\hfil}
  \fi
  \frac{\box\@topbox}{\box\@botbox}
  \hbox{\;\footnotesize$
    \begin{scope}%
      \renewcommand{\arraystretch}{1}%
      \begin{array}[c]{l}%
        #4%
      \end{array}%
    \end{scope}%
    $}%
}

\newcommand{\slinfer}[2][{}]{\renewcommand{\arraystretch}{1}%
                  \begin{array}{l}{\scriptstyle #1}\\#2\end{array}}
\newcommand{\slinferSIDE}[3][{}]{\renewcommand{\arraystretch}{1}%
                  \begin{array}{ll}{\scriptstyle #1}\\#2 &#3\end{array}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% $ 4 Arrows
%% expanding ARROWS from James
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% usage
%%single arrow:
%\newcommand{\ar}[1]{\goesto[{#1}]}
%% double arrow:
%%\newcommand{\dar}[1]{\Goesto[{\vspace{1em}#1}]} 
%% definition follows
\def\mine{\@transition\mapstofill}
\def\goesto{\@transition\rightarrowfill}
\def\Goesto{\@transition\Rightarrowfill}
\def\ngoesto{\@transition\nrightarrowfill}
\def\nsgoesto{\@transition\nmapstofill}
\def\comesfrom{\@transition\leftarrowfill}
\def\nGoesto{\@transition\nRightarrowfill}
\def\@transition#1{\@ifnextchar[{\@@transition{#1}}{\@@transition{#1}[]}}
\newbox\@transbox
\newbox\@arrowbox
\def\mapstofill{$\m@th\mathord\mapstochar\mathord-\mkern-6mu%
  \cleaders\hbox{$\mkern-2mu\mathord-\mkern-2mu$}\hfill
  \mkern-6mu\mathord\rightarrow$}
\def\Rightarrowfill{$\m@th\mathord=\mkern-6mu%
  \cleaders\hbox{$\mkern-2mu\mathord=\mkern-2mu$}\hfill
  \mkern-6mu\mathord\Rightarrow$}
\def\nrightarrowfill{$\m@th\mathord-\mkern-6mu%
  \cleaders\hbox{$\mkern-2mu\mathord-\mkern-2mu$}\hfill
  \mkern-6mu\mathord\not\mathord-\mkern-6mu
  \cleaders\hbox{$\mkern-2mu\mathord-\mkern-2mu$}\hfill
  \mkern-6mu\mathord\rightarrow$}
\def\nmapstofill{$\m@th\mathord\mapstochar\mathord-\mkern-6mu%
  \cleaders\hbox{$\mkern-2mu\mathord-\mkern-2mu$}\hfill
  \mkern-6mu\mathord\not\mathord-\mkern-6mu
  \cleaders\hbox{$\mkern-2mu\mathord-\mkern-2mu$}\hfill
  \mkern-6mu\mathord\rightarrow$}
\def\nRightarrowfill{$\m@th\mathord=\mkern-6mu%
  \cleaders\hbox{$\mkern-2mu\mathord=\mkern-2mu$}\hfill
  \mkern-6mu\mathord\not\mathord=\mkern-6mu
  \cleaders\hbox{$\mkern-2mu\mathord=\mkern-2mu$}\hfill
  \mkern-6mu\mathord\Rightarrow$}
\def\@@transition#1[#2]%
   {\setbox\@transbox\hbox
%      doublespace.sty screws up \goesto, so we replace following line:
%      {\strut\hskip0.25em$\scriptstyle#2$\hskip0.25em}
%      with this one:
       {\vrule height 1.5ex depth .7ex width 0ex\hskip0.25em$\scriptstyle#2$\hskip0.25em}
   \ifdim\wd\@transbox<1.5em
      \setbox\@transbox\hbox to 1.5em{\hfil\box\@transbox\hfil}\fi
   \setbox\@arrowbox\hbox to \wd\@transbox{#1}
   \ht\@arrowbox\z@\dp\@arrowbox\z@
   \setbox\@transbox\hbox{$\mathop{\box\@arrowbox}\limits^{\box\@transbox}$}
   \ht\@transbox\z@\dp\@transbox\z@
   \mathrel{\box\@transbox}}   
\def\nxmapsto{\@transition\nmapstofill}
\def\xmapsto{\@transition\mapstofill}
\def\mapstofill{$\m@th\mathord\mapstochar\mathord-\mkern-6mu%
  \cleaders\hbox{$\mkern-2mu\mathord-\mkern-2mu$}\hfill
  \mkern-6mu\mathord\rightarrow$}
\def\nmapstofill{$\m@th\mathord\mapstochar\mathord-\mkern-6mu%
  \cleaders\hbox{$\mkern-2mu\mathord-\mkern-2mu$}\hfill
  \mkern-6mu\mathord\arrownot\mathord-\mkern-6mu
  \cleaders\hbox{$\mkern-2mu\mathord-\mkern-2mu$}\hfill
  \mkern-6mu\mathord\rightarrow$}
%%%%% end of arrows definition
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\makeatother
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% $ 5 Operational semantics
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\ar}[1]{\mathrel{\goesto[{#1}]}}
\newcommand{\dar}[1]{\mathrel{\Goesto[\raisebox{.08em}{\scriptsize$#1$}]}} %weak arrow
\newcommand{\hatar}[1]{\mathrel{\goesto[\hat{{#1}}]}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

\begin{frontmatter}
\title{Remarks on Testing Probabilistic Processes}

\author{Yuxin Deng$^{\mbox{\small \,B,1}}$}
\author{Rob van Glabbeek$^{\mbox{\small \,A,B}}$}
\author{Matthew Hennessy$^{\mbox{\small \,C,A,2}}$}
\author{Carroll Morgan$^{\mbox{\small \,B,1}}$}
\author{Chenyi Zhang$^{\mbox{\small \,A,B}}$}

\address{$^{\rm A}$ National ICT Australia,
Locked Bag 6016, Sydney, NSW 1466, Australia}
\address{$^{\rm B}$ School of Computer Science and Engineering,
The University of New South Wales, Sydney, Australia}
\address{$^{\rm C}$ Department of Informatics,
University of Sussex, Falmer, Brighton, BN1 9QN, UK}

\begin{abstract}
We develop a general testing scenario for probabilistic processes, 
giving rise to two theories: \emph{probabilistic may testing} and 
\emph{probabilistic must testing}. These are applied to a simple 
probabilistic version of the process calculus CSP.
%
We examine the algebraic theory of probabilistic testing, and show that 
many of the axioms of standard testing  are no longer valid
in our probabilistic setting; even for non-probabilistic CSP
processes, the distinguishing power of probabilistic tests is much greater
than that of standard tests. We develop a method for deriving
inequations valid in {probabilistic may testing} based on a
probabilistic extension of the notion of \emph{simulation}.
%
Using this, we obtain a complete axiomatisation for non-probabilistic
processes subject to probabilistic may testing.
\end{abstract}
\begin{keyword}
 Probabilistic processes, nondeterminism, CSP, transition systems, testing equivalences,
 simulation, complete axiomatisations, structural operational semantics
\end{keyword}

\thanks{We acknowledge the support of the Australian Research  
        Council (ARC) Grant DP034557.}
\thanks{This research was carried out while on a Royal Society/Leverhulme
        Trust Senior Research Fellowship.}
\end{frontmatter}

\section{Introduction}\label{sec:intro}

Operational semantics has played a useful role in computer science
since the very inception of the subject
\cite{landin,elgot,vienna1,vienna2}.
But with the publication of \cite{plotkin81structural} (republished as
\cite{plotkin04structural}) came the realisation that, properly
structured, operational semantics provides an elegant compositional
method for specifying the semantics of programming languages.
Because of its mathematical foundations, structural operational semantics
can also be used to reason about the behavioural properties of
programs, to the extent it even brings into question the necessity of
denotational semantics.

Nowhere is the power of operational semantics more evident than in the
development of process calculi: the semantic theory underlying CCS
\cite{ccs}, bisimulation equivalence, is founded entirely on
operational semantics. It provides powerful co-inductive proof methods
for establishing process equivalences; it also supports compositional
and algebraic reasoning techniques.

With CSP \cite{csp} the story is somewhat different: the
\emph{failures model} \cite{BHR84} is denotational and was used to justify
the algebraic laws so characteristic of the
subsequent development of CSP as a specification language for
processes. However, it later became apparent
that, just as for CCS, this model and its algebraic theory could be
fully justified using purely operational concepts based on  notions of
process testing \cite{OH86,DNH84}. So with CSP we have the best of all
possible worlds:
\begin{itemize}
\vspace{-.5ex}
\item a denotational model,
\vspace{-.5ex}
\item an operational model and
\vspace{-.5ex}
\item an algebraic theory,
\vspace{-.5ex}\end{itemize}
all of which are in some sense equivalent.

The topic of this paper is probabilistic process calculi. The various
semantic approaches for standard process calculi are essentially
theories of \emph{nondeterministic} processes, where the
nondeterminism represents possible choices that can be resolved in a
wholly unpredictable way. With probabilistic constructs the resolution
becomes predictable up to a point, in that it is quantified; but the
interaction between the quantified and unquantified forms of choice
then requires close attention. The issue is mainly that the two forms
of choice differ, not that one is quantified and the other is not: for
example, a similar effect occurs when considering demonic and angelic
choice together. Because they differ it is necessary to consider
carefully the order in which they occur, and how they might or might
not distribute over each other.

The first papers on probabilistic process calculi \cite{GJS90,Chr90,larsenskou}
proceed by \emph{replacing} nondeterministic with probabilistic choice.
The reconciliation of nondeterministic and probabilistic choice starts
with \cite{HJ90} and has received a lot of attention in the literature
[\nocite{JL91,WL92,JHW94,SL94,Low93,Lowe95,Seg95,MMSS96,PLS00,BS01,JW02,aTSfPA}%
\hyperlink{cite.JL91}{JL91},%
\hyperlink{cite.WL92}{WL92},%
\hyperlink{cite.JHW94}{JHW94},%
\hyperlink{cite.SL94}{SL94},%
\hyperlink{cite.Low93}{Low93},%
\hyperlink{cite.Lowe95}{Low95},%
\hyperlink{cite.Seg95}{Seg95},%
\hyperlink{cite.MMSS96}{MMSS96},
\hyperlink{cite.PLS00}{PLS00},%
\hyperlink{cite.BS01}{BS01},%
\hyperlink{cite.JW02}{JW02},%
\hyperlink{cite.aTSfPA}{SV03}%
],
even in the sequential world \cite{HSM97,MMS96}, and, more recently,
within general semantic domains \cite{MM01,Mis00,mislove03,TKP05,VW06};
as such it could be
argued that it is one of the central problems of the area. And CSP
makes the issue more interesting still, by having two forms of choice
already (both internal and external), so that probabilistic choice
becomes the third.

\bigskip\noindent
The emphasis in this paper is on the development of an algebraic
theory. Following \cite{WL92} we adapt
the original idea of testing \cite{DNH84} to probabilistic processes,
arriving at two refinement relations between processes,
the \emph{probabilistic may preorder} and
the \emph{probabilistic must preorder}.  For example $P \pMayleq Q$
means that the probability that $Q$ might pass a test is at least as
good as the probability that $P$ might pass it.  We then apply this
general framework of probabilistic testing to a simple finite
probabilistic process algebra, \pCSP, obtained by adding a
probabilistic choice operator to a cut-down version of CSP. In order
to do so we first need to interpret \pCSP as a \emph{probabilistic
  labelled transition system} \cite{JWL01,HJ90,Seg95}, a
generalisation of the well known concept of \emph{labelled transition
system}, which describes the interactions which processes may have with
their users.
 
With these generalisations it turns out that very few of the
attractive algebraic laws underlying the algebraic theory of CSP, and
indeed its denotational model, remain valid in the presence of
probabilistic choice; this is demonstrated by a series of
counterexamples, consisting of tests which distinguish process
expressions previously identified. The main result of the paper is the
development of a method for demonstrating positive algebraic
identities. We develop a
 notion of \emph{simulation} for
probabilistic processes, writing $P \simpreo Q$ to mean that process
$Q$ can simulate the behaviour or $P$. We then go on to show 
\begin{itemize}
\item the simulation relation $\simpreo$ is preserved by all the
  operators in \pCSP

\item the simulation relation is included in the {probabilistic 
may preorder}:\\  $P \simpreo Q$ implies $P \pMayleq Q$.
\end{itemize}
This enables us to develop an algebraic theory for probabilistic may testing, which
we briefly outline.  The concept of simulation can also be adapted, by introducing a notion of
\emph{failure}, to obtain similar results  for the
{probabilistic must preorder}; but in order to keep the paper concise,
the details are omitted. We do however show that, as expected, the theory based
on \emph{must} testing is more discriminating than that based on \emph{may}
testing; specifically $P \pMustleq Q$ implies $Q \pMayleq P$.

In the final section we re-examine the behaviour of standard (non-probabilistic) CSP,
using probabilistic tests. We show that these are in general more discriminating than
non-probabilistic tests, and we give a complete equational characterisation for the
resulting \emph{may} theory.

Although this paper develops an algebraic theory of probabilistic
testing in terms of \pCSP, we could have obtained similar results
using probabilistic versions of CCS or ACP, because processes defined
in these calculi can be interpreted likewise.

\section{Testing processes}\label{sec:testing}

It is natural to view the semantics of processes as being determined
by their ability to pass tests \cite{DNH84,henn,BHR84,WL92,Seg96};
processes $P_1$ and $P_2$ are deemed to be semantically equivalent
unless there is a test which can distinguish them.  The actual tests
used typically represent the ways in which users, or indeed other
processes, can interact with $P_i$.

Let us first set up a general testing scenario, within which this idea
can be formulated.  It assumes
\begin{itemize} 
\item a set of processes \Proc
\item a set of tests \Tests, which can be applied to processes
\item a set of outcomes \Outcomes, the possible results from applying
a test to a process
\item
a function $\Apply: \Tests \times \Proc \rightarrow \Fsubs{\Outcomes}$, representing
the possible results of applying a specific test to a specific process.
\end{itemize}
Here $\Fsubs{\Outcomes}$ denotes the collection of finite non-empty
subsets of \Outcomes; so the result of applying a test $T$ to a
process $P$, $\Apply(T,P)$, is in general a \emph{set} of outcomes,
representing the fact that the behaviour of processes, and indeed
tests, may be nondeterministic. A more general theory would allow
$\Apply(T,P)$ to be an arbitrary non-empty subset of \Outcomes, but
for the class of finite processes we consider in this paper, a finite
set of outcomes turns out to be sufficient.

Moreover, some outcomes are considered better then others; for example
the application of a test may simply succeed, or it may fail, with
success being better than failure.  So we can assume that \Outcomes is
endowed with a partial order, in which $o_1 \leq o_2$ means that $o_2$
is a better outcome than $o_1$.

When comparing the result of applying tests to processes we need to
compare subsets of \Outcomes. There are two standard approaches to
make this comparison, based on viewing these sets as elements of
either the Hoare or Smyth powerdomain \cite{Hen82,AJ94} of \Outcomes.
For $O_1, O_2 \in \Fsubs{\Outcomes}$ we let
\begin{enumerate}[(i)]
\item $O_1 \Hleq O_2$ if for every $o_1 \in O_1$ there exists some $o_2 \in O_2$
such that $o_1 \leq o_2$

\item $O_1 \Sleq O_2$ if for every $o_2 \in O_2$ there exists some $o_1 \in O_1$
such that $o_1 \leq o_2$.
\end{enumerate}
Using these two comparison methods we obtain two different semantic
preorders for processes:
\begin{enumerate}[(i)]
\item 
For $P,Q \inp \Proc$ let $P \mathbin{\Mayleq} Q$ if
$\Apply(T,P) \mathbin{\Hleq} \Apply(T,Q)$ for every test $T$

\item 
Similarly, let  $P \Mustleq Q$ if
$\Apply(T,P) \Sleq \Apply(T,Q)$  for every test $T$.
\end{enumerate}  
We use $P \Mayeq Q$ and $P \Musteq Q$ to denote the associated equivalences.

{\newcommand{\PupCl}[1]{\mbox{\fsc P}^\uparrow\kern -.1em (#1)}
The terminology \emph{may} and \emph{must} refers to the following
reformulation of the same idea.  Let ${\it Pass} \subseteq \Outcomes$
be an upwards-closed subset of $\Outcomes$, i.e.\ satisfying
$o'\geq o\inp{\it Pass} \Rightarrow o'\inp {\it Pass}$, thought of as
the set of outcomes that can be regarded as \emph{passing} a
test. Then we say that a process $P$ \emph{may} pass a test $T$ with
an outcome in {\it Pass}, notation ``$P$ {\bf may} ${\it Pass}~T$'',
if there is an outcome $o\in\Apply(P,T)$ with $o\inp\textit{Pass}$,
and likewise $P$ \emph{must} pass a test $T$ with an outcome in {\it
Pass}, notation \mbox{``$P$ {\bf must} ${\it Pass}~T$''}, if for all
$o\in\Apply(P,T)$ one has $o\inp\textit{Pass}$.  Now
\begin{eqnarray*}
P \Mayleq Q \mbox{~~iff~~} \forall T\inp\Tests\, \forall \textit{Pass}
 \inp \PupCl{\Outcomes}\, (P~\textbf{may}~\textit{Pass}~T
 ~\Rightarrow~ Q~\textbf{may}~\textit{Pass}~T)~~\\
P \Mustleq Q \mbox{~~iff~~} \forall T\inp\Tests\, \forall \textit{Pass}
 \inp \PupCl{\Outcomes}\, (P~\textbf{must}~\textit{Pass}~T
 ~\Rightarrow~ Q~\textbf{must}~\textit{Pass}~T)
\end{eqnarray*}
where $\PupCl{\Outcomes}$ is the set of upwards-closed
subsets of $\Outcomes$.
}

The original theory of testing \cite{DNH84,henn} is obtained by using
as the set of outcomes \Outcomes the two-point lattice
\begin{center}
  \begin{picture}(40,50)(0,0)
  \linethickness{0.5pt} 
  \put(20,0){$\bot$}
  \put(20,45){$\top$}
  \put(24.2,13.7){\line(0,1){25}}
  \end{picture}
\end{center}
with $\top$ representing the success of a test application, and $\bot$ failure. 

However, for probabilistic processes we consider an
application of a test to a process to succeed with a given
probability. Thus we take as the set of outcomes
the unit interval $[0,1]$, with the standard
mathematical ordering; if $0 \leq p < q \leq 1$ then succeeding with 
probability $q$ is considered better than succeeding with probability $p$.
This yields two preorders for probabilistic
processes, which for convenience we rename 
 $\pMayleq$ and $\pMustleq$, with the associated equivalences 
 $\pMayeq$ and $\pMusteq$ respectively.
These preorders, and their associated equivalences, were first
defined by Wang and Larsen \cite{WL92}. The purpose of the current paper is to apply
them to a simple probabilistic process algebra. 

Before doing so let us first point out a useful simplification: the
Hoare and Smyth preorders on finite subsets of $[0,1]$ (and more
generally on \emph{closed} subsets of $[0,1]$) are determined by their
maximum and minimum elements respectively.
\begin{proposition}\rm\label{min-max}
  For $O_1,\;O_2 \in \Fsubs{\Outcomes_{\text{prob}}}$ we have
  \begin{enumerate}[(i)]
  \item $O_1 \Hleq O_2$  if and only if $\max(O_1) \leq \max (O_2)$
  \item $O_1 \Sleq O_2$  if and only if $\min (O_1) \leq \min (O_2)$.
  \end{enumerate}
\end{proposition}
\begin{proof}
  Straightforward calculations.
%  For example to prove (i) let  $m_i$
%  denote the maximum element of $O_i$. First suppose $O_1 \Hleq O_2$. Then
%  there exists some element $o_2$ of $O_2$ such that $m_1 \leq o_2$,
%  from which it follows immediately that $m_1 \leq m_2$. Conversely
%  suppose $m_1 \leq m_2$. If $o_1$ is an arbitrary element of $O_1$
%  then, since $o_1 \leq m_1$, we have that $o_1 \leq m_2$. It follows
%  by definition that $O_1 \Hleq O_2$.
\end{proof} 
\noindent
As in the non-probabilistic case \cite{DNH84}, we could also define
a testing preorder combining the may- must-preorders; we will not  
study this combination here.

\section{Finite probabilistic CSP}

We first define the language and its operational semantics. Then we show how the
general probabilistic testing theory just outlined can be applied to processes from this
language.

\subsection{The language}

Let $\Act$ be a set of actions, ranged over by $a,b,c,\ldots$, which
processes can perform.  Then the finite probabilistic CSP
processes are given by the following syntax:
\begin{equation*}
  P ::=  \Cnil \BNFsep a.P \BNFsep P \intc P \BNFsep P \extc P \BNFsep P \Par{A} P
             \BNFsep P \probc{p} P
\end{equation*}    
The intuitive meaning of the various constructs is straightforward:
\begin{enumerate}[(i)]
\item $\Cnil$ represents the stopped process.

\item $a.P$, where $a$ is in \Act, is a process which first performs the action $a$, and then proceeds as $P$.

\item $P \intc Q$ is the \emph{internal choice} between the processes
  $P$ and $Q$; it will act either like $P$ or like $Q$, but a user is
  unable to influence which.
  
\item $P \extc Q$ is the \emph{external choice} between $P$ and $Q$;
  again it will act either like $P$ or like $Q$ but, in this case, according to the demands
  of a user.
  
\item $P \Par{A} Q$, where $A$ is a subset of \Act,
  represents processes $P$ and $Q$ running in parallel. They may
  synchronise by performing the same action from $A$ simultaneously; such a
  synchronisation results in an internal action $\tau\not\in\Act$.
  In addition $P$ and $Q$ may independently do any action from
  $(\Act\setminus A)\cup\{\tau\}$.
  
\item $P \probc{p} Q$, where $p$ is an arbitrary probability, a real
  number strictly between 0 and 1, is the \emph{probabilistic choice} between
  $P$ and $Q$. With probability $p$ it will act like $P$ and with
  probability $(1\mathord-p)$ it will act like $Q$.
\end{enumerate}
We use \pCSP to denote the set of terms defined by this grammar, and
\CSP denotes the subset of that which does not use the probabilistic choice.
Of course the language CSP in all its glory \cite{BHR84,csp,OH86} has
many more operators; we have simply chosen a representative selection,
adding probabilistic choice to obtain an
elementary probabilistic version of CSP\@. Our parallel operator is
not a CSP primitive, but it can easily be expressed in terms of the
CSP primitives---in particular $P\Par{A}Q = (P\|_AQ)\backslash A$,
where $\|_A$ and $\backslash A$ are the parallel composition and
hiding operators of \cite{OH86}.  It can also be expressed in terms of
the parallel composition, renaming and restriction operators of CCS\@.
We have chosen this (non-associative) operator for its convenience
in defining the application of tests to processes.

As usual we tend to omit occurrences of $\Cnil$; the action prefixing
operator $a.\_\!\_$ binds stronger than any of the binary operators, and
precedence between the binary operators will be indicated via brackets
or spacing. We will also sometimes use $n$-ary versions of the binary
operators, such as $\bigoplus_{i\in I}p_i P_i$ with
$\sum_{i\in I}p_i=1$, and $\bigbox_{i \in I}P_i$.

\subsection[Operational Semantics of pCSP]{Operational Semantics of \pCSP}
\label{sec:operational}

The above intuitive reading of the various operators can be formalised
by an \emph{operational semantics} which associates with each process
term a graph-like structure representing the manner in which it
may react to users' requests. Let us briefly recall this procedure for
(non-probabilistic) \CSP.

\begin{definition}
  A \emph{labelled transition system} (LTS) is a triple $\langle S,
  \Act_\tau, \rightarrow\rangle$, where
  \begin{enumerate}[(i)]
  \item $S$ is a set of states
  \item $\Act_\tau$ is a set of actions \Act, augmented with a new action symbol 
        $\tau$ to represent synchronisations, and more generally internal unobservable
        activity
  \item $ \rightarrow \;\;\subseteq\;\; S \times \Act_\tau \times S$ 
   represents the effect of performing actions. 
  \end{enumerate}
It is usual to use the more intuitive notation $s \ar{\mu} s'$ instead of 
$(s,\mu,s') \in\; \rightarrow$.
\end{definition}

\noindent
The operational semantics of \CSP is obtained by endowing the set of
terms with the structure of an LTS. Specifically
\begin{enumerate}[(i)]
\item the set of states $S$ is taken to be all terms from the language \CSP

\item the action relations  $P \ar{\mu} Q$ are defined inductively on the syntax of terms.
\end{enumerate}
A precise definition may be found in \cite{OH86}.

In order to interpret the full \pCSP operationally we need to
generalise the notion of LTS to take probabilities into account. First
we need some notation for \emph{probability distributions}. A
(discrete) probability distribution over a set $S$ is a mapping
\mbox{$\Delta: S \rightarrow [0,1]$} with $\sum_{s\in S}\Delta(s)=1$. The
\emph{support} of $\Delta$ is given by $\support{\Delta} := \setof{s
\in S}{\Delta(s) > 0}$.  For our simple setting we only require
distributions with finite support; let $\dist{S}$, ranged over by
$\Delta, \Theta,\Phi$, denote the collection of all such
distributions over $S$.  We use $\pdist{s}$ to denote the point
distribution, satisfying
\begin{equation*}
  \pdist{s}(t) =
     \begin{cases}
          1 &\text{if $t=s$},\\
          0 &\text{otherwise}
      \end{cases} 
\end{equation*}
while if $p_i\geq 0$ and $\Delta_i$ is a distribution for each 
$i$ in some finite index set $I$, then $\sum_{i \in I}p_i \ocdot \Delta_i$ is  given by
\begin{equation*}
  (\sum_{i \in I}p_i \ocdot \Delta_i)(s) ~~~=~~~ \sum_{i \in I} p_i \cdot\Delta_i(s)
\end{equation*}
If $\sum_{i \in I} p_i = 1$ then this is easily seen to be a distribution in
$\dist{S}$, and we will sometimes write it as $p_1 \ocdot \Delta_1 + \ldots + p_n \ocdot \Delta_n$
when the index set $I$ is $\sset{1,\ldots,n}$.

We can now present the probabilistic generalisation of an LTS:
\begin{definition}
A \emph{probabilistic labelled transition system} (pLTS) is a triple\\
$\langle S, \Act_\tau, \rightarrow \rangle$, where
\begin{enumerate}[(i)]
\item $S$ is a set of states
\item $\Act_\tau$ is a set of actions \Act, augmented by a new action
  $\tau$, as above
\item $\rightarrow \;\;\subseteq\;\; S \times \Act_\tau \times \dist{S}$.
\end{enumerate}
As with LTSs, we usually write $s \ar{\mu} \Delta$ in place of 
$(s,\mu,\Delta) \in \;\rightarrow$.
An LTS may be viewed as a degenerate pLTS, one in which only point 
distributions are used.
\end{definition}

\noindent
We now mimic the operational interpretation of \CSP as an LTS by associating with
\pCSP a particular pLTS  $\langle \pS, \Act_\tau, \rightarrow \rangle$. 
However there are two major differences:
\begin{enumerate}[(i)]
\item only a subset of terms in \pCSP will be used as the set of states $\pS$ in the pLTS

\item terms in \pCSP will be interpreted as distributions over $\pS$,
  rather than as elements of $\pS$.
\end{enumerate}
First we define the subset $\pS$ of states that we use: it is the least set satisfying
\begin{enumerate}[(i)]
\item $\Cnil \in \pS$

\item $a.P \in \pS$

\item $P \intc Q \in \pS$

\item $s_1,s_2 \in \pS$ implies $s_1 \extc s_2 \in \pS$

\item $s_1,s_2 \in \pS$ implies $s_1 \Par{A} s_2 \in \pS$.
\end{enumerate}
Thus, $\pS$ is the set of \pCSP expressions in which every occurrence
of the probabilistic choice operator $\probc{p}$ is \emph{weakly guarded},
i.e.\ is within a subexpression of the form $a.P$ or $P \intc Q$.
The interpretation of terms in \pCSP as distributions in $\dist{\pS}$ is
as follows:
\begin{enumerate}
\item $\Op{\Cnil} = \pdist{\Cnil}$

\item $\Op{a.P} = \pdist{a.P}$

\item $\Op{P \intc Q} = \pdist{P \intc Q}$

\item $\Op{P \probc{p} Q} = p \ocdot \Op{P} + (1\mathord-p) \ocdot \Op{Q}$

\item $\Op{P \extc Q} = \Op{P} \extc \Op{Q}$

\item $\Op{P \Par{A} Q} = \Op{P} \Par{A} \Op{Q}$.
\end{enumerate}
In the last two cases we take advantage of the fact that both $\extc$ and 
$\Par{A}$ can be viewed as binary operators over $\pS$, and can therefore 
be lifted to $\dist{\pS}$ in the standard manner. Namely we define
 \begin{equation*}
  (\Delta_1 \extc \Delta_2)(s) ~~~=~~~
     \begin{cases}
          \Delta_1(t_1) \cdot \Delta_2(t_2) &\text{if $s = t_1 \extc t_2$},\\
          0 &\text{otherwise}
      \end{cases} 
\end{equation*}
with $\Delta_1 \Par{A} \Delta_2$ given similarly;
note that as a result we have $\Op{P}=\pdist{P}$ for all $P\inp \pS$.
Finally the definition of the relations $\ar{\mu}$ is given in
Figure~\ref{fig:opsem}.
\begin{figure}[t]
\vspace{-.5em}
  \begin{align*}
    &\slinfer[\Rlts{action}]{a.P \ar{a} \Op{P}} 
\\
    & \slinfer[\Rlts{int.l}]{P \intc Q \ar{\tau} \Op{P}}
    && \slinfer[\Rlts{int.r}]{P \intc Q \ar{\tau} \Op{Q}}
\\
   &\linfer[\Rlts{ext.i.l}]{s_1 \ar{\tau} \Delta}
                 {s_1 \extc s_2 \ar{\tau} \Delta \extc \pdist{s_2}}
   && \linfer[\Rlts{ext.i.r}]{s_2 \ar{\tau} \Delta}
                 {s_1 \extc s_2 \ar{\tau} \pdist{s_1} \extc \Delta}
\\
  &\linfer[\Rlts{ext.l}]{s_1 \ar{a} \Delta}
                {s_1 \extc s_2 \ar{a} \Delta}
  &&
 \linfer[\Rlts{ext.r}]{s_2 \ar{a} \Delta}
                {s_1 \extc s_2 \ar{a} \Delta}
\\
  &\linferSIDE[\Rlts{par.l}]{s_1 \ar{\mu} \Delta}
                 {s_1 \Par{A} s_2 \ar{\mu} \Delta \Par{A} \pdist{s_2}}
                 {\mu \not\in A}
   && \linferSIDE[\Rlts{par.r}]{s_2 \ar{\mu} \Delta}
                 {s_1 \Par{A} s_2 \ar{\mu} \pdist{s_1} \Par{A} \Delta}
                 {\mu \not\in A}
\\
  &\linferSIDE[\Rlts{par.i}]{s_1 \ar{a} \Delta_1,\;s_2 \ar{a} \Delta_2}
                {s_1 \Par{A} s_2 \ar{\tau} \Delta_1 \Par{A} \Delta_2}
		{a\in A}
 \end{align*}

  \caption{Operational semantics of \pCSP.\label{fig:opsem}
  Here $a$ ranges over $\Act$ and $\mu$ over $\Act_\tau$.}
  
\end{figure}
These rules are very similar to the
standard ones used to interpret \CSP as an LTS \cite{OH86}, modified
to take into account that the result of an action must be a
distribution.  For example \Rlts{int.l} and \Rlts{int.r} say that $P
\intc Q$ makes an internal unobservable choice to act either like $P$
or like $Q$. Similarly the four rules \Rlts{ext.l}, \Rlts{ext.r},
\Rlts{ext.i.l} and \Rlts{ext.i.r} can be read as giving the standard
interpretation to the external choice operator: the process $P \extc
Q$ may perform any external action of its components $P$ and $Q$,
which resolves the choice; it may also perform any of their internal
actions, but when these are performed the choice is not resolved.

\subsection{The precedence of probabilistic choice}

Our operational semantics entails that $\extc$ and
$\Par{A}$ distribute over probabilistic choice:
\vspace{-1ex}
$$\begin{array}{rcl}
     \Op{P \extc (Q \probc{p} R)}    &=& \Op{(P \extc Q) \probc{p} (P \extc R)}\\   
     \Op{P \Par{A}  (Q \probc{p} R)} &=& \Op{(P \Par{A}  Q) \probc{p} (P \Par{A}  R)}
\end{array}$$
In Section~\ref{sec:axioms}, these identities will return as
axioms of may testing. However, this is not so much a consequence of
our testing methodology: it is hardwired in our interpretation
$\Op{\_\!\_}$ of \pCSP expressions as distributions. We could have
obtained the same effect by introducing \pCSP as a two-sorted
language, given by the grammar
\begin{eqnarray*}
  P &::=&  S \BNFsep P \probc{p} P
\\
  S &::=&  \Cnil \BNFsep a.P \BNFsep P \intc P \BNFsep S \extc S \BNFsep S \Par{A} S
\end{eqnarray*}
and introducing expressions like $P \extc (Q \probc{p} R)$ and $P
\Par{A}  (Q \probc{p} R)$ as syntactic sugar for the grammatically
correct expressions obtained by distributing $\extc$ and $\Par{A}$
over $\probc{p}$. In that case, the $S$-expressions would constitute
the set $S_p$ of states in the pLTS of \pCSP, and $\Op{s} = \pdist{s}$
for any $s\inp S_p$.
  
A consequence of our operational semantics is that in
the process $a.(b\probc{\frac{1}{2}}c) \Par{\emptyset} d$
the action $d$ can be scheduled either before $a$, or after the
probabilistic choice between $b$ and $c$---but it can \emph{not} be
scheduled after $a$ and before this probabilistic choice.
We justify this by thinking of $P \probc{p} Q$ not as a process that
starts with making a probabilistic choice, but rather as one that
\emph{has} just made such a choice, and with probability $p$ \emph{is}
no more and no less than the process $P$. Thus \mbox{$a.(P\probc{p}Q)$}
is a process that in doing the $a$-step makes a probabilistic choice
between the alternative targets $P$ and $Q$.

This design decision is in full agreement with previous work featuring
nondeterminism, probabilistic choice and parallel composition
\cite{HJ90,WL92,Seg95}. Moreover, a probabilistic choice between
processes $P$ and $Q$ that does not take precedence over actions
scheduled in parallel can simply be written as $\tau.(P\probc{p}Q)$.
Here $\tau.P$ is an abbreviation for $P\intc P$.  Using the
operational semantics of $\intc$ in Figure~\ref{fig:opsem}, $\tau.P$
is a process whose sole initial transition is \mbox{$\tau.P \ar{\tau}
P$}, hence $\tau.(P\probc{p}Q)$ is a process that starts with making a
probabilistic choice, modelled as an internal action, and with
probability $p$ proceeds as $P$. Any activity scheduled in parallel
with $\tau.(P\probc{p}Q)$ can now be scheduled before or after this
internal action, hence before or after the making of the choice.
In particular, $a.\tau.(b\probc{\frac{1}{2}}c) \Par{\emptyset} d$
allows $d$ to happen between $a$ and the probabilistic choice.

\subsection[Graphical representation of pCSP processes]{Graphical representation of \pCSP processes}
\label{sec:graphical}

We graphically depict the operational semantics of a \pCSP expression
$P$ by drawing the part of the pLTS defined above that is reachable
from $\Op{P}$ as a finite acyclic directed graph. Given that in a pLTS
transitions go from states to distributions, we need to introduce
additional edges to connect distributions back to states, thereby
obtaining a bipartite graph.  States are represented by nodes of the
form $\bullet$ and distributions by nodes of the form $\circ$. For any
state $s$ and distribution $\Delta$ with $s\ar{\alpha}\Delta$ we draw
an edge from $s$ to $\Delta$, labelled with $\alpha$. Consequently,
the edges leaving a $\bullet$-node are all labelled with actions from
$\Act_\tau$.  For any distribution $\Delta$ and state
$s$ in $\support{\Delta}$, the support of $\Delta$, we draw an edge from
$\Delta$ to $s$, labelled with $\Delta(s)$. Consequently, the edges
leaving a $\circ$-node are labelled with positive real numbers that
sum up to 1. Because for our simple language the resulting directed
bipartite graphs are acyclic, we leave out arrowheads on edges and we
assume control to flow from top to bottom.

\begin{figure}[t]
\vspace{-1ex}
$$
  \begin{array}{ccc}
     \pstree[nodesep=0pt,levelsep=20pt,labelsep=.05]{\Tdot[dotstyle=o]}
      {\pstree{\Tdot \tlput{1}}
              {\pstree{\Tdot[dotstyle=o] \tlput{d}}
                     {\pstree {\Tdot \tlput{1}}{}
                     }}} 
\qquad \text{abbrev. to}\qquad 
     \pstree[nodesep=0pt,levelsep=20pt,labelsep=.05]{\Tdot}
      {\pstree{\Tdot \tlput{d}}{}}
&\qquad\qquad\qquad\quad&
     \pstree[nodesep=0pt,levelsep=20pt,labelsep=.05]{\Tdot[dotstyle=o]}
       {\pstree{\Tdot \tlput{1}}
               {\pstree{\Tdot[dotstyle=o] \tlput{\tau}}
                       {\pstree{\Tdot \tlput{1}}
                         {\pstree{\Tdot[dotstyle=o] \tlput{b}}
                           {\pstree{\Tdot \tlput{1}}{}
			    }
                          }
                       }
                \pstree{\Tdot[dotstyle=o] \trput{\tau}}
                       {\pstree{\Tdot \trput{1}}
                         {\pstree{\Tdot[dotstyle=o] \trput{c}}
                           {\pstree{\Tdot \trput{1}}{}
			    }
                          }
                       }
               }
               
       }
 \qquad \text{abbrev. to}\qquad 
    \pstree[nodesep=0pt,levelsep=20pt,labelsep=.05]{\Tdot}
          {\pstree{\Tdot \tlput{\tau}}
                  {\pstree{\Tdot \tlput{b}}{}}
           \pstree{\Tdot \trput{\tau}}
                 {\pstree{\Tdot \trput{c}}{}}
           }
\\[-.5em]
i)\;\;d.\Cnil &\qquad& ii)\;\;b.\Cnil \intc c.\Cnil
  \end{array}
$$
$$
  \begin{array}{@{}ccc@{}}
    \pstree[nodesep=0pt,levelsep=20pt,labelsep=.05]{\Tdot[dotstyle=o]}
      {\pstree{\Tdot \tlput[tpos=.1]{\scriptscriptstyle{\frac{1}{2}}}}
              {\pstree{\Tdot\tlput{\tau}}
                      {\pstree{\Tdot\tlput{b}}{}
                       \pstree{\Tdot\trput{d}}{}}
               \pstree{\Tdot\tlput[tpos=.7]{d}}{}
               \pstree{\Tdot\trput{\tau}}
                      {\pstree{\Tdot\tlput{c}}{}
                       \pstree{\Tdot\trput{d}}{}}
              }
       \pstree{\Tdot \trput[tpos=.1]{\scriptscriptstyle{\frac{1}{2}}}}
              {\pstree{\Tdot\tlput{\tau}}
                      {\pstree{\Tdot\tlput{b}}{}
                       \pstree{\Tdot\trput{a}}{}}
               \pstree{\Tdot\tlput[tpos=.7]{a}}{}
               \pstree{\Tdot\trput{\tau}}
                      {\pstree{\Tdot\tlput{c}}{}
                       \pstree{\Tdot\trput{a}}{}}
              }
      }

&\qquad\qquad\quad&
    \pstree[nodesep=0pt,levelsep=20pt, labelsep=.05]{\Tdot[dotstyle=o]}
        {\pstree{\Tdot \tlput[tpos=.1]{\scriptscriptstyle{\frac{1}{3}}}}
                     {\pstree{\Tdot \tlput{a}}{}}
         \pstree{\Tdot \trput[tpos=.7,labelsep=0]{\scriptscriptstyle{\frac{1}{3}}}}
             {\pstree{\Tdot\tlput{\tau}}
                      {\pstree{\Tdot\tlput{b}}{}
                       \pstree{\Tdot\trput{d}}{}}
               \pstree{\Tdot\tlput[tpos=.7]{d}}{}
               \pstree{\Tdot\trput{\tau}}
                      {\pstree{\Tdot\tlput{c}}{}
                       \pstree{\Tdot\trput{d}}{}}
              }         
         \pstree{\Tdot \trput[tpos=.1]{\scriptscriptstyle{\frac{1}{3}}}}
             {\pstree{\Tdot\tlput{\tau}}
                      {\pstree{\Tdot\tlput{b}}{}
                       \pstree{\Tdot\trput{a}}{}}
               \pstree{\Tdot\tlput[tpos=.7]{a}}{}
               \pstree{\Tdot\trput{\tau}}
                      {\pstree{\Tdot\tlput{c}}{}
                       \pstree{\Tdot\trput{a}}{}}
              }  
        }
\\
 iii)\;\;   (b \intc c) \extc (d \probc{\frac{1}{2}} a)
&\qquad&
 iv)\;\; a \probc{\frac{1}{3}} ( (b \intc c) \extc (d \probc{\frac{1}{2}} a) )
  \end{array}
$$
  \caption{Example pLTSs}\label{fig:plts.exs}
\end{figure}
A few examples are described in
Figure~\ref{fig:plts.exs}. In \textit{i}) we find $\Op{d.\Cnil}$ as the point
distribution $\pdist{d.\Cnil}$, represented by a tree with one edge
from the root, labelled with the probability $1$, to the state
$d.\Cnil$. In turn this state is represented as the subtree with one
outgoing edge, labelled by the only possible action $d$ to  $\Op{\Cnil}$.
Finally this is also a point distribution, represented as a
subtree with one edge leading to a leaf, labelled by the probability $1$. 

These edges labelled by probability $1$ occur so frequently
that it makes sense to omit them, together with the associated nodes $\circ$
representing point distributions. With this convention $\Op{d.\Cnil}$
turns out to be a simple tree with one edge labelled by the action
$d$. The same convention simplifies considerably the representation of
$b \intc c$ in \textit{ii}), resulting in an LTS detailing an internal choice
between the two actions.
Officially, the endnodes of this graph ought to be merged, as both of
them represent the process $\Cnil$. However, for reasons of clarity,
in graphical representations we often unwind the underlying graph into
a tree, thus representing the same state or distribution multiple times.

The interpretation of $(b \intc c) \extc (d \probc{\frac{1}{2}} a)$ is
more interesting.  This requires clause (\textit{v}) above in the definition of
$\Op{\_\!\_}$, resulting in the distribution \plat{$\pdist{(b \intc
c)} \extc \Delta$}, where $\Delta$ is the distribution resulting from
the interpretation of $(d \probc{\frac{1}{2}} a)$, itself a two-point
distribution mapping both the states $d.\Cnil$ and $a.\Cnil$ to the
probability \plat{$\frac{1}{2}$}. The result is again a two-point
distribution, this time mapping the two states $(b \intc c) \extc d$
and $(b \intc c) \extc a$ to \plat{$\frac{1}{2}$}. The end result in
\textit{iii}) is obtained by further interpreting these two states using the
rules in Figure~\ref{fig:opsem}. Finally in \textit{iv}) we show the graphical
representation which results when this term is combined
probabilistically with the simple process $a.\Cnil$.
  
To sum up, the operational semantics endows \pCSP with the structure
of a pLTS, and the function $\Op{\_\!\_}$ interprets process terms in \pCSP
as distributions in this pLTS, which can be represented by finite
acyclic directed graphs (typically drawn as trees), with edges
labelled either by probabilities or actions, so that edges labelled by
actions and probabilities alternate (although in pictures we may
suppress 1-labelled edges and point distributions).

\subsection[Testing pCSP processes]{Testing \pCSP processes}

Let us now turn to applying the testing theory from
Section~\ref{sec:testing} to \pCSP. As with the standard theory
\cite{DNH84,henn}, we use as tests any process from \pCSP itself, which
in addition can use a special symbol \eureka to report success.
For example, $a.\eureka \probc{\frac{1}{4}} (b \extc c.\eureka)$ is a
probabilistic test, which 25\% of the time requests an $a$ action, and
75\% requests that $c$ can be performed. If it is used as {\it must} test
the 75\% that requests a $c$ action additionally requires that $b$ is not
possible. As in \cite{DNH84,henn}, it is not the execution of \eureka that
constitutes success, but the arrival in a state where \eureka is possible.
The introduction of the \eureka-action is simply a method of defining a
success predicate on states without having to enrich the language of
processes explicitly with such predicates.

Formally, let $\eureka\mathop{\not\in}\Act_\tau$ and write
$\Act^\eureka$ for $\Act\cup\{\eureka\}$ and $\Act^\eureka_\tau$ for
$\Act\cup\{\tau,\eureka\}$. In Figure~\ref{fig:opsem} we now let $a$
range over $\Act^\eureka$ and $\alpha$ over $\Act^\eureka_\tau$.
Tests may have subterms $\eureka.P$, but other processes may not.
To apply the test $T$ to the process $P$ we run them in
parallel, tightly synchronised; that is, we run the combined process
$T \Par{\Act} P$. Here $P$ can only synchronise with $T$, and
in turn the test $T$ can only perform the success action $\eureka$, in
addition to synchronising with the process being tested; of course
both tester and testee can also perform internal actions.
\begin{figure}[t]

\begin{center}
\pstree[nodesep=2pt,levelsep=40pt,labelsep=1pt]{\TR{$(a.\eureka \probc{\frac{1}{4}} (b \extc c.\eureka)) \parT
  (b \extc c \extc d)$}}
  {\pstree{\TR{$a. \eureka \parT (b\extc c\extc d)$}
  \tlput{$\scriptscriptstyle{\frac{1}{4}}$}}{}
  \pstree{\TR{$(b\extc c. \eureka) \parT (b\extc c\extc d)$}
  \trput{$\scriptscriptstyle{\frac{3}{4}}$}}
  	{\pstree{\TR{$0\parT 0$} \tlput{$\tau$}}{}
	\pstree{\TR{$\eureka \parT 0$} \trput{$\tau$}}{
		\pstree{\TR{$0\parT 0$}\tlput{$\eureka$}}{}}}}

$\Apply{((a.\eureka \probc{\frac{1}{4}} (b \extc c.\eureka)) ,
 (b \extc c \extc d))} = \frac{1}{4}\ocdot\sset{0} + \frac{3}{4}\ocdot\sset{0, 1}
 = \sset{0, \frac{3}{4}}$
  
\end{center}
  \caption{Example of testing}
  \label{fig:testing.ex}
\end{figure}
An example is provided in Figure~\ref{fig:testing.ex}, where the test
$a.\eureka \probc{\frac{1}{4}} (b \extc c.\eureka)$ is applied to the
process $b\extc c\extc d$. We see that 25\% of the time the test is
unsuccessful, in that it does not reach a state where $\eureka$ is
possible, and 75\% of the time it \emph{may} be successful, depending
on how the now internal choice between the actions $b$ and $c$ is
resolved, but it is not the case that it \emph{must} be successful.

$\Op{T \parT P}$ is representable as a finite graph which encodes all
possible interactions of the test $T$ with the process $P$.  It only
contains the actions $\tau$ and $\omega$.  Each occurrence of $\tau$
represents a nondeterministic choice, either in $T$ or $P$ themselves,
or as a nondeterministic response by $P$ to a request from $T$, while
the distributions represent the resolution of underlying probabilities
in $T$ and $P$. We use the structure $\Op{T \parT P}$ to
define $\Apply(T,P)$, the non-empty finite subset of $[0,1]$ representing the
set of probabilities that applying $T$ to $P$ will be a success.

First we define a function $\results{\_\!\_}$, which when applied to any
state in $\pS$ returns a finite subset of $[0,1]$.  The definition
will require that it be also applied to distributions, and to do so we
need to use \emph{choice functions} for collecting elements from
subsets of $[0,1]$. Suppose $R: \pS \rightarrow \Fsubs{[0,1]}$, and
$c: X \rightarrow [0,1]$, where $X$ is a subset of $\pS$.  Then we
write
\begin{math}
  c \cfun{X} R
\end{math}
if $c(s) \inp R(s)$ for every $s$ in $X$, and
the results-collecting function can be defined as follows:
\begin{align*}
  \results{s} &~~~=~~~ 
  \begin{cases}
                 \sset{1} &\text{if $s \ar{\eureka}$}, \\
\bigcup \setof{\results{\Delta}}{s \ar{\tau} \Delta}
                     &\text{if $s \not\ar{~\;\eureka},\;s \ar{\tau}$},\\
                 \sset{0} &\text{otherwise}
  \end{cases}
\intertext{where}
 \results{\Delta} &~~~=~~~ \setof{ \sum_{s\in\support{\Delta}}\Delta(s)\cdot c(s)}
                     { \textstyle c  \cfun{\support{\Delta}} \resultsN }
\end{align*}
However, instead of the explicit use of
choice functions, we will tend to use the more convenient notation 
\begin{align*} 
   \results{\Delta}&~~~=~~~ \Delta(s_1) \cdot \results{s_1} + \ldots +
                    \Delta(s_n) \cdot \results{s_n}
\end{align*}
where $\support\Delta = \sset{s_1,\ldots s_n}$.
Note that $\results{\_\!\_}$ is indeed a well-defined function, because the pLTS 
$\langle \pS,\Act_\tau, \rightarrow \rangle$ is finitely branching and well-founded.

For example consider the transition systems in Figure~\ref{fig:results.ex},
\begin{figure}[t]
\vspace{-1ex}
  \begin{displaymath}
    \begin{array}{ccc}
 \pstree[nodesep=2pt,levelsep=30pt,labelsep=1pt]{\TR{\Delta_s}}
       {\pstree{\TR{s_1}   \tlput{\scriptscriptstyle{\frac{1}{2}}}}
            {\pstree{\Tdot \tlput{\tau}}{\pstree{\Tdot \tlput{\eureka}}{}}   
             \pstree{\Tdot \trput{\tau}}{} } 
         \pstree{\TR{s_2}   \trput{\scriptscriptstyle{\frac{1}{2}}}}
           {\pstree{\Tdot \tlput{\tau}}
               {\pstree{\Tdot \tlput{\eureka}}{}} }
       }
&\qquad\qquad\qquad
 \pstree[nodesep=2pt,levelsep=30pt,labelsep=1pt]{\TR{\Delta_t}}
       {\pstree{\TR{t_1}   \tlput{\scriptscriptstyle{\frac{1}{4}}}}
            {\pstree{\Tdot \tlput{\tau}}{\pstree{\Tdot \tlput{\eureka}}{}}   
             \pstree{\Tdot \trput{\tau}}{} } 
         \pstree{\TR{t_2}   \trput{\scriptscriptstyle{\frac{3}{4}}}}
           { \pstree{\Tdot \tlput{\tau}}{}
             \pstree{\Tdot \trput{\tau}}
               {\pstree{\Tdot \tlput{\eureka}}{}} }
       }
\\
\results{\Delta_s} = \sset{\frac{1}{2},\;1}
&\qquad\qquad\qquad
\results{\Delta_t} = \sset{0,\;\frac{1}{4},\;\frac{3}{4},\;1}
    \end{array}
  \end{displaymath}
  \caption{Collecting results}
  \label{fig:results.ex}
\end{figure}
where for reference we have labelled the nodes. Then $\results{s_1} = \sset{1,0}$
while $\results{s_2} = \sset{1}$, and therefore 
$\results{\Delta_s} = \frac{1}{2} \ocdot \sset{1,0} + \frac{1}{2} \ocdot \sset{1}$ which, since
there are only two possible choice functions 
$c \cfun{\support{\Delta_s}} \resultsN$, evaluates further to $ \sset{\frac{1}{2},1}$. Similarly 
$\results{t_1}\linebreak = \results{t_2} = \sset{0,1}$ and using the four choice functions
$c \cfun{\support{\Delta_t}} \resultsN$, the calculation of 
$\results{\Delta_t} = \frac{1}{4} \ocdot \sset{0,1}  + \frac{3}{4} \ocdot \sset{0,1}$ leads to
$\sset{0,\frac{1}{4},\frac{3}{4},1}$.

\begin{definition}
For any $P \inp$ \pCSP and $T\inp\Tests$ let 
$\Apply(T,P) = \results{\Op{T \mathbin{\parT} P}}$.
\end{definition}

\noindent
With this definition we now have two testing preorders for \pCSP, one based on
\emph{may} testing, $P \pMayleq Q$, and the other on \emph{must} testing, $P \pMustleq Q$.


\section{Counterexamples}\label{sec:examples}

We will see in this section that many of the standard testing axioms
are not valid in the presence of probabilistic choice. 
We also provide counterexamples for a few distributive laws
involving probabilistic choice that may appear plausible at first sight.
In all cases we establish a statement $P \notpMayeq Q$ by exhibiting a
test $T$ such that $\max(\Apply(T,P)) \neq \max(\Apply(T,Q))$ and
a statement $P \notpMusteq Q$ by exhibiting a test $T$ such that
$\min(\Apply(T,P)) \neq \min(\Apply(T,Q))$. In case
$\max(\Apply(T,P)) > \max(\Apply(T,Q))$ we find in particular that
$P \notpMayleq Q$, and in case $\min(\Apply(T,P)) > \min(\Apply(T,Q))$
we obtain $P \notpMustleq Q$.

\begin{example}\label{Q1}
The axiom $a.(P \probc{p} Q) = a.P \probc{p} a.Q$ is unsound.
\\[1ex]
\begin{figure}[t]
  \begin{displaymath}
    \begin{array}{cccc}
    \pstree[nodesep=0pt,levelsep=20pt,labelsep=.05]{\Tdot}
                {\pstree{\Tdot[dotstyle=o] \tlput{a} }
                  {\pstree{\Tdot \tlput{\scriptscriptstyle{\frac{1}{2}}}}
                      {\pstree{\Tdot \tlput{b}}{}}
                    \pstree{\Tdot \trput{\scriptscriptstyle{\frac{1}{2}}}}
                      {\pstree{\Tdot \trput{c}}{}}
                  }
                 }
&\qquad\qquad\qquad
    \pstree[nodesep=0pt,levelsep=20pt,labelsep=.05]{\Tdot[dotstyle=o]}
                {\pstree{\Tdot \tlput{\scriptscriptstyle{\frac{1}{2}}}}
                      {\pstree{\Tdot \tlput{a}}
                        {\pstree{\Tdot \tlput{b}}{}}}
                  \pstree{\Tdot \trput{\scriptscriptstyle{\frac{1}{2}}}}
                      {\pstree{\Tdot \trput{a}}
                         {\pstree{\Tdot \trput{c}}{}}}
                 }
&\qquad\qquad\qquad
    \pstree[nodesep=0pt,levelsep=20pt,labelsep=.05]{\Tdot}
                {\pstree{\Tdot \tlput{\tau}}
                      {\pstree{\Tdot \tlput{a}}
                        {\pstree{\Tdot \tlput{b}}
                             {\pstree{\Tdot \tlput{\eureka}}{}}}}
                  \pstree{\Tdot \trput{\tau}}
                      {\pstree{\Tdot \trput{a}}
                         {\pstree{\Tdot \trput{c}}
                            {\pstree{\Tdot \trput{\eureka}}{}}}}
                 }
\\
R_1 = a.(b \probc{\frac{1}{2}} c)
&\qquad\qquad\qquad
R_2 = a.b \probc{\frac{1}{2}} a.c
&\qquad\qquad\qquad
T = a.b.\eureka \intc a.c.\omega                 
    \end{array}
  \end{displaymath}

  \begin{displaymath}
    \begin{array}{cc}
    \pstree[nodesep=0pt,levelsep=20pt,labelsep=.05]{\Tdot}
                {\pstree{\Tdot \tlput{\tau}}
                      {\pstree{\Tdot[dotstyle=o] \tlput{\tau}}
                         {\pstree{\Tdot \tlput{\scriptscriptstyle{\frac{1}{2}}}}
                        {\pstree{\Tdot \tlput{\tau}}
                            {\pstree{\Tdot \tlput{\eureka}}{}}}
                          \pstree{\Tdot \trput{\scriptscriptstyle{\frac{1}{2}}}}{}
                      }}
                 \pstree{\Tdot \trput{\tau}}
                      {\pstree{\Tdot[dotstyle=o] \tlput{\tau}}
                         {\pstree{\Tdot \tlput{\scriptscriptstyle{\frac{1}{2}}}}{}
                          \pstree{\Tdot \trput{\scriptscriptstyle{\frac{1}{2}}}}
                        {\pstree{\Tdot \trput{\tau}}
                            {\pstree{\Tdot \trput{\eureka}}{}}}
                      }}
                 }
&\qquad\qquad\qquad
    \pstree[nodesep=0pt,levelsep=20pt,labelsep=.05]{\Tdot[dotstyle=o]}
                {\pstree{\Tdot \tlput[tpos=.4]{\scriptscriptstyle{\frac{1}{2}}}}
                      {\pstree{\Tdot \tlput{\tau}}
                        {\pstree{\Tdot \tlput{\tau}}
                            {\pstree{\Tdot \tlput{\tau}}
                                 {\pstree{\Tdot \tlput{\eureka}}{}}}}
                          \pstree{\Tdot \trput{\tau}}
                               {\pstree{\Tdot \tlput{\tau}}{}}
                      }
                \pstree{\Tdot \trput[tpos=.4]{\scriptscriptstyle{\frac{1}{2}}}}
                      {\pstree{\Tdot \tlput{\tau}}
                        {\pstree{\Tdot \tlput{\tau}}{}}
                          \pstree{\Tdot \trput{\tau}}
                               {\pstree{\Tdot \trput{\tau}}
                            {\pstree{\Tdot \trput{\tau}}
                                 {\pstree{\Tdot \trput{\eureka}}{}}}}
                      }
                 }
\\
T \parT R_1 
&\qquad\qquad\qquad
T \parT R_2 \\
\Apply(T,R_1) = \sset{\frac{1}{2}}
&\qquad\qquad\qquad
\Apply(T,R_2) = \sset{0,\frac{1}{2},1}\\
    \end{array}
  \end{displaymath}
  \caption{Counterexample: action prefix does not distribute over probabilistic choice}
  \label{fig:ex.probc}
\vspace{1em}
\end{figure}
Consider the example in Figure~\ref{fig:ex.probc}. In $R_1$ the
probabilistic choice between $b$ and $c$ is taken after the action
$a$, while in $R_2$ the choice is made before the action has happened.
These processes can be distinguished by the nondeterministic test $T =
a.b.\eureka \intc a.c.\omega$. First consider running this test on $R_1$.
There is an immediate choice made by the test, effectively running
either the test $a.b.\eureka$ on $R_1$ or the test $a.c. \eureka$; in
fact the effect of running either test is exactly the same. Consider
$a.b.\eureka$. When run on $R_1$ the $a$ action immediately happens, and
there is a probabilistic choice between running $b.\eureka$ on either 
$b$ or $c$, giving as possible results $\sset{1}$ or $\sset{0}$;
combining these according to the definition of the function $\results{\_\!\_}$ we get
$\frac{1}{2} \ocdot \sset{0} + \frac{1}{2} \ocdot \sset{1} = \sset{\frac{1}{2}}$.
Since running the test $a.c.\eureka$ has the same effect, $\Apply(T,R_1)$
turns out to be the same set $\sset{\frac{1}{2}}$.

Now consider running the test $T$ on $R_2$. Because $R_2$, and hence
also $T \parT R_2$, starts with a probabilistic choice, due to the
definition of the function $\results{\_\!\_}$, the test must first
be applied to the probabilistic components, $a.b$ and $a.c$,
respectively, and the results subsequently combined
probabilistically. When the test is run on $a.b$, immediately a
nondeterministic choice is made in the test, to run either
$a.b.\eureka$ or $a.c.\eureka$. With the former we get the result
$\sset{1}$, with the latter $\sset{0}$, so overall, for running $T$ on
$a.b$, we get the possible results $\sset{0,1}$.  The same is true when
we run it on $a.c$, and therefore $\Apply(T,R_2) = \frac{1}{2}
\ocdot \sset{0,1} + \frac{1}{2} \ocdot \sset{0,1} = \sset{0,\frac{1}{2},1}$.

So we have $R_2 \notpMayleq R_1$ and $R_1 \notpMustleq R_2$.
\end{example}

\begin{figure}[t]
$$
 \begin{array}{ccc}
 \pstree[nodesep=0pt,levelsep=20pt,labelsep=.05]{\Tdot}
  {  \pstree{\Tdot \tlput{a}}
      {\pstree{{\Tdot}\tlput{\tau}}
            {\Tdot\tlput{b}}
     \pstree{\Tdot\trput{\tau}}
           {\Tdot\trput{c}}
   }
 }
&\qquad\qquad\qquad
 \pstree[nodesep=0pt,levelsep=20pt,labelsep=.05]{\Tdot}
  {  \pstree{\Tdot \tlput{\tau}}
      {\pstree{{\Tdot}\tlput{a}}
            {\Tdot\tlput{b}}
      }
 \pstree{\Tdot \trput{\tau}}
     {\pstree{\Tdot\trput{a}}
           {\Tdot\trput{c}}
     }
 } 
&\qquad\qquad\qquad
    \pstree[nodesep=0pt,levelsep=20pt,labelsep=.05]{\Tdot}
                {\pstree{\Tdot[dotstyle=o] \tlput{a} }
                  {\pstree{\Tdot \tlput{\scriptscriptstyle{\frac{1}{2}}}}
                      {\pstree{\Tdot \tlput{b}}{\pstree{\Tdot \tlput{\eureka}}{}}}
                    \pstree{\Tdot \trput{\scriptscriptstyle{\frac{1}{2}}}}
                      {\pstree{\Tdot \trput{c}}{\pstree{\Tdot \trput{\eureka}}{}}}
                  }
                 }
\\
R_1 = a.(b  \intc c)  
&\qquad\qquad\qquad
R_2 = a.b \intc a.c
&\qquad\qquad\qquad
T = a.(b.\eureka \probc{\frac{1}{2}} c.\eureka)
\end{array}
$$

\begin{displaymath}
  \begin{array}{cc}
    \pstree[nodesep=0pt,levelsep=20pt,labelsep=.05]{\Tdot}
         {\pstree{\Tdot[dotstyle=o] \tlput{\tau}}
          {\pstree{\Tdot \tlput[tpos=.4]{\scriptscriptstyle{\frac{1}{2}}}}
                      {\pstree{\Tdot \tlput{\tau}}
                          {\pstree{\Tdot \tlput{\tau}}{\pstree{\Tdot \tlput{\eureka}}{}}}
                        \pstree{\Tdot \trput{\tau}}{}
                       }
            \pstree{\Tdot \trput[tpos=.4]{\scriptscriptstyle{\frac{1}{2}}}}
                      {\pstree{\Tdot \tlput{\tau}}{}
                           \pstree{\Tdot \trput{\tau}}
                          {\pstree{\Tdot \trput{\tau}}{\pstree{\Tdot \trput{\eureka}}{}}}                            }       
           }}
&\qquad\qquad\qquad
    \pstree[nodesep=0pt,levelsep=20pt,labelsep=.05]{\Tdot}
        {\pstree{\Tdot \tlput{\tau}}
           {\pstree{\Tdot[dotstyle=o] \tlput{\tau}}
                      {\pstree{\Tdot \tlput{\scriptscriptstyle{\frac{1}{2}}}}
                          {\pstree{\Tdot \tlput{\tau}}{\pstree{\Tdot \tlput{\eureka}}{}}}
                        \pstree{\Tdot \trput{\scriptscriptstyle{\frac{1}{2}}}}{}
                       }}
        \pstree{\Tdot \trput{\tau}}
           {\pstree{\Tdot[dotstyle=o] \trput{\tau}}
                      {\pstree{\Tdot \tlput{\scriptscriptstyle{\frac{1}{2}}}}{}
                       \pstree{\Tdot \trput{\scriptscriptstyle{\frac{1}{2}}}}
                          {\pstree{\Tdot \trput{\tau}}{\pstree{\Tdot \trput{\eureka}}{}}}
                       }}
        }
\\
T \parT R_1 
&\qquad\qquad\qquad
T \parT R_2
\\
\Apply(T,R_1) = \sset{0,\frac{1}{2},1}
&\qquad\qquad\qquad
\Apply(T,R_2) = \sset{\frac{1}{2}}
  \end{array}
\end{displaymath}
  \caption{Counterexample: action prefix does not distribute over internal choice}
  \label{fig:ex.intc}
\vspace{1em}
\end{figure}
 
\begin{example}\label{ex:action over intc}
The axiom $a.(P \intc Q) = a.P \intc a.Q$ is unsound.
\\[1ex]
It is well known that this axiom
is valid in the standard theory of testing, for non-probabilistic
processes.  However, consider the instance $R_1$ and $R_2$ in
Figure~\ref{fig:ex.intc}, and note that these processes do not contain
any probabilistic choice. But they can be differentiated by the
probabilistic test $T = a.(b.\eureka \probc{\frac{1}{2}} c.\eureka)$; the
details are in Figure~\ref{fig:ex.intc}.
There is only one possible outcome from applying $T$ to $R_2$, the
probability $\frac{1}{2}$, because the nondeterministic choice is made
before the probabilistic choice. On the other hand when $T$ is applied
to $R_1$ there are three possible outcomes, $0,\;\frac{1}{2}$ and $1$,
because effectively the probabilistic choice takes precedence over the
nondeterministic choice.
So we have $R_1 \notpMayleq R_2$ and $R_2 \notpMustleq R_1$.
\end{example}

\begin{example}
The axiom $a.(P \extc Q)=a.P \extc a.Q$ is unsound.
\\[1ex]
This axiom is valid in the standard may-testing semantics.
However, consider the two processes
 $R_1 = a.(b \extc c)$, $R_2 = a.b \extc a.c$ and the probabilistic
test $T = a.(b.\eureka
\probc{\frac{1}{2}} c.\eureka)$. Now
$\Apply(T,R_1)=\sset{1}$ and \plat{$\Apply(T, R_2)=\sset{\frac{1}{2}}$}.
Therefore $R_1 \notpMayleq R_2$ and $R_1 \notpMustleq R_2$.
\end{example}

\begin{example}
The axiom $P = P \extc P$ is unsound.
\\[1ex]
Let $R_1,\ R_2$ denote
$(a \probc{\frac{1}{2}} b)$ and $(a \probc{\frac{1}{2}} b) \extc (a \probc{\frac{1}{2}} b)$,
respectively. It is easy to calculate that \plat{$\Apply(a.\eureka,R_1) =
\sset{\frac{1}{2}}$} but, because of the way we interpret external choice as an
operator over distributions of states in a pLTS, it turns out that
\mbox{$\Op{R_2} = \Op{((a \extc a) \probc{\frac{1}{2}} (a \extc b)) \probc{\frac{1}{2}}
((b \extc a) \probc{\frac{1}{2}} (b \extc b))}$} and so
\plat{$\Apply(a.\eureka,R_2) = \sset{\frac{3}{4}}$}.
Therefore $R_2\notpMayleq R_1$ and $R_2\notpMustleq R_1$.
\end{example} 

\begin{example}
The axiom $P \probc{p} (Q \intc R)= (P \probc{p} Q) \intc (P \probc{p}
R)$ is unsound.
\\[1ex]
Consider the processes $R_1 = a \probc{\frac{1}{2}} (b \intc c)$ and
$R_2 = (a \probc{\frac{1}{2}} b) \intc (a \probc{\frac{1}{2}} c)$, and
the test $T_1 = a.\eureka \intc (b.\eureka \probc{\frac{1}{2}} c.\eureka)$.
In the best of possible worlds, when we apply $T_1$ to $R_1$ we obtain
probability $1$, that is $\max(\Apply(T_1,R_1)) = 1$. Informally this
is because half the time when it is applied to the subprocess $a$ of
$R_1$, optimistically the sub-test $a.\eureka$ is actually run.  The
other half of the time, when it is applied to the subprocess $(b \intc c)$,
optimistically the sub-test $T_r = (b.\eureka \probc{\frac{1}{2}} c.\eureka)$
is actually used. And here again, optimistically, we obtain probability $1$:
whenever the test $b.\eureka$ is used it might be applied to the subprocess $b$,
while when $c.\eureka$ is used it might be applied to $c$.
Formally we have\pagebreak[2]
\begin{align*}
\Apply(T\!_1,R_1) &= \textstyle\frac{1}{2} \ocdot \Apply(T_1, a)  
                           + \frac{1}{2} \ocdot \Apply(T_1, b\intc c) \\
                &= \textstyle\frac{1}{2} \ocdot
                           (\Apply(a.\eureka,a)\cup \Apply(T_r,a))\;+\\
                &~ \textstyle\frac{1}{2}\!\ocdot\! (\Apply(T_1,b) \cup \Apply(T_1,c)
                    \cup \Apply(a.\eureka, b \mathop{\intc} c) \cup \Apply(T_r,b\mathop{\intc} c))\\
                &= \textstyle \frac{1}{2} \ocdot(\sset{1} \cup \sset{0}) +
                   \frac{1}{2} \ocdot (\sset{0,\frac{1}{2}} \cup \sset{0,\frac{1}{2}} 
                     \cup \sset{0} \cup \sset{0,\frac{1}{2},1}) \\
                &= \textstyle\sset{0,\frac{1}{4},\frac{1}{2},\frac{3}{4},1}
\end{align*}
However no matter how optimistic we are when applying $T_1$ to $R_2$
we can never get probability $1$; the most we can hope for is
$\frac{3}{4}$, which might occur when $T_1$ is applied to the
subprocess $(a \probc{\frac{1}{2}} b)$. Specifically when the
subprocess $a$ is being tested the sub-test $a.\eureka$ might be used,
giving probability $1$, and when the subprocess $b$ is being tested
the sub-test $(b.\eureka \probc{\frac{1}{2}} c.\eureka)$ might be
used, giving probability $\frac{1}{2}$.  We leave the reader to check
that formally
\begin{align*}
  \Apply(T_1,R_2) = \textstyle\sset{0,\frac{1}{4},\frac{1}{2},\frac{3}{4}}
\end{align*}
from which we can conclude $R_1 \notpMayleq R_2$.

We can also show that $R_2 \notpMustleq R_1$, using the test 
$$T_2 = (b.\eureka \extc c.\eureka) \intc (a.\eureka
\probc{\frac{1}{3}}(b.\eureka \probc{\frac{1}{2}} c.\eureka)).$$
Reasoning pessimistically, the worst that can happen when applying
$T_2$ to $R_1$ is we get probability $0$. Each time the subprocess $a$
is tested the worst probability will occur when the sub-test
$(b.\eureka \extc c.\eureka)$ is used; this results in probability
$0$. Similarly when the subprocess $(b \intc c)$ is being tested the
subtest $(a.\eureka \probc{\frac{1}{3}}(b.\eureka \probc{\frac{1}{2}}
c.\eureka))$ will give probability $0$. In other words
$\min(\Apply(T_2,R_1)) = 0$.  When applying $T_2$ to $R_2$, things can
never be as bad. The worst probability will occur when $T_2$ is
applied to the subprocess $(a \probc{\frac{1}{2}} b)$, namely
probability $\frac{1}{6}$.  We leave the reader to check that formally
$\Apply(T_2,R_1) = \textstyle\sset{0, \frac{1}{6}, \frac{1}{3},
\frac{1}{2}, \frac{2}{3}}$ and $\Apply(T_2,R_2) =
\textstyle\sset{\frac{1}{6}, \frac{1}{3}, \frac{1}{2}, \frac{2}{3}}$.
\end{example}

\begin{example}
The axiom $P \intc (Q \probc{p} R) = (P \intc Q) \probc{p} (P \intc
R)$ is unsound.
\\[1ex]
Let $R_1 = a \intc (b \probc{\frac{1}{2}} c)$, $R_2 = (a\intc b) \probc{\frac{1}{2}}
(a\intc c)$ and $T = a.(\eureka \probc{\frac{1}{2}} \Cnil) \extc
b.\eureka$. One can check that $\Apply(T,R_1) = \sset{\frac{1}{2}}$ and
$\Apply(T, R_2) = \frac{1}{2}\sset{\frac{1}{2},1} + \frac{1}{2}\sset{\frac{1}{2},0} =
\sset{\frac{1}{4}, \frac{1}{2}, \frac{3}{4}}$. Therefore we have
$R_2\notpMayleq R_1$ and $R_1\notpMustleq R_2$.
\end{example}  

\begin{example}
The axiom $P \extc (Q \intc R)= (P \extc Q) \intc (P \extc R)$ is unsound. 
\\[1ex]
Let $R_1 = (a \probc{\frac{1}{2}} b) \extc (c \intc d)$,
$R_2 = ((a \probc{\frac{1}{2}} b)\extc c) \intc ((a \probc{\frac{1}{2}} b)\extc
d)$ and $T=(a.\eureka\probc{\frac{1}{2}}c.\eureka) \intc (b.\eureka
\probc{\frac{1}{2}} d.\eureka)$. This time we get
$\Apply(T,R_1)=\sset{0,\frac{1}{4},\frac{1}{2}, \frac{3}{4},1}$ and 
$\Apply(T,R_2)=\sset{\frac{1}{4},\frac{3}{4}}$. So $R_1\notpMayleq
R_2$ and $R_2\notpMustleq R_1$.
\end{example}

\begin{example}\label{Q8}
The axiom $P \intc (Q \extc R)= (P \intc Q) \extc (P \intc R)$ is unsound.
\\[1ex]
Let $R_1 = (a \probc{\frac{1}{2}} b) \intc ((a \probc{\frac{1}{2}} b)
\mathop{\extc} \Cnil)$ and $R_2 = 
((a \probc{\frac{1}{2}} b) \intc (a \probc{\frac{1}{2}} b)) \extc ((a
\probc{\frac{1}{2}} b) \intc \Cnil)$.\\ One obtains
$\Apply(a.\eureka,R_1) =\sset{\frac{1}{2}}$ and 
$\Apply(a.\eureka,R_2) = \sset{\frac{1}{2},\frac{3}{4}}$.
So $R_2 \notpMayleq R_1$.  Let $R_3$ and $R_4$ result from
substituting $a \probc{\frac{1}{2}} b$ for each of $P$, $Q$ and $R$ in
the axiom above. Now $\Apply(a.\eureka,R_3) =\sset{\frac{1}{2},\frac{3}{4}}$
and $\Apply(a.\eureka,R_4) = \sset{\frac{3}{4}}$. So $R_4 \notpMustleq R_3$.
\end{example}

\begin{example}\label{JW}
The axiom $P \probc{p} (Q \extc R)= (P \probc{p} Q) \extc (P \probc{p}
R)$ is unsound.
\\[1ex]
Let $R_1 = a \probc{\frac{1}{2}} (b \extc c)$, $R_2 = (a \probc{\frac{1}{2}} b)
\extc (a \probc{\frac{1}{2}} c)$ and $R_3=(a \extc b) \probc{\frac{1}{2}} (a
\extc c)$.\linebreak[2]
$R_1$ is an instance of the left-hand side of the axiom, and
$R_2$ an instance of the right-hand side. Here we use $R_3$ as a tool to
reason about $R_2$, but in Section~\ref{Related Work} we need $R_3$ in its own right.
Note that $\Op{R_2} = \frac{1}{2}\cdot\Op{R_1} + \frac{1}{2}\cdot\Op{R_3}$.
Let $T = a.\eureka$. It is easy to see that $\Apply(T, R_1) = \sset{\frac{1}{2}}$
and $\Apply(T, R_3) = \sset{1}$. Therefore $\Apply(T, R_2) = \sset{\frac{3}{4}}$.
So we have $R_2 \notpMayleq R_1$ and $R_2 \notpMustleq R_1$.

Of all the examples in this section, this is the only one for
which we can show that $\pMayleq$ and $\sqsupseteq_{\text{pmay}}$ both
fail, i.e.\ both inequations that can be associated with the axiom are
unsound for \emph{may} testing.
Let $T=a.(\eureka \probc{\frac{1}{2}} \Cnil) \intc (b.\eureka
\probc{\frac{1}{2}} c.\eureka)$. It is not hard to check that
$\Apply(T,R_1)=\sset{0, \frac{1}{4}, \frac{1}{2}, \frac{3}{4}}$ and
$\Apply(T,R_3)=\sset{\frac{1}{2}}$. Thus
$\Apply(T,R_2)=\sset{\frac{1}{4}, \frac{3}{8}, \frac{1}{2}, \frac{5}{8}}$.
Therefore, we have $R_1\notpMayleq R_2$.

For future reference, we also observe that $R_1\notpMayleq R_3$ and
$R_3 \notpMayleq R_1$.
\end{example}


\section{Must versus may testing}

On \pCSP there are two differences between the preorders $\pMayleq$
and $\pMustleq$:
\begin{itemize}
\item Must testing is more discriminating
\item The preorders $\pMayleq$ and $\pMustleq$ are oriented in
  opposite directions.
\end{itemize}
In this section we substantiate these claims by proving that
$P \pMustleq Q$ implies $Q \pMayleq P$, and by providing a counterexample
that shows the implication is strict. We are only able to obtain the
implication since our language does not feature \emph{divergence},
infinite sequences of $\tau$-actions. It is well known from the
non-probabilistic theory of testing \cite{DNH84,henn} that in the
presence of divergence $\Mayeq$ and $\Musteq$ are incomparable.

To establish a relationship between must testing and may testing, we
define the context $C[\_\!\_]=\_\!\_\, \Par{\sset{\eureka}}(\eureka\extc (\nu\intc \nu))$ so
that for every test $T$ we obtain a new test $C[T]$, by considering
$\nu$ instead of $\eureka$ as success action.
\begin{lemma}\rm \label{l:ctest}
For any process $P$ and test $T$, it holds that
\begin{enumerate}
\item
if $p\inp \Apply(T,P)$ then $(1\mathord-p) \inp \Apply(C[T],P)$

\item 
if $p\inp \Apply(C[T],P)$ then there exists a $q\inp\Apply(T,P)$
such that $1\mathord-q\leq p$.
\end{enumerate}
\end{lemma}

\begin{proof}
A state of the form $C[s]\parT t$ can always do a $\tau$-move, and
never directly a success action $\nu$. The $\tau$-steps that $C[s]\parT t$
can do fall into three classes: the resulting distribution is either
\begin{itemize}
\item a point distribution $\pdist{v}$ with $v\ar{\nu}\,$; we call this
 a \emph{successful} $\tau$-step, because it contributes $1$ to the
 set $\results{C[s]\parT t}$
\item a point distribution $\pdist{u}$ with $u$ a state from which the
 success action $\nu$ is unreachable; we call this an
 \emph{unsuccessful} $\tau$-step, because it contributes $0$ to the
 set $\results{C[s]\parT t}$
\item or a distribution of form $C[\Theta] \parT \Delta$.
\end{itemize}
Note that
\begin{itemize}
\item $C[s]\parT t$ can always do a successful $\tau$-step
\item $C[s]\parT t$ can do an unsuccessful $\tau$-step iff
  $s \parT t$ can do a $\eureka$-step
\item and $C[s] \parT t \ar{\tau} C[\Theta] \parT \Delta$ iff
  $s \parT t \ar{\tau} \Theta \parT \Delta$.
\end{itemize}
Using this, both claims follow by a straightforward induction on $T$ and $P$.
\end{proof}

\begin{proposition}\rm
If $P \pMustleq Q$ then $Q \pMayleq P$.
\end{proposition}
\begin{proof}
Suppose $P \pMustleq Q$. We must show that,
for any test $T$, if $p\in\Apply(T,Q)$ then there exists a
$q\in\Apply(T,P)$ such that $p\leq q$.
So suppose $p\in\Apply(T,Q)$.
By the first clause of Lemma~\ref{l:ctest}, we have
$(1\mathord-p) \in \Apply(C[T],Q)$. Given that $P \pMustleq Q$, there must be an
$x\in\Apply(C[T],P)$ such that $x\leq 1\mathord-p$.
By the second clause of
Lemma~\ref{l:ctest}, there exists a $q\in\Apply(T,P)$ such that
$1\mathord-q \leq x$.
It follows that $p\leq q$. Therefore $Q \pMayleq P$.
\end{proof}

\begin{example}
To show that must testing is strictly more discriminating than may
testing consider the processes $a\extc b$ and $a\intc b$, and expose
them to test $a.\eureka$. It is not hard to see that
$\Apply(a.\eureka,a\extc b)=\{1\}$, whereas $\Apply(a.\eureka,a\intc
b)=\{0,1\}$.  Since $\min(\Apply(a.\eureka,a\extc b))=1$ and
$\min(\Apply(a.\eureka,a\intc b))=0$, using Proposition~\ref{min-max}
we obtain that $(a\extc b) \not\pMustleq (a\intc b)$.

Since $\max(\Apply(a.\eureka,a\extc b))=\max(\Apply(a.\eureka,a\intc
b))=1$, as a \emph{may} test, the test $a.\eureka$ does not
differentiate between $a\extc b$ and $a\intc b$.  In fact, we have
$(a\intc b)\pMayleq (a\extc b)$, and even $(a\extc b)\pMayeq (a\intc
b)$, but this cannot be shown so easily, as we would have to consider
all possible tests. In Section~\ref{sec:simulations} we will develop a
tool to prove statements $P \pMayleq Q$, and apply it to derive the
equality above (axiom \Ename{EI} in Figure~\ref{fig:equations}).
\end{example}

\section{Simulations}\label{sec:simulations}

The examples of Section~\ref{sec:examples} have been all negative, because
one can easily demonstrate an inequivalence between two processes by
exhibiting a test which distinguishes them in the appropriate manner.
A direct application of the definition of the testing preorders is
usually unsuitable for establishing positive results, as this involves
a universal quantification over all possible tests that can be applied.
To give positive results of the form $P \pMayleq Q$ (and similarly for
$P \pMustleq Q$) we need to come up with a preorder $\sqsubseteq_{\rm
finer}$ such that $(P \sqsubseteq_{\rm finer} Q) \Rightarrow (P
\pMayleq Q)$ and statements $P \sqsubseteq_{\rm finer} Q$ 
can be obtained by exhibiting a single witness.

In this section we report on investigations in this direction,
using \emph{simulations} as our witnesses. We confine ourselves to
\emph{may} testing, although similar results hold for \emph{must} testing.
The definitions are somewhat complicated by the fact that in a pLTS
transitions go from states to distributions; consequently if we are to
use sequences of transitions, or \emph{weak transitions} $\dar{a}$
which abstract from sequences of internal actions that might precede or follow the $a$-transition, then we need to generalise transitions
so that they go from distributions to distributions. We first develop
the mathematical machinery for doing this.

\subsection{Lifting relations}

Let $\mathord{\aRel} \subseteq S \mathop{\times} \dist{S}$ be a relation from states to distributions. We lift it to a relation $\mathord{\lift{\aRel}} \subseteq \dist{S}
\mathop{\times} \dist{S}$ by letting $\Delta_1 \lift{\aRel} \Delta_2$
whenever
\begin{enumerate}[(i)]
\item 
$\Delta_1 = \sum_{i\in I}{p_i \ocdot \pdist{s_i}}$, where
  $I$ is a finite index set and  $\sum_{i\in I}{p_i} = 1$
 
\item 
For each $i \inp I$ there is a distribution $\Phi_i$ such that
$s_i \aRel \Phi_i$

\item 
$\Delta_2 = \sum_{i \in I} {p_i \ocdot \Phi_i}$.
\end{enumerate}
An important point here is that in the decomposition (i) of $\Delta_1$
into $\sum_{i\in I}{p_i \ocdot \pdist{s_i}}$, the states $s_i$ are
\emph{not necessarily distinct}: that is, the decomposition is not in general unique. Thus when establishing the relationship
between $\Delta_1$ and $\Delta_2$, a given state $s$ in $\Delta_1$ may
play a number of different roles, and this is seen clearly if we apply this
definition to the action relations $\mathord{\ar{\mu}} \subseteq \pS
\mathop{\times} \dist{\pS}$ in the operational semantics of \pCSP.  We
obtain lifted relations between $\dist{\pS}$ and $\dist{\pS}$, which
to ease the notation we write as $\Delta_1 \ar{\mu} \Delta_2$; then, using \pCSP terms to represent
distributions, a simple instance of a transition between distributions
is given by
\begin{align*}
  (a.b \extc a.c) \probc{\frac{1}{2}} a.d  &~~~\ar{a}~~~ b \probc{\frac{1}{2}} d 
\end{align*}
But we also have 
\begin{align}\label{eq:amove}
  (a.b \extc a.c) \probc{\frac{1}{2}} a.d  &~~~\ar{a}~~~ (b \probc{\frac{1}{2}} c) \probc{\frac{1}{2}} d
\end{align}
because, viewed as a distribution, the term
$ (a.b \extc a.c) \probc{\frac{1}{2}} a.d$ may be re-written as
$((a.b  \extc a.c) \probc{\frac{1}{2}} (a.b  \extc a.c)) \;\probc{\frac{1}{2}}\; a.d$
representing the sum of point distributions
\begin{displaymath}\textstyle
  \frac{1}{4} \ocdot \pdist{(a.b \extc a.c)} 
+  \frac{1}{4} \ocdot \pdist{(a.b \extc a.c)} + \frac{1}{2} \ocdot \pdist{a.d}
\end{displaymath}
from which the move (\ref{eq:amove}) can easily be derived using the three moves
from states
\begin{align*}
  a.b \extc a.c \ar{a} \pdist{b} \qquad\qquad  a.b \extc a.c \ar{a} \pdist{c} \qquad\qquad 
    a.d \ar{a} \pdist{d}
\end{align*}
%
The lifting construction satisfies the following two useful properties,
whose proofs we leave to the reader.
\begin{proposition}\rm\label{prop:lifting}
Suppose $\mathord{\aRel}\subseteq S \mathop{\times} \dist{S}$ and  
 $\sum_{i\in I} p_i = 1$. Then we have
\begin{enumerate}[(i)]
\item 
$\Theta_i \lift{\aRel} \Delta_i$ implies
$(\sum_{i\in I}{p_i \ocdot \Theta_i}) \lift{\aRel} (\sum_{i\in I}{p_i \ocdot \Delta_i})$.

\item 
If 
$(\sum_{i\in I}{p_i \ocdot \Theta_i}) \lift{\aRel} \Delta$ then 
$\Delta = \sum_{i\in I}{p_i \ocdot \Delta_i}$  for some set of distributions
$\Delta_i$ such that $\Theta_i \lift{\aRel} \Delta_i$.
\hfill{$\Box$}
\end{enumerate}
\end{proposition}

\noindent
The lifting construction can also be used to define the concept of a
\emph{partial} internal move between distributions, one where part of
the distribution does an internal move and the remainder remains
unchanged. Write $s \hatar{\tau} \Delta$ if either $s \ar{\tau}
\Delta$ or $\Delta = \pdist{s}$.  This relation between states and
distributions can be lifted to one between distributions and
distributions, and again for notational convenience we use
\mbox{$\Delta_1 \hatar{\tau} \Delta_2$} to denote the lifted relation.
As an example, again using process terms to denote distributions, we
have
\begin{align*}
  (a \intc b) \probc{\frac{1}{2}} (a \intc c)
  \;\;\hatar{\tau}\;\; a \probc{\frac{1}{2}} (a\intc b \;\;\probc{\frac{1}{2}}\;\; c)
\end{align*}
This follows because as a distribution $ (a \intc b) \probc{\frac{1}{2}} (a
\intc c)$ may be written as
\begin{align*}\textstyle
  \frac{1}{4} \ocdot \pdist{(a \intc b)} +  \frac{1}{4} \ocdot \pdist{(a \intc b)} +  
\frac{1}{4} \ocdot \pdist{(a \intc c)} +  \frac{1}{4} \ocdot \pdist{(a \intc c)} 
\end{align*}
and we have the four moves from states to distributions:
\begin{align*}
  (a \intc b) &\hatar{\tau} \pdist{a} \qquad\qquad&
  (a \intc b) &\hatar{\tau} \pdist{(a \intc b)}\\
  (a \intc c) &\hatar{\tau} \pdist{a} \qquad\qquad&
  (a \intc c) &\hatar{\tau} \pdist{c}
\end{align*}


\subsection{The simulation preorder}

Following tradition it would be natural to define simulations as
relations between states in a pLTS \cite{JWL01,SL94}. However,
technically it is more convenient to use relations in $\pS
\leftrightarrow \dist{\pS}$. One reason may be understood through
the example in Figure~\ref{fig:ex.probc}. Although
in Example~\ref{Q1} we found that $R_2 \notpMayleq R_1$, we do
have $R_1 \pMayleq R_2$.
If we are to relate these processes via a simulation-like relation,
then the initial state of $R_1$ needs to be related
to the initial \emph{distribution} of $R_2$, containing the two states
$a.b$ and $a.c$. 

Our definition of simulation uses \emph{weak transitions}
\cite{ccs}, which have the standard definitions except that they now
apply to distributions, and $\ar{\hat\tau}$ is used instead of $\ar{\tau}$.
This reflects the understanding that if a distribution may perform a
sequence of internal moves before or after executing a visible action,
different parts of the distribution may perform different numbers of
internal actions:
\begin{itemize}
\item Let $\Delta_1 \dar{\hat\tau} \Delta_2$ whenever $\Delta_1
  \ar{\hat{\tau}}^* \Delta_2$.
\item Similarly $\Delta_1 \dar{\hat{a}} \Delta_2$ denotes 
$\Delta_1 \ar{\hat{\tau}}^*\, \ar{a} \,\ar{\hat{\tau}}^* \Delta_2$
  whenever $a\in \Act$.
\end{itemize}

\begin{definition}\cite{Seg95}\label{def:forsim}
A relation $\mathord{\aRel} \subseteq \pS \mathop{\times} \dist{\pS}$ is 
said to be a \emph{simulation} if for all $s,\Delta,\mu,\Theta$ we
have that $s \aRel \Delta$ and $s \ar{\mu}  \Theta$ implies
there exists some $\Delta'$ with $\Delta \dar{\hat{\mu}} \Delta'$
and $\Theta \lift{\aRel} \Delta'$.
\end{definition}

\noindent
We write $s \forsim \Delta$ to mean that there is some simulation
$\aRel$ such that $s \aRel \Delta$. Note that the lifting operation on
relations is \emph{monotone}, in the sense that $\cal R \subseteq S$
implies $\mathord{\cal\lift{R}} \subseteq \mathord{\lift{S}}$.
Hence $\forsim$, which is the union of all simulations, is a
simulation itself. Therefore, $\forsim$ could just as well have been
defined co-inductively as the largest relation $\mathord{\forsim}
\subseteq \pS \mathop{\times} \dist{\pS}$  satisfying, for all $s\inp
\pS$, $\Delta \inp \dist{\pS}$ and $\alpha\in \Act_\tau$,\vspace{-1ex}
$$s \aRel \Delta \wedge s \ar{\mu}  \Theta ~\Rightarrow~ \exists \Delta'.\,
\Delta \dar{\hat{\mu}} \Delta' \wedge \Theta \lift{\aRel} \Delta'$$
\vspace{-2.5em}
\begin{definition}\label{df-simulation preorder}
The \emph{simulation preorder} on process terms is defined
by letting $P \simpreo Q$ whenever there is a distribution $\Delta$ with
$\Op{Q}\dar{\hat{\tau}}\Delta$ and $\Op{P} \liftforsim \Delta$.
The symmetric closure of $\simpreo$ is denoted $\simequiv$.
\end{definition}

\begin{figure}[t]
\vspace{-1em}
  \begin{displaymath}
    \begin{array}{ccc}
           \pstree[nodesep=2pt,levelsep=30pt,labelsep=1pt]{\TR{s_0}}
              {\pstree{\TR{\Delta_1} \tlput{a}}
                  {\pstree{\TR{s_1} \tlput{\scriptscriptstyle{\frac{1}{2}}}}
                     {\pstree{\Tdot\tlput{b}}{}}
                   \pstree{\TR{s_2} \trput{\scriptscriptstyle{\frac{1}{4}}}}
                     {\pstree{\Tdot\tlput{c}}{}}
                    \pstree{\TR{s_3} \trput{\scriptscriptstyle{\frac{1}{4}}}}
                     {\pstree{\Tdot\tlput{c}}{}}
                  }
             }
&\qquad\qquad\qquad
 \pstree[nodesep=2pt,levelsep=30pt,labelsep=1pt]{\TR{t_0}}
              {\pstree{\TR{\Delta_2} \tlput{a}}
                  {\pstree{\TR{t_1} \tlput{\scriptscriptstyle{\frac{1}{4}}}}
                     {\pstree{\Tdot\tlput{b}}{}}
                   \pstree{\TR{t_2} \trput{\scriptscriptstyle{\frac{1}{4}}}}
                     {\pstree{\Tdot\tlput{b}}{}}
                    \pstree{\TR{t_3} \trput{\scriptscriptstyle{\frac{1}{2}}}}
                     {\pstree{\Tdot\tlput{c}}{}}
                  }
             }
\\
P_1 = a.(b \probc{\frac{1}{2}} (c \probc{\frac{1}{2}} c)) 
&\qquad\qquad\qquad
P_2 = a.((b \probc{\frac{1}{2}} b)  \probc{\frac{1}{2}} c) 
    \end{array}
  \end{displaymath}

  \caption{Two simulation equivalent processes}\label{fig:sversusd}
  
\end{figure}

\noindent
If $P\in \pS$, that is if $P$ is a state in the pLTS of \pCSP and so $\Op{P}=\pdist{P}$, then to
establish $P \simpreo Q$ it is sufficient to exhibit a simulation
between the state $P$ and the distribution $\Op{Q}$, because
trivially $s \forsim \Delta$ implies $\pdist{s} \liftforsim
\Delta$.
\begin{example}\label{ex:one}
Consider the two processes $P_i$ in Figure~\ref{fig:sversusd}. 
To show $P_1 \simpreo P_2$ it is sufficient to exhibit a simulation
$\aRel$ such that $s_0 \aRel \pdist{t_0}$.
Let $\mathord{\aRel} \subseteq \pS \mathop{\times} \dist{\pS}$ be defined by
  \begin{align*}
    s_0   ~\aRel~ \pdist{t_0} \qquad
   s_1   ~\aRel~ \Delta_t  \qquad
   s_2  ~\aRel~ \pdist{t_3}  \qquad
   s_3  ~\aRel~ \pdist{t_3}  \qquad
   \Cnil ~\aRel~ \pdist{\Cnil}
  \end{align*}
where $\Delta_t$ is the two-point distribution mapping both $t_1$ and $t_2$ to the
probability $\frac{1}{2}$. Then it is straightforward to check that it satisfies the requirements
of a simulation: the only non-trivial requirement is that $\Delta_1 \lift{\aRel} \Delta_2$.
But this follows from the fact that\vspace{-1em}
\begin{align*}
  \Delta_1  &~~~=~~~\textstyle \frac{1}{2} \ocdot \pdist{s_1} + \frac{1}{4} \ocdot \pdist{s_2} + \frac{1}{4} \ocdot \pdist{s_3}\\
  \Delta_2  &~~~=~~~\textstyle \frac{1}{2} \ocdot \Delta_t + \frac{1}{4} \ocdot \pdist{t_3} + \frac{1}{4} \ocdot \pdist{t_3}
\end{align*}
As another example reconsider $R_1 = a.(b \probc{\frac{1}{2}} c)$ and $R_2 = a.b
\probc{\frac{1}{2}} a.c$ from
Figure~\ref{fig:ex.probc}, where for convenience we use process terms to denote their
semantic interpretations. It is easy to see that $R_1 \simpreo R_2$ because of the
simulation
\begin{align*}
  R_1 ~\aRel~ \Op{R_2}
\qquad\qquad b ~\aRel~ \pdist{b}
\qquad\qquad c ~\aRel~ \pdist{c}
\qquad\qquad \Cnil ~\aRel~ \pdist{\Cnil}
\end{align*}
Namely $R_2 \ar{a} (b \probc{\frac{1}{2}} c)$
and $(b \probc{\frac{1}{2}} c) \lift\aRel (b \probc{\frac{1}{2}} c)$.

Similarly  
\begin{math}
  (a \probc{\frac{1}{2}} c) \intc (b \probc{\frac{1}{2}} c) \simpreo (a \intc b) \probc{\frac{1}{2}} c
\end{math}
because it is possible to find a simulation between the state 
$(a \probc{\frac{1}{2}} c) \intc (b \probc{\frac{1}{2}} c)$ and the distribution
$(a \intc b) \probc{\frac{1}{2}} c$. 
\end{example}
\noindent
In case $P\mathop{\not\in}\pS$, a statement $P \simpreo Q$ cannot
always be established by a simulation $\aRel$ such that $\Op{P}
\lift\aRel \Op{Q}$.

\begin{example}
Compare the processes $P = a\probc{\frac{1}{2}}b$ and $P\intc P$.
Note that $\Op{P}$ is the distribution \plat{$\frac{1}{2}\lift{a} + \frac{1}{2}\lift{b}$}
whereas $\Op{P \intc P}$ is the point distribution \plat{$\lift{P \intc P}$}.
The relation $\aRel$ given by
  \begin{align*}\textstyle
   (P \intc P)  ~\aRel~ (\frac{1}{2}\lift{a} + \frac{1}{2}\lift{b}) \qquad
   a ~\aRel~ \pdist{a} \qquad
   b ~\aRel~ \pdist{b} \qquad
   \Cnil ~\aRel~ \pdist{\Cnil}
  \end{align*}
is a simulation, because the $\tau$-step ${P \intc P}\ar{\tau}
(\frac{1}{2}\lift{a} + \frac{1}{2}\lift{b})$ can be matched by the
idle transition $(\frac{1}{2}\lift{a} + \frac{1}{2}\lift{b})
\dar{\hat\tau}(\frac{1}{2}\lift{a} + \frac{1}{2}\lift{b})$,
and we have $(\frac{1}{2}\lift{a} + \frac{1}{2}\lift{b})\lift\aRel
(\frac{1}{2}\lift{a} + \frac{1}{2}\lift{b})$.
Thus $(P \intc P) \forsim (\frac{1}{2}\lift{a} +
\frac{1}{2}\lift{b}) = \Op{P}$, hence $\mathord{\Op{P \intc P}}
\lift\forsim \Op{P}$, and therefore $\mathord{P \intc P} \simpreo P$.

This type of reasoning does not apply to the other direction.
Any simulation $\aRel$ with $(\frac{1}{2}\lift{a} +
\frac{1}{2}\lift{b}) \lift\aRel \mathord{\lift{P \intc P}}$ would have
to satisfy $a \aRel \mathord{\lift{P \intc P}}$ and $b \aRel \mathord{\lift{P \intc P}}$.
However, the move $a \ar{a}\Cnil$ cannot be matched by the process
$\lift{P \intc P}$, as the only transition the latter process can do
is $\lift{P \intc P} \ar{\tau} (\frac{1}{2}\lift{a} +
\frac{1}{2}\lift{b})$, and only half of that distribution can
match the $a$-move. Thus, no such simulation exists, and we
find $\mathord{\Op{P}} \not\lift\forsim \Op{P \intc P}$.
Nevertheless, we still have $\mathord{P} \simpreo P \intc P$.
Here, the transition $\dar{\hat\tau}$ from Definition~\ref{df-simulation preorder}
comes to the rescue. As $\Op{P \intc P} \dar{\hat\tau} \Op{P}$ and
$\Op{P} \lift\forsim \Op{P}$, we obtain $\mathord{P} \simpreo P \intc P$.
\end{example}

\noindent
Because of the asymmetric use of distributions in the definition of simulation it is not immediately
obvious that $\simpreo$ is actually a preorder (a reflexive and transitive
relation) and hence $\simequiv$ an equivalence relation.
In order to show this, we first need to establish some properties of $\forsim$.
\begin{lemma}\rm\label{lemma:fors.sum}
  Suppose $\sum_{i \in I} p_i = 1$ and $\Delta_i \dar{\hat \alpha} \Phi_i$
  for each $i \inp I$, with $I$ a finite index set. (Recall that
  $\sum_{i \in I}{p_i \ocdot \Delta_i}$ is only defined for finite $I$.) Then
    $$\sum_{i \in I}{p_i \ocdot \Delta_i} \;\dar{\hat \alpha}\;
       \sum_{i \in I}{p_i \ocdot \Phi_i}$$
\end{lemma}
\begin{proof}
We first prove the case $\alpha=\tau$. For each $i\inp I$ there is
a number $k_i$ such that
$\Delta_i=\Delta_{i0} \ar{\hat\tau} \Delta_{i1} \ar{\hat\tau} \Delta_{i2}
\ar{\hat\tau} \cdots \ar{\hat\tau} \Delta_{ik_i} = \Delta'_i$.
Let $k = \max\{k_i \mid i\inp I\}$, using that $I$ is finite.
Since we have $\Phi \ar{\hat\tau} \Phi$ for any $\Phi\inp\dist{S}$, we
can add spurious transitions to these sequences, until all $k_i$ equal $k$.
After this preparation the lemma follows by $k$ applications of
Proposition~\ref{prop:lifting}(i), taking $\ar{\hat\tau}$ for $\aRel$.

The case $\alpha\inp\Act$ now follows by one more application of
Proposition~\ref{prop:lifting}(i), this time with $\mathord{\aRel} =
\mathord{\ar{a}}$,
preceded and followed by an application of the case $\alpha=\tau$.
\end{proof}
\begin{lemma}\rm\label{lemma:dist.moves}
  Suppose $\Delta \liftforsim \Phi$ and $\Delta \ar{\mu} \Delta'$. Then 
  $\Phi \dar{\hat{\mu}} \Phi'$ for some $\Phi'$ such that $\Delta' \liftforsim \Phi'$.
\end{lemma}
\begin{proof}
  First $\Delta \liftforsim \Phi$ means that
  \begin{alignat}{3}\label{eq:1}
    \Delta &= \sum_{i \in I}{p_i \ocdot \pdist{s_i}},
     &\qquad
    s_i &\forsim \Phi_i,
     &\qquad
   \Phi &= \sum_{i \in I}{ p_i \ocdot \Phi_i} ~;
  \end{alignat}
also $\Delta \ar{\mu} \Delta'$ means
  \begin{alignat}{3}\label{eq:2}
    \Delta &= \sum_{j \in J}{q_j \ocdot \pdist{t_j}},
     &\qquad
    t_j &\ar{\mu} \Theta_j,
     &\qquad
   \Delta' &= \sum_{j \in J}{ q_j \ocdot \Theta_j} ~,
  \end{alignat}
and we can assume \emph{w.l.o.g.}\ that all the coefficients $p_i,q_j$ are non-zero.
Now define
\begin{math}
I_j = \setof{i \inp I}{s_i = t_j}
\end{math}
and
\begin{math}
J_i = \setof{j \inp J}{t_j = s_i},
 \end{math}
so that trivially
\begin{equation}\label{indices}
\{(i,j)\mid i\in I,~ j\inp J_i\} \qquad=\qquad \{(i,j)\mid j\in J,~ i\inp I_j\}
\end{equation}
and note that
\begin{alignat}{2}
  \label{eq:3}
  \Delta(s_i) &= \sum_{j \in J_i} q_j
&\qquad \text{and}\qquad
  \Delta(t_j) &= \sum_{i \in I_j} p_i
\end{alignat}
Because of (\ref{eq:3}) we have
\begin{align*}
  \Phi  = \sum_{i \in I}{ p_i \ocdot \Phi_i} 
       &= \sum_{i \in I} {p_i \ocdot \sum_{j \in J_i}{\frac{q_j}{\Delta(s_i)} \ocdot \Phi_i}}\\
       &= \sum_{i \in I} \sum_{j \in J_i} {\frac{p_i \ocdot q_j}{\Delta(s_i)} \ocdot \Phi_i}
\end{align*}
Now for each $j$ in $J_i$ we know that in fact $t_j=s_i$, and so from the
middle parts of (\ref{eq:1}) and (\ref{eq:2}) we obtain $\Phi_i \dar{\hat{\mu}}
\Phi_{ij}$ such that $\Theta_j \liftforsim \Phi_{ij}$.
Lemma~\ref{lemma:fors.sum} yields
\begin{align*}
  \Phi \dar{\hat{\mu}} \Phi' = \sum_{i \in I} \sum_{j \in J_i} 
         {\frac{p_i \ocdot q_j}{\Delta(s_i)} \ocdot \Phi_{ij}}
\end{align*}
where within the summations $s_i=t_j$, so that, using (\ref{indices}), $\Phi'$
can also be written as
\begin{align}\label{eq:4}
  \phantom{ \Phi \dar{\hat{\mu}} \Phi_i =}
   \sum_{j \in J} \sum_{i \in I_j} {\frac{p_i \ocdot q_j}{\Delta(t_j)} \ocdot \Phi_{ij}}
\end{align}
All that remains is to show that 
\begin{math}
  \Delta' \liftforsim \Phi',
\end{math}
which we do by manipulating $\Delta'$ so that it takes on a form
similar to that in (\ref{eq:4}):
\begin{align*}
   \Delta' &= \sum_{j \in J}{ q_j \ocdot \Theta_j} \\
           &= \sum_{j \in J} {q_j \ocdot \sum_{i \in I_j} {\frac{p_i}{\Delta(t_j)} \ocdot \Theta_j}}
              \qquad\text{using (\ref{eq:3}) again}\\
           &= \sum_{j \in J} \sum_{i \in I_j} {\frac{p_i\ocdot q_j}{\Delta(t_j)} \ocdot \Theta_j}
\end{align*}
Comparing this with (\ref{eq:4}) above we see that the required result, $\Delta' \liftforsim \Phi'$,
follows from an application of Proposition~\ref{prop:lifting}(i).
\end{proof}

\begin{lemma}\rm\label{lemma:dist.dmoves}
  Suppose $\Delta \liftforsim \Phi$ and $\Delta \dar{\hat{\mu}} \Delta'$. Then 
  $\Phi \dar{\hat{\mu}} \Phi'$ for some $\Phi'$ such that $\Delta' \liftforsim \Phi'$.
\end{lemma}
\begin{proof}
First we consider two claims
\begin{enumerate}[(i)]
\item 
If $\Delta \liftforsim \Phi$ and $\Delta \ar{\hat{\tau}} \Delta'$, then 
  $\Phi \dar{\hat{\tau}} \Phi'$ for some $\Phi'$ such that $\Delta' \liftforsim \Phi'$. 

\item
If $\Delta \liftforsim \Phi$ and $\Delta \dar{\hat{\tau}} \Delta'$, then 
  $\Phi \dar{\hat{\tau}} \Phi'$ for some $\Phi'$ such that $\Delta' \liftforsim \Phi'$. 
\end{enumerate}
The proof of claim (i) is similar to the proof of Lemma~\ref{lemma:dist.moves}.
Claim (ii) follows from claim (i) by induction on the length of the derivation of $\dar{\hat{\tau}}$.
By combining claim~(ii) with Lemma~\ref{lemma:dist.moves}, we obtain the required result.
\end{proof}
  
\begin{proposition}\label{p2015}\rm
  The relation $\liftforsim$ is both reflexive and transitive on distributions.
\end{proposition}
\begin{proof}
  We leave reflexivity to the reader; it relies on the fact that $s \forsim \pdist{s}$ for every state
  $s$. 

For transitivity, let $\mathord{\aRel} \subseteq \pS \mathop{\times}
\dist{\pS}$ be given by $s \aRel \Phi$ iff $s \forsim \Delta \liftforsim \Phi$
for some intermediate distribution $\Delta$. Transitivity follows from the two claims
\begin{enumerate}[(i)]
\item $\Theta \liftforsim \Delta \liftforsim \Phi$
implies $\Theta \lift{\aRel} \Phi$

\item $\aRel$ is a simulation, hence ${\lift{\aRel}}\subseteq{\liftforsim}$.
\end{enumerate}
Claim (ii) is a straightforward application of Lemma~\ref{lemma:dist.dmoves}, so let us
look at (i).
From $\Theta \liftforsim \Delta$ we have
 \begin{alignat*}{3}
    \Theta &= \sum_{i \in I}{p_i \ocdot \pdist{s_i}},
     &\qquad
    s_i &\forsim \Delta_i,
     &\qquad
   \Delta &= \sum_{i \in I}{ p_i \ocdot \Delta_i}
  \end{alignat*}
Since $\Delta \liftforsim \Phi$, from  part (ii) of Proposition~\ref{prop:lifting} we know
\begin{math}
  \Phi = \sum_{i\in I}{p_i \ocdot \Phi_i}
\end{math}
such that $\Delta_i \liftforsim \Phi_i$. 
So for each $i$ we have $s_i \aRel \Phi_i$, from which it follows that
$\Theta \lift{\aRel} \Phi$.
\end{proof}

\begin{corollary}\rm\label{preorder}
$\simpreo$ is a preorder, i.e.\ it is reflexive and transitive.
\end{corollary}
\begin{proof}
By combination of Lemma~\ref{lemma:dist.dmoves} and Proposition~\ref{p2015}.
\end{proof}

\subsection{The simulation preorder is a precongruence}

In Theorem~\ref{thm:cong} of this section we establish that the \pCSP operators
are monotone w.r.t.\ the simulation preorder $\simpreo$, i.e.\ that $\simpreo$
is a precongruence for \pCSP.  This implies that the \pCSP operators are
compositional for $\simequiv$ or, equivalently, that $\simequiv$ is a congruence
for \pCSP.
The following two lemmas gather some facts we need in the proof of this
theorem. Their proofs are straightforward, although somewhat tedious.
\vspace{1pt}

\begin{lemma}\rm\label{choice moves}
\begin{enumerate}[(i)]
\item
If $\Phi \dar{\hat\tau} \Phi'$ then
$\Phi \extc \Delta \dar{\hat\tau} \Phi'\extc \Delta$ and
$\Delta \extc \Phi \dar{\hat\tau} \Delta \extc \Phi'$.

\item
If $\Phi \ar{a} \Phi'$ then
$\Phi \extc \Delta \ar{a} \Phi'$ and
$\Delta\extc\Phi \ar{a} \Phi'$.

\item
$(\sum_{j\in J}p_j\cdot\Phi_j) \extc (\sum_{k\in K}q_k\cdot\Delta_k) ~=~
 \sum_{j\in J}\sum_{k\in K}(p_j\cdot q_k)\cdot(\Phi_j \extc \Delta_k)$.

\item 
Given relations $\mathord{\aRel},\mathord{\aRel'} \subseteq \pS
\mathop{\times} \dist{\pS}$ satisfying $s{\aRel'}\Delta$ whenever
$s=s_1\extc s_2$ and $\Delta=\Delta_1\extc \Delta_2$ with
$s_1\aRel\Delta_1$ and $s_2\aRel\Delta_2$. Then $\Phi_i
\lift{\aRel}\Delta_i$ for $i=1,2$ implies $(\Phi_1\extc\Phi_2)
\lift{\aRel'} (\Delta_1\extc\Delta_2)$.  \hfill$\Box$
\end{enumerate}
\end{lemma}

\begin{lemma}\rm\label{l:par.move}
\begin{enumerate}[(i)]
\item
If $\Phi \dar{\hat\tau} \Phi'$ then
$\Phi \Par{A} \Delta \dar{\hat\tau} \Phi'\Par{A} \Delta$ and
$\Delta \Par{A} \Phi \dar{\hat\tau} \Delta \Par{A} \Phi'$.

\item
If $\Phi \ar{a} \Phi'$ and $a\not\in A$ then
$\Phi \Par{A} \Delta \ar{a} \Phi' \Par{A} \Delta$ and
$\Delta\Par{A}\Phi \ar{a} \Delta \Par{A} \Phi'$.

\item
If $\Phi \ar{a} \Phi'$, $\Delta \ar{a} \Delta'$ and $a\in A$ then 
$\Delta\Par{A}\Phi \ar{\tau} \Delta' \Par{A} \Phi'$. 

\item
$(\sum_{j\in J}p_j\cdot\Phi_j) \Par{A} (\sum_{k\in K}q_k\cdot\Delta_k) =
 \sum_{j\in J}\sum_{k\in K}(p_j\cdot q_k)\cdot(\Phi_j \Par{A} \Delta_k)$.

\item 
Given relations $\mathord{\aRel},\mathord{\aRel'} \subseteq \pS
\mathop{\times} \dist{\pS}$ satisfying $s{\aRel'}\Delta$ whenever
$s=s_1\Par{A} s_2$ and $\Delta=\Delta_1\Par{A} \Delta_2$ with
$s_1\aRel\Delta_1$ and $s_2\aRel\Delta_2$. Then $\Phi_i
\lift{\aRel}\Delta_i$ for $i=1,2$ implies $(\Phi_1\Par{A}\Phi_2)
\lift{\aRel'} (\Delta_1\Par{A}\Delta_2)$.\hfill$\Box$
\end{enumerate}
\end{lemma}

\begin{theorem}\rm\label{thm:cong}
  Suppose $P_i \simpreo Q_i$ for $i = 1,2$. Then
  \begin{enumerate}
  \item 
  $a.P_1 \simpreo a.Q_1$

  \item 
  $P_1 \intc P_2 \simpreo Q_1 \intc Q_2$

 \item 
 $P_1 \extc P_2 \simpreo Q_1 \extc Q_2$

\item 
 $P_1 \probc{p} P_2 \simpreo Q_1 \probc{p} Q_2$

\item
 $P_1 \Par{A} P_2 \simpreo Q_1 \Par{A} Q_2$
  \end{enumerate}
\end{theorem}
\vspace{3pt}
\noindent
{\bf Proof.}
\begin{enumerate}
\item
Since $P_1 \simpreo Q_1$, there must be a $\Delta_1$ such that $\Op{Q_1}
\dar{\hat\tau} \Delta_1$ and $\Op{P_1} \liftforsim \Delta_1$. It is
easy to see that $a.P_1 \forsim \pdist{a.Q_1}$ because the transition
$a.P_1 \ar{a} 
 \Op{P_1}$ can be matched by $\pdist{a.Q_1} \ar{a} \Op{Q_1} \dar{\hat\tau}
 \Delta_1$. Thus $\Op{a.P_1}\,=\,\pdist{a.P_1} \,\liftforsim\, 
 \pdist{a.Q_1}\,=\,\Op{a.Q_1}$. 

\item
Since $P_i \simpreo Q_i$, there must be a $\Delta_i$ such that $\Op{Q_i}
\dar{\hat\tau} \Delta_i$ and $\Op{P_i} \liftforsim \Delta_i$. It is
easy to see that $P_1\intc P_2 \forsim \pdist{Q_1 \intc Q_2}$ because
the transition $P_1\intc P_2 \ar{\tau} 
 \Op{P_i}$, for $i=1$ or $i=2$,
  can be matched by $\pdist{Q_1 \intc Q_2} \ar{\tau} \Op{Q_i} \dar{\hat\tau}
 \Delta_i$. Thus $\Op{P_1 \intc P_2}\,=\,\pdist{P_1 \intc P_2} \,\liftforsim\, 
 \pdist{Q_1 \intc Q_2}\,=\,\Op{Q_1 \intc Q_2}$. 

\item
Let $\mathord{\aRel} \subseteq \pS \mathop{\times} \dist{\pS}$ be
defined by $s\aRel\Delta$ iff either $s\forsim\Delta$ or $s=s_1\extc s_2$
and $\Delta=\Delta_1\extc\Delta_2$ with $s_1\forsim\Delta_1$
and $s_2\forsim\Delta_2$. We show that $\aRel$ is a simulation.

Suppose $s_1\forsim\Delta_1$, $s_2\forsim\Delta_2$ and $s_1\extc
s_2\ar{a}\Theta$ with $a\inp\Act$. Then $s_i \ar{a}\Theta$ for $i=1$
or $i=2$. Thus $\Delta_i\dar{\hat a}\Delta$ for some $\Delta$ with
$\Theta \liftforsim \Delta$, and hence $\Theta \lift\aRel \Delta$.
By Lemma~\ref{choice moves} we have $\Delta_1 \extc \Delta_2 \dar{\hat a}\Delta$.

Now suppose $s_1\forsim\Delta_1$, $s_2\forsim\Delta_2$ and $s_1\extc
s_2 \ar{\tau}\Theta$. Then $s_1 \ar{\tau} \Phi$ and $\Theta = \Phi
\extc \pdist{s_2}$ or $s_2 \ar{\tau} \Phi$ and $\Theta =
\pdist{s_1} \extc \Phi$.  By symmetry we may
restrict attention to the first case.  Thus $\Delta_1\dar{\hat\tau}\Delta$
for some $\Delta$ with $\Phi \liftforsim \Delta$.
By Lemma~\ref{choice moves} we have
$(\Phi\extc \pdist{s_2}) \lift{\aRel}
(\Delta\extc\Delta_2)$ and $\Delta_1\extc \Delta_2
\dar{\hat\tau}\Delta\extc\Delta_2$. 

The case that $s \forsim \Delta$ is trivial,
so we have checked that $\aRel$ is a simulation indeed.
Using this, we proceed to show that $P_1 \extc P_2 \simpreo Q_1 \extc Q_2$.

Since $P_i \simpreo Q_i$, there must be a $\Delta_i$ such that $\Op{Q_i}
\dar{\hat\tau} \Delta_i$ and $\Op{P_i} \liftforsim \Delta_i$.
By Lemma~\ref{choice moves}, we have $\Op{P_1 \extc P_2} =
(\Op{P_1}\extc \Op{P_2})\lift{\aRel}
(\Delta_1 \extc \Delta_2)$. 
Therefore $\Op{P_1 \extc P_2} \liftforsim (\Delta_1 \extc \Delta_2)$.
By Lemma~\ref{choice moves} we also obtain $\Op{Q_1\extc Q_2} =\linebreak[2] \Op{Q_1} \extc \Op{Q_2}
\dar{\hat\tau}\Delta_1\extc\Op{Q_2}\dar{\hat\tau}\Delta_1\extc\Delta_2$,
 so the required result is established.
\item
Since $P_i \simpreo Q_i$, there must be a $\Delta_i$ such that $\Op{Q_i}
\dar{\hat\tau} \Delta_i$ and $\Op{P_i} \liftforsim \Delta_i$.
Thus $\Op{Q_1 \probc{p} Q_2} = p\ocdot\Op{Q_1} + (1\mathord{-}p)\ocdot\Op{Q_2}
~\dar{\hat\tau}~ p\ocdot\Delta_1 + (1\mathord-p) \ocdot\Delta_2$ by Lemma~\ref{lemma:fors.sum}\\
and $\Op{P_1 \probc{p} P_2} = p\ocdot\Op{P_1} + (1\mathord-p)\ocdot \Op{P_2}
 ~\liftforsim~ p\ocdot\Delta_1 + (1\mathord-p)\ocdot \Delta_2$ by Proposition~\ref{prop:lifting}(i).
Hence $P_1 \probc{p} P_2 \simpreo Q_1 \probc{p} Q_2$.

\item
Let $\mathord{\aRel} \subseteq \pS \mathop{\times} \dist{\pS}$ be
defined by $s\aRel\Delta$ iff $s=s_1\Par{A} s_2$
and $\Delta=\Delta_1\Par{A}\Delta_2$ with $s_1\forsim\Delta_1$
and $s_2\forsim\Delta_2$. We show that $\aRel$ is a simulation.
There are three cases to consider.

\begin{enumerate}
\item
Suppose $s_1\forsim\Delta_1$, $s_2\forsim\Delta_2$ and $s_1\Par{A}
s_2\ar{\mu}\Theta_1 \Par{A} \pdist{s_2}$ because of the transition
$s_1\ar{\mu}\Theta_1$ with $\mu\not\in A$.
Then $\Delta_1\dar{\hat\mu}\Delta'_1$ for some $\Delta'_1$ with
$\Theta_1 \liftforsim \Delta'_1$.
By Lemma~\ref{l:par.move} we have $\Delta_1 \Par{A} \Delta_2
\dar{\hat\mu}\Delta'_1 \Par{A} \Delta_2$ and also $(\Theta_1 \Par{A} \pdist{s_2})
~ \lift{\aRel} ~(\Delta'_1\Par{A} \Delta_2)$.

\item The symmetric case can be similarly analysed.

\item 
Suppose $s_1\forsim\Delta_1$, $s_2\forsim\Delta_2$ and $s_1\Par{A}
s_2 \ar{\tau}\Theta_1\Par{A}\Theta_2$ because of the transitions
$s_1 \ar{a} \Theta_1$ and $s_2\ar{a}\Theta_2$ with $a\in A$. 
Then for $i=1$ and $i=2$ we have 
$\Delta_i\dar{\hat{\tau}}\Delta'_i \ar{a} \Delta''_i
\dar{{\hat{\tau}}} \Delta'''_i$ 
for some $\Delta'_i,\Delta''_i, \Delta'''_i$ 
with $\Theta_1 \liftforsim \Delta'''_i$.
By Lemma~\ref{l:par.move} we have 
$\Delta_1\Par{A} \Delta_2 \dar{\hat\tau}\Delta'_1\Par{A}\Delta'_2
\ar{\tau}\Delta''_1 \Par{A} \Delta''_2
\dar{\hat\tau}\Delta'''_1\Par{A}\Delta'''_2$ and
$(\Theta_1\Par{A} \Theta_2) \lift{\aRel} (\Delta'''_1\Par{A}\Delta'''_2)$.  
\end{enumerate}
So we have checked that $\aRel$ is a simulation.

Since $P_i \simpreo Q_i$, there must be a $\Delta_i$ such that $\Op{Q_i}
\dar{\hat\tau} \Delta_i$ and $\Op{P_i} \liftforsim \Delta_i$.
By Lemma~\ref{l:par.move} we have $\Op{P_1 \Par{A}
  P_2}=(\Op{P_1}\Par{A}\Op{P_2})\lift{\aRel}(\Delta_1\Par{A}\Delta_2)$.
Therefore $\Op{P_1 \Par{A} P_2} \liftforsim (\Delta_1 \Par{A} \Delta_2)$.
By Lemma~\ref{l:par.move} we also obtain $\Op{Q_1\Par{A} Q_2} =\linebreak[2] \Op{Q_1} \Par{A} \Op{Q_2}
\dar{\hat\tau}\Delta_1\Par{A}\Op{Q_2}\dar{\hat\tau}\Delta_1\Par{A}\Delta_2$,
which had to be established.
\hfill$\Box$
\end{enumerate}


\subsection{Simulation is sound for may testing}

This section is devoted to the proof that $P \simpreo Q$ implies $P \pMayleq Q$.
It involves a slightly different method of analysing the transition systems
which result from applying a test to a process. Instead of collecting the set
of probabilities of success it calculates the maximum probability that
\emph{some} action can be performed.
Let $\textit{maxlive}: \pS \rightarrow [0,1]$ be defined by
\begin{align*}
  \maxlive{s} &= 
  \begin{cases}
1                     & \text{if $s \ar{a}$ for some $a \inp \Act^\eureka$}\\
\max( \setof{\maxlive{\Delta}}{s \ar{\tau} \Delta})\!
                      & \text{if $s \not\ar{~\,a}$ for all $a \inp \Act^\eureka$ and
                     $s \ar{\tau}$}\\
0 &\text{otherwise}
  \end{cases}\\
\intertext{where}
 \maxlive{\Delta} &= \sum_{s\in\support{\Delta}} \Delta(s) \cdot \maxlive{s}
\end{align*}
If $s \inp \pS$ only ever gives rise to the special action $\eureka$ then it is easy
to see that  $\maxlive{s} = \max(\results{s})$. Because of this fact the following 
result is straightforward:
\begin{proposition}\rm\label{prop:maxlive}
  $P \pMayleq Q$ if and only if for every test $T$ we have\\[1ex]
\mbox{}\hfill$\maxlive{\Op{T\parT P}} \leq \maxlive{\Op{T\parT Q}} $
\hfill $\Box$ 
\end{proposition}

\noindent
The main technical property we require of $\maxlive{\_\!\_}$ is that it does not
increase as $\tau$-transitions are performed:
\begin{lemma}\rm\label{l:tau}
  $\Delta_1 \ar{\hat{\tau}}^* \Delta_2$ implies $\maxlive{\Delta_1} \geq \maxlive{\Delta_2}$.
\end{lemma}
\begin{proof}
First we prove one special case:
\begin{equation}\label{e:simple}
\Delta_1 \ar{\hat{\tau}} \Delta_2 \mbox{ implies } \maxlive{\Delta_1} \geq
  \maxlive{\Delta_2}.
\end{equation}
We know from $\Delta_1 \ar{\hat{\tau}} \Delta_2$ that
\begin{equation}\label{e:lift}
    \Delta_1 = \sum_{i \in I}{p_i \cdot \pdist{s_i}},
     \qquad
    s_i \ar{\hat{\tau}} \Phi_i,
     \qquad
   \Delta_2 = \sum_{i \in I}{ p_i \cdot \Phi_i}
  \end{equation}
The second part of (\ref{e:lift}) means that (i) either
$\Phi_i=\overline{s_i}$ or (ii) $s_i\ar{\tau}\Phi_i$. In \mbox{case (i)} we have
$\maxlive{s_i} = \maxlive{\Phi_i}$; in case (ii) we know from 
the definition of $\maxlive{\_\!\_}$ that $\maxlive{s_i} \geq
\maxlive{\Phi_i}$.  
Therefore,
\[\begin{array}{rcl}
\maxlive{\Delta_1} & = & \sum_{i \in I} p_i \cdot \maxlive{s_i}\\
                   & \geq & \sum_{i \in I} p_i \cdot
                   \maxlive{\Phi_i}\\
                   & = & \maxlive{\Delta_2}
\end{array}\]
This completes the proof of (\ref{e:simple}), from which the general
case follows by transition induction.
\end{proof}

\noindent
This lemma is the main ingredient to the following result:
\begin{proposition}\rm\label{prop:maxlive.sim}
  Suppose $\aRel$ is a simulation. Then
  \begin{enumerate}[(i)]
  \item $s \aRel \Delta$ implies $\maxlive{s} \leq \maxlive{\Delta}$

  \item $\Theta \lift{\aRel} \Delta$ implies $\maxlive{\Theta} \leq \maxlive{\Delta}$.
  \end{enumerate}
\end{proposition}
\noindent
{\bf Proof}.\,
Given that the states of our pLTS are \pCSP expressions, there exists a
well-founded order on the combination of states in $\pS$ and distributions in
$\dist{\pS}$, such that $s \ar{\mu} \Delta$ implies that $s$ is larger than
$\Delta$, and any distribution is larger than the states in its support.
We prove (i) and (ii) by simultaneous induction on this order, applied to $s$
and $\Theta$.
\begin{description}
\item[(i)] We distinguish two cases.
\begin{itemize}
\item If $s \ar{a} \Theta$ for some action $a\in\Act$ and distribution
  $\Theta$, then $\maxlive{s}=1$. Since $s \aRel \Delta$, there
  exists $\Delta',\ \Delta''$ such that $\Delta \ar{\hat{\tau}}^* \Delta'
  \ar{a}\,\ar{\hat{\tau}}^*\Delta''$ and $\Theta \lift{\aRel} \Delta''$.
  By definition $\maxlive{\Delta'}=1$, and
  $\maxlive{\Delta}\geq\maxlive{\Delta'}$ by Lemma~\ref{l:tau}. Therefore, 
  $\maxlive{\Delta}=1=\maxlive{s}$.

\item If $s \ar{\tau} \Theta$, then $s \aRel \Delta$ implies the
  existence of some $\Delta_\Theta$ such that
  $\Delta\ar{\hat{\tau}}^*\Delta_\Theta$ and $\Theta \lift{\aRel}
  \Delta_\Theta$. By induction, using (ii), $\maxlive{\Theta} \leq \maxlive{\Delta_\Theta}$.
  Consequently, we have that
  \[\begin{array}{@{~~~~}rcll}
  \maxlive{s} & = & max(\sset{\maxlive{\Theta} ~|~ s \ar{\tau} \Theta})\\ 
              & \leq  & max(\sset{\maxlive{\Delta_\Theta} ~|~ s \ar{\tau}
              \Theta}) \\
              & \leq & max(\sset{\maxlive{\Delta} ~|~ s \ar{\tau}
              \Theta}) & \qquad\mbox{(by Lemma~\ref{l:tau})}\\
                 & = & \maxlive{\Delta} 
  \end{array}\] 
\end{itemize}  
\item[(ii)]  $\Theta \lift{\aRel} \Delta$ means
  \begin{alignat*}{3}
    \Theta &= \sum_{i \in I}{p_i \cdot \pdist{s_i}},
     &\qquad
    s_i &\aRel \Delta_i,
     &\qquad
   \Delta &= \sum_{i \in I}{ p_i \cdot \Delta_i}
  \end{alignat*}
~~~\,So we can derive that
\begin{center}\mbox{}\hfill
  $\begin{array}[b]{rcll}
  \maxlive{\Theta} & = & \sum_{i \in I} p_i \cdot \maxlive{s_i}\\
                 & \leq & \sum_{i \in I} p_i \cdot \maxlive{\Delta_i}
                 & \qquad\mbox{(by induction)}\\
                 & = & \maxlive{\Delta}
  \end{array}$\hfill$\Box$
\end{center}
\end{description}
We now have all of the ingredients to prove that showing $P \simpreo Q$ is
a sound method of establishing $P \pMayleq Q$.

\begin{theorem}\rm\label{thm:fwimpliespM} 
  $P \simpreo Q$ implies $P \pMayleq Q$.
\end{theorem}

\begin{proof}
Suppose $P \simpreo Q$.
Because of Proposition~\ref{prop:maxlive} it is sufficient to prove
$\maxlive{\Op{T\parT P}} \leq \maxlive{\Op{T\parT Q}} $ for an arbitrary test $T$.
Since $\simpreo$ is preserved by the parallel operator we have that 
$T \parT P \simpreo T \parT Q$. (Strictly speaking, since $\eureka$ is not actually 
allowed to appear in processes, here we can replace it in $T$ with a fresh action
$\nu\inp\Act$, and accordingly use $\Par{\Act\setminus \sset{\nu}}$ instead of 
$\parT$.) By definition $T \parT P \simpreo T \parT Q$ means that there
is a distribution $\Delta$ and a simulation $\aRel$ such that
$\Op{T \parT Q}\dar{\hat{\tau}} \Delta$ and $\Op{T \parT P} \lift{\aRel} \Delta$.
The result now follows from the second part of  
Proposition~\ref{prop:maxlive.sim} and Lemma~\ref{l:tau}.
\end{proof}

\subsection{Some properties of simulations}\label{sec:axioms}

Because of the co-inductive nature of the definition of simulations we
can begin to develop properties of the preorder $\simpreo$ on \pCSP
terms. By Theorem~\ref{thm:fwimpliespM}, any equation $P = Q$ or $P
\sqsubseteq Q$ that we show to be sound for $\simequiv$, respectively
$\simpreo$, is also sound for $\pMayeq$, respectively $\pMayleq$.
In section~\ref{sec:examples} we have seen that many of the equations true for standard testing
no longer apply to probabilistic processes. But some interesting identities can be salvaged.

\begin{figure}[p]
\vspace{-1.5em}
  \begin{displaymath}
    \begin{array}[t]{@{}lrl@{}}
      \Ename{I1}\hspace{2em}& P \intc P&= P\\
      \Ename{I2}            & P \intc Q&= Q \intc P\\
      \Ename{I3}            & (P \intc Q) \intc R&= P \intc (Q \intc R)\\
      \Ename{P1}            & P \probc{p} P&= P\\
      \Ename{P2}            & P \probc{p} Q&= Q \probc{1-p} P\\
      \Ename{P3}            & (P \probc{p} Q) \probc{q} R&= 
                       P \probc{p\ocdot q} (Q \probc{\frac{(1-p)\ocdot q}{1-p\ocdot q}} R)\\
      \Ename{E1}            & P \extc \Cnil&= P\\
      \Ename{E2}            & P \extc Q&= Q \extc P\\
      \Ename{E3}            & (P \extc Q) \extc R&= P \extc (Q \extc R)\\
      \Ename{EI}            & a.P \extc b.Q&= a.P \intc b.Q\\
      \Ename{D1}            & P \extc (Q \probc{p} R)&= (P \extc Q) \probc{p} (P \extc R)\\   
      \Ename{D2}            & a.P \extc (Q \intc R)&= (a.P \extc Q) \intc (a.P \extc R)\\
      \Ename{D3}            &P \extc Q&= (P_1 \extc Q) \intc (P_2 \extc Q) \intc (P \extc Q_1)
                                     \intc (P \extc Q_2),\\[-1.3ex]
                    & &  \qquad\qquad\qquad \text{provided $P = P_1
      \intc P_2,\;Q = Q_1 \intc Q_2$}\\ 
      \Ename{L1}            & P \Par{A} Q & = Q \Par{A} P\\
      \Ename{L2}            & \Cnil \Par{A} \Cnil & = \Cnil\\
      \Ename{L3}            & \Cnil \Par{A} a.P   & =
                             \left\{\begin{array}{ll}
                              a.(\Cnil \Par{A} P)\qquad & \text{if $a\mathop{\not\in} A$}\\
                              \Cnil               & \text{if $a\inp A$}
                             \end{array}\right.\\
      \Ename{L4}            & \Cnil \Par{A} (P\intc Q) & = (\Cnil
                               \Par{A} P)\intc (\Cnil \Par{A} Q)\\
      \Ename{L5}            & a.P\Par{A}b.Q &=
                              \left\{\begin{array}{ll}
                        \Cnil  & \text{if $a,b\inp A$ and $a\not=b$}\\
                        P\Par{A}Q & \text{if $a,b\inp A$ and $a=b$}\\
%               b.(a.P\Par{A}Q) & \text{if $a\inp A$ and $b\not\in A$}\\
                a.(P\Par{A}b.Q) & \text{if $a\mathop{\not\in} A$ and $b\inp A$}\\
                a.(P\Par{A}b.Q)\extc b.(a.P\Par{A}Q) & \text{if
      $a,b\mathop{\not\in} A$}
                             \end{array}\right.\\
      \Ename{L6}            & (P \intc Q) \Par{A}  a.R & =
                              \left\{\begin{array}{ll}
                 (P \Par{A} a.R) \intc (Q \Par{A} a.R) \intc
                 a.((P\intc Q) \Par{A}  R) & \text{if $a\mathop{\not\in} A$}\\
                 (P \Par{A} a.R) \intc (Q \Par{A} a.R) & \text{if $a\inp A$}
                              \end{array}\right.\\ 
         \Ename{L7}            & P \Par{A}  Q & = (P_1 \Par{A}  Q)
                 \intc (P_2 \Par{A}  Q) \intc (P \Par{A}  Q_1)
                 \intc (P \Par{A}  Q_2)\\[-1.3ex]
                    & &  \qquad\qquad\qquad \text{provided $P = P_1
      \intc P_2,\;Q = Q_1 \intc Q_2$} \\
         \Ename{L8}            & P \Par{A}  (Q \probc{p} R) & = (P
                 \Par{A}  Q) \probc{p} (P \Par{A}  R)
    \end{array}  
  \end{displaymath}


  \caption{Some equations}
  \label{fig:equations}
\end{figure}

\begin{proposition}\rm\label{prop:pcsp.eq}
  All the equations in Figure~\ref{fig:equations} are valid for $\simequiv$ over \pCSP.
\end{proposition}

\noindent
{\bf Proof.}
\begin{itemize}
\item
Case \Ename{I1}: It is clear that $P \simpreo P\intc P$ since
$\Op{P\intc P}=\pdist{P\intc P}\ar{\tau}\Op{P}$ and $\Op{P}\liftforsim
\Op{P}$. 
For the inverse direction, observe that $P\intc P \forsim \Op{P}$
because the transition $P\intc P\ar{\tau}\Op{P}$ is matched by
$\Op{P}\dar{\hat\tau}\Op{P}$. Therefore we have $\Op{P\intc
  P}=\pdist{P\intc P}~ \liftforsim ~\Op{P}$, thus $P\intc P\simpreo P$.

\item
Case \Ename{I3}: Think for the moment of $P \intc Q \intc R$ as the
ternary instance of a new auxiliary operator $\bigsqcap_{i\in I}P_i$
with $I$ a finite index set, whose operational semantics consists of
the transitions $\bigsqcap_{i\in I}P_i \ar{\tau} P_i$ for $i\inp I$.
Now we show $P \intc Q \intc R \pMayeq (P \intc Q) \intc R$, and the
proof of $P \intc Q \intc R \pMayeq P \intc (Q \intc R)$ goes likewise.

That $P \intc Q \intc R \forsim (P \intc Q) \intc R$ follows because
a move $\pdist{P\intc Q \intc R} \ar{\tau} P$ can be simulated by
a sequence of two $\tau$-steps from $\pdist{(P \intc Q) \intc R}$.
Conversely, that $(P \intc Q) \intc R \forsim P \intc Q \intc R$ follows because
the move $\pdist{(P\intc Q) \intc R} \ar{\tau} P \intc Q$ can be
simulated by the idle $\hat\tau$-move $P \intc Q \intc R \ar{\hat\tau}
P \intc Q \intc R$ and we have $P \intc Q \forsim P \intc Q \intc R$.
The latter follows because any outgoing transition of $P \intc Q$ is
also an outgoing transition of $P \intc Q \intc R$.

Given the above, and its obvious extension to the case $|I|>3$, it
doesn't matter how to add brackets to the right-hand sides of
\Ename{D3}, \Ename{L6} and \Ename{L7}; one can just as well think of these
right-hand sides as instances of $\bigsqcap_{i\in I}P_i$.

\item
Case \Ename{I2}: It can easily be verified that $\Op{P\intc Q}~\liftforsim
~ \Op{Q \intc P}$ because both sides of the equation have the same outgoing transitions.
Similarly for \Ename{D3}, \Ename{L2\mbox{--}4} and \Ename{L7}.

\item
Case \Ename{P1}: By definition we have $\Op{P\probc{p}P} =
\Op{P}$. Similarly for \Ename{P2} and \Ename{P3}.

\item 
Case \Ename{E1}: Recall that $\Cnil$ is  a deadlock state in $\pS$,
i.e. $\Cnil\not\ar{~\,\mu}$ for all $\mu\in\Act_\tau$. Let
$\mathord{\aRel} \subseteq \pS \mathop{\times} \dist{\pS}$ be
defined by $s\aRel\Delta$ iff either $\Delta = \pdist{s}$ or $s=t\extc
\Cnil$ and $\Delta= \pdist{t}$ for some $t\in \pS$. It can be checked
that $\aRel$ is a simulation.
Let $\Op{P} = \sum_{j\in J}p_j \ocdot \pdist{s_j}$. Then $\Op{P\extc\Cnil} =
\sum_{j\in J}p_j \ocdot \pdist{s_j\extc\Cnil}$, thus $\Op{P\extc\Cnil}
\lift{\aRel} \Op{P}$ and $\Op{P\extc\Cnil} \liftforsim
\Op{P}$. Therefore we have $P\extc\Cnil \simpreo P$. Similarly we can
prove $P\simpreo P\extc\Cnil$.

\item
Case \Ename{E2}: Let
$\mathord{\aRel} \subseteq \pS \mathop{\times} \dist{\pS}$ be
defined by $s\aRel\Delta$ iff either $\Delta = \pdist{s}$ or \mbox{$s=t_1\extc
t_2$} and $\Delta=\pdist{t_2\extc t_1}$ for some $t_1,t_2\in \pS$. 
It can be checked that $\aRel$ is a simulation. Now it is easy to
show that $\Op{P\extc Q} \liftforsim \Op{Q\extc P}$, thus $P\extc Q
\simpreo Q\extc P$. The proof of \Ename{L1} goes likewise.

\item
Case \Ename{E3}: Let
$\mathord{\aRel} \subseteq \pS \mathop{\times} \dist{\pS}$ be
defined by $s\aRel\Delta$ iff either
$s=(t_1\extc t_2)\extc t_3$ and $\Delta=\pdist{t_1 \extc(t_2\extc t_3)}$ for some
$t_1,t_2,t_3\in \pS$ or $\Delta =\pdist{s}$.  
It can be checked that $\aRel$ is a simulation. Again it is easy to
show that $\Op{(P\extc Q)\extc R} \liftforsim \Op{P\extc(Q\extc R)}$,
hence $(P\extc Q)\extc R \simpreo P\extc(Q\extc R)$.
The other direction goes likewise.
 
\item
Case \Ename{EI}: Let $R_1$ and $R_2$ be the processes on the left and
right hand side of the equation. 
It can be checked that both $\Op{R_1} \liftforsim \Op{R_2}$ and
$\Op{R_2} \liftforsim \Op{R_1}$ hold.
In particular, the $\tau$-move from $R_2$ to $a.P$ can be simulated by
the idle move $R_1 \dar{\hat\tau} R_1$, since we also have $\Op{a.P} \liftforsim \Op{R_1}$.
Similarly for \Ename{L6}.

\item
Case \Ename{D1}: $\Op{P\extc (Q\probc{p}R)} = \Op{P}\extc
(p\ocdot\Op{Q}+(1-p)\ocdot\Op{R}) = p\ocdot(\Op{P}\extc\Op{Q})
+\linebreak[2]  (1-p)\ocdot(\Op{P}\extc\Op{R}) 
=\Op{(P\extc Q)\probc{p}(P\extc R)}$. Similarly for \Ename{L8}.

\item
Cases \Ename{D2} and \Ename{L5}: It is trivial to construct
simulations in both directions.
\hfill$\Box$\vspace{1ex}
\end{itemize}
It can be argued that the equations \Ename{L1\mbox{--}8} are not all
that interesting, because they merely apply to our own parallel
composition operator. The reason to mention them here, is that, as we
will see below, they allow the parallel operator to be eliminated from
\pCSP expressions, and we believe the same can be achieved, with
similar axioms, for the more traditional parallel composition and
hiding operators of CSP.

We also have certain inequations which are valid for $\simpreo$, the most obvious
being 
\begin{displaymath}
\begin{array}[t]{lr}
\Ename{May1}\qquad\qquad&  P ~\sqsubseteq~ P \intc Q\\
\end{array}
\end{displaymath}
More inequations are listed in Figure~\ref{fig:inequations}.  The
inequations \Ename{Q1\mbox{--}8} complement the counterexamples
\ref{Q1}--\ref{Q8}. In each case, an equation that holds in
non-probabilistic may-testing semantics is salvaged in the shape of an
inequation, with a counterexample against the opposite direction.
\begin{figure}[t]
  \begin{displaymath}
    \begin{array}[t]{lr@{\,}l}
      \Ename{Q0}           & \Cnil & ~\sqsubseteq~ P\\
      \Ename{Q1}\hspace{3em}& a.(P \probc{p} Q)&~\sqsubseteq~ a.P \probc{p} a.Q\\
      \Ename{Q2}           & a.P \intc a.Q &~\sqsubseteq~ a.(P \intc Q)\\
      \Ename{Q3}           & a.P \extc a.Q &~\sqsubseteq~ a.(P \extc Q)\\
      \Ename{Q4}           & P &~\sqsubseteq~ P \extc Q\\
      \Ename{Q5}           & (P \probc{p} Q) \intc (P \probc{p} R) & 
                            ~\sqsubseteq~  P \probc{p} (Q \intc R)\\
      \Ename{Q6}           & P \intc (Q \probc{p} R) &
                            ~\sqsubseteq~ (P\intc Q) \probc{p} (P \intc R)\\
      \Ename{Q7}           & (P\extc Q) \intc (P \extc R) &~\sqsubseteq~ P \extc (Q \intc R)\\
      \Ename{Q8}           & P \intc (Q\extc R) 
                            &~\sqsubseteq~ (P\intc Q)\extc(P \intc R)
      
    \end{array}  
  \end{displaymath}

  \caption{Some inequations}
  \label{fig:inequations}
\end{figure}
\begin{proposition}\rm\label{prop:pcsp.ineq}
All the inequations in Figure~\ref{fig:inequations} are valid for $\simpreo$ over \pCSP.
\end{proposition}
\begin{proof}
The soundness of \Ename{Q0} and \Ename{Q1} is easy to check. All other
inequations can be derived from \Ename{Q0}, \Ename{May1} and the equations in
Figure~\ref{fig:equations} by using the precongruence property of
$\simpreo$. For example, we can reason
\[\begin{array}{rll}
P & = P\extc\Cnil \qquad & {\rm by\ \Ename{E1}}\\
     &\sqsubseteq P\extc Q & {\rm by\ \Ename{Q0}}
\end{array}\]
so as to obtain \Ename{Q4}.

We can also reason
\[\begin{array}{rll}
a.P\extc a.Q & \sqsubseteq a.(P\extc Q) \extc a.(P\extc Q)\qquad & {\rm by\ \Ename{Q4}}\\
     & = a.(P\extc Q) \intc a.(P\extc Q) & {\rm by\ \Ename{EI}}\\
     & = a.(P\extc Q) & {\rm by\ \Ename{I1}}
\end{array}\]
so as to obtain \Ename{Q3}.

As another example, we can reason
\[\begin{array}{@{}rll@{}}
P \intc (Q \probc{p} R) & = (P\probc{p}P) \intc (Q \probc{p} R) & {\rm by\ \Ename{P1}}\\
 & \sqsubseteq ((P\intc Q)\probc{p}(P\intc R)) \intc ((P\intc Q)\probc{p}
 (P\intc R))\qquad\!\! & {\rm by\ \Ename{May1}\scriptstyle (4\times\!)}\\
     &=(P\intc Q)\probc{p}(P\intc R)  & {\rm by\ \Ename{I1}}
\end{array}\]
so as to obtain \Ename{Q6}.
\end{proof}

\noindent
Another important inequation that follows from \Ename{May1} and
\Ename{P1} is $$P \probc{p} Q ~\sqsubseteq~ P \intc Q$$
saying that any probabilistic choice can be simulated by an internal choice.

Now with these equations and inequations, together with Theorem~\ref{thm:cong}
we have the beginnings of an algebraic
theory for \pCSP processes.
An application of this theory is to show
that the use of the parallel composition and external choice operators
can be eliminated. 
Let us use $P =_E Q$ to indicate that $P = Q$
can be derived using applications of the equations in
Figure~\ref{fig:equations}, without the inequations.   
Then define  \emph{standard processes} to be
the least subset of \pCSP satisfying:
\begin{enumerate}[(i)]
\item $\Cnil \in \standP$

\item $a.P \in \standP$, whenever $P \in \standP$

\item $P_1 \intc P_2 \in \standP$, whenever $P_i \in \standP$

\item $P_1 \probc{p} P_2 \in \standP$, whenever $P_i \in \standP$.

\end{enumerate}
\begin{proposition}\rm\label{prop:standardP}
For every $P$ in \pCSP there  exists a \emph{standard process} $\standf{P}$
such that $P =_E \standf{P}$.
\end{proposition}
\begin{proof}
  By induction on the structure of $P$.
\end{proof}


\section[Another look at CSP]{Another look at \CSP}

We have already seen that probabilistic tests have greater
distinguishing power than purely nondeterministic tests, when applied
to processes in \CSP, that is those which contain no probabilistic
choice. In Example~\ref{ex:action over intc} we have seen that $a.(P \intc Q)$ and
$a.P \intc a.Q$ can be distinguished using a probabilistic test, while
it is well known that they can not be distinguished using
non-probabilistic tests \cite{henn}. In this section we look briefly at
the theory of \CSP relative to probabilistic testing; we concentrate
on \emph{may} testing, although again similar results can be obtained for
\emph{must} testing.

First we have the converse of Theorem~\ref{thm:fwimpliespM}, showing
that simulations are both sound and complete with respect to
probabilistic \emph{may} testing for this sub-language.

\begin{theorem}\rm
  For $P,\;Q \in \CSP$, $P \pMayleq Q$ if and only if   $P \simpreo Q$.
\end{theorem}

\noindent
{\bf Proof.}\,
$(\Leftarrow)$ This implication is proved in
  Theorem~\ref{thm:fwimpliespM}.

$(\Rightarrow)$
Instead of directly showing that $\pMayleq$ implies $\simpreo$, we define
a seemingly weaker preorder $\sqsubseteq_w$: 
\[\mbox{$P\sqsubseteq_w Q$ iff for every test $T$:
  $(\maxlive{\Op{T \mathop{\parT} P}}=1) \Rightarrow (\maxlive{\Op{T \mathop{\parT} Q}}=1)$.}\]
By Proposition~\ref{prop:maxlive}, we can see that $\pMayleq$ implies $\sqsubseteq_w$.
If we can show that $\sqsubseteq_w$ is a simulation, then we are done because
$P \pMayleq Q$ will imply $P \simpreo Q$.

Given $P \sqsubseteq_w Q$ and
$P \ar{\mu} P'$, we want to find a process $Q'$ such that $Q
\dar{\hat{\mu}} Q'$ and $P' \sqsubseteq_w Q'$. We distinguish two cases.
\begin{enumerate}
\item 
$\mu = \tau$. Then $\Op{T \parT P} \ar{\tau} \Op{T \parT P'}$ for every test
  $T$, so $P'\sqsubseteq_w P$ by Lemma~\ref{l:tau} and hence
  $P'\sqsubseteq_w Q$. By taking $Q' = Q$, we complete the proof for this case. 
\item
$\mu = a$ for some $a\in\Act$. We define the set $Z = \sset{R ~|~ Q
  \dar{\hat a} R \mbox{ and } P'\not \sqsubseteq_w R}$. As $Q$ is a \CSP process,
  $Z$ is always finite. For each $R\inp Z$ there must be a test $T_R$
  such that $\maxlive{\Op{T_R \parT P'}}=1$ but $\maxlive{\Op{T_R \parT R}}<1$.
  Let $T_Z$ be the test $\bigoplus_{R\in Z}p_R  T_R$, where
  each $p_R$ is a positive probability. Then 
  \[\maxlive{\Op{T_Z \parT P'}} =
  \sum_{R\in Z}p_R\cdot \maxlive{\Op{T_R \parT P'}}=1\]
  and, for all $R'\inp Z$,
  \[\maxlive{\Op{T_Z \parT R'}}=\sum_{R\in Z}p_R\cdot \maxlive{\Op{T_R \parT R'}} <1\]
  So we have $\maxlive{\Op{a.T_Z \parT P}} \!=\! 1$, which implies
  $\maxlive{\Op{a.T_Z \parT Q}} \!=\! 1$  since $P \sqsubseteq_w Q$. By the definition
  of $\maxlive{\_\!\_}$ there exists a $Q'$ such that $Q\ar{\tau}^*\ar{a}Q'$
  and $\maxlive{\Op{T_Z \parT Q'}} \!=\! 1$. Thus $Q'\mathop{\not\in}
  Z$, and $P' \sqsubseteq_w Q'$.\hfill$\Box$
\end{enumerate}  

\noindent
We can also give a complete equational characterisation. The extra axiom which is
valid for this non-probabilistic sub-language is
\begin{displaymath}
\begin{array}[t]{lrl}
\Ename{May2}\qquad\qquad&  P \extc Q&= P \intc Q
\end{array}
\end{displaymath}
In particular this means that, as with standard testing, there is no difference
between internal and external choice. Now let us write $P \sqsubseteq_{E_\text{may}} Q$ to denote
the fact that $P \sqsubseteq Q$ can be derived using the equations of Figure~\ref{fig:equations}
and the inequations \Ename{May1} and \Ename{May2}.
\begin{theorem}\rm
    For $P,\;Q \in \CSP$, $P \pMayleq Q$ if and only if   $P \sqsubseteq_{E_\text{may}} Q$.
\end{theorem}

\begin{proof}
One direction follows from the fact that all the equations and inequations mentioned
are valid for $\simpreo$. The converse depends on being able to rewrite all processes into
a normal form:
$\bigbox_{i \in I} a_i.P_i$, where $I$ is a finite and possibly empty index set, is a
\emph{normal form} if each $P_i$ is in turn a normal form. This
conversion into normal form is enabled by
Proposition~\ref{prop:standardP} and \Ename{May2}.
Using \Ename{May1}, \Ename{E1\mbox{--}3} and the law $P \extc P =P$, which follows
from \Ename{May2} and \Ename{I1}, it is straightforward to show that for normal forms\\[1em]
\mbox{}\hfill
$\displaystyle \bigbox_{i \in I} a_i.P_i  \;\;\simpreo\;\; \bigbox_{j \in J} b_j.Q_j 
 \;\;\text{implies}\;\;
  \bigbox_{i \in I} a_i.P_i \;\;\sqsubseteq_{E_\text{may}}\;\;  \bigbox_{j \in J} b_j.Q_j $
\end{proof}

\section{Related work}\label{Related Work}

Models for probabilistic concurrent systems have been studied for a
long time \cite{Rabin63,Derman70,Vardi85,Jones89}.  One of the
first models obtained as a simple adaptation of the traditional labelled
transition systems from concurrency theory appears in \cite{LS91}.
Their \emph{probabilistic transition systems} are classical labelled
transition systems, where in addition every transition is labelled
with a probability, a real number in the interval [0,1], such that for
every state $s$ and every action $a$, the probabilities of all
$a$-labelled transitions leaving $s$ sum up to either 0 or 1.

In \cite{GJS90} a similar model was proposed, but where the
probabilities of \emph{all} transitions leaving $s$ sum up to either 0 or 1.
\cite{GSST90} propose the terminology \emph{reactive} for the type of
model studied in \cite{LS91}, and \emph{generative} for the type of
model studied in \cite{GJS90}. In a generative model, a process can
be considered to spontaneously generate actions, unless restricted by
the environment; in generating actions, a probabilistic choice is made
between all transitions that can be taken from a given state, even if
they have different labels. In a reactive model, on the other hand,
processes are supposed to perform actions only in response to requests
by the environment. The choice between two different actions is
therefore not under the control of the process itself. When the
environment requests a specific action, a probabilistic choice is made
between all transitions (if any) that are labelled with the requested action.

In the above-mentioned models, the nondeterministic choice that can be
modelled by non-probabilistic labelled transition systems is \emph{replaced}
by a probabilistic choice (and in the generative model also a
deterministic choice, a choice between different actions, is made
probabilistic). Hence reactive and generative probabilistic transition
systems do not generalise non-probabilistic labelled transition systems.
A model, or rather a calculus, that features both nondeterministic and
reactive probabilistic choice was proposed in \cite{HJ90}. It was
slightly reformulated in \cite{SL94} under the name \emph{simple
  probabilistic automata}, and is essentially the same model we use in
this paper.

Following the classification above, our model is reactive rather than
generative. The reactive model of \cite{LS91} can be reformulated by
saying that a state $s$ has at most one outgoing transition for any
action $a$, and this transition ends in a probability distribution
over its successor states. The generalisation of \cite{SL94}, that we
use here as well, is that a state can have multiple outgoing
transitions with the same label, each ending in a probability distribution.
%
Simple probabilistic automata are a special case of the
\emph{probabilistic automata} of \cite{SL94}, that also generalise the
generative models of probabilistic processes to a setting with
nondeterministic choice.

\subsection{Bisimulation, and the alternating approach}

Whereas the testing semantics explored in the present paper is based
on the idea that processes should be \emph{distinguished} only when there is a
compelling reason to do so, (strong) bisimulation semantics \cite{ccs} is based
on the idea that processes should be \emph{identified} only when there is a
compelling reason to do so. It has been extended to reactive probabilistic
processes in \cite{LS91}, to generative ones in \cite{GSST90}, and to
processes combining nondeterminism and probability in \cite{HJ90}.
The latter paper also features a complete axiomatisation of a
probabilistic extension of recursion-free CCS.

Weak and branching bisimulation \cite{ccs,GW96} are versions of strong
bisimulation that respect the hidden nature of the internal action
$\tau$.  Generalisations of these notions to nondeterministic
probabilistic processes appear, amongst others, in
\cite{SL94,Seg95,PLS00,AB01,BS01,DP05,AW06}, with complete
axiomatisations reported in \cite{BS01,DP05,DPP05,ABW06}.  The authors
of these paper tend to distinguish whether they work in an
\emph{alternating} \cite{PLS00,AB01,AW06,ABW06} or a \emph{non-alternating}
model of probabilistic processes \cite{SL94,Seg95,DP05,DPP05}, the two
approaches being compared in \cite{BS01}. The non-alternating model
stems from \cite{SL94} and is similar to our model of Section~\ref{sec:operational}.
The alternating model is attributed to \cite{HJ90}, and resembles our
graphical representation of processes in Section~\ref{sec:graphical}.
It is easy to see that mathematically the alternating and
non-alternating model can be translated into each other without loss
of information \cite{BS01}. 
The difference between the two is one of interpretation.
In the alternating interpretation, the nodes of form $\circ$ in our
graphical representations are interpreted as actual states a process
can be in, whereas in the non-alternating representation they are not.
Take for example the process $R_1 = a.(b\probc{\frac{1}{2}}c)$ depicted in
Figure~\ref{fig:ex.probc}. In the alternating representation this
process passes through a state in which $a$ has already happened, but
the probabilistic choice between $b$ and $c$ has not yet been made.
In the non-alternating interpretation on the other hand the execution
of $a$ is what constitutes this probabilistic choice; after doing $a$
there is a fifty-fifty change of ending up in either state.
Although in strong bisimulation semantics the alternating and
non-alternating interpretation lead to the same semantic equivalence,
in weak and branching bisimulation semantics the resulting
equivalences are different, as illustrated in \cite{PLS00,BS01,AW06}.
Our testing and simulation preorders as presented here can be
classified as non-alternating; however, we believe that an alternating
approach would lead to the very same preorders.

\subsection{Testing}

Generalisations of the testing theory of \cite{DNH84} to probabilistic
systems first appear in \cite{Chr90} and \cite{CSZ92}, for generative
processes without nondeterministic choice. The application of testing
to the probabilistic processes we consider here stems from \cite{WL92}.
In \cite{Seg96} a richer testing framework is proposed, for
essentially the same class of processes, namely one in which multiple
success actions $\omega_i$ for $i=1,2,\ldots$ exists, and the
application of a test to a process yields not a set of real numbers,
indicating success probabilities, but a set of tuples of real numbers,
the $i^{th}$ component in the tuple indicating the success probability
of $\omega_i$.

In \cite{JHW94}, a testing theory is proposed that
associates a \emph{reward}, a non-negative real number, to every
success-state in a test process; in calculating the set of results
of applying a test to a process, the probabilities of reaching a
success-state are multiplied by the reward associated to that state.
They allow non-probabilistic tests only, but apply these to arbitrary
nondeterministic probabilistic processes, and provide a trace-like
denotational characterisation of the resulting may-testing preorder.
Denotational characterisations of the variant of our testing preorders
in which only $\tau$-free processes are allowed as test-processes
appear in \cite{JW95,JW99}. These characterisations are improved in
\cite{JW02}, discussed below.

In \cite{CCRPP03} a testing theory for nondeterministic
probabilistic processes is developed in which, as in \cite{MMSS96},
all probabilistic choices are resolved first. A consequence of this is
that the idempotence of internal choice (our axiom \Ename{I1}) must be
sacrificed.
Some papers distill preorders for probabilistic processes by means of
\emph{testing scenarios} in which the premise that a test is itself a
process is given up. These include \cite{LS91,KN98} and \cite{aTSfPA}.

\subsection{Simulations}

Four different notions of simulation for probabilistic processes occur in the literature, each a
generalisation of the well know concept of simulation for nondeterministic
processes \cite{Pa81}. The most straightforward generalisation \cite{JL91}
defines a simulation as a relation $\aRel$ between states, satisfying, for all $s,t,\mu,\Theta$,
\begin{center}
if $s \aRel t $ and $s \ar{\mu} \Theta$ then there is a $\Delta'$ with
$t \ar{\mu} \Delta'$ and $\Theta \lift{\aRel} \Delta'$.
\end{center}
This simulation induces a preorder that does not satisfy the law
$$a.(P \probc{p} Q) \sqsubseteq a.P\extc a.Q$$
which holds in probabilistic \emph{may} testing semantics.
The reason is that the process $a.P\extc a.Q$ can answer the initial
$a$-move of $a.(P \probc{p} Q)$ by taking either the
$a$-move to $P$, or the $a$-move to $Q$, but not by a
probabilistic combination of the two.  Such probabilistic combinations
are allowed in the probabilistic simulation of \cite{SL94}, which
induces a coarser preorder on processes, satisfying the above law. In
our terminology it can be defined by changing the requirement above into
\begin{center}
if $s \aRel t $ and $s \ar{\mu} \Theta$ then there is a $\Delta'$ with
$\pdist{t} \ar{\mu} \Delta'$ and $\Theta \lift{\aRel} \Delta'$.
\end{center}
A \emph{weak} version of this probabilistic simulation, abstracting
from the internal action $\tau$, weakens this requirement into
\begin{center}
if $s \aRel t $ and $s \ar{\mu} \Theta$ then there is a $\Delta'$ with
$\pdist{t} \dar{\hat{\mu}} \Delta'$ and $\Theta \lift{\aRel} \Delta'$.
\end{center}
Nevertheless, also this probabilistic simulation does not satisfy all the
laws we have shown to hold for probabilistic may testing. In
particular, it does not satisfy the law\vspace{-1ex}
$$a.(P \probc{p} Q) \sqsubseteq a.P \probc{p} a.Q\vspace{1ex}.$$
Consider for instance the processes $R_1 = a.b.c.(d \probc{\frac{1}{2}} e)$
and $R_2 = a.(b.c.d \probc{\frac{1}{2}} b.c.e)$.
The law \Ename{Q1} above, which holds for probabilistic \emph{may} testing,
would yield $R_1 \sqsubseteq R_2$.
If we are to relate these processes via a probabilistic simulation \`a
la \cite{SL94}, the state $c.(d \probc{\frac{1}{2}} e)$ of $R_1$,
reachable after an $a$ and a $b$-step, needs to be related
to the \emph{distribution} $(c.d \probc{\frac{1}{2}} c.e)$ of $R_2$,
containing the two states $a.b$ and $a.c$. 
This relation cannot be obtained through lifting, as
this would entail relating the single state $c.(d \probc{\frac{1}{2}} e)$ to each of the
states $c.d$ and $c.e$. Such a relation would not be sound, because
$c.(d \probc{\frac{1}{2}} e)$ is able to perform the sequence of actions $ce$ half of the time,
whereas the process $c.d$ cannot mimic this.

In \cite{JW02}, another notion of simulation is proposed, whose
definition is too complicated to explain in a few sentences.  They
show for a class of probabilistic processes that do not contain
$\tau$-actions, that probabilistic \emph{may} testing is captured
exactly by their notion of simulation. Nevertheless, their notion of
simulation makes strictly more identifications than ours.  As an
example, consider the processes $R_1=a \probc{\frac{1}{2}} (b\extc c)$
and $R_3=(a \extc b) \probc{\frac{1}{2}} (a \extc c)$ of
Example~\ref{JW}, which also appear in Section 5 of \cite{JW02}. There
it is shown that $R_1 \sqsubseteq R_3$ holds in their semantics.
However, in our framework we have $R_1\notpMayleq R_3$, as
demonstrated in Example~\ref{JW}. The difference can only be explained
by the circumstance that in \cite{JW02} processes, and hence also
tests, may not have internal actions. So this example shows that tests
with internal moves can distinguish more processes than tests without
internal moves, even when applied to processes that have no internal moves
themselves.

Our notion of simulation first appears in \cite{Seg95}, although the
preorder $\simpreo$ of Definition~\ref{df-simulation preorder}
is new.  Segala has no expressions that denote
distributions and consequently is only interested in the restriction
of the simulation preorder to states (\emph{automata} in his framework).
It turns out that for states $s$ and $t$ (which in our framework are
expressions in the set $S_p$) we have $s\simpreo t$ iff $s\forsim
\pdist{t}$, so on their common domain of definition, the simulation
preorder of \cite{Seg95} agrees with ours.

This notion of simulation is strictly
more discriminating than the simulation of \cite{JW02}, and strictly
less discriminating than the ones from \cite{SL94} and \cite{JL91}.
We conjecture that, for the class of processes considered in this
paper, it captures probabilistic \emph{may} testing exactly, i.e.\
that $P \simpreo Q$ iff $P \pMayleq Q$. In \cite{LSV03} it has been
shown that the simulation preorder of \cite{Seg95} coincides with the
\emph{congruence closure of inclusion of sets of trace distributions},
a preorder also defined in \cite{Seg95}. In \cite{Seg96} it has been shown
that the latter notion coincides with the preorder generated by
Segala's different form of probabilistic \emph{may} testing, mentioned
earlier, in which there are countably
many different success actions, and the set of outcomes $\Outcomes$
consists of the countably-dimensional vectors over the unit interval
[0,1].  To the best of our knowledge, the question whether this form
of testing yields the same preorders as the notion of testing from
\cite{WL92} and our paper is, as of yet, unanswered.

\bibliographystyle{alpha}
%\bibliography{gdpf}
\newcommand{\etalchar}[1]{$^{#1}$}
\makeatletter
\def\small{\@setfontsize\small\@ixpt{12}
\abovedisplayskip 11\p@ plus3\p@ minus6\p@
\belowdisplayskip \abovedisplayskip
\abovedisplayshortskip  \z@ plus3\p@
\belowdisplayshortskip  6.5\p@ plus3.5\p@ minus3\p@
\def\@listi{\leftmargin\leftmargini
 \parsep 4.5\p@ plus2\p@ minus\p@ \itemsep 5\p@%\parsep
            \topsep 9\p@ plus3\p@ minus5\p@}}
\makeatother
\begin{thebibliography}{CCR{\etalchar{+}}03}

\bibitem[AB01]{AB01}
{ S.~Andova \& J.C.M. Baeten} (2001):
\newblock {\em Abstraction in probabilistic process algebra.}
\newblock In {\sl {\rm Proceedings of the 7th International Conference on} Tools and Algorithms for the Construction and Analysis of Systems}, {\sl \rm LNCS} 2031, Springer, pp. 204--219.

\bibitem[ABW06]{ABW06}
{ S.~Andova, J.C.M. Baeten \& T.A.C. Willemse} (2006):
\newblock {\em A complete axiomatisation of branching bisimulation for probabilistic systems with an application in protocol verification.}
\newblock In {\sl {\rm Proceedings of the 17th International Conference on} Concurrency Theory}, {\sl \rm LNCS} 4137, Springer, pp. 327--342.

\bibitem[AJ94]{AJ94}
{ S.~Abramsky \& A.~Jung} (1994):
\newblock {\em Domain theory.}
\newblock In {\sl Handbook of Logic and Computer Science}, volume~3, Clarendon Press, pp. 1--168.

\bibitem[AW06]{AW06}
{ S.~Andova \& T.A.C. Willemse} (2006):
\newblock {\em Branching bisimulation for probabilistic systems: Characteristics and decidability.}
\newblock {\sl Theoretical Computer Science} 356(3), pp. 325--355.

\bibitem[BHR84]{BHR84}
{ S.D. Brookes, C.A.R. Hoare \& A.W. Roscoe} (1984):
\newblock {\em A theory of communicating sequential processes.}
\newblock {\sl Journal of the ACM} 31(3), pp. 560--599.

\bibitem[BJ78]{vienna2}
{ D.~Bj{\o}rner \& C.B. Jones}, editors (1978):
\newblock {\em The {V}ienna {D}evelopment {M}ethod: The Meta-Language}, {\sl \rm LNCS} 61. Springer.

\bibitem[BS01]{BS01}
{ E.~Bandini \& R.~Segala} (2001):
\newblock {\em Axiomatizations for probabilistic bisimulation.}
\newblock In {\sl {\rm Proceedings of the 28th International Colloquium on} Automata, Languages and Programming}, {\sl \rm LNCS} 2076, Springer, pp. 370--381.

\bibitem[CCR{\etalchar{+}}03]{CCRPP03}
{ D.~Cazorla, F.~Cuartero, V.V. Ruiz, F.L. Pelayo \& J.J. Pardo} (2003):
\newblock {\em Algebraic theory of probabilistic and nondeterministic processes.}
\newblock {\sl Journal of Logic and Algebraic Programming} 55(1-2), pp. 57--103.

\bibitem[Chr90]{Chr90}
{ I.~Christoff} (1990):
\newblock {\em Testing equivalences and fully abstract models for probabilistic processes.}
\newblock In {\sl {\rm Proceedings the 3rd International Conference on} Concurrency Theory}, {\sl \rm LNCS} 458, Springer, pp. 126--140.

\bibitem[CSZ92]{CSZ92}
{ R.~Cleaveland, S.A. Smolka \& A.E. Zwarico} (1992):
\newblock {\em Testing preorders for probabilistic processes.}
\newblock In {\sl {\rm Proceedings of the 19th International Colloquium on} Automata, Languages and Programming}, {\sl \rm LNCS} 623, Springer, pp. 708--719.

\bibitem[Der70]{Derman70}
{ C.~Derman} (1970):
\newblock {\em Finite State Markovian Decision Processes}.
\newblock Academic Press.

\bibitem[DH84]{DNH84}
{ R.~De~Nicola \& M.~Hennessy} (1984):
\newblock {\em Testing equivalences for processes.}
\newblock {\sl Theoretical Computer Science} 34, pp. 83--133.

\bibitem[DP05]{DP05}
{ Y.~Deng \& C.~Palamidessi} (2005):
\newblock {\em Axiomatizations for probabilistic finite-state behaviors.}
\newblock In {\sl {\rm Proceedings of the 8th International Conference on} Foundations of Software Science and Computation Structures}, {\sl \rm LNCS} 3441, Springer, pp. 110--124.

\bibitem[DPP05]{DPP05}
{ Y.~Deng, C.~Palamidessi \& J.~Pang} (2005):
\newblock {\em Compositional reasoning for probabilistic finite-state behaviors.}
\newblock In {\sl Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday}, {\sl \rm LNCS} 3838, Springer, pp. 309--337.

\bibitem[ER64]{elgot}
{ C.C. Elgot \& A.~Robinson} (1964):
\newblock {\em Random-access stored-program machines, an approach to programming languages.}
\newblock {\sl Journal of the ACM} 11(4), pp. 365--399.

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

\bibitem[GSST90]{GSST90}
{ 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 {\rm Proceedings of the 5th Annual IEEE Symposium on} Logic in Computer Science}, Computer Society Press, pp. 130--141.

\bibitem[GW96]{GW96}
{ R.J.~van Glabbeek \& W.P. Weijland} (1996):
\newblock {\em Branching time and abstraction in bisimulation semantics.}
\newblock {\sl Journal of the ACM} 43(3), pp. 555--600.

\bibitem[Hen82]{Hen82}
{ M.~Hennessy} (1982):
\newblock {\em Powerdomains and nondeterministic recursive definitions.}
\newblock In {\sl {\rm Proceedings of the 5th International} Symposium on Programming}, {\sl \rm LNCS} 137, Springer, pp. 178--193.

\bibitem[Hen88]{henn}
{ M.~Hennessy} (1988):
\newblock {\em An Algebraic Theory of Processes}.
\newblock MIT Press.

\bibitem[HJ90]{HJ90}
{ H.~Hansson \& B.~Jonsson} (1990):
\newblock {\em A calculus for communicating systems with time and probabilities.}
\newblock In {\sl {\rm Proceedings of the} Real-Time Systems Symposium {\rm(RTSS '90)}}, Computer Society Press, pp. 278--287.

\bibitem[Hoa85]{csp}
{ C.A.R. Hoare} (1985):
\newblock {\em Communicating Sequential Processes}.
\newblock Prentice-Hall.

\bibitem[HSM97]{HSM97}
{ Jifeng He, K.~Seidel \& A.K. McIver} (1997):
\newblock {\em Probabilistic models for the guarded command language.}
\newblock {\sl Science of Computer Programming} 28, pp. 171--192.

\bibitem[JHW94]{JHW94}
{ B.~Jonsson, C.~Ho-Stuart \& Wang Yi} (1994):
\newblock {\em Testing and refinement for nondeterministic and probabilistic processes.}
\newblock In {\sl {\rm Proceedings of the 3rd International Symposium on} Formal Techniques in Real-Time and Fault-Tolerant Systems}, {\sl \rm LNCS} 863, Springer, pp. 418--430.

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

\bibitem[JP89]{Jones89}
{ C.~Jones \& G.~Plotkin} (1989):
\newblock {\em A probabilistic powerdomain of evaluations.}
\newblock In {\sl {\rm Proceedings of the 4th Annual {IEEE} Symposium on} Logic in Computer Science}, Computer Society Press, pp. 186--195.

\bibitem[JW95]{JW95}
{ B.~Jonsson \& Wang Yi} (1995):
\newblock {\em Compositional testing preorders for probabilistic processes.}
\newblock In {\sl {\rm Proceedings of the 10th Annual IEEE Symposium on} Logic in Computer Science}, Computer Society Press, pp. 431--441.

\bibitem[JW99]{JW99}
{ B.~Jonsson \& Wang Yi} (1999):
\newblock {\em Fully abstract characterization of probabilistic may testing.}
\newblock In {\sl {\rm Proceedings of the 5th International AMAST Workshop on} Formal Methods for Real-Time and Probabilistic Systems}, {\sl \rm LNCS} 1601, Springer, pp. 1--18.

\bibitem[JW02]{JW02}
{ B.~Jonsson \& Wang Yi} (2002):
\newblock {\em Testing preorders for probabilistic processes can be characterized by simulations.}
\newblock {\sl Theoretical Computer Science} 282(1), pp. 33--51.

\bibitem[JWL01]{JWL01}
{ B.~Jonsson, Wang Yi \& K.G. Larsen} (2001):
\newblock {\em Probabilistic extensions of process algebras.}
\newblock In {\sl Handbook of Process Algebra}, chapter~11, Elsevier, pp. 685--710.

\bibitem[KN98]{KN98}
{ M.Z. Kwiatkowska \& G.~Norman} (1998):
\newblock {\em A testing equivalence for reactive probabilistic processes.}
\newblock {\sl Electronic Notes in Theoretical Computer Science}, 16(2).

\bibitem[Lan63]{landin}
{ P.J. Landin} (1963):
\newblock {\em The mechanical evaluation of expressions.}
\newblock {\sl Computer Journal} 6(4), pp. 308--320.

\bibitem[Low93]{Low93}
{ G.~Lowe} (1993):
\newblock {\em Representing nondeterminism and probabilistic behaviour in reactive processes.}
\newblock Technical Report TR-11-93, Computing laboratory, Oxford University.

\bibitem[Low95]{Lowe95}
{ G.~Lowe} (1995):
\newblock {\em Probabilistic and prioritized models of timed {CSP}.}
\newblock {\sl Theoretical Computer Science} 138, pp. 315--352.

\bibitem[LS91]{LS91}
{ K.G. Larsen \& A.~Skou} (1991):
\newblock {\em Bisimulation through probabilistic testing.}
\newblock {\sl Information and Computation} 94(1), pp. 1--28.

\bibitem[LS92]{larsenskou}
{ K.G. Larsen \& A.~Skou} (1992):
\newblock {\em Compositional verification of probabilistic processes.}
\newblock In {\sl {\rm Proceedings of the 3rd International Conference on} Concurrency Theory}, {\sl \rm LNCS} 630, Springer, pp. 456--471.

\bibitem[LSV03]{LSV03}
{ N.~Lynch, R.~Segala \& F.W. Vaandrager} (2003):
\newblock {\em Compositionality for probabilistic automata.}
\newblock In {\sl {\rm Proceedings of the 14th International Conference on} Concurrency Theory}, {\sl \rm LNCS} 2761, Springer, pp. 204--222.

\bibitem[Luc71]{vienna1}
{ P.~Lucas} (1971):
\newblock {\em Formal definition of programming languages and systems.}
\newblock In {\sl IFIP Congress}, volume~1, pp. 291--297.

\bibitem[Mil89]{ccs}
{ R.~Milner} (1989):
\newblock {\em Communication and Concurrency}.
\newblock Prentice-Hall.

\bibitem[Mis00]{Mis00}
{ M.W. Mislove} (2000):
\newblock {\em Nondeterminism and probabilistic choice: Obeying the laws.}
\newblock In {\sl {\rm Proc. of} CONCUR'00}, {\sl \rm LNCS} 1877, Springer, pp. 350--364.

\bibitem[MM01]{MM01}
{ A.K. McIver \& C.C. Morgan} (2001):
\newblock {\em Partial correctness for probabilistic programs.}
\newblock {\sl Theoretical Computer Science} 266(1--2), pp. 513--41.

\bibitem[MMS96]{MMS96}
{ C.C. Morgan, A.K. McIver \& K.~Seidel} (1996):
\newblock {\em Probabilistic predicate transformers.}
\newblock {\sl ACM Transactions on Programming Languages and Systems} 18(3), pp. 325--353.

\bibitem[MMSS96]{MMSS96}
{ C.C. Morgan, A.K. McIver, K.~Seidel \& J.W. Sanders} (1996):
\newblock {\em Refinement-oriented probability for {CSP}.}
\newblock {\sl Formal Aspects of Computing} 8(6), pp. 617--47.

\bibitem[MOW04]{mislove03}
{ M.W. Mislove, J.~Ouaknine \& J.~Worrell} (2004):
\newblock {\em Axioms for probability and nondeterminism.}
\newblock {\sl Electronic Notes in Theoretical Computer Science} 96, pp. 7--28.

\bibitem[OH86]{OH86}
{ E.-R. Olderog \& C.A.R. Hoare} (1986):
\newblock {\em Specification-oriented semantics for communicating processes.}
\newblock {\sl Acta Informatica} 23, pp. 9--66.

\bibitem[Par81]{Pa81}
{ D.M.R. Park} (1981):
\newblock {\em Concurrency and automata on infinite sequences.}
\newblock In {\sl {\rm Proceedings of 5th} GI Conference}, {\sl \rm LNCS} 104, Springer, pp. 167--183.

\bibitem[Plo81]{plotkin81structural}
{ G.D. Plotkin} (1981):
\newblock {\em {A Structural Approach to Operational Semantics}.}
\newblock Technical Report DAIMI FN-19, University of Aarhus.

\bibitem[Plo04]{plotkin04structural}
{ G.D. Plotkin} (2004):
\newblock {\em {A Structural Approach to Operational Semantics}.}
\newblock {\sl Journal of Logic and Algebraic Programming} 60-61, pp. 17--139.

\bibitem[PLS00]{PLS00}
{ A.~Philippou, I.~Lee \& O.~Sokolsky} (2000):
\newblock {\em Weak bisimulation for probabilistic systems.}
\newblock In {\sl {\rm Proceedings of the 11th International Conference on} Concurrency Theory}, {\sl \rm LNCS} 1877, Springer, pp. 334--349.

\bibitem[Rab63]{Rabin63}
{ M.O. Rabin} (1963):
\newblock {\em Probabilistic automata.}
\newblock {\sl Information and Control} 6, pp. 230--245.

\bibitem[Seg95]{Seg95}
{ R.~Segala} (1995):
\newblock {\em Modeling and Verification of Randomized Distributed Real-Time Systems}.
\newblock PhD thesis, MIT.

\bibitem[Seg96]{Seg96}
{ R.~Segala} (1996):
\newblock {\em Testing probabilistic automata.}
\newblock In {\sl {\rm Proceedings of the 7th International Conference on} Concurrency Theory}, {\sl \rm LNCS} 1119, Springer, pp. 299--314.

\bibitem[SL94]{SL94}
{ R.~Segala \& N.A. Lynch} (1994):
\newblock {\em Probabilistic simulations for probabilistic processes.}
\newblock In {\sl {\rm Proceedings of the 5th International Conference on} Concurrency Theory}, {\sl \rm LNCS} 836, Springer, pp. 481--496.

\bibitem[SV03]{aTSfPA}
{ M.I.A. Stoelinga \& F.W. Vaandrager} (2003):
\newblock {\em A testing scenario for probabilistic automata.}
\newblock In {\sl {\rm Proceedings of the 30th International Colloquium on} Automata, Languages and Programming}, {\sl \rm LNCS} 2719, Springer, pp. 407--18.

\bibitem[TKP05]{TKP05}
{ R.~Tix, K.~Keimel \& G.D. Plotkin} (2005):
\newblock {\em Semantic domains for combining probability and non-determinism.}
\newblock {\sl Electronic Notes in Theoretical Computer Science} 129, pp. 1--104.

\bibitem[Var85]{Vardi85}
{ M.Y. Vardi} (1985):
\newblock {\em Automatic verification of probabilistic concurrent finite-state programs.}
\newblock In {\sl {\rm Proceedings 26th Annual Symposium on} Foundations of Computer Science}, pp. 327--338.

\bibitem[VW06]{VW06}
{ D.~Varacca \& G.~Winskel} (2006):
\newblock {\em Distributing probability over non-determinism.}
\newblock {\sl Mathematical Structures in Computer Science} 16(1), pp. 87--113.

\bibitem[WL92]{WL92}
{ Wang Yi \& K.G. Larsen} (1992):
\newblock {\em Testing probabilistic and nondeterministic processes.}
\newblock In {\sl {\rm Proceedings of the IFIP TC6/WG6.1 Twelfth International Symposium on} Protocol Specification, Testing and Verification}, {\sl IFIP Transactions} C-8, North-Holland, pp. 47--61.

\end{thebibliography}

\end{document}
