\documentclass{eptcs}
\usepackage{latexsym}
\usepackage{times}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{stmaryrd}
\SetSymbolFont{stmry}{bold}{U}{stmry}{m}{n}
\usepackage{xspace}
\usepackage{enumerate}
\usepackage{graphicx}
\usepackage{color}   
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%Theorem-like environments
\newtheorem{defi}{Definition}[section]
\newtheorem{theo}[defi]{Theorem}
\newtheorem{prop}[defi]{Proposition}
\newtheorem{lemm}[defi]{Lemma}
\newtheorem{coro}[defi]{Corollary}
\newtheorem{exam}[defi]{Example}
\newtheorem{rema}[defi]{Remark}

\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}{ \hfill $\Box$\end{exam}}
\newenvironment{remark}{\begin{rema} \rm}{\end{rema}}
\newenvironment{proof}{\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]}
                 {\hfill $\Box$\end{trivlist}}
\newenvironment{Reason}{%
 \begin{tabbing}\hspace{4em}\=\kill}{\end{tabbing}\vspace{-2.5ex}}
\newcommand\Space {~ \\}
\newcommand\Step[2]%
 {#1 \> $\begin{array}[t]{lll}#2\end{array}$ \\}
\newcommand\StepR[3]%
 {#1 \> $\begin{array}[t]{lll}#3\end{array}$
 \` {\RF \makebox[0pt][r]{#2}} \\}
\newcommand\WideStep[2] {#1 \> $\begin{array}[t]{lll}#2\end{array}$ \\}
\newcommand\WideStepR[3] {#1 \` {\RF #2} \\ \> $\begin{array}[t]{lll}#3\end{array}$ \\}
\newcommand\WideThinStepR[3] {#1 \` {\RF #2} \\ \> $#3$ \\}
\newcommand\ThinStep[2] {#1 \> $#2$ \\}
\newcommand\ThinStepR[3] {#1 \> $#3$ \` {\RF #2} \\}
\newcommand\RF {\small}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Fonts
\newfont{\bbb}{bbm10}       % blackboard bold

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Spacing
\newcommand{\inp}{\mathop\in}                           % takes less space
\newcommand{\Times}{\mathord{\kern.08em\cdot\kern.08em}}
\newcommand{\Defs}{\mathrel{:=}}
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{#1}}     % no vertical space
\newenvironment{itemise}{\begin{list}{$\bullet$}{\leftmargin 20pt
                        \labelwidth\leftmargin\advance\labelwidth-\labelsep
                        \topsep 2pt \itemsep 0pt \parsep 0pt}}{\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% General
\newcommand{\dcup}{\stackrel{\mbox{\huge .}}{\cup}}
\renewcommand{\phi}{\varphi}
\renewcommand{\vec}{\overrightarrow}
\newcommand{\aRel}{\ensuremath{\mathrel{{\mathcal R }}}}
\newcommand{\size}[1]{\mathrel{|{#1}|}}
\newcommand\Thm[1] {Thm.~\ref{thm:#1}}
\newcommand\Wide[1] {~~~#1~~~}
\newcommand\WideRM[1] {~~~\textrm{#1}~~~}
\newcommand\WIDERM[1] {\Wide{\WideRM{#1}}}
\def \cV{{\cal V}}
\def \cF{{\cal F}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  CSP
\newcommand{\BNFsep}{\;\;|\;\;}
\newcommand{\intc}{\mathrel{\sqcap}}
\newcommand{\extc}{\mathrel{\Box}}
\newcommand{\probc}[1]{\mathrel{\!_{\scriptscriptstyle #1}\oplus}}
\newcommand{\Par}[1]{\|}
\newcommand{\parT}{\Par{\Act}}
\newcommand{\Cnil}{\mathop{\textbf{\textsf{0}}}}
\newcommand{\Crec}[2]{\mathsf{rec}\,#1.\,#2}
\newcommand{\Crecx}[1]{\Crec{x}{#1}}

\newcommand{\Act}{\ensuremath{\mathsf{Act}}\xspace}
\newcommand{\Var}{{\sf Var}}
\newcommand{\pCSP}{\ensuremath{\mathsf{pCSP}}\xspace}
\newcommand{\sCSP}{\ensuremath{\mathsf{sCSP}}\xspace}
\newcommand{\pCSPO}{\ensuremath{\mathsf{pCSP}^{\Omega}}\xspace}
\newcommand{\sCSPO}{\ensuremath{\mathsf{sCSP}^{\Omega}}\xspace}
\newcommand{\Op}[1]{\mbox{\bbb [}#1\mbox{\bbb ]}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Testing
\newcommand{\VV}{{\mathbb V}}
\newcommand{\minResultsN}{\ensuremath{{\mathbb  V_{\text{min}}}}}
\newcommand{\maxResultsN}{\ensuremath{{\mathbb  V_{\text{max}}}}}
\newcommand{\ResultsN}{\ensuremath{{\mathbb V}}}

\newcommand{\eMinApply}{\ensuremath{{\mathcal A}_{\text{min}}^{\text{e}}\xspace}}
\newcommand{\eMaxApply}{\ensuremath{{\mathcal A}_{\text{max}}^{\text{e}}\xspace}}
\newcommand{\MApply}{\ensuremath{{{\mathcal A}^{\raisebox{-.1em}{\scriptsize${\Omega}$}}\xspace}}}
\newcommand{\Apply}{\ensuremath{{\mathcal A}^\text{d}}\xspace}
\newcommand{\RApply}{\ensuremath{{\mathcal A}}\xspace}
\newcommand{\RPApply}{\ensuremath{{\mathcal A}^{\text{p}}\xspace}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preorders
\newcommand{\Hleq}{\mathrel{\leq_{\rm Ho}}}
\newcommand{\Sleq}{\mathrel{\leq_{\rm Sm}}}
\newcommand{\eMayleq}{\mathrel{{\sqsubseteq}_{\text{\rm pmay}}^{\raisebox{-.3em}{\scriptsize$e$}}}}
\newcommand{\eMustleq}{\mathrel{{\sqsubseteq}_{\text{\rm pmust}}^{\raisebox{-.3em}{\scriptsize$e$}}}}
\newcommand{\pmMayleq}{\mathrel{{\sqsubseteq}_{\text{\rm pmay}}^{\raisebox{-.3em}{\scriptsize${\Omega}$}}}}
\newcommand{\pmMustleq}{\mathrel{{\sqsubseteq}_{\text{\rm pmust}}^{\raisebox{-.3em}{\scriptsize${\Omega}$}}}}
\newcommand{\InvpmMustleq}{\mathrel{{\sqsupseteq}_{\text{\rm pmust}}^{\raisebox{-.3em}{\scriptsize${\Omega}$}}}}
\newcommand{\pMustleq}{\mathrel{\relax{\sqsubseteq}_{\text{\rm pmust}}}}
\newcommand{\pMayleq}{\mathrel{\relax{\sqsubseteq}_{\text{\rm pmay}}}}

\newcommand{\forsim}{\mathrel{\lhd_{\raisebox{-.1em}{\tiny\it S}}}}
\newcommand{\failsim}{\mathrel{\lhd_{\raisebox{-.1em}{\tiny \it FS}}}}
\newcommand{\failsime}{\mathrel{\lhd_{\raisebox{-.1em}{\tiny\it FS}}}}
\newcommand{\iterfailsim}[1]{\mathrel{\lhd^{#1}_\textit{\tiny\it FS}}}
\newcommand{\forsimpreo}{\sqsubseteq_{S}}
\newcommand{\failsimpreo}{\sqsubseteq_{\it FS}}
\newcommand{\Invfailsimpreo}{\sqsupseteq_{\it FS}}
\newcommand{\iterfailsimpreo}[1]{\sqsupseteq_{\it FS}^{#1}}
\newcommand{\nrmMayleq}{\mathrel{{\sqsubseteq}_{\text{{\bf nr}may}}^{\raisebox{-.3em}{\scriptsize$\Omega$}}}}
\newcommand{\nrmMustleq}{\mathrel{{\sqsubseteq}_{\text{{\bf nr}must}}^{\raisebox{-.3em}{\scriptsize$\Omega$}}}}
\newcommand{\rrmMayleq}{\mathrel{{\sqsubseteq}_{\text{{\bf rr}may}}^{\raisebox{-.3em}{\scriptsize$\Omega$}}}}
\newcommand{\rrmMustleq}{\mathrel{{\sqsubseteq}_{\text{{\bf rr}must}}^{\raisebox{-.3em}{\scriptsize$\Omega$}}}}
\newcommand{\nrMayleq}{\mathrel{{\sqsubseteq}_{\text{{\bf nr}may}}}}
\newcommand{\nrMustleq}{\mathrel{{\sqsubseteq}_{\text{{\bf nr}must}}}}
\newcommand{\rrMayleq}{\mathrel{{\sqsubseteq}_{\text{{\bf rr}may}}}}
\newcommand{\rrMustleq}{\mathrel{{\sqsubseteq}_{\text{{\bf rr}must}}}}

\newcommand{\InvmodalFSpreo}{\mathrel{\sqsupseteq}^{\FSL}\!}
\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{$\mathcal D$}} ({#1})   } % distributions
\newcommand{\pdist}[1]{\overline{#1}  } % point distributions
\newcommand{\subdist}[1]{\mathop{\mbox{$\cal D_{\textsl{sub}}$}} ({#1})   }
\newcommand{\support}[1]{\lceil{#1}\rceil}
\newcommand{\lift}[1]{\mathrel{\overline{#1}}}
\newcommand{\eDis}{\mathop{\varepsilon}}
\newcommand{\Exp}[1]{\textrm{Exp}_{#1}}
\newcommand{\ExpDeltaf}{\Exp{\Delta}(f)}
\newcommand{\Imgf}[1]{\textrm{Img}_f(#1)}
\newcommand{\Stop}{{\times}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Maths
\def \Nat{\mbox{\bbb N}}
\newcommand{\setof}[2]{\{ \, #1 \, \mid \, #2 \, \}}% set comprehension
\newcommand{\sset}[1]{\{ {#1}  \}  } % singleton set
\def \Real{\mbox{\bbb R}}
\newcommand{\Pfun}{\mathbin{\rightharpoonup}}
\newcommand{\Rfun}{\$} % The name of the "immediate reward" function from state to reals.
\newcommand{\Equ}[1]{\buildrel{#1}\over{=}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Miscellaneous
\newcommand{\match}{{^\natural}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%% 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
\newcommand{\darE}[1]{\mathrel{\dar{#1}\kern-.3em\succ}}
\newcommand{\Move}{\rightarrow}
\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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Operational semantics
\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{\Ref}[2]{#1 \nar{#2}}
\newcommand{\RefE}[2]{#1 \dar{}\Ref{}{#2}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\newcommand\FN[1] {\footnote{\textbf{#1}}} %%% for comments to other authors.
%
%\definecolor{greenish}{rgb}{.24,.5,.26} % Only RGB, CMYK and BW are predefined.
%\newcommand{\MHx}{\color{greenish}} % M's for Matthew
%\newcommand{\MHc}[1]{{\MHx #1}}
%\newcommand{\MHf}[1]{\marginpar{\MHx~\bf\fbox{\footnotemark}~}\footnotetext{ \color{greenish}   #1}}
%
%\newcommand{\Y}[1]{{\color{red}   #1}}
%\newcommand{\R}[1]{{\color{magenta} #1}}
%\newcommand\C[1] {{\color{blue}#1}} % For Carroll, at last able to use C since Chenyi is absent.

\begin{document}

\def\titlerunning{Real-Reward Testing for Probabilistic Processes}
\def\authorrunning{Y. Deng, R.J. van Glabbeek, M. Hennessy \& C.C. Morgan}
\title{\titlerunning}

\author{Yuxin Deng$^1$%
\thanks{Deng was partially supported by the National Natural Science Foundation
  of China (61173033, 61261130589, 61033002).}
\quad Rob van Glabbeek$^2$
\quad Matthew Hennessy$^3$%
\thanks{Hennessy was supported by SFI project SFI 06 IN.1 1898.}
\quad Carroll Morgan$^4$%
  \thanks{Morgan acknowledges the support of ARC Discovery Grant DP0879529.}
\institute{\makebox[1.7em][r]{$^1$} Shanghai Jiao Tong University, China}
\institute{\makebox[1.7em][r]{$^{2}$} NICTA, Sydney, Australia}%
\thanks{NICTA is funded by the Australian Government as represented by the Department of Broadband, Communications and the Digital Economy and the Australian Research Council through the ICT Centre of Excellence program.}
\institute{\makebox[1.7em][r]{$^3$} Trinity College Dublin, Ireland}
\institute{\makebox[1.7em][r]{$^{2,4}$} University of New South Wales, Sydney, Australia}
}

\maketitle

\begin{abstract}
We introduce a notion of real-valued reward testing for probabilistic
processes by extending the traditional nonnegative-reward testing with
negative rewards. In this richer testing framework, the may- and must
preorders turn out to be inverses. We show that for convergent
processes with finitely many states and transitions, but not in the
presence of divergence, the real-reward must-testing preorder
coincides with the nonnegative-reward must-testing preorder. To prove
this coincidence we characterise the usual resolution-based testing in
terms of the weak transitions of processes, without having to involve
policies, adversaries, schedulers, resolutions or similar structures
that are external to the process under investigation. This requires
establishing the continuity of our function for calculating testing
outcomes.
\end{abstract}

\section{Introduction}\label{sec:intro}
Extending classical testing semantics
\cite{DNH84,henn} to a setting in which probability and nondeterminism
co-exist was initiated in \cite{WL92}.  The application of a test to a
process yields a set of probabilities for reaching a success state.
Traditionally, this set of result probabilities is obtained by
  \emph{resolving} \cite{esop} a 
  system into a non-empty set of deterministic but probabilistic
  systems, each representing a possible probabilistic run of the
  original system; concepts such as \emph{policy} \cite{Put94},
  \emph{adversary} \cite{KNP04}, \emph{scheduler} \cite{Seg95} and 
 \emph{resolution} \cite{esop} have
   been used for this purpose. 
\emph{Reward testing}
was introduced in \cite{JHW94} for concurrency, though earlier pioneered in \cite{Kozen:85}
for sequential programs; here the success states are labelled 
by nonnegative real numbers---\emph{rewards}---to indicate degrees of
success, and reaching a success state
accumulates the associated reward. In \cite{Seg96} an infinite set of
success actions is used to report success, and the testing
outcomes are vectors of probabilities of performing these success
actions.  Compared to \cite{JHW94} this amounts to distinguishing
different qualities of success, rather than different quantities.
\advance\textheight 13.6pt

In \cite{WL92} and \cite{Seg96}, both tests and testees are
nondeterministic probabilistic processes, whereas \cite{JHW94} allows
nonprobabilistic tests only, thereby obtaining a less discriminating
form of testing. In \cite{esop} we strengthened reward testing by also
allowing probabilistic tests. Taking reward testing in this form we showed that for finitary
processes, i.e.\ finite-state and finitely branching processes, all
three modes of testing lead to the same testing preorders. Thus, vector-based
testing is no more powerful than \emph{scalar} testing that employs
only one success action, and likewise reward testing is no more
powerful than the special case of reward testing in which all rewards are 1.
\footnote{In spite of this there \emph{is} a difference in power
between the notions of testing from \cite{WL92} and \cite{Seg96}, but
this is an issue that is entirely orthogonal to the distinction
between scalar testing, reward testing and vector-based testing. In
\cite{Seg96} it is the execution of a success \emph{action} that
constitutes success, whereas in \cite{DNH84,henn,WL92,JHW94} it is
reaching a success \emph{state} (even though typically success actions
are used to identify those states). In \cite[Ex 5.3]{lmcs} we showed
that state-based testing is (slightly) more powerful than action-based
testing. The results presented in \cite{esop} about the coincidence of
scalar, reward, and vector-based testing preorders pertain to
action-based version of each, but in the conclusion it is observed
that the same coincidence could be obtained for their state-based
versions.  In the current paper we stick to state-based testing.}

In certain situations it is natural to introduce negative rewards; this is the case, for instance, in the theory of Markov Decision
Processes \cite{Put94}. Intuitively, we could understand negative rewards as costs, while positive rewards are often viewed as benefits
or profits.
Consider for instance the (nonprobabilistic) processes $q_1$ and $q_2$ of
Figure~\ref{fig:diverg}. Here $a$ represents the action of making an investment.
Assuming that the investment is made by bidding for some commodity, the $\tau$-action
represents an unsuccessful bid --- if this happens one simply tries again. Now $b$ represents
the action of reaping the benefits of this investment. Wheres $q_1$ models a process
in which making the investment is always followed by an opportunity to reap the benefits,
the process $q_2$ allows, nondeterministically, for the possibility that the investment is
unsuccessful, so that $a$ does not always lead to a state where $b$ is enabled.
The test $t$, which will be explained later, allows us to give a negative reward
to action $a$---its cost---and a positive reward to $b$.

This leads to the question: \emph{if both negative- and positive rewards are
allowed, how would the original reward-testing semantics change?}%
\footnote{One might suspect no change at all, for any assignment of rewards from
    the interval $[-1,+1]$ can be converted into a non-negative assignment simply by
    adding 1 to all of them. But that would not preserve the testing order
    in the case of zero-outcomes that resulted from a process's failing to reach any
    success state at all: those zeroes would remain zero.}
We refer to the more relaxed form of testing, using positive and
negative rewards, as \emph{real-reward testing} and the original one
(from \cite{JHW94}, but with probabilistic tests as in \cite{esop}) as
\emph{nonnegative-reward testing}.

\begin{figure}
\begin{center} \tiny
\includegraphics[width=11cm,height=5cm]{diverge.eps}
\end{center}
\vspace{-4ex}
\caption{Two processes with divergence and a test} \label{fig:diverg}
\end{figure}

The power of real-reward testing is illustrated in Figure~\ref{fig:diverg}.
The two (nonprobabilistic) processes in the left- and central diagrams are equivalent under
(probabilistic) may- as well as must testing; the $\tau$-loops in the
initial states cause both processes to fail any nontrivial must test. Yet, if a
reward of $-1$ is associated with performing the action $a$, and a
reward of $2$ with the subsequent performance of $b$,
it turns out that in the first  process the net reward is
either 0, if the process remains stuck in its initial state,  or  
positive, whereas running the second process may yield a loss.
% (implemented by the test in the right diagram; see Example~\ref{ex:divergence}
% for more details), in the first process the net 
% reward is either $0$ (if the process remains stuck in its initial state)
% or positive, whereas running the second process may yield a loss.
See Example 3.8 for details of how these rewards are assigned,
and how net rewards are associated with the application of tests such  
as $t$.
This example shows that for processes that may exhibit
divergence, real-reward testing is more discriminating than
nonnegative-reward testing, or other forms of probabilistic testing.
It also illustrates that the extra power is relevant in applications.

As remarked, in \cite{esop} we established that for finitary processes the
nonnegative-reward must-testing preorder ($\nrMustleq$) coincides
with the probabilistic must-testing preorder ($\pMustleq$), and
likewise for the may preorders.
The main result of this paper is that  restricted to finitary convergent
processes, the real-reward must preorder $\rrMustleq$ coincides with the
nonnegative-reward must preorder, i.e.\ for any finitary convergent
processes,\vspace{-1ex}
\begin{equation}\label{eq:rrmust.nrmust}
\Delta \rrMustleq \Gamma \WIDERM{iff} \Delta\nrMustleq \Gamma.
\end{equation}
Here, as we shall see, convergence is the natural generalisation of the standard 
concept for nonprobabilistic processes to the probabilistic setting;
in particular it rules out the processes of Figure~\ref{fig:diverg}.

There is also a surprisingly simple proof of the fact that 
for real-reward testing the may- and must preorders are the
inverse of each other, i.e.\ that for any processes $\Delta$ and $\Gamma$,
\begin{equation}\label{eq:rrmay.rrmust}
\Delta \rrMayleq \Gamma \WIDERM{iff} \Gamma \rrMustleq \Delta.
\end{equation}
This pleasing symmetry does not hold for the more restrictive
nonnegative-reward (or scalar) testing.   Moreover, the analogy of
(\ref{eq:rrmust.nrmust}) for the may preorder does not hold,
i.e.\ $\rrMayleq$ does not coincide with $\nrMayleq$
(q.v.~the end of Section~\ref{sec:conclusion}).  

Although it is easy to see that in (\ref{eq:rrmust.nrmust}) the former
implies the latter, to prove the opposite is far from trivial;
see more discussion in Section~\ref{sec:discussion}.
We employ a characterisation of $\pMustleq$ from \cite{lmcs,concur}. 
\emph{Failure simulation} is a well-known behavioural preorder for nondeterministic processes \cite{vG93}; in \cite{lmcs} we showed that it could be adapted to characterise the
probabilistic must-testing preorder $\pMustleq$, and in \cite{concur} this work was
generalised from finite to finitary processes. This involved the generalisation of the 
standard notion of (weak) derivations in state-based systems \cite{ccs}, to probabilistic 
processes, i.e.\ probability distributions. By capitalising on this novel notion of derivation
between distributions we can show that the failure simulation preorder $\failsimpreo$ is
contained in $\rrMustleq$.
Convergence is essential here, even though it is not needed to
establish that $\failsimpreo$ is contained in $\nrMustleq$.
Recall that $\rrMustleq$ is defined using \emph{resolutions}; the 
key to proving this containment, the heart of the paper, is showing that certain derivations,
which we call \emph{extreme derivations},
are essentially the same as \emph{resolutions}. 
Combining this with the results from \cite{esop} and \cite{concur} mentioned above
leads to our required result that $\nrMustleq$ is included in
$\rrMustleq$, as far as finitary convergent processes are
concerned. Consequently, in this case, all the relations of
Figure~\ref{fig:preorders} collapse into one.

\begin{figure}[t]
\begin{center}
\vspace{-1em}
$$\begin{array}{l@{\quad}l@{\quad}l@{\quad}l@{\quad}c@{\quad}l@{\quad}l@{\quad}l@{\quad}l}
(\rrMayleq)^{-1} & \Equ{\rm \Thm{rrmay.rrmust}} & \rrMustleq &
  \Equ{\rm\Thm{rrm.nrm}} &\nrMustleq & \Equ{\cite{esop}} & \pMustleq &
  \Equ{\cite{concur}} & \failsimpreo
\end{array}$$
\textit{\small The symbol $=$ between two relations means that they
  coincide for finitary convergent processes.}\vspace{-1.5ex}
\end{center}
\caption{The relationship of different testing preorders.}\label{fig:preorders}
\end{figure}

The rest of this paper is organised as follows. We start by recalling
notation for probabilistic labelled transition systems.  In
Section~\ref{sec:testing} we review the resolution-based testing
approach and show that the real-reward may preorder is simply the
inverse of the real-reward must preorder. Moreover, using the example
of Figure~\ref{fig:diverg}, we show that in the presence of divergence
the inclusion of $\rrMustleq$ in $\nrMustleq$ is proper. In
Section~\ref{sec:derivation} we recall the notions of derivation
and the failure simulation preorder. In Section ~\ref{sec:compare}
we show that resolutions can be seen as certain kinds of derivations. 
Then in Section~\ref{sec:agree} we show
for finitary convergent processes that real-reward must testing
coincides with nonnegative-reward must testing. 
We explain in Section~\ref{sec:discussion} why the proof of the coincidence result cannot easily
be simplified, and then conclude in Section~\ref{sec:conclusion}.

Besides the related work already mentioned above, many
other studies on probabilistic testing and simulation semantics
have appeared in the literature. They are reviewed in
\cite{gdpf,lmcs}. An extended abstract of the current work has appeared as \cite{abstract}. All the
proofs omitted there are now detailed. Section~\ref{sec:discussion} is newly added to explain the
subtle difference between $\rrMustleq$ and $\nrMustleq$.

\section{Probabilistic Processes}\label{sec:lang}

A (discrete) probability \emph{subdistribution} over a set $S$ is a
function $\Delta: S \rightarrow [0,1]$ with $\sum_{s\inp S}\Delta(s)
\leq 1$; the \emph{support} of such a $\Delta$ is
$\support{\Delta}\Defs\setof{s \inp S}{\Delta(s) > 0}$, and its
\emph{mass} $|\Delta|$ is
\plat{$\sum_{s\inp\support{\Delta}}\Delta(s)$}.  A subdistribution is
a (total, or full) \emph{distribution} if $|\Delta| = 1$.  The point
distribution $\pdist{s}$ assigns probability $1$ to $s$ and $0$ to all
other elements of $S$, so that $\support{\pdist{s}}=\sset{s}$.  With
$\subdist{S}$ we denote the set of subdistributions over $S$, and with
$\dist{S}$ its subset of full distributions.

\advance\textheight -13.6pt
Let $\sset{\Delta_k \mid k \in K}$ be a set
of subdistributions, possibly infinite. Then $\sum_{k \in K} \Delta_k$ is the
real-valued function in $S \rightarrow \Real$ defined by
$(\sum_{k \in K} \Delta_k)(s) \mathrel{:=} \sum_{k \in K} \Delta_k(s)$.
This is a partial operation on subdistributions because
for some state $s$ the sum of $\Delta_k(s)$ might exceed $1$. If the
index set is finite, say $\sset{1..n}$, we often write $\Delta_1 +
\ldots + \Delta_n$.  For $p$ a real
number from $[0,1]$ we use
\begin{math}
  p\Times \Delta
\end{math}
to denote the subdistribution given by $(p\Times \Delta)(s)
\mathrel{:=} p\Times\Delta(s)$. Finally we use $\eDis$ to denote the
everywhere-zero subdistribution that thus has empty support. These
operations on subdistributions do not readily adapt themselves to
distributions; yet if $\sum_{k \in K} p_k \mathbin= 1$ for
some $p_k \geq 0$, and the $\Delta_k$ are distributions,
then so is $\sum_{k \in K}p_k \Times \Delta_k$.

The expected value $\sum_{s\in S} \Delta(s) \Times f(s)$ over a
subdistribution $\Delta$ of a bounded nonnegative function $f$ to the
reals or tuples of them is written $\ExpDeltaf$, and the image of a
subdistribution $\Delta$ through a function $f:S\rightarrow T$, for some set $T$, is written
$\Imgf{\Delta}$ --- the latter is the subdistribution over
$T$ given by $\Imgf{\Delta}(t):=\sum_{f(s)=t}\Delta(s)$ for each $t\in T$.

\begin{definition} \rm
A \emph{probabilistic labelled transition system} (pLTS) is a triple
$\langle S, \Act, \rightarrow \rangle$, where\vspace{-3pt}
\begin{enumerate}[(i)] \parskip 0pt \itemsep 0pt
\item $S$ is a set of states,
\item $\Act$ is a set of visible actions,
\item relation $\rightarrow$ is a subset of $S \times \Act_\tau \times \dist{S}$.
\end{enumerate}
Here $\Act_\tau$ denotes $\Act\cup \{\tau\}$, where
$\tau \not\in\Act$ is the invisible- or internal action.
\end{definition}
\noindent
A (nonprobabilistic) labelled transition system (LTS) may be viewed
as a degenerate pLTS --- one in which only point distributions are
used. As with LTSs, we write $s \ar{\alpha} \Delta$ for
$(s,\alpha,\Delta) \inp \mathord\rightarrow$, as well as
$s\ar{\alpha}$ for $\exists\Delta: s\ar{\alpha}\Delta$ and
$s\!\rightarrow$ for $\exists\alpha\!: s\,\ar{\alpha}$,
with $s\nar{\alpha}$ and $s \not\!\rightarrow$ representing their negations.

We graphically depict pLTSs as follows.
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$.
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)$.
We leave out point-distributions, diverting an incoming
edge to the unique state in its support.
See e.g. Figure~\ref{fig:ex1B} in the next section for some example pLTSs.

In this paper a \emph{(probabilistic) process} will simply be a
distribution over the state set of a pLTS\@.
A pLTS is \emph{deterministic} if for any state $s$ and
label $\alpha$ there is at most one distribution $\Delta$ with $s\ar{\alpha}\Delta$.
It is \emph{finitely branching} if the set $\sset{\Delta\mid
s\ar{\alpha}\Delta,~ \alpha\inp L}$ is finite for all states $s$;
if moreover $S$ is finite, then the pLTS is \emph{finitary}.
A subdistribution $\Delta$ over the state set $S$ of an arbitrary pLTS is \emph{finitary}
if restricting $S$ to the states reachable from $\Delta$ in the graphical representation of the pLTS
yields a finitary sub-pLTS\@. Similarly, a subdistribution $\Delta$ is \emph{finite} if
restricting $S$ to the states reachable from $\Delta$
yields a finitary sub-pLTS without loops.

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

A \emph{test} is a finite distribution over the state set of a pLTS having 
$\Act_\tau \cup \Omega$ as its set of transition labels, where $\Omega$ is a
set of fresh \emph{success} actions, not already in $\Act_\tau$, introduced specifically to
report testing outcomes.\footnote{For \emph{vector-based} testing we
  normally take $\Omega$ to be countably infinite \cite{Seg96}.  This
  way we have an unbounded supply of success actions for
  building tests, of course without obligation to use them all.
  \emph{Scalar} testing is obtained by taking $|\Omega|=1$.}
For simplicity we may assume a fixed pLTS of
processes---our results apply to any choice of such a pLTS---and a
fixed pLTS of tests.  Since the power of testing depends on the expressivity
of the pLTS of tests---in particular certain types of tests are
necessary for our results---let us just postulate that this pLTS is sufficiently expressive
for our purposes --- for example that it can be used to interpret all
processes from the language \pCSP, as in our previous papers
\cite{gdpf,lmcs,concur}. \footnote{In \cite{concur} tests are allowed to be finitary, but
  if two processes are behaviourally different they can be distinguished by some
  characteristic tests which are always finite. Therefore, the results in \cite{concur}
  still hold if tests are required to be finite, as we do here.}
  
Although we use success \emph{actions}, they are used merely to mark
certain states as success states, namely the sources of transitions labelled by success
actions. For this reason we systematically ignore
the distributions that can be reached after a success action.
We impose two requirements on all states in a pLTS of tests, namely
\begin{itemise}
\item[(A)]\label{uniqueness}
if $t \ar{\omega_1}$ and $t \ar{\omega_2}$ with $\omega_1,\omega_2\in\Omega$
then $\omega_1 = \omega_2$.\hfill\textit{uniqueness}
\item[(B)]
if $t \ar{\omega}$ with $\omega\in\Omega$ and $t \ar{\alpha} \Delta$ with
$\alpha\in\Act_\tau$ then $u\ar{\omega}$ for all $u\in\support{\Delta}$.\hfill\emph{no $\omega$-disabling}
\end{itemise}
The first condition says that a success state can have one success
identity only, whereas the second condition is a slight weakening
of the requirement from \cite{JHW94} that success states must be end
states; it allows further progress from an $\omega$-success state, for
some $\omega\in\Omega$, but $\omega$ must remain enabled.
\footnote{This simplifies our treatment of test but, as can be seen from
 Appendix A of \cite{esop}, it is not a heavy restriction.}

To apply test $\Theta$ to process $\Delta$ we form a parallel
composition $\Theta \parT \Delta$ in which \emph{all} visible actions
of $\Delta$ must synchronise with $\Theta$. Those synchronisations are
immediately renamed into $\tau$ so that the resulting composition is a
process whose only possible actions are the elements of $\Omega_\tau
:=\Omega \cup \{\tau\}$.  Formally, if $\langle {\bf P}, \Act,
\rightarrow_{\bf P} \rangle$ and $\langle {\bf T}, \Act \cup
\Omega, \rightarrow_{\bf T} \rangle$ are the pLTSs of processes and
tests, then the pLTS of applications of tests to processes is $\langle
{\bf C}, \Omega, \rightarrow \rangle$, with ${\bf C} =
\{t\|p \mid t \inp {\bf T} \wedge p\inp {\bf P}\}$ and $\rightarrow$ the
transition relation generated by the rules in Fig.~\ref{fig:par}.
Here if $\Theta\in\dist{\bf T}$ and $\Delta\in\dist{\bf P}$,
then $\Theta \| \Delta$ is the distribution given by $(\Theta \|
\Delta)(t\|p)\mathrel{:=} \Theta(t)\cdot\Delta(p)$.
The resulting pLTS also satisfies (A), (B) above;
this would not be the case if we had strengthened
(B) to require that success states must be end states.

\begin{figure}[t]
$$
   \linferSIDE[\Rlts{par.l}]{t \ar{\alpha}_{\bf T} \Theta}
                 {t \Par{A} p \ar{\alpha} \Theta \Par{A} \pdist{p}}
                 {~~~~~\alpha \mathop{\not\in} \Act}
\qquad
\linferSIDE[\Rlts{par.r}]{p \ar{\tau}_{\bf P} \Delta}
                 {t \Par{A} p \ar{\tau} \pdist{t} \Par{A} \Delta}
                {}
\qquad
   \makebox[4.5cm][l]{$\linferSIDE[\Rlts{par.i}]{t \ar{a}_{\bf T} \Theta\;\;\;p \ar{a}_{\bf P} \Delta\;\;}
                {t \Par{A} p\ar{\tau} \Theta \Par{A} \Delta}
        {a\inp \Act}$}
$$
\caption{Synchronous parallel composition between tests and processes\label{fig:par}}
\end{figure}

We will define the result $\RApply(\Theta,\Delta)$ of applying the test
$\Theta$ to the process $\Delta$ to be a set of testing outcomes, exactly
one of which results from each resolution of the choices in $\Theta \parT \Delta$.
Each \emph{testing outcome} is
an $\Omega$-tuple of real numbers in the interval
[0,1], i.e.\ a function $o:\Omega\rightarrow [0,1]$, and its
$\omega$-component $o(\omega)$, for $\omega \in \Omega$, gives the
probability that the resolution in question will reach an
\emph{$\omega$-success state}, one in which the success action
$\omega$ is possible.

Due to the presence of nondeterminism in pLTSs, we need a mechanism to
reduce a nondeterministic structure into a set of deterministic
structures, each of which determines a single possible outcome. Here we adapt
the notion of \emph{resolution}, defined in \cite{esop} for
probabilistic automata, to pLTSs.

\begin{definition} \bf[Resolution]\rm\label{def:resolution}
A \emph{resolution} of a subdistribution $\Phi \inp\subdist{S}$ in a
pLTS  $\langle S, {\Omega}, \rightarrow \rangle$  is a triple
 $\langle R, \Lambda, \rightarrow_R \rangle$
where
$\langle R, {\Omega}, \rightarrow_R \rangle$ is a deterministic pLTS and
$\Lambda \inp \subdist{R}$, such that there exists a
\emph{resolving function} $f: R\rightarrow S$ satisfying
\begin{enumerate}[(i)]
\item $\Imgf{\Lambda} = \Phi$
\item if $r\ar{\alpha}_R\Lambda'$ for $\alpha\in {\Omega}_\tau$
      then $f(r)\ar{\alpha}\Imgf{\Lambda'}$
\item if $f(r)\ar{\alpha}$ for $\alpha\in {\Omega}_\tau$ then $r\ar{\alpha}_R$\;.
 \end{enumerate}
\end{definition}
\noindent
The reader is referred to Section 2 of \cite{esop} for a detailed
discussion of the concept of resolution, and the manner in which a
resolution represents a run of a process; in particular in a
resolution states in $S$ are allowed to be resolved into distributions,
and computation steps can be \emph{probabilistically interpolated}.
Our resolutions match the results of applying a scheduler as defined
in \cite{Seg95}.

We now explain how to associate  an outcome with a particular
resolution, which in turn will associate a set of outcomes with a
subdistribution in a pLTS\@. Given a deterministic pLTS $\langle R,
{\Omega}, \rightarrow_R \rangle$ consider the functional
\begin{math}\label{page:resolutions}
  {\cal F}: (R \rightarrow [0,1]^\Omega) \rightarrow  (R \rightarrow [0,1]^\Omega)
\end{math}
defined by
\begin{align}\label{eq:functional}
   {\cal F}(g)(r)(\omega) \mathrel{:=}
\begin{cases}
1 &\mbox{if $r \ar{\omega}$}\\
0 &\mbox{if $r \nar{\omega}$ and $r \nar{\tau}$}\\
\Exp{\Delta}(g)(\omega) &\mbox{if $r \nar{\omega}$ and $r \ar{\tau}
\Delta$.} 
\end{cases}
\end{align}
We view the unit interval $[0,1]$ ordered in
the standard manner as a complete lattice;
this induces the structure of a complete lattice on the product   $ [0,1]^\Omega$ and in turn
on the  set of functions
$R \rightarrow [0,1]^\Omega$.  The functional ${\cal F}$ is easily seen to be
monotonic and therefore has a least fixed point, which we denote by
$\ResultsN_{\langle R, {\Omega}, \rightarrow_R \rangle}$; this is abbreviated to $\ResultsN$ when the
deterministic pLTS in question is understood.
Intuitively $\Exp{\Lambda}(\ResultsN_{\langle R, {\Omega}, \rightarrow_R \rangle})$ is the result of executing
the resolution $\langle R, \Lambda, \rightarrow_R \rangle$
starting from the initial distribution $\Lambda$, a vector of
probabilities.  From Definition~\ref{def:resolution}
we see that in general a distribution $\Phi$ gives rise to a non-empty set of resolutions.
Collecting all of the possible results of executing them we get
\begin{equation}\label{eq:apply}
\RApply(\Phi) = \setof {\Exp{\Lambda}(\ResultsN_{\langle R, {\Omega}, \rightarrow_R \rangle})}
{\langle R, \Lambda, \rightarrow_R \rangle \mbox{ is a resolution of }  \Phi
}\;.
  \end{equation}
This notation is most often used in calculating the results of applying a test to a process.
To emphasise this, we will sometimes use the notation  $\RApply(\Theta,\Delta)$ for 
$\RApply( \Theta \| \Delta)$.

\begin{figure}[t]
\begin{center} \tiny
\includegraphics[width=8cm,height=5.5cm]{Qa.eps}
\end{center}
\caption{Testing the  process $\pdist{q_1}$} \label{fig:ex1B}
\end{figure}

\begin{example}\rm\label{ex:ex1B}
  Consider the process $\pdist{q_1}$ depicted in Figure~\ref{fig:ex1B}(a).
When we apply the test
  $\pdist{t}$ depicted in Figure~\ref{fig:ex1B}(b) to it we get the process
  $\pdist{t\|q_1}$ depicted in  Figure~\ref{fig:ex1B}(c).
This process is already deterministic, hence has essentially only one resolution: itself.
Moreover the outcome {$\Exp{\pdist{t\|q_1}}(\ResultsN) =
  \ResultsN(t\|q_1)$} associated with it is
the least solution of the equation
\begin{math}
  \ResultsN(t\|q_1) = \frac{1}{2}\cdot \ResultsN(t\|q_1) + \frac{1}{2}\vec{\omega}
\end{math}
where $\vec{\omega}: \Omega\rightarrow[0,1]$ is the $\Omega$-tuple
with $\vec{\omega}(\omega)=1$ and $\vec{\omega}(\omega')=0$ for all
$\omega'\not=\omega$.
In fact this equation has a unique solution in $[0,1]^\Omega$, namely $\vec{\omega}$.
Thus $\RApply(\pdist{t},\pdist{q_1}) = \sset{\vec{\omega}}$.  
\end{example}

\begin{example}\rm\label{ex:ex2B}
  Consider the process
$\pdist{q_2}$ and the application of the test $\pdist{t}$ to it, as
outlined in Figure~\ref{fig:ex2}.
For each $k \geq 1$ the process $\pdist{t \parT q_2}$ has a resolution
$\langle R_k, \Lambda, \rightarrow_{R_k} \rangle$ such that
$\Exp{\Lambda}(\ResultsN) = (1 \mathord-\frac{1}{2^k})\vec{\omega}$; intuitively it goes around
the loop $(k-1)$ times before at last taking the right hand $\tau$
action.  Thus $\RApply(\pdist{t},\pdist{q_2})$ contains $(1 - \frac{1}{2^k})\vec{\omega}$ for
every $k \geq 1$. But it also contains $\vec{\omega}$, because of the
resolution which takes the left hand $\tau$-move every time. Thus
$\RApply(\pdist{t},\pdist{q_2})$ includes the set
\begin{align*}\textstyle
\sset{(1 \mathord-\frac{1}{2})\vec{\omega},\;
      (1\mathord-\frac{1}{2^2})\vec{\omega},\ldots, (1 \mathord-\frac{1}{2^k})\vec{\omega}, \ldots, \vec{\omega}}
\end{align*}
As resolutions allow any interpolation between the two $\tau$-transitions
from state $s_1$,
$\RApply(\pdist{t},\pdist{q_2})$ is actually the convex closure of the above set.
\begin{figure}[t]
\begin{center}
\includegraphics[width=12cm,height=6cm]{Q2.eps}
\end{center}
\caption{Testing the process $\pdist{q_2}$} \label{fig:ex2}
\end{figure}
\end{example}

\noindent
There are two standard methods for comparing two sets of ordered outcomes:
\vspace{-5pt}
\begin{align*}
  O_1 \Hleq O_2  &\qquad\text{if for every $o_1 \in O_1$ there exists some $o_2 \in O_2$ such that $o_1 \leq o_2$}
\\[-3pt]
  O_1 \Sleq O_2  &\qquad\text{if for every $o_2 \in O_2$ there exists some $o_1 \in O_1$ such that $o_1 \leq o_2$}
\end{align*}
This gives us our definition of the probabilistic may- and must-testing preorders;
they are decorated with $\Times^\Omega$ for
the repertoire $\Omega$ of testing actions they employ.

\begin{definition} \bf[Probabilistic testing preorders]\rm\label{def:d1445}\qquad
  \begin{enumerate}[(i)]
  \item $\Delta \pmMayleq \Gamma$ if for every $\Omega$-test $\Theta$, $\RApply(\Theta,\Delta) \Hleq \RApply(\Theta,\Gamma) $.
  \item $\Delta \pmMustleq \Gamma$ if for every $\Omega$-test $\Theta$, $\RApply(\Theta,\Delta) \Sleq \RApply(\Theta,\Gamma) $.
\end{enumerate}
These preorders are abbreviated to $\Delta \pMayleq \Gamma$ and $\Delta \pMustleq \Gamma$ when $\size{\Omega} = 1$.
\end{definition}

In \cite{esop} we established that for finitary processes $\pmMayleq$
coincides with $\pMayleq$ and $\pmMustleq$ with $\pMustleq$ for any
choice of $\Omega$.  We also defined the reward-testing preorders in
terms of the mechanism set up so far. The idea is to associate with
each success action $\omega\in \Omega$ a reward, which is a nonnegative
number in the unit interval $[0,1]$; and then a run of a probabilistic
process in parallel with a test yields an expected reward accumulated
by those states which can enable success actions. A reward tuple $h\in
[0,1]^\Omega$ is used to assign reward $h(\omega)$ to success action
$\omega$, for each $\omega\in\Omega$.
Due to the presence of nondeterminism, the application of a test
$\Theta$ to a process $\Delta$ produces a set of expected rewards.
Two sets of rewards can be compared by examining their suprema/infima; this gives
us two methods of testing called reward may/must testing. In
\cite{esop} all rewards are required to be nonnegative, so we refer to
that approach of testing as \emph{nonnegative-reward testing}. If we
also allow negative rewards, which intuitively can be understood as
costs, then we obtain an approach of testing called \emph{real-reward
  testing}. Technically, we simply let reward tuples $h$ range over
the set $[-1,1]^\Omega$. If $o\in [0,1]^\Omega$, we use the
dot-product $h\cdot o=\sum_{\omega\in\Omega} h(\omega)\cdot
o(\omega)$. It can apply to a set $O\subseteq [0,1]^\Omega$ so that
$h\cdot O=\sset{h\cdot o\mid o\in O}$. Let $A\subseteq [-1,1]$. We use
the notation $\bigsqcup A$ for the supremum of set $A$, and $\bigsqcap
A$ for the infimum.
\begin{definition} \bf[Reward testing preorders]\rm\label{def:d1509}\qquad
 \begin{enumerate}[(i)]
  \item $\Delta \nrmMayleq \Gamma$ if for every $\Omega$-test $\Theta$ and nonnegative-reward tuple $h\in [0,1]^\Omega$,\\ $\bigsqcup h\cdot\RApply(\Theta,\Delta) \leq \bigsqcup h\cdot \RApply(\Theta,\Gamma) $.
  \item $\Delta \nrmMustleq \Gamma$ if for every $\Omega$-test $\Theta$ and nonnegative-reward tuple $h\in [0,1]^\Omega$,\\ $\bigsqcap h\cdot\RApply(\Theta,\Delta) \leq \bigsqcap h\cdot\RApply(\Theta,\Gamma) $.
  \item $\Delta \rrmMayleq \Gamma$ if for every $\Omega$-test $\Theta$ and real-reward tuple $h\in [-1,1]^\Omega$,\\ $\bigsqcup h\cdot\RApply(\Theta,\Delta) \leq \bigsqcup h\cdot\RApply(\Theta,\Gamma) $.
  \item $\Delta \rrmMustleq \Gamma$ if for every $\Omega$-test $\Theta$ and real-reward tuple $h\in [-1,1]^\Omega$,\\ $\bigsqcap h\cdot\RApply(\Theta,\Delta) \leq \bigsqcap h\cdot\RApply(\Theta,\Gamma) $.
\end{enumerate}
This time we drop the superscript $\Omega$ iff $\Omega$ is countably infinite.
\end{definition}

\noindent
It is shown in Corollary 1 of \cite{esop} that nonnegative-reward testing is equally powerful as probabilistic testing.
\begin{theorem} {\bf\cite{esop}}\label{thm:nr.pb}
For any finitary processes $\Delta$ and $\Gamma$,
\begin{enumerate}[(i)]
\item $\Delta \nrMayleq \Gamma$ if and only if $\Delta \pMayleq \Gamma$.
\item $\Delta \nrMustleq \Gamma$ if and only if $\Delta \pMustleq \Gamma$.
\end{enumerate}
\end{theorem}

\noindent
In this paper we focus on the real-reward testing preorders
$\rrMayleq$ and $\rrMustleq$, by comparing them with the nonnegative
reward testing preorders $\nrMayleq$ and $\nrMustleq$.
Although these two nonnegative-reward testing preorders are in
general incomparable, we have for the real-reward testing preorders:

\begin{theorem}\label{thm:rrmay.rrmust}
For any processes $\Delta$ and $\Gamma$, it holds that
 $\Delta \rrMayleq \Gamma$ if and only if $\Gamma \rrMustleq \Delta$.
\end{theorem}
\begin{proof}
We first notice that for any nonempty set $A\subseteq [0,1]^\Omega$ and any reward tuple $h\in [-1,1]^\Omega$,
\begin{equation}\label{e:h1}
\bigsqcup h\cdot A \Wide{=} -(\bigsqcap\; (-h)\cdot A)
\end{equation}
where $-h$ is the negation of $h$, i.e.\ $(-h)(\omega)=-(h(\omega))$ for any $\omega\in\Omega$. We consider the ``if'' direction; the ``only if'' direction is similar.
Let $\Theta$ be any $\Omega$-test and $h$ be any real reward tuple in $[-1,1]^\Omega$. Clearly, $-h$ is also a real reward tuple. Suppose $\Gamma \rrMustleq \Delta$, then
\begin{equation}\label{e:h2}
\bigsqcap\; (-h)\cdot\RApply(\Theta,\Gamma) \Wide{\leq} \bigsqcap\; (-h)\cdot\RApply(\Theta,\Delta)
\end{equation}
Therefore, we can infer that\\[2ex]\mbox{}\hfill
$\begin{array}[b]{rcll}
\bigsqcup h\cdot \RApply(\Theta,\Delta) & = &
 -(\bigsqcap\; (-h)\cdot \RApply(\Theta,\Delta)) \quad &\mbox{by (\ref{e:h1})}\\
& \leq &  -(\bigsqcap\; (-h)\cdot \RApply(\Theta,\Gamma)) \quad &\mbox{by (\ref{e:h2})}\\
& = & \bigsqcup h\cdot \RApply(\Theta,\Gamma) \quad &\mbox{by (\ref{e:h1})}.
\end{array}$
\end{proof}

\noindent
Our next task is to compare $\rrMustleq$ with $\nrMustleq$. The former
is included in the latter, which directly follows from
Definition~\ref{def:d1509}. Surprisingly, it turns out that for
finitary convergent processes the latter is also included in the
former, thus establishing that the two preorders are in fact the same. The rest of the
paper is devoted to proving this result. However, we first show that
this result does not extend to divergent processes.

\begin{example}\label{ex:divergence}
Consider the processes $\pdist{q_1}$ and $\pdist{q_2}$ depicted in Figure~\ref{fig:diverg}.
Using the characterisations of $\pMayleq$ and $\pMustleq$ in \cite{concur},
it is easy to see that these processes cannot be distinguished by
probabilistic may- and must testing, and hence not by nonnegative-reward testing either.
However, let $\pdist{t}$ be the test in the right diagram of Figure~\ref{fig:diverg} that first synchronises on the action
$a$, and then with probability $\frac{1}{2}$ reaches a state in which a reward
of $-2$ is allocated, and with the remaining probability $\frac{1}{2}$
synchronises with the action $b$ and reaches a state that yields a reward of $4$.
Thus the test employs two success actions $\omega_1$ and $\omega_2$, and we use
the reward tuple $h$ with $h(\omega_1)=-2$ and $h(\omega_2)=4$.
Then the resolution of $\pdist{q_1}$ that does not involve the
$\tau$-loop contributes the value  $-2\cdot \frac{1}{2} + 4\cdot \frac{1}{2} = -1+2 = 1$
to the set $h\cdot\RApply(\pdist{t},\pdist{q_1})$, whereas the
resolution that only involves the $\tau$-loop contributes the value $0$.
Due to interpolation, $h\cdot\RApply(\pdist{t},\pdist{q_1})$ is in fact
the entire interval $[0,1]$. On the other hand, the resolution
corresponding to the $a$-branch of $q_2$ contributes the value $-1$ and
$h\cdot\RApply(\pdist{t},\pdist{q_2}) = [-1,1]$.
Thus 
$\bigsqcap h\cdot\RApply(\pdist{t},\pdist{q_1}) = 0 >
 -1 = \bigsqcap h\cdot\RApply(\pdist{t},\pdist{q_2})$,
and hence $\pdist{q_1} \not \rrMustleq \pdist{q_2}$.
\end{example}


\section{Failure simulations}\label{sec:derivation}
In this section we explain the characterisation of 
probabilistic testing from \cite{lmcs,concur};
it depends on a generalisation of failure simulations \cite{vG93} to the probabilistic 
setting. The key ingredient is that of weak derivations for distributions.
To deal with infinite (but finitary) processes, we need to employ the
weak derivations of \cite{concur} rather than those of \cite{lmcs}.

In a pLTS actions are performed only by states, in that actions are
given by relations from states to distributions. But processes
in general correspond to distributions over states, so in order to
define what it means for a process to perform an action, we need to
\emph{lift} these relations so that they also apply to
distributions. In fact we will find it convenient to lift them to
subdistributions.
\begin{definition}\rm\label{def:lift}
Let $(S,L,\rightarrow)$ be a pLTS and $\mathord{\aRel} \subseteq
  S\times\subdist{S}$ be a relation from states to subdistributions.
Then $\mathord{\lift{\aRel}} \subseteq \subdist{S} \times \subdist{S}$
is the smallest relation that satisfies:\vspace{-1ex}
\begin{enumerate}[(i)]
\item $s \aRel \Delta$ implies $\pdist{s} \lift{\aRel} \Delta$, and
\vspace{-1ex}
\item\label{i1529} (Linearity)
 $\Gamma_i \lift{\aRel} \Delta_i$ for $i\inp I$ implies
 $(\sum_{i\in I}p_i\Times\Gamma_i)~\lift{\aRel}~(\sum_{i\in I}p_i\Times\Delta_i)$
 for any $p_i \inp [0,1]$ ($i\inp I$) with $\sum_{i\in I}p_i \leq 1$, where $I$ is a countable set.
\end{enumerate}
\end{definition}

\noindent
An application of this notion is when the relation is $\ar{\alpha}$
for $\alpha\in \Act_\tau$; in that case we also write $\ar{\alpha}$
for $\lift{\raisebox{0pt}[0.7em][0pt]{$\ar{\alpha}$}}$. Thus, as source of a relation $\ar{\alpha}$ we
now also allow distributions, and even subdistributions.
A subtlety of this approach is that for any action $\alpha$, we have
$\eDis \ar{\alpha} \eDis$
simply by taking $I=\emptyset$ or $\sum_{i\in I}p_i=0$ in
Definition~\ref{def:lift}. That turns out to make $\eDis$ especially useful for
modelling the ``chaotic'' aspects of divergence in \cite{concur}, in
particular that in the must-case a divergent process can mimic any
other.

Definition~\ref{def:lift} is very similar to  our previous definition in \cite{lmcs},
although there it applied only to (full)  distributions:
\begin{lemma}\label{lem:l1415}
  $\Gamma \lift{\aRel} \Delta$ if and only if
\begin{enumerate}[(i)]
\vspace{-1ex}
\item
$\Gamma = \sum_{i\in I} p_i \Times \pdist{s_i}$, where
  $I$ is an index set and  $\sum_{i\in I}{p_i} \leq 1$,
\vspace{-1ex}
\item
For each $i \in I$ there is a subdistribution $\Delta_i$ such that
$s_i \aRel \Delta_i$\,,
\vspace{-1ex}
\item
$\Delta = \sum_{i \in I} p_i \Times \Delta_i$.
\end{enumerate}
\begin{proof}
Straightforward.
\end{proof}
\end{lemma}
An important point here is that a single state can be split into
several pieces: that is, the decomposition of $\Gamma$ into
$\sum_{i\in I}{p_i \Times \pdist{s_i}}$ is not unique.

\begin{definition} \bf[Weak derivation]\rm
\label{def:d0839}
Suppose we have subdistributions $\Delta, \Delta_k^{\rightarrow},
\Delta_k^{\Stop}$, for $k \geq 0$, with the following properties:
\vspace{-1.5em}
\label{weaktau}
\begin{eqnarray*}
  \Delta &=& \Delta_0^{\rightarrow} + \Delta_0^\Stop\\
  \Delta_0^{\rightarrow}  &\ar{\tau}& \Delta_1^{\rightarrow} + \Delta_1^\Stop\\[-7pt]
&\vdots \\
  \Delta_k^{\rightarrow}  &\ar{\tau}& \Delta_{k{+}1}^{\rightarrow} + \Delta_{k{+}1}^\Stop~.\\[-7pt]
&\vdots
\end{eqnarray*}
\vspace{-2em}

\noindent
Then we call $\Delta'\Defs \sum_{k=0}^\infty \Delta_k^{\Stop}$ a
\emph{weak derivative} of $\Delta$, and write $\Delta\dar{}\Delta'$
to mean that $\Delta$ can make a \emph{weak derivation} to its
derivative $\Delta'$.
\end{definition}
\noindent
There is always at least one weak derivative of any subdistribution (the
subdistribution itself) and there can be many.

\begin{proposition}{\bf[Transitivity, linearity and decomposition of weak derivations \cite{finitary}]}
\label{finitary import}\vspace{-1pt}
\begin{enumerate}[(i)]
\item If $\Delta \dar{} \Delta'$ and $\Delta' \dar{} \Delta''$ then $\Delta \dar{} \Delta''$.\vspace{-3pt}
\item []\mbox{}\hspace{-27pt} Let $p_i \in [0,1]$ for $i\inp I$ with $\sum_{i\in I}p_i \leq 1$.
\item If $\Delta_i \dar{} \Delta'_i$ for all $i \inp I$
  then $\sum_{i\in I} p_i\Times\Delta_i \dar{} \sum_{i\in I} p_i\Times\Delta'_i$.
\item If $\sum_{i\in I} p_i \Times \Delta_i \dar{} \Delta'$ then $\Delta' = \sum_{i\in I} p_i \Times \Delta'_i$ for
  subdistributions $\Delta'_i$ such that $\Delta_i \dar{} \Delta'_i$ for all $i\inp I$.
\end{enumerate}
\end{proposition}

\noindent
We now use these weak derivations to define, in the standard manner of \cite{ccs}, weak
action relations between derivations; these, together with 
 the refusal relations $\nar{A}$ for $A
\subseteq \Act$  are the key ingredients in the definition of
the failure-simulation preorder.  
\begin{definition}\rm\label{def:weak.refuse}
Let $\Delta$ and its variants $\Delta', \Delta^{\text{pre}}, \Delta^{\text{post}}$ be
subdistributions in a pLTS $\langle S,\Act,\rightarrow \rangle$.
\begin{itemize}
\item For $a \in \Act$ write $\Delta \dar{a} \Delta'$ whenever $\Delta
  \dar{} \Delta^{\text{pre}} \ar{a} \Delta^{\text{post}} \dar{}
  \Delta'$, for some $\Delta^{\text{pre}}$ and $\Delta^{\text{post}}$. Extend this to $\Act_\tau$ by allowing as a special case
  that $\dar{\tau}$ is simply $\dar{}$, i.e.\ including identity
  (rather than requiring at least one $\ar{\tau}$).
\item For $A \subseteq \Act$ and $s \inp S$ write
  $\Ref{s}{A}$ if $s \nar{\alpha}$ for every $\alpha \inp A\cup\{\tau\}$;
  write $\Ref{\Delta}{A}$ if $\Ref{s}{A}$ for every $s \inp \support{\Delta}$.
\item More generally write $\RefE{\Delta}{A}$ if $\Delta \dar{}
  \Delta^{\text{pre}}$ for some $\Delta^{\text{pre}}$ such that
  $\Ref{\Delta^{\text{pre}}}{A}$.
\end{itemize}
\end{definition}

\begin{definition} \bf[Failure simulation preorder]\rm\label{def:efailsimA}
Define $\failsime$ to be the largest relation in $S\times\subdist{S}$
such that if $s\failsime\Delta$ then
\begin{enumerate}[(i)]
\item whenever $\pdist{s}\dar{\alpha}\Gamma'$, for $\alpha\inp\Act_\tau$, then
  there is a $\Delta' \inp\subdist{S}$ with
  $\Delta\dar{\alpha}\Delta'$ and $\Gamma'\lift{\failsime}\Delta'$,
\item and whenever $\RefE{\pdist{s}}{A}$ then $\RefE{\Delta}{A}$.
\end{enumerate}
Any relation $\mathord{\aRel} \subseteq S\times\subdist{S}$ that
satisfies the two clauses above is called a {\em failure simulation}.
The failure simulation preorder
$\mathord{\failsimpreo}\subseteq \subdist{S}\times \subdist{S}$ is defined by letting  $\Delta\failsimpreo\Gamma$
whenever there is a $\Delta\match$ with $\Delta\dar{}\Delta\match$ and
$\Gamma\lift{\failsime}\Delta\match$.
\end{definition}
Note that the simulating process, $\Delta$, occurs at the right of
$\failsime$, but at the left of $\failsimpreo$.
The following lemma will bee needed in Section~\ref{sec:agree}.

\begin{lemma}\label{lem:matching}
If $\Gamma\lift{\failsime}\Delta$ and $\Gamma\dar{}\Gamma'$ then
there is a matching transition $\Delta\dar{}\Delta'$ such that $\Gamma'\lift{\failsime}\Delta'$.
\end{lemma}

\begin{proof}
$\Gamma \lift\failsime \Delta$ implies by Lemma~\ref{lem:l1415} that
$\qquad\displaystyle
    \Gamma = \sum_{i \in I}{p_i \cdot \pdist{s_i}},
     \qquad
    s_i \failsime \Delta_i,
     \qquad
   \Delta = \sum_{i \in I}{ p_i \cdot \Delta_i}$.\\
By Proposition~\ref{finitary import}(iii) there are $\Gamma'_i\in\subdist{S}$ for $i\inp I$ with
$\pdist{s_i}\dar{}\Gamma'_i$ and $\Gamma'=\sum_{p_i\in I}p_i\Times\Gamma'_i$.
For each $i \inp I$ we infer from $s_i \failsime \Delta_i$ and $\pdist{s_i} \dar{}
\Gamma'_i$ that there is a $\Delta'_i \inp\subdist{S}$ with
$\Delta_i\dar{}\Delta'_i$ and
$\Gamma'_i\lift{\failsime}\Delta'$. Let $\Delta' := \sum_{i\in
I}p_i\Times \Delta'_i$. Then Definition~\ref{def:lift}(2) and Proposition~\ref{finitary import}(ii)
yield $\Gamma'\lift{\failsime}\Delta'$ and $\Delta\dar{}\Delta'$.
\end{proof}

\noindent
The failure simulation preorder is preserved under parallel composition
with a test and it is sound and complete for probabilistic
must testing of finitary processes.
\begin{theorem} {\bf\cite{concur}}\label{thm:sound.complete}
For finitary processes $\Delta$ and $\Gamma$,
\begin{enumerate}[(i)]
\item If $\Delta \failsimpreo \Gamma$ then for any $\Omega$-test $\Theta$,
$\Theta\parT \Delta \failsimpreo \Theta\parT \Gamma$.
\item $\Delta \failsimpreo \Gamma$ if and only if $\Delta  \pMustleq \Gamma$.
\end{enumerate}
\end{theorem}

\section{From derivations to resolutions}\label{sec:compare}
In this section we explain how resolutions, on which the definitions of
the testing preorders in 
Definitions~\ref{def:d1445} and~\ref{def:d1509} are based, can be seen as certain kinds of derivations. 

\begin{definition} {\bf[Extreme derivatives]}\rm\label{def:d1814}
A state $s$ in a pLTS is called \emph{stable} if $s\nar{\tau}$, and a
subdistribution $\Delta$ is called \emph{stable} if every state in its
support is stable.  We write $\Delta \darE{}\Delta'$ whenever $\Delta
\dar{} \Delta'$ and $\Delta'$ is stable, and call $\Delta'$ an
\emph{extreme} derivative of $\Delta$.
\end{definition}
\noindent
Referring to Definition~\ref{def:d0839}, we see this means that in the extreme
derivation of $\Delta'$ from $\Delta$ at every stage a state must move
on if it can, so that every stopping component can contain only states
which \emph{must} stop: for $s \in \support{\Delta_k^{\rightarrow} + \Delta_k^{\Stop}}$
we have $s \in \support{\Delta_k^{\Stop}}$ if \emph{and now also} only if $s\nar{\tau}$.

\begin{lemma} {\bf[Existence and uniqueness of extreme derivatives]} \label{lem:unique.der}
  \begin{enumerate}[(i)]\item\label{item:i0834} For every
    subdistribution $\Delta$ there exists some (stable) $\Delta'$ such
    that $\Delta \darE{} \Delta'$.
\item\label{item:i1319} In a deterministic pLTS if $\Delta \darE{} \Delta'$ and $\Delta \darE{} \Delta''$ then $\Delta' = \Delta''$.
\end{enumerate}
\end{lemma}
\begin{proof}
We construct a derivation as in Definition~\ref{def:d0839} of a stable $\Delta'$ by
defining the components $\Delta_k, \Delta_k^\Stop$ and
$\Delta_k^\Move$  using induction on $k$. Let us assume that the
subdistribution $\Delta_k$ has been defined; in the base case $k=0$
this is simply $\Delta$. The decomposition of this $\Delta_k$ into
the components $\Delta_k^\Stop$ and $\Delta_k^\Move$ is carried out
by defining the former to be precisely those states which must stop,
i.e.\ those $s$ for which $s\nar{\tau}$. Formally $\Delta_k^\Stop$
is determined by:\vspace{-2ex}
\begin{align*}
\Delta_k^\Stop (s) =
  \begin{cases}
    \Delta_k(s)  & \text{if}\;\; s\nar{\tau}\\
     0           & \text{otherwise}
  \end{cases}
\end{align*}
Then $\Delta_k^\Move$ is given by the \emph{remainder} of $\Delta_k$, namely
those states which can perform a $\tau$ action:
\begin{align*}
\Delta_k^\Move (s) =
  \begin{cases}
    \Delta_k(s)  & \text{if}\;\; s\ar{\tau}\\
     0           & \text{otherwise}
  \end{cases}
\end{align*}
Note that these definitions divide the support of $\Delta_k$  into two disjoints sets,
namely the support of $\Delta_k^\Stop$ and the support of $\Delta_k^\Move$.
Moreover by construction we know that $\Delta_k^\Move   \ar{\tau} \Theta$ for some $\Theta$;
we let $\Delta_{k+1}$ be an arbitrary such $\Theta$.

This completes our construction of an extreme derivative as in Definition \ref{def:d0839} and so
we have established   (\ref{item:i0834}).


  For (\ref{item:i1319}) we observe that in a deterministic pLTS the
  above choice of $\Delta_{k+1}$ is unique, so that the whole
  derivative construction becomes unique.
\end{proof}

\noindent
\emph{Sub}distributions are essential in the definition of extreme derivations.
Consider  a state $t$ that has only one transition, a self $\tau$-loop
$t\ar{\tau}\pdist{t}$.  Then it diverges and it has a unique
extreme derivative $\eDis$, the empty subdistribution. More generally, suppose a subdistribution
$\Delta$ diverges, that is there is an infinite sequence of
internal transitions \mbox{$\Delta \ar{\tau}
\Delta_1 \ar{\tau} \ldots \Delta_k \ar{\tau} \ldots$}.  Then one
extreme derivative of $\Delta$ is $\eDis$, but it may have others.

In the extreme derivative $\Delta \darE{} \Delta'$, the  
subdistribution $\Delta'$ may be viewed as a final result of 
an execution starting in $\Delta$ and dynamically resolving nondeterministic choices 
as the execution proceeds. We can tabulate the outcome of this execution in the following manner:
\begin{definition} {\bf[Outcomes]}\rm\label{def:immediate reward}
The outcome $\Rfun\Phi \in [0,1]^\Omega$ of a stable subdistribution
$\Phi$ is given by
$\Rfun\Phi(\omega) = \sum\sset{\Phi(s) \mid s \in \support{\Phi},~s \ar{\omega}}$.
For any distribution $\Phi$ we write  $\cV(\Phi)$ for
the set of possible outcomes $\sset{\Rfun\Phi'\mid
\Phi\darE{}\Phi'}$ via extreme derivatives.
\end{definition}

\noindent
Let $p_i \in [0,1]$ for $i\inp I$ with $\sum_{i\in I}p_i \leq 1$, and let $\Delta_i,\Phi_i$, for
$i\in I$, be subdistributions. We use $\sum_{i\in I} p_i\Times \cV(\Delta_i)$ as shorthand for
$\{\sum_{i\in I} p_i\Times\nu_i \mid \nu_i \in \cV(\Delta_i)\}$.
By construction, $\Rfun\sum_{i\in I}p_i\Times\Phi_i = \sum_{i\in I}p_i\Times\Rfun\Phi_i$.
Using this, we establish the linearity of $\cV$:

\begin{lemma}\label{lem:linearity of outcomes}
Let $p_i \in [0,1]$ for $i\inp I$ with $\sum_{i\in I}p_i \leq 1$.
Then $\cV(\sum_{i\in I} p_i\Times\Delta_i) = \sum_{i\in I} p_i\Times \cV(\Delta_i)$.
\end{lemma}

\begin{proof}
Suppose $\nu \in \cV(\sum_{i\in I} p_i\Times\Delta_i)$.
Then $\nu=\Rfun\Phi$ for some stable $\Phi$ with $\sum_{i\in I} p_i\Times\Delta_i \dar{} \Phi$.
By Proposition~\ref{finitary import}(iii) $\Phi$ can be written as $\sum_{i\in I}p_i\Times\Phi_i$
for subdistributions $\Phi_i$ such that $\Delta_i \dar{} \Phi_i$ for all $i\inp I$; moreover,
the $\Phi_i$ must be stable. Hence $\nu_i := \Rfun\Phi_i\in\cV(\Delta_i)$ and thus $\nu =
\sum_{i\in I} p_i\Times\nu_i \in \sum_{i\in I} p_i\Times\cV(\Delta_i)$.

Conversely, suppose $\nu \in\sum_{i\in I} p_i\Times \cV(\Delta_i)$, i.e.,
$\nu = \sum_{i\in I} p_i\Times\nu_i$ with $\nu_i \in\cV(\Delta_i)$.
Then for all $i\in I$ there are stable subdistributions $\Phi_i$ with $\nu_i := \Rfun\Phi_i$ and
$\Delta_i \dar{} \Phi_i$. So $\sum_{i\in I} p_i\Times\Delta_i \dar{} \sum_{i\in I}p_i\Times\Phi_i$
by Proposition~\ref{finitary import}(ii). Moreover $\sum_{i\in I}p_i\Times\Phi_i$ is stable and
$\nu = \sum_{i\in I} p_i\Times\nu_i = \Rfun\sum_{i\in I}p_i\Times\Phi_i\in \cV(\sum_{i\in I} p_i\Times\Delta_i)$. 
\end{proof}

\noindent
The following two examples illustrate that this manner of calculating outcomes 
often gives the same result as when resolutions are used.
\begin{example}\rm\label{ex:ex1} (Revisiting Example~\ref{ex:ex1B}.)
The pLTS  in  Figure~\ref{fig:ex1B}(c) is deterministic and 
therefore 
from part (\ref{item:i1319}) of Lemma~\ref{lem:unique.der}
it follows that $\pdist{t\parT q_1}$  has a unique extreme derivative
$\Lambda$. Moreover $\Lambda$ can be calculated to be
\plat{\begin{math}
  \sum_{k \geq 1} \frac{1}{2^k} \cdot \pdist{s_3},
\end{math}}
which simplifies to the distribution $\pdist{s_3}$. Therefore, 
since 
$\Rfun\pdist{s_3}=\vec{\omega}$,  it follows that 
$\cV(\pdist{t\parT q_1}) = \sset{\vec{\omega}}$.
This is exactly the same result as obtained
in  Example~\ref{ex:ex1B}, using resolutions.
\end{example}

\begin{example}\rm\label{ex:ex2} (Revisiting Example~\ref{ex:ex2B}.)
The application of the test $\pdist{t}$ to processes $\pdist{q_2}$
is outlined in Figure~\ref{fig:ex2}(c).
Consider any extreme derivative $\Delta'$ from $s_0 = \pdist{t} \parT \pdist{q_2}$.
Using the
notation of Definition~\ref{def:d0839}, it is clear that
$\Delta_0^\Stop$ and $\Delta_0^\Move$ must be $\eDis$ and $\pdist{s_0}$ respectively.
Similarly,  $\Delta_1^\Stop$ and $\Delta_1^\Move$ must be
$\eDis$ and $\pdist{s_1}$ respectively.
 But $s_1$ is a
nondeterministic state, having two possible transitions:
\begin{enumerate}[(i)]
\item $s_1 \ar{\tau} \Lambda_0$ where $\Lambda_0$ has support $\sset{s_0,s_2}$ and assigns each of them
the weight $\frac{1}{2}$

\item $s_1 \ar{\tau} \Lambda_1$ where $\Lambda_1$ has the support $\sset{s_3,s_4}$, again dividing the mass
equally among them.
\end{enumerate}
So  there are many possibilities for $\Delta_2$;
from Definition~\ref{def:d0839} one sees that in fact $\Delta_2$ can be of the form
\vspace{-1ex}
\begin{equation}\label{eq:choiceofp}
  p \cdot \Lambda_0 + (1-p) \cdot \Lambda_1
\vspace{-1ex}
\end{equation}
for any choice of $p \in [0,1]$.

Let us consider one possibility, an extreme one where $p$ is chosen to be $0$; only the transition
(ii) above is used.  Here $\Delta_2^\Move$ is the subdistribution $\frac{1}{2}\pdist{s_4}$, and
$\Delta_k^\Move = \eDis$ whenever $k >2$. A simple calculation shows that in this case the extreme
derivative generated is  $ \Lambda_1^e =
\frac{1}{2}\pdist{s_3}+\frac{1}{2}\pdist{s_6}$ which implies that
$\frac{1}{2}\vec{\omega} \in  \cV(\pdist{t} \parT \pdist{q_2})$.

Another possibility for $\Delta_2$ is $\Lambda_0$, corresponding to
$p = 1$ in (\ref{eq:choiceofp}) above. Continuing
this derivation leads to $\Delta_3$ being $\frac{1}{2} \cdot
\pdist{s_1} + \frac{1}{2} \cdot \pdist{s_5}$; thus
$\Delta_3^\Stop = \frac{1}{2} \cdot  \pdist{s_5}$ and
$\Delta_3^\Move = \frac{1}{2} \cdot \pdist{s_1}$. Now in the
generation of $\Delta_4$ from $\Delta_3^\Move$ again we
resolve a transition from the nondeterministic state $s_1$, by
choosing some arbitrary $p \in [0,1]$ in (\ref{eq:choiceofp}).
Suppose we choose $p\mathbin=1$ every time, completely ignoring
transition (ii) above. Then the extreme derivative generated is
\vspace{-1ex}
\begin{equation*}
  \Lambda_0^e = \sum_{k \geq 1} \frac{1}{2^k} \cdot  \pdist{s_5}
\vspace{-1ex}
\end{equation*}
which simplifies to the distribution $\pdist{s_5}$. This in turn
means that $\vec{\omega} \in 
 \cV(\pdist{t} \parT \pdist{q_2})$.

We have seen two possible derivations of extreme derivatives from
$\pdist{s_0}$.  But there are many others.  In general whenever
$\Delta_k^\Move$ is of the form $q \cdot \pdist{s_1}$ we have to
resolve the nondeterminism by choosing a $p \in [0,1]$ in
(\ref{eq:choiceofp}) above; moreover each such choice is
independent. It turns out that every extreme derivative
$\Delta'$ of $\pdist{s_0}$ is of the form
\begin{math}
  q \cdot \Lambda_0^e + (1\mathord-q)\cdot \Lambda_1^e
\end{math}
for some choice of $q \in [0,1]$, which implies that
$\cV(\pdist{t} \parT \pdist{q_2})$ 
is the convex closure of the set $\sset{\frac{1}{2}\vec{\omega},\vec{\omega}}$.

Again this is similar to the results obtained using resolutions, in 
Example~\ref{ex:ex2B}.
\end{example}
\noindent
Unfortunately there is not an exact agreement between 
using resolutions and extreme derivations, as the next example shows.
\begin{example}\label{ex:pruning} \rm
Let $\pdist{p}$ be a process that first does an $a$-action, to the
point distribution $\pdist{q}$, and then diverges, via the
$\tau$-loop $q \ar{\tau}\pdist{q}$. Let $\pdist{t}$ be the test used in
Examples~\ref{ex:ex1B} and~\ref{ex:ex2B}.  
It is easy to see that the distribution $\pdist{p \parT t}$ has a unique resolution, 
with expected outcome $\vec{\omega}$; thus $\RApply(\pdist{t},\pdist{p}) = \sset{\vec{\omega}}$. 

It turns out that $\pdist{t}\parT \pdist{p}$ also has a unique extreme
derivative; unfortunately this turns out to be $\eDis$.  Since $\Rfun
\eDis = 0$ this means that $\cV(\pdist{t}\parT \pdist{p}) = \vec{0}$; so in
this case, which is actually nonprobabilistic, there is a difference
between the use of resolutions and extreme derivations.  
\end{example}
To rectify this anomaly, we restrict our attention to a subset of pLTSs. 

\begin{definition} \bf[$\omega$-respecting] \rm A pLTS $\langle S, \Omega, \rightarrow \rangle$
is said to be \emph{$\omega$-respecting} when it satisfies the uniqueness requirement
(A) from Page~\pageref{uniqueness}, and
$s \ar{\omega}$, for any $\omega \in \Omega$, implies $s \nar{\tau}$.
\end{definition}
\noindent
It is straightforward to modify the pLTS of applications of tests to
processes into one that it is $\omega$-respecting, namely by removing
all transitions $s \ar{\tau}\Delta$ for states $s$ with $s
\ar{\omega}$; we call this \emph{pruning}. 
We denote the result of pruning the pLTS $\langle S, \Omega, \rightarrow \rangle$ by
$\langle S, \Omega, [\rightarrow] \rangle$, and
the distribution $\Phi$ in this pruned pLTS by $[\Phi]$.

\begin{example}(Revisiting  Example~\ref{ex:pruning}) \rm
Let $\pdist{p}, \pdist{q}$ and $\pdist{t}$ be as in
Example~\ref{ex:pruning}. As we have already seen, 
$\pdist{t}\parT \pdist{p}$ has the unique derivative 
$\eDis$. But by pruning it we obtain a different extreme derivative. 
If we denote the state reachable from $\pdist{t}$ with the outgoing $\omega$-transition, 
in Figure~\ref{fig:ex2}(c), as $\omega$ also, then 
$[\pdist{t}\parT \pdist{p}]$ has the unique extreme derivative
$[\omega\parT q]$. Since $\Rfun [\omega\parT q] =\vec{\omega}$,
we obtain $\cV([\pdist{t}\parT \pdist{p}]) = \sset{\vec{\omega}}$;
this is exactly the result obtained using resolutions. 
\end{example}
Note that pruning has no effect on Examples~\ref{ex:ex1} and \ref{ex:ex2},
as the pLTSs concerned are already $\omega$-respecting.
It also has no
effect on the closure of the failure simulation preorder under parallel composition:
\begin{lemma}{\bf \cite{finitary}}\label{lemma:pf}
For finitary processes $\Delta$ and $\Gamma$,
if $\Delta \failsimpreo \Gamma$ then for any $\Omega$-test $\Theta$,
$[\Theta\parT \Delta] \failsimpreo [\Theta\parT \Gamma]$.
\end{lemma}

\bigskip
In the remainder of this section we show that, at least in $\omega$-respecting pLTSs,
using resolutions to calculate outcomes, as used in the definition of testing (Definitions~\ref{def:d1445}
and \ref{def:d1509}), leads to the same results
as using extreme derivations. In the former a set of deterministic structures are associated with
a distribution, while in the latter nondeterministic
choices are resolved dynamically as the derivation proceeds.  
We start by showing that resolution-based testing is insensitive to
pruning. Let $\RPApply(\Phi)$ denote the set of vectors
\[\setof{\Exp{\Lambda}(\ResultsN_{\langle R, {\rm\Omega}, \rightarrow_R \rangle})}
{\langle R, \Lambda, \rightarrow_R \rangle \mbox{ is a resolution of }
[\Phi]}\;.\] 

\begin{proposition}\label{prop:rpa}
For any distribution $\Phi$ in a pLTS $\langle S, \Omega, \rightarrow \rangle$ we have that
$\RPApply(\Phi)=\RApply(\Phi)$.
\end{proposition}
\begin{proof}
``$\supseteq$'': Let $\langle R, \Lambda, \rightarrow_R \rangle$ be a
resolution of $\Phi$.
Then, following Definition~\ref{def:resolution}, $\langle R, [\Lambda], [\rightarrow_R]
\rangle$ is a resolution of $[\Phi]$ and, by (\ref{eq:functional}),
$\Exp{[\Lambda]}(\ResultsN_{\langle R, {\rm\Omega}, [\rightarrow_R] \rangle})
=\Exp{\Lambda}(\ResultsN_{\langle R, {\rm\Omega}, \rightarrow_R \rangle})$.

``$\subseteq$'': Let $\langle R, \Lambda, \rightarrow_R \rangle$ be a
resolution of $[\Phi]$ with resolving function $f$. We construct a resolution
$\langle R', \Lambda, \rightarrow'_R \rangle$ of $\Phi$
as a random extension of $\langle R, \Lambda, \rightarrow_R \rangle$.
For every pair $(s,\alpha)\inp S\times \Omega_\tau$ with $s\ar{\alpha}$
pick a distribution $\Psi^{(s,\alpha)}\inp\dist{S}$ such that $s\ar{\alpha}\Psi^{(s,\alpha)}$.
Now define $R':= R\dcup (S\times\Nat)$, where $\dcup$ denotes the disjoint union operation, and obtain $\rightarrow'_R$
from $\rightarrow_R$ by adding
(A) a transition \plat{$(s,k)\ar{\alpha}'_R\Psi^{(s,\alpha)}_{k+1}$}
for each $k\inp\Nat$ and each $s\inp S$ with $s\ar{\alpha}$,
and (B) a transition $r\ar{\tau}'_R\Psi^{(f(r),\tau)}_0$ for each
$r\inp R$ with $f(r)\ar{\tau}$ as well as $f(r)\ar{\omega}$ for some $\omega\inp\Omega$.
Here \plat{$\Psi^{(s,\alpha)}_{k+1}\in\dist{S\mathop\times\{k\mathord+1\}}$} is given by
\plat{$\Psi^{(s,\alpha)}_{k+1}(t,k\mathord+1)=\Psi^{(s,\alpha)}(t)$} for all $t\inp S$.
The resolving function $f$ is extended by $f(s,k):=s$.
Using Definition~\ref{def:resolution} it follows that $\langle R', \Lambda, \rightarrow'_R
\rangle$ is a resolution of $\Phi$ and, again by (\ref{eq:functional}),
$\Exp{\Lambda}(\ResultsN_{\langle R', {\rm\Omega}, \rightarrow'_R \rangle})
=\Exp{\Lambda}(\ResultsN_{\langle R, {\rm\Omega}, \rightarrow_R \rangle})$.
\end{proof}

\noindent
The rest of this section is devoted to showing that 
$\cV([\Phi])=\RPApply(\Phi)$ for any composition $\Phi=\Theta \parT \Delta$ of a test $\Theta$
and process $\Delta$; this amounts to showing 
\[\sset{\Rfun\Phi' \mid \Phi\darE{}\Phi'} = 
\setof{\Exp{\Lambda}(\ResultsN_{\langle R, {\rm\Omega}, \rightarrow \rangle})}
{\langle R, \Lambda, \rightarrow \rangle \mbox{ is a resolution of }
\Phi}\]
for any distribution $\Phi$ in an $\omega$-respecting pLTS $\langle S, {\rm\Omega}, \rightarrow \rangle$.

Let us see how an extreme derivation can be viewed as a method for dynamically generating
a resolution.
\begin{proposition} {\bf [Resolutions from extreme derivatives]}\label{prop:reso.der.1}
Let $\Phi\darE{}\Phi'$ in a pLTS $\langle
S,\Omega,\rightarrow \rangle$. Then there is a resolution
$\langle R,\Lambda,\rightarrow_R\rangle$ of $\Phi$, with resolving
function $f$, such that $\Lambda\darE{}_R \Lambda'$ for some $\Lambda'$
for which $\Phi' = \Imgf{\Lambda'}$.
\end{proposition}
\begin{proof}
Consider an extreme derivation of $\Phi \darE{} \Phi'$ as given
in Definition~\ref{def:d0839} where all $\Phi_k^{\Stop}$ must be stable:
$$\textstyle\Phi=\Phi_0, \qquad \Phi_k=\Phi_k^\Stop+\Phi_k^{\rightarrow}, \qquad
\Phi_k^{\rightarrow} \ar{\tau}\Phi_{k+1}, \qquad
\Phi'=\sum_{k=0}^\infty\Phi_k^\Stop.$$
By Lemma~\ref{lem:l1415}, $\Phi_k^{\rightarrow}\ar{\tau}\Phi_{k+1}$ implies
that there are states $s_{ik}\inp S$ and
distributions $\Phi_{i(k+1)}\inp\dist{S}$, such that
\\
\mbox{}
\hfill\hfill
$\Phi_k^{\rightarrow} = \sum_{i\in I_k} p_{ik} \Times \pdist{s_{ik}}$,
\hfill
$s_{ik} \ar{\tau} \Phi_{i(k+1)}$~~for each $i\in I_k$
\hfill
and
\hfill
$\Phi_{k+1} = \sum_{i \in I_k} p_{ik} \Times \Phi_{i(k+1)}$~.
\hfill\hfill
\mbox{}
\\[2ex]
Let $\Phi_{ik}^\Stop(s):=\left\{\begin{array}{@{}l@{~~\mbox{if}~}l@{}}
\Phi_{ik}(s)   & s \nar{\tau} \\
0   & s \ar{\tau}
\end{array}\right.$.
Since $\Phi_{k}^\Stop(s)=\left\{\begin{array}{@{}l@{~~\mbox{if}~}l@{}}
\Phi_{k}(s)   & s \nar{\tau} \\
0   & s \ar{\tau}
\end{array}\right.$
it follows that $\Phi_{k+1}^\Stop = \sum_{i \in I_k} p_{ik} \Times \Phi_{i(k+1)}^\Stop$.

We will now define the resolution
$\langle R,  \Lambda,\rightarrow_R \rangle$ and the resolving function $f$.
The set of states $R$ is $(S \mathord\times \Nat) \cup \bigcup_{k\in \Nat}(I_k \times \{k\})$.
The resolving function $f:R\rightarrow S$ maps $(s,k)\inp
S\mathord\times\Nat$ to $s$ and $(i,k)\inp I_k\mathord\times\{k\}$ to $s_{ik}\inp S$.
The second component $k$ of a state counts how many transitions have
fired already: each transition in $\rightarrow_R$ goes from a state $(i,k)$
or $(s,k)$ to a distribution over $(S\cup I_{k+1})\times\{k\mathord+1\}$.

Define the subdistributions $\Lambda_k^\Stop \inp\subdist{S\mathord\times\{k\}}$ and
$\Lambda_k^{\rightarrow}\inp\subdist{I_k\times\{k\}}$ by
$\Lambda_k^\Stop(s,k)=\Phi_k^\Stop(s)$
and
$\Lambda_k^{\rightarrow}(i,k)=p_{ik}$.
Let $\Lambda_k := \Lambda_k^\Stop + \Lambda_k^{\rightarrow}$ and $\Lambda := \Lambda_0$.
Furthermore, for all $k>0$ and $i\inp I_{k-1}$, define
$\Lambda_{ik} \inp\subdist{(S\cup I_k)\mathord\times\{k\}}$ by\\[1ex]
\mbox{}\hfill\hfill
$\Lambda_{ik}(s,k)=\Phi_{ik}^\Stop(s)$
\hfill
and
\hfill
$\displaystyle\Lambda_{ik}(j,k)=p_{jk}\Times\frac{\Phi_{ik}(s_{jk})}{\Phi_{k}(s_{jk})}$
\hfill
\hfill
\mbox{}\\[1ex]
for $j\inp I_k$.
We introduce the transitions $(i,k)\ar{\tau}_R\Lambda_{i(k+1)}$ for
$k\geq 0$ and $i\inp I_k$.
Moreover, for each state $s\inp S$ and label $\alpha\inp\Act_\tau$ such that
$s\ar{\alpha}$, pick a transition $s\ar{\alpha}\Psi$, and add the
transition $(s,k)\ar{\alpha}_R \Psi_{k+1}$ to $\rightarrow_R$, for
all $k\inp\Nat$. Here $\Psi_{k+1}$ is the distribution with
$\Psi_{k+1}(t,k\mathord+1)=\Psi(t)$ for all $t\inp S$.
Likewise, for each $k\in\Nat$, $i\inp I_k$ and $\omega\inp\Omega$ such
that $s_{ik}\ar{\omega}$, pick a transition $s_{ik}\ar{\omega}\Psi$, and add the
transition $(i,k)\ar{\omega}_R \Psi_{k+1}$ to $\rightarrow_R$.
This ends the definition of the resolution 
$\langle R,  \Lambda,\rightarrow_R \rangle$ and the resolving function $f$.
By construction, $\langle R, \Omega,\rightarrow_R \rangle$ is a
deterministic pLTS\@. We now check that $f$ satisfies the requirements
for a resolving function of Definition~\ref{def:resolution}.
\begin{enumerate}[(i)]
\item \mbox{}\hfill$\displaystyle\Imgf{\Lambda_k}(s)
= \Lambda_k(s,k)+\sum_{s_{ik}=s}\Lambda_k(i,k)
= \Lambda^\Stop_k(s,k)+\sum_{s_{ik}=s}p_{ik}
= \Phi^\Stop_k(s)+\Phi^{\rightarrow}_k(s)
= \Phi_k(s)$\hfill\mbox{}\\for all $s\inp S$, so $\Imgf{\Lambda_k}=\Phi_k$,
and in particular $\Imgf{\Lambda}=\Phi$.
\vspace{-1ex}
\item Let $r\ar{\alpha}_R\Gamma$ for $\alpha\inp\Omega_\tau$.
In case $r\mathbin=(s,k)$ it must be that $\Gamma=\Psi_{k+1}$ and
$f(r) = s \ar{\alpha} \Psi = \Imgf{\Psi_{k+1}}$.
Likewise, in case $r\mathbin=(i,k)$ and $\alpha\inp\Omega$ it must be that $\Gamma=\Psi_{k+1}$ and
$f(r) = s_{ik} \ar{\alpha} \Psi = \Imgf{\Psi_{k+1}}$.
The remaining case is $r\mathbin=(i,k)$, $\alpha=\tau$ and $\Gamma=\Lambda_{i(k+1)}$.
Then $f(r)=s_{ik}\ar{\tau}\Phi_{i(k+1)}$, so it suffices to show
that $\Imgf{\Lambda_{ik}}=\Phi_{ik}$ for all $k\inp\Nat$ and $i\inp I_k$. For any $s\inp S$ we have
$$\Imgf{\Lambda_{ik}}(s) = \Lambda_{ik}(s,k)+\sum_{s_{jk}=s}\Lambda_{ik}(j,k)
= \Phi_{ik}^\Stop(s)+\sum_{s_{jk}=s} p_{jk}\Times\frac{\Phi_{ik}(s_{jk})}{\Phi_{k}(s_{jk})}
= \Phi_{ik}^\Stop(s)+\frac{\Phi_{ik}(s)}{\Phi_{k}(s)}\Times\sum_{s_{jk}=s} p_{jk}\;.
$$
In case $s\nar{\tau}$ we have $s_{jk}=s$ for no $j\inp I_k$, so
$\Imgf{\Lambda_{ik}}(s)=\Phi_{ik}^\Stop(s)=\Phi_{ik}(s)$.
\\
In case $s\ar{\tau}$ we have $\Phi_{ik}^\Stop(s)=0$ and
$\sum_{s_{jk}=s} p_{jk}=\Phi^{\rightarrow}_{k}(s)=\Phi_k(s)$, so again 
$\Imgf{\Lambda_{ik}}(s)=\Phi_{ik}(s)$.
\vspace{-1ex}
\item Let $f(r)\ar{\alpha}$ for $\alpha\inp\Omega_\tau$.
By construction there is a $\Psi_{k+1}$ such that $r\ar{\alpha}_R\Psi_{k+1}$.
\vspace{-1ex}
\end{enumerate}
Hence $\langle R,  \Lambda,\rightarrow_R \rangle$ is a resolution of $\Phi$.
We have:
$$\sum_{i\in I_{k}}p_{ik}\Times\Lambda_{i(k+1)}(s,k\mathord+1)
=\sum_{i\in I_{k}}p_{ik}\Times \Phi_{i(k+1)}^\Stop(s)
=\Phi_{k+1}^\Stop(s)
=\Lambda_{k+1}^\Stop(s,k\mathord+1)
=\Lambda_{k+1}(s,k\mathord+1)$$
\vspace{-1em}
$$\sum_{i\in I_{k}}p_{ik}\Times\Lambda_{i(k+1)}(j,k\mathord+1)
=\sum_{i\in I_{k}}p_{ik}\Times p_{j(k+1)}\Times
  \frac{\Phi_{i(k+1)}(s_{j(k+1)})}{\Phi_{k+1}(s_{j(k+1)})}
=p_{j(k+1)}
=\Lambda_{k+1}^{\rightarrow}(j,k\mathord+1)
=\Lambda_{k+1}(j,k\mathord+1).$$
Hence $\Lambda_{k+1}=\sum_{i\in I_{k}}p_{ik}\Times\Lambda_{i(k+1)}$.
Since also $\Lambda_k^{\rightarrow} = \sum_{i\in I_k} p_{ik} \Times \pdist{(i,k)}$
and
$(i,k) \ar{\tau}_R \Lambda_{i(k+1)}$, Lemma~\ref{lem:l1415} yields
$\Lambda_k^{\rightarrow} \ar{\tau}_R \Lambda_{k+1}$.
Let $\Lambda'=\sum_{k=0}^\infty\Lambda_k^\Stop$.
Then, by Definition~\ref{def:d0839}, $\Lambda \darE{}_R \Lambda'$.

By construction $\Imgf{\Lambda^\Stop_k}=\Phi_k^\Stop$ for all $k\inp \Nat$.
Hence $\Imgf{\Lambda'} = \sum_{k=0}^\infty \Imgf{\Lambda^\Stop_k}
= \sum_{k=0}^\infty \Phi_k^\Stop = \Phi'$.
\end{proof}

\noindent
The converse is somewhat simpler.
\begin{proposition} {\bf [Extreme derivatives from resolutions]}\label{prop:reso.der.2}
Let $\langle R,\Lambda,\rightarrow_R\rangle$ be a resolution of a
subdistribution $\Phi$ in a pLTS
$\langle S,\Omega,\rightarrow \rangle$ with resolving function
$f$. Then $\Lambda\darE{}_R\Lambda'$ implies $\Phi \darE{}
\Imgf{\Lambda'}$.
\end{proposition}
\begin{proof}
The definition of $\textrm{Img}_f$ implies that
$\Imgf{\sum_ip_i\cdot\Psi_i}=\sum_ip_i\cdot\Imgf{\Psi_i}$.
Furthermore
$\Psi\ar{\tau}\Psi'$ implies $\Imgf{\Psi}\ar{\tau}\Imgf{\Psi'}$.
Namely, by Lemma~\ref{lem:l1415}, $\Psi\ar{\tau}\Psi'$ implies
\\[2ex]
\mbox{}
\hfill\hfill
$\Psi = \sum_{i\in I} p_i \Times \pdist{s_i}$,
\hfill
$s_i \ar{\tau} \Psi_i$~~for each $i\in I$
\hfill
and
\hfill
$\Psi' = \sum_{i \in I} p_i \Times \Psi_i$
\hfill\hfill
\mbox{}
\\[2ex]
which, using Definition~\ref{def:resolution}, entails
\\[2ex]
\mbox{}
\hfill\hfill
$\Imgf{\Psi} = \sum_{i\in I} p_i \Times \pdist{f(s_i)}$,
\hfill
$f(s_i) \ar{\tau} \Imgf{\Psi_i}$~~for each $i\in I$
\hfill
and
\hfill
$\Imgf{\Psi'} = \sum_{i \in I} p_i \Times \Imgf{\Psi_i}$.
\hfill\hfill
\mbox{}
\\[2ex]
Hence $\Imgf{\Psi}\ar{\tau}\Imgf{\Psi'}$.

Now consider any derivation of $\Lambda\darE{}_R\Lambda'$ along the lines
of Definition~\ref{def:d0839}. By systematically applying the
function $f$ to the component subdistributions in this derivation we
get a derivation $\Imgf{\Lambda} \dar{} \Imgf{\Lambda'}$, that is
$\Phi \dar{} \Imgf{\Lambda'}$. To show that $\Imgf{\Lambda'}$ is
actually an extreme derivative it suffices to show that $s$ is
stable for every $s \in \support{\Imgf{\Lambda'}}$. But if $s \in
\support{\Imgf{\Lambda'}}$ then by definition there is some $t \in
\support{\Lambda'}$ such that $ s = f(t)$. Since
$\Lambda\darE{}_R\Lambda'$ the state $t$ must be stable. The stability
of $s$ now follows from requirement (iii) of
Definition~\ref{def:resolution}.
\end{proof}

Our next step is to relate the outcomes extracted from extreme
derivatives to those extracted from the corresponding resolutions.
 This requires some analysis of the evaluation function
$\VV$ applied to $\omega$-respecting
deterministic pLTSs. We show that the function ${\cal F}$ defined in (\ref{eq:functional}) on Page~\pageref{page:resolutions} and its least fixed point $\VV$ are continuous with respect to  the standard Euclidean metric.

\begin{definition} {\bf [Continuous functions]}
An $\omega$-chain in a complete lattice $L$ is a sequence of elements $\setof{c_n}{n \geq 0}$
satisfying $c_i \leq c_{i+1}$. Since the lattice is complete, $\omega$-chains have least upper bounds;
we denote them by
\begin{math}
  \bigsqcup_{n \geq 0} c_n.
\end{math}
A function $f: L \rightarrow L$ is said to be ($\omega$)-continuous \cite{Win93} if it preserves the least upper bounds of
$\omega$-chains:
\begin{equation*}
  f( \bigsqcup_{n \geq 0} \; c_n) = \bigsqcup_{n  \geq 0} \;f(c_n)\;.
\end{equation*}
\end{definition}

\begin{lemma} {\bf [Exchange of suprema]}\label{l:exchange}
Let function $g:\Nat\times\Nat\rightarrow\Real$ be such that it is
\begin{enumerate}[(i)]
\item\label{i0847} monotonic in both of its arguments separately, so that $i \leq i'$ implies
  $g(i,j) \leq g(i',j)$ for all $j$, and $j \leq j'$ implies $g(i,j) \leq g(i,j')$ for all
  $i$, and
\item\label{i0848} bounded above, so that there is a $c\in\Real_{\geq 0}$ with $g(i,j)\leq c$ for all $i,j$.
\end{enumerate}
Then \[
\lim_{i\rightarrow\infty}\lim_{j\rightarrow\infty} g(i,j)~~=~~\lim_{j\rightarrow\infty}\lim_{i\rightarrow\infty} g(i,j).\] 
\end{lemma}
\begin{proof}
Conditions (i) and (ii) guarantee the existence of all the limits. Moreover, for a
non-decreasing sequence its limit and supremum agree, and both sides equal the supremum of
all $g(i,j)$ for $i,j\in \Nat$.
In fact, $(\Real,\leq)$ is a complete partial order (CPO), and 
it is a basic result of CPOs \cite{Win93} that\\[2ex]\mbox{}\hfill
$\displaystyle
\bigsqcup_{i\in\Nat}(\bigsqcup_{j\in\Nat} g(i,j)) ~~=~~ \bigsqcup_{j\in\Nat}(\bigsqcup_{i\in\Nat} g(i,j)).$
\end{proof}

\noindent
The following technical proposition states that some real functions satisfy the property of \emph{bounded continuity}, which allows the exchange of limit and sum operations. It plays a crucial role in proving the continuity of ${\cal F}$.

\begin{proposition} {\bf [Bounded continuity]} \label{p:continuity.positive}
Given a function $f:\Nat\times\Nat\rightarrow\Real_{\geq 0}$ which 
satisfies the following conditions:
\begin{enumerate}
\item[\textbf{C1.}] $f$ is monotonic in the second parameter, i.e.\ $j_1\leq j_2$ implies $f(i,j_1)\leq f(i,j_2)$ for all $i,j_1,j_2\in\Nat$;
\item[\textbf{C2.}] for any $i\in\Nat$, the limit $\lim_{j\rightarrow\infty}f(i,j)$ exists;
\item[\textbf{C3.}] the partial sums $S_n=\sum_{i=0}^n\lim_{j\rightarrow\infty} f(i,j)$ are bounded, i.e.\ there exists some $c\in\Real_{\geq 0}$ such that $S_n\leq c$ for all $n\geq 0$;
\end{enumerate}
then it holds that
\[\sum_{i=0}^\infty\lim_{j\rightarrow\infty}f(i,j) ~=~ \lim_{j\rightarrow\infty}\sum_{i=0}^\infty f(i,j).\]
\end{proposition}
\begin{proof}
Let $g:\Nat\times\Nat\rightarrow\Real_{\geq 0}$ be the function defined by $g(n,j) =
\sum_{i=0}^nf(i,j)$. It is easy to see that $g$ is monotonic in both arguments. By
\textbf{C1} and \textbf{C2}, we have that $f(i,j)\leq\lim_{j\rightarrow\infty}f(i,j)$ for any $i,j\in\Nat$. So
for any $j,n\in\Nat$ we have that\vspace{-2ex}
\[g(n,j) = \sum_{i=0}^nf(i,j)~\leq~\sum_{i=0}^n \lim_{j\rightarrow\infty}f(i,j) ~\leq~ c\]
according to \textbf{C3}. In other words, $g$ is bounded above. Therefore we can apply Lemma~\ref{l:exchange} and obtain
\begin{equation}\label{eq:lim4}
\lim_{n\rightarrow\infty}\lim_{j\rightarrow\infty}\sum_{i=0}^nf(i,j) 
~~=~~ \lim_{j\rightarrow\infty}\lim_{n\rightarrow\infty}\sum_{i=0}^nf(i,j).
\end{equation}
For any $j\inp\Nat$, the sequence $\sset{g(n,j)}_{n\geq 0}$ is nondecreasing and
bounded, so its limit $\sum_{i=0}^\infty f(i,j)$ exists. That is,\vspace{-1ex}
\begin{equation}\label{eq:lim2}
\lim_{n\rightarrow\infty}\sum_{i=0}^nf(i,j) 
~~=~~ \sum_{i=0}^\infty f(i,j).
\end{equation}
In view of \textbf{C2}, we have that, for any given $n\inp\Nat$, the limit $\lim_{j\rightarrow\infty}\sum_{i=0}^n f(i,j)$ exists and
\begin{equation}\label{eq:commute}
\sum_{i=0}^n\lim_{j\rightarrow\infty}f(i,j) ~=~
\lim_{j\rightarrow\infty}\sum_{i=0}^n f(i,j).
\end{equation}
By \textbf{C3} the sequence $\sset{S_n}_{n\geq 0}$ is
bounded. Since it is also nondecreasing, it converges to
\plat{$\displaystyle\sum_{i=0}^\infty\lim_{j\rightarrow\infty} f(i,j)$}. That is,\vspace{-1ex}
\begin{equation}\label{eq:lim1}
\lim_{n\rightarrow\infty}\sum_{i=0}^n\lim_{j\rightarrow\infty} f(i,j) 
~~=~~ \sum_{i=0}^\infty\lim_{j\rightarrow\infty} f(i,j).
\end{equation}
Hence the left-hand side of the desired equality exists.
By combining (\ref{eq:lim4})-(\ref{eq:lim1}) we obtain the result that\vspace{3pt}
\plat{$\displaystyle\sum_{i=0}^\infty\lim_{j\rightarrow\infty}f(i,j) ~=~ \lim_{j\rightarrow\infty}\sum_{i=0}^\infty f(i,j)$}.
\vspace{12pt}
\end{proof}

\begin{lemma}\label{l:continuous expectation}
Let $R$ be a set and $h:R\rightarrow [0,1]^\Omega$.
Furthermore, let $\Delta_0 \leq \Delta_1 \leq \cdots$ be an $\omega$-chain of subdistributions over
$R$ --- here $\Delta \leq \Delta'$ iff $\Delta(r) \leq \Delta'(r)$ for all $r\in R$.
Then $\Exp{\bigsqcup_{n\geq 0}\Delta_n}h = \bigsqcup_{n\geq 0}\Exp{\Delta_n}h$.
\end{lemma}
\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]
$\big(\Exp{\bigsqcup_{n\geq 0}\Delta_n}h \big) (\omega)
\begin{array}[t]{ll}
= \big(\sum_{r\in R}(\bigsqcup_{n\geq 0}\Delta_n)(r)\Times h(r) \big) (\omega) \\
= \big(\sum_{r\in R}(\bigsqcup_{n\geq 0}\Delta_n(r))\Times h(r) \big) (\omega) \\
= \big(\sum_{r\in R}\bigsqcup_{n\geq 0}(\Delta_n(r)\Times h(r)) \big) (\omega) \\
= \sum_{r\in R}\bigsqcup_{n\geq 0}(\Delta_n(r)\Times h(r)(\omega)) \\
= \sum_{r\in R}\lim_{n\rightarrow\infty}(\Delta_n(r)\Times h(r)(\omega)) \\
= \lim_{n\rightarrow\infty}\sum_{r\in R}(\Delta_n(r)\Times h(r)(\omega))
  & \mbox{by Proposition~\ref{p:continuity.positive}}\\
= \bigsqcup_{n\geq 0}\sum_{r\in R}(\Delta_n(r)\Times h(r) (\omega)) \\
= \big(\bigsqcup_{n\geq 0}\sum_{r\in R}(\Delta_n(r)\Times h(r))\big) (\omega) \\
= \big(\bigsqcup_{n\geq 0}\Exp{\Delta_n}h \big) (\omega).
\end{array}$\\[1ex]
 In the above reasoning, Proposition~\ref{p:continuity.positive} can
be applied because we can define $f:R\times\Nat\rightarrow\Real_{\geq 0}$ by letting
$f(r,n)=\Delta_n(r)\cdot h(r)(\omega)$ and checking that $f$ satisfies
the three conditions in Proposition~\ref{p:continuity.positive}. If
$R$ is finite, we can extend it to a countable set $R'\supseteq R$
and require $f(r',n)=0$ for all $r'\in R'\backslash R$ and
$n\in\Nat$.
\begin{enumerate}
\item $f$ satisfies condition \textbf{C1}. For any $r\in R$ and
$j_1,j_2\in\Nat$, if $j_1\leq j_2$ then $\Delta_{j_1}\leq \Delta_{j_2}$. It
follows that\vspace{-1ex}
\[f(r,j_1)~=~\Delta_{j_1}(r)\cdot h(r)(\omega)~\leq~ \Delta_{j_2}(r)\cdot h(r)(\omega) ~=~ f(r,j_2).\vspace{-1ex}\]

\item $f$ satisfies condition \textbf{C2}. For any $r\in R$, the
sequence $\sset{\Delta_n(r)\cdot h(r)(\omega)}_{n\geq 0}$ is
nondecreasing and bounded by $h(r)(\omega)$. It follows that the limit
$\lim_{n\rightarrow\infty}f(r,n)$ exists.

\item $f$ satisfies condition \textbf{C3}. For any finite $R''\subseteq R$,
the partial sum $\sum_{r\in R''}\lim_{n\rightarrow\infty}f(r,n)$ is
bounded because\\[1ex]\mbox{}\hfill
$\begin{array}[b]{clclcl}
       & \sum_{r\in R''}\lim_{n\rightarrow\infty}f(r,n)
       &=& \lim_{n\rightarrow\infty}\sum_{r\in R''}f(r,n)

       &=& \lim_{n\rightarrow\infty}\sum_{r\in R''}\Delta_n(r)\cdot h(r)(\omega)\\
  \leq &      \lim_{n\rightarrow\infty}\sum_{r\in R''}\Delta_n(r)
       &\leq& \lim_{n\rightarrow\infty}\sum_{r\in R}\Delta_n(r)
       &\leq& \lim_{n\rightarrow\infty}1 =  1.
 \end{array}$
\hfill$\Box$\vspace{2ex}
\end{enumerate}
\end{trivlist}

\begin{lemma}\label{lem:continuity}
Consider a deterministic pLTS $\langle R, {\rm\Omega}, \rightarrow \rangle$. The function $\cF$ defined in (\ref{eq:functional}) is  continuous.
\end{lemma}
\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]
Let $f_0 \leq f_1\leq ...$ be an increasing chain in
$R\rightarrow[0,1]^\Omega$. We need to show that
\begin{equation}\label{e:limit}
\cF(\bigsqcup_{n\geq 0}f_n)~=~\bigsqcup_{n\geq 0}\cF(f_n)
\end{equation}
For any $r\in R$, we are in one of the following three cases:
\begin{enumerate}
\item $r\ar{\omega}$ for some $\omega\in\Omega$. We have
 \[\begin{array}{rcll}
 \cF(\bigsqcup_{n\geq 0}f_n)(r)(\omega) & = & 1 & \mbox{by (\ref{eq:functional})}\\
                           & = & \bigsqcup_{n\geq 0} 1 & \\
                           & = & \bigsqcup_{n\geq 0}\cF(f_n)(r)(\omega) & \\
                           & = & (\bigsqcup_{n\geq 0}\cF(f_n))(r)(\omega) &
 \end{array}\]
 and \[\cF(\bigsqcup_{n\geq 0}f_n)(r)(\omega') = 0 = (\bigsqcup_{n\geq
   0}\cF(f_n))(r)(\omega')\vspace{-1ex}\] for all $\omega'\not=\omega$.
\item $r\not\!\rightarrow$. Similar to the last case. We have
 \[\cF(\bigsqcup_{n\geq 0}f_n)(r)(\omega) = 0 = (\bigsqcup_{n\geq
   0}\cF(f_n))(r)(\omega)\vspace{-1ex}\] for all $\omega\in\Omega$.
\item Otherwise, $r\ar{\tau}\Delta$ for some $\Delta\in\dist{R}$. Then we infer
that,  for any $\omega\in \Omega$,
  \[\begin{array}{rcll}
 \cF(\bigsqcup_{n\geq 0}f_n)(r)(\omega) & =
 & \Exp{\Delta}(\bigsqcup_{n\geq 0}f_n)(\omega) & \mbox{by (\ref{eq:functional})}\\
 & = & \sum_{r\in\support{\Delta}}\Delta(r)\cdot (\bigsqcup_{n\geq
 0}f_n)(r)(\omega)& \\
& = & \sum_{r\in\support{\Delta}}\Delta(r)\cdot (\bigsqcup_{n\geq
 0}f_n(r))(\omega)& \\
& = & \sum_{r\in\support{\Delta}} \bigsqcup_{n\geq
 0}\Delta(r)\cdot f_n(r)(\omega)& \\
 & = & \sum_{r\in\support{\Delta}} \lim_{n\rightarrow\infty}\Delta(r)\cdot f_n(r)(\omega)& \\
 & = & \lim_{n\rightarrow\infty}\sum_{r\in\support{\Delta}} \Delta(r)\cdot f_n(r)(\omega)& \mbox{by Proposition~\ref{p:continuity.positive}}\\
& = & \bigsqcup_{n\geq 0}\sum_{r\in\support{\Delta}}\Delta(r)\cdot
 f_n(r)(\omega) & \\
& = & \bigsqcup_{n\geq 0}\Exp{\Delta}(f_n)(\omega) & \\
& = & \bigsqcup_{n\geq 0}\cF(f_n)(r)(\omega) &\\
& = & (\bigsqcup_{n\geq 0}\cF(f_n))(r)(\omega)\;. &
 \end{array}\]
 In the above reasoning, Proposition~\ref{p:continuity.positive} can
be applied because we can define the function
$f:R\times\Nat\rightarrow\Real_{\geq 0}$ by letting
$f(r,n)=\Delta(r)\cdot f_n(r)(\omega)$ and checking that $f$ satisfies
the three conditions in Proposition~\ref{p:continuity.positive}. If
$R$ is finite, we can extend it to a countable set $R'\supseteq R$
and require $f(r',n)=0$ for all $r'\in R'\backslash R$ and
$n\in\Nat$.
\begin{enumerate}
\item $f$ satisfies condition \textbf{C1}. For any $r\in R$ and
$j_1,j_2\in\Nat$, if $j_1\leq j_2$ then $f_{j_1}\leq f_{j_2}$. It
follows that\vspace{-1ex}
\[f(r,j_1)~=~\Delta(r)\cdot f_{j_1}(r)(\omega)~\leq~ \Delta(r)\cdot f_{j_2}(r)(\omega) ~=~ f(r,j_2).\]

\item $f$ satisfies condition \textbf{C2}. For any $r\in R$, the
sequence $\sset{\Delta(r)\cdot f_n(r)(\omega)}_{n\geq 0}$ is
nondecreasing and bounded by $\Delta(r)$. It follows that the limit
$\lim_{n\rightarrow\infty}f(r,n)$ exists.

\item $f$ satisfies condition \textbf{C3}. For any $R''\subseteq R$,
the partial sum $\sum_{r\in R''}\lim_{n\rightarrow\infty}f(r,n)$ is
bounded because\\\mbox{}\hfill
$\displaystyle\sum_{r\in R''}\lim_{n\rightarrow\infty}f(r,n) =
\sum_{r\in R''}\lim_{n\rightarrow\infty}\Delta(r)\cdot f_n(r)(\omega) \leq
\sum_{r\in R''}\Delta(r) \leq \sum_{r\in R}\Delta(r) = 1.$\hfill$\Box$
\end{enumerate}
\end{enumerate}
\vspace{1ex}
\end{trivlist}

\noindent
The continuity of $\cF$ implies that its fixed point $\VV$ can be captured by a
chain of approximants. The functions $\VV^n,\; n \geq 0$ are defined by induction on $n$:
\begin{align*}
  \VV^0 (r)(\omega) &= 0 \qquad\mbox{for all $r\in R$ and $\omega\in\Omega$}\\
  \VV^{n+1} &=  {\cal F}( \,\VV^{n}\, )
\end{align*}
Now
\begin{math}
  \VV = \bigsqcup_{n \geq 0} \;\; \VV^n.
\end{math}
This is used in the following result.

\begin{lemma}\label{lem:v.der}
Let $\Lambda$ be a subdistribution in an $\omega$-respecting deterministic pLTS $\langle R, \Omega, \rightarrow_R \rangle$.
If $\Lambda\darE{}\Lambda'$ then
$\Exp{\Lambda}(\VV_{\langle R, \Omega, \rightarrow_R \rangle})=
\Exp{\Lambda'}(\VV_{\langle R, \Omega, \rightarrow_R \rangle})$.
\begin{proof}
For simplicity let us write $\VV(\Delta)$ for $\Exp{\Delta}(\VV_{\langle R, \Omega, \rightarrow_R \rangle})$ for any $\Delta$.
Since the pLTS is $\omega$-respecting we know that $s \ar{\tau} \Delta$ implies $s \nar{\omega}$
for any $\omega$. Therefore, from the definition of the \hyperref[eq:functional]{functional ${\cal F}$}
we have that
  $s\ar{\tau}\Delta$ implies $\VV^{n+1}(s)=\VV^n(\Delta)$,  whence by
  lifting and linearity we get:
\begin{equation*}\label{eq:1step}
\textrm{if $\Delta\ar{\tau}\Delta'$ then
$\VV^{n+1}(\Delta)=\VV^n(\Delta')$ for all $n\geq 0$.}
\end{equation*}
Now suppose $\Lambda\darE{}\Lambda'$. Then\vspace{-1ex}
$$\Lambda=\Lambda_0, \qquad \Lambda_k=\Lambda_k^\Stop+\Lambda_k^{\rightarrow}, \qquad
\Lambda_k^{\rightarrow} \ar{\tau}\Lambda_{k+1}, \qquad
\Lambda'=\sum_{k=0}^\infty\Lambda_k^\Stop.$$
Using in the base case that $\ResultsN^0(\Delta)(\omega) \mathbin= 0$ for each $\Delta$,
a straightforward induction on $n$ yields, for all $\ell\mathbin\geq 0$\vspace{-1ex},
\begin{equation}\label{eq:vnn}
  \VV^{n}(\Lambda_\ell)\Wide{=}
\sum_{k=0}^{n}\VV^{n-k}(\Lambda_{\ell+k}^\Stop)\;.\vspace{-1ex}
\end{equation}
Namely $\VV^{n+1}(\Lambda_\ell)
= \VV^{n+1}(\Lambda_\ell^\Stop+\Lambda_\ell^{\rightarrow})
= \VV^{n+1}(\Lambda_\ell^\Stop)+\VV^{n+1}(\Lambda_\ell^{\rightarrow})
= \VV^{n+1}(\Lambda_\ell^\Stop)+\VV^{n}(\Lambda_{\ell+1})
\stackrel{\rm induction}=\\ \VV^{n+1}(\Lambda_\ell^\Stop)
  + \sum_{k=0}^{n}\VV^{n-k}(\Lambda_{\ell+1+k}^\Stop)
= \VV^{n+1}(\Lambda_\ell^\Stop)
  + \sum_{k=1}^{n+1}\VV^{n+1-k}(\Lambda_{\ell+k}^\Stop)
= \sum_{k=0}^{n+1}\VV^{n+1-k}(\Lambda_{\ell+k}^\Stop)$.

Since $\Lambda_k^\Stop$ is stable, we have 
\begin{equation}\label{eq:vvn}
\ResultsN^{m} (\Lambda_k^\Stop) =
\ResultsN(\Lambda_k^\Stop) \qquad\mbox{for every $k,m \geq 0$.}
\end{equation}
We conclude by reasoning\\[2ex]
\mbox{}\hfill$\begin{array}[b]{rll}
 \VV(\Lambda) &=   \bigsqcup_{n\geq 0} \VV^{n}(\Lambda) &\qquad \text{by continuity of $\cal F$  }\\
              &=    \bigsqcup_{n\geq 0}
 \sum_{k=0}^n\VV^{n-k}(\Lambda_k^\Stop) &\qquad \text{from
   (\ref{eq:vnn}) above, taking $\ell=0$ }\\
              &=    \bigsqcup_{n\geq 0} \sum_{k=0}^n\VV(\Lambda_k^\Stop) &\qquad \text{by (\ref{eq:vvn})  }\\
              &=    \bigsqcup_{n\geq 0} \VV (\sum_{k=0}^n \Lambda_k^\Stop) &\qquad \text{by linearity of  $\VV$  }\\
              &=   \VV (  \bigsqcup_{n\geq 0} \sum_{k=0}^n \Lambda_k^\Stop  ) &\qquad \text{by Lemma~\ref{l:continuous expectation}}\\
              &=  \VV (  \sum_{k=0}^\infty \Lambda_k^\Stop  ) \\
              &=   \VV (\Lambda')\;.
\end{array}$
\end{proof}
\end{lemma}

\noindent
We are now ready to compare the two methods for calculating the set of outcomes associated with a subdistribution:
\begin{itemize}
\vspace{-1ex}
\item using extreme derivatives and the reward function $\Rfun$ from
Definition~\ref{def:immediate reward}
\vspace{-1ex}
\item using resolutions and the evaluation function $\VV$ from page~\pageref{page:resolutions}.
\end{itemize}

\begin{theorem}\label{thm:der.reso}
In an $\omega$-respecting pLTS $\langle
S,\Omega,\rightarrow\rangle$, the following statements hold.
\begin{enumerate}[(a)]
\item If $\Phi\darE{}\Phi'$ then there is a
resolution $\langle R, \Lambda, \rightarrow_R \rangle$ of $\Phi$
such that $\Exp{\Lambda}(\VV_{\langle R, \Omega, \rightarrow_R \rangle})=\Rfun \Phi'$.

\item For any resolution $\langle R, \Lambda, \rightarrow_R \rangle$ of $\Phi$,
 there exists a $\Phi'$ such that $\Phi\darE{}\Phi'$ and
 $\Exp{\Lambda}(\VV_{\langle R, \Omega, \rightarrow_R \rangle})=\Rfun \Phi'$.
\end{enumerate}
\begin{proof}
Suppose $\Phi\darE{}\Phi'$. By Proposition~\ref{prop:reso.der.1},
there is a resolution $\langle R,\Lambda,\rightarrow_R\rangle$ of
$\Phi$ with resolving function $f$ and a subdistribution $\Lambda'$
such that $\Lambda\darE{}\Lambda'$ and $\Phi' = \Imgf{\Lambda'}$. By
Lemma~\ref{lem:v.der}, we have\vspace{-1ex}
\begin{equation}\label{eq:l1}
\Exp{\Lambda}(\VV)=\Exp{\Lambda'}(\VV).\vspace{-1ex}
\end{equation}
Since $\Lambda'$ is an extreme derivative, all the
states $s$ in its support are stable, so $\VV(s)(\omega)=0$ if $s\nar{\omega}$,
for all $\omega\inp\Omega$. Hence
\begin{equation}\label{eq:l2}
\Exp{\Lambda'}(\VV)(\omega)
= \sum_{s\in\support{\Lambda'}}\Lambda'(s)\cdot\VV(s)(\omega)
= \!\!\!\!\sum_{s\in\support{\Lambda'},~s\ar{\omega}}\!\!\!\!\Lambda'(s)
= \$\Lambda'(\omega)\;.
\end{equation}
Furthermore, for all $t\inp\support{\Phi'}$, $\Phi'(t) =\Imgf{\Lambda'}(t) =
\sum_{f(s)=t}\Lambda'(s)$, so, for all $\omega\in\Omega$,
$$\$\Phi'(\omega)
= \!\!\!\!\sum_{t\in\support{\Phi'},~t\ar{\omega}}\!\!\!\! \Phi'(t)
= \!\!\!\!\sum_{t\in\support{\Phi'},~t\ar{\omega}}\!\!\!\! \Imgf{\Lambda'}(t)
= \!\!\!\!\sum_{t\in\support{\Phi'},~t\ar{\omega}}\!\!\!\!
  {\textstyle \sum_{f(s)=t}\Lambda'(s)}
= \!\!\!\!\sum_{s\in\support{\Lambda'},~f(s)\ar{\omega}}\!\!\!\! \Lambda'(s)
= \$\Lambda'(\omega)\;,$$
where in the last step we the use the property of resolutions that
$f(s)\ar{\omega}$ iff $s\ar{\omega}$. Combining this with (\ref{eq:l1}) and (\ref{eq:l2}) yields that $\Exp{\Lambda}(\VV)=\Rfun\Phi'$.

To prove part (b), suppose that
$\langle R, \Lambda, \rightarrow_R \rangle$
 is a resolution of $\Phi$ with resolving function $f$, so that
$\Phi = \Imgf{\Lambda}$.
 We know from
Lemma~\ref{lem:unique.der} that there exists a (unique)
subdistribution $\Lambda'$ such that
 $\Lambda\darE{}\Lambda'$. By
Proposition~\ref{prop:reso.der.2} we have that $\Phi \darE{} \Imgf{\Lambda'}$.
The same arguments as in the other
direction show that $\Exp{\Lambda}(\VV)=  \Rfun (\Imgf{\Lambda'})$.
\end{proof}
\end{theorem}

\noindent
A direct consequence of the above theorem is that 
$\cV(\Phi) =\RApply(\Phi)$ for any subdistribution $\Phi$ in an $\omega$-respecting pLTS
$\langle S,\Omega,\rightarrow\rangle$. This implies that
$\cV([\Phi]) =\RPApply(\Phi)$ for any subdistribution $\Phi$ in a pLTS  $\langle
S,\Omega,\rightarrow\rangle$. This, in turn, together with Proposition~\ref{prop:rpa}, implies the following result.
\begin{corollary}\label{cor:der.reso}
For any subdistribution $\Phi$ in a pLTS $\langle S,\Omega,\rightarrow\rangle$ we have that
$\cV([\Phi])   =\RApply(\Phi)$.
\hfill $\Box$
\end{corollary}

\section{Agreement of nonnegative- and real-reward must testing}\label{sec:agree}
In this section we prove the agreement of $\nrMustleq$ with $\rrMustleq$ for 
finitary convergent processes, by using failure simulation \cite{concur}, recalled in
Definition~\ref{def:efailsimA},  as a stepping stone.

Because we prune our pLTSs before extracting values from them, we
will be concerned mainly with $\omega$-respecting
structures. Moreover, we require the pLTSs to be \emph{convergent} in
the sense that there is no wholly divergent state $s$, i.e.\ with $s\dar{}\eDis$. 
It follows from Theorem 8 in \cite{concur}, in combination with Lemma~\ref{finitary import}(iii),
that on a finitary convergent pLTS, if $\Delta\dar{}\Delta'$ with $\Delta$ a full distribution, then
$\Delta'$ is a full distribution.

\begin{lemma}\label{lem:stable}
Let $\Delta$ and $\Gamma$ be full distributions in an
$\omega$-respecting finitary convergent pLTS $\langle
S,\Omega,\rightarrow\rangle$. If distribution
$\Gamma$ is stable and $\Gamma\lift{\failsime}\Delta$, then
$\Rfun\Gamma\in\cV(\Delta)$.
\begin{proof}
We first show that if $s$ is stable and $s\failsime\Delta$ with $\Delta$ a full distribution, then
$\Rfun\pdist{s}\in\cV(\Delta)$. Since $s$ is stable, we have only two cases:
\begin{enumerate}[(i)]
\item $s\not\rightarrow$\qquad
Here $\Rfun\pdist{s}{=}\vec{0}$, where $\vec{0}(\omega)=0$ for all $\omega\in
\Omega$. Since $s\failsime\Delta$ we have
$\Delta\dar{}\Delta'$ with $\Delta'\not\rightarrow$, whence in fact
$\Delta\darE{}\Delta'$ and $\Rfun\Delta'=\vec{0}$. Thus
$\Rfun\pdist{s}=\vec{0}\in\cV(\Delta)$.

\item $s\ar{\omega}\Gamma'$ for some $\Gamma'$\qquad
Here $\Rfun\pdist{s}{=}\vec{\omega}$, and since $s\failsime\Delta$ we have $\Delta\dar{}\Delta'\ar{\omega}$.
As remarked above, also $\Delta'$ is a full distribution.
Hence $\Rfun\Delta'{=}\vec{\omega}$.
Because the pLTS is $\omega$-respecting, in fact
$\Delta\darE{}\Delta'$ and so again $\Rfun\pdist{s} = \vec{\omega}\in \cV(\Delta)$.
\end{enumerate}
Now for the general case we suppose $\Gamma\lift{\failsime}\Delta$.
By Lemma~\ref{lem:l1415} there is an index set $I$ and states $s_i$, subdistributions
$\Delta_i$ and probabilities $p_i$ for $i\in I$, with $\sum_{i\in I}p_i\leq 1$, such that
\\[2ex]
\mbox{}
\hfill\hfill
$\Gamma = \sum_{i\in I} p_i \Times \pdist{s_i}$,
\hfill
$s_i \failsime \Delta_i$~~for each $i\in I$
\hfill
and
\hfill
$\Delta = \sum_{i \in I} p_i \Times \Delta_i$.
\hfill\hfill
\mbox{}
\\[2ex]
Since $\Delta$ is full, $\sum_{i\in I}p_i=1$ and the $\Delta_i$ are full distributions.
Since $\Gamma$ is stable, each state $s_i$ is stable.
From above we have that $\Rfun\pdist{s_i}\in\cV(\Delta_i)$ for all $i\in I$, and so
$\Rfun\Gamma=\sum_{i\in I}p_i\Times\Rfun\pdist{s_i}\in
\sum_{i\in I}p_i\Times\cV(\Delta_i)=\cV(\Delta)$, using
Lemma~\ref{lem:linearity of outcomes}.
\end{proof}
\end{lemma}



\begin{lemma}\label{lem:failsim}
Let $\Delta$ and $\Gamma$ be full distributions in an
$\omega$-respecting finitary convergent pLTS $\langle
S,\Omega,\rightarrow\rangle$. Then
$\Delta\failsimpreo\Gamma$ implies
$\cV(\Delta)\supseteq\cV(\Gamma)$.
\begin{proof}
Let $\Gamma, \Delta\in\dist{S}$.
We first claim that
\begin{enumerate}[(i)]
\item  If $\Delta\dar{}\Delta'$ then $\cV(\Delta')\subseteq\cV(\Delta)$.
\item  If $\Gamma\lift{\failsime}\Delta$, then we have
$\cV(\Gamma)\subseteq\cV(\Delta)$.
\end{enumerate}
The first claim holds because if $\Delta'\darE{}\Delta''$ then
$\Delta\dar{}\Delta'\darE{}\Delta''$, i.e.\ every extreme
derivative of $\Delta'$ is also an extreme derivative of $\Delta$.
For the second claim, we assume  $\Gamma\lift{\failsime}\Delta$. For any $\Gamma\darE{}\Gamma'$
Lemma~\ref{lem:matching} gives a matching transition $\Delta\dar{}\Delta'$ such that
$\Gamma'\lift{\failsime}\Delta'$.
By definition $\Gamma'$ is stable and since $\langle S,\Omega,\rightarrow\rangle$ is finitary
and convergent $\Delta'$ and $\Gamma'$ must be full. It follows from
Lemma~\ref{lem:stable} and Claim (i) that
$\Rfun\Gamma'\in\cV(\Delta')\subseteq\cV(\Delta)$. Consequently, we
obtain $\cV(\Gamma)\subseteq\cV(\Delta)$.

Now suppose $\Delta\failsimpreo\Gamma$. By definition there exists some $\Delta'$ such that
$\Delta\dar{}\Delta'$ and $\Gamma\lift{\failsime}\Delta'$. By
the above two claims we obtain
$\cV(\Gamma)\subseteq\cV(\Delta')\subseteq\cV(\Delta)$.
\end{proof}
\end{lemma}

\noindent
This lemma shows that the failure-simulation preorder is a very strong
relation in the sense that if $\Delta$ is related to $\Gamma$ by
the failure-simulation preorder then the set of outcomes generated by
$\Delta$ includes the set of outcomes given by $\Gamma$. It is mainly
due to this strong property that we can show that the failure-simulation
preorder is sound for the real-reward must-testing preorder.
Convergence is a crucial condition in this lemma.

\begin{theorem}\label{thm:fs.rr}
For any finitary convergent processes $\Delta$ and $\Gamma$, if $\Delta\failsimpreo \Gamma$ then we have that $\Delta\rrMustleq \Gamma$.
\end{theorem}
\begin{proof}
We reason as follows.
\begin{Reason}
\Step{}{\Delta \failsimpreo \Gamma}
\StepR{\textrm{implies}}{
Lemma~\ref{lemma:pf}, for any $\Omega$-test $\Theta$}{[\Theta\parT \Delta] \failsimpreo [\Theta\parT \Gamma] }
\StepR{\textrm{implies}}{$[\Times]$ is $\omega$-respecting; Lemma~\ref{lem:failsim}}{
 \cV([\Theta\parT \Delta])\supseteq\cV([\Theta\parT \Gamma])
}
\StepR{\textrm{iff}}{Corollary~\ref{cor:der.reso}
}{
 \RApply(\Theta,\Delta)\supseteq\RApply(\Theta,\Gamma)
}
\StepR{\textrm{implies}}{}{h\cdot\RApply(\Theta,\Delta)\supseteq h\cdot\RApply(\Theta,\Gamma) \quad\mbox{ for any $h\in[-1,1]^\Omega$}}
\StepR{\textrm{implies}}{}{\bigsqcap h\cdot\RApply(\Theta,\Delta)\leq \bigsqcap h\cdot\RApply(\Theta,\Gamma) \quad\mbox{ for any $h\in[-1,1]^\Omega$}}
\StepR{\textrm{iff}}{}{\Delta\rrmMustleq \Gamma ~.}
\end{Reason}
Note that in the second line above, both $[\Theta\parT \Delta]$ and $[\Theta\parT \Gamma]$
are convergent, since for any convergent process $\Xi$ and finite process $\Theta$, by
induction on the structure of $\Theta$, it can be shown that the composition $\Theta\parT
\Xi$ is also convergent.
Furthermore, since processes $\Delta,\Gamma$ and tests $\Theta$ are defined to be full
distributions, also $[\Theta\parT \Delta]$ and $[\Theta\parT \Gamma]$ are full.
\end{proof}
\noindent
The proof of the above theorem is subtle. The failure-simulation preorder
is defined via weak derivations (cf.\ Definition~\ref{def:efailsimA}),
while the reward must-testing preorder is defined in terms of resolutions
(cf.\ Definition~\ref{def:d1509}). Fortunately, we have shown in
Corollary~\ref{cor:der.reso} that we can just as well characterise
the reward must-testing preorder in terms of weak derivations.
Based on this observation, the proof was carried out by exploiting
Lemmas~\ref{lemma:pf} and \ref{lem:failsim}.

This result does not extend to divergent processes. One witness example is given in Figure~\ref{fig:diverg}. 
A simpler example is as follows.     
Let $\Delta$ be a process that diverges, by
performing a $\tau$-loop only, and let $\Gamma$ be a process that merely
performs a single action $a$.
It holds that
$\Delta\failsimpreo \Gamma$ because $\Delta\dar{}{\eDis}$ and the empty
subdistribution can failure-simulate any processes. However, if we
apply the test $\pdist{t}$ from Example~\ref{ex:ex1B} again, and the
reward tuple $h$ with $h(\omega)=-1$, then
\[\begin{array}{l@{\Wide{=}}l@{\Wide{=}}l@{\Wide{=}}l@{\Wide{=}}r}
\bigsqcap h\cdot\RApply(\pdist{t},\Delta) & \bigsqcap h\cdot\cV([\pdist{t}\|\Delta]) &
 \bigsqcap h\cdot\sset{\Rfun{\eDis}} &\bigsqcap \sset{0} & 0\\
\bigsqcap h\cdot\RApply(\pdist{t},\Gamma) & \bigsqcap h\cdot\cV([\pdist{t}\|\Gamma]) &
 \bigsqcap h\cdot\sset{\vec{\omega}} &\bigsqcap \sset{-1} & -1
\end{array}\]
As $\bigsqcap h\cdot\RApply(\pdist{t},\Delta) \not\leq \bigsqcap h\cdot\RApply(\pdist{t},\Gamma)$, we see that $\Delta\not\rrMustleq \Gamma$.
Since $\cV([\pdist{t}\|\Gamma])= \{\vec{\omega}\}$ but
$\vec{\omega}\not\in\cV([\pdist{t}\|\Delta])$, this also is a
counterexample against an extension of Lemma~\ref{lem:failsim} with divergence.

Finally, by combining Theorems~\ref{thm:nr.pb}(ii) and
\ref{thm:sound.complete}(ii), together with Theorem~\ref{thm:fs.rr},
we  obtain the main result of the paper which states that, in the
absence of divergence, nonnegative-reward must testing is as discriminating as real-reward must testing.

\begin{theorem}\label{thm:rrm.nrm}
For any finitary convergent processes $\Delta$ and $\Gamma$,
it holds that $\Delta\rrMustleq \Gamma$ if and only if
$\Delta\nrMustleq \Gamma$.
\end{theorem}
\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]
The ``only if'' direction is obvious (cf.\ Definition~\ref{def:d1509}). For the
``if'' direction, suppose $\Delta$ and $\Gamma$ are finitary convergent
processes. We reason as follows. 
\begin{Reason}
\Step{}{\Delta \nrmMustleq \Gamma}
\StepR{\textrm{iff}}{Theorem~\ref{thm:nr.pb}(ii)}{\Delta \pmMustleq \Gamma}
\StepR{\textrm{iff}}{Theorem~\ref{thm:sound.complete}(ii)}{\Delta \failsimpreo \Gamma}
\StepR{\textrm{implies}}{Theorem~\ref{thm:fs.rr} $\;\Box$}{\Delta \rrmMustleq \Gamma~.}
\end{Reason}
\end{trivlist}

\section{Discussion}\label{sec:discussion}
Below we give a characterisation of $\rrMustleq$ in terms of the set
inclusion relation between testing outcome sets. As a similar
characterisation for $\nrMustleq$ does in general not hold for
finitary (non-convergent) processes, hopefully this gives some indication
of the subtle difference between $\rrMustleq$ and $\nrMustleq$, and we
see more clearly why our proof of Theorem~\ref{thm:rrm.nrm} involves
the failure simulation preorder.
\begin{theorem}\label{thm:nr.subset}
Let $\Delta$ and $\Gamma$ be any finitary processes. Then $\Delta\rrMustleq \Gamma$ if and only if $\RApply(\Theta,\Delta)\supseteq\RApply(\Theta,\Gamma)$ for any $\Omega$-test $\Theta$.
\end{theorem}
\begin{proof}
($\Leftarrow$) Let $\Theta$ be any $\Omega$-test and $h\in [-1,1]^\Omega$ be any real-reward tuple. Suppose 
$\RApply(\Theta,\Delta)\supseteq\RApply(\Theta,\Gamma)$.
It is obvious that
$h\cdot\RApply(\Theta,\Delta)\supseteq h\cdot\RApply(\Theta,\Gamma)$,
from which it easily follows that
\[\bigsqcap h\cdot\RApply(\Theta,\Delta) ~\leq~ \bigsqcap h\cdot\RApply(\Theta,\Gamma).\]
As this holds for an arbitrary real-reward tuple $h$, we see that $\Delta\rrMustleq \Gamma$.

($\Rightarrow$) Suppose for a contradiction that there is some $\Omega$-test $\Theta$ with
$\RApply(\Theta,\Delta)\not\supseteq\RApply(\Theta,\Gamma)$.
Then there exists some outcome $o\in \RApply(\Theta,\Gamma)$ lying outside $\RApply(\Theta,\Delta)$, i.e. 
\begin{equation}\label{eq:sep1}
o\not\in\RApply(\Theta,\Delta).
\end{equation}
Since $\Theta$ is finite, it contains only finitely many elements of $\Omega$, so that we may
  assume wlog that $\Omega$ is finite.
Since $\Delta$ and $\Theta$ are finitary, it is easy to see that the pruned composition $[\Delta \parT \Theta]$ is also finitary.
By Theorem~1/Corollary 1 in \cite{concur}, the set $\sset{\Phi\mid [\Delta \parT \Theta] \dar{}\Phi}$ is convex and compact. With an analogous proof, it can be shown that so is the set
$\sset{\Phi\mid [\Delta \parT \Theta] \darE{}\Phi}.$
 It follows that the set
\[\sset{\$\Phi\mid [\Delta \parT \Theta] \darE{}\Phi}\]
i.e.\ $\cV([\Theta \parT \Delta])$, is also convex and compact. By Corollary~\ref{cor:der.reso} the set $\RApply(\Theta,\Delta)$ is thus convex and compact. Combining this with (\ref{eq:sep1}), and using the Separation Hyperplane Lemma \cite{esop,Mat02}, we infer the existence of some hyperplane whose normal is $h\in\Real^\Omega$ such that 
$h\cdot o' > h\cdot o$
for all $o'\in \RApply(\Theta,\Delta)$. By scaling $h$, we obtain without loss of generality that $h\in [-1,1]^\Omega$.
It follows that
\[\bigsqcap h\cdot\RApply(\Theta,\Delta) ~~>~~ h\cdot o ~~\geq~~ \bigsqcap h\cdot\RApply(\Theta,\Gamma)\]
which is a contradiction to the assumption that $\Delta\rrMustleq \Gamma$.
\end{proof}

\noindent
Note that in the above proof the normal of the separating hyperplane
belongs to $[-1,1]^\Omega$ rather than $[0,1]^\Omega$. So we cannot
repeat the above proof for $\nrMustleq$. In general, we do not have that
$\Delta\nrMustleq \Gamma$ implies
$\RApply(\Theta,\Delta)\supseteq\RApply(\Theta,\Gamma)$ for any
$\Omega$-test $\Theta$ and for arbitrary finitary processes $\Delta$ and $\Gamma$, that is
  finitary processes which might not be convergent. However, when we
  restrict ourselves to finitary convergent processes, this property
  does indeed hold, as can be seen from the first four lines in the
  proof of Theorem~\ref{thm:fs.rr}.  Note that in that proof there
  is an essential use of the failure simulation preorder; in
  particular the pleasing property stated in
  Lemma~\ref{lem:failsim}. Even for finitary convergent processes
  we cannot give a direct and simple proof of that
  property for $\nrMustleq$, analogous to that of
  Theorem~\ref{thm:nr.subset}.  

\section{Conclusion}\label{sec:conclusion}
We have studied a notion of real-reward testing which extends the
traditional nonnegative-reward testing with negative rewards. It
turned out that the real-reward may preorder is the inverse of the real-reward
must preorder, and vice versa. More interestingly, for finitary
convergent processes, the real-reward must testing preorder coincides with
the nonnegative-reward testing preorder. In order to prove this result, we
have capitalised on a characterisation of nonnegative-reward testing in terms of
a derivation based simulation preorder. Relating derivations to resolutions, 
on which the testing theories are based, involved proving some analytic properties such as
the continuity of a function for calculating testing outcomes. 

Although for finitary convergent processes real-reward must testing
is no more powerful than non\-negative-reward must testing,
the same does not hold for may testing. This is immediate from
our result that (the inverse of) real-reward may testing is as
powerful as real-reward must testing, that is known not to hold for
nonnegative-reward may- and must testing. For finitary processes we
know from \cite{concur} that $\nrMayleq$ and $\nrMustleq$
correspond to the simulation and failure simulation preorder
respectively, and without divergence the latter is strictly more
discriminating than the former.

\bibliographystyle{eptcs}
\begin{thebibliography}{10}
\providecommand{\bibitemdeclare}[2]{}
\providecommand{\urlprefix}{Available at }
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\href}[2]{\texttt{#2}}
\providecommand{\urlalt}[2]{\href{#1}{#2}}
\providecommand{\doi}[1]{doi:\urlalt{http://dx.doi.org/#1}{#1}}
\providecommand{\bibinfo}[2]{#2}

\bibitemdeclare{article}{DNH84}
\bibitem{DNH84}
\bibinfo{author}{R.~De~Nicola} \& \bibinfo{author}{M.~Hennessy}
  (\bibinfo{year}{1984}): \emph{\bibinfo{title}{Testing equivalences for
  processes}}.
\newblock {\sl \bibinfo{journal}{Theoretical Computer Science}}
  \bibinfo{volume}{34}, pp. \bibinfo{pages}{83--133},
  \doi{10.1016/0304-3975(84)90113-0}.

\bibitemdeclare{article}{lmcs}
\bibitem{lmcs}
\bibinfo{author}{Y.~Deng}, \bibinfo{author}{R.J. van Glabbeek},
  \bibinfo{author}{M.~Hennessy} \& \bibinfo{author}{C.C. Morgan}
  (\bibinfo{year}{2008}): \emph{\bibinfo{title}{Characterising testing
  preorders for finite probabilistic processes}}.
\newblock {\sl \bibinfo{journal}{Logical Methods in Computer Science}}
  \bibinfo{volume}{4}(\bibinfo{number}{4}):\bibinfo{eid}{4},
  \doi{10.2168/LMCS-4(4:4)2008}.

\bibitemdeclare{inproceedings}{concur}
\bibitem{concur}
\bibinfo{author}{Y.~Deng}, \bibinfo{author}{R.J. van Glabbeek},
  \bibinfo{author}{M.~Hennessy} \& \bibinfo{author}{C.C. Morgan}
  (\bibinfo{year}{2009}): \emph{\bibinfo{title}{Testing finitary probabilistic
  processes}}.
\newblock In: {\sl \bibinfo{booktitle}{{\rm Proc.} CONCUR'09}}, {\sl
  \bibinfo{series}{\rm LNCS}} \bibinfo{volume}{5710},
  \bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{274--288},
  \doi{10.1007/978-3-642-04081-8\_19}.

\bibitem{finitary} { Y.~Deng, R.J. van Glabbeek, M.~Hennessy \& C.C.~Morgan} (2009):
\newblock {\em Testing finitary probabilistic processes.}
\newblock Full version of \cite{concur}. Available at
\url{http://www.cse.unsw.edu.au/~rvg/pub/finitary.pdf}.

\bibitemdeclare{article}{abstract}
\bibitem{abstract}
\bibinfo{author}{Y.~Deng}, \bibinfo{author}{R.J. van Glabbeek},
  \bibinfo{author}{M.~Hennessy} \& \bibinfo{author}{C.C. Morgan}
  (\bibinfo{year}{2011}): \emph{\bibinfo{title}{Real Reward Testing for
  Probabilistic Processes}}.
\newblock In: {\sl {\rm Proc.} QAPL'11}.
\newblock {\sl \bibinfo{journal}{EPTCS}} \bibinfo{volume}{57}, pp.
  \bibinfo{pages}{61--73}, \doi{10.4204/EPTCS.57.5}.

\bibitemdeclare{article}{gdpf}
\bibitem{gdpf}
\bibinfo{author}{Y.~Deng}, \bibinfo{author}{R.J. van Glabbeek},
  \bibinfo{author}{M.~Hennessy}, \bibinfo{author}{C.C. Morgan} \&
  \bibinfo{author}{C.~Zhang} (\bibinfo{year}{2007}):
  \emph{\bibinfo{title}{Remarks on Testing Probabilistic Processes}}.
\newblock {\sl \bibinfo{journal}{ENTCS}} \bibinfo{volume}{172}, pp.
  \bibinfo{pages}{359--397}, \doi{10.1016/j.entcs.2007.02.013}.

\bibitemdeclare{inproceedings}{esop}
\bibitem{esop}
\bibinfo{author}{Y.~Deng}, \bibinfo{author}{R.J. van Glabbeek},
  \bibinfo{author}{C.C. Morgan} \& \bibinfo{author}{C.~Zhang}
  (\bibinfo{year}{2007}): \emph{\bibinfo{title}{Scalar Outcomes Suffice for
  Finitary Probabilistic Testing}}.
\newblock In: {\sl \bibinfo{booktitle}{{\rm Proc.} ESOP'07}}, {\sl
  \bibinfo{series}{\rm LNCS}} \bibinfo{volume}{4421},
  \bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{363--368},
  \doi{10.1007/978-3-540-71316-6\_25}.

\bibitemdeclare{inproceedings}{vG93}
\bibitem{vG93}
\bibinfo{author}{R.J. van Glabbeek}
  (\bibinfo{year}{1993}): \emph{\bibinfo{title}{The Linear Time -- Branching Time Spectrum {II}; The
                 semantics of sequential systems with silent moves
                 (extended abstract)}}.
\newblock In: {\sl \bibinfo{booktitle}{{\rm Proc.} CONCUR'93}}. {\sl
  \bibinfo{series}{\rm LNCS}} \bibinfo{volume}{751},
  \bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{66--81}, \doi{10.1007/3-540-57208-2\_6}.

\bibitemdeclare{book}{henn}
\bibitem{henn}
\bibinfo{author}{M.~Hennessy} (\bibinfo{year}{1988}): \emph{\bibinfo{title}{An
  Algebraic Theory of Processes}}.
\newblock \bibinfo{publisher}{MIT Press}.

\bibitemdeclare{inproceedings}{JHW94}
\bibitem{JHW94}
\bibinfo{author}{B.~Jonsson}, \bibinfo{author}{C.~Ho-Stuart} \&
  \bibinfo{author}{Wang Yi} (\bibinfo{year}{1994}):
  \emph{\bibinfo{title}{Testing and Refinement for Nondeterministic and
  Probabilistic Processes}}.
\newblock In: {\sl \bibinfo{booktitle}{{\rm Proc.} FTRTFT'94}}, {\sl
  \bibinfo{series}{\rm LNCS}} \bibinfo{volume}{863},
  \bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{418--430},
  \doi{10.1007/3-540-58468-4\_176}.
  
\bibitemdeclare{article}{Kozen:85}
\bibitem{Kozen:85}
\bibinfo{author}{D.~Kozen} (\bibinfo{year}{1985}):
  \emph{\bibinfo{title}{A Probabilistic {PDL}}}.
\newblock {\sl \bibinfo{journal}{JCSS}} \bibinfo{volume}{30(2)}, pp.
  \bibinfo{pages}{162--178}, \doi{10.1016/0022-0000(85)90012-1}.

\bibitemdeclare{book}{Mat02}
\bibitem{Mat02}
\bibinfo{author}{J.~Matousek} (\bibinfo{year}{2002}):
  \emph{\bibinfo{title}{Lectures on Discrete Geometry}}.
\newblock \bibinfo{publisher}{Springer}.

\bibitemdeclare{book}{ccs}
\bibitem{ccs}
\bibinfo{author}{R.~Milner} (\bibinfo{year}{1989}):
  \emph{\bibinfo{title}{Communication and Concurrency}}.
\newblock \bibinfo{publisher}{Prentice-Hall}.

\bibitemdeclare{book}{Put94}
\bibitem{Put94}
\bibinfo{author}{M.L. Puterman} (\bibinfo{year}{1994}):
  \emph{\bibinfo{title}{Markov Decision Processes}}.
\newblock \bibinfo{publisher}{Wiley}, \doi{10.1002/9780470316887}.

\bibitemdeclare{book}{KNP04}
\bibitem{KNP04}
\bibinfo{author}{J.J.M.M. Rutten}, \bibinfo{author}{M.Kwiatkowska},
  \bibinfo{author}{G.~Norman} \& \bibinfo{author}{D.~Parker}
  (\bibinfo{year}{2004}): \emph{\bibinfo{title}{Mathematical Techniques for
  Analyzing Concurrent and Probabilistic Systems, {\rm P. Panangaden and F. van
  Breugel (eds.)}}}.
\newblock {\sl \bibinfo{series}{CRM Monograph Series}}~\bibinfo{volume}{23},
  \bibinfo{publisher}{American Mathematical Society}.

\bibitemdeclare{phdthesis}{Seg95}
\bibitem{Seg95}
\bibinfo{author}{R.~Segala} (\bibinfo{year}{1995}):
  \emph{\bibinfo{title}{Modeling and Verification of Randomized Distributed
  Real-Time Systems}}.
\newblock Ph.D. thesis, \bibinfo{school}{MIT}.

\bibitemdeclare{inproceedings}{Seg96}
\bibitem{Seg96}
\bibinfo{author}{R.~Segala} (\bibinfo{year}{1996}):
  \emph{\bibinfo{title}{Testing Probabilistic Automata}}.
\newblock In: {\sl \bibinfo{booktitle}{{\rm Proceedings} CONCUR'96}}, {\sl
  \bibinfo{series}{\rm LNCS}} \bibinfo{volume}{1119},
  \bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{299--314},
  \doi{10.1007/3-540-61604-7\_62}.

\bibitemdeclare{inproceedings}{WL92}
\bibitem{WL92}
\bibinfo{author}{Wang Yi} \& \bibinfo{author}{K.G. Larsen}
  (\bibinfo{year}{1992}): \emph{\bibinfo{title}{Testing Probabilistic and
  Nondeterministic Processes}}.
\newblock In: {\sl \bibinfo{booktitle}{{\rm Proc.} PSTV'92}}. {\sl
  \bibinfo{series}{IFIP Transactions}} \bibinfo{volume}{C-8},
  \bibinfo{publisher}{North-Holland}, pp. \bibinfo{pages}{47--61}.

\bibitemdeclare{book}{Win93}
\bibitem{Win93}
\bibinfo{author}{Glynn Winskel}
  (\bibinfo{year}{1993}): \emph{\bibinfo{title}{The Formal Semantics of Programming Languages: An Introduction}}.
  \bibinfo{publisher}{The MIT Press}.

\end{thebibliography}

\end{document}

Names of distributions:
Delta              default (sub)distribution
Delta, Gamma       processes related by preorders, with Gamma on the right
Xi                 one of Delta or Gamma (used only once)
Theta              test
Phi                result of applying a test to a process
Lambda             initial distribution of a resolution
Lambda             example extreme derivative
Psi                reachable distribution in a resolution
