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

ʔ = ʔ 0 + ʵ

˄
−ₒ ʔ 0 ʔ 1 + ʵ

. .

˄
−ₒ

+

ʔ k − 1 ʵ ʔ k

˄
−ₒ ʵ + ʵ
. —

ʵ

In total: ʘ

This implies that is indeed a generalisation of the standard notion for non-

probabilistic transition systems of performing an indefinite sequence of internal ˄
moves.
In Sect. 5.5, we wrote s

⃒

˄
−ₒ

ˆ ˄

−ₒ

ʔ , if either s ʔ or ʔ = s . Hence, the lifted

˄
−ₒ

˄
−ₒ

ʔ if and only if there are ʔ ₒ , ʔ × and ʔ 1 with

relation satisfies ʔ

˄
−ₒ

˄
−ₒ ʔ ₒ + ʔ × , ʔ ₒ ʔ 1 and ʔ = ʔ × . Clearly, ʔ ʔ implies

ʔ = ʔ 1 +

˄
−ₒ

ʔ . With a little effort, one can also show that ʔ

ʔ implies ʔ

ʔ .

ʔ ⃒ ⃒

In fact, this follows directly from the reflexivity and transitivity of ⃒ ; the latter

will be established in Theorem 6.6 .
Conversely, in Sect. 5.5.1 we dealt with recursion-free rpCSP processes P , and
these have the property that in a sequence as in Definition 6.4 with ʔ

=

[[ P ]] w e

necessarily have that ʔ k = ʵ for some k ≥ 0. On such processes we have that the

˄
−ₒ

relations coincide.

In Definition 6.4 , we can see that ʔ =

and ⃒

ʵ iff ʔ k = ʵ for all k . Thus ʔ ⃒ ʵ iff

˄
−ₒ there is an infinite sequence of subdistributions ʔ k such that ʔ = ʔ 0 and ʔ k

ʔ k + 1 , that is ʔ can give rise to a divergent computation.
Example 6.3 Consider the process rec x.x , which recall is a state, and for

˄
−ₒ

˄
−ₒ

which we have rec x.x [[ rec x.x ]] and thus [[ rec x.x ]] [[ rec x.x ]]. Then

[[ rec x.x ]]

⃒

ʵ.

Example 6.4 Recall the process Q 1 = rec x. ( ˄.x 2 ↕ a. 0 ) from Sect. 6.1 .Wehave

[[ Q 1 ]] ⃒ [[ a. 0 ]] because

[[ Q 1 ]] = [[ Q 1 ]] + ʵ

1
2 ·

1
2 ·

˄
−ₒ [[ Q 1 ]] [[ ˄.Q 1 ]] + [[ a. 0 ]]

1
2 ·

1
2 ·

˄
−ₒ

[[ ˄.Q 1 ]] [[ Q 1 ]] + ʵ

1
2 ·

1
2 2 ·

1
2 2 ·

˄
−ₒ

[[ Q 1 ]] [[ ˄.Q 1 ]] + [[ a. 0 ]]

...