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

Sect. 5.5.2, but here there is a significant extra proof obligation; in order to relate two
processes we have to demonstrate that if the first diverges then so does the second.
Here, in order to avoid such complications, we introduce yet another version of
failure simulation; it modifies Definition 6.21 by checking divergence coinductively
instead of using a predicate.

C
FS

Definition 6.22 Define to be the largest relation in S × D sub ( S ) such that if

C

s

FS ʘ then
1. whenever s

˄
−ₒ⃒ ʵ , there are some ʔ , ʘ such that s ʔ ⃒ ⃒ ⃒ ʵ ,

˄
−ₒ⃒ ʘ and ʔ (

FS ) † ʘ ; otherwise

ʘ ⃒

ʱ
−ₒ

ʱ
⃒ ʔ , for some ʱ Act ˄ , then there is a ʘ with ʘ ʘ and

2. whenever s ∈

FS ) † ʘ and
3. whenever s

ʔ (

A A

−ₒ then ʘ ⃒ −ₒ .

Lemma 6.24 The following statements about divergence are equivalent.

(1) ʔ ʵ.

(2) There is an infinite sequence ʔ

⃒

˄
−ₒ

˄
−ₒ

˄
−ₒ

ʔ 1 ʔ 2 ....

˄
−ₒ⃒ ʔ 1 ⃒

˄
−ₒ⃒ ʔ 2 ⃒

˄
−ₒ⃒ (3) There is an infinite sequence ʔ ⃒

....

Proof By the definition of weak transition, it is immediate that (1) ⃔ (2). Clearly,

we have (2) (2), we introduce another characterisation of

divergence. Let ʔ be a subdistribution in a pLTS L .A pLTS induced by ʔ isapLTS
whose states and transitions are subsets of those in L and all states are reachable
from ʔ .

⃒ (3). To show that (3) ⃒

(4) There is a pLTS induced by ʔ where all states have outgoing ˄ transitions.

It holds that (3) (4) because we can construct a pLTS whose states and transitions

are just those used in deriving the infinite sequence in (3). For this pLTS, each state
has an outgoing ˄ transition, which gives (4)

⃒

⃒ (2).

FS by checking divergence

The next lemma shows the usefulness of the relation

in a coinductive way.

FS ) † ʘ and ʔ

C

ʵ. Then there exist ʔ , ʘ such that

Lemma 6.25 Suppose ʔ ( ⃒

˄
−ₒ⃒

˄
−ₒ⃒

FS ) † ʘ .

⃒

ʔ ⃒

⃒

ʘ, and ʔ (

ʔ ʵ, ʘ

FS ) † ʘ and ʔ

C

Proof Suppose ʔ ( ⃒ ʵ . In analogy with Proposition 6.8 , we can

FS is convex. By Corollary 6.1 , we can decompose ʘ as s ∈ ʔ

show that ʔ ( s ) · ʘ s

C

and s

FS ʘ s for each s ∈ ʔ

. Now each s must also diverge. So there exist

˄
−ₒ⃒

˄
−ₒ⃒

FS ) † ʘ s

ʔ s , ʘ s such that s ʔ s ⃒ ʘ s and ʔ s (

⃒ ʵ , ʘ s ⃒

. Let ʔ = s ∈ ʔ ʔ s and ʘ = s ∈ ʔ ʘ s .By

for each s ∈ ʔ ʔ ( s ) · ʔ ( s ) ·

FS ) †

˄
−ₒ⃒ Definition 6.2 and Theorem 6.5 (i), we have ʔ (

C

ʘ , ʔ ʔ , and

⃒

˄
−ₒ⃒

ʘ . We also have that ʔ ⃒ ʵ because for e ach state s in ʔ it ʘ ⃒

holds that s ∈ ʔ s for some ʔ s and ʔ s ⃒ ʵ , which means s ⃒ ʵ .