Testing Finite Probabilistic Processes - Semantics of Probabilistic Processes: An Operational Approach - page 116

1, as a may test, the test a.ˉ
does not differentiate between the two processes a b and a b . In fact, we have
( a b )

Since max ( A ( a.ˉ , a b )) = max ( A ( a.ˉ , a b )) =

pmay ( a b ), but this cannot be shown so
easily, as we would have to consider all possible tests. In Sect. 5.5 we will develop a
tool to prove statements P

pmay ( a b ), and even ( a b )

pmay Q , and apply it to derive the equality above (axiom

( May0 ) in Fig. 5.8 ).

5.5 Forward and Failure Simulation

The examples of Sect. 5.3 have been all negative, because one can easily demonstrate
an inequivalence between two processes by exhibiting a test that distinguishes them in
the appropriate manner. A direct application of the definition of the testing preorders
is usually unsuitable for establishing positive results, as this involves a universal
quantification over all possible tests that can be applied. To give positive results
of the form P pmay Q (and similarly for P pmust Q ) we need to come up with a

preorder finer such that ( P finer Q ) ⃒ ( P pmay Q ) and statements P finer Q can

be obtained by exhibiting a single witness.
In this section we introduce coinductive relations: forward simulations and failure
simulations .For may testing we use forward simulations as our witnesses, and for
must testing we use failure simulations as witnesses. The definitions are somewhat
complicated by the fact that in a pLTS transitions go from states to distributions;
consequently, if we are to use sequences of transitions, or weak transitions a

⃒
that abstract from sequences of internal actions that might precede or follow the a
transition, then we need to generalise transitions so that they go from distributions
to distributions. We first recall the mathematical machinery developed in Sect. 3.3,
where we have discussed various ways of lifting a relation R ↆ S × S to a relation

†

R ↆ D ( S ) × D ( S ). Exactly the same idea can be used to lift a relation R ↆ S × D ( S )

†

to a relation R ↆ D ( S ) × D ( S ). This justifies our slight abuse of notation here of

†

keeping writing R for the lifted relation.

Definition 5.3 Let R ↆ S × D ( S ) be a relation from states to subdistributions.

†

Then R ↆ D ( S ) × D ( S ) is the smallest relation that satisfies:

† ʘ , and

(1) s R ʘ implies s R

I implies ( i ∈ I p i · ( i ∈ I p i ·

† ʘ i for all i †

(2) (Linearity) ʔ i R ∈ ʔ i ) R ʘ i ),

where I is a finite index set and i ∈ I p i =

1.

From the above definition we immediately get the following property.

† ʘ if and only if there is a collection of states

Lemma 5.3 ʔ R { s i } i ∈ I , a collection

of distributions { ʘ i } i ∈ I and a collection of probabilities { p i } i ∈ I , for some finite index

set I , such that i ∈ I p i =

1 and ʔ , ʘ can be decomposed as follows:

= i ∈ I p i ·

1. ʔ s i

= i ∈ I p i ·

2. ʘ ʘ i

3. For each i ∈ I we have s i R ʘ i .