\documentclass[10pt,twocolumn]{article}
\usepackage{latexsym}
\usepackage{times}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{xspace}
\usepackage{enumerate}

%% IEEE 8.5 x 11-Inch Proceedings Style `latex8.sty'.
\setlength{\textheight}{8.875in}
\setlength{\textwidth}{6.875in}
\setlength{\columnsep}{0.3125in}
\setlength{\topmargin}{0in}
\setlength{\headheight}{0in}
\setlength{\headsep}{0in}
\setlength{\parindent}{1pc}
\setlength{\oddsidemargin}{-.304in}
\setlength{\evensidemargin}{-.304in}

\makeatletter
\def\@maketitle
   {
   \newpage
   \null
   \vskip .375in 
   \begin{center}
      {\Large \bf \@title \par} 
      % additional two empty lines at the end of the title 
      \vspace*{24pt} 
      {
      \large 
      \lineskip .5em
      \begin{tabular}[t]{c}
         \@author 
      \end{tabular}
      \par
      } 
      % additional small space at the end of the author name 
      \vskip .5em 
      {
       \large 
      \begin{tabular}[t]{c}
         \@affiliation 
      \end{tabular}
      \par 
      \ifx \@empty \@email
      \else
         \begin{tabular}{r@{~}l}
            E-mail: & {\tt \@email}
         \end{tabular}
         \par
      \fi
      }
      % additional empty line at the end of the title block 
      \vspace*{12pt} 
   \end{center}
   } 

\def\abstract
   {%
   \centerline{\large\bf Abstract}%
   \vspace*{12pt}%
   \it%
   }

\def\endabstract
   {
   % additional empty line at the end of the abstract 
   \vspace*{12pt} 
   }

\def\affiliation#1{\gdef\@affiliation{#1}} \gdef\@affiliation{}

\def\email#1{\gdef\@email{#1}}
\gdef\@email{}

\font\tenhv  = phvb at 10pt
\newlength{\@ctmp}
\newlength{\@figindent}
\setlength{\@figindent}{1pc}

\long\def\@makecaption#1#2{
   \vskip 10pt
   \setbox\@tempboxa\hbox{\tenhv\noindent #1.~#2} 
   \setlength{\@ctmp}{\hsize}
   \addtolength{\@ctmp}{-\@figindent}\addtolength{\@ctmp}{-\@figindent} 
   % IF longer than one indented paragraph line
   \ifdim \wd\@tempboxa >\@ctmp
      % THEN set as an indented paragraph
      \begin{list}{}{\leftmargin\@figindent \rightmargin\leftmargin} 
         \item[]\tenhv #1.~#2\par
      \end{list}
   \else
      % ELSE center
      \hbox to\hsize{\hfil\box\@tempboxa\hfil} 
   \fi}

\def\section{\@startsection {section}{1}{\z@}
   {14pt plus 2pt minus 2pt}{14pt plus 2pt minus 2pt} {\large\bf}} 
\makeatother
\newcommand{\Section}[1]{\section{\hskip -1em.~~#1}} 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Fonts
\newfont{\fsc}{eusm10 scaled 1100}      % frenchscript letters
\newfont{\bbb}{bbm10 scaled 1100}       % blackboard bold
\newfont{\bbbs}{bbm10 scaled 800}       % blackboard bold scriptstyle

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Spacing
\newcommand{\inp}{\mathop\in}                           % takes less space
\newcommand{\Cdot}{\mathord\cdot}
\newcommand{\Defs}{\mathrel{:=}}
\newcommand{\Minus}{\mathord-}
\newcommand{\Leq}{\mathord\leq}
\newcommand{\Eq}{\mathord=}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% General
\newcommand{\CClose}{\mathord{\updownarrow}}
\newcommand{\IN}{\mathrel{\overline{\in}}}
\newcommand{\outc}{o}                                   % outcome
\newcommand{\Exp}[1]{\textrm{Exp}_{#1}}
\renewcommand{\phi}{\varphi}
\renewcommand{\mu}{\alpha}                              % actions in Act_\tau
\newcommand{\aRel}{\ensuremath{\mathrel{{\cal R }}}}
\newcommand\Wide[1] {~~~#1~~~}
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{#1}}     % no vertical space

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  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{\sCSP}{\ensuremath{\mathsf{sCSP}}\xspace}
\newcommand{\CSP}{\ensuremath{\mathsf{CSP}}\xspace}
\newcommand{\Op}[1]{\mbox{\bbb [}#1\mbox{\bbb ]}}
\newcommand{\Ops}[1]{\mbox{\bbbs [}#1\mbox{\bbbs ]}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Testing
\newcommand{\VV}{{\mathbb V}}
\newcommand{\Overline}[1]{\widehat{#1}}
\newcommand{\Apply}{\ensuremath{{\mathcal A}}\xspace}
\newcommand{\DApply}{\ensuremath{{\Overline{\mathcal A}}}\xspace}
\newcommand{\MDApply}{\ensuremath{{\Overline{\mathcal A}^{\raisebox{-.1em}{\scriptsize$\Omega$}}\xspace}}}
\newcommand{\CApply}{\ensuremath{{{\mathcal A}_{\scriptscriptstyle\updownarrow}}}}
\newcommand{\DCApply}{\ensuremath{{\Overline{\mathcal A}_{\scriptscriptstyle\updownarrow}}}}
\newcommand{\MDCApply}{\ensuremath{{\Overline{\mathcal A}_{\scriptscriptstyle\updownarrow}^{\raisebox{-.1em}{\scriptsize$\Omega$}}\xspace}}}
\newcommand{\results}[1]{\ensuremath\VV(#1)}
\newcommand{\resultsN}{\ensuremath\VV\xspace}
\newcommand{\Dresults}[1]{\ensuremath{{\Overline\VV}}(#1)}
\newcommand{\DresultsN}{\ensuremath{{\Overline\VV}}\xspace}
\newcommand{\Cresults}[1]{\plat{$\VV_{\scriptscriptstyle\updownarrow}$}(#1)}
\newcommand{\CresultsN}{\plat{$\VV_{\scriptscriptstyle\updownarrow}$}}
\newcommand{\CDresults}[1]{\plat{$\Overline\VV\kern -0.2em_{\scriptscriptstyle\updownarrow}$}(#1)}
\newcommand{\CDresultsN}{\plat{$\Overline\VV\kern-0.2em_{\scriptscriptstyle\updownarrow}$}}
\newcommand{\MDresults}[1]{\ensuremath{{\Overline\VV_{\scriptscriptstyle\updownarrow}^{\raisebox{-.3em}{\scriptsize$\Omega$}}(#1)}}}
\newcommand{\MDresultsN}{\ensuremath{{\Overline\VV_{\scriptscriptstyle\updownarrow}^{\raisebox{-.3em}{\scriptsize$\Omega$}}\xspace}}}
\newcommand{\Fsubs}[1]{\mathop{\mbox{\fsc P}^{\mbox{\tiny\kern .1em$+$}}_{\it \kern -.2em fin}(#1)}} % CCM 060807
\newcommand{\subs}[1]{\mathop{\mbox{\fsc P}^{\mbox{\tiny\kern .1em$+$}}\kern-.15em(#1)}}
\newcommand{\subsN}{\mathop{\mbox{\fsc P}^{\mbox{\tiny\kern .1em$+$}}\kern-.15em}}
\newcommand{\eureka}{\ensuremath{\omega}\xspace}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preorders
\newcommand{\Hleq}{\mathrel{\leq_{\rm Ho}}}
\newcommand{\Sleq}{\mathrel{\leq_{\rm Sm}}}
\newcommand{\Mustleq}{\sqsubseteq_{\text{must}}}
\newcommand{\Mayleq}{\sqsubseteq_{\text{may}}}
\newcommand{\Musteq}{\simeq_{\text{must}}}
\newcommand{\Mayeq}{\simeq_{\text{may}}}
\newcommand{\pMustleq}{\mathrel{\relax{\sqsubseteq}_{\text{pmust}}}}
\newcommand{\pMayleq}{\mathrel{\relax{\sqsubseteq}_{\text{pmay}}}}
\newcommand{\pMusteq}{\simeq_{\text{pmust}}}
\newcommand{\pMayeq}{\simeq_{\text{pmay}}}
\newcommand{\rMustleq}{\mathrel{\sqsubseteq_{\text{must}}}}
\newcommand{\rMayleq}{\mathrel{\sqsubseteq_{\text{may}}}}
\newcommand{\dMustleq}{\mathrel{\Overline{\sqsubseteq}_{\text{must}}}}
\newcommand{\dMayleq}{\mathrel{\Overline{\sqsubseteq}_{\text{may}}}}
\newcommand{\prMustleq}{\mathrel{\sqsubseteq_{\text{pmust}}}}
\newcommand{\prMayleq}{\mathrel{\sqsubseteq_{\text{pmay}}}}
\newcommand{\pdMustleq}{\mathrel{\Overline{\sqsubseteq}_{\text{pmust}}}}
\newcommand{\pdMayleq}{\mathrel{\Overline{\sqsubseteq}_{\text{pmay}}}}
\newcommand{\pdmMustleq}{\mathrel{\Overline{\sqsubseteq}_{\text{pmust}}^{\raisebox{-.3em}{\scriptsize$\Omega$}}}}
\newcommand{\pdmMayleq}{\mathrel{\Overline{\sqsubseteq}_{\text{pmay}}^{\raisebox{-.3em}{\scriptsize$\Omega$}}}}

%CCM060810: Tuck the "S" under.
\newcommand{\forsiminv}{\mathrel{\lhd_{\raisebox{-.1em}{\tiny\it S}}}}
\newcommand{\forsim}{\mathrel{\rhd\kern -.3em_{\raisebox{-.1em}{\tiny\it S}}}}
\newcommand{\failsim}{\mathrel{\rhd\kern -.3em_{\raisebox{-.1em}{\tiny\it FS}}}}
\newcommand{\failsiminv}{\mathrel{\lhd_{\raisebox{-.1em}{\tiny \it FS}}}}
\newcommand{\liftforsim}{\mathrel{\lift{\rhd\kern-.3em_{\raisebox{-.1em}{\tiny\it S}}}}}
\newcommand{\liftfailsim}{\mathrel{\lift{\rhd\kern-.3em_{\raisebox{-.1em}{\tiny\it FS}}}}}
\newcommand{\forsimequiv}{\simeq_{S}}
\newcommand{\forsimpreo}{\sqsubseteq_{S}}
\newcommand{\failsimpreo}{\sqsubseteq_{\it FS}}
\newcommand{\Invfailsimpreo}{\sqsupseteq_{\it FS}}
\newcommand{\failsimequiv}{\simeq_{\it FS}}

\newcommand{\modalFSpreo}{\mathrel{\sqsubseteq}^{\FSL}\!}
\newcommand{\modalSpreo}{\mathrel{\sqsubseteq}^{\SL}\!}
\newcommand{\tdc}{\sqsubseteq_{\it TD}}
\newcommand{\fdc}{\sqsubseteq_{\it FD}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Distributions
%CCM060810 The \mbox stops the D hanging below the baseline.
\newcommand{\dist}[1]{\mathop{\mbox{$\cal D$}} ({#1})   } % distributions
\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}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Modal logic
\newcommand{\FSL}{\mathcal{F}}
\newcommand{\SL}{\mathcal{L}}
\newcommand{\diam}[1]{\langle#1\rangle}
\newcommand{\refuse}[1]{\mathop{\mathbf{ref}(#1)}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Maths
\newcommand{\setof}[2]{\{ \, #1 \, \mid \, #2 \, \}}% set comprehension
\newcommand{\sset}[1]{\{ {#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)}}}%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%% Inferences %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\makeatletter

\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][{}]{%
    \setbox\@topbox\hbox{%
      \renewcommand{\arraystretch}{1}%
      $\begin{array}{l}#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][{}]{%
    \setbox\@topbox\hbox{%
      \renewcommand{\arraystretch}{1}%
      $\begin{array}{lr@{}}#2&#4\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{\slinfer}[2][{}]{\renewcommand{\arraystretch}{1}%
                  \begin{array}{l}#2\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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Operational semantics
\newcommand{\Ar}[1]{\mathbin{\stackrel{#1}{\longrightarrow}}}
\newcommand{\ar}[1]{\mathrel{\goesto[{#1}]}}
\newcommand{\nar}[1]{\hspace{6pt}\not\hspace{-6pt}\mathrel{\goesto[{#1\;}]}}
\newcommand{\dar}[1]{\mathrel{\Goesto[\raisebox{.08em}{\scriptsize$#1$}]}} %weak arrow
\newcommand{\hatar}[1]{\mathrel{\goesto[\hat{{#1}}]}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Theorem-like environments
\newtheorem{defi}{Definition}
\newtheorem{theo}{Theorem}
\newtheorem{prop}{Proposition}
\newtheorem{lemm}{Lemma}
\newtheorem{coro}{Corollary}
\newtheorem{exam}{Example}

\newenvironment{definition}{\begin{defi} \rm}{\end{defi}}
\newenvironment{theorem}{\begin{theo} \rm}{\end{theo}}
\newenvironment{proposition}{\begin{prop} \rm}{\end{prop}}
\newenvironment{lemma}{\begin{lemm} \rm}{\end{lemm}}
\newenvironment{corollary}{\begin{coro}\rm}{\end{coro}}
\newenvironment{example}{\begin{exam}\rm}{\end{exam}}
\newenvironment{proof}{\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]}
                  {\hfill $\Box$\end{trivlist}}
\newenvironment{itemise}{\begin{list}{$\bullet$}{\leftmargin 18pt
                        \labelwidth\leftmargini\advance\labelwidth-\labelsep
                        \topsep 4pt \itemsep 2pt \parsep 2pt}}{\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Cross referencing
\newcommand\Def[1] {Def.~\ref{#1}}
\newcommand\Thm[1] {Thm.~\ref{#1}}
\newcommand\Eqn[1] {(\ref{#1})}
\newcommand\Lem[1] {Lem.~\ref{#1}}
\newcommand\Fig[1] {Fig.~\ref{#1}}
\newcommand\Prop[1] {Prop.~\ref{#1}}
\newcommand\Sect[1] {Sec.~\ref{#1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Axiomatisations
\newcommand{\MustAxleq}{\mathrel{\sqsubseteq_{E_\text{must}}}}
\newcommand{\MustAxeq}{\mathrel{=_{E_\text{must}}}}
\newcommand{\Eeq}{\mathrel{=_{E}}}
\newcommand{\Peq}{\mathrel{=_{\text{prob}}}}
\newcommand{\MayAxleq}{\mathrel{\sqsubseteq_{E_\text{may}}}}
\newcommand{\MayAxeq}{\mathrel{=_{E_\text{may}}}}
\newcommand{\nCSP}{\ensuremath{\mathsf{nCSP}}\xspace}
\newcommand{\inits}[1]{\mathrel{\textit{inits}(#1)}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}

\title{Characterising Testing Preorders for Finite Probabilistic Processes}

\author{Yuxin Deng\thanks{We acknowledge the support of the Australian Research
        Council (ARC) Grant DP034557.}\\
       \makebox[0pt]{\small Jiao Tong University}\\[-3pt]
       \makebox[0pt]{\small Shanghai, China}\\
       \hline
  \makebox[62pt][l]{$\!\!$\small School of CSE, University of New South Wales}\\[-3pt]
       \makebox[0pt][l]{\small ~~~~~~~Sydney, Australia}
\and Rob van Glabbeek\\
       \small National ICT Australia\\[-3pt]
       \makebox[0pt]{\small Sydney, Australia}\\
       \hline
\and Matthew Hennessy\\
       \makebox[0pt]{\small Department of Informatics}\\[-3pt]
       \small University of Sussex\\[-3pt]
       \small Falmer, Brighton, UK
\and Carroll Morgan$^*$~~~~~Chenyi Zhang\\
       \makebox[0pt][l]{\small ~~~National ICT Australia}\\[-10pt]
       \makebox[0pt][l]{~~\rule{2.95cm}{.5pt}}\\[-3pt]
       \small School of Computer Science and Engineering\\[-3pt]
       \small The University of New South Wales\\[-3.5pt]
       \small Sydney, Australia
}

\maketitle
\thispagestyle{empty}

\begin{abstract}\noindent
In 1992 Wang \& Larsen extended the may- and must preorders of De
Nicola and Hennessy to processes featuring probabilistic as well as
nondeterministic choice. They concluded with two problems that have
remained open throughout the years, namely to find complete
axiomatisations and alternative characterisations for these preorders.
This paper solves both problems for finite processes with silent
moves. It characterises the may preorder in terms of simulation, and
the must preorder in terms of failure simulation. It also gives a
characterisation of both preorders using a modal logic. Finally it
axiomatises both preorders over a probabilistic version of CSP.
\end{abstract}

%-------------------------------------------------------------------------
\Section{Introduction}

\noindent
A satisfactory semantic theory for processes which encompass both
nondeterministic and probabilistic behaviour has been a long-standing
research problem
\cite{HJ90,WL92,Low93,JHW94,SL94,Sei95,Seg95,JW95,MMSS96,Seg96,HSM97,KN98,Mis00,BS01,JW02,LSV03,CCVP03,TKP05,DP07}.
In 1992 Wang \& Larsen posed the problems of finding
complete axiomatisations and
alternative characterisations for a natural generalisation of the
standard testing preorders \cite{DNH84} to such processes \cite{WL92}.
Here we solve both problems, at least for finite processes, by providing
a detailed account of both may- and must testing preorders for a
finite version of the process calculus CSP extended with
probabilistic choice. For each preorder we provide three independent
characterisations, using
(i)  co-inductive simulation relations, \,
(ii) a modal logic \, and
(iii) sets of inequations.

\paragraph*{Testing processes:}
Our starting point is the finite process calculus \pCSP \cite{DGHMZ07}
obtained by adding a probabilistic choice operator to finite CSP;
like others who have done the same, we now have \emph{three} choice
\pagebreak[1]
operators, external $P \extc Q$, internal  $P \mathbin{\intc} Q$ and the newly added
probabilistic choice $P \mathbin{\probc{p}} Q$. So a semantic theory for \pCSP
will have to provide a coherent account of the precise relationships
between these operators.

As a first step, in \Sect{sec:pcsp} we provide an interpretation of
\pCSP as a \emph{probabilistic labelled transition system}, in which,
following \cite{SL94}, transitions like $s \Ar{\mu} s'$ from
standard labelled transition systems are generalised to the form $s
\ar{\mu} \Delta$, where $\Delta$ is a \emph{distribution}, a mapping
assigning probabilities to states. With this interpretation we
obtain in \Sect{sec:testing} a version of the testing preorders of \cite{DNH84} for \pCSP
processes, $\pMayleq$ and $\pMustleq$.
These are based on the ability of processes to pass \emph{tests}; the
tests we use are simply \pCSP processes in which certain \emph{states}
are marked as \emph{success states}. See \cite{DGHMZ07} for a
detailed discussion of the power of such tests.

The object of this paper is to give useful characterisations of these
testing preorders. This problem was addressed previously by Segala
in \cite{Seg96}, but using testing preorders $\pdmMayleq$ and
$\pdmMustleq$ that differ in two ways from the ones in
\cite{DNH84,henn,WL92,DGHMZ07} and the present paper. First of all, in
\cite{Seg96} the success of a test is achieved by the \emph{actual
execution} of a predefined \emph{success action}, rather than the
reaching of a success state.  We call this an \emph{action}-based, as
opposed to a \emph{state}-based, approach.  Secondly, \cite{Seg96}
employs a countable number of success actions instead of a single one;
we call this \emph{vector-based}, as opposed to \emph{scalar},
testing. Segala's results in \cite{Seg96} depend crucially on this
form of testing. To achieve our current results, we need Segala's
preorders as a stepping stone. We relate them to ours by considering
intermediate preorders $\pdMayleq$ and \plat{$\pdMustleq$} that arise from
action-based but scalar testing, and use a recent result \cite{DGMZ07}
saying that for finite processes the preorders $\pdmMayleq$ and
$\pdmMustleq$ coincide with \plat{$\pdMayleq$} and \plat{$\pdMustleq$}.
Here we show that on {\pCSP} \plat{$\pdMayleq$} and
\plat{$\pdMustleq$} also coincide with $\pMayleq$ and $\pMustleq$.%
\footnote{However in the presence of divergence they are slightly different.}

\paragraph*{Simulation preorders:} In \Sect{sec:simulations} we
use the transitions $s \Ar{\mu} \Delta$ to define two co-inductive
preorders, the \emph{simulation} preorder $\forsimpreo$
\cite{Seg95,LSV03,DGHMZ07}, and the novel
\emph{failure simulation} preorder $\failsimpreo$ over \pCSP
processes. The latter extends the failure simulation preorder of
  \cite{vG93} to probabilistic processes.
Their definition uses a natural generalisation of the
transitions, first (Kleisli-style) to take the form $\Delta \Ar{\mu} \Delta'$, and then to
\emph{weak} versions $\Delta \dar{\mu} \Delta'$. The latter
preorder differs from the former in the use of a \emph{failure}
predicate $ s \nar{X}$, indicating that in the state $s$ none of the
actions in $X$ can be performed.

Both preorders are preserved by all the operators
in \pCSP, and are \emph{sound} with respect to the testing
preorders; that is $P \forsimpreo Q$ implies $P \pMayleq Q$
and $P \failsimpreo Q$ implies $P \pMustleq Q$.
For $\forsimpreo$ this was established in \cite{DGHMZ07}, and the
proofs for $\failsimpreo$ are similar. But \emph{completeness}, that the
testing preorders imply the respective simulation preorders, requires
some ingenuity. We prove it indirectly, involving a characterisation of
the testing and simulation preorders in terms of a modal logic.

\paragraph*{Modal logic:} Our modal logic, defined in
\Sect{sec:modal-logic}, uses finite conjunction $\bigwedge_{i\in I}\phi_i$,
the modality $\diam{a}\phi$ from the Hennessy-Milner Logic, and a novel
probabilistic construct $\bigoplus_{i\in I}p_i \cdot \phi_i$.
A satisfaction relation between processes and formulae then gives, in a
natural manner, a \emph{logical preorder} between processes:
$P \modalSpreo Q$ means that every $\SL$-formula satisfied by $P$ is
also satisfied by $Q$. We establish that $\modalSpreo$
coincides with $\forsimpreo$ and $\pMayleq$.

To capture failures, we add, for every set of actions $X$, a formula
$\refuse{X}$ to our logic, satisfied by any process which, after it
can do no further internal actions, can perform none of the actions in
$X$ either. The constructs $\bigwedge$, $\diam{a}$ and $\refuse{}$
stem from the modal characterisation of the non-probabilistic failure
simulation preorder, given in \cite{vG93}. We show that $\pMustleq$,
as well as $\failsimpreo$, can be characterised in a similar manner
with this extended modal logic.

\paragraph*{Proof strategy:}
We prove these characterisation results through two cycles of inclusions:
\vspace{-9pt}
$$\begin{array}{@{}l@{\;\,\;}c@{\;\,\;}l@{\;\,\;}c@{\;\,\;}l@{\;\,\;}c@{\;\,\;}l@{\;\,\;}c@{\;\,\;}l@{\;\,\;}c@{\;\,\;}l@{}}
  \modalSpreo  &\subseteq&  \forsimpreo  &\stackrel{\mbox{\scriptsize\cite{DGHMZ07}}}{\subseteq}&  \pMayleq  &\subseteq&  \pdMayleq  &\stackrel{\mbox{\scriptsize\cite{DGMZ07}}}{=}&  \pdmMayleq  &\subseteq&  \modalSpreo\\[1pt]
  \modalFSpreo &\subseteq&  \failsimpreo &\subseteq&  \pMustleq &\subseteq&  \pdMustleq &\stackrel{\mbox{\scriptsize\cite{DGMZ07}}}{=}&  \pdmMustleq &\subseteq&  \modalFSpreo\\[-6pt]
\multicolumn{2}{@{}c@{\;\,\;}}{\underbrace{~~~~~~~~~~~}}&
\multicolumn{2}{@{}c@{\;\,\;}}{\underbrace{~~~~~~~~~~~~~~}}&
\underbrace{~~~~~~~~~~}&
\multicolumn{2}{@{}c@{\;\,\;}}{\underbrace{~~~~~~~~~~~~~~~~}}&
\multicolumn{2}{@{}c@{\;\,\;}}{\underbrace{~~~~~~~~~~~~~~~~}}&
\multicolumn{2}{@{}c@{}}{\underbrace{~~~~~~~~~~~}}\\[-1pt]
\multicolumn{2}{@{}c@{\;\,\;}}{\mbox{\small\sl \Sect{sec:modal-logic}}} &
\multicolumn{2}{@{}c@{\;\,\;}}{\mbox{\small\sl \Sect{sec:simulations}}} &
  \mbox{\small\sl \Sect{sec:testing}} &
\multicolumn{2}{@{}c@{\;\,\;}}{\mbox{\small\sl \Sect{sec:state-vs-action}}} &
\multicolumn{2}{@{}c@{\;\,\;}}{\mbox{\small\sl \Sect{sec:vector}}} &
\multicolumn{2}{@{}c@{}}{\mbox{\small\sl \Sect{sec:chartests}}}
\end{array}\vspace{-3pt}$$
In \Sect{sec:modal-logic} we show that $P \modalSpreo Q$
implies $P \forsimpreo Q$ (and hence $P \pMayleq Q$), and likewise for
$\modalFSpreo$ and $\failsimpreo$; the proof involves constructing,
for each \pCSP process $P$, a \emph{characteristic formula} $\phi_P$.
To obtain the other direction, in \Sect{sec:chartests} we show how
every modal formula $\phi$ can be captured, in some sense, by a test
$T_\phi$; essentially the ability of a \pCSP process to satisfy $\phi$
is determined by its ability to pass the test $T_\phi$. We capture
the conjunction of two formulae by a probabilistic choice between the
corresponding tests; in order to prevent the results from these tests
getting mixed up, we employ the vector-based tests of \cite{Seg96}, so
that we can use different success actions in the separate probabilistic branches.
Therefore, we complete our proof by demonstrating that the state-based testing
preorders imply the action-based ones (\Sect{sec:state-vs-action})
and recalling the result from \cite{DGMZ07} that the action-based scalar
testing preorders imply the vector-based ones (\Sect{sec:vector}).

\paragraph*{Equations:}
It is well-known that may- and must testing for standard CSP can be
captured equationally \cite{DNH84,BHR84,henn}. In \cite{DGHMZ07} we
showed that most of the standard equations are no longer valid in
the probabilistic setting of \pCSP; we also provided
a set of axioms which are complete with respect to
(probabilistic) may-testing for the sub-language of \pCSP without
probabilistic choice. Here we extend this result, by
showing, in \Sect{sec:inequations}, that both $P \pMayleq Q$ and $P
\pMustleq Q$ can still be captured equationally over full \pCSP.
In the may case the essential (in)equation required is
\begin{equation*}
 a.(P \probc{p} Q) \Wide{\sqsubseteq} a.P \probc{p} a.Q
\end{equation*}
The must case is more involved: in the absence of the
distributivity of the external and internal choices over each other,
to obtain completeness we require a complicated inequational schema.

%-------------------------------------------------------------------------
\Section{Finite probabilistic CSP}\label{sec:pcsp}

\noindent
%% The set of actions is required to be finite, because later on we
%% make a characteristic test (a finite PCSP expression) out of ref(X)
%% by means of an external choice of all actions that cannot be done.
Let $\Act$ be a finite set of actions, ranged over by $a,b,\cdots$, which
processes can perform.  Then the finite probabilistic CSP
processes are given by the following two-sorted syntax:
\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*}
Here $P \probc{p} Q$, for $0< p < 1$,
represents a \emph{probabilistic choice} between $P$ and $Q$: with
probability $p$ it will act like $P$ and with probability $1\Minus p$ it
will act like $Q$.  Any process is a probabilistic combination of
state-based processes (the sub-sort $S$ above)
built by repeated application of the operator $\probc{p}$. The
state-based processes have a CSP-like syntax, involving the
stopped process $\Cnil$, action prefixing $a.\_\!\_$, \emph{internal-}
and \emph{external choices} $\intc$ and $\extc$,
and a \emph{parallel composition} $\Par{A}$ for $A\subseteq \Act$.

The process $P\intc Q$ will first do a so-called \emph{internal action} $\tau\mathop{\not\in}\Act$,
choosing \emph{nondeterministically} between $P$ and $Q$.
Therefore $\intc$, like $a.\_\!\_$\,, acts as a \emph{guard}, in the
sense that it converts any process arguments into a state-based process.

The process $P\extc Q$ on the other hand does not perform actions itself,
but merely allows its arguments to proceed, disabling one argument as
soon as the other has done a visible action. In order for this process
to start from a state rather than a probability distribution of states,
we require its arguments to be state-based as well; the
same applies to $\Par{A}$.
Expressions $P\extc Q$ and $P\Par{A} Q$ for processes $P$
and $Q$ that are \emph{not} state-based are therefore syntactic
sugar for an expression in the above syntax obtained by
distributing $\extc$ and $\Par{A}$ over $\probc{p}$.

Finally, the expression $P \Par{A} Q$, where $A \subseteq \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 $\tau$.
In addition $P$ and $Q$ may independently do any action from
$(\Act\mathord{\setminus} A)\cup\{\tau\}$.

We write \pCSP for the set of process terms defined by this
grammar, and \sCSP for the subset comprising only the state-based
process terms.
The full language of CSP \cite{BHR84,csp,OH86} has many more
operators; we have simply chosen a representative selection, and have added
probabilistic choice.
Our parallel operator is not a CSP primitive, but it can easily
be expressed in terms of them---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 convenience in defining the application of tests to processes.

As usual we may elide $\Cnil$; the prefixing
operator $a.\_\!\_$ binds stronger than any binary operator; and
precedence between binary operators is indicated via brackets
or spacing. We will also sometimes use indexed binary
operators, such as $\bigoplus_{i\in I}p_i\Cdot P_i$ with
$\sum_{i\in I}p_i=1$ and all $p_i>0$, and $\bigbox_{i \in I}P_i$.

The above intuitions are formalised
by an \emph{operational semantics} associating with each process
term a graph-like structure representing its possible reactions to
users' requests: we use a generalisation of labelled transition
systems \cite{ccs} that includes probabilities.

\bigskip
A (discrete) probability distribution over a set $S$ is a function
{$\Delta\!: S \rightarrow [0,1]$} with \mbox{$\sum_{s\in S}\! \Delta(s)=1$};
the \emph{support} of $\Delta$ is given by
$\support{\Delta} = \setof{s \inp S}{\Delta(s) > 0}$.
%% We only deal with distributions with finite support, because for
%% other ones we can't define a characteristic formula whose
%% characteristic test is a finite pCSP expression.
We write $\dist{S}$, ranged over by $\Delta, \Theta,\Phi$, for the set
of all  distributions over $S$ with finite support; these finite distributions
are sufficient for the results of this paper. We also write
$\pdist{s}$ to denote the point distribution assigning probability 1
to $s$ and 0 to all others, so that $\support{\pdist{s}} = \{s\}$.

For $\Delta$ a distribution over $S$ and function
\mbox{$f\!:S\mathbin\rightarrow X$} into a vector space $X$
(typically the reals%
%
\footnote{Other possibilities are tuples of reals, or distributions
over some set.}%
%
) we write $\bigoplus_{\!s \in S}\! \Delta_s \Cdot f_{\!s}$ or $\Exp{\Delta}(f)$
for $\sum_{s\in S} \Delta(s) \Cdot f(s)$, the \emph{weighted average}
of the $f_s$, or \emph{expected value} of $f$. When $p\inp\,[0,1]$, we
also write $f_1 \probc{p} f_2$ for $p\,\Cdot f_1 + (1\Minus  p)\,\Cdot f_2$.
More generally, for function $F: S \rightarrow \subs{X}$ with
$\subs{X}$ being the collection of non-empty subsets of $X$, we define
$\Exp{\Delta}{F} \Defs \setof{\Exp{\Delta}(f)}{f \IN F}$, where  $f  \IN F$ means that $f$ is
a \emph{choice function} with $f(s)\inp F(s)$ for all $s\inp S$.

We now give the probabilistic generalisation (pLTSs) of labelled transition systems (LTSs):

\begin{definition}
A \emph{probabilistic labelled transition system} is a triple
$\langle S, \Act_\tau, \rightarrow \rangle$, where
\begin{enumerate}[(i)]
\vspace{-1ex}
\item $S$ is a set of states
\vspace{-1ex}
\item $\Act_\tau$ is a set of actions \Act, augmented by $\tau\mathop{\not\in}\Act$; we let $a$ range over $\Act$ and $\mu$ over $\Act_\tau$.
\vspace{-1ex}
\item relation $\rightarrow$ is a subset of $S \times \Act_\tau \times \dist{S}$.
\vspace{-1ex}
\end{enumerate}
As with LTSs, we usually write $s \Ar{\mu} \Delta$ for
$(s,\mu,\Delta) \inp \mathord\rightarrow$,
$s\ar{\mu}$ for $\exists\Delta: s\Ar{\mu}\Delta$ and
$s\!\rightarrow$ for $\exists\mu\!: s\,\Ar{\mu}$.
An LTS may be viewed as a degenerate pLTS, one in which only point
distributions are used.
\end{definition}
We now define the operational semantics of \pCSP by means of
a particular pLTS  $\langle \sCSP, \Act_\tau, \rightarrow \rangle$,
constructed by taking \sCSP to be the set of states
and interpreting \pCSP processes $P$ as distributions $\Op{P} \in \dist{\sCSP}$
as follows:
$$\begin{array}{r@{~~\Defs~~}l}
\Op{s} & \pdist{s} ~~~~~~\mbox{for } s \inp\sCSP\\
\Op{P \probc{p} Q} & \Op{P} \probc{p} \Op{Q}\;.
\end{array}$$
Note that for each $P\in\pCSP$ the distribution $\Op{P}$ is finite,
i.e.\ it has finite support.
The definition of the relations $\ar{\mu}$ is given in
\Fig{fig:opsem}.
\begin{figure}[t]
\vspace{-1em}
  \begin{align*}
    &\slinfer[\Rlts{action}]{a.P \ar{a} \Op{P}}
\\[3pt]
    & \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.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}
\\
   &\linfer[\Rlts{ext.i.l}]{s_1 \ar{\tau} \Delta}
                 {s_1 \extc s_2 \ar{\tau} \Delta \extc {s_2}}
   && \linfer[\Rlts{ext.i.r}]{s_2 \ar{\tau} \Delta}
                 {s_1 \extc s_2 \ar{\tau} {s_1} \extc \Delta}
\\
  &\linferSIDE[\Rlts{par.l}]{s_1 \ar{\mu} \Delta}
                 {s_1 \Par{A} s_2 \ar{\mu} \Delta \Par{A} {s_2}}
                 {~~~~~\mu \mathop{\not\in} A}
   && \linferSIDE[\Rlts{par.r}]{s_2 \ar{\mu} \Delta}
                 {s_1 \Par{A} s_2 \ar{\mu} {s_1} \Par{A} \Delta}
                 {~~~~~\mu \mathop{\not\in} A}
\\
  &\makebox[4.5cm][l]{$\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\inp A}$}
 \end{align*}
\caption{Operational semantics of $\mathsf{pCSP}$\label{fig:opsem}.}
\end{figure}
These rules are very similar to the
standard ones used to interpret CSP as an LTS \cite{OH86}, but modified
so that the result of an action is a distribution.
We sometimes write $\tau.P$ for $P\intc P$, thus giving $\tau.P \ar{\tau} \Op{P}$.

%-------------------------------------------------------------------------
\Section{Testing \pCSP processes}\label{sec:testing}

\noindent
A \emph{test} is a \pCSP process except that it may have subterms
$\omega.P$ for fresh $\omega\mathop{\not\in}\Act_\tau$, a special action
reporting success; and the operational semantics above
is extended by treating $\eureka$ like any other action from $\Act$.
To apply test $T$ to process $P$ we form the process
\mbox{$T \parT P$} in which \emph{all} visible actions of $P$ must synchronise with $T$,
and define a set of testing outcomes
$\Apply(T,P)$ where each outcome, in $[0,1]$, arises from a resolution
of the nondeterministic choices in \mbox{$T \parT P$} and gives the
probability that this resolution will reach a \emph{success state}, one in which $\omega$ is possible.

To this end, we inductively define a \emph{results-gathering} function
$\resultsN : S \rightarrow \subs{[0,1]}$; it extends to type $\dist{S}
\rightarrow \subs{[0,1]}$ via the convention $\results{\Delta} \Defs
\Exp{\Delta}\resultsN$.
\[\begin{array}{@{}r@{~\Defs~}l@{}}
  \results{s} &
  \begin{cases}
                 \sset{1} &\text{if $s \ar{\eureka}$}, \\
\bigcup \setof{\results{\Delta}}{s \ar{\tau} \Delta}
                     &\text{if $s \nar{\eureka},\;s \ar{\tau}$},\\
                 \sset{0} &\text{if $s\!\not\rightarrow{}$}
  \end{cases}
\end{array}\]
Note that these choices are exhaustive because \mbox{$T \parT P$} has only $\tau,\eureka$ actions,
and that $\resultsN$ is well defined when applied to finite,
loop-free pLTSs, such as the one of \pCSP.

\begin{definition}\label{d1659}
For any \pCSP process $P$ and test $T$, define
$$\Apply(T,P) ~\Defs~ \resultsN{\Op{T\mathbin{\parT}P}}~.$$
\end{definition}
%
With this definition, the general testing framework of \cite{DNH84}
yields two testing preorders for \pCSP, one based on \emph{may}
testing, written $P \pMayleq Q$, and the other on \emph{must} testing,
written $P \pMustleq Q$.

\begin{definition}\label{d1700}
The \emph{may-} and \emph{must} preorders are given by
\[
 \begin{array}{@{}r@{\hspace{.7em}}c@{\hspace{.7em}}l@{}}
  P \pMayleq Q &\textrm{iff}& \text{$\forall$
  tests $T$: } \Apply(T,P) \Hleq \Apply(T,Q) \\
  P \pMustleq Q &\textrm{iff}& \text{$\forall$
  tests $T$: } \Apply(T,P) \Sleq \Apply(T,Q)
 \end{array}
\]
with $\Hleq,\Sleq$ the Hoare, Smyth preorders on $\subsN{
[0,1]}$.%
\footnote{The Hoare order is defined by $X \Hleq Y$ iff $\forall
  x\inp X\!\! : \exists y\inp Y\!\! : x \leq y$, similarly the Smyth order
  by $X \Sleq Y$ iff $\forall y\inp Y \!\!: \exists x\inp X\!\! : x \leq y$.}
\end{definition}

%-------------------------------------------------------------------------
\Section{Simulation and failure simulation}\label{sec:simulations}

\noindent
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 \!\lift{\aRel}\! \Theta$ whenever there is an index
set $I$ and $p\inp\dist{I}$ such that
\begin{enumerate}[(i)]
\vspace{-1ex}
\item
$\Delta = \bigoplus_{i\in I}{p_i \Cdot \pdist{s_i}}$~,
\vspace{-1ex}
\item
For each $i \inp I$ there is a distribution $\Phi_i$ s.t.
$s_i \aRel \Phi_i$~,
\vspace{-1ex}
\item
$\Theta = \bigoplus_{i \in I} {p_i \Cdot \Phi_i}$~.
\vspace{-1ex}
\end{enumerate}
For notational convenience, the lifted versions of the transition
relations $\ar\alpha$ for $\alpha\inp\Act_\tau$ are again denoted $\ar\alpha$.

We write $s \hatar{\tau} \Delta$ if either $s \ar{\tau}
\Delta$ or $\Delta = \pdist{s}$; again
\mbox{$\Delta_1 \hatar{\tau} \Delta_2$} denotes the lifted relation.
Thus e.g.\ we have\vspace{6pt}
$\Op{(a \intc b) \probc{\frac{1}{2}} (a \intc c)}
  \;\hatar{\tau}\; \Op{a \probc{\frac{1}{2}} ((a\intc b) \probc{\frac{1}{2}} c)}$
\hfill\cite{DGHMZ07}.\vspace{6pt}

We now define the weak transition relation $\dar{\hat\tau}$ as the
transitive and reflexive closure $\ar{\hat\tau}^*$ of $\ar{\hat\tau}$,
while for $a\neq \tau$ $\Delta_1 \dar{\hat{a}} \Delta_2$ denotes
$\Delta_1 \dar{\hat\tau}\ar{a}\dar{\hat\tau} \Delta_2$.
We write $s\nar{X}$ with $X\subseteq\Act$ when $\forall \alpha\in
X\cup\sset{\tau}: s\nar{\alpha}$, and $\Delta\nar{X}$ when $\forall
s\in\support{\Delta}: s\nar{X}$.

\begin{definition}\label{def:failsim}
A relation $\mathord{\aRel} \subseteq S \mathop{\times} \dist{S}$ is
said to be a
 \emph{failure simulation} if for all $s,\Theta,\mu,\Delta$ we have
 that
\begin{itemize}
\vspace{-1ex}
\item $s \aRel \Theta \land s \ar{\mu}  \Delta$ implies
 $\exists \Theta'\!:\Theta \dar{\hat{\mu}} \Theta' \land
  \Delta \lift{\aRel} \Theta'$
\vspace{-1ex}
\item $s \aRel \Theta \land s \nar{X}  \Delta$ implies
 $\exists \Theta'\!:\Theta \dar{\hat{\tau}} \Theta' \land
  \Theta' \nar{X}$.
\end{itemize}
We write $s \failsim \Theta$ to mean that there is some failure simulation
$\aRel$ such that $s \aRel \Theta$. Similarly, we define
\emph{simulation} and $s \forsim \Theta$ by dropping the second clause
in \Def{def:failsim}.
\end{definition}

\begin{definition}\label{def:simulation preorder}
The \emph{simulation preorder} $\forsimpreo$ and \emph{failure simulation
preorder} $\failsimpreo$ on \pCSP are defined as follows:
\[
 \begin{array}{@{}rcl@{}}
  P \forsimpreo Q &\textrm{iff}& \Op{Q} \dar{\hat{\tau}} \Theta
  \text{ for some $\Theta$ with } \Op{P} \liftforsim \Theta \\
  P \failsimpreo Q &\textrm{iff}& \Op{P} \dar{\hat{\tau}} \Theta
  \text{ for some $\Theta$ with } \Op{Q} \liftfailsim \Theta\,.
 \end{array}
\]
(Note the opposing directions.)
The kernels of $\forsimpreo$ and $\failsimpreo$ are
called \emph{(failure) simulation equivalence}, denoted
$\forsimequiv$ and $\failsimequiv$, respectively.
\end{definition}
%
We have already shown in \cite{{DGHMZ07}} that $\forsimpreo$ is a
precongruence and that it implies $\pMayleq$. Similar results
can be established for $\failsimpreo$ as well. We summarise these facts as follows:
\begin{proposition}\label{thm:cong}
Suppose $\mathord{\sqsubseteq}\in\sset{\forsimpreo, \failsimpreo}$.
Then $\sqsubseteq$ is a preorder, and if $P_i \sqsubseteq Q_i$ for $i =
1,2$ then $a.P_1 \sqsubseteq a.Q_1$ for $a\inp\Act$ and
  $P_1 \odot P_2 ~\sqsubseteq~ Q_1 \odot Q_2~$ for
  $\odot\inp\,\{\intc,\,\extc,\,\probc{p},\,\Par{A}\}$.
\end{proposition}
\begin{proof}
The case $\forsimpreo$ was proved in
\cite[Cor.~6.10 and Thm.~6.13]{DGHMZ07};
the case $\failsimpreo$ is analogous.
\end{proof}

\begin{theorem}\label{t:simtest}\mbox{}
\begin{enumerate}
\vspace{-1ex}
\item If $P \forsimpreo Q$ then $P \pMayleq Q$.
\vspace{-1ex}
\item If $P \failsimpreo Q$ then $P \pMustleq Q$.
\vspace{-1ex}
\end{enumerate}
\end{theorem}
\begin{proof}
The first clause was proved in \cite[Thm.~6.17]{DGHMZ07}; the
second can be shown similarly.
\end{proof}
The next four sections are devoted to obtaining the converse.

%-------------------------------------------------------------------------
\Section{State- versus action-based testing}\label{sec:state-vs-action}

\noindent
Much work on testing \cite{DNH84,WL92,DGHMZ07} uses success
\emph{states} marked by outgoing $\eureka$-actions; in other work
\cite{Seg96,DGMZ07}, however, it is the \emph{actual execution} of
$\eureka$ that constitutes success. The former, \emph{state-based}
testing, leads to the preorders we defined in
\Sect{sec:testing}; the latter, \emph{action-based} testing, leads
to slightly different preorders $\pdMayleq$ and $\pdMustleq$. Without
probability there is no difference between $\dMayleq$ and
$\rMayleq$; but possible divergence makes $\rMustleq$ strictly more
discriminating than $\dMustleq$, and in fact $\rMustleq$ coincides
with CSP refinement based on failures and divergences
\cite{BHR84,csp,OH86}. The action-based approach is formalised
as in the state-based approach,  via a suitable $\DresultsN$:
\[\begin{array}{@{}r@{\,\Defs\,}l@{}}
\Dresults{s}
  &
  \begin{cases}
\bigcup \setof{\!\Dresults{\Delta}\!}{\!s \Ar{\tau} \Delta\!} \cup
        \setof{\!1\!}{\!s \Ar{\eureka}}
                     &\text{if $s\!\rightarrow$}\\
                 \sset{0} &\text{\hspace{-1.4em}otherwise}
  \end{cases}
\end{array}\]

\begin{proposition}\label{p:action-based}\mbox{}
\begin{enumerate}
\vspace{-1ex}
\item If $P \pMayleq Q$ then $P \pdMayleq Q$.
\vspace{-1ex}
\item If $P \pMustleq Q$ then $P \pdMustleq Q$.
\vspace{-1ex}
\end{enumerate}
\end{proposition}
\begin{proof}
For any test $\Overline{T}$ construct $T$ by replacing each subterm $\omega.Q$ by $\tau.\omega$; then $\resultsN{\Op{T\parT P}} = \DresultsN{\Op{\Overline{T}\parT P}}$ for
all \pCSP processes $P$.
\end{proof}
%
In fact we use the action-based preorders  in
\Thm{t:simtest-reverse} below, a (quasi-, thus) converse of
\Thm{t:simtest}; but with \Prop{p:action-based} above the two kinds
of preorders become identified so that Thms.~\ref{t:simtest}
and~\ref{t:simtest-reverse} are converse to each other.

\begin{theorem}\label{t:simtest-reverse}\mbox{}
\begin{enumerate}
\vspace{-1ex}
\item If $P \pdMayleq Q$ then $P \forsimpreo Q$.
\vspace{-1ex}
\item If $P \pdMustleq Q$ then $P \failsimpreo Q$.
\end{enumerate}
\end{theorem}
%
We set this theorem as our goal in the next three sections.

%-------------------------------------------------------------------------
\Section{Vector-based testing}\label{sec:vector}

\noindent
This section describes another variation on testing,
a richer testing framework due to Segala
\cite{Seg96}, in which countably many success actions exist: the
application of a test to a process yields a set of \emph{vectors} over
the real numbers, rather than a set of scalars. The resulting
action-based testing preorders will serve as a stepping stone in proving
\Thm{t:simtest-reverse}.

Let $\Omega$ be a \emph{set} of fresh success actions with
$\Omega\cap\Act_\tau=\emptyset$. An $\Omega$-test is again a \pCSP
process, but this time allowing subterms $\omega.P$ for any
$\omega\inp\Omega$.  Applying such a test to a process yields a non-empty
set of test outcome-\emph{tuples} $\MDApply(T,P) \subseteq [0,1]^\Omega$. Each
\emph{tuple} arises from a resolution within $T\parT P$ of
nondeterministic choices into probabilistic choices,
and its $\omega$-component gives the probability that this
resolution will perform the success action $\omega$.

For vectors we again inductively define a results-gathering function
$\MDresultsN : S \rightarrow \subsN{[0,1]^\Omega}$; it extends to
type \plat{$\dist{S} \rightarrow \subsN{[0,1]^\Omega}$} via
$\MDresults{\Delta} \Defs \Exp{\Delta}\MDresultsN$ just as
$\resultsN$ and $\DresultsN$ did.
First, for any $\alpha$ define $\alpha!:[0,1]^\Omega \rightarrow
[0,1]^\Omega$ so that $\alpha!o(\omega)$ becomes 1 if $\omega\Eq\alpha$
but remains $o(\omega)$ otherwise; this function lifts to sets
$O\subseteq[0,1]^\Omega$ as usual, via $\alpha!O\Defs\{\alpha!o\mid o\inp O\}$.
Now we define
\[\begin{array}{@{}r@{~~\Defs~~}l@{}}
\MDresults{s} &
\begin{cases}
\CClose \bigcup \setof{\alpha!(\MDresults{\Delta})}{s \Ar{\alpha} \Delta}
                     &\text{if $s\rightarrow$}\\
                 \sset{\vec{0}} &\text{\hspace{-1.4em}otherwise}
\end{cases}
\end{array}\]
where $\vec0 \in [0,1]^\Omega$ is given by $\vec0(\omega)=0$ for all
$\omega\in\Omega$, and the \emph{convex closure} $\CClose X$ of a set
$X$ is defined
\[\textstyle
\CClose X \Defs \setof{\bigoplus_{i\in I}p_i\,\Cdot\, o_i }{p\inp\dist{I}
    \mbox{ and } o: I\rightarrow X}~ .
\]

We extend our earlier results-gathering definitions so that
$\Cresults{s}\Defs\CClose\results{s}$ and
$\CDresults{s}\Defs\CClose\Dresults{s}$.
Note that in case $\Omega\Defs\{\eureka\}$ we have $\MDresultsN =
\CDresultsN$, and the convex-closing preorders based on
$\CresultsN,\CDresultsN$ coincide with the simpler ones based on $\resultsN,\DresultsN$. Thus convex closure matters only for proper vectors, as explained in the remark following
\Def{def:vector-testing}.

In \cite{DGMZ07} the results-gathering function $\MDresultsN$
with $\Omega= \{\omega_1,\omega_2,\cdots\}$ was
called simply $\mathbb W$ (because
action-based/ convex/vector-based testing was assumed there throughout, making the
$\widehat{\cdot}_{\scriptscriptstyle\updownarrow}^{\raisebox{-.2em}{\scriptsize$~\Omega$}}$-indicators
superfluous); and it was defined in terms of a formalisation of the
notion of a resolution. The inductive definition above yields the same
results.

\begin{definition}\label{def:vector-testing}
For any \pCSP process $P$ and $\Omega$-test $T$, let
$$\MDCApply(T,P) ~\Defs~ \MDresultsN{\Op{T \mathbin{\parT} P}}~.$$
The \emph{vector-based} \emph{may-} and \emph{must} preorders are given by
\[
 \begin{array}{@{}r@{\hspace{.7em}}c@{\hspace{.7em}}l@{}}
  P \pdmMayleq Q &\textrm{iff}& \text{$\forall\,
  \Omega$-tests $T$: } \MDCApply(T,P) \Hleq \MDCApply(T,Q) \\
  P \pdmMustleq Q &\textrm{iff}& \text{$\forall\,
  \Omega$-tests $T$: } \MDCApply(T,P) \Sleq \MDCApply(T,Q)
 \end{array}
\]
where $\Hleq$ and $\Sleq$ are the Hoare- and Smyth preorders on
$\subsN{[0,1]^\Omega}$ generated from $\leq$ index-wise on $[0,1]^\Omega$ itself.
\end{definition}

\noindent{\bf Remark:}
For proper vector-based testing, convex closure matters, as it allows internal choice to simulate probabilistic choice \cite{HSM97}. Consider the following two processes
\[P:= a \intc b \intc (a \probc{\frac{1}{2}} b)\quad
 {\rm \ and\ } \quad Q := a \intc b.\]
It is obvious that $P \forsimpreo Q$,
and from \Thm{t:simtest} it therefore follows that
$P \pMayleq Q$. However if $\Omega=\sset{\omega_1,\omega_2}$
and we remove the convex closure in the
definition of $\MDresultsN$, then with the test  $T:=  a.w_1 \extc
b.w_2$  we would have
\begin{align*}
\MDApply(T, P) & = \sset{(1,0), (0,1), (0.5, 0.5)}\\
 \MDApply(T, Q) & = \sset{(1,0), (0,1)}
\end{align*}
and so $\MDApply(T, P) \not\Hleq \MDApply(T, Q)$. However, their convex
closures $\MDCApply(T, P)$ and $\MDCApply(T, Q)$ \emph{are} related under
the Hoare preorder.
\hfill$\Box$

The testing preorders of \cite{Seg96} are obtained by taking
$\Omega$ to be a countably infinite set, whereas the preorders
$\pdMayleq$ and $\pdMustleq$ of \Sect{sec:state-vs-action} were
obtained by taking $\Omega$ to be the singleton set $\{\eureka\}$.
In \cite{DGMZ07} we established that for our finite \pCSP\ processes the two coincide:

\begin{theorem}\label{t:multiUni}\cite{DGMZ07}.
\begin{enumerate}
\vspace{-1ex}\item $P \pdmMayleq Q$ iff $P \pdMayleq Q$
\vspace{-1ex}\item $P \pdmMustleq Q$ iff $P \pdMustleq Q$. \hfill{$\Box$}
\end{enumerate}
\end{theorem}
Thus, with the \emph{if}-direction of \Thm{t:multiUni}, for
\Thm{t:simtest-reverse} it will suffice to show that \plat{$P \pdmMayleq Q$}
implies $P \forsimpreo Q$ and $P \pdmMustleq Q$ implies $P \failsimpreo Q$.
The crucial characteristics of $\MDCApply$ needed for that implication
are summarised in this lemma (proof omitted):

\begin{lemma}\label{lem:inductive}
Let $P$ be a \pCSP process, and $T,T_i$ be tests.
\begin{enumerate}
\item
  $\outc \in \MDCApply(\omega,P)$ iff $\outc=\vec{\eureka}$.
\item
  Suppose the action $\omega$ does not occur in the test $T$.\\
  Then $\outc\in\MDCApply(\omega \mathop\Box a.T,P)$ with $o(\omega)=0$ iff
  there is a $\Delta\inp \dist{\sCSP}$
  with $\Op{P}\dar{\hat a}\Delta$ and $\outc\in\MDCApply(T,\Delta)$.
\item $\vec0\in\MDCApply(\bigbox_{a\in X}a.\omega,P)$ iff
  $\exists\Delta:\Op{P}\dar{\hat\tau}\Delta\nar{X}$.
\item $\outc\in\MDCApply(\bigoplus_{i\in I} p_i\Cdot T_i,P)$ iff
  $\outc=\sum_{i\in I}p_i\outc_i$ for certain $\outc_i\in\MDCApply(T_i,P)$.
\item $\outc\inp\MDCApply(\bigsqcap_{i\in I}\!T_i,P)$ iff for all $i\inp I$
  there are $p_i\inp\,[0,1]$ and $\Delta_i\inp\dist{\sCSP}$ such that
  $\Op{P}\dar{\hat\tau}\bigoplus_{i\in I}p_i\Cdot\Delta_i$ and
  $\outc=\sum_{i\in I}p_i\outc_i$ for certain
  $\outc_i\in\MDCApply(T_i,\Delta_i)$.
\end{enumerate}
Here $\vec{\eureka}\in [0,1]^\Omega$ is given by
$\vec{\eureka}(\eureka) = 1$ and $\vec{\eureka}(\eureka') = 0$ for
$\eureka'\neq\eureka$.
\hfill{$\Box$}
\end{lemma}
In writing $\MDCApply(T,\Delta)$ above we treat a distribution
$\Delta$ as the \pCSP expression $\bigoplus_{s\in \support{\Delta}}\Delta_s\Cdot s$;
and as usual we define $\MDCApply(T,\Delta) \Defs \Exp{\Delta}\MDCApply(T, \_\!\_)$.

%-------------------------------------------------------------------------
\Section{Modal logic}\label{sec:modal-logic}

\noindent
Our next step towards \Thm{t:simtest-reverse} is to define a set $\FSL$ of modal formulae, inductively, as follows:
\begin{itemise}
\item $\diam{a}\phi \in\FSL$ when $\phi\inp \FSL$ and $a\inp \Act$,
\item $\refuse{X} \in \FSL$ when $X\subseteq \Act$,
\item $\bigwedge_{i\in I}\phi_i\in\FSL$ when $\phi_i \inp \FSL$ for all
  $i\inp I$, with $I$ finite
\item and $\bigoplus_{i\in I}p_i\Cdot\phi_i \in \FSL$ when $p_i\inp [0,1]$ and
  $\phi_i \inp \FSL$ for all $i\inp I$, with $I$ a finite index set,
  and $\sum_{i\in I}p_i=1$.
\end{itemise}
We often write $\phi_1 \probc{p} \phi_2$ for
\plat{$\bigoplus_{i\in \{1,2\}}p_i\Cdot\phi_i$} with $p=p_1$, and
$\phi_1 \land \phi_2$ for $\bigwedge_{i\in \{1,2\}}\phi_i$
and finally $\top$ for $\bigwedge_{i\in \emptyset}\phi_i$.

The \emph{satisfaction relation} $\models\:\subseteq \dist{\sCSP} \times \FSL$ is given by:
\begin{itemise}
\item $\Delta\models \diam{a}\phi$ iff there is a $\Delta'$
  with $\Delta \dar{\hat a}\Delta'$ and $\Delta'\models \phi$,
\item $\Delta\models \refuse{X}$ iff there
  is a $\Delta'$ with $\Delta \dar{\hat\tau}\Delta'$ and \plat{$\Delta'\nar{X}$},
\item $\Delta\models\bigwedge_{i\in I}\phi_i$ iff
  $\Delta\models\phi_i$ for all $i\inp I$
\item and $\Delta\models\bigoplus_{i\in I}p_i\Cdot\phi_i$ iff there are $\Delta_i\!\in \dist{\sCSP}$, for all $i\inp I$,
with $\Delta_i\models \phi_i$,
  such that $\Delta \dar{\hat\tau}\bigoplus_{i\in I}p_i\Cdot\Delta_i$.
\end{itemise}
Let $\SL$ be the subclass of $\FSL$ obtained by skipping the $\refuse{X}$ clause.
We write $P \modalSpreo Q$ just when $\Op{P}\models\phi$ implies
$\Op{Q}\models\phi$ for all $\phi\inp \SL$, and $P\modalFSpreo Q$
just when $\Op{P}\models\phi$ is implied by $\Op{Q}\models\phi$ for
all $\phi\inp \FSL$. (Note the opposing directions.)

\begin{definition}
The \emph{characteristic formula} $\phi_s$ or $\phi_\Delta$
of a process $s\inp\sCSP$ or $\Delta\inp\dist\sCSP$ is defined inductively:
\begin{itemise}
\item $\phi_s \Defs \bigwedge_{s \ar{a} \Delta} \diam{a}\phi_\Delta \land \refuse{\{a \mid s \nar{a}\}}$
       if $s\nar{\tau}$,
\item $\phi_s \Defs \bigwedge_{s \ar{a} \Delta} \diam{a}\phi_\Delta \land
       \bigwedge_{s \ar{\tau} \Delta} \phi_\Delta$ otherwise,
\item $\phi_\Delta \Defs \bigoplus_{s \in \support\Delta} \Delta(s)\Cdot\phi_s$.
\end{itemise}
Here the conjunctions $\bigwedge_{s \ar{a} \Delta}$ range over suitable pairs $a,\Delta$, and $\bigwedge_{s \ar{\tau} \Delta}$ ranges over suitable $\Delta$.
\end{definition}
Write $\phi\Rrightarrow \psi$ with $\phi,\psi\inp\FSL$ if for each
  distribution $\Delta$ one has $\Delta \models \phi$ implies $\Delta \models \psi$.
  Then it is easy to see that $\phi_{\overline{s}}\Lleftarrow\!\!\!\Rrightarrow \phi_s$
  and $\bigwedge_{i\in I}\phi_i \Rrightarrow \phi_i$ for any $i\inp I$.

The following property can be established by an easy inductive proof.
\begin{lemma}\label{lem-characteristic formulae}
For any $\Delta\inp\dist\sCSP$ we have
$\Delta \models \phi_\Delta$.
\hfill$\Box$
\end{lemma}
It and the following lemma help to prove \Thm{thm-characteristic formulae}.

\begin{lemma}\label{characteristic formulae}
For any processes $P,Q\in\pCSP$ we have that
$\Op{P} \models \phi_{\Ops{Q}}$ implies $P \failsimpreo Q$.
\end{lemma}

\begin{proof}
Define $\aRel$ by $s \aRel \Theta$ iff $\Theta \models \phi_s$. We first show that
\begin{equation}\label{eq:modal}
\Theta \models \phi_\Delta ~~\mbox{implies}~~ \exists \Theta':
\Theta\dar{\hat\tau}\Theta' \land \Delta\mathrel{\overline\aRel}\Theta'.
\end{equation}
Suppose $\Theta \models \phi_\Delta$
with $\phi_\Delta = \bigoplus_{i\in I}p_i\Cdot\phi_{s_i}$,
so that we have $\Delta = \bigoplus_{i\in I}p_i\Cdot\pdist{s_i}$ and
for all $i\inp I$ there are $\Theta_i\inp \dist{\sCSP}$ with
$\Theta_i\models \phi_{s_i}$ such that
$\Theta \dar{\hat\tau}\Theta'$ with
\plat{$\Theta'\Defs\bigoplus_{i\in I}p_i\Cdot\Theta_i$}.
Since $s_i\aRel\Theta_i$ for all $i\inp I$ we have
$\Delta\mathrel{\overline\aRel}\Theta'$.

Now we show that $\aRel$ is a failure simulation.
\begin{itemise}
\item Suppose ${s} \aRel \Theta$ and $s
  \ar{\tau} \Delta$. Then $\phi_{s} \Rrightarrow \phi_\Delta$, so
  $\Theta \models \phi_{\Delta}$. Now apply (\ref{eq:modal}).
\item Suppose $s \aRel \Theta$ and $s
  \ar{a} \Delta$ with $a\inp A$. Then $\phi_{s}
  \Rrightarrow \diam{a}\phi_\Delta$, so $\Theta \models
  \diam{a}\phi_{\Delta}$. Hence $\exists\Theta'$ with $\Theta
  \dar{\hat a} \Theta'$ and $\Theta' \models \phi_{\Delta}$. Now apply
  (\ref{eq:modal}).
\item Suppose ${s} \aRel \Theta$ and
  \plat{$s\nar{X}$} with $X\subseteq A$. Then $\phi_{{s}}
  \Rrightarrow \refuse{X}$, so $\Theta\models\refuse{X}$.
  Hence $\exists \Theta'$ with $\Theta \dar{\hat\tau}
  \Theta'$ and \plat{$\Theta'\nar{X}$}.
\end{itemise}
Thus we have $\Theta\models\phi_s$ implies $s\failsim \Theta$.
Using \Eqn{eq:modal} with $\Op{P} \models \phi_{\Ops{Q}}$ gives
$P \failsimpreo Q$ via \Def{def:simulation preorder}.
\end{proof}

\begin{theorem}\label{thm-characteristic formulae}\mbox{}
\begin{enumerate}
\vspace{-1ex}
\item If $P \modalSpreo Q$ then $P \forsimpreo Q$.
\vspace{-1ex}
\item If $P \modalFSpreo Q$ then $P \failsimpreo Q$.
\end{enumerate}
\end{theorem}

\begin{proof}
Suppose $P\modalFSpreo Q$. By \Lem{lem-characteristic formulae}
we have $\Op{Q}\!\models\!\phi_{\Ops{Q}}$ and hence $\Op{P}\models\phi_{\Ops{Q}}$.
\Lem{characteristic formulae} gives $P\failsimpreo Q$.

For the $\modalSpreo$ case, omit $\refuse{X}$ from the definition of a
characteristic formula and begin with $\Op{P}\!\models\!\phi_{\Ops{P}}$.
The counterpart of \Lem{characteristic formulae} now says that
$\Op{Q}\models\phi_{\Ops{P}}$ implies $P \forsimpreo Q$.
\end{proof}

%-------------------------------------------------------------------------
\Section{Characteristic tests}\label{sec:chartests}

\noindent
Our final step towards \Thm{t:simtest-reverse} is taken in this section, where we show that every modal formula $\phi$ can
be characterised by a vector-based test $T_\phi$ such that any \pCSP process satisfies $\phi$ just when it passes the test $T_\phi$.

\begin{lemma}\label{lem:char tests}
For every $\phi\inp\FSL$ there exists a pair $(T_\phi,v_\phi)$ with
$T_\phi$ an $\Omega$-test and $v_\phi \in [0,1]^\Omega$, such that
\begin{equation}\label{eq:chartest}
\Delta\models\phi \Wide{\Leftrightarrow} \exists o \in
\MDCApply({T_\phi,\Delta}):~o\leq v_\phi
\end{equation}
for all $\Delta\inp\dist{\sCSP}$, and in case $\phi\in\SL$ we also have
\begin{equation}\label{eq:chartestmay}
\Delta\models\phi \Wide{\Leftrightarrow} \exists o \in
\MDCApply({T_\phi,\Delta}):~o\geq v_\phi\,.
\end{equation}
\end{lemma}
$T_\phi$ is called a \emph{characteristic test} of $\phi$ and $v_\phi$
its \emph{target value}.

\begin{proof}
First of all note that if a pair $(T_\phi,v_\phi)$ satisfies the
requirements above, then  any pair obtained from $(T_\phi,v_\phi)$
by bijectively renaming the elements of $\Omega$ also satisfies these
requirements. Hence a characteristic test can always be chosen in such
a way that there is a success action $\omega\inp\Omega$ that does not
occur in (the finite) $T_\phi$. Moreover, any countable collection of characteristic
tests can be assumed to be \emph{$\Omega$-disjoint}, meaning that no
$\omega\inp\Omega$ occurs in two different elements of the collection.

The required characteristic tests and target values are obtained as
follows.
\begin{itemise}
\item Let $\phi\Eq\top$. Take $T_\phi \Defs \omega$ for some
  $\omega\inp\Omega$, and $v_\phi\!\Defs\vec\omega$.
\item Let $\phi=\diam{a}\psi$. By induction, $\psi$
  has a characteristic test $T_\psi$ with target value $v_\psi$.
  Take $T_\phi \Defs \omega \mathop\Box a.T_\psi$ where
  $\omega\inp\Omega$ does not occur in $T_{\psi}$,
  and $v_\phi \Defs v_\psi$.
\item Let $\phi=\refuse X$ with $X\subseteq\Act$.
  Take $T_\phi \Defs \bigbox_{a\in X}a.\omega$ for some $\omega\inp\Omega$,
  and $v_\phi = {\vec 0}$.
\item Let $\phi=\bigwedge_{i\in I}\phi_i$ with $I$
  a finite and non-empty index set. Choose a $\Omega$-disjoint family
  $(T_i,v_i)_{i\in I}$ of characteristic tests $T_i$ with target values
  $v_i$ for each $\phi_i$.  Furthermore, let $p_i\inp\,(0,1]$ for $i\inp
  I$ be chosen arbitrarily such that $\sum_{i\in I}p_i=1$.  Take
  $T_\phi \Defs \bigoplus_{i\in I}p_i\Cdot T_{i}$ and
  $v_\phi \Defs \sum_{i\in I}p_iv_{i}$.
\item Let $\phi=\bigoplus_{i\in I}p_i\Cdot\phi_i$. Choose a $\Omega$-disjoint family
  $(T_i,v_i)_{i\in I}$ of characteristic tests $T_i$ with target values
  $v_i$ for each $\phi_i$, such that there are distinct success actions
  $\omega_i$ for $i\inp I$ that do not occur in any of those tests.
  Let \plat{$T'_i \Defs T_i \mathop{_\frac{1}{2}\!\oplus} \omega_i$} and
  \plat{$v'_i\Defs\frac{1}{2}v_i + \frac{1}{2}\vec{\omega_i}$}.
  Note that for all $i\inp I$ also $T'_i$ is a characteristic test of
  $\phi_i$ with target value $v'_i$.
  Take $T_\phi \Defs \bigsqcap_{i\in I} T'_{i}$
  and $v_\phi \Defs \sum_{i\in I}p_iv'_i$.
\end{itemise}
Note that $v_\phi(\omega)=0$ whenever $\omega\inp\Omega$ does not
occur in $T_\phi$.
By induction on $\phi$ we now check (\ref{eq:chartest}) above.
\begin{itemise}
\item Let $\phi=\top$. For all $\Delta\in\dist{\sCSP}$ we have
  $\Delta\models\phi$ as well as $\exists o \in
  \MDCApply({T_\phi,\Delta}):~o\leq v_\phi$, using \Lem{lem:inductive}(1).
\item Let $\phi=\diam{a}\psi$ with $a\inp\Act$.
Suppose $\Delta\models\phi$. Then there is a $\Delta'$
  with $\Delta \dar{\hat a}\Delta'$ and $\Delta'\models \psi$.
By induction, $\exists o \inp \MDCApply({T_\psi,\Delta'}):~o\leq v_\psi$.
By \Lem{lem:inductive}(2), $o\inp \MDCApply({T_\phi,\Delta})$.

Now suppose $\exists o \inp \MDCApply({T_\phi,\Delta}):~o\leq v_\phi$.
This implies $o(\omega)=0$, so by \Lem{lem:inductive}(2) there is a
$\Delta'$ with $\Delta \dar{\hat a}\Delta'$ and $o \inp \MDCApply({T_\psi,\Delta'})$.
By induction, $\Delta'\!\models\! \psi$, so $\Delta\!\models\!\phi$.
\item Let $\phi=\refuse X$ with $X\subseteq\Act$.
Suppose $\Delta\models\phi$. Then there is a $\Delta'$
  with $\Delta \dar{\hat\tau}\Delta'$ and \plat{$\Delta'\nar{X}$}.
By \Lem{lem:inductive}(3), $\vec{0}\inp \MDCApply({T_\phi,\Delta})$.

Now suppose $\exists o \inp \MDCApply({T_\phi,\Delta}):~o\leq v_\phi$.
This implies $o=\vec{0}$, so by \Lem{lem:inductive}(3) there is a
$\Delta'$ with $\Delta \dar{\hat\tau}\Delta'$ and \plat{$\Delta'\nar{X}$}.
Hence $\Delta\models\phi$.
\item Let $\phi=\bigwedge_{i\in I}\phi_i$ with $I$ a
finite and non-empty index set.
Suppose $\Delta\models\phi$. Then $\Delta\models\phi_i$ for all $i\inp I$,
and hence, by induction, $\exists o_i \inp\, \MDCApply({T_i,\Delta}):~o_i\leq v_i$.
Thus $o\!\Defs\!\sum_{i\in I}p_io_i\inp \MDCApply({T_\phi,\Delta})$
by \Lem{lem:inductive}(4), and $o\!\leq\! v_\phi$.

Now suppose $\exists o \inp \MDCApply({T_\phi,\Delta}):~o\leq v_\phi$.
Then, using \Lem{lem:inductive}(4), $o=\sum_{i\in I}p_io_i$ for
certain $o_i\inp\MDCApply({T_i,\Delta})$.
One has \mbox{$o_i\leq v_i$} for all $i\inp I$, for if $o_i(\omega)> v_i(\omega)$
for some $i\inp I$ and $\omega\inp \Omega$, then $\omega$ must occur
in $T_i$ and hence cannot occur in $T_j$ for $j\mathop{\neq} i$. This implies
$v_j(\omega)=0$ for all $j\neq i$ and thus $o(\omega)>v_\phi(\omega)$,
in contradiction with the assumption.  By induction,
$\Delta\models\phi_i$ for all $i\inp I$, and hence $\Delta\models\phi$.
\item Let $\phi=\bigoplus_{i\in I}p_i\Cdot\phi_i$. Suppose $\Delta\models\phi$.
Then for all $i\inp I$ there are $\Delta_i\inp
\dist{\sCSP}$ with $\Delta_i\models \phi_i$ such that $\Delta
\dar{\hat\tau}\bigoplus_{i\in I}p_i\Cdot\Delta_i$.
By induction, there are $o_i \inp \MDCApply({\Delta_i,T'_i})$ with $o_i\leq v'_i$.
By \Lem{lem:inductive}(5), $o\Defs\sum_{i\in I}p_io_i\inp \MDCApply({T_\phi,\Delta})$,
and $o \leq v_\phi$.

Now suppose $\exists o \inp \MDCApply({T_\phi,\Delta}):~o\leq v_\phi$.
Then, by \Lem{lem:inductive}(5),
 there are $q\inp\dist{I}$ and $\Delta_i$, for $i\inp I$, such
that $\Delta\dar{\hat\tau}\bigoplus_{i\in I}q_i\Cdot\Delta_i$ and $o=\sum_{i\in
I}q_io_i$ for some $o_i\inp\MDCApply({\Delta_i,T'_i})$.
Now $\forall i:o_i(\omega_i)=v'_i(\omega_i)=\frac{1}{2}$,
so $\frac{1}{2}q_i = q_io_i(\omega_i) = o(\omega_i) \leq
v_\phi(\omega_i) = p_iv'_i(\omega_i) = \frac{1}{2}p_i$.
As $\sum_{i\in I}q_i = \sum_{i\in I}p_i = 1$, it must be that
$q_i = p_i$ for all $i\inp I$.
Exactly as in the previous case one obtains $o_i\leq v'_i$ all $i\inp I$.
By induction, $\Delta_i\models\phi_i$ for all $i\inp I$, and hence
$\Delta\models\phi$.
\end{itemise}
In case $\phi\inp\SL$, a straightforward induction yields that
$|v_\phi|=1$ and for all $\Delta \inp \dist{\pCSP}$ and $o\inp
\MDCApply({T_\phi,\Delta})$ we have $|o|=1$.
Here $|o|$ denotes $\sum_{\omega\in\Omega}o(\omega)$.
Therefore, $o\leq v$ iff $o\geq v$ iff $o = v$, yielding
(\ref{eq:chartestmay}).
\end{proof}

\begin{theorem}\label{thm-characteristic tests}\mbox{}
\begin{enumerate}
\vspace{-1ex}
\item If $P \pdmMayleq Q$ then $\Op{P} \modalSpreo \Op{Q}$.
\vspace{-1ex}
\item If $P \pdmMustleq Q$ then $\Op{P} \modalFSpreo \Op{Q}$.
\end{enumerate}
\end{theorem}

\begin{proof}
Suppose $P\pdmMustleq Q$ and $\Op{Q}\models\phi$
for some $\phi\inp\FSL$. Let $T_\phi$ be a characteristic test of
$\phi$ with target value $v_\phi$. Then \Lem{lem:char tests}
yields $\exists o \inp \MDCApply({T_\phi,\Op{Q}}).~o\leq v_\phi$, and
hence, given that $P\pdmMustleq Q$ and $\MDCApply({T_\phi,\Op{R}})=
\MDCApply({T_\phi,R})$ for any $R\in\pCSP$, we have $\exists o' \in
\MDCApply({T_\phi,\Op{P}}):~o'\leq v_\phi$. Thus $\Op{P}\models\phi$.

The may-case goes likewise.
\end{proof}

\noindent
Combining Thms.~\ref{t:multiUni}-\ref{thm-characteristic tests}
we obtain
\Thm{t:simtest-reverse}, the goal we set ourselves in
  \Sect{sec:state-vs-action}. Thus, with \Thm{t:simtest} and
  \Prop{p:action-based},  we have shown that the may
  preorder coincides
with simulation and that the must preorder coincides with failure simulation.
\hfill{$\Box$}

%---------------------------------------------------
\Section{Equational theories}\label{sec:equations}

\begin{figure}
\vspace{-1.1em}
%These axioms are satisfied by both $\simpreo$ and $\failsimpreo$:
  \begin{displaymath}
    \begin{array}[t]{@{}lr@{}c@{}l@{}}
     \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\cdot q} (Q \probc{\frac{(1-p)\cdot q}{1-p\cdot q}} R)\\
      \Ename{I1}            & 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{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 a.Q&=& a.P \intc a.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) \\
                            &&&\qquad\intc (P \extc Q_1) \intc (P \extc Q_2),\\
                            && \text{\tiny provided} & ~~P = P_1 \intc P_2,\;Q = Q_1 \intc Q_2
   \end{array}\!\!\!\!\!
  \end{displaymath}

%Note: in gdpf  \Ename{EI} had  $b.Q$ in place of $a.Q$

  \caption{Common equations}
  \label{fig:cequations}
\end{figure}

\noindent In order to focus on the essentials we now consider just those
processes that do not use the parallel operator $\Par{A}$; we call
the resulting sub-language \nCSP. For a discussion of the axiomatisation for
terms involving $\Par{A}$ and the other parallel operators commonly
used in \CSP see \Sect{sec:conc}.

Let us write $P \Eeq Q$ to denote that $P = Q$ can be derived using the equations
given in \Fig{fig:cequations}.
Given the way we defined the syntax of \pCSP, axiom \Ename{D1} is merely a
case of abbreviation-expansion.
Many of the standard equations for \CSP \cite{csp} are missing;
they are not sound for $\failsimequiv$, as shown in Sec.\ 4 of \cite{DGHMZ07}.
Typical examples include:
\begin{align*}
  a.(P \intc Q) &= a.P \intc a.Q\\
              P &= P \extc P \\
P \extc (Q \intc R) &= (P \extc Q) \intc (P \extc R)\\
P \intc (Q \extc R) &= (P \intc Q) \extc (P \intc R)
\end{align*}
\begin{proposition}
  Suppose $P \Eeq Q$. Then $P \failsimequiv Q$.
\end{proposition}
\begin{proof}
  Because of \Prop{thm:cong} it is sufficient to
  exhibit witness failure-simulations for axioms in \Fig{fig:cequations}.
\end{proof}
\noindent
Note that this result also means $P \Eeq Q$ implies $P \forsimequiv Q$.

Despite the weakness of this equational theory, it does allow us to reduce
terms to a form in which the external choice operator is applied to prefix
terms only.

\begin{definition}[Normal forms]
The set of \emph{normal forms} $N$ is given by the following grammar:
  \begin{align*}
    N &::= N_1 \probc{p} N_2 \BNFsep N_1 \intc N_2 \BNFsep \bigbox_{i \in I} a_i.N_i
  \end{align*}
\end{definition}

\begin{proposition}
 For every $P \in \nCSP$ there is a normal form $N$ such that $P \Eeq N$.
\end{proposition}

\begin{proof}
A fairly straightforward induction, heavily relying on \Ename{D1}--\Ename{D3}.
\end{proof}

%-------------------------------------------------------------------------
\Section{Inequational theories}\label{sec:inequations}

\begin{figure}
\emph{May:}\vspace{-1.5em}
  \begin{displaymath}
    \begin{array}[t]{@{}lrl@{}}
      \Ename{May0}            & a.P \extc b.Q &= a.P \intc b.Q\\
      \Ename{May1}            &  P &\sqsubseteq P \intc Q\\
      \Ename{May2}            &  \Cnil & \sqsubseteq  P \\
     \Ename{May3}            & a.(P \probc{p} Q)&\sqsubseteq a.P \probc{p} a.Q\\
   \end{array}
  \end{displaymath}

\vspace{1em}

\emph{Must:}
\begin{displaymath}
\begin{array}[t]{@{}lrl@{}}
\Ename{Must1}  & P \intc Q  & \sqsubseteq Q\\\\
\Ename{Must2} & R \intc \bigsqcap_{i\in I}P_i & \sqsubseteq
                    \bigbox_{i\in I} a_i.Q_i,\\
& \text{\tiny provided} & P_i=\bigoplus_{j\in J_i}p_j (a_i.Q_{ij}
\extc P_{ij})\\
& & Q_i = \bigoplus_{j\in J_i}p_j Q_{ij}\\
& & \mathord{\inits{R}} \subseteq \sset{a_i}_{i\in I}
   \end{array}
  \end{displaymath}

  \caption{Inequations}
  \label{fig:inequations}
\end{figure}

\noindent
In order to characterise the simulation preorders, and the associated
testing preorders, we introduce \emph{inequations}. We write $P \MayAxleq
Q$ when $P\sqsubseteq Q$ is derivable from the inequational theory
obtained by adding the four
\emph{may} inequations in \Fig{fig:inequations} to the
equations in \Fig{fig:cequations}.
The first three additions,
\Ename{May0}--\Ename{May2}, are used in the standard testing theory of
\CSP \cite{csp,DNH84,henn}. For the \emph{must} case, in addition to the
standard inequation \Ename{Must1}, we require an inequational schema,
\Ename{Must2}; this uses the notation $\inits{P}$ to denote the
(finite) set of  initial visible actions of $P$.
Formally,
\[\begin{array}{@{}r@{~=~}l@{}}
\inits{0} & \emptyset\\
\inits{a.P} & \sset{a}\\
\inits{P \probc{p} Q} & \inits{P} \cup \inits{Q}\\
\inits{P \extc Q} & \inits{P} \cup \inits{Q}\\
\inits{P \intc Q} & \inits{P} \cup \inits{Q}
\end{array}\]
The side conditions of \Ename{Must2} entail that $\Op{P_i}\ar{a_i}\Op{Q_i}$
and that there exists some $\Delta$ such that
$R\dar{\hat{\tau}}\Delta\nar{X}$ with
$X=\Act\backslash\sset{a_i}_{i\in I}$.
Note that \Ename{Must2} can be used, together with \Ename{I1},
to derive the dual of \Ename{May3}, that is $ a.P \probc{p} a.Q \sqsubseteq a.(P \probc{p} Q)$.
We write $P \MustAxleq Q$ when $P\sqsubseteq Q$ is derivable from
the resulting  inequational theory.

An important inequation that follows from \Ename{May1} and \Ename{P1}
is \[\quad P \probc{p} Q ~\MayAxleq~ P \intc Q\] saying
that any probabilistic choice can be simulated by an internal choice.
Likewise, we have  \[\quad P \intc Q ~\MustAxleq~ P \probc{p} Q\;.\]

\begin{theorem}\label{thm:complete} For $P,\;Q$ in \nCSP, it holds that
  \begin{enumerate}[(i)]
\vspace{-1ex}  \item $P \forsimpreo Q$ if and only if $P \MayAxleq Q$
\vspace{-1ex}  \item $P \failsimpreo Q$ if and only if $P \MustAxleq Q$
\vspace{-1ex}  \end{enumerate}
\end{theorem}
\begin{proof}
Omitted due to lack of space.
\end{proof}

\Section{Conclusions and related work}\label{sec:conc}

\noindent
In this paper we continued our previous work \cite{DGHMZ07,DGMZ07}
in our quest for a testing theory for processes which exhibit both
nondeterministic and probabilistic behaviour. We have studied
three different aspects of may- and must testing preorders for finite processes: (i) we have
shown that the may preorder can be characterised as a co-inductive
simulation relation, and the must preorder as a failure simulation
relation; (ii) we have given a characterisation of both preorders in a
finitary modal logic; and (iii) we have also provided complete
axiomatisations for both preorders over a probabilistic version of
recursion-free CSP. Although we omitted our parallel operator
$\Par{A}$ from the axiomatisations, it
and similar CSP and CCS-like parallel operators can be handled using standard
techniques, in the must case at the expense of introducing auxiliary
operators. In future work we hope to extend these results to recursive processes.

We believe these results, in each of the three areas, to be novel, although
a number of partial results along similar lines exist in the literature.
These are detailed below.

\paragraph{Related work:}
Early additions of probability to CSP include work by Lowe
\cite{Low93}, Seidel \cite{Sei95} and Morgan et al.\ \cite{MMSS96};
but all of them were forced to make compromises of some kind in
order to address the potentially complicated interactions between
the three forms of choice. The last \cite{MMSS96} for example
applied the Jones/Plotkin probabilistic powerdomain \cite{Jones89}
directly to the failures model of CSP \cite{BHR84}, the resulting
compromise being that probability distributed outwards
through all other operators; one controversial result of that was
that internal choice was no longer idempotent, and that it was
``clairvoyant'' in the sense that it could adapt to
probabilistic-choice outcomes that had not yet occurred.
Mislove addressed this problem in \cite{Mis00} by presenting a
denotational model in which internal choice distributed outwards
through probabilistic choice.
However, the distributivities of both \cite{MMSS96} and \cite{Mis00} constitute
identifications that cannot be justified by our testing approach; see \cite{DGHMZ07}.

In Jou and Smolka \cite{JS90}, as in \cite{Low93,Sei95}, probabilistic equivalences
based on traces, failures and readies are defined. These equivalences are coarser
than $\pMayeq$. For let
\begin{align*}
P & :=a.((b.d\ \Box\
c.e)\probc{\frac{1}{2}}(b.f\ \Box\ c.g))\\
Q & :=a.((b.d\ \Box\
c.g)\probc{\frac{1}{2}}(b.f\ \Box\ c.e)).
\end{align*}
These two processes cannot
be distinguished by the equivalences of \cite{JS90,Low93,Sei95}.
However, we can tell them apart by the test\vspace{-2ex}
\[~~~~~~~~~~~~~~~T :=a.((b.d.\eureka \probc{\frac{1}{2}} c.e.\eureka) \intc (b.f.\eureka
\probc{\frac{1}{2}} c.g.\eureka))\]
since
$\Apply(T,P)=\sset{0,\frac{1}{2},1}$ and
$\Apply(T,Q)=\sset{\frac{1}{2}}$, that is, $P\not\pMayleq Q$.

Probabilistic extensions of testing equivalences \cite{DNH84} have
been widely studied.
There are two different proposals on how to include probabilistic choice:
  (i) a test should be non-probabilistic, i.e., there is no occurrence
  of probabilistic choice in a test
  \cite{LS91,Chr90,JHW94,KN98,GN99}; or (ii) a test can be
  probabilistic, i.e., probabilistic choice may occur in tests as well
  as processes \cite{CDSY99,WL92,Nun03,JW95,Seg96,JW02,CCVP03}.
  This paper adopts the second approach.

Some work \cite{LS91,Chr90,CDSY99,Nun03} does not consider nondeterminism
  but deals exclusively with \emph{fully probabilistic} processes. In this setting a process
  passes a test with a unique probability instead of a set of probabilities,
  and testing preorders in the style of \cite{DNH84} have been
  characterised in terms of \emph{probabilistic traces}
  \cite{CDSY99} and \emph{probabilistic acceptance trees} \cite{Nun03}.
Cazorla et al.\ \cite{CCVP03} extended the results of \cite{Nun03}
with nondeterminism, but suffered from the same problems as \cite{MMSS96}.

The work most closely related to ours is \cite{JW95,JW02}.
  In \cite{JW95} Jonsson and Wang characterised may- and must-testing
  preorders in terms of ``chains'' of traces and failures,
  respectively, and in \cite{JW02} they presented a ``substantially
  improved'' characterisation of their may-testing preorder
  using a notion of simulation which is weaker than $\forsimpreo$
(cf.\ \Def{def:simulation preorder}).
They only considered processes without $\tau$-moves. In
 \cite{DGHMZ07} we have shown 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.

Segala \cite{Seg96} defined two preorders called trace
distribution precongruence ($\tdc$) and failure distribution
precongruence ($\fdc$). He proved that the former coincides with an
infinitary version of $\pdmMayleq$ (cf.\ \Def{def:vector-testing})
and that the latter coincides with an infinitary version of \plat{$\pdmMustleq$}.
In \cite{LSV03} it has been shown that $\tdc$
coincides with a notion of simulation akin to $\forsimpreo$.
Other probabilistic extensions of simulation occurring in the
literature are reviewed in \cite{DGHMZ07}.

\bibliographystyle{plain}
\small
\begin{thebibliography}{10}

\bibitem{BS01}
{ E.~Bandini \& R.~Segala} (2001):
\newblock {\em Axiomatizations for probabilistic bisimulation.}
\newblock In {\sl {\rm Proc.} ICALP'01}, {\sl \rm LNCS} 2076, Springer, pp. 370--381.

\bibitem{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{CCVP03}
{ 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, pp. 57--103.

\bibitem{Chr90}
{ I.~Christoff} (1990):
\newblock {\em Testing equivalences and fully abstract models for probabilistic processes.}
\newblock In {\sl {\rm Proc.} CONCUR'90}, {\sl \rm LNCS} 458, Springer, pp. 126--140.

\bibitem{CDSY99}
{ R.~Cleaveland, Z.~Dayar, S.A. Smolka \& S.~Yuen} (1999):
\newblock {\em Testing preorders for probabilistic processes.}
\newblock {\sl Information and Computation} 154(2), pp. 93--148.

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

\bibitem{DP07}
{ Y.~Deng \& C.~Palamidessi} (2007):
\newblock {\em Axiomatizations for probabilistic finite-state behaviors.}
\newblock {\sl Theoretical Computer Science} 373(1-2), pp. 92--114.

\bibitem{DGHMZ07}
{ Y.~Deng, R.J. van Glabbeek, M.~Hennessy, C.C. Morgan \& C.~Zhang} (2007):
\newblock {\em Remarks on testing probabilistic processes.}
\newblock {\sl ENTCS} 172, pp. 359--397.

\bibitem{DGMZ07}
{ Y.~Deng, R.J. van Glabbeek, C.C. Morgan \& C.~Zhang} (2007):
\newblock {\em Scalar outcomes suffice for finitary probabilistic testing.}
\newblock In {\sl {\rm Proc.} ESOP'07}, {\sl \rm LNCS} 4421, Springer, pp. 363--368.

\bibitem{vG93}
{ R.J.~van Glabbeek} (1993):
\newblock {\em The linear time -- branching time spectrum {II}; the semantics of sequential systems with silent moves.}
\newblock In {\sl {\rm Proc.} CONCUR'93}, {\sl \rm LNCS} 715, Springer, pp. 66--81.

\bibitem{GN99}
{ C.~Gregorio-Rodr\'{\i}guez \& M.~N{\'u}{\~n}ez} (1999):
\newblock {\em Denotational semantics for probabilistic refusal testing.}
\newblock {\sl ENTCS} 22, pp. 111--137.

\bibitem{HJ90}
{ H.~Hansson \& B.~Jonsson} (1990):
\newblock {\em A calculus for communicating systems with time and probabilities.}
\newblock In {\sl {\rm Proc.} RTSS'90}, IEEE Computer Society Press, pp. 278--287.

\bibitem{HSM97}
{ He~Jifeng, 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{henn}
{ M.~Hennessy} (1988):
\newblock {\em An Algebraic Theory of Processes}.
\newblock MIT Press.

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

\bibitem{Jones89}
{ C.~Jones \& G.D. Plotkin} (1989):
\newblock {\em A probabilistic powerdomain of evaluations.}
\newblock In {\sl {\rm Proc.} LICS'89}, Computer Society Press, pp. 186--195.

\bibitem{JHW94}
{ B.~Jonsson, C.~Ho-Stuart \& Wang Yi} (1994):
\newblock {\em Testing and refinement for nondeterministic and probabilistic processes.}
\newblock In {\sl {\rm Proc.} FTRTFT'94}, {\sl \rm LNCS} 863, Springer, pp. 418--430.

\bibitem{JW95}
{ B.~Jonsson \& Wang Yi} (1995):
\newblock {\em Compositional testing preorders for probabilistic processes.}
\newblock In {\sl {\rm Proc.} LICS'95}, IEEE Computer Society Press, pp. 431--441.

\bibitem{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{JS90}
{ C.-C. Jou \& S.A. Smolka} (1990):
\newblock {\em Equivalences, congruences, and complete axiomatizations for probabilistic processes.}
\newblock In {\sl {\rm Proc.} CONCUR '90}, {\sl \rm LNCS} 458, Springer, pp. 367--383.

\bibitem{KN98}
{ M.Z. Kwiatkowska \& G.~Norman} (1998):
\newblock {\em A testing equivalence for reactive probabilistic processes.}
\newblock {\sl ENTCS} 16(2), pp. 114--132.

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

\bibitem{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{LSV03}
{ N.~Lynch, R.~Segala \& F.W. Vaandrager} (2003):
\newblock {\em Compositionality for probabilistic automata.}
\newblock In {\sl {\rm Proc.} CONCUR'03}, {\sl \rm LNCS} 2761, Springer, pp. 204--222.

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

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

\bibitem{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, pp. 617--647.

\bibitem{Nun03}
{ M.~N{\'u}{\~n}ez} (2003):
\newblock {\em Algebraic theory of probabilistic processes.}
\newblock {\sl Journal of Logic and Algebraic Programming} 56, pp. 117--177.

\bibitem{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{Seg95}
{ R.~Segala} (1995):
\newblock {\em Modeling and Verification of Randomized Distributed Real-Time Systems}.
\newblock PhD thesis, MIT.

\bibitem{Seg96}
{ R.~Segala} (1996):
\newblock {\em Testing probabilistic automata.}
\newblock In {\sl {\rm Proc.} CONCUR'96}, {\sl \rm LNCS} 1119, Springer, pp. 299--314.

\bibitem{SL94}
{ R.~Segala \& N.A. Lynch} (1994):
\newblock {\em Probabilistic simulations for probabilistic processes.}
\newblock In {\sl {\rm Proc.} CONCUR'94}, {\sl \rm LNCS} 836, Springer, pp. 481--496.

\bibitem{Sei95}
{ K.~Seidel} (1995):
\newblock {\em Probabilistic communicating processes.}
\newblock {\sl Theoretical Computer Science} 152(2), pp. 219--249.

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

\bibitem{WL92}
{ Wang Yi \& K.G. Larsen} (1992):
\newblock {\em Testing probabilistic and nondeterministic processes.}
\newblock In {\sl {\rm Proc.} PSTV'92}, {\sl IFIP Transactions} C-8, North-Holland, pp. 47--61.

\end{thebibliography}
\end{document}
