\documentclass[runningheads]{llncs}
\usepackage{amssymb}
\usepackage[pdftex]{graphicx}
\setcounter{page}{363} % Page numbers adapted to forthcoming ESOP proceedings
%%% General principle is that "our" macros begin with a capital,
%%% the idea being to make it easy to tell them apart from
%%% macros inherited from TeX, LaTeX or Springer.

%%%%%%
%%% Fonts
\newfont{\Fsc}{eusm10}   % Frenchscript letters

%%%%%%
%%% Theorem-like environments and accoutrements
\newenvironment{Definition}{\begin{definition}\rm}{\end{definition}}
\newenvironment{Theorem}{\begin{theorem}\rm}{\end{theorem}}
\newenvironment{Proposition}{\begin{proposition}\rm}{\end{proposition}}
\newenvironment{Lemma}{\begin{lemma}\rm}{\end{lemma}}
\newenvironment{Corollary}{\begin{corollary}\rm}{\end{corollary}}
\newenvironment{Figure}{\begin{figure}[t]}{\end{figure}}
\newenvironment{Itemize}{
 \begin{list}{$-$}{\leftmargin 18pt
                   \labelwidth\leftmargini\advance\labelwidth-\labelsep
                   \topsep 2pt \itemsep 0pt \parsep 0pt}}{\end{list}}
\newcommand\EndMathSym {\raisebox{.05em}{\small \P}}
\newcommand\EndMath {\hfill\EndMathSym}
\newcommand\EndMathUp[1] {\hfill\raisebox{#1}[0pt][0pt]{\EndMathSym}}

%%%%%%
%%% Symbols
%%%
%%% Those ending with K are \kern'd, usually negatively
%%%	to make a following "." slip under neatly.
%%%
\newcommand\StartA {a^\circ}
\newcommand\StartM {m^\circ}
\newcommand\StartMK {m^\circ}
\newcommand\StartS {s^\circ}
\newcommand\StartSK {s^\circ \kern -0.2em}
\newcommand\StartR {r^\circ}
\newcommand\StartRK {r^\circ \kern -0.2em}
\newcommand\StartT {t^\circ}
\newcommand\StartTK {t^\circ \kern -0.2em}
\newcommand\StartU {u^\circ}
\newcommand\StartV {v^\circ}
\newcommand\W {\omega}
\newcommand\AllW {\Omega}
\newcommand\WW {w}
\newcommand\AllWW {{\mathbb W}}
\newcommand\AllWWK {{\mathbb W}\kern -0.1em}
\newcommand\AllWWF {{\mathbb W}_{\kern -0.25em f}}
\newcommand\AllWWFK {{\mathbb W}_{\kern -0.25em f}\kern -0.1em}
\newcommand\Inact {{\bf 0}} 
\newcommand\Spot {{\mathrel{\mbox{\boldmath$\cdot$}}}}
\newcommand\LFP {{\sf lfp}}
\newcommand\MT {{\mathbb T}}
\newcommand\ME {{\mathbb E}}
\newcommand\MI {{\mathbb I}}
\newcommand\SDol {S_{\$}}
\newcommand\STransS[1] {{\CT} \kern -.2em .#1}
\newcommand\Nat  {\bbbn}
\newcommand\Real {\bbbr}
\newcommand\Zero {\underline{0}}
\newcommand\Ones {\underline{1}}
\newcommand\STrans {\CT}
\newcommand\SProbs {{\mathbb W}}
\newcommand\SProb {w}
\newcommand\PowK {\mbox{\Fsc P} \kern -0.1em}
\newcommand\ActA {\alpha}
\newcommand\ActB {\beta}
\newcommand\Pow {\mathop{\mbox{\Fsc P}}}

%%%%%%
%%% Words
\newcommand\CSP {\textrm{CSP}}
\newcommand\MDP {\textit{MDP}}

%%%%%%
%%% Unary operators and types
\newcommand\Dist[1] {\overline{#1}}
\newcommand\Dirac[1] {\overline{#1}}
\newcommand{\CD}[1] {\widehat{#1}}
\newcommand\INF {\mathop{\mbox{\Large$\sqcap$}}}
\newcommand\Inf {\mathop\sqcap}
\newcommand\SUP {\mathop{\mbox{\Large$\sqcup$}}}
\newcommand\Sup {\mathop\sqcup}
\newcommand\UNION {\mathop\bigcup}

%%%%%%
%%% Binary operators
%%%
%%% Those ending with N are \mathord'd --- in some contexts they
%%%	look better that way.
%%%
\newcommand\Occurs[2] {#1!#2}
\newcommand\Min {\mathbin\sqcap}
\newcommand\Fun {\mathord\rightarrow}
\newcommand\PC[1] {\mathbin{_{#1}\oplus}}
\newcommand\PCF[1] {\mathbin{_{#1}\kern -.1em\oplus}} % For when \frac is used.
\newcommand\Max {\mathbin\sqcup}
\newcommand\Union {\mathbin\cup}
\newcommand\Inter {\mathbin\cap}
\newcommand\TimesN {\mathord\times}
\newcommand\MinusN {\mathord-}
\newcommand\PlusN {\mathord+}
\newcommand\GeqN{\mathord\geq}
\newcommand{\GtN}{\mathord>}
\newcommand\ParN {\mathord\parallel}
\newcommand{\EqN}{\mathord=}
\newcommand\Dot {\mathop\cdot}
\newcommand\DOTN {\mathord\cdot}
\newcommand\HoareHN[2] {#1_H \DOTN #2}
\newcommand\SmythHN[2] {#1_S \DOTN #2}

%%%%%%
%%% Binary relations
\newcommand\Implies {\mathrel\Rightarrow}
\newcommand\Implied {\mathrel\Leftarrow}
\newcommand\Equiv {\mathrel\Leftrightarrow}
\newcommand\FArrow[3] {#1\!\stackrel{#2}{\longrightarrow}\!#3}
\newcommand\LeqS {\leq_S}
\newcommand\LeqH {\leq_H}
\newcommand\InN {\mathop\in}

%%%%%%
%%% Complex and miscellaneous
\newcommand\Both {\textrm{\,--}}
\newcommand\Length[1] {\mathord{|}#1\mathord{|}}
\newcommand\Defs {\mathrel{{\colon}\mathord=}}
\newcommand\DefsR {\mathrel{\mathord={\colon}}}
\newcommand\Supp[1] {\lceil#1\rceil}
\newcommand\SmustA[1] {\sqsubseteq_{\tt must}^{#1}}
\newcommand\SmayA[1] {\sqsubseteq_{\tt may}^{#1}}
\newcommand\SbothA[1] {\sqsubseteq_{\Both}^{#1}}
\newcommand\Smust[1] {\leq_{\tt must}^{#1}}
\newcommand\Smay[1] {\leq_{\tt may}^{#1}}
\newcommand\Sboth[1] {\leq_{\Both}^{#1}}
\newcommand\Smxx[1] {\sqsubseteq^{#1}}
\newcommand\FootNoteRef[1] {$^{{\rm #1}}$}
\newcommand\CT {{\cal T}}
\newcommand\CTP {\CT'}
\newcommand\CTK {\CT\kern -.2em}
\newcommand\CTPK {\CTP\kern -.2em}
\newcommand\SetST[2]{\{#1\mid#2\}}
\newcommand\Set[1]{\{#1\}}
\newcommand{\F}{f}
\newcommand{\FK}{\F \kern -.15em}
\newcommand{\GPK}{g' \kern -.2em}
\newcommand{\FFK}{F \kern -.15em}
\newcommand\At[1] {\mbox{\scriptsize @\,$#1$}}
\newcommand\Scalar {1}
\newcommand\AllFin {{\raisebox{-.07em}[0pt][0pt]{\large$\ast$}}}
\newcommand\Reward {{\rm reward}}
\newcommand\Comma {\kern -.5em,\kern .5em }
\newcommand\Point {\kern -.5em.\kern .5em }


%%%%%
%%% Typesetting trix
\newcommand\Plat[1] {\raisebox{0pt}[0pt][0pt]{#1}} % No vertical space.
\newcommand\Smal[1] {\makebox[0pt][c]{#1}} % No horizontal space.
\newcommand\Wide[1] {~~~#1~~~} % For outermost operator in displays.
\newcommand\HangLeft[1] {\makebox[0pt][r]{#1}} % Hang out to left.
\newcommand\HangRight[1] {\makebox[0pt][l]{#1}} % Hang out to right.

%%%%%
%%% Abbreviations
\newcommand\Sec[1] {Sec.~\ref{#1}}
\newcommand\Fig[1] {Fig.~\ref{#1}}
\newcommand\Thm[1] {Thm.~\ref{#1}}
\newcommand\Lem[1] {Lem.~\ref{#1}}
\newcommand\Prop[1] {Prop.~\ref{#1}}
\newcommand\Eqn[1] {(\ref{#1})}
\newcommand\WLOG {\textit{wlog}}
\newcommand\PClosed {\textit{p-closed}}
\newcommand\PClosure {\textit{p-closure}}
\newcommand\Def[1] {Def.~\ref{#1}}
\newcommand\IE {\textit{i.e.}} % This is non-standard, but I like it.
\newcommand\EG {\textit{e.g.}}
\newcommand\EtC {\textit{etc.}}
\newcommand\App[1] {App.~\ref{#1}}
\newcommand\Cor[1] {Cor.~\ref{#1}}
\newcommand\EtAl {\textit{et al.}}

%%%%%
%%% Labelled transition systems
\newcommand\LT[1] {\buildrel #1 \over \longrightarrow}
\newcommand\WLT[1] {\buildrel #1 \over \Longrightarrow}
\newcommand\SR[1] {\buildrel #1 \over \rightarrow}
\newcommand\SRP[1] {\buildrel #1 \over {\rightarrow'}}
\newcommand\SRPP[1] {\buildrel #1 \over {\rightarrow''}}
\newcommand\RSA[1] {\buildrel #1 \over \rightsquigarrow}
\newcommand\RULE[2] {\begin{tabular}{c}#1\\\hline#2\end{tabular}} 
\newcommand\RT {\rightarrowtail}
\newcommand\EV {\rightsquigarrow}
\newcommand\Finish[1] {\vskip.2cm\noindent{\bf #1}\vskip.2cm}
\mathcode`\|="326A % `|' as relation operator
\newcommand\Mid {\mathbin{\mbox{\Large{$\mid$}}}}

%%%%%%
%%% Reasoning environment
%%%
%%% Use this rather than eg array, because it breaks properly
%%% at page boundaries.
%%%
\newenvironment{Reason}{%
 \begin{tabbing}\hspace{4em}\=\kill}{\end{tabbing}\vspace{-2.5ex}}
\newcommand\Space {~ \\}
\newcommand\Step[2]%
 {#1 \> $\begin{array}[t]{ll}#2\end{array}$ \\}
\newcommand\StepR[3]%
 {#1 \> $\begin{array}[t]{ll}#3\end{array}$
 \` {\RF \makebox[0pt][r]{#2}} \\}
\newcommand\WideStep[2] {#1 \> $#2$ \\}
\newcommand\WideStepR[3] {#1 \` {\RF #2} \\ \> $#3$ \\}
\newcommand\WideThinStepR[3] {#1 \` {\RF #2} \\ \> $#3$ \\}
\newcommand\ThinStep[2] {#1 \> $#2$ \\}
\newcommand\ThinStepR[3] {#1 \> $#3$ \` {\RF #2} \\}
\newcommand\RF {\small}

%%%%%%
%%% Graphic helper
%%%
%%% \JPGinText{upNudge}{rightNudge}{scaleFactor}{PDFfileName}
%%%
\newcommand\JPGinText[4]%
{\makebox[0pt][l]{%
{\def\Up{#1}\def\Right{#2}% Use \def in case they're already defined.
\hfill%
\raisebox{\Up}[0pt][0pt]{% No height, no depth.
\makebox[0pt][l]{\hspace{\Right}% No width.
\includegraphics[scale=#3]{#4.jpg}%
}}}}}

%%%%% Rob's macros
\def\lastandname{~{\small\&}}			% between last two authors
\newcommand{\deterministic}{fully probabilistic}% at most one outgoing trans.
\newcommand{\prob}{\textrm{Pr}_{\kern -0.05em\raisebox{-.2em}{\tiny R}}}	% probability
\newcommand{\probK}{\textrm{Pr}_{\kern -0.1em\raisebox{-.25em}{\tiny R}}\kern -.2em}	% probability kerned
\newcommand{\eM}{{\rm M}}			% an automaton
\newcommand{\eR}{{\rm R}}			% a fully probabilistic automaton
\newcommand{\eT}{{\rm T}}			% a test automaton
\newcommand{\eU}{{\rm U}}			% a test automata converter
\newcommand{\eV}{{\rm V}}			% a test automata converter
\newcommand{\eA}{{\rm A}}			% a combined automaton

\newcommand{\Deleted}[1]{}

\begin{document}
\title{Scalar Outcomes Suffice \\ for Finitary Probabilistic Testing}
\authorrunning{Y. Deng, R.J. van Glabbeek, C.C. Morgan \& C. Zhang}
\author{Yuxin Deng\inst{1}%
  \thanks{We acknowledge the support of the Australian Research Council Grant DP034557.}
\and Rob van Glabbeek\inst{\,2}\fnmsep\inst{1}
\and Carroll Morgan\inst{1\star}
\and Chenyi Zhang\inst{\,1}\fnmsep\inst{2}}
\institute{School of Comp.\ Sci.\ and Eng., University of New South Wales, Sydney, Australia% 2052
\and National ICT Australia, Locked Bag 6016, Sydney, NSW 1466, Australia}
\maketitle
\setcounter{footnote}{0}

\begin{abstract}
The question of equivalence has long vexed research in concurrency,
leading to many different denotational- and bisimulation-based
approaches; a breakthrough occurred with the insight that tests
expressed within the concurrent framework itself, based on a
special ``success action''\Comma yield
equivalences that make only inarguable distinctions.

When probability was added, however, it seemed necessary to extend the
testing framework beyond a direct probabilistic generalisation in order to
remain useful. An attractive possibility was the extension to \emph{multiple}
success actions that yielded \emph{vectors} of real-valued outcomes.

Here we prove that such vectors are unnecessary when
processes are \emph{finitary}, that is finitely branching and finite-state:
single \emph{scalar} outcomes are just as powerful. Thus for finitary
processes we can retain
the original, simpler testing approach and its
direct connections to other naturally scalar-valued phenomena. 
\end{abstract}

\section{Introduction}

The theory of testing of De Nicola \& Hennessy \cite{DH84} yields equivalences making only inarguable distinctions: two processes are may-testing inequivalent iff there is a context, built with parallel composition and hiding or restriction operators, in which one of them \emph{might} do a visible action but the other definitely can not; they are must-testing inequivalent iff there is a context in which one \emph{must} do a visible action, but the other might never do any. This reduces a complex phenomenon to a scalar- (in fact Boolean-) valued outcome.

Wang \& Larsen \cite{WL92} generalised this theory in a straightforward way to processes with probabilistic and nondeterministic choice, again yielding only distinctions that are hard to argue with: two processes are may-testing inequivalent iff there is a context in which, in the best case (when resolving nondeterministic choice), one of them might do a visible action with some probability $p$ whereas the other falls short of that. They are must-testing inequivalent iff there is a context in which, in the worst case, one must do a visible action with probability $p$, whereas the other might fall short of that.

Wang \& Larsen ended with the question of finding denotational characterisations of may- and must testing; for non-trivial examples this is necessary to show 
the equivalence of two processes. The question is still open today,
although Jonsson \& Wang \cite{JW02} have found a denotational characterisation
\pagebreak[3] % to prevent bad page break on page 4
in the special case of may-testing for processes without internal actions.

Meanwhile, progress has been made elsewhere for notions of testing
that are seemingly more powerful than Wang \& Larsen's.
Most notably,
Segala \cite{Seg96} found denotational characterisations of variants
of may- and must testing that employ multiple success actions instead
of a single one, and consequently yield vectors of real-valued
outcomes instead of scalars. Earlier, Jonsson, Ho-Stuart \& Wang \cite{TaRfNaPP} characterised variants that employ so-called ``reward testing''\Comma and that consider non-probabilistic test processes only.

It follows immediately from the definitions that Segala's vector-based
testing is \emph{at least} as powerful as the scalar testing of Wang \& Larsen,
while reward testing sits in between.  Unfortunately, the possibility
that these extended notions of testing are strictly \emph{more} powerful suggests that the argument above, that
testing equivalences make no unwarranted distinctions, might not
apply to them.%
\footnote{However, Stoelinga \& Vaandrager \cite{aTSfPA} offer evidence that
  the distinctions of Segala's vector-based may-testing are observable
  by repeating experiments many times.}

In this paper we show that in fact the argument \emph{does} apply, at least for finitary processes, where we prove all three notions to be equally powerful. This is a fundamental prerequisite for a stable notion of program equivalence, a core concept for rigorous software engineering.

\section{Probabilistic Testing of Probabilistic Automata}\label{s1507}

\subsection{Probabilistic Structures and Notational Conventions}\label{s2117}

We write $\FK.s$ instead of $f(s)$ for function application, with left
association so that $\FK.g.x$ means $(f(g))(x)$.
\begin{Itemize}
\item A \emph{discrete probability distribution} over
  a set $X$ is a function $\mu\in X\Fun[0,1]$ with $\mu.X=1$, where
  for subset $X'$ of $X$ we define $\mu.X' \Defs \sum_{x\in
  X'}\mu.x$.\\ We write \Plat{$\Dist{X}$} for the set of all such distributions
  over $X$.
\item The \emph{point-} or \emph{Dirac distribution} $\Dirac{x}$
  assigns probability one to $x\InN X$.
\item The \emph{support} $\Supp{\mu}$ of distribution $\mu$ is the set
  of elements $x$ such that $\mu.x \neq 0$.
\item Given $p\in[0,1]$ and distributions $\mu,\zeta \InN \Dist{X}$,
  the \emph{weighted average} $\mu\PC{p}\zeta\InN\Dist{X}$ is the distribution defined
  $(\mu\PC{p}\zeta).x \Defs p\TimesN \mu.x+ (1\MinusN p)\TimesN \zeta.x$~.
\item Given some function $f\in X\Fun\Real$ (a \emph{random variable}),
  its \emph{expected value} $\mu.f$ over distribution $\mu$ is the
  weighted average $\sum_{x\in X}(\mu.x \times \FK.x)$.%
\footnote{\label{n1426}This extends to any linear vector space, in particular to functions in $X\Fun\Real^N$\kern -.6em.}
\item Given a function $f\in X\Fun Y$, we write
  $\FK.\mu$ for the \emph{image distribution} in \Plat{$\Dist{Y}$} formed by
  applying $f$ to a distribution $\mu\in\Dist{X}$: for element $y\in
  Y$ we define $\FK.\mu.y \Defs\mu.\SetST{x\in X}{\FK.x=y}$.
\item The \emph{product} of two discrete probability distributions $\mu,\mu'$ over
  $X,X'$ is the distribution $\mu\times\mu'$ over $X\times X'$ defined
  $(\mu\times\mu').(x,x')\Defs\mu.x\times\mu'.x'$.
% \item A distribution $\mu\InN\Dist D$ over a set $D\subseteq \Dist X$
%   of distributions over $X$ can be collapsed into a single distribution
%   $\mathord\downarrow{\mu} \in \Dist X$ by adding up the distributions
%   in $D$ according to the weight that $\mu$ gives them:
%   $$\mathord\downarrow\mu.x := \sum_{\nu\in D} (\mu.\nu \times \nu.x).$$
\end{Itemize}


\subsection{Probabilistic Automata and their Resolutions}
In this paper we employ probabilistic automata \cite{SL94} as
representatives of a class of models that treat both
probabilistic and nondeterministic choice \cite{Var85,HJ90,WL92,HSM97}.

\begin{Definition}
A \emph{probabilistic automaton} is a tuple ${\eM}=(M,\StartMK\hspace{-2pt},E,I,\CT)$ where
\begin{Itemize}
\item $M$ is a set of \emph{states},
\item $\StartM \in \Dist{M}$ is a distribution of \emph{start states},
\item $E$ and $I$ are disjoint sets of \emph{external-} and \emph{internal actions} respectively and
\item $\CT\in M\Fun \Pow(\Sigma\times\Dist{M})$ is the
  \emph{transition relation}, where $\Sigma \Defs E\Union I$.
\end{Itemize}
Automaton $\eM$ is \emph{fully probabilistic} if from each state $m\InN M$ there is at most
one outgoing transition, \IE\ if the set $\CTK.m$ contains at most one element.
If $\CTK.m$ is finite for all $m\in M$,
then $\eM$ is said to be \emph{finitely branching}.
An \emph{execution sequence} of $\eM$ is an alternating sequence of
states and actions $m_0,\alpha_1,m_1,\alpha_2,\cdots$, either infinite
or ending in state $m_n$, such that $m_0\InN\Supp{\StartM}$ and for
all $i>0$ (and $i\leq n$ if finite) we have
$\exists(\alpha_{i},\mu_{i})\InN\CTK.m_{i-1}$ with $m_i\InN\Supp{\mu_i}$.
The execution sequence is \emph{maximal} if either it is infinite or $\CTK.m_n=\emptyset$.
\EndMath
\end{Definition}
From here on we use ``automaton'' to mean ``probabilistic automaton"\Point

Any automaton can be ``resolved'' into {\deterministic} automata as follows.
\begin{Definition}
A \emph{resolution} of an automaton $\eM=(M,\StartMK,E,I,\CT\kern .04em)$ is a
{\deterministic} automaton $\eR=(R,\StartRK,E,I,\CTP)$ such that there
is a \emph{resolving function} $\F \in R \Fun M$ with
\begin{Itemize}
\item $\FK.\StartR = \StartM$, \hfill \emph{equivalent initialisations}
\item if $\CTPK.r = \{(\alpha,\mu)\}$ then
  $(\alpha,\FK.\mu)\in\CTK.(\FK.r)$ and \hfill \emph{compatible choice taken}
\item if $\CTPK.r = \emptyset$ then $\CTK.(\FK.r) = \emptyset$ \hfill \emph{liveness preserved}
\end{Itemize}
for any $r\InN R$. \EndMath%
\HangRight{~\footnotemark}%
\footnotetext{We use this abstract definition because of its useful
  mathematical properties; it is equivalent to Segala's \cite{Seg96} in
  that it generates the same distributions over action sequences, as
  the following discussion illustrates.}
\end{Definition}

\noindent
A resolution has as its main effect the choosing in any state of a single outgoing transition
from all available ones; but $f$ can be non-injective, so that the choice can vary between different departures from that state, depending \EG\ on
the history of states and actions that led there. Further, since a single state of $\eM$ can be ``split''
into a distribution over several {states of $\eR$}, all mapped to it by $f$,
probabilistic \emph{interpolation} between distinct
choices is obtained automatically.\footnote{In this regard our
  resolutions strictly generalise the ones of Jonsson \EtAl\ \cite{TaRfNaPP}.}

\Fig{f0950} illustrates the history-dependent choice with states
$r_{1,{4}}$ both mapped to $m_1$; it illustrates interpolation with
states $r_{2,4}$ both mapped to $m_1$.
\begin{Figure}
We show that $\eM$ is resolved by $\eR$ in the following diagram. Enclosing circles
and ovals represent distributions, the enclosed shapes' relative sizes within hinting
at probabilities; on the left the shapes are associated 1-1 with the
distinct states, but the right-hand states' shapes indicate the
left-hand states \emph{to which they are mapped}. Thus the resolving
function $f$ is given by $\FK.r_{1,2,3,4} \Defs m_1$, $\FK.r_5 \Defs m_2$
and $\FK.r_6 \Defs m_3$.

\begin{center}
\Smal{\includegraphics[scale=0.45]{scalar1016.jpg}}
\end{center}

The left-hand automaton $\eM$ has initial (Dirac) distribution $\StartM=\Dirac{m_1}$ and transitions
\[
  \CTK.m_1 ~\Defs~ \{ (\ActA,\,\Dirac{m_1}) ~,~ (\ActB,\,\Dirac{m_2} \PCF{\frac{1}{2}} \Dirac{m_3}) ~,~ (\ActB,\Dirac{m_3}) \} ~,
  \hspace{4em}
  \CTK.m_2 ~=~ \CTK.m_3 ~\Defs~ \emptyset ~.
\]
The right-hand ({\deterministic}) resolution $\eR$ has initial distribution $\StartR= \Dirac{r_1}\PCF{\frac{1}{3}} \Dirac{r_2}$; its non-$\emptyset$ transitions are
\[
 \begin{array}{rcl}
  \CTPK.r_1 & ~\Defs~ 
 & \{(\ActA,\,\Dirac{r_3} \PCF{\frac{1}{2}}\Dirac{r_4})\} \\[.4em]
  \CTPK.r_2 & \Defs & \{(\ActB,\,\Dirac{r_5} \PCF{\frac{1}{2}} \Dirac{r_6})\}
 \end{array}
 \hspace{4em}
 \begin{array}{rcl}
  \CTPK.r_3 & ~\Defs~ & \{(\ActA,\,\Dirac{r_2} \PCF{\frac{1}{2}} \Dirac{r_4})\} \\[.4em]
  \CTPK.r_4 & ~\Defs~ & \{(\ActB,\,\Dirac{r_6}) \} ~.
  \end{array}
\]

\caption{\label{f0950} Example of a {\deterministic} resolution}
\end{Figure}

\subsection{Probabilities of Action Occurrences in Resolutions}

For a fully probabilistic automaton  in which all execution sequences
are finite, like $\eR$ from \Fig{f0950}, the probability of an action's
occurrence is easily obtained: we calculate probabilities for the maximal execution sequences, given for each
by multiplication of the probabilities of the choices
occurring along it; the probability of an action's occurrence is then
the sum of the so-calculated probabilities for all maximal sequences containing it.
For example, in $\eR$ the maximal-execution-sequence probabilities are
 \[
 \begin{array}{ll@{\hspace{3em}}p{4em}p{8em}}
  \langle r_1, \ActA, r_3, \ActA, r_2, \ActB, r_5 \rangle
    & \At{(1/3\TimesN 1/2\TimesN 1/2\TimesN 1/2)} & that is, &probability $1/24$ \\
  \langle r_1, \ActA, r_3, \ActA, r_2, \ActB, r_6 \rangle
    & \At{(1/3\TimesN 1/2\TimesN 1/2\TimesN 1/2)} & &probability $1/24$ \\
  \langle r_1, \ActA, r_3, \ActA, r_4, \ActB, r_6 \rangle
    & \At{(1/3\TimesN 1/2\TimesN 1/2\TimesN 1)} & &probability $1/12$ \\
  \langle r_1,\ActA,r_4,\ActB,r_6 \rangle & \At{(1/3\TimesN 1/2\TimesN 1)} &&probability $1/6$ \\
  \langle r_2, \ActB, r_5 \rangle &\At{2/3\TimesN 1/2}&& probability $1/3$ \\
  \langle r_2, \ActB, r_6 \rangle &\At{2/3\TimesN 1/2}&& probability $1/3$ ~,
 \end{array}
\]
with all other sequences being assigned probability zero. If we use
$f$ to map this distribution back to $\eM$, and aggregate, we get
\[
 \begin{array}{l@{\hspace{8em}}p{12em}}
  \langle m_1, \ActA, m_1, \ActA, m_1, \ActB, m_2 \rangle &probability $1/24$ \\
  \langle m_1, \ActA, m_1, \ActA, m_1, \ActB, m_3 \rangle &probability $1/24+1/12$ \\
  \langle m_1,\ActA,m_1,\ActB,m_3 \rangle &probability $1/6$ \\
  \langle m_1, \ActB, m_2 \rangle & probability $1/3$ \\
  \langle m_1, \ActB, m_3 \rangle & probability $1/3$ ~,
 \end{array}
\]
where we can see both history-dependence and interpolation at work.
Finally, concentrating on just the actions gives us
\[
 \begin{array}{l@{\hspace{8em}}p{16em}}
  \langle \ActA, \ActA, \ActB \rangle &probability $1/24+1/24+1/12$ \\
  \langle \ActA, \ActB \rangle &probability $1/6$ \\
  \langle \ActB \rangle & probability $1/3+ 1/3$ ~.\\
 \end{array}
\]
No matter which of the three views above we use, the probability that
a particular action occurs is the probability assigned to the
\emph{set} of all sequences containing that action: thus the
probability of $\ActA$'s occurrence is $1/24+1/24+1/12+1/6=1/3$; for
$\ActB$ the probability is 1. (The sum exceeds one because both can occur.)
\Deleted{The equivalence is argued as follows. The set of (finite or infinite)
sequences containing $\alpha$ is exactly the set of sequences having a
(finite) prefix in $\Sigma^{*\alpha}$, which is in turn exactly the
union of the $\sigma$-cones for $\sigma\InN\Sigma^{*\alpha}$, where a
$\sigma$-\emph{cone} is the set of sequences having prefix $\sigma$.

As we may restrict $\Sigma$ to the countably many actions that can
actually occur in the fully probabilistic automaton $\eR$, there are
only countably many such cones; and they are pairwise disjoint (no
element of $\Sigma^{*\alpha}$ can be a proper prefix of another); thus
the measure of that union is the sum of the measures of its individual
cones. And the measure of a cone is the probability assigned to its
prefix, as above.
}

When our automata can generate infinite executions, however, there
might be uncountably many of them: consider a looping automaton,
choosing forever between bits 0 and 1, whose infinite sequences thus
encode the whole unit interval $[0,1]$ in binary. Simple summation
within discrete distributions is then not appropriate;%
\footnote{Discrete distributions' supports must be countable and so
  they cannot, for example, describe a situation in which the
  uncountably many infinite sequences are equally likely --- unless
  they are all (equally) impossible.}
in this case we apply the following more general definition.

\begin{Definition}\label{probabilities of cones}\label{action probabilities}
Given a fully probabilistic automaton $\eR=(R,\StartRK,E,I,\CT)$, the
\emph{probability that $\eR$ starts with} a sequence of actions
$\sigma\InN \Sigma^*$, with $\Sigma\Defs E\Union I$, is given by
$\StartRK.(\probK.\sigma)$, where $\prob\in \Sigma^*
\Fun R \Fun [0,1]$ is defined inductively:
\[
 \probK.\varepsilon.r\Defs 1\quad\mbox{and}\quad
  \probK.(\alpha\sigma).r\Defs\left\{\begin{array}{l@{~~}l}
     \mu.(\probK.\sigma) & \mbox{if $\CTK.r = \{(\alpha,\mu)\}$ for some $\mu$} \\
     0 & \mbox{otherwise}
  \end{array}\right.
\]
Here $\varepsilon$ denotes the empty sequence of actions and
$\alpha\sigma$ the sequence starting with $\alpha\InN \Sigma$ and
continuing with $\sigma\InN \Sigma^*$. Recall from \Sec{s2117} that
$\mu.(\probK.\sigma)$ is the expected value over $\mu$ of the random
variable $\probK.\sigma \in R \Fun [0,1]$.
The value $\probK.\sigma.r$ is the probability that
$\eR$ proceeds with sequence $\sigma$ from state $r$.
% \footnote{Intuitively, there should be be a probability distribution over
% the set of all sequences of actions $\eR$ can perform that stem from
% \emph{total executions} rather than partial ones; these are either
% infinite or lead to a state from which no further transitions are possible.
% But, as observed above, these probability distributions are not always discrete.
% In probability theory, one therefore measures the probability of
% certain \emph{sets} of sequences only, without necessarily associating
% probabilities with each individual sequence.
% 
% A \emph{probability space} over a set $X$ is a triple $(X,\CX,\mu)$
% where the \emph{field} $\CX$ comprises those subsets of $X$ whose
% probability is well-defined, called the \emph{events}, and the
% \emph{distribution} $\mu\in\CX\Fun[0,1]$ gives the probability of each
% event. The field contains $\emptyset$, and is closed under complements
% and countable unions; the distribution satisfies $\mu.X = 1$, and
% $\mu.(\UNION_{n=0}^\infty X_n) = \sum_{n=0}^\infty (\mu.X_n)$ whenever
% the events $X_n\in\CX$ are pairwise disjoint.
% 
% In the case of infinite sequences of actions performed by a
% probabilistic automaton, the field conventionally used is the
% so-called \emph{sigma algebra} based on \emph{cones}, which latter are
% sets of sequences having a common finite prefix.
% The probability of a cone is simply the probability of its
% identifying prefix, as calculated in \Def{probabilities of cones}.}

Let $\Sigma^{*\alpha}$ be the set of finite sequences in
$\Sigma^*$ that contain $\alpha$ just once, namely at the end.
Then the probability that a fully probabilistic automaton $\eR$ ever
performs an action $\alpha$ is given by $\sum_{\sigma\InN\Sigma^{*\alpha}}\; \StartRK.(\probK.\sigma)$.
\footnote{\label{n1802}An alternative, but equivalent definition appeals to more general probabilistic measures: the probability of $\eR$'s performing $\alpha$ is the measure of the set of sequences containing $\alpha $ at any point \cite{Seg96}. We have specialised here for simplicity.
}
\EndMath
\end{Definition}

\subsection{Probabilistic Testing}\label{ProbAutomata:ProbTesting}

We now recall the testing framework of Segala \cite{Seg96} which, as
we will see, differs from the testing framework of Wang and Larsen
\cite{WL92} in that a test may have countably many success actions
rather than just one.\footnote{Another difference is that Segala's success actions must actually occur, whereas for Wang and Larsen (and earlier De Nicola and Hennessy \cite{DH84}), it is sufficient that a state be reached from which the action is possible. Here we treat only the former.}

We begin by defining the parallel composition of two automata in the \CSP\
style~\cite{Hoa85}, synchronising them on their common external actions.
\begin{Definition}
Let $\eM_1=(M_1,\StartM_1,E_1,I_1,\CT_1)$ and
$\eM_2=(M_2,\StartM_2,E_2,I_2,\CT_2)$ be two automata, and let
$\Sigma_i\Defs E_i\Union I_i$. They are
\emph{compatible} when the only actions they share are external, that
is when $\Sigma_1\Inter \Sigma_2 \subseteq E_1\Inter E_2$.
In that case their \emph{parallel composition} $\eM_1\ParN \eM_2$ is
$(M_1\TimesN M_2,\StartM_1\TimesN\StartM_2,E_1\Union E_2,I_1\Union I_2,\CT)$ where\\[1ex]
\mbox{}\quad
 $\CTK.(m_1,m_2) \Defs 
 \begin{array}[t]{l} \{(\ActA,\,\mu_1\TimesN\mu_2) \mid
 \alpha\InN\Sigma_1\Union\Sigma_2 \quad\wedge\\
  \quad(\ActA,\mu_i)\InN\CT_i.m_i \textrm{ if $\ActA\InN\Sigma_i$ else }
 \mu_i=\Dirac{m_i}, \textrm{for $i=1,2\}$}.\end{array}$%
\EndMathUp{-1.1em}
\end{Definition}

\noindent
Parallel composition is the basis of testing: it models the
interaction of the observer with the process being tested;
and it models the observer himself --- as an automaton.

From here on, we fix some disjoint sets $\ME$ and $\MI$ of external and internal actions,
and the automata we subject to testing ---the ones for which testing
preorders will be defined--- are the ones whose components of external-
and internal actions are subsets of $\ME$ and $\MI$.
Now let $\Omega\Defs\{\omega_1,\omega_2, \cdots\}$ be a countable set of
\emph{success actions}, disjoint from $\ME$ and $\MI$, and define a
\emph{test} to be an automaton $\eT=(T,\StartT,E,I,\CT)$ with
$E\supseteq\ME\Union\Omega$ and $I\Inter \MI=\emptyset$.
Thus every such test $\eT$ is automatically compatible with the automaton $\eM$ that is
to be tested, and in the parallel composition $\eM\ParN\eT$ \emph{all} the
external actions of $\eM$ must synchronise with actions of $\eT$.
Let $\MT$ be the class of all such tests, and write $\MT_N$ for the subclass
of $\MT$ that uses only $N$ success actions; we write $\MT_\AllFin$
for $\UNION_{N\in\Nat} \MT_N$ and, for convenience, allow $\MT_\Nat$ as a
synonym for $\MT$ itself.

To \emph{apply} test $\eT$ to automaton $\eM$ we first form the
composition $\eM \ParN \eT$ and then consider all resolutions of that
composition separately: in each one, any particular success action
$\W_i$ will have some probability of occurring; and those
probabilities, taken together, give us a single \emph{success tuple}
for the whole resolution, so that if $\WW$ is the tuple then $\WW_i$ is the
recorded probability of $\W_i$'s occurrence. The set of all those
tuples, \IE\ over all resolutions of $\eM \ParN \eT$, is then the
complete outcome of applying test $\eT$ to automaton $\eM$: as such,
it will be a subset of \Plat{$\AllWW \Defs [0,1]^{\Nat^+}$}.

\begin{Definition}\label{d1533}
For a {\deterministic} automaton $\eR$, let its (single) success tuple
\Plat{$\AllWWK.\eR \in [0,1]^{\Nat^+}$} be such that $(\AllWWK.\eR)_i$ is the
probability that $\eR$ performs the action $\omega_i$, as given in
\Def{action probabilities}.

Then for a (not necessarily {\deterministic}) automaton $\eM$ we
define the set of its success tuples to be those resulting as above
from all its resolutions:
\\[1ex]\mbox{}\hfill$
 \AllWWK.\eM \Wide{\Defs} \SetST{\AllWWK.\eR}{\textrm{$\eR$ is a resolution of $\eM$}}$.%
\EndMath
\end{Definition}
%
We note that the success-tuple set $\AllWWK.\eM$ is \emph{convex} in the following sense:
\begin{Lemma}\label{l1032}
For any two tuples $\WW_1,\WW_2\in\AllWWK.\eM$, their weighted average
$\WW_1\PC{p}\WW_2$
%, defined as $p\TimesN \WW_1 + (1\mathord-p)\TimesN\WW_2$,
is also in $\AllWWK.\eM$ for any $p\InN\,[0,1]$.
\begin{proof}
Let $\eR_1,\eR_2$ be the resolutions of $\eM$ that gave rise to $\WW_1,\WW_2$. Form $\eR$ as their disjoint union, except initially where we define $\StartR\Defs \StartR_1 \PC{p} \StartR_2$.
The new resolution $\eR$ generates the interpolated tuple
$\WW_1\PC{p}\WW_2$ as required.
% ; the argument extends to countably infinite interpolations.
\EndMath
\end{proof}
\end{Lemma}

\subsection{May- and Must Preorders}\label{s1207}

We now define various preorders $\sqsubseteq$ on testable
automata; in general $\eM_1\sqsubseteq\eM_2$ will mean that
$\eM_2$ scores at least as well as $\eM_1$ does on certain tests.

For $w,w'\in\AllWWK$, we write $w\leq w'$ if $w_i \leq w'_i$ for all $i\InN\Nat^+$.
Given that $\AllW$ comprises ``success'' actions it is natural to
regard $\leq$ on $\AllWW$ as a (non-strict) ``better than'' order,
\IE\ that it is better to have higher probabilities for the occurrence
of success actions. Since nondeterminism generates however \emph{sets}
of success tuples (\Def{d1533}), rather than merely individuals, we
are led to appeal to two complementary testing preorders on
automata; they are based on the standard techniques for promoting an
underlying order to a preorder on powersets.

\begin{Definition}\label{d:multi-testing}
Given two automata $\eM_1,\eM_2$ and a testing automaton $\eT$ compatible with both, say that
\[
 \begin{array}{r@{\hspace{2em}}c@{\hspace{2em}}l}
  \eM_1 \SmayA{\eT} \eM_2 &\textrm{iff}& \AllWWK.(\eM_1\ParN \eT) \LeqH \AllWWK.(\eM_2\ParN \eT) \\
  \eM_1 \SmustA{\eT} \eM_2 &\textrm{iff}& \AllWWK.(\eM_1\ParN \eT) \LeqS \AllWWK.(\eM_2\ParN \eT) ~,
 \end{array}
\]
where $\LeqH,\LeqS$ are the Hoare, resp.\ Smyth preorders on
$\Pow\AllWW$ generated from the index-wise order $\leq$ on $\AllWW$ itself.%
\footnote{The Hoare order is defined by $X \LeqH Y$ iff $\forall
  x\InN X : \exists y\InN Y : x \leq y$; similarly the Smyth order
  is defined by $X \LeqS Y$ iff $\forall y\InN Y : \exists x\InN X : x \leq y$
  \cite{AJ94}.}
%
Abstracting over all tests in $\MT$ then gives us
\[
 \begin{array}{r@{\hspace{2em}}c@{\hspace{2em}}l}
  \eM_1 \SbothA{\MT} \eM_2 &\textrm{iff}& \forall\, \eT\InN\MT :  \eM_1 \SbothA{\eT} \eM_2 ~,
 \end{array}
\]
where within a single formula or phrase we use ``--'' for
``\texttt{may}, \texttt{must} respectively'' in the obvious way,
and we define the preorders $\SbothA{\MT_\AllFin}$, and $\SbothA{\MT_N}$
for $N\GeqN 1$, by similar abstractions.
Finally, \emph{scalar testing} as employed by Wang \& Larsen
\cite{WL92} is defined by taking suprema and infima, as follows:
\[
 \begin{array}{r@{\hspace{2em}}c@{\hspace{2em}}l}
  \eM_1 \SmayA{\Scalar} \eM_2 &\textrm{iff}& \forall\, \eT\InN\MT_1 :
  \SUP\AllWWK.(\eM_1\ParN \eT) \leq \SUP\AllWWK.(\eM_2\ParN \eT) \\
  \eM_1 \SmustA{\Scalar} \eM_2 &\textrm{iff}& \forall\, \eT\InN\MT_1 :
  \INF\AllWWK.(\eM_1\ParN \eT) \leq \INF\AllWWK.(\eM_2\ParN \eT) ~.
 \end{array}
\]
\EndMathUp{1.5em}\vspace{-1.5em}
\end{Definition}
Thus, in vector-based testing $\SbothA{\MT}$, for each test
one compares sets of \emph{tuples} of reals, whereas for
\Plat{$\SbothA{\MT_1}$} one is merely comparing sets of (\mbox{mono-tuple-,} hence scalar) reals.  Then, by
taking extrema, scalar testing abstracts
even further to a comparison of single scalars.

Clearly $(\SbothA{\MT}) \Implies (\SbothA{\MT_\AllFin}) \Implies (\SbothA{\MT_1}) \Implies (\SbothA{\Scalar})$. Our principal interest is in determining the
situations in which the last is as powerful as all the others, that
is when the reverse implications also hold, giving equivalence: we ask
\begin{quote}
Under what conditions are \emph{scalar} tests on their own sufficient to distinguish probabilistic automata?
\end{quote}
In \Sec{s1632} we identify general criteria which suffice for scalar
testing; then in Secs.~\ref{s1006} and~\ref{s1520} we identify
classes of automata on which we can achieve those criteria.
Sections \ref{s1508} and \ref{s1111} introduce ``reward testing'' for that purpose.

\section{Reward Testing of Finite-Dimensional Tuple Sets}\label{s1508}

\Def{d1533} gives tuple sets $\AllWWK.(\eM\ParN \eT)$, coming from a
testee $\eM$ and test $\eT\InN\MT_\Nat$; when
in fact $\eT\InN\MT_\AllFin$ they can be considered to
lie in some $N$-dimensional unit cube $[0,1]^N$\kern -.2em.
We now abstract from automata, considering just those tuple sets; let $N$ be fixed.
This section shows it sufficient, under suitable conditions, to
record only an ``extremal expected reward'' for each set of $N$-tuple
outcomes, a single scalar rather than the whole tuple-set.

\begin{Definition}\label{l1023} A \emph{reward tuple} is an $N$-tuple
  $h\in[0,1]^N$ of real numbers; given such an $h$ we define two forms
  of \emph{extremal reward outcomes} with respect to any tuple set $W\subseteq[0,1]^N$:
\begin{Itemize}
\item The \emph{Hoare} outcome $\HoareHN{h}{W}$ is the supremum \quad$\SUP_{\WW\in W} (h\Dot\WW)$, and
\item The \emph{Smyth} outcome $\SmythHN{h}{W}$ is the infimum \quad$\INF_{\WW\in W} (h\Dot\WW)$\,,
\end{Itemize}
where within the extrema we write $h\Dot\WW$ for the dot-product of the two tuples.

Given a reward-tuple $h\InN\,[0,1]^N$\kern -.2em, the two forms of outcome give us two corresponding
\emph{reward orders} on tuple-sets $W_1,W_2\subseteq[0,1]^N$:
\[
 \begin{array}{r@{\hspace{2em}}c@{\hspace{2em}}l}
  W_1 \Smay{h} W_2 &\textrm{iff}& \HoareHN{h}{W_1} \leq \HoareHN{h}{W_2} \\
  W_1 \Smust{h} W_2 &\textrm{iff}& \SmythHN{h}{W_1} \leq \SmythHN{h}{W_2} ~,
 \end{array}
\]
where (note) the comparison $\leq$ on the right has now been reduced to simple scalars.  As in \Def{d:multi-testing}, this generalises so that we can define
\[
 \begin{array}{r@{\hspace{2em}}c@{\hspace{2em}}l}
  W_1 \Sboth{N} W_2 &\textrm{iff}& \forall h\InN\,[0,1]^N : W_1 \Sboth{h} W_2 ~.
 \end{array}
\]
\EndMathUp{2.1em}
\end{Definition}

\vspace{-1.9em}
\noindent
We will now show that these preorders coincide with $\LeqH$ and
$\LeqS$, respectively,
provided the tuple-sets have a certain form of closure, as follows:

\begin{Definition}\label{d1153}
We say that a subset $W$ of the $N$-dimensional Euclidean space is \PClosed\ (for \emph{probabilistically} closed) iff
\begin{Itemize}
\item It is \emph{convex}, that is if $w_1, w_2\InN W$ and
  $p\InN\,[0,1]$ then the weighted average $\WW_1\PC{p}\WW_2$
  is also in $W$, and
\item It is \emph{Cauchy closed}, that is it contains all its limit points in the usual Euclidean metric, and it is \emph{bounded}.%
\footnote{Cauchy closure and boundedness together amounts to
\emph{compactness}.}
\EndMath
\end{Itemize}
\end{Definition}
Our sets' being \PClosed\ will allow us to appeal to the
\emph{Separating Hyperplane Lemma} from discrete geometry  \cite[Thm.~1.2.4 paraphrased]{Mat02}:%
\footnote{The hyperplanes are motivated indirectly by a proof of McIver \cite[Lem.~8.2]{PPT}.}
\begin{Lemma} \label{l:sep}
Let $A$ and $B$ be two convex- and Cauchy-closed subsets of Euclidean $N$-space; assume that they are disjoint and that at least one of them is bounded. Then there is a
hyperplane that strictly separates them. \EndMath
\end{Lemma}
Here a \emph{hyperplane} is a set of the form $\{w\InN\Real^N \mid
h\cdot w = c\}$ for certain $h\InN \Real^N$ (the \emph{normal} of the
hyperplane) and $c\InN \Real$, and such a hyperplane \emph{strictly
  separates} $A$ and $B$ if for all $a\InN A$ and $b\InN B$ we have
$h\Dot a < c < h\Dot b$ or $h\Dot a > c > h\Dot b$.
\pagebreak[1]

Our main theorem is then a direct application of \Lem{l:sep}: the
normal $h$ of the asserted hyperplane provides the rewards used in \Def{l1023}.

\begin{Theorem}\label{t:geo}
Let $A,B$ be subsets of $[0,1]^N$; then we have
\[
 \begin{array}{rcl@{\hspace{2em}}p{10em}}
  A \LeqH B & \Wide{\textrm{iff}} & A \Smay{N} B & if $B$ is \PClosed, and \\
  A \LeqS B & \textrm{iff} & A \Smust{N} B  & if $A$ is \PClosed.
 \end{array}
\]
\begin{proof}
We consider first the \emph{only-if} -direction for the Smyth/must case:
\begin{Reason}
\Step{}{
 A \LeqS B
}
\StepR{$\Equiv$}{defn.~$\LeqS$}{
\forall b\InN B : \exists a\InN A : a \leq b
}
\StepR{$\Implies$}{$h\geq 0$}{
\forall h\InN\,[0,1]^N : \forall b\InN B : \exists a\InN A : h\Dot a \leq h\Dot b
}
\StepR{$\Implies$}{$\SmythHN{h}{A} \leq h\Dot a$}{
\forall h\InN\,[0,1]^N: \forall b\InN B : \SmythHN{h}{A} \leq h\Dot b
}
\StepR{$\Equiv$}{defn.~$(\SmythHN{h})$; properties of $\Inf$}{
\forall h\InN\,[0,1]^N: \SmythHN{h}{A} \leq \SmythHN{h}{B}
}
\StepR{$\Equiv$}{defn.~$\Smust{h}$}{
\forall h\InN\,[0,1]^N: A \Smust{h} B ~.
}
\StepR{$\Equiv$}{defn.~$\Smust{N}$}{
A \Smust{N} B ~.
}
\end{Reason}
For the \emph{if}-direction we use separating hyperplanes, proving the contrapositive:
\begin{Reason}
\Step{}{
 A \not\LeqS B
}
\StepR{$\Equiv$}{defn.~$\LeqS$; for some $b\InN B$}{
\forall a\InN A : \neg(a \leq b)
}
\StepR{$\Equiv$}{define $B' \Defs \SetST{b'\InN\Real^N}{b'\leq b}$}{
A \Inter B' = \emptyset
}
\Space
\StepR{$\Equiv$}{\Lem{l:sep}; $A$ is \PClosed; $B'$ is convex and Cauchy-closed}{
 \begin{array}[t]{@{}l}
  \exists h\InN\Real^N, c\InN \Real : \\
  \quad \forall a\InN A, b'\InN B' : \\
  \quad\quad h\Dot b' < c < h\Dot a ~,
 \end{array}
}
\end{Reason}
\JPGinText{-13.5em}{19em}{0.4}{scalar2046}
\parshape=1 0pt 0.596\textwidth % Narrow paragraphs until further notice (because inside list).
where \WLOG\ the inequality can be in the direction shown, else we simply multiply $h,c$ by $-1$.

We now argue that $h$ is non-negative, whence by scaling of $h,c$ we
obtain \WLOG\ that $h\InN\,[0,1]^N\!$. Assume
for a contradiction that $h_n<0$. Choose scalar $d\geq0$ large enough
so that the point\linebreak $b':=(b_1, \cdots, b_n\MinusN d, \cdots, b_N)$
falsifies $h\Dot b' < c$; since $b'$ is still in $B'$, however, that
contradicts the separation. Thus we continue

\begin{Reason}
\StepR{$\Equiv$}{above comments concerning $d$}{
 \begin{array}[t]{@{}l}
  \exists h\InN\,[0,1]^N, c\InN \Real : \\
  \quad \forall a\InN A, b'\InN B' : \\
  \quad\quad h\Dot b' < c < h\Dot a ~,
 \end{array}
}
\Space
\StepR{$\Equiv$}{set $b'$ to $b$; note $b\InN B'$}{
  \exists h\InN\,[0,1]^N,c\InN\Real : \forall a\InN A : h\Dot b  < c < h\Dot a
}
\StepR{$\Implies$}{defn.~$(\SmythHN{h})$; properties of $\Inf$}{
  \exists h\InN\,[0,1]^N, c\InN\Real : h\Dot b  <  c \leq \SmythHN{h}{A}
}
\StepR{$\Implies$}{$b\InN B$, hence $\SmythHN{h}{B} \leq h\Dot b$}{
  \exists h\InN\,[0,1]^N, c\InN\Real : \SmythHN{h}{B}  <  c \leq \SmythHN{h}{A}
}
\StepR{$\Equiv$}{defn.~$\Smust{h}$}{
  \exists h\InN\,[0,1]^N : A \not\Smust{h} B
}
\StepR{$\Equiv$}{defn.~$\Smust{N}$}{
  A \not\Smust{N} B ~.
}
\end{Reason}
\parshape=0
The proof for the Hoare-case is analogous. \EndMath
\end{proof}
\end{Theorem}

\section{Reward Testing of Automata}\label{s1111}

We now combine Secs.~\ref{s1507} and~\ref{s1508} by introducing
preorders that use testing processes and rewards together: we define
\[
 \begin{array}{r@{\hspace{2em}}c@{\hspace{2em}}l}
  \eM_1 \SbothA{N} \eM_2 &\textrm{iff}& \forall\, \eT\InN\MT_N :
   \AllWWK.(\eM_1\ParN \eT) \Sboth{N} \AllWWK.(\eM_2\ParN \eT) ~.  \end{array}
\]
We call the $\SbothA{N}$ relations ---and $\SbothA{\AllFin},\,\SbothA{\Nat}$ similarly--- the \emph{reward-testing} preorders for automata.
When $N\EqN1$ this definition of $\SbothA{1}$ is just scalar testing again (from \Sec{s1207}) as, in this case, the reward ``vectors'' are just scalars themselves: thus the notations do not clash.
%
The following is an immediate corollary of \Thm{t:geo}.
\begin{Corollary}\label{c:reward}
If $\eM_1$ and $\eM_2$ are automata with the property that for any 
test $\eT \InN\MT_\AllFin$ the sets $\AllWWK.(\eM_1\ParN \eT)$ and
$\AllWWK.(\eM_2\ParN \eT)$ are \PClosed,
then finite-dimensional vector-based testing is equivalent to
reward testing: from \Thm{t:geo} we have
\[
 \eM_1\SbothA{\MT_{N}} \eM_2 \Wide{\textrm{iff}} \eM_1\SbothA{N} \eM_2 \textrm{\hspace{3em} for all $N$},
\]
which in turn implies that $\eM_1\SbothA{\MT_\AllFin} \eM_2$ iff $\eM_1\SbothA{\AllFin} \eM_2$.
\hfill\EndMath
\end{Corollary}

\section{Closure Suffices for Scalar Testing}\label{s1632}

We now show that scalar testing is equally powerful as
finite-dimensional reward
testing which, with \Cor{c:reward}, implies that
\PClosure\ of the generated tuple-sets $\AllWWK.(\eM\ParN \eT)$ is a sufficient
condition for scalar testing to be as powerful as finite-dimensional vector-based
testing.  In doing so, we assume that tests are $\W$-terminal in the
sense that they halt after execution of any success action.%
\footnote{\label{f0958}This assumption is justified in \App{a1210}.}

\begin{Theorem}\label{t:equivtest}
For automata $\eM_1$ and $\eM_2$
we have that $\eM_1\SbothA{\AllFin} \eM_2$ iff $\eM_1\SbothA{\Scalar} \eM_2$.
\begin{proof}
The \emph{only-if} is trivial in both cases. For \emph{if} we prove the must-case in the contrapositive;
the may-case is similar.

\JPGinText{-11em}{18em}{0.4}{scalar1322a}
Suppose thus that $\eM_1\not\SmustA{N} \eM_2$, \IE\ that
$\eM_1,\eM_2$ are must-distinguished
by some test $\eT\InN\MT_N$ and reward $h\in[0,1]^N$, so that
\begin{equation}\label{e1354}
 \AllWWK.(\eM_1\ParN \eT) ~~\not\Smust{h}~~ \AllWWK.(\eM_2\ParN \eT)\;.
\end{equation}

\parshape=1 0pt 0.5\textwidth% Narrow paragraphs until further notice (because inside list).
Assuming \WLOG\ that the success actions are $\W_1,\cdots,\W_N$ we construct an automaton $\eU$ such that
\begin{Itemize}
\item The state space is $\{u_0,\cdots,u_N\}$ and $u$,
\item The actions are $\W_1,\cdots\W_N$ and $\W$, all external,
\item The initial distribution $\StartU$ is $\Dirac{u_0}$ and
\item The transitions for $1\leq i\leq N$ take $u_0$ via action $\W_i$ to $(\Dirac{u_i}\PC{h_i}\Dirac{u})$, thence each $u_i$ via $\W$ to deadlock at $\Dirac{u}$. 
\end{Itemize}
%
\parshape=0% Back to normal paragraphs.
We now consider the test $\eT\ParN \eU$ with $\omega$ as its only success action.
In $\eT\ParN \eU$ an occurrence of $\W_i$ is with probability $h_i$
followed immediately by an occurrence of $\W$ (and with probability
$1\MinusN h_i$ by deadlock); and the overall probability of $\W$'s occurrence, in any
resolution of $\eM_{1,2}\ParN \eT \ParN \eU$, is therefore the $h$-weighted
reward $h\Dot \WW$ for the tuple $\WW\Defs(\WW_1,\cdots,\WW_N)$ in the
corresponding resolution of $\eM_{1,2}\ParN \eT$.

Thus from \Eqn{e1354} we have that $\eM_1,\eM_2$ can be distinguished using the scalar test
$\eT \ParN \eU$ with its single success action $\W$; that is, we achieve
$\eM_1 \not\SmustA{\Scalar} \eM_2$ as required.
\EndMath
\end{proof}
\end{Theorem}

\section{Very Finite Testing is \PClosed, hence Scalar}\label{s1006}

Say that an automaton is \emph{very finite} if it is finite-state,
finitely branching and loop-free (no execution sequence repeats a state), so that
there is a finite upper bound on the length of its execution sequences.

In \Thm{t1709} below we show that scalar outcomes suffice when
  dealing with very finite automata and tests, because the sets of success
  tuples are \PClosed\ and thus \Thm{t:equivtest} applies. We rely on
  the fact that when a test $\eT$ is very finite, so are the composite
  automata $\eT\ParN \eU$ and $\eT\ParN \eV$ constructed in
  \Sec{s1632} and \App{a1210}.

\begin{Lemma}\label{l1203}
Let $W_{1,\cdots, N} \mathop\subseteq \AllWW$ be \PClosed\ success-tuple sets,
and let $\mu\InN \Dist{\{1,\!\cdots\!, N\}\hspace{-1.05557pt}}$ be a discrete distribution
over their indices. Then we have
\footnote{Here we are taking the expected value of vectors: recall Footnote~\ref{n1426}.}
\begin{enumerate}
\item\label{i1213-1} The set $\SetST{\mu.f}{f\in\{1,\!\cdots,\! N\}\Fun\AllWW ~\land~ \forall i : f.i \InN W_i}$ is \PClosed, and
\item\label{i1213-2} The set $\bigcup_{\mu\in\Dist{\{1,\!\cdots\!,
    N\}}}~\SetST{\mu.f}{f\in \{1,\!\cdots\!, N\}\Fun\AllWW ~\land~ \forall i : f.i \InN W_i}$ is \PClosed.%
\end{enumerate}
That is, a specific interpolation $\mu$ of \PClosed\ sets is again
\PClosed\ \Eqn{i1213-1}, and the union of \emph{all} such
interpolations is also \PClosed\ \Eqn{i1213-2}.
\begin{proof} Standard results on convex hulls of  compact sets
\cite[Sec.~5.3]{AB99}.
 \EndMath
\end{proof}
\end{Lemma}

\begin{Lemma}\label{l:closed}
If $\eM$ and $\eT$ are very finite automata, then the set
$\AllWWK.(\eM \ParN \eT)$ of success tuples  is \PClosed.
% \begin{proof}
% Let $\eM\ParN \eT$ be $\eA=(A,\StartA,E,I,\CT)$, and note that it is
% very finite also; thus we can prove \PClosure\ of $\AllWWK.\eA$ by
% induction on its execution depth. We work with tuple-functions $g\in
% A\Fun\Pow\AllWW$ that give for any starting state $a\InN A$ the set of
% success tuples $\eA$ generates from there; we show that $g.a$ is
% \PClosed\ for all $a$.
% 
% If $A$ is zero-depth, then its tuple-function satisfies $g.a = \Set{\Zero}$ for all states $a$.
% 
% If $A$ is depth $K\PlusN1$ then its tuple-function is determined by its first transitions, and the tuple-functions of its depth-$K$ immediate children, as follows.
% 
% Fix $a$ and consider $\{\mu\}\Defs \CTK.a.\ActA$ for some action $\ActA$ in $A$; by induction, each $a'\in\Supp{\mu}$ defines a \PClosed\ set $g.a'$ of success tuples; by Lem.~\ref{l1203}(\ref{i1213-1}) the $\mu$-wise interpolation of all those sets is again \PClosed; call it $\GPK.a.\ActA$, the set of success tuples arising after action $\ActA$ at $a$ but not yet taking $\ActA$ itself into account.
% 
% Now if $\ActA$ is in fact some success action $\W_i$, set the $i$-component of all tuples in $\GPK.a.\ActA$ to one; otherwise, leave them unchanged. Call the result $\Occurs{\ActA}{(\GPK.a.\ActA)}$; it is trivially still \PClosed.
% Finally take all interpolations over $\ActA$'s of $\Occurs{\ActA}{(\GPK.a.\ActA)}$, giving the set $g.a$ of success tuples arising from state $a$; by Lem.~\ref{l1203}(\ref{i1213-2}) it too is \PClosed.
% 
% Since $\AllWWK.A$ is the $\StartA$-wise interpolation of sets $g.a$ for $a\in\Supp{\StartA}$, by Lem.~\ref{l1203}(\ref{i1213-1}) again it is \PClosed. \EndMath
%\end{proof}
\begin{proof}(Sketch) \Lem{l1203} shows that \PClosure\ is preserved in a fairly straightforward induction on the upper bound of the length of the execution sequences of the very
finite automata $\eM\ParN\eT$. The details are omitted here, because \Thm{t2146} subsumes \Thm{t1709} anyway.
\EndMath
\end{proof}
\end{Lemma}

\begin{Theorem}\label{t1709} For very finite tests and automata, scalar testing suffices: we have
\[
 \eM_1\SbothA{\MT_\Nat} \eM_2 \Wide{\textrm{iff}} \eM_1\SbothA{1} \eM_2 ~.
\]
\begin{proof}
Any very finite test has only finitely many success actions, and thus
belongs to $\MT_\AllFin$. Consequently, we have
$\eM_1\SbothA{\MT_{\Nat}} \eM_2$ iff $\eM_1\SbothA{\MT_\AllFin} \eM_2$.
Using this, the result follows from
\Lem{l:closed}, \Cor{c:reward} and \Thm{t:equivtest}.
\EndMath
\end{proof}
\end{Theorem}

\section{Also Finitary Testing is Scalar}\label{s1520}

We now remove the no-looping restriction of \Sec{s1006}, retaining however that the automata are finite-branching and have finitely many states:%
\footnote{Having finitely many states and transitions is an equivalent restriction. Finitely many states does not on its own imply finite branching, however: there are infinitely many distributions possible over even a finite state space.}
%
this allows their execution sequences to become of infinite length. Such automata we call
\emph{finitary}.
% As in \Sec{s1632} we assume that tests are $\omega$-terminal.

The result depends on a connection with Markov Decision Processes
(\MDP's) \cite{Put94}, abstracted here as a lemma implicitly using
the more general probability measures mentioned in \Def{probabilities
  of cones} (Footnote~\ref{n1802}).

\begin{Lemma}\label{l1246} \emph{Static resolutions suffice for finitary testing}\quad
Say that a resolution $\eR$ of an automaton $\eM$ is \emph{static} if
its associated resolving function $f\in R\Fun M$ is injective,
so that on every visit to a state $m\InN M$ any nondeterminism is
resolved in the same way, and does not interpolate. Then,  for all
reward tuples $h\in [0,1]^N\!$,
\begin{Itemize} 
\item There is a static resolution $\eR_h$ of $\eM$ so that $\SmythHN {h}{(\AllWWK.\eM)} = \SmythHN{h}{(\AllWWK.\eR_h)}$ and 
\item There is a static resolution $\eR'_h$ of $\eM$ so that $\HoareHN{h}{(\AllWWK.\eM)} = \HoareHN{h}{(\AllWWK.\eR'_h)}$.
\end{Itemize}
Thus in both cases the extremum over all resolutions is attained statically.%
\footnote{More general work on games \cite{GPatQMCQ} led us to this; a
  similar result is argued directly by Philippou, Lee \& Sokolsky \cite{WBfPS} and Cattani and Segala \cite{CS02}, in both cases in the context of decision procedures for bisimulation.}
\begin{proof}
An automaton $\eM = (M,\StartM,E,I,\CT)$ with a reward tuple
\Plat{$h\InN\,[0,1]^{\Nat^+}$} constitutes isomorphically an \MDP\ \cite[Sec.~2.1]{Put94}:
in the tuple at the end of Sec.~2.1.3 take $T:=\Nat^+$, $S := M$,
$A_s := \CTK.s$ for $s \InN S$, $p_t(\cdot|s,(\alpha,\mu)):=\mu$ and
$r_t(s,(\alpha,\mu)) := h_i$ if $\alpha=\omega_i$, or $0$ if $\alpha\mathop{\not\in}\Omega$.
The values of $p$ and $r$ are independent of $t$ and $s$.
Our resolutions are the (history-dependent, randomised) policies of
Sec.~2.1.5, and
our Smyth- and Hoare-outcomes (\Def{l1023}) are the optimal outcomes
accruing from such policies [Secs.~2.1.6, 4.1 and 5.2]; the
Smyth-case is obtained by using negative rewards so that ``optimal'' is supremum either way.

Theorem~7.1.9 [Sec.~7.1.4] states (paraphrased) \emph{Suppose that the state space and
the set of actions available at each state are finite. Then there is a stationary
deterministic optimal policy}. ``Stationary deterministic'' equates to ``static'' in our setting, and ``optimal'' means ``attains the extremum''\Point\EndMath
\end{proof}
\end{Lemma}
%
The crucial lever that \Lem{l1246} gives us in our treatment of testing is that a finitary automaton has only finitely many static resolutions (up to isomorphism), since neither variation-by-visit nor interpolation is allowed for them. With infinitely many resolutions in general, even for the finitary case, needing only finitely many is  a significant advantage --- as we now see in the following lemmas.

\begin{Lemma}\label{l1220} Let $\AllWWFK.\eM$ be the convex closure of the statically generated success tuples of $\eM$; then $\AllWWFK.\eM \subseteq \AllWWK.\eM$. If $\eM$ is finitary, then $\AllWWFK.\eM$ is \PClosed.
\begin{proof}  The first statement is trivial, since static resolutions are still resolutions and from \Lem{l1032} we know that $\AllWWK.\eM$ is convex. For the second we note that as $\eM$ has  only finitely many static resolutions, the set $\AllWWFK.\eM$ is the convex-closure of a finite number of points, and is thus  \PClosed\ by \Lem{l1203}(2). \EndMath
\end{proof}
\end{Lemma}

\begin{Lemma}\label{l1257} For all finitary automata $\eM$ with $N$ success actions, and reward tuples $h\in[0,1]^N\kern -.2em$, we have
\[
  \SmythHN{h}{{(\AllWWK.\eM)}} = \SmythHN{h}{{(\AllWWFK.\eM)}}
  \textrm{\quad\quad and \quad\quad}
  \HoareHN{h}{{(\AllWWK.\eM)}} = \HoareHN{h}{{(\AllWWFK.\eM)}}\,,
\]
hence $\AllWWK.\eM$ and $\AllWWFK.\eM$ are equivalent under $\Sboth{N}$.
\begin{proof}
The $\leq$-case for Smyth is immediate from \Lem{l1220}; from \Lem{l1246} there is some static resolution $\eR_h$ of $\eM$ with $\SmythHN{h}{(\AllWWK.\eM)} = \SmythHN{h}{(\AllWWK.\eR_h)} \geq \SmythHN{h}{(\AllWWFK.\eM)}$.

The Hoare-case is similar; the equivalence then follows from \Def{l1023}. \EndMath
\end{proof}
\end{Lemma}
%
Lemmas~\ref{l1220} and~\ref{l1257} allow us to strengthen
  \Cor{c:reward}, effectively requiring \PClosure\ only of
  $\AllWWFK.(\eM_{1,2}\ParN \eT)$ rather than of
  $\AllWWK.(\eM_{1,2}\ParN \eT)$.

\begin{Lemma}\label{l:equivtestA}
For finitary automata $\eM_1,\eM_2$ we have
$\eM_1\SbothA{\MT_\AllFin} \eM_2$ iff $\eM_1\SbothA{\AllFin} \eM_2$~.
\begin{proof} 
For ``only-if'' apply \Thm{t:geo} --- this direction does not require $p$-closure.
For \emph{if} we prove the must-case in the contrapositive;
the may-case is similar.
\begin{Reason}
\StepR{}{for some $N$}{\eM_1\not\SmustA{\MT_{N}} \eM_2}
\StepR{$\Equiv$}{\Def{d:multi-testing}, for some $\eT\in \MT_N$}{
\AllWWK.(\eM_1\ParN \eT) \not\LeqS \AllWWK.(\eM_2\ParN \eT)
}
\StepR{$\Implies$}{\Lem{l1220}, $\AllWWFK.(\eM_1\ParN \eT)\subseteq\AllWWK.(\eM_1\ParN \eT)$}{
\AllWWFK.(\eM_1\ParN \eT) \not\LeqS \AllWWK.(\eM_2\ParN \eT)
}
\StepR{$\Equiv$}{\Lem{l1220}, $\AllWWFK.(\eM_1\ParN \eT)$ is \PClosed; \Thm{t:geo}}{
\AllWWFK.(\eM_1\ParN \eT) \not\Smust{N} \AllWWK.(\eM_2\ParN \eT)
}
\StepR{$\Equiv$}{\Lem{l1257}}{
\AllWWK.(\eM_1\ParN \eT) \not\Smust{N} \AllWWK.(\eM_2\ParN \eT)
}
\StepR{$\Implies$}{Definition of reward testing.\HangRight{~~\EndMathSym}}{
\eM_1\not\SmustA{N} \eM_2~.
}
\end{Reason}
\vspace{-1em}
\end{proof}
\end{Lemma}
We can now establish the extension of \Thm{t1709} to finitary automata.

\begin{Theorem}\label{t2146}
For finitary tests and automata, scalar testing suffices.
\begin{proof}
As in the proof of \Thm{t1709} we observe that
$\eM_1\SbothA{\MT_{\Nat}} \eM_2$ iff $\eM_1\SbothA{\MT_\AllFin} \eM_2$
  for (this time) finitary tests; we then apply
\Lem{l:equivtestA} and \Thm{t:equivtest}.
\EndMath
\end{proof}
\vspace{-1em}
\end{Theorem}

\section{Beyond Finitary Testing}

The principal technical ingredient of our results is \PClosure\ of the result sets  in
$\AllWW$, since that is what enables the hyperplane separation. Separation itself is
not inherently finitary, since \Lem{l:sep} extends to countably infinite dimensions
\cite[Lem.~B.5.3 adapted]{ARP}, delivering a hyperplane whose normal is non-zero in only
finitely many dimensions --- just as required for our constructions above (although
automaton V in \App{a1210} needs a slightly different
approach).

It is the \PClosure\ which (currently) depends essentially on finite
dimensions (hence a finite state space). For countably infinite
dimensions, its convexity component must be extended to infinite
interpolations; but that happens automatically provided the sets are
Cauchy closed. And it is again the closure that (within our bounded
space) implies the compactness that separation requires. Thus
Cauchy closure is the crucial property.
\pagebreak[1]

When the automata are finitely branching (up to interpolation), we
believe a direct fixed-point construction of $\AllWWK.M$ (\IE\ not
indirectly via resolutions) gives, via intersection of a
$\supseteq$-chain, a set whose up-closure (\textit{wrt} $\leq$ over
$\AllWW$) is compact. Since must- (\IE\ Smyth) testing is insensitive
to up-closure, that would seem to extend our results
to countably-infinite dimensional must-testing.
%
For the may-testing case the analogous technique would be down-closure; but here, unfortunately, the limit is via union of a $\subseteq$-chain, and closure/compactness is not obviously preserved.
%
As further evidence for this we note
that the \MDP-based results allow countably infinite
state spaces in the infimum case (still however with finite branching)
\cite[Thm.~7.3.6]{Put94}, whereas the supremum case requires a
finite state space.

Thus the key question is \emph{What conditions are necessary to establish \PClosure\ for infinitely many states?} At present, may- seems harder than must-.

\section{Conclusion}

Our reduction of vector- to scalar testing uses geometry (hyperplanes), 
elementary topology (compactness) and game theory (\MDP's); and it highlights 
the importance of \PClosure\ and static resolutions. That those techniques 
contribute to probabilistic semantics is of independent theoretical interest;  
but our result ultimately is \emph{practical} --- any program calculus/algebra, a 
fundamental tool for rigorous software engineering, relies crucially on a tractable 
definition of equality.

A key feature is our use of \emph{expected values of ``rewards''}
as outcomes for probabilistic tests; this approach subsumes the
usual direct probabilities because an event's probability is just the
expected value of its characteristic function.%
\footnote{For $\mu.X$ is the same whether $X$ is taken as a set or as a characteristic function.}
It has been suggested
before both for sequential \cite{aPPDL} and concurrent \cite{TaRfNaPP}
applications; and we believe it deserves greater attention, since it
can lead to significant simplifications (of which this report provides
an example).

We have shown that scalar testing suffices when requiring the
\emph{tests}, as well as their testees, to be finitary, and one may
wonder whether the same holds if arbitrarily complex tests are
allowed. We think this is indeed the case, for we conjecture that if
two finitary automata can be distinguished by an arbitrary test, then
they can be distinguished by a finitary test.

\Deleted{
The approach of \Sec{s1520} requires a finite state space in order to
yield only finitely many static resolutions, and hence a
\PClosed\ set of success tuples. We believe however that for
must-testing the approach of \Sec{s1006} can be extended to
infinite-state finitely branching processes, relying on a
generalisation of \Lem{l:sep} to countably infinite dimensions.}

As stated in \Sec{ProbAutomata:ProbTesting}, Segala's testing framework \cite{Seg96} 
differs from others' \cite{DH84,WL92} not only in the number
of success actions, but also in how to report success.
We claim that action- and state-based testing give
 rise to different must-testing preorders
when the tested processes display divergence,
because a success action $\omega$ may be delayed forever.
Here we used action-based testing throughout, 
although we could have obtained the same results for state-based testing.

Finally, we note that our reduction via Thms.~\ref{t:equivtest}--\ref{t2146} of
vector-based testing to extremal scalar testing has reduction to $\MT_1$-testing as a corollary --- thus showing that, under our assumptions, single success actions suffice for Segala's approach
even if it is otherwise unchanged.

\vspace{-.5em}% Cosmetic.
\section*{Acknowledgements}
We thank Anna Philippou for corresponding with us about static resolutions, and Kim Border
for a hyperplane-related counterexample.

\vspace{-.5em}% Cosmetic.
\bibliographystyle{plain} 
%\bibliography{scalar,probs}
\begin{thebibliography}{10}

\bibitem{AJ94}
{\sc S.~Abramsky \& A.~Jung} (1994):
\newblock {\em Domain theory.}
\newblock In S.~Abramsky, D.M. Gabbay \& T.S.E. Maibaum, editors: {\sl Handbook of Logic and Computer Science}, volume~3, Clarendon Press, pp. 1--168.

\bibitem{AB99}
{\sc C.D. Aliprantis \& K.C. Border} (1999):
\newblock {\em Infinite Dimensional Analysis}.
\newblock Springer, second edition.

\bibitem{CS02}
{\sc S.~Cattani \& R.~Segala} (2002):
\newblock {\em Decision algorithms for probabilistic bisimulation.}
\newblock In {\sl {\rm Proc.} {CONCUR} 2002}, {\sl {\rm LNCS}} 2421, Springer, pp. 371--85.

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

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

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

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

\bibitem{TaRfNaPP}
{\sc B.~Jonsson, C.~Ho-Stuart \& Wang Yi} (1994):
\newblock {\em Testing and refinement for nondeterministic and probabilistic processes.}
\newblock In {\sl {\rm Proc.} Formal Techniques in Real-Time and Fault-Tolerant Systems}, {\sl {\rm LNCS}} 863, Springer, pp. 418--30.

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

\bibitem{aPPDL}
{\sc D.~Kozen} (1985):
\newblock {\em A probabilistic {PDL}.}
\newblock {\sl Jnl.\ Comp.\ Sys.\ Sciences} 30(2), pp. 162--78.

\bibitem{Mat02}
{\sc J.~Matou\v{s}ek} (2002):
\newblock {\em Lectures on Discrete Geometry}.
\newblock Springer.

\bibitem{GPatQMCQ}
{\sc A.K. McIver \& C.C. Morgan} (2002):
\newblock {\em Games, probability and the quantitative $\mu$-calculus \textit{qMu}.}
\newblock In {\sl Proc.~LPAR}, {\sl {\rm LNAI}} 2514, Springer, pp. 292--310.

\bibitem{ARP}
{\sc A.K. McIver \& C.C. Morgan} (2005):
\newblock {\em Abstraction, Refinement and Proof for Probabilistic Systems}.
\newblock Tech.\ Mono.\ Comp.\ Sci., Springer.

\bibitem{PPT}
{\sc C.C. Morgan, A.K. McIver \& K.~Seidel} (1996):
\newblock {\em Probabilistic predicate transformers.}
\newblock {\sl ACM Trans. on Programming Languages and Systems} 18(3), pp. 325--53.

\bibitem{WBfPS}
{\sc A.~Philippou, I.~Lee \& O.~Sokolsky} (2000):
\newblock {\em Weak bisimulation for probabilistic systems.}
\newblock In {\sl {\rm Proc.} {CONCUR} 2000}, Springer, pp. 334--49.

\bibitem{Put94}
{\sc M.L. Puterman} (1994):
\newblock {\em Markov Decision Processes}.
\newblock Wiley.

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

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

\bibitem{aTSfPA}
{\sc M.I.A. Stoelinga \& F.W. Vaandrager} (2003):
\newblock A testing scenario for probabilistic automata.
\newblock In {\sl {\rm Proc.} {ICALP} '03}, LNCS 2719, Springer, pp. 407--18.

\bibitem{Var85}
{\sc M.Y. Vardi} (1985):
\newblock {\em Automatic verification of probabilistic concurrent finite state programs.}
\newblock In {\sl {\rm Proc.} FOCS '85}, IEEE Computer Society Press, pp. 327--38.

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

\end{thebibliography}

\appendix
\section{One Success Never Leads to Another}\label{a1210}

Here we substantiate the claim made in \Sec{s1006} (Footnote~\ref{f0958}) that \WLOG\ we can assume that our testing automata halt
after engaging in any success action. The
reward-testing construction requires this because the automaton $\eU$ used in
\Thm{t:equivtest} implementing a particular reward-tuple $h$
effectively causes the composite automaton $\eT\ParN \eU$ to halt
after the reward is applied --- hence for correctness of the
construction we required that the automaton $\eT$ must have halted
anyway.

  Below we show that the may- and must testing preorders do not change upon
  restricting the class of available tests to those that cannot
  perform multiple success actions in a single run. A second
  reduction to tests that actually halt after performing any success
  action is trivial: just change any transition of the form
  $(s,\omega_i,\mu)$ into a transition $(s,\omega_i,\Dirac{0})$ leading
  to a deadlocked state $0$.

Suppose our original testing automaton $\eT$ has $N$ success actions
$\W_1,\cdots,\W_N$. By running it in parallel with another automaton
$\eV$ (below) we will convert it to
an automaton with the required property and corresponding success actions
  $\W'_1,\cdots,\W'_N$, and with success $N$-tuples that are exactly $1/N$
  times the success tuples of $\eT$;
since testing is insensitive to scaling of the tuples, that will give
us our result. Note that the $1/N$ factor is natural given that we are
making our $N$ success actions mutually exclusive: it ensures the tuple's elements' total does not exceed one.

We construct the automaton $\eV:=(V,\StartV,E,I,\CT)$ as follows:
\begin{Itemize}
\item The state space is $V\Defs \Pow\{\W_1,\ldots,\W_n\} \Union
  (0,\ldots,N)$, where the powerset-states record which success actions
  have already occurred, the scalar states $1,\ldots,N$ are
  ``about-to-terminate'' states, and $0$ is a deadlock state;
\item The actions are $\W_1,\ldots,\W_N$ and $\W'_1,\ldots,\W'_N$, all external; and
\item The initial distribution $\StartV$ is the Dirac'd powerset-state $\Dirac{\emptyset}$.
\end{Itemize}
%
The transitions of $\eV$ are of three kinds:
\begin{Itemize}
\item ``Terminating'' transitions take state $n$ with probability one via action $\W'_n$ to the deadlocked state $0$;
\item {``Do-nothing'' transitions, from state
  $v\InN\Pow\{\W_1,\cdots,\W_N\}$, lead with probability one via action
  $\W_n\InN v$ back to $v$,  implementing that second and subsequent
  occurrences of any success action in $\eT$ can be ignored; and}
\item\JPGinText{-7.3em}{11.4em}{0.4}{scalar1303a}
\parbox[t]{\textwidth}{%
\parshape=8 0pt .34\textwidth 0pt .3\textwidth 0pt .3\textwidth 0pt .3\textwidth 0pt .3\textwidth 0pt .3\textwidth 0pt .3\textwidth 0pt .94\textwidth
%
``Success'' transitions, from state $v\InN\Pow\{\W_1,\cdots,\W_N\}$
lead via action $\W_n\mathop{\not\in} v$ with probability
$\frac{1}{N\MinusN\#v}$ to state $n$, whence the subsequent terminating transition will
emit $\W'_n$; the remaining probability at $v$ leads to state
$v\Union\{\W_n\}$, recording silently that $\W_n$ has now been taken
care of.}
\end{Itemize}
When the original test $\eT$ has finitely many states and
transitions, so does the composite test $\eT\ParN \eV$.

\end{document}
