text:
\section{Introduction}\label{sec:introduction}

A central paradigm behind process semantics based on observability
(e.g. \cite{csp}) is that the exact moment of occurring of an
internal nondeterministic choice is unobservable. This is because an
observer does not have insight into the internal structure of a
process but only in the externally visible actions. Unobservability
of  internal choice has been also accomplished by the testing theory
\cite{DH84}\footnote{In fact, the process semantics based on
\cite{csp} and \cite{DH84} do coincide for a broad class of
processes, as shown in \cite{D87}.}. It is natural, therefore, for
this property to hold when the internal choice is quantified with
probabilities. However, it turned out that unobservability of
internal probabilistic choice is not trivial to achieve in
probabilistic testing theory. To explain why, we start with an
example.

\paragraph{Motivation}Consider a machine which flips a fair coin
internally. A user can guess the result of the flipping by pressing
a ``head'' or a ``tail'' button.
 If the user has guessed correctly, the
machine offers a prize. The machine can be modeled by process graph
(or shortly process) $s$ in Fig. \ref{fig_machine}  and the user can
be modeled by process $u$ in Fig. \ref{fig_machine}. The user is
happy if, after pressing a button, a prize follows.

Let the user and the machine interact, i.e. let them synchronize on
all actions (except on the ``user happiness'' reporting action
$\ddot\smile$). In terms of testing theory \cite{DH84},   process $s$ is
tested with test $u$.
 Intuitively, the probability that the user has guessed the
 output of flipping  is $\frac{1}{2}$. That is, the probability of a
 $\ddot\smile$ action being reported is $\frac{1}{2}$. However,  most
  of the existing approaches for probabilistic testing, in particular probabilistic may/must testing
   \cite{YL92,JY02,segala_testing96,DGHM08, PNM07},
   do not give this answer.
Consider the synchronization $s \parallel u$ represented by the graph in
Fig. \ref{fig_machine}, where actions are hidden after they have
synchronized.  In order to compute the probability of $\ddot\smile$
being reported, the approaches in
\cite{YL92,JY02,segala_testing96,DGHM08, PNM07} use
\emph{schedulers}, that have insight into the internal structure of
the graph of the synchronized system. Each scheduler resolves the
nondeterminism in the nondeterministic nodes of $s \parallel u$ and
yields a fully probabilistic system. For $s \mathrel{\parallel} u$ in
Fig. \ref{fig_machine}, there are four possible schedulers, which
yield the following set of probabilities with which $s$ passes the
test $u$: $\{0, \frac{1}{2}, 1\}$. We can see that, because the
power of the schedulers is unrestricted, unrealistic upper and lower
bounds for the probabilities are obtained. Observe that this happens
due to the effect of ``cloning'' the nondeterminism after hiding the
synchronized actions. The choice between $h$ and $t$ has been
``cloned'' in both futures after the probabilistic choice in $s \parallel
u$. When resolving nondeterminism in $s \parallel u$, a scheduler assumes
that the user has unrealistic power to \emph{see} the result of the
coin-flipping \emph{before} guessing.

 The above example challenges us to reconsider the design choice to hide
actions after synchronization. Namely, although hiding is harmless
and actually useful in \cite{DH84}, and helps to abstract away from
unnecessary information, in probabilistic testing  it may actually
``hide too much'' and produce overestimation of the probability
information about the system. It is highly undesirable to obtain
lower and upper probability bounds of $0$ and $1$ resp. for the
probabilistic behaviour of a simple system (as the one in Fig.
\ref{fig_machine}), when the actual probability is $\frac{1}{2}$.
This may render a testing equivalence insufficient for verification
purposes.

\begin{figure}[t]\centering
\large
$\xymatrix@R=0.3cm@C=0.05cm{
    & & & s \\
    & & & \circ  \ar@{-->}[dll]_{\frac{1}{2}} \ar@{-->}[drr]^{\frac{1}{2}} \\
& \circ \ar[dl]_{h} \ar[dr]^{t} & & & & \circ  \ar[dl]_{h} \ar[dr]^{t} \\
          \circ \ar[d]^{p}  && \circ   & & \circ&& \circ\ar[d]_{p} \\
           \circ &&  & &  && \circ  \\
           }$

$\xymatrix@R=0.3cm@C=0.05cm{ u \\
   \circ \ar@/_/[d]_{h} \ar@/^/[d]^{t} \\
          \circ \ar[d]_{p} \\
           \circ\ar[d]_{\ddot\smile} \\
            \circ \\
           }$

           $\xymatrix@R=0.3cm@C=0.05cm{
&& s \parallel u \\
     & & \circ  \ar@{-->}[dl]_{\frac{1}{2}} \ar@{-->}[drr]^{\frac{1}{2}} \\
& \circ \ar[dl]_{\tau} \ar[dr]^{\tau} & &  & \circ  \ar[dl]_{\tau} \ar[dr]^{\tau} \\
          \circ \ar[d]_{\tau}  && \circ   &  \circ&& \circ\ar[d]_{\tau} \\
           \circ\ar[d]_{\ddot\smile} &&  & &  & \circ\ar[d]_{\ddot\smile}  \\
           \circ &&  & &  & \circ  \\
           }$
         $\xymatrix@R=0.3cm@C=0.05cm{
         & & & \bar{s} \\
    & & & \circ  \ar[dll]_{h} \ar[drr]^{t} \\
& \circ \ar@{-->}[dl]_{\frac{1}{2}} \ar@{-->}[dr]^{\frac{1}{2}} & & & & \circ  \ar@{-->}[dl]_{\frac{1}{2}} \ar@{-->}[dr]^{\frac{1}{2}} \\
          \circ\ar[d]^{p}  && \circ  & & \circ&& \circ\ar[d]_{p} \\
          \circ &&  & &  && \circ
           }$
 \caption{\small Processes $s$ and $\bar{s}$ are distinguished in  probabilistic may/must testing theory
 \hbox{}\vspace{-1cm}
 \label{fig_machine}
\end{figure}

 Consider now  process
$\bar{s}$ in Fig. \ref{fig_machine}. To the user this graph may as
well represent the behaviour of the coin-flipping machine -- the
user cannot see whether the machine flips the coin \emph{before} or
\emph{after} making the ``head or tail'' guess. According to her,
the machine acts as specified as long as she is able to guess the
result in half of the cases. In fact, both schedulers applied to
$\bar{s} \parallel u$  yield  that the probability of reporting a
$\ddot\smile$ action is exactly $\frac{1}{2}$. Because of the last, none
of the approaches in \cite{YL92,JY02,segala_testing96,DGHM08,PNM07}
equate processes $s$ and $\bar{s}$, as, when tested with $u$, they
produce different bounds for the probabilities of reporting
$\ddot\smile$.
 \footnote{If we ignore
the probabilities, processes $s$ and $\bar{s}$ are
testing-equivalent by \cite{DH84}.} Note that being able to equate
$s$ and $\bar{s}$ means allowing distribution of external choice
over internal probabilistic choice \cite{csp}

Not allowing distribution of external choice over internal
probabilistic choice has an additional effect, undesirable for
compositional verification. Namely,
 if distribution of external choice over
internal probabilistic choice is not allowed, then distribution of
prefix over internal probabilistic choice  is questioned too, as
this implies congruence issues for \emph{asynchronous} or
\emph{concurrent} parallel composition \cite{csp} (where processes
synchronize on their common actions while  interleave on the other
actions). For instance, we would not be able to equate processes
$e.a. (b \oplus_{\frac{1}{2}}c)$ and $e.((a.b)
\oplus_{\frac{1}{2}}(a.c))$. (The operator ``.'' stands for
prefixing and the operator ``$\oplus$'' stands for a probabilistic
choice.) This  is because these two processes, running each
concurrently with process $e.d$, yield systems that cannot be
equated, unless we allow distribution of external choice over
internal probabilistic choice. If we are not able to relate
processes $e.a. (b \oplus_{\frac{1}{2}}c)$ and $e.((a.b)
\oplus_{\frac{1}{2}}(a.c))$, i.e. to allow distribution of prefix
over internal probabilistic choice, then for verification
 we can only rely on equivalences that inspect the internal
structure of processes, as bisimulations and simulations
\cite{spectrum1}, and, moreover, expect overestimation of
probabilities.

All together, the above discussions trigger the following question:
``In a model where the internal nondeterminism has been quantified
with probabilities \cite{LS91}, is it possible to test  process $s$
with
 test $u$ (Fig. \ref{fig_machine}) such that the result of
testing would imply that the probability of $s$ passing the test $u$
is exactly $\frac{1}{2}$?''. In this case not only  we could
preserve the information on  probability, but  we could also allow
distribution of  prefix  over  probabilistic choice without losing
compositionality.

\paragraph{Contributions} In this paper we show that the answer to
the above question is positive. The main contributions of the paper
are the following:
\begin{itemize}

\item We introduce a technique for labeling the synchronized actions
when a reactive probabilistic process is tested
(Section~\ref{sec:testing}). The labels are in form of rational
functions, whose argument names are constructed from the action
labels set. The labeling is achieved automatically when processes
synchronize, i.e. no additional manipulation on the process graphs
is needed.

\item We propose a testing semantics (Section~\ref{sec:testing}) exploiting the new labeling method,
such that the result of testing process $s$ with test $u$ in Fig.
\ref{fig_machine} is $\frac{1}{2}$, and processes $s$ and $\bar{s}$
in Fig. \ref{fig_machine} are testing-equivalent.

\item We define a probabilistic ready trace equivalence  for reactive
probabilistic processes using the Bayesian definition of probability
(Section~\ref{sec:barbed}). The definition allows a testing scenario
in the lines of \cite{spectrum1, CSV07} to be easily constructed.

\item We define an algebra of finite processes  and show that the ready trace equivalence is congruence for the standard operators (Section~\ref{sec:algebra}).

\item We show that  all operators of our algebra, including external choice, distribute over probabilistic choice, allowing us to consider the latter one as unobservable (Section~\ref{sec:algebra}).
\item We  show that the testing equivalence of Sec. \ref{sec:testing} and the ready-trace equivalence of Sec. \ref{sec:barbed} coincide
(Section~\ref{sec:relationship}).
\end{itemize}

Section \ref{sec:conclusion} ends with concluding remarks, future
work directions regarding coexistence of probabilistic and internal
choice, and related work.

 \begin{SHORTVERSION} An extended version
of this paper, containing the proofs of the main results, can be
found in the report \cite{testing_report}.\end{SHORTVERSION}

\section{Preliminaries}\label{sec:prelim}
We define some preliminary notions needed for the rest of the paper.
\paragraph{Bayesian probability} For a set $A$, $2^A$ denotes its power-set.
The following definitions are taken from~\cite{lindley}.

We consider a sample space, $\Omega$, consisting of points called
\emph{elementary events}. Selection of a particular $a \in \Omega$
is referred to as an ``$a$ has occurred''. An \emph{event} is a set
of elementary events. $A, B, C, \ldots$ range over events. An event
$A$ \emph{has occurred} iff  for some  $a \in A$ $a$ has occurred.
Let $A_1, A_2, \ldots$ be a sequence of events and $C$ be an event.
The members of the sequence are \emph{exclusive given C}, if
whenever $C$ has occurred no two of them can occur together, that
is, if $A_i \cap A_j \cap C=\emptyset$ whenever $i\not = j$. $C$ is
called a \emph{conditioning} event. If the conditioning event is
$\Omega$,
then ``given $\Omega$'' is  omitted.

 For certain pairs of events $A$ and $B$, a real number $P(A|B)$ is
 defined and called the \emph{probability} of $A$ given $B$. These
 numbers satisfy the following axioms:

 \begin{enumerate}
 \item[A1:] $0 \leq P(A|B)\leq1$ and $P(A|A)=1$.
 \item[A2:]  If the events in $\{A_i\}_{i=1}^{\infty}$ are
 exclusive given $B$, then  $P(\cup_{i=1}^{\infty}
 A_i\ |\ B)=\sum_{i=1}^{\infty}P(A_i | B).$
 \item[A3:]  $P(C|A \cap B)\cdot P(A|B)=P(A \cap C|B)$.
 \end{enumerate}
For $P(A|\Omega)$ we simply write $P(A)$.

 \paragraph{Probabilistic transition systems} In a probabilistic transition system (PTS)  there are two types of  transitions,
 viz. action and probabilistic transitions;
 a state can either perform action transitions only
(nondeterministic state) or (unobservable) probabilistic transitions
only (probabilistic state). To simplify, we assume that
probabilistic transitions lead to nondeterministic states. The
nondeterministic states exhibit only a so-called \emph{external}
(observable) nondeterminism, i.e the choice is between the actions,
but once the action is chosen, the next  state is determined. The
outgoing transitions of a probabilistic state $s$ define probability
over the power-set of the set of nondeterministic states.

We give a formal definition of a PTS. Presuppose a finite set of
actions $\mathcal{A}$.

\begin{definition}[Probabilistic Transition System (PTS)]
\label{def:PTS} A \emph{PTS} is a tuple $\mathcal{P}=(S_n, S_p, \mathalpha{\rightarrow}, \mathalpha{\dashrightarrow})$, where
\begin{itemize}
\item $S_n$ and $S_p$
are finite disjoint sets of \emph{nondeterministic} and
\emph{probabilistic states}, resp.,
\item $\mathalpha{\rightarrow}\subseteq
S_n \times \mathcal{A} \times S_n \cup S_p$ is an
\emph{action transition relation} such that $(s,a,t) \in \mathalpha{\rightarrow}$
and $(s,a,t') \in \mathalpha{\rightarrow}$ implies $t=t'$, and
\item $\mathalpha{\dashrightarrow} \subseteq
S_p \times (0,1] \times S_n$ is a \emph{probabilistic
transition relation} such that, for all $s \in S_p$,
$\sum_{(s,\pi,t)\in \mathalpha{\dashrightarrow}}\pi =1$

\end{itemize}
\end{definition}

\noindent We denote $S_n \cup S_p$ by $S$. We write
$s \atran{a} t$ rather than $(s,a,t) \in \mathalpha{\rightarrow}$, and $s
\ptran{\pi} t$  rather than $(s,\pi,t)\in \mathalpha{\dashrightarrow}$ (or $s \ptran{}
t$ if the value of $\pi$ is irrelevant in the context).  We write $s
\atran{a}$ to denote that there exists an action transition $s
\atran{a}s'$ for some $s' \in S$. We agree that a state
without outgoing transitions
belongs to $S_n$

As standard, we define a \emph{process graph} (or simply
\emph{process}) to be a state $s \in S$ together with all
states reachable from $s$, and the transitions between them. A
process graph is usually named by its \emph{root} state, in this
case $s$.

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

In this section we define a testing equivalence in the style of
\cite{DH84} for reactive probabilistic
processes.

Recall from elementary mathematics that a division of two
polynomials is called a \emph{rational function}. For example,
$\frac{2x}{x+y}$ is a rational function with  arguments $x$ and $y$.
A possible domain for this function is $(0, \infty) \times (0,
\infty)$. We are going to exploit a subset $\mathcal{R}$ of the
rational functions
 whose argument names
belong to the action labels $\mathcal{A}$, which is generated by the
following grammar:

\[\varphi::=\alpha  \ \mid \   a \ \mid \ \varphi + \varphi \ \mid \
\varphi \cdot \varphi \ \mid \ \frac{\varphi}{\varphi},\]

\noindent where $\alpha$ is a non-negative scalar, $a \in \mathcal{A}$,
and $+, \ \cdot, \ $ and $ \frac{\cdot}{\cdot}$ are ordinary
algebraic addition, multiplication and fraction, resp. Brackets are
used in the standard way to change the priority of the operators.
For our purposes, we assume that the arguments  $a,b, ...$ can only
take positive values, i.e. the domain of every function in
$\mathcal{R}$ is $(0, \infty)^{n}$, where $n$ is the size of the action
set. Therefore, two rational functions in $\mathcal{R}$ are equal iff
they can be transformed to equal terms using the standard
transformations that preserve equivalence (e.g. for $a,b \in
\mathcal{A}$, $ \frac{1}{2}\cdot \frac{a}{a+b}+\frac{1}{2}\cdot
\frac{b}{a+b}=\frac{1 \cdot (a+b)}{2 \cdot(a+b)}=\frac{1}{2}$).

As standard, a \emph{test} $T$ is a finite process
 such that,
 for a symbol $\omega \not \in \mathcal{A}$, there may exist
transitions $s \atran{\omega} $
 for some  states $s$ of $T$. Denote the set of all tests by $\mathcal{T}$. Given a process $s$ and
action $a \in \mathcal{A}$, denote by $s_a$ the process (if exists) for
which $s \atran{a}s_a$. Given a PTS $\mathcal{P} = (S_n, S_p, \mathalpha{\rightarrow}, \mathalpha{\dashrightarrow})$, let $I\colon
S_n \mapsto 2^\mathcal{A}$ be a function such that, for all $a \in
\mathcal{A}, s \in S_n$, it holds $a \in I(s)$ iff $s \atran{a}$.
$I (s)$ is called the \emph{menu} of $s$. Intuitively, for $s \in
S_n$, $I(s)$ is the set of actions that the process  $s$ can
perform initially. Next, we define the result of testing a process
with a given test. The informal explanation follows afterwards.

\begin{definition}\label{def:Results} The function
$\mathsf{Result} \colon S \times \mathcal{T} \mapsto \mathcal{R}$ that gives
the result of testing a process $s$ with a test $T$ is defined as
follows:

\[
\mathsf{Result}(s,T)=
\begin{cases} {}
1, & \text{if } T \atran{\omega}, \\

\sum_{i \in I}{\pi_i \cdot \mathsf{Result}(s_i , T)}, &  \text{if } s
\pitran{\pi_i}s_i \text{ for } i \in I$ \text{and } $T  \not \atran{\omega} \\

\sum_{i \in I}{\pi_i \cdot \mathsf{Result}(s , T_i)}, &  \text{if } T
\pitran{\pi_i}T_i \text{ for } i \in I$ \text{and } $s  \not \ptran{} \\

\sum_{a \in K} \frac{a}{\sum_{b \in K}{b}} \cdot \mathsf{Result}(s_a , T_a),
& \text{for } K = I(s) \cap I(T),\text{ otherwise}.

\end{cases}
\]
\end{definition}

\noindent As usual, the result of testing a process  with a test
denoting success is one, while the result of testing a process with
a probabilistic state as a root (i.e. initially probabilistic
process) is a weighted sum of the results of testing the subsequent
processes with the same test. Similarly when the test is initially
probabilistic. The novelty is in the result of testing an initially
nondeterministic process $s$ with a test $T$ that can initially
perform actions from $\mathcal{A}$ only. Namely, when the process and
the test synchronize on an action, the resulting transition is
labeled with a ``weighting factor'', containing information about
the way this synchronization happened.
 \begin{wrapfigure}{r}{39mm}
\centering \large \hbox{}\vspace{-1cm}
           $\xymatrix@R=0.3cm@C=0.07cm{
    & & & \circ  \ar@{-->}[dll]_{\frac{1}{2}} \ar@{-->}[drr]^{\frac{1}{2}} \\
& \circ \ar[dl]_{\frac{h}{h+t}} \ar[dr]^{\frac{t}{h+t}} & & & & \circ  \ar[dl]_{\frac{h}{h+t}} \ar[dr]^{\frac{t}{h+t}} \\
          \circ \ar[d]_{\frac{p}{p}}  && \circ   & & \circ&& \circ\ar[d]_{\frac{p}{p}} \\
           \circ\ar[d]_{\ddot\smile} &&  & &  && \circ\ar[d]_{\ddot\smile}  \\
           \circ &&  & &  && \circ  \\
           }$
 \caption{\small Graphical representation of the  result of testing $s$ (Fig. \ref{fig_machine})  with $u$
\hbox{}\vspace{-1cm}
 \label{fig_testing}
\end{wrapfigure}
This information has form of a rational function, the numerator of
which represents the synchronized action itself, while the
denominator is the sum of the common initial actions of $s$ and $T$,
i.e., all actions on which $s$ and $T$ could have synchronized at
the current step. Then, the rational function is temporarily treated
as ``symbolic'' probability, in order to compute the final result of
the testing. The final result is again a rational function in
$\mathcal{R}$.

Fig. \ref{fig_testing} represents graphically the result of testing
process $s$ in Fig. \ref{fig_machine} with the test $u$ from the
same figure. It is easy to compute that the result of testing is
equal to $\frac{1}{2}$, which establishes one of our goals set in
Section \ref{sec:introduction}. However, in many cases the result is
a non-scalar rational function. For example, denote by ``$+$'' the
external choice operator. The result of applying  test $h.p.\omega
+t.\omega$  to each of processes $s$ and $\bar{s}$ in Fig.
\ref{fig_machine} is $\frac{h+2t}{2(h+t)}$.

\begin{definition} \label{def:testing} Two processes $s$ and $\bar{s}$ are \emph{testing
equivalent}, notation $s \mathrel{\approx_{\mathcal{T}}} \bar{s}$, iff $\mathsf{Result}(s,T)$ and
$\mathsf{Result}(\bar{s},T)$ are equal functions for every test $T$.
\end{definition}

\noindent Obviously, comparing two results boils down to comparing
two polynomials, after both rational functions have been transformed
to equal denominators.

\begin{example}Consider the processes in Fig. \ref{fig_notequiv}. The test
$a.\omega + b.c.\omega$ distinguishes between the two processes.
\end{example}
\begin{figure}[t]\centering
\large \hbox{}\vspace{-0.7cm}
     $
    \xymatrix@R=0.3cm@C=0.05cm{
    & & & \circ  \ar@{-->}[dll]_{\frac{1}{2}} \ar@{-->}[drr]^{\frac{1}{2}} \\
& \circ \ar[dl]_{a} \ar[dr]^{b} & & & & \circ  \ar[dl]_{b} \ar[dr]^{e} \\
          \circ  && \circ\ar[d]_{c}  & & \circ\ar[d]_{d} && \circ \\
           && \circ & & \circ &&   \\
           }
           \quad \not \mathrel{\approx_{\mathcal{T}}} \quad
           \xymatrix@R=0.3cm@C=0.05cm{
    & & & \circ  \ar@{-->}[dll]_{\frac{1}{2}} \ar@{-->}[drr]^{\frac{1}{2}} \\
& \circ \ar[dl]_{a} \ar[dr]^{b} & & & & \circ  \ar[dl]_{b} \ar[dr]^{e} \\
          \circ  && \circ\ar[d]_{d}  & & \circ\ar[d]_{c} && \circ \\
           && \circ & & \circ &&   \\
           }$
\newline
\hbox{}\vspace{-0.3cm}
 \caption{Processes $s$ (left) and $\bar{s}$ (right) are not testing equivalent}
 \hbox{}\vspace{-0.7cm}
 \label{fig_notequiv}
\end{figure}
\begin{remark} Def. \ref{def:Results} assumes that, when the process and the
test are ready to synchronize on an action,  the  test can
\emph{see} which actions have been offered from the process. This
corresponds to the user (e.g. $u$ in Fig. \ref{fig_machine}) being
able to see the menu that the machine (e.g. $s$ in Fig.
\ref{fig_machine}) offers. Note that this assumption does not exist
in the standard non-probabilistic testing theory \cite{DH84}.
However, in real-life systems this is usually the case. Moreover,
this assumption is mild with respect to probabilistic may/must
testing approaches, where one needs to know the complete internal
structure of the composed process, which, on the other side, yields
unrealistic over-estimations of probabilities. In contrary, in our
case, in order to compute the function $\mathsf{Result}(s,T)$, it is not
necessary that the probabilistic transitions of $s$ and their labels
are known. Their effect can be inferred
 statistically, by testing $s$ with $T$ sufficiently many times. To
 simplify the presentation, we do not go into details on statistical testing.
\end{remark}

\section{Probabilistic ready trace semantics}\label{sec:barbed}

In this section we define a probabilistic version of ready trace
equivalence~\cite{Pnueli85, BBKready}.

\begin{definition}[Ready trace] A \emph{ready trace of length $n$} is a  sequence
 $\mathcal{O} = (
 M_1, a_1, M_2, a_2, \ldots, M_{n-1}, a_{n-1}, M_n)$ where $M_i \in 2^\mathcal{A}$ for all
$i \in \{1, 2, \ldots , n\}$ and $a_i \in M_i$ for all $i \in
\{1,2, \ldots, n-1\}$ .
\end{definition}

\noindent We assume that  the observer has  ability to observe the
actions that the process performs, together with the menus out of
which actions are chosen. Intuitively, a ready trace $\mathcal{O} = (
 M_1, a_1, M_2, a_2, \ldots, M_{n-1}, a_{n-1}, M_n)$ can be
observed if the initial menu is $M_1$,  then action $a_1 \in
M_1$ is performed, then the next menu is $M_2$,  then action
$a_2 \in M_2$ is performed and so on, until the observing ends
at a point when the  menu is $M_n$. It is essential that, since
the probabilistic transitions are not observable, the observer
cannot infer where exactly they happen in the ready trace.

Clearly the probability of observing a ready trace
$(\{a,b\},a,\{c\})$ is conditioned on choosing the action $a$ from
the menu $\{a,b\}$.
 This suggests that, when
defining probabilities on ready traces, the Bayesian definition of
probability is more appropriate than the measure-theoretic
definition that is usually taken.

Next, given a  process $s$, we define a process $s_{(M, a)}$.
Intuitively, $s_{(M, a)}$ is  the process that $s$ becomes,
assuming that menu $M$ was offered to $s$ and action $a$ was
performed.

\begin{definition}\label{def:pafter}
Let $s$ be a process graph. Let $M \subseteq \mathcal{A}$, $a \in
M$ be such that $I(s)=M$ if $s \in S_n$ or otherwise
there exists a transition $s \ptran{}s'$ such that $I(s')=M$.
The process graph $s_{(M,a)}$ is obtained from $s$ in the
following way:
\begin{itemize} \item if $s \in S_n$ then the root of
$s_{(M,a)}$ is the state $s'$ such that $s \atran{a} s'$, and
\item if $s \in S_p$ then a new state $s_{(M, a)}$ is
created. Let $\pi = $
$\sum_{s\ptran{\pi_i}s_i,I(s_i)=M}{\pi_i}$. For all $s_i'$ such
that $s \ptran{\pi_i}s_i\atran{a}s_i'$ and $I(s_i)=M$:

\begin{itemize} \item if $s_i' \not \ptran{}$, then an edge
$s_{(M,a)}\ptran{\pi_i/\pi}s_i'$  is created;
\item for all transitions $s_i' \ptran{\rho_i}s_i''$, an edge
$s_{(M,a)}\ptran{\pi_i \rho_i/\pi}s_i''$  is created.
\end{itemize}
\end{itemize}
\end{definition}

\begin{example} Consider processes  $s$ and $s_{(\{a,b\},a)}$ in Fig. \ref{fig_pafter}.
Assuming that the initial menu of $s$ was $\{a,b\}$ and action $a$
was performed,   process  $s_{(\{a,b\},a)}$  describes the further
behaviour of $s$: with  probability
$\frac{1}{8}/(\frac{1}{8}+\frac{3}{8}) = \frac{1}{4}$ action
 $c$ is performed, while with  probability
$\frac{3}{8}/(\frac{1}{8}+\frac{3}{8}) = \frac{3}{4}$
action  $d$ is performed.
\end{example}

\begin{figure}[t]\centering
\large
       $ \xymatrix@R=0.3cm@C=0.1cm{
          & & & & & & \circ \ar@{-->}[dlllll]_{\frac{1}{8}} \ar@{-->}[dll]^{\frac{3}{8}} \ar@{-->}[drr]_{\frac{1}{4}} \ar@{-->}[drrrrr]^{\frac{1}{4}} & & & & & &\\
          & \circ \ar[dl]_{a} \ar[dr]^{b} & & & \circ \ar[dl]_{a} \ar[dr]^{b} & & & & \circ \ar[dl]_{a} \ar[dr]^{c} &&&  \circ \ar[dl]_{a} \ar[dr]^{e} & \\
          \circ\ar[d]_{c}  && \circ\ar[d]_{e} & \circ\ar[d]_{d} && \circ\ar[d]_{f} && \circ\ar[d]_{d} && \circ\ar[d]_{e} & \circ\ar[d]_{d} && \circ\ar[d]_{f} \\
          \circ && \circ & \circ && \circ && \circ &&  \circ & \circ && \circ
        }$
        \quad \quad
$\xymatrix@R=0.3cm@C=0.1cm{

& \circ \ar@{-->}[dl]_{\frac{1}{4}} \ar@{-->}[dr]^{\frac{3}{4}} \\
          \circ\ar[d]_{c}  && \circ\ar[d]_{d}  \\%& & \circ\ar[d]_{f} && \circ\ar[d]_{c} \\
          \circ  && \circ
           }
           $
\newline
 \caption{Example of a process $s$ (left) and $s_{(\{a,b\},a)}$
 (right).}
 \hbox{}\vspace{-0.5cm}
 \label{fig_pafter}
\end{figure}

\begin{definition} \label{def:P}Let $(
 M_1, a_1, M_2, a_2, \ldots, M_{n-1}, a_{n-1}, M_n)$
 be a ready trace of length $n$ and $s$ be a process graph.
 Functions $P_s^1(M )$  and
 $P_s^n(M_n | M_1, a_1, \ldots M_{n-1}, a_{n-1})$ (for $n > 1$)
 are defined in the following way:\\

\noindent$ P_s^1(M )=
\begin{cases}{}
\sum_{s \ptran{\pi}s'}{\pi \cdot P_{s'}^1(
M )} & \textrm{if } s \in S_p,\\
1 & \textrm{if } s \in S_n, \ I(s)=M, \\
0 & \textrm{otherwise. } \\%s \in S_n, I(s)\not =M \\
\end{cases}$\\\\
\noindent$P_s^2(M_2 | M_1, a_1) =
\begin{cases}{}
P_{s_{(M_1,a_1)}}^1(M_2) & \textrm{if} \ P_s^1(M_1)>0, \\
\textrm{undefined} & {otherwise}.
\end{cases}
$\\\\
\noindent$P_s^n(M_n | M_1, a_1, \ldots, a_{n-1})=
\begin{cases}{}
P_{s_{(M_1,a_1)}}^{n-1}(M_n | M_2, a_2, \ldots,
 a_{n-1}) & \textrm{if} \ P_s^1(M_1)>0, \\
\textrm{undefined} & {otherwise}.
\end{cases}
$
\end{definition}

Let the sample space consist of all possible menus and $s \in
S$. Function $P_s^1(M)$ can be interpreted as the
probability that the menu $M$ is observed initially when process
$s$ starts executing.  Let the sample space consist of all ready
traces of length $n$ and let $s \in S$. The function
$P_s^n(M_n | M_1, a_1, \ldots M_{n-1}, a_{n-1})$ can be
interpreted as the probability of the event $ \{(M_1, a_1,
\ldots, M_{n-1}, a_{n-1}, M_n) \} $, given the event $
\{(M_1, a_1, \ldots M_{n-1}, a_{n-1}, X) \textrm{~:~}
X \in 2^{\mathcal{A}} \}$, if observing ready traces of process
$s$. It can be checked that these probabilities are well defined,
i.e., they satisfy the axioms A1-A3 of Section \ref{sec:prelim}.

\begin{definition}[Probabilistic ready trace
equivalence]\label{def:barbed} Two processes $s$ and $\bar{s}$ are
\emph{probabilistically ready trace equivalent}, notation $s \mathrel{\approx_{\obs}}
\bar{s}$, iff:
\begin{itemize}
\item for all $M$ in $2^\mathcal{A}$, $P_s^1(M)=P_{\bar{s}}^1(M)$ and
\item for all $n > 1$, $P_s^n(M_n | M_1, a_1, \ldots M_{n-1},
a_{n-1})$ is defined if and only if $P_{\bar{s}}^n(M_n |
M_1, a_1, \ldots M_{n-1}, a_{n-1})$ is defined, and in  that
case $P_s^n(M_n | M_1, a_1, \ldots M_{n-1}, a_{n-1})$
$=$ $ P_{\bar{s}}^n(M_n | M_1, a_1, \ldots M_{n-1},
a_{n-1})$.
\end{itemize}
\end{definition}

\noindent Informally, two processes $s$ and $\bar{s}$ are
ready-trace equivalent iff for every $n$ and every ready trace
$(M_1, a_1, M_2, a_2 , \ldots M_n )$ , the probabilitity
to observe $M_n$, under condition that previously the sequence
$(M_1, a_1, M_2, a_2 , \ldots a_{n-1} )$ was observed, is
defined at the same time for both $s$ and $\bar{s}$; moreover, in
case both probabilities are defined, they coincide. Note that it is
straightforward to construct a black-box testing scenario
\cite{spectrum1, CSV07} for this ready-trace equivalence.

\begin{example} Processes $s$ and $\bar{s}$ in Fig. \ref{fig_machine} are  ready-trace equivalent. Processes in Fig. \ref{fig_notequiv} are not
ready-trace equivalent: for process $s$ it holds $P_s^2(\{c\} |
\{a,b\}, b)=\frac{1}{2}$, while for  process $\bar{s}$ it holds
$P_t^2(\{c\} | \{a,b\}, b)=0$.
\end{example}

\section{Algebra}\label{sec:algebra}

In this section we define an algebra $\textrm{CSP}_p$ of finite processes
using $\mathrel{\approx_{\obs}}$ as an underlying equivalence. The purpose is to show
that $\mathrel{\approx_{\obs}}$ is congruence for the standard operators on the model
of reactive probabilistic processes and that all operators
distribute through probabilistic choice, as all operators distribute
through  internal choice in standard CSP~\cite{csp}. As discussed in
Sec. \ref{sec:introduction}, we do not use hiding operator. For more
discussions on including internal nondeterminism in general, please
see Sec. \ref{sec:conclusion}.

The set of $\textrm{CSP}_p$ processes $\mathsf{P}$ is generated by the
following grammar:
\[\begin{array}{lcl}
 \mathsf{P} ::=\ \delta \ \mid\

          \mathsf{\sum}_{i \in I}{a_i}.\mathsf{P}_i \mid\

          \bigoplus_{i \in I}{\pi_i}\mathsf{P}_i \mid\
          \mathrel{\Theta} \mathsf{P} \mid\
          \mathsf{P}\parallel \mathsf{P} \mid\
          \mathsf{P} \parallel_L  \mathsf{P}

\enskip
\end{array}\] where $\delta \not \in  \mathcal{A}$ is a new symbol,   $\{a_i\}_{i \in I} \subseteq \mathcal{A}$,
$a_i \not = a_j$ for $i,j \in I, \ i \not = j$,  $\pi_i \in (0,1]$,
$\sum_{i \in I}{\pi_i}=1$, and $L \subseteq \mathcal{A}$ is the set of
actions that appear both in the left and in the right process  of
the expression
$\mathsf{P} \parallel_L  \mathsf{P}$.

Let $p,q,r,...$  range over $\textrm{CSP}_p$ processes. The constant
$\delta$ stands for the \emph{empty} process. The process
${a}.p$ performs the action $a$ and continues as process $p$ (we
write $a$ rather than $a.\delta$). The \emph{external choice}
$\mathsf{\sum}_{i \in I}{a_i}.p_i$ stands for a choice among the actions
$\{a_i\}_{i \in I}$ and proceeds as process $p_j$ if action $a_j$ is
chosen and executed. The \emph{probabilistic choice} $\bigoplus_{i \in
I}{\pi_i}p_i$ behaves as $p_i$ with probability $\pi_i$ for $i \in
I$. The \emph{priority} operator $\mathrel{\Theta}$  assumes a partial order
$>$ on $\mathcal{A}$. For actions $a$ and $b$,
 we say $a$ has higher priority than $b$ iff $a > b$.  $\mathrel{\Theta}$ forces the process  to always perform the action with the highest
priority in the current menu. In a \emph{synchronized parallel
composition} $p \parallel q$, the processes operate in a lock-step
synchronization. In a \emph{parallel composition} $p  \parallel_L  q$, the
processes synchronize on their common actions, while the other
actions are interleaved. \footnote{To preserve associativity of
$ \parallel_L $, we  require that for any processes $p,q$, and $r$, if $p$ and
$q$ share actions and $q$ and $r$ share actions then $p$ and $r$ do
not share actions.} \footnote{Sequential composition and successful
termination can be also defined, which we avoid here to shorten.}

Table~\ref{table:procsem} represents the operational semantics of
$\textrm{CSP}_p$ processes (we omit the symmetric rules for $ \parallel_L $ and
$\parallel$).

\begin{table}[t!]
 \center\framebox{{\small
\begin{tabular}{c}

\renewcommand{\thesosrule}{\mathalpha{\ensuremath{}}}
    $\sosrule{}{\mathsf{\sum}_{i \in I}{a_i}.p_i\exec{a_i}p_i}$

       $\renewcommand{\thesosrule}{\mathalpha{\ensuremath{}}}
    \sosrule{p\exec{a} p',\ q\exec{a}{q'}}
            {p\parallel q\exec{a} p'\parallel q'}$

  $ \renewcommand{\thesosrule}{\mathalpha{\ensuremath{}}}
    \sosrule{p \pexec{\pi} p',\ q \pexec{\rho} q'}
            {p\parallel q \pexec{\pi \rho} p' \parallel q'}$

  \\\\

  $ \renewcommand{\thesosrule}{\mathalpha{\ensuremath{}}}
    \sosrule{p \pexec{\pi} p',\ q \mathalpha{\not\dashrightarrow}}
            {p\parallel q \pexec{\pi} p' \parallel q}$

    $\renewcommand{\thesosrule}{\mathalpha{\ensuremath{}}}
    \sosrule{ p_k\mathalpha{\not\dashrightarrow}, k \in I}
            {\bigoplus_{i \in I}{\pi_i p_i}\ptran{\pi_k}p_k}$

            $\renewcommand{\thesosrule}{\mathalpha{\ensuremath{}}}
    \sosrule{ p_k\pexec{\rho_k}p_k', k \in I}
            {\bigoplus_{i \in I}{\pi_i p_i}\ptran{\pi_k\rho_k}p_k'}$
\\\\

    $\renewcommand{\thesosrule}{\mathalpha{\ensuremath{}}}
    \sosrule{a \not \in L, \ p\exec{a}\torp{p'},\ q\mathalpha{\not\dashrightarrow}}{p \parallel_L  q\exec{a} {p' \parallel_L  q}}$

       $\renewcommand{\thesosrule}{\mathalpha{\ensuremath{}}}
    \sosrule{a \in L, \ p\exec{a} p',\ q\exec{a}{q'}}
            {p \parallel_L  q\exec{a} p' \parallel_L  q'}$

$ \renewcommand{\thesosrule}{\mathalpha{\ensuremath{}}}
    \sosrule{p \pexec{\pi} p',\ q \mathalpha{\not\dashrightarrow}}
            {p \parallel_L  q \pexec{\pi} p'  \parallel_L  q}$

\\\\
  $ \renewcommand{\thesosrule}{\mathalpha{\ensuremath{}}}
    \sosrule{p \pexec{\pi} p',\ q \pexec{\rho} q'}
            {p \parallel_L  q \pexec{\pi \rho} p'  \parallel_L  q'}$

$ \renewcommand{\thesosrule}{\mathalpha{\ensuremath{}}}
    \sosrule{p \exec{a} p',\ p \not \exec{b} \textrm{ for } a < b}
            {\mathrel{\Theta} p \exec{a} \ \mathrel{\Theta} p'}$

$ \renewcommand{\thesosrule}{\mathalpha{\ensuremath{}}}
    \sosrule{p \ptran{\pi} p'}
            {\mathrel{\Theta} p \ptran{\pi} \ \mathrel{\Theta} p'}$\\\\

\end{tabular} } } \caption{Operational semantics for $\textrm{CSP}_p$ processes}\label{table:procsem}
\end{table}
As usual, a context is a $\textrm{CSP}_p$ process  with a hole in it.
Given a context $C[\cdot]$ and a process $p$, we write $C[p]$ to
denote the process obtained by filling in the hole of $C[\cdot]$
with $p$. \begin{SHORTVERSION}The proofs of the following theorems
are given in \cite{testing_report}.\end{SHORTVERSION}

\begin{theorem}[Congruence]\label{thm:congruence} The equivalence $\mathrel{\approx_{\obs}}$ is congruence for
the operators of $\textrm{CSP}_p$, i.e., if $p \mathrel{\approx_{\obs}} \bar{p}$ then for
each context $C[\cdot]$, it holds that $C[p] \mathrel{\approx_{\obs}} C[\bar{p}]$.
\end{theorem}
\begin{LONGVERSION}
\begin{proof}
We prove the congruence result for parallel composition, because
this is the most complicated case. We prove that if $p \mathrel{\approx_{\obs}}
\bar{p}$ then $p  \parallel_L  q \mathrel{\approx_{\obs}} \bar{p}  \parallel_L  q$.  Denote by $L$ the set of
the common actions for $p$ and $q$ (and therefore $\bar{p}$ and $q$).
Without loss of generality, assume that $p,\bar{p}, $ and $q$ are
probabilistic processes. For arbitrary menus $M', M''$,
denote by $M' \otimes M''$ the menu $(M' \cup
M'')\setminus
(L \setminus (M' \cap M''))$.\\

By induction on $n$, we prove that if $p \mathrel{\approx_{\obs}} \bar{p}$ then
$P_{(p  \parallel_L   q)}^{n} (M_n | M_1, a_1, \ldots
M_{n-1},a_{n-1})$ $=$ $P_{(\bar{p}  \parallel_L  q)}^{n} (M_n |
M_1, a_1, \ldots M_{n-1},a_{n-1})$.

For arbitrary menus $M_p$ and  $M_q$, we have
$P_p^1(M_p)=P_{\bar{p}}^1(M_p)$. Let $M$ be a menu
such that $P_{p  \parallel_L  q}^1(M)>0$. This means that there exist
menus $M_p, M_q$ such that $P_p^1(M_p)>0$,
$P_q^1(M_q)>0$, and $M=M_p \otimes M_q$ (by
Table \ref{table:procsem}). We have,
\begin{align*}
&P_{p  \parallel_L  q}^1(M)=  \sum_{ \begin{scriptsize}
\begin{array}{c}
                                     p  \parallel_L  q \ptran{\lambda_k}r_k, \\
                                    I(r_k)=M
                                   \end{array}\end{scriptsize}
}\lambda_k =\sum_{ \begin{scriptsize}\begin{array}{c}
                      p \ptran{\pi_i} p_i,q \ptran{\rho_j}q_j, \\
                     I(p_i)\otimes I(q_j)=M
                   \end{array}\end{scriptsize}
 }{\pi_i \cdot \rho_j}\\
=&\sum_{q\ptran{\rho_j}q_j}{\rho_j\sum_{
p\ptran{\pi_i}p_i,M=I(p_i)\otimes I(q_j)}{\pi_i}}
=\sum_{q\ptran{\rho_j}q_j}{\rho_j\sum_{\bar{p}\ptran{\bar{\pi}_i}\bar{p}_i,M=I(\bar{p}_i)\otimes
I(q_j)}{\bar{\pi}_i}} = P_{\bar{p}  \parallel_L  q}^1(M).
\end{align*}
Suppose $P_{(p  \parallel_L   q)}^{k} (M_k | M_1, a_1, \ldots
M_{k-1},a_{k-1})$$=$$P_{(\bar{p}  \parallel_L  q)}^{k} (M_k |
M_1, a_1, \ldots M_{k-1},a_{k-1})$ if $p \mathrel{\approx_{\obs}} \bar{p}$ and
$k<n$.

\noindent \textbf{Case 1} Suppose first that both $P_{(p  \parallel_L
q)}^{n} (M_n | M_1, a_1, \ldots M_{n-1},a_{n-1})$ and
$P_{(\bar{p}  \parallel_L  q)}^{n} (M_n | M_1, a_1, \ldots
M_{n-1},a_{n-1})$ are defined.
 Because of Def. \ref{def:P} and the inductive assumption, it is enough to prove that $P_{(p  \parallel_L
q)_{(M_1,a_1)}}^{n-1} (M_n | M_2, a_2, \ldots
M_{n-1},a_{n-1})$ = $P_{(\bar{p}  \parallel_L  q)_{(M_1,a_1)}}^{n-1}
(M_n | M_2, a_2, \ldots M_{n-1},a_{n-1})$. Because of
the inductive assumption, to prove the last, it is enough to prove
that  $(p
 \parallel_L  q)_{(M_1,a_1)} \mathrel{\approx_{\obs}} (\bar{p}  \parallel_L  q)_{(M_1,a_1)}$ .\\

\noindent \textbf{Case 1.1} \ $a_1=a \in L$.\\\\

\noindent Denote $\sum_{p \ptran{\pi_i}p_i,q\ptran{\rho_j}q_j,
I(p_i)\otimes I(q_j) = M_1} \pi_i \rho_j$ by $\alpha$. By Def.
\ref{def:pafter} and the rules in Table \ref{table:procsem}, we have
\begin{equation} \label{eq:cong1}
(p  \parallel_L  q)_{(M_1,a)} \equiv
 \bigoplus_{\begin{scriptsize}\begin{array}{c}
          p \ptran{\pi_i}p_i,q\ptran{\rho_j}q_j, \\
         I(p_i)\otimes I(q_j) = M_1
       \end{array}\end{scriptsize}
}{\frac{\pi_i\rho_j}{\alpha} \Bigl(p_{i_{(I(p_i),a)}} \parallel_L
q_{j_{(I(q_j),a)}}}\Bigr).
\end{equation}
\noindent On the other hand, denoting $\sum_{M_1=M_p\otimes
M_q}{P_p(M_p) P_q(M_q)}$ by $\beta$, we have
\begin{align}\label{eq:cong2}
 &\  \bigoplus_{
M_1=M_p\otimes M_q}
\frac{P_p(M_p)P_q(M_q)}{\beta
}{\Bigl(p_{(M_p,a)} \parallel_L  q_{(M_q,a)}\Bigr)} \notag \\
\equiv & \biggl(\bigoplus_{M_1=M_p\otimes M_q}
\frac{P_p(M_p)P_q(M_q)}{\beta}\biggr)\times \notag \\
& \ \ \ \ \times {\biggl(\bigoplus_{p
\ptran{\pi_i}p_i,I(p_i)=M_p}\frac{\pi_i}{P_p(M_p)}
p_{i_{(M_p,a)}}\biggr) \parallel_L  \biggr(\bigoplus_{q
\ptran{\rho_j}q_j,I(q_j)=M_q}\frac{\rho_j}{P_q(M_q)}
q_{j_{(M_q,a)}}\biggr)} \notag \\
\equiv & \biggl(\bigoplus_{ M_1=M_p\otimes M_q}
\frac{P_p(M_p)P_q(M_q)}{\beta
}\biggr)\times \notag \\
& \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \times
{\biggl(\bigoplus_{\begin{scriptsize}\begin{array}{c}
                                 p \ptran{\pi_i}p_i,I(p_i)=M_p, \\
                                 q \ptran{\rho_j}q_j,I(q_j)=M_q
                               \end{array}\end{scriptsize}
}\frac{\pi_i \rho_j}{P_p(M_p)P_q(M_q)}
\Bigl(p_{i_{(M_p,a)}} \parallel_L
q_{j_{(M_q,a)}}\Bigr)\biggr)} \notag \\
\equiv&\bigoplus_{\begin{scriptsize}\begin{array}{c}
               p \ptran{\pi_i}p_j,q\ptran{\rho_j}q_j, \\
               M_1=I(p_i)\otimes
I(q_j)
             \end{array}\end{scriptsize}
 }{\frac{\pi_i\rho_j}{\alpha} \Bigl(p_{i_{(I(p_i),a)}} \parallel_L
q_{j_{(I(q_j),a)}}}\Bigl).
\end{align}\\

From \eqref{eq:cong1} and \eqref{eq:cong2} we have

\begin{equation}\label{eq:cong3}
(p  \parallel_L  q)_{(M_1,a)} \equiv \bigoplus_{M_p,M_q:
M_1=M_p\otimes M_q}
\frac{P_p(M_p)P_q(M_q)}{\sum_{M_p,M_q}{P_p(M_p)
P_q(M_q)}}{\Bigl(p_{(M_p,a)} \parallel_L  q_{(M_q,a)}\Bigr)}.
\end{equation}

Similarly,
 \begin{equation}\label{eq:cong4}(\bar{p}  \parallel_L  q)_{(M_1,a)} \equiv
\bigoplus_{M_p,M_q: M_1=M_p\otimes M_q}
\frac{P_{\bar{p}}(M_p)P_q(M_q)}{\sum_{M_p,M_q}{P_{\bar{p}}(M_p)
P_q(M_q)}}{\Bigl(\bar{p}_{(M_p,a)} \parallel_L
q_{(M_q,a)}\Bigr)}.
\end{equation}

From the inductive assumption and because $p \mathrel{\approx_{\obs}} \bar{p}$ and
$\mathrel{\approx_{\obs}}$ is congruence for $\bigoplus$, we have

\begin{align}\label{eq:cong5}
&\bigoplus_{M_p,M_q: M_1=M_p\otimes M_q}
\frac{P_p(M_p)P_q(M_q)}{\sum_{M_p,M_q}{P_p(M_p)
P_q(M_q)}}{\Bigl(p_{(M_p,a)} \parallel_L  q_{(M_q,a)}\Bigr)} \notag \\
\equiv & \bigoplus_{M_p,M_q: M_1=M_p\otimes M_q}
\frac{P_{\bar{p}}(M_p)P_q(M_q)}{\sum_{M_p,M_q}{P_{\bar{p}}(M_p)
P_q(M_q)}}{\Bigl(\bar{p}_{(M_p,a)} \parallel_L
q_{(M_q,a)}\Bigr)}.
\end{align}

 From \eqref{eq:cong3}, \eqref{eq:cong4}, and \eqref{eq:cong5}
 it follows that $(p  \parallel_L  q)_{(M_1,a)} \equiv$ $(\bar{p}
 \parallel_L  q)_{(M_1,a)} $.\\

\noindent \textbf{Case 1.2} \ $a_1 \not \in L$, $a_1$ appears in
$p$. The proof is similar to Case 1, with the difference that
instead of a process $q_{(M_q,a_1)}$, we use a process
$q_{(M_q)}$. The last one is defined by a process graph obtained
in a similar way as $q_{(M_q,a_1)}$, with the exception that
$q_{(M_q)}$ is
``ready'' to choose any action from the menu $M_q$.\\

\noindent \textbf{Case 1.3} \ $a_1 \not \in L$, $a_1$ appears in $q$
- symmetric to Case
2.\\

\noindent \textbf{Case 2} Suppose now that $P_{(p  \parallel_L   q)}^{k}
(M_k | M_1, a_1, \ldots M_{k-1},a_{k-1})$ is defined but
$P_{(\bar{p}  \parallel_L  q)}^{k} (M_k | M_1, a_1, \ldots
M_{k-1},a_{k-1})$ is not defined. Either $P_{(p  \parallel_L
q)}(M_1)>0$ while $P_{(\bar{p}  \parallel_L  q)}(M_1)=0$, which is
not possible because $p \mathrel{\approx_{\obs}} \bar{p}$, or $P_{(p  \parallel_L
q)_{(M_1,a_1)}}^{k-1} (M_k | M_2, a_2, \ldots
M_{k-1},a_{k-1})$ is defined but $P_{(\bar{p}  \parallel_L
q)_{(M_1,a_1)}}^{k-1} (M_k | M_2, a_2, \ldots
M_{k-1},a_{k-1})$ is not defined, which again is not possible
because of the inductive assumption.
\end{proof}
\end{LONGVERSION}

The following two theorems formulate the laws of distributivity of
the operators over probabilistic choice.

\begin{theorem}\label{thm:external} For processes $\{x_{ij}\}_{i \in I, j \in J}$ and actions $\{a_{i}\}_{i \in I} \subseteq \mathcal{A}$, it holds $\mathsf{\sum}_{i \in I}a_i.\bigoplus_{j \in J}\pi_j x_{ij}\mathrel{\approx_{\obs}} \bigoplus_{j \in
J}\pi_j\mathsf{\sum}_{i \in I}a_i. x_{ij}$.

\end{theorem}
\begin{LONGVERSION}
\begin{proof}
Let $M=\{a_i\}_{i \in I}$, $p \equiv \mathsf{\sum}_{i \in I}a_i.\bigoplus_{j
\in J}\pi_j x_{ij}$ and $\bar{p} \equiv \bigoplus_{j \in J}\pi_j\mathsf{\sum}_{i
\in I}a_i. x_{ij}$. Then,  it is easy to show that, for every $i \in
I$, $p_{(M, a_i)} \mathrel{\approx_{\obs}} \bar{p}_{(M, a_i)}$. Let $n
> 1$ and  $(M_1,b_1, \ldots M_n)$ be an observation.  Then,

\[P_p^n(M_n|M_1,b_1, \ldots,  b_{n-1})=
\begin{cases}{}
 P_{p_{(M_1,b_1)}}^{n-1}(M_n|M_2,b_2, \ldots
 b_{n-1}) & \textrm{if } M_1=M , b_1 \in M
\\
\textrm{undefined} & \textrm{otherwise},
\end{cases}
\]
and
\[P_{\bar{p}} ^n(M_n|M_1,b_1, \ldots,  b_{n-1})=
\begin{cases}{}
 P_{{\bar{p}}_{(M_1,b_1)}}^{n-1}(M_n|M_2,b_2, \ldots
 b_{n-1}) & \textrm{if } M_1=M , b_1 \in M
\\
\textrm{undefined} & \textrm{otherwise}.
\end{cases}
\]

Now, it easily follows that
$p \mathrel{\approx_{\obs}} \bar{p}$.
\end{proof}
\end{LONGVERSION}

\begin{theorem}\label{thm:distr} For every context $C[\cdot]$, it holds $C[\bigoplus_{i \in I}\pi_i x_i]\mathrel{\approx_{\obs}} \bigoplus_{i \in I}\pi_i C[ x_i]
$.
\end{theorem}
\begin{LONGVERSION}
\begin{proof}
By structural induction, similarly to the proof of Theorem
\ref{thm:external}.
\end{proof}
\end{LONGVERSION}

\section{Relationship between $\mathrel{\approx_{\mathcal{T}}}$ and
$\mathrel{\approx_{\obs}}$}\label{sec:relationship}

We establish our main result, namely that the testing equivalence
$\mathrel{\approx_{\mathcal{T}}}$ coincides with the probabilistic ready trace equivalence
$\mathrel{\approx_{\obs}}$. As an intermediate result, we prove that probabilistic
transitions do not add distinguishing power to the tests.
\begin{SHORTVERSION}The complete proofs of the results can be found
in \cite{testing_report}.\end{SHORTVERSION}

\begin{theorem}\label{thm:desno_levo}
Let $s$ and $t$ be two processes. If $s \mathrel{\approx_{\obs}} t$ then $s \mathrel{\approx_{\mathcal{T}}}
t$.
\end{theorem}
\begin{LONGVERSION}
\begin{proof}
Suppose $s \not \mathrel{\approx_{\mathcal{T}}} t$.  There exists a test $T$ such that
$\mathsf{Result}(s,T) \not = \mathsf{Result}(t,T)$. W.l.g., assume that $s$ and $t$
start with probabilistic transitions. By Def. \ref{def:Results},

\begin{equation}\label{eq:proof2_1}
 \mathsf{Result}(s,T)   =    \sum_{T\ptran{\rho_j}T_j} \rho_j \sum_{s \ptran{\pi_i}s_i}{\pi_i  \sum_{a
\in I(s_i)\cap I(T_j)}{\frac{a}
 {\sum_{b \in I(s_i)\cap I(T_j)}{b}} \cdot \mathsf{Result} (s_{ia},T_{ja}).}}
 \end{equation}

\noindent By Def. \ref{def:pafter}, from \eqref{eq:proof2_1} we
obtain

\begin{align}\label{eq:proof2_a}
\mathsf{Result}(s,T) = & \sum_{M':P_T^1(M')>0}P_T^1(M') \sum_{M:P_s^1(M)>0}P_s^1(M) \times  \qquad \qquad \qquad \qquad \qquad \qquad \qquad \notag\\
   & \qquad \qquad \qquad \times  \sum_{a \in M \cap M'} \frac{a}{\sum_{b \in M
\cap M'}b}  \mathsf{Result}(s_{(M,a)}, T_{(M',a)}).
\end{align}

Similarly  we obtain

\begin{align}\label{eq:proof2_aa}
\mathsf{Result}(t,T) = & \sum_{M':P_T^1(M')>0}P_T^1(M') \sum_{M:P_t^1(M)>0}P_t^1(M) \times  \qquad \qquad \qquad \qquad \qquad \qquad \qquad \notag\\
   & \qquad \qquad \qquad \times  \sum_{a \in M \cap M'} \frac{a}{\sum_{b \in M
\cap M'}b}  \mathsf{Result}(t_{(M,a)}, T_{(M',a)}).
\end{align}

Now, assume $s \mathrel{\approx_{\obs}} t$. Define a \emph{length of a test} to be
the length of the longest sequence of actions the test can perform
before executing the action $\omega$.
  The proof is by induction on the minimal length of
 a nonprobabilistic test that distinguishes between $s$ and $t$.

Let $T$ be a test of length $1$ such that $\mathsf{Result}(s,T) \not =
\mathsf{Result}(t,T)$. From Def. \ref{def:Results} it follows that for every
process $u$,
\begin{equation}\label{eq:proof2_b}
\mathsf{Result}(u, T_{(M,a)})=P^1_{T_{(M',a)}}(\{\omega\}).
\end{equation}

From \eqref{eq:proof2_a} and \eqref{eq:proof2_b} we have

\begin{align}\label{eq:proof2_c}
\mathsf{Result}(s,T) = & \sum_{M':P_T^1(M')>0}P_T^1(M') \sum_{M:P_s^1(M)>0}P_s^1(M) \times  \qquad \qquad \qquad \qquad \qquad \qquad \qquad \notag\\
   & \qquad \qquad \qquad \qquad \qquad \qquad \times  \sum_{a \in M \cap M'} \frac{a}{\sum_{b \in M
\cap M'}b}  P^1_{T_{(M',a)}}(\{\omega\}).
\end{align}

Similarly we obtain

\begin{align}\label{eq:proof2_d}
\mathsf{Result}(t,T) = & \sum_{M':P_T^1(M')>0}P_T^1(M') \sum_{M:P_t^1(M)>0}P_t^1(M) \times  \qquad \qquad \qquad \qquad \qquad \qquad \qquad \notag\\
   & \qquad \qquad \qquad \qquad \qquad \qquad  \times  \sum_{a \in M \cap M'} \frac{a}{\sum_{b \in M
\cap M'}b}  P^1_{T_{(M',a)}}(\{\omega\}).
\end{align}

 From \eqref{eq:proof2_c},\eqref{eq:proof2_d} and from the assumption that $P_s^1(M) =P_t^1(M)$
for every menu $M$,
 we obtain that $\mathsf{Result}(s,T) = \mathsf{Result}(t,T)$, i.e. we obtain contradiction. Therefore,
 there exists a menu $M$ such that $P^1_s(M)\not =P^1_t(M)$, i.e. $s \not \mathrel{\approx_{\obs}} t$. \\

Let $T$ be a  test of length greater than one such that
$\mathsf{Result}(s,T) \not = \mathsf{Result}(t,T)$
 If there exists a
menu $M$ such that $P_s^1(M)\not =P_t^1(M) $,
then $s \not \mathrel{\approx_{\obs}} t$ and the proof is over. Therefore, suppose
$P_s^1(M) =P_t^1(M) $ for every menu $M
\subseteq \mathcal{A}$. From \eqref{eq:proof2_a} and
\eqref{eq:proof2_aa} we have that for some menus $M$, $M'$
and action $a \in M \cap M'$, it holds
$\mathsf{Result}(s_{(M,a)}, T_{(M',a)})$ $\not
 =$ $\mathsf{Result}(t_{(M,a)}, T_{(M',a)})$. Now, by the inductive
 assumption, we have $s_{(M,a)}\not \mathrel{\approx_{\obs}} t_{(M,a)}$, i.e.
 there exists a ready trace $(M_2,a_2, \ldots M_k)$  such that $P_{s_{(M,a)}}^{k-1}(M_k | M_2, a_2, \ldots a_{k-1})$
  $\not =$ $P_{t_{(M,a)}}^{k-1}(M_k | M_2, a_2, \ldots
  a_{k-1})$ (or they are not defined at the same time). From the last,  from the assumption that  $P_s^1(M)=
  P_t^1(M)>0$, and from Def. \ref{def:P} it follows  that $P_{s}^{k}(M_k | M,a, M_2, a_2, \ldots a_{k-1})$
  $\not =$ $P_{t}^{k}(M_k | M,a, M_2, a_2, \ldots
  a_{k-1})$ (or they are not defined at the same time), i.e. $s \not \mathrel{\approx_{\obs}}
  t$. This completes the proof of the theorem.
\end{proof}
\end{LONGVERSION}

\begin{LONGVERSION}
The following lemma, which considers the determinant of a certain
type of an almost-triangular matrix, shall be needed in the proof of
Theorem \ref{thm:levo_desno}.

\begin{lemma} \label{lem:determinant}Let $\mathbf{Q}$ be a square $n \times n$ matrix
with elements $q_{ij}$, for $1\leq i \leq n$ and $1\leq j \leq n$.
Suppose $q_{ij}\in \{0,1\}$ for $i>1$, $q_{ij}=1$ for $i=j+1$,
$q_{ij}=0$ for $i>j+1$, and $q_{1j}=\frac{Q_1}{Q_j}$ for $1\leq j
\leq n$, where $Q_1, Q_2\ldots Q_n$ are  irreducible, mutually prime
polynomials with positive variables, and of non-zero degrees. Then
the determinant of $\mathbf{Q}$ is a non-zero rational function.
\end{lemma}

\begin{proof}
The determinant $\mathsf{Det}(\mathbf{Q})$ of  matrix $\mathbf{Q}$ can be
obtained from the general recursive formula
$\mathsf{Det}(\mathbf{Q})=\sum_{j=1}^{n}(-1)^{1+j}q_{1j}\mathsf{Det}(\mathbf{Q_{1j}})
$, where $\mathbf{Q_{1j}}$  is  the matrix obtained by deleting the
first row and the $j$-th column of $\mathbf{Q}$. Observe that
$\mathbf{Q_{1n}}$ is an upper-triangular matrix, the diagonal
elements of which are all equal to one. Since the determinant of a
triangular matrix is equal to the product of its diagonal elements,
we have $\mathsf{Det}(\mathbf{Q_{1n}})=1$. Therefore, the coefficient in
front of the rational function $\frac{Q_1}{Q_n}$ in
$\mathsf{Det}(\mathbf{Q})$ is equal to $1$. Suppose $\mathsf{Det}(\mathbf{Q})$ is a
zero-function. Then, the rational function $\frac{1}{Q_n}$ is equal
to a
 linear combination of $\frac{1}{Q_1}, \ldots \frac{1}{Q_{n-1}}$. This means  that the rational function $\frac{Q_1 \cdot
Q_2\cdot Q_{n-1}}{Q_n}$ is a polynomial. The last
 is impossible,
since, by assumption, the denominator is irreducible polynomial of
non-zero degree and is not contained in the numerator. Therefore,
$\mathsf{Det}(\mathbf{Q})$ is not a zero-function.
\end{proof}
\end{LONGVERSION}

\begin{theorem} \label{thm:levo_desno}
 Let $s$ and $t$ be two processes such that $s \not \mathrel{\approx_{\obs}}
t$. There exists a test $T$ that has no probabilistic transitions
such that $\mathsf{Result}(s,T) \not = \mathsf{Result}(t,T)$.
\end{theorem}

\begin{proof}\begin{SHORTVERSION} (Outline)
The proof is technically rather involved \cite{testing_report},
which is why here we give only the main lines of it.
\end{SHORTVERSION} We prove the theorem by induction on the minimal
length $m$ of a ready trace that distinguishes between $s$ and $t$.
For $m=1$, we prove that the test $T=\mathsf{\sum}_{a\not \in
M}{a.\omega}$, where $M$ is a menu with a minimal possible
number of actions such that $P_s^1(M)\not =
P_t^1(M)$, distinguishes between $s$ and $t$. For $m>1$ the
proof goes as follows. If $P_s^1(M) = P_t^1(M)$ for
every menu $M$, then by the inductive assumption it follows that
there exists a test $T_1$, menu $M_1$ and action $a_1 \in
M_1$ such that $\mathsf{Result}(s_{(M_1,a_1)},T_1)
 \not  = \mathsf{Result}(t_{(M_1,a_1)},T_1)$. We show that there exists
 a subset of the action set, say $\mathsf{Act}$, such that the test $T=a_1.T_1+\mathsf{\sum}_{b \in
 \mathsf{Act}}.\omega$ distinguishes between $s$ and $t$. To prove this,
we take $M_1$ to be
 the menu containing a minimal possible number of actions such that $P_s^1(M_1)>0$, $a_1 \in M_1$,  and
$\mathsf{Result}(s_{(M_1,a_1)},T_1)
 \not  = \mathsf{Result}(t_{(M_1,a_1)},T_1)$. Then we take the set
 $\mathsf{Act'}$ to consist of the actions that can be initially
 performed by $s$ but do not belong to menu $M_1$. Then, we show
 that there must exist a subset $\mathsf{Act}$ of $\mathsf{Act'}$
 such that the test $T=a_1.T_1+\mathsf{\sum}_{b \in
 \mathsf{Act}}.\omega$ distinguishes between $s$ and $t$ (otherwise, we obtain that $\mathsf{Result}(s_{(M_1,a_1)},T_1)
   = \mathsf{Result}(t_{(M_1,a_1)},T_1)$, which contradicts our assumption).

\begin{LONGVERSION}
We now proceed with a detailed presentation of the proof.

 From $s \not \mathrel{\approx_{\obs}} t$ and by Def. \ref{def:barbed}, there
must exist a ready trace $(M_1, a_1, \ldots M_m)$ such that
$P_s^m(M_m | M_1, a_1, \ldots a_{m-1}) \not =
P_t^m(M_m | M_1, a_1, \ldots a_{m-1})$. The proof is by
induction on $m$.\\

\textbf{Case 1 ($m=1$)} Suppose first that there exists a menu
$M$ such that
$P_s^1(M)\not = P_t^1(M)$.
Let $M$ be a menu with a minimal possible number of actions such
that $P_s^1(M)\not = P_t^1(M)$. Take
$T=\mathsf{\sum}_{a\not \in M}{a.\omega}$. We have $\mathsf{Result}(s,T) = 1-
\sum_{M' \subseteq M}P_s^1(M')$, because the actions
of $s$ and $T$ will fail to synchronize if and only if the random
choice decides that menu $M$ or some menu $M' \subset M$
is offered to process $s$ initially. Similarly, $\mathsf{Result}(t,T) = 1-
\sum_{M' \subseteq M}P_t^1(M')$. Now, suppose that
$\mathsf{Result}(s,T)
  = \mathsf{Result}(t,T)$. We have
   $\sum_{M' \subseteq M}P_s^1(M')=
   \sum_{M' \subseteq M}P_t^1(M')$. From this and  $P_s^1(M)\not =
P_t^1(M)$, it follows that there  exists a menu $M'
\subset M$ such that also $P_s^1(M')\not =
P_t^1(M')$. But this contradicts the assumption that $M$
is a menu with a minimal possible number of actions such that
$P_s^1(M)\not =
P_t^1(M)$.\\

\textbf{Case 2 ($m>1$)} Suppose now that $P_s^1(M) =
P_t^1(M)$ for every menu $M$. Let $(M_1, a_1, \ldots
M_m)$ be a ready trace
such that
$P_s^{m-1}(M_m | M_1, a_1, \ldots a_{m-1}) \not =
P_t^{m-1}(M_m | M_1, a_1, \ldots a_{m-1})$. From
$P_s^1(M_1) = P_t^1(M_1)$, and from  Definitions
\ref{def:pafter} and \ref{def:P}, it follows that
$P_{s_{(M_1,a_1)}}^{m-1}(M_m | M_2, a_2, \ldots
a_{m-1}) \not = P_{t_{(M_1,a_1)}}^{m-1}(M_m | M_2,
a_2, \ldots a_{m-1})$ (in case $m=2$,
$P_{s_{(M_1,a_1)}}^1(M_2 ) \not =
P_{t_{(M_1,a_1)}}^1(M_2) $). Now, by the inductive
assumption, there exists a non-probabilistic test $T_1$ such that
$\mathsf{Result}(s_{(M_1,a_1)},T_1)
 \not  = \mathsf{Result}(t_{(M_1,a_1)},T_1)$.\\

\textbf{Case 2.1} \ Suppose first that $a_1$ does not belong to any
first-level menu of $s$ other than $M_1$, i.e. that for every
menu $M$, $P_s^1(M)>0$ and $a_1 \in M$ implies
$M = M_1$.  Then the test $T=a_1.T_1$ distinguishes
between $s$  and $t$.\\

\textbf{Case 2.2} \ Suppose now that $a_1$ belongs to at least one
first-level menu of
 $s$ other than $M_1$, i.e.
there exists at least one menu $M \not = M_1$ such that
$P_s^1(M)>0$ and $a_1 \in M$.
 Without loss of
 generality, assume that $M_1$ is a menu with a minimal possible number of actions such that
$P_s^1(M_1)>0$, $a_1 \in M_1$,  and
$\mathsf{Result}(s_{(M_1,a_1)},T_1)
 \not  = \mathsf{Result}(t_{(M_1,a_1)},T_1)$.
 Let $\{b_j\}_{j \in J}$ be
the set of actions that appear in the first level of $s$ (and
therefore $t$) but not in $M_1$, i.e. $b \in \{b_j\}_{j \in J}$
if and only if $b \not \in M_1$ and there exists a menu $M$
such that $P_s^1(M)>0$, $b \in M$. We shall prove that
there exists $J' \subseteq J$ such  that the test $T=a_1.T_1+
\mathsf{\sum}_{j \in J' }b_j.\omega$ distinguishes between $s$ and $t$.
More concretely, we shall prove that, assuming the opposite, it
follows that $\mathsf{Result}(s_{(M_1,a_1)},T_1)
  = \mathsf{Result}(t_{(M_1,a_1)},T_1)$, thus obtaining contradiction.
  \\

\textbf{Case 2.2.a} \ Suppose first that $\{b_j\}_{j \in J} =
\emptyset$. This means that there are no actions other than those in
$M_1$, that appear in the first level of $s$. Therefore, all
menus $M$ for which $P_s^1(M)>0$ satisfy $M
\subseteq M_1$. We prove that the test $T=a_1.T_1$ distinguishes
between $s$ and $t$. Assume that $\mathsf{Result}(s,T)=\mathsf{Result}(t,T)$. From
the last and from Def. \ref{def:Results}, we obtain

\begin{equation}\label{eq:submenus}
\sum_{M:P_s^1(M)>0,a_1\inM \subseteq
M_1}(\mathsf{Result} (s_{(M,a_1)},T_1)-\mathsf{Result}
(t_{(M,a_1)},T_1))=0.
\end{equation}
 By
assumption, for every $M \subset M_1$ such that $a_1 \in
M$ it holds $\mathsf{Result} (s_{(M,a_1)},T_1)=\mathsf{Result}
(t_{(M,a_1)},T_1)$. Therefore, from \eqref{eq:submenus} we
obtain $\mathsf{Result} (s_{(M_1,a_1)},T_1)=\mathsf{Result}
(t_{(M_1,a_1)},T_1)$, which contradicts the assumption $\mathsf{Result}
(s_{(M_1,a_1)},T_1)\not =\mathsf{Result} (t_{(M_1,a_1)},T_1)$.\\

\textbf{Case 2.2.b} \ Suppose now that $\{b_j\}_{j \in J} \not =
\emptyset$.
 Given action
$b_i \in \{b_j\}_{j \in J}$, denote by $\mathcal{M}_i$ the set of
all first-level menus of $s$ that contain $b_i$ and $a_1$, i.e.
$M \in \mathcal{M}_i$ iff $P_s^1(M) >0$ and $b_i,a_1 \in
M$; denote by $\mathcal{M}_i^C$ the set of all first-level menus
of $s$ that do not contain $b_i$ but have $a_1$, i.e. $M \in
\mathcal{M}_i^C$ iff $P_s^1(M) >0$, $b_i \not \in M$ and
$a_1 \in M$.

Let $T=a_1.T_1+\mathsf{\sum}_{j \in J' }b_j.\omega$ for some
$J'=\{1,2,\ldots n\} \subseteq J$ and suppose $\mathsf{Result}(s,T)
  = \mathsf{Result}(t,T)$. Since $P_s^1(M)=P_t^1(M)$ for every menu $M$,
  observe that only if action $a_1$ is performed initially, it is
possible for the test $T=a_1.T_1+\mathsf{\sum}_{j \in J' }b_j.\omega$  to
make a difference between $s$ and $t$. Because of this and by
Definitions \ref{def:Results} and \ref{def:pafter}  it follows  that

 \begin{align}\label{eq:thebig}
&\sum_{M \in \mathcal{M}_n^C \cap \mathcal{M}_{n-1}^C \cap
\cdots \cap
\mathcal{M}_1^C}\frac{a_1}{a_1}P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))  \notag\\
+&\sum_{M \in \mathcal{M}_n^C \cap \mathcal{M}_{n-1}^C \cap
\cdots \cap
\mathcal{M}_1}\frac{a_1}{a_1+b_1}P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))  \notag\\
+&\cdots \notag\\
+&\sum_{M \in \mathcal{M}_n   \cap \cdots \cap
\mathcal{M}_1}\frac{a_1}{a_1+\sum_{j=1}^{n}b_j}P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))\notag\\
=& \quad 0.
\end{align}

\noindent Each intersection appearing under the $\sum$-operators of
\eqref{eq:thebig} can be mapped bijectively to a binary number of
$n$ digits -- the i-th digit being $0$ if the intersection contains
$\mathcal{M}_{n+1-i}^C$, and $1$ if the intersection contains
$\mathcal{M}_{n+1-i}$. (For reasons that will become clear later,
the order of the indexing is reversed.)

Suppose  $\mathsf{Result}(s,T) = \mathsf{Result}(t,T)$ for every test
$T=a_1.T_1+\mathsf{\sum}_{j \in J' }b_j.\omega$, where $J'\subseteq J$.
We shall prove that, in this case, every sum
$\sum(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))$
that appears in \eqref{eq:thebig} when $J'=J$ is equal to a
zero-function. In particular, the equality

\begin{equation}\label{eq:presek}
\sum_{M \in \bigcap_{j \in
J}\mathcal{M}_j^C}(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))=0
\end{equation}

\noindent will hold. Note  that the set $\bigcap_{j \in
J}{\mathcal{M}_j^C}$ contains all first-level menus of $s$ that have
the action $a_1$ but do not have any other action that does not
appear in $M_1$. Therefore, $\bigcap_{j \in J}{\mathcal{M}_j^C}$
consists of the subsets of $M_1$ that contain $a_1$. Thus, the
equation \eqref{eq:presek} is equivalent to the equation
\eqref{eq:submenus} which leads to $\mathsf{Result}(s_{(M_1,a_1)},T_1)
=\mathsf{Result}(t_{(M_1,a_1)},T_1)$, i.e. to  contradiction. This would complete the proof of the theorem.\\

We now proceed with proving the above stated claim. We prove a more
general result,  namely that for $J' \subseteq J$, under assumption
that $\mathsf{Result}(s,T) = \mathsf{Result}(t,T)$ for every test
$T=a_1.T_1+\mathsf{\sum}_{i \in J'' }b_i.\omega$ such that $J'' \subseteq
J$ and $|J''|\leq|J'|$, it holds that every sum
$\sum(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))$
that appears in \eqref{eq:thebig} is equal to zero. \\%The proof is

Suppose first that $|J'|=1$, i.e. $J'=\{1\}$. Assume that
\begin{equation}\label{eq:eden1}
\mathsf{Result}(s,a_1.T_1) = \mathsf{Result}(t,a_1.T_1)
\end{equation}
  and
\begin{equation}\label{eq:eden2}
\mathsf{Result}(s,a_1.T_1+b_1.\omega) = \mathsf{Result}(t,a_1.T_1+b_1.\omega).
\end{equation}
 From \eqref{eq:eden1}, Def. \ref{def:Results}, and because $P_s^1(M)=P_t^1(M)$ for every menu $M$, we  obtain

\begin{align}\label{eq:b1}
\sum_{M \in \mathcal{M}_1 \cup \mathcal{M}_1^C
}\frac{a_1}{a_1}P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))=0.
\end{align}
The equation \eqref{eq:thebig} turns into
\begin{align}\label{eq:b2}
& \sum_{M \in \mathcal{M}_1^C}\frac{a_1}{a_1}P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))\notag\\
+ & \sum_{M \in
\mathcal{M}_1}\frac{a_1}{a_1+b_1}P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))\notag
\\
= & \quad 0.
\end{align}

Denote $\sum_{M \in
\mathcal{M}_1^C}P_a^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))$
by $x_0$ and $\sum_{M \in
\mathcal{M}_1}P_a^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))$
by $x_1$. Our goal is to show  that $x_0=0$ and $x_1=0$, i.e. that
they are zero-functions.  From \eqref{eq:b1} and \eqref{eq:b2} we
obtain the following system of equations for the unknowns $x_0$ and
$x_1$:
$$
\begin{cases}{}
\frac{a_1}{a_1}x_0  +  \frac{a_1}{a_1+b_1}x_1  =0\\
x_0  +  x_1  =0,
\end{cases}
$$

 \noindent or in a matrix form $$ \mathbf{Q_1}\mathbf{x}=\mathbf{0},$$ where
$$\mathbf{Q_1}=\left(
                      \begin{array}{cc}
                        \frac{a_1}{a_1} & \frac{a_1}{a_1+b_1} \\
                        1 & 1 \\
                      \end{array}
                    \right), \mathbf{x}=\left(
                                            \begin{array}{c}
                                              x_1 \\
                                              x_2 \\
                                            \end{array}
                                          \right)
                    , \textrm{ and } \mathbf{0}=\left(
                                         \begin{array}{c}
                                           0 \\
                                           0 \\
                                         \end{array}
                                       \right).
                    $$
Since the determinant of the matrix $\mathbf{Q_1}$ is not a
zero-function, it follows that $x_0=0$ and $x_1=0$ is the only
solution of
the system.\\

To present a better intuition on the proof in the general case, we
shall also consider separately  the case $|J'|=2$. Let $J'=\{1,2\}$
and assume that $\mathsf{Result}(s,T) = \mathsf{Result}(t,T)$ for every test
$T=a_1.T_1+\mathsf{\sum}_{i \in J'' }b_i.\omega$ such that $J'' \subseteq
J$ and $|J''|\leq|J'|$. The equation \eqref{eq:thebig} turns into

 \begin{align}\label{eq:thebig2}
& \sum_{M \in \mathcal{M}_2^C \cap \mathcal{M}_1^C}\frac{a_1}{a_1}P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))  \notag\\
+& \sum_{M \in \mathcal{M}_2^C \cap \mathcal{M}_1}\frac{a_1}{a_1+b_1}P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))  \notag\\
+& \sum_{M \in \mathcal{M}_2 \cap \mathcal{M}_1^C}\frac{a_1}{a_1+b_2}P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))  \notag\\
+& \sum_{M \in \mathcal{M}_2 \cap \mathcal{M}_1}\frac{a_1}{a_1+b_1+b_2}P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))\notag\\
=& \qquad 0.
\end{align}

Denoting   $\sum_{M \in \mathcal{M}_2^C \cap \mathcal{M}_1^C
}P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))$
by $x_{00}$ and so on, \eqref{eq:thebig2} turns into
\begin{align}
\frac{a_1}{a_1}x_{00} + \frac{a_1}{a_1+b_1}x_{01} +
\frac{a_1}{a_1+b_2} x_{10} + \frac{a_1}{a_1+b_1+b_2} x_{11}=0.
\end{align}

From $\sum_{M \in
\mathcal{M}_2^C}P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))=0$
we obtain $x_{00}+x_{01}=0$, and from $\sum_{M \in
\mathcal{M}_2}P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))=0$
we obtain $x_{10}+x_{11}=0$. Similarly, from $\sum_{M \in
\mathcal{M}_1}P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))=0$
we obtain that $x_{01}+x_{11}=0$. Therefore, we have the following
system of equations:

$$
\begin{cases}{}
\frac{a_1}{a_1}x_{00} + \frac{a_1}{a_1+b_1}x_{01} +
\frac{a_1}{a_1+b_2} x_{10} + \frac{a_1}{a_1+b_1+b_2} x_{11}=0\\
x_{00}+x_{01}=0\\
x_{01}+x_{11}=0 \\
 x_{10}+x_{11}=0.
\end{cases}
$$

The main matrix of the system is $$\mathbf{Q_2}= \left(
  \begin{array}{cccc}
    \frac{a_1}{a_1} & \frac{a_1}{a_1+b_1} & \frac{a_1}{a_1+b_2} & \frac{a_1}{a_1+b_1+b_2} \\
    1 & 1 & 0 & 0 \\
    0 & 1 & 0 & 1 \\
    0 & 0 & 1 & 1 \\
  \end{array}
\right). $$

By Lemma \ref{lem:determinant}, $\mathsf{Det}(\mathbf{Q_2})$ is not a
zero-function, which implies that the vector of zero-functions is
the only solution of the above system of equations.\\

We now present how each matrix $\mathbf{Q_{n+1}}$ can be obtained
from the matrix $\mathbf{Q_{n}}$.

In general, for $\mathcal{M}_i^* \in
\{\mathcal{M}_i,\mathcal{M}_i^C\}$, it holds

\begin{align}
&\sum_{M \in (\bigcap_{i=1}^n{\mathcal{M}_i^*}) \cap
\mathcal{M}_{n+1}}
P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))
\notag \\
+& \sum_{M \in (\bigcap_{i=1}^n{\mathcal{M}_i^*}) \cap
\mathcal{M}_{n+1}^{C}}
P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1))
\notag \\
=& \ \ \ \ \sum_{M \in (\bigcap_{i=1}^n{\mathcal{M}_i^*})}
P_s^1(M)(\mathsf{Result}(s_{(M,a_1)},T_1)-\mathsf{Result}(t_{(M,a_1)},T_1)).
\end{align}

This means that, in the general case, each solution $x_{i_1 i_2
\ldots i_n}=0$ of the system $\mathbf{Q_n}\mathbf{x}=\mathbf{0}$
generates  the following equations for the next system: \[x_{i_1 i_2
\ldots i_{k} 0 i_{k+1} \ldots i_{n}} + x_{i_1 i_2 \ldots i_{k} 1
i_{k+1} \ldots
i_{n}}=0,\] for every $0\leq k \leq n$.
For example, in case $|J'|=3$ we obtain the following matrix:
$$\mathbf{Q_3}=\left(
              \begin{array}{cccccccc}
                \frac{a_1}{a_1} & \frac{a_1}{a_1+b_1} & \frac{a_1}{a_1+b_2} & \frac{a_1}{a_1+b_1+b_2} & \frac{a_1}{a_1+b_3} & \frac{a_1}{a_1+b_1+b_3} & \frac{a_1}{a_1+b_2+b_3} & \frac{a_1}{a_1+b_1+b_2+b_3} \\
                1 & 1 & 0 & 0 & 0 & 0 & 0 & 0 \\
                0 & 1 & 0 & 1 & 0 & 0 & 0 & 0 \\
                0 & 0 & 1 & 1 & 0 & 0 & 0 & 0 \\
                0 & 0 & 0 & 1 & 0 & 0 & 0 & 1 \\
                0 & 0 & 0 & 0 & 1 & 1 & 0 & 0 \\
                0 & 0 & 0 & 0 & 0 & 1 & 0 & 1 \\
                0 & 0 & 0 & 0 & 0 & 0 & 1 & 1 \\
              \end{array}
            \right).
$$
Note that each row of $\mathbf{Q_3}$, except the first one, contains
exactly two $1$'s, at positions whose binary representations differ
in exactly one place (for example at the positions $001$ and $011$).

Informally, the general algorithm for obtaining the elements
$q_{n+1}^{ij}$ of a $2^{n+1}\times 2^{n+1}$ matrix
$\mathbf{Q}_{n+1}$ from matrix $\mathbf{Q}_n$, assuming
$\mathbf{Q}_n$ is non-singular, is as follows. First, initialize all
elements of $\mathbf{Q}_{n+1}$ to zero. Then, copy $\mathbf{Q}_{n}$
into the upper left corner of $\mathbf{Q}_{n+1}$. Then, copy
$\mathbf{Q}_{n}$, excluding the first row, into the lower right
corner of $\mathbf{Q}_{n+1}$. Then, assign $1$ to $q_{n+1}^{ij}$ for
$i=2^n+1$ and $j \in \{2^n, 2^{n+1}\}$. Finally, add the appropriate
new rational fractions in the second half of the first row of
$\mathbf{Q}_{n+1}$. The key observation is that in this way, we
obtain again a matrix such that each row, except the first one,
contains exactly two $1$'s, at positions whose binary
representations differ in exactly one place. Formally,
\[ q_{n+1}^{ij}=
\begin{cases}{}
q_n^{ij} & \textrm{if } 1 \leq i \leq 2^n \textrm{ and } j \leq 2^n, \\
1 & \textrm{if } i=2^n+1 \textrm{ and } j \in \{2^n, 2^{n+1}\}, \\
q_n^{ij} & \textrm{if } 2^n+1<i \textrm{ and } 2^n <j, \\
\frac{a_1}{a_1+\sum_{k \in K}{b_k}+b_{n+1}} & \textrm{if } i=1,j>2^n, \textrm{ and }  q_n^{(i) (j-2^n)}= \frac{a_1}{a_1+\sum_{k \in K}{b_k}}\\%,  n+1 \not \in K\\% b_{n+1} \not \in \{b_k\}_{k \in K}\\
0 & \textrm{otherwise}.
\end{cases}
\]

Assuming matrix $\mathbf{Q}_{n}$ satisfies the conditions of Lemma
\ref{lem:determinant}, it easily follows that  matrix
$\mathbf{Q}_{n+1}$ also satisfies the conditions of Lemma
\ref{lem:determinant}. Therefore, its determinant is  not a zero
function. This means that the system
$\mathbf{Q}_{n+1}\mathbf{x}=\mathbf{0}$ has only zero-functions as
solutions, which we were aiming to prove. Therefore, the proof of
the theorem is complete.
\end{LONGVERSION}
\end{proof}

From Theorems \ref{thm:desno_levo} and \ref{thm:levo_desno} the
following statements directly follow.
\begin{corollary} For arbitrary processes $s$ and $t$,  $s \mathrel{\approx_{\mathcal{T}}} t$
if and only if $s \mathrel{\approx_{\obs}} t$.
\end{corollary}

\begin{corollary} For arbitrary processes $s$ and $t$,  $s \not \mathrel{\approx_{\mathcal{T}}}
t$ if and only if there exists a test $T$ without probabilistic
transitions such that $\mathsf{Result}(s,T)\not = \mathsf{Result}(t,T)$.
\end{corollary}

\section{Conclusion, future work, and related work }\label{sec:conclusion}
 \paragraph{Concluding remarks} We have proposed a testing equivalence in the style of \cite{DH84} for
processes where the internal nondeterminism is quantified with
probabilities. The testing semantics allows distribution of external
choice over probabilistic choice, i.e. accomplishes unobservability
of the internal probabilistic choice. The definition exploits a new
method for labeling the synchronized actions using rational
functions over the action labels, which, we believe, is of
independent interest. We have also developed an alternative
characterization of the testing equivalence, namely as a
probabilistic version of the ready trace equivalence
~\cite{Pnueli85, BBKready}. The definition of the latter uses
Bayesian probability. It is intuitive and can be easily justified by
a black box testing scenario akin to those in \cite{spectrum1,
CSV07}. We have also shown that it is congruence for all standard
operators for the given model, including asynchronous parallel
composition and priority.

\paragraph{Internal nondeterminism} It can be anticipated by now
that combining internal choice, probabilistic choice and parallel
composition is challenging. Again  ``cloning'' the internal
nondeterminism after the probabilistic choice in a parallel context
can ``erase'' the probabilities, which disallows distribution of
prefix over probabilistic choice (this phenomenon has been also
studied in ~\cite{CP07,CLSV06, GRS07, Lowe93, GD09,segalaPhD}).
\begin{figure}[t]\centering \large
$\xymatrix@R=0.3cm@C=0.1cm{

& X \ar@{-->}[dl]_{\frac{1}{2}} \ar@{-->}[dr]^{\frac{1}{2}} \\
          \circ\ar[d]_{wrt}  && \circ\ar[d]_{wrt}  \\%& & \circ\ar[d]_{f} && \circ\ar[d]_{c} \\
          \circ\ar[d]_{rev}  && \circ\ar[d]_{rev} \\
          \circ\ar[d]_{head}  && \circ\ar[d]_{tail}  \\%& & \circ\ar[d]_{f} && \circ\ar[d]_{c} \\

          \circ && \circ \\
           }$
 \quad $ \parallel_L $ \quad
$\xymatrix@R=0.3cm@C=0.1cm{

&  Y \ar[d]_{wrt} \\
& \circ \ar[dl]_{} \ar[dr]^{} \\
          \circ\ar[d]_{rev}  && \circ\ar[d]_{rev}  \\%& & \circ\ar[d]_{f} && \circ\ar[d]_{c} \\
          \circ\ar[d]_{head}  && \circ\ar[d]_{tail} \\
          \circ\ar[d]_{\ddot\smile} && \circ\ar[d]_{\ddot\smile} \\
          \circ && \circ \\
           }
           $
           \quad $\longrightarrow$ \quad
  $
\xymatrix@R=0.3cm@C=0.1cm{
    & & & \circ  \ar@{-->}[dll]_{\frac{1}{2}} \ar@{-->}[drr]^{\frac{1}{2}} \\
    & \circ \ar[d]_{wrt}  & & & & \circ  \ar[d]_{wrt}  \\
& \circ \ar[dl]_{} \ar[dr]^{} & & & & \circ  \ar[dl]_{} \ar[dr]^{} \\
          \circ\ar[d]_{rev}  && \circ\ar[d]_{rev}  & & \circ\ar[d]_{rev} && \circ\ar[d]_{rev} \\
          \circ\ar[d]_{head}  && \circ  & & \circ && \circ\ar[d]_{tail} \\

          \circ\ar[d]_{\ddot\smile} &&  & &  && \circ\ar[d]_{\ddot\smile} \\
          \circ &&  & &  && \circ \\
           }$
\newline
 \caption{Synchronized coin tosser($X$) and  result-guesser($Y$) } \hbox{}\vspace{-0.5cm}
 \label{fig:game1}
\end{figure}
Namely, consider the following game. The player $X$ tosses a fair
coin and hides the outcome. Player $Y$ guesses the outcome of the
tossing and writes it down. While he is writing down the result,
player $X$ waits (i.e. he may write down something meaningless).
Then they both agree to reveal their outcomes, i.e. $X$ to uncover
the coin and $Y$ to show what he/she has written.\footnote{Note the
difference between this game and the example in Sec.
\ref{sec:introduction} -- in the former there is no external choice
in the original processes, while in the latter they don't have
internal nondeterminism.} Obviously, the probability that the second
player has guessed correctly equals $\frac{1}{2}$. However, the
resulting graph for the synchronization of both players (Fig.
\ref{fig:game1}) suggests that there is a strategy such that player
$Y$ can always guess the correct result. On  the other hand, if
process $\bar{X}=wrt.rev.(head \oplus_{\frac{1}{2}} tail)$ is
synchronized with $Y$, the resulting graph suggests that the
probability of reporting a $\ddot\smile$ action is exactly
$\frac{1}{2}$. This prevents equating processes $X$ and $\bar{X}$,
i.e. allowing distribution of prefix over internal probabilistic
choice.
 Indeed, in
presence of internal nondeterminism, the testing equivalence of
\cite{YL92} and its variants have all been characterized as
simulations \cite{JY02,LSV07,DGHM08}. The proposed solutions
\cite{CP07,CLSV06, GRS07, GD09} to the problem with parallel
composition
 suggest that the process composition
needs to ``remember'' the outcome of the internal choice that a
component makes locally.
 To solve the problem in our setting in the
lines of these solutions, we  also plan to enrich the internal
transitions with labels that cannot communicate. Before composing
all labels would be different. If the original process has, for
example, two outgoing internal transitions labeled with $l_1$ and
$l_2$, then the composed process shall have transitions labeled with
$\frac{l_1}{l_1+l_2}$ and $\frac{l_2}{l_1+l_2}$.  Fig.
\ref{fig:game2} presents the result of testing process $X$ of Fig.
\ref{fig:game1} with process $Y$, assuming the internal transitions
of $Y$ are labeled with $l_1$ and $l_2$. Two processes would not be
distinguished by a test if both results of testing are equal modulo
isomorphism on the labels set. However, we leave the formal
definition of this testing semantics for future work.

\paragraph{Related Work}
\begin{wrapfigure}{r}{48mm}\centering
\large \hbox{}\vspace{-5mm} $ \xymatrix@R=0.3cm@C=0.2cm{
    & & & \circ  \ar@{-->}[dll]_{\frac{1}{2}} \ar@{-->}[drr]^{\frac{1}{2}} \\
    & \circ \ar[d]_{\frac{w}{w}}  & & & & \circ  \ar[d]_{\frac{w}{w}}  \\
& \circ \ar[dl]_{\frac{l_1}{l_1+l_2}} \ar[dr]^{\frac{l_2}{l_1+l_2}} & & & & \circ  \ar[dl]_{\frac{l_1}{l_1+l_2}} \ar[dr]^{\frac{l_2}{l_1+l_2}} \\
           \circ\ar[d]_{\frac{r}{r}}  && \circ\ar[d]_{\frac{r}{r}}  & & \circ\ar[d]_{\frac{r}{r}} && \circ\ar[d]_{\frac{r}{r}} \\
          \circ\ar[d]_{\frac{h}{h}}  &&   & & && \circ\ar[d]_{\frac{t}{t}} \\
           \circ\ar[d]_{\ddot\smile} &&  & &  && \circ\ar[d]_{\ddot\smile} \\
           \circ &&  & &  && \circ
           }$
\newline
 \caption{Testing with internal transitions.} \hbox{}\vspace{-0.5cm}
 \hbox{}\vspace{-1cm}
 \label{fig:game2}
\end{wrapfigure}
Process equivalences  that allow distribution of prefix over
probabilistic choice (i.e. unobservability of the random choice)
have been a research topic ever since probabilities were introduced
in concurrency theory (see
e.g.\cite{Lowe93,Seidel95,segalaPhD,morgan96refinementoriented,KN98b,CCVPP03,CP07,CSV07}).
However,  only \cite{Lowe93}, \cite{Seidel95}, and, under certain
conditions, \cite{CP07}, also allow distribution of external choice
over probabilistic, i.e. equate  processes $s$ and $\bar{s}$ of Fig.
\ref{fig_machine}. In~\cite{Lowe93} probabilistic versions of broom
(ready/failure) and barbed (ready/failure trace) equivalences are
defined. These definitions use ``probability functions'' that
 compute the maximal probability for a ready trace to occur
(i.e. they do not generate probability spaces over the set of ready
traces), which makes it hard to construct corresponding ``black-
box'' testing scenarios. In~\cite{Seidel95}, in the model with
external choice, a process is defined as conditional probability
measure over sequences of actions. This semantics also  identifies
processes $(a+b) \oplus_{\frac{1}{2}} c$ and $(a+c)
\oplus_{\frac{1}{2}} b$. Obviously, this is  not desirable.
In~\cite{CP07} processes are enriched with labels, and a testing
equivalence is defined by means of  schedulers that synchronize with
processes on the process labels. For a certain labeling, processes
$s$ and $\bar{s}$ can be equated. Although this is an elegant and
compositional solution to the problem of overestimating
probabilities in testing semantics, we believe that our approach is
more feasible in practice. In fact, the task of the schedulers and
the purpose of the process labels in \cite{CP07} in our testing
semantics have been accomplished by the rational functions formed
from the action labels.

\paragraph{Acknowledgements} We thank Jos Baeten and Erik de Vink
for their valuable comments on a draft version of this paper.

\bibliographystyle{plain}

redpajama_set_name: RedPajamaArXiv


be joining the jbws team as their CEO and President, remarks Diane Williams. . Company founders Noah Tepperberg and Jason Strauss were also reportedly in attendance, which begs the question, what is the minimum amount of nightclub executives one must invite to a Hamptons party? 1 in 3 teens are victims of dating abuse. He seems to fit right in with Tiffany's crew, alternatively referred to as the Snap Pack or the, rich Kids of Instagram. Dianes passion for the mission, professional skills, experience, and working relationships in Morris County make her the ideal choice to lead jbws. But another source claimed it was the second first daughter, who spent the day posting Instagram Stories of the festivities, which began on a party bus full of the kind of people who look like they laugh when they see a waiter drop a tray. Thanks to the golfers and sponsors, the event raised 154,000 to support the mission of jbws. Jbws Board Chair, amy Komoroski Wiwi and a Partner with Lowenstein Sandler, LLP (l) welcomes Diane Williams as the new President CEO to lead the agency. Beginning July 16th, Diane Williams can be reached at or Ext.
Tiffany Trump might be dating Chris Allam, a "businessman" from New York, you guys. Jbws "Painted the eronnut katolinen dating sivustot Green Purple" with balloons and staffed a table where people stopping by had a chance to learn more about the services and spin a wheel to win prizes. Consider these statistics: 1 in 4 women will be physically or sexually abused by a partner in her lifetime. A child's exposure to domestic abuse is the strongest risk factor for passing violent behavior from one generation to the next. As the Chief Operating Officer with FIS, Diane managed the internal operations with a budget of over 9 million and was actively involved in all aspects of the organization including management, finance, fundraising, grant writing, human resources, marketing, quality assurance, and program development. Why is this important? Allam attended Darien High School in Connecticut, the paper reported, then Hobart College. We offer regional, tri-state, and over the road.
Created by student leaders from Delbarton, the slogan was selected by professionals from Marketsmith at the county-wide Teens for Healthy Relationships Leadership Conference hosted by Randolph High School and sponsored by jbws last November. Testimonials "Great place to work.
Kuolleen henkilön some-tilejä ei välttämättä suljeta, sillä niillä voi olla oma osansa suruprosessissa, sanoo aiheesta väitellyt Anna Haverinen. Salon taidemuseo Veturitallissa näyttely oli esillä.1. Viikko..
This sense of being in the drivers seat, of choosing, can be appealing. But be careful not to be lulled into habits that will undermine..
M, Adobe Raising Prices on Creative Cloud Subscriptions in UK Sweden. Gear 360 julkaistiin jo viime vuoden huhtikuussa ja Suomeen se saapui käytännössä vasta vuoden..
Other examples of medieval oval domes can be found covering rectangular bays in churches. Calls a family meeting to discuss respect, compromise and honesty.
Your rights in relation to your information. Finnish Kuinka kauan kestä, ennen kuin komissio tekee velvollisuutensa ja muistuttaa Ruotsin sosiaalidemokraattista hallitusta hyvin tärkeän sopimuksen allekirjoittamisesta?


Back in June, Minnesota's Department of Employment and Economic Development (DEED) reflected on the supposed 'labor shortage' in the state. "[E]mployers in the Twin Cities will need to get creative in order to sustain economic vibrancy," DEED wrote. Some of our state's employers have been showing how to do that.
One often underappreciated issue for workers, and why some employers struggle to attract and retain employees, has to do with transportation, said John Kammeyer-Mueller, a professor at the University of Minnesota's Carlson School of Management.
It's the reason some companies are starting to create specialized transportation solutions for employees. Amazon — and its regular bus service from the Cedar-Riverside community to its fulfillment center in Shakopee — is the best-known example. But they're not alone. Kammeyer-Mueller said a manufacturing company located just across the Minnesota-Wisconsin border is also planning to put together a transportation system that would transport workers from the Twin Cities metro area.
Another thing employers have been doing, as we at the Center have spoken about before, is to reach into the parts of Minnesota's labor market where there is 'slack'. This can be found in sections with higher rates of unemployment. Primarily, these are teenagers and certain ethnic groups. As MinnPost reports, Summit Academy OIC President and CEO Louis King, goes into minority neighborhoods and churches to advertise employment opportunities.
A free economy has more potential to generate widespread wealth than any other system in human history. If it is allowed to be free, that is. What the 'labor shortage' really means is that demand for labor is greater than supply at the current price. At some higher price, wages in this case, supply and demand will reach equilibrium. As we've said before, the current labor market situation represents an opportunity to see wage growth. It represents an opportunity to bring in sections of the community which have, traditionally, struggled to get into the workforce. Minnesota's businesses are leading the way.


text:
Private Space Habitat to Launch in 2020 Under Commercial Spaceflight Deal
By Mike Wall 2016-04-12T00:19:01Z Spaceflight
This cutaway shows a concept B330 space habitat for astronauts designed by Bigelow Aerospace. The private spaceflight company has teamed up with launch provider United Launch Alliance to put a huge private space habitat in orbit by 2020.
(Image: © Bigelow Aerospace)
Two aerospace companies are teaming up to launch giant space habitats to orbit, with the first such liftoff targeted for 2020.
Bigelow Aerospace will loft its giant, expandable B330 modules — each of which will provide one-third as much usable volume as the entire International Space Station (ISS) — aboard United Launch Alliance (ULA) Atlas V rockets, representatives from both companies announced today (April 11).
The agreement marks the first commercial partnership between a launch provider and a space-habitat provider, ULA representatives said. [Bigelow Aerospace's Inflatable Space Stations in Images]
Two B330s should be ready to go by 2020, and the goal is to launch at least one of the modules that year. The first B330 would ideally be attached to the ISS, which would require NASA's approval, said Bigelow Aerospace founder and president Robert Bigelow. But the module could also operate on its own, flying freely in space, he added.
"Each [B330] is able to be its own space station," Bigelow said during a press briefing today at the 32nd Space Symposium in Colorado Springs, Colorado. "They need no other habitats, modules or anything of the sort."
This United Launch Alliance diagram shows how the launch provider's Atlas V rocket will carry a Bigelow Aerospace B330 expandable habitat module into orbit. The private space habitat is slated to launch in 2020 under a deal between the two companies.
(Image credit: United Launch Alliance)
This first orbiting B330 — which is so named because it contains 330 cubic meters, or about 11,650 cubic feet, of internal volume — could house visiting space tourists and accommodate a variety of scientific experiments, Bigelow said. Indeed, it's likely that these modules will serve multiple purposes and customers, operating on a time-share basis.
"We're offering discrete quantities of time — a matter of one or two weeks to maybe 45 days — to various kinds of clientele, and also certain areas onboard the spacecraft that we have permission for that clientele to locate packages and experiments that was the motivation for them to be there," Bigelow said.
Bigelow Aerospace's BEAM expandable module will enhance the living area of the International Space Station. See how the BEAM module works in our full infographic.
(Image credit: Karl Tate, SPACE.com contributor)
Bigelow and ULA president and CEO Tory Bruno see their companies' partnership as a watershed moment for humanity's exploration and exploitation of space.
The first B330s should allow for greatly expanded opportunities for researchers, companies and space tourists in low Earth orbit, they said, and the modules could eventually allow for human habitation on and around the moon, and even as far away as Mars.
"We are standing on the very threshold of an expanded and permanent human presence beyond our planet," Bruno said at today's briefing. "This is a very bright future, and you and I right now are standing here, looking right into it."
Bigelow Aerospace founder Robert Bigelow speaks with reporters on April 11, 2016 during the announcement of a partnership with United Launch Alliance to launch an expandable space habitat for astronauts by 2020.
(Image credit: Calla Cofield/Space.com)
Las Vegas-based Bigelow Aerospace specializes in building habitats that launch in a compressed configuration and expand greatly once they reach space. Such expandable modules offer much more usable volume per unit launch mass than do traditional rigid structures.
Bigelow has already flown three expandable modules in space — the free-flying Genesis 1 and Genesis 2 prototypes, which launched in 2006 and 2007, respectively, and the Bigelow Expandable Activity Module, which just arrived at the ISS aboard SpaceX's Dragon cargo capsule this weekend.
The goal of BEAM — which offers just 5 percent the volume of a B330 — is to prove out expandable technology for human use on orbit. It will stay attached to the ISS for the next two years.
The partnership between Bigelow and ULA is very much a work in progress, and there's still a lot to work out in terms of how the launch of the first B330 (and any others that follow) will be funded, Bruno and Bigelow said.
NASA might end up paying for the first launch if the B330 goes to the ISS, Bruno said. But he stressed that other opportunities could present themselves as well.
"It's premature to talk in specifics about these kinds of things," Bigelow said.
Follow Mike Wall on Twitter @michaeldwall and Google+. Follow us @Spacedotcom, Facebook or Google+. Originally published on Space.com.
Hey, Star Wars Fans! Check Out These Amazon Prime Day Deals
Pictures from Space! Our Image of the Day
Watch Today! NASA Celebrates Apollo 11 Moon Launch Anniversary
New Sci-Fi Series 'Pandora' Launches on CW Tonight!
Hundreds Demonstrated Against Poverty at Apollo 11 Moon Launch

redpajama_set_name: RedPajamaCommonCrawl


text:
Meet Kent
Like many of us at CMBA, Kent had a grandfather who was a carpenter. He loved spending time with him on job sites, and Kent also had an uncle who was an architect. He discovered at a young age that his artistic gifts and interest in building were a perfect blend for a career in architecture. Kent grew up in the central Kansas town of Great Bend – surrounded by a rural life of oil wells, agriculture, wetlands, and wildlife. After graduating from the University of Kansas, he started his career working for a small firm in his home state. Within a few years, Kent joined CMBA's Des Moines office and was promoted to an Associate Principal in 2015. Kent has a passion for collegiate and healthcare spaces. When asked about his favorites, the Learning Commons at University of Iowa is top on his list. He loves the dramatic transformation from an underutilized, drab space – to a vibrant, open, collaborative, and highly utilized student space that has exceeded people's expectations. Kent's other passion – family. Kent, and his wife Melanie, have one son and two daughters that keep their lives busy and full. Some lesser known facts about him? He's a tap dancer, loves college basketball, has a weakness for nice shoes, describes himself as a foody, practices yoga and is an aviation buff. Like most CMBA professionals, Kent is an active advocate for serving his community. His recent service has been with the Heritage Carousel of Des Moines Foundation, a nonprofit entity that looks to provide families of diverse backgrounds opportunities to create lasting memories on a vintage carousel. We are proud to call Kent a CMBA "Champion!"
Our Culture Has an Impact on Your Project
People are important to us. And we believe that allowing people the freedom and flexibility to...
CMBA Offices Temporarily Closed to Visitors
ALL CMBA ARCHITECTS OFFICE LOCATIONS WILL BE CLOSED TO VISITORS STARTING THURSDAY, MARCH 19TH UNTIL...
A Message from CMBA Architects on COVID-19
As we continue to monitor COVID-19 and take precautions in our own lives, we want to share what...
Contact us for more information and for all of your project inquiries.
Our offices across Iowa and Nebraska have specialists ready to work on projects throughout the country. Learn more about each office below and reach out to discuss your next project.
©2023 CMBA Architects. All Rights Reserved


In our never-ending search for high quality beef, we ran into a group of Uruguayans who have over 20 years of experience cross-breeding. A few years ago they started experimenting with Wagyu-Angus, and now... its arrived stateside.
Is it as good as Wagyu A5? No it isnt. But it also is nowhere near as expensive.
Our Prime+ is a Premium Steak priced slightly above Choice, on par with Prime (sometimes a little more expensive). This is a steak you can enjoy EVERY DAY if you wished to.
Simply put, cross bred Wagyu is an affordable addition to our lineup.


text:
Q: Writing script to retrieve number I want to cut the number and unit to save as number only in a file.
The input is:
Data byte rate:      24 bytes/s
Average packet size: 118.59 bytes
Data byte rate:      2 Kbytes/s
Average packet size: 10 Kbytes

the expected output is:
24
118.59
2000
10000

This is what I have done so far to retrieve only number.
sed -r 's/.* ([0-9]+\.*[0-9]*).*?/\1/'

A: In order to do the format conversion, you could capture and preserve the optional multiplier and then pipe the result into numfmt
So
$ sed -r 's/.* ([0-9]+\.?[0-9]*)[ \t]*([kKMGTP])?.*/\1\U\2/' input
24
118.59
2K
10K

which becomes
$ sed -r 's/.* ([0-9]+\.?[0-9]*)[ \t]*([kKMGTP])?.*/\1\U\2/' input | numfmt --from si
24
118.59
2000
10000

redpajama_set_name: RedPajamaStackExchange


Melissa J. Patneaude, 40, formerly of Rumford, passed away in her sleep on March 11, 2019.
Melissa was born on January 13, 1979 to Roland and Gloria (Daigle) Patneaude.
Melissa attended Mountain Valley High School, graduating with the Class of 1997. A stay at home mom, Melissa lived her life for her children.
There was nothing she loved or cared about more then them. She may not be here with us in the present but her memory lives on in the hearts and minds of those that she loved. Melissa is survived by her parents, Roland and Gloria Patneaude; two daughters, Morgan Theriault, and Chloe Lill and a son, Chase Lill; her sister Renee Hodsdon and husband Roy; her fiancee Christopher Lill; grandparents, aunts, uncles and cousins.
A Celebration of Missy's life will be held from 1-4 p.m. on Sunday, March 24 at the Dixfield American Legion Post 100.
In lieu of flowers, contributions can be made to help defer the cost incurred at this difficult time.
Please send contributions to Morgan Theriault, 78 Harlow Hill Road, Mexico, ME 04257.
Want to get notified whenever we write about Gallant Funeral Home ?
Next time we write about Gallant Funeral Home, we'll email you a link to the story. You may edit your settings or unsubscribe at any time.


text:
Tulsa Elementary Students Treated For Drug Use
Friday, March 5th 2010, 4:19 PM CST
Saturday, March 6th 2010, 1:43 PM CST
EMSA transported three Walt Disney Elementary School students -- an 11-year-old boy, a 12-year-old boy and an 11-year-old girl.
NewsOn6.com
TULSA, OK -- Three students from Walt Disney Elementary School were transported to Tulsa hospitals Friday to be examined after taking a prescription muscle relaxant.
The drug use happened after a young girl handed out the drug to friends, according to Tami Marler, Tulsa Public Schools. The girl was one of the students transported.
EMSA transported three students -- an 11-year-old boy, a 12-year-old boy and an 11-year-old girl. EMSA paramedics also assessed five additional patients on scene, but none of those children were transported by ambulance to hospitals.
School officials said they believe the girl got the pills from her parents' medicine cabinet.
"Right now, our main concern is that child's health. We definitely want to figure out where that child is and help that child to ensure that something like this doesn't happen in the future," said Millard L House II, Assistant Superintendent for Elementaries.
There is no word yet on what punishment the child faces.
Walt Disney Elementary is located at 11702 E. 25th Street.