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

˄
−ₒ k ·

˄
−ₒ k + 1 ·

˄
−ₒ k + 2 ···

As we h ave seen, by taking transitio ns s we have

1

s ⃒

k ·

0 for any k ≥ 2; but crucially s ⃒ ʵ . Since trivially 0 ⃒ ʵ there is no

full distribution ʔ such that ʔ ⃒ ʵ .
Now to contradict the distillation of divergence for this pLTS, n o te that s

1

⃒

2 ·

0 ,

( ʔ 1 p ↕ ʔ ʵ ),

but this derivation cannot be factored in the required manner to s ⃒

because no possible full distribution ʔ ʵ can exist satisfying ʔ ʵ ⃒ ʵ .

Corollary 6.8 and Lemma 6.19 are not affected by infinite branching, because
they are restricted to the deterministic case (i.e. the case of no branching at all).
What fails is the combination of a number of deterministic distillations to make a
nondeterministic one, in Theorem 6.11 : it depends on Theorem 6.9 , which in turn
requires finite branching.
Corollary 6.9 (Zero-One Law - General Case) If in a finitary pLTS we have ʔ , ʔ
with ʔ then there is some state s reachable with non-zero

probability from ʔ such that s ⃒

ʔ and ʔ | ⃒ | ʔ | > |

ʵ. That is, the pLTS based on ʔ must have a

wholly diverging state somewhere.

Proof Assume at first that | ʔ |= 1; then the result is immediate from Theorem 6.11

since any s ∈ ʔ ʵ

will do. The general result is obtained by dividing the given

| |

derivation by ʔ .

6.6 The Failure Simulation Preorder

We have already defined a failure simulation preorder in Definition 5.5, which looks
natural for finite processes. However, for general processes divergence often exists,
which makes it subtle to formulate a good notion of failure simulation preorder.
This section is divided in four: the first subsection presents a definition of the
failure simulation preorder in an arbitrary pLTS by taking divergence into account,
together with some explanatory examples. It gives two equivalent characterisations
of this preorder: a coinductive one as a largest relation between subdistributions
satisfying certain transfer properties, and one that is obtained through lifting and
an additional closure property from a relation between states and subdistributions
that we call failure similarity . It also investigates some elementary properties of
the failure simulation preorder and of failure similarity. In the second subsection,
we restrict attention to finitary processes, and on this realm characterise the failure
simulation preorder in terms of a simple failure similarity . All further results on the
failure simulation preorder, in particular precongruence for the operators of rpCSP
and soundness and completeness with respect to the must testing preorder, are in
terms of this characterisation, and hence pertain to finitary processes only. The third
subsection establishes monotonicity of the operators of rpCSP with respect to the
failure simulation preorder. In other words, we show that the failure simulation
preorder is a precongruence with respect to these operators. The last subsection is
devoted to showing soundness with respect to must testing. Completeness is the
subject of Sect. 6.7 .