Testing Finitary Probabilistic Processes - Semantics of Probabilistic Processes: An Operational Approach - page 193

Our final examples pursue the consequences of the fact that the empty distribution
ʵ is behaviourally indistinguishable from divergent processes like [[ rec x.x ]] .

Example 6.19 (Subdistributions formally unnecessary) For any subdistribution ʔ ,
let ʔ e denote the (full) distribution defined by

ʔ e :

= ʔ + (1 −| ʔ | ) · [[ rec x.x ]] .

Intuitively, it is obtained from ʔ by padding the missing support with the divergent
state [[ rec x.x ]] .
Then ʔ FS ʔ e . This follows because ʔ e ⃒ ʔ , which is sufficient to estab-

FS ) †

lish ʔ e FS ʔ ; but also ʔ e

e e

( ʔ because [[ rec x.x ]]

FS ʵ , and that implies

FS ʔ e . The equivalence shows that formally we have no need for
subdistributions and that our technical development could be carried out using (full)
distributions only.
But abandoning subdistributions comes at a cost; the definition of weak transition,
Definition 6.4 , would be much more complex if expressed with full distributions, as
would syntactic manipulations such as those used in the proof of Theorem 6.6 .
More significant, however is that, diverging processes have a special character in
failure simulation semantics. Placing them at the bottom of the

the converse ʔ

FS preorder—as
we do—requires that they failure-simulate every processes, thus allowing all visible
actions and all refusals and so behaving in a sense “chaotically”; yet applying the
operational semantics of Fig. 6.2 to rec x.x literally would suggest exactly the oppo-
site, since rec x.x allows no visible actions (all its derivatives enable only ˄ ) and no
refusals (all its derivatives have ˄ enabled). The case analyses that discrepancy would
require are entirely escaped by allowing subdistributions, as the chaotic behaviour
of the diverging ʵ follows naturally from the definitions, as we saw in Example 6.16 .
We conclude with an example involving divergence and subdistributions.

Example 6.20 For 0 ≤ c ≤ 1 let P c be the process 0 c ↕ rec x.x . We show that

c . (Refusals can be ignored, since P c refuses every set

[[ P c ]] FS [[ P c ]] just when c ≤

of actions, for all c .)
Suppose first that c c , and split the two processes as follows: ≤

( c − c ) [[ P c ]] = c · [[ 0 ]] + c ) · [[ rec x.x ]] + (1 − · [[ rec x.x ]]

= ·

[[ 0 ]]

+

( c −

·

[[ 0 ]]

+ −

c )

·

[[ rec x.x ]]

[[ P c ]] c c ) (1 .

e FS

Because 0 [[ rec x.x ]] (the middle terms), we have immediately

e FS ) †

[[ P c ]] ( FS [[ P c ]] .

For the other direction, note that [[ P c ]]

[[ P c ]], whence [[ P c ]]

⃒

c · [[ 0 ]] . I f [[ P c ]]

FS [[ P c ]], then from

ʘ for some subdistribution
ʘ , a derivative of weight not more than c . But the smallest weight P c can reach via
⃒

⃒

c ·

Definition 6.19 we would have to have [[ P c ]]

is just c , so that we must have in fact c ≤ c .
We end this subsection with two properties of failure similarity that will be useful
later on.