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

Example 6.12 Consider the finite state but infinitely branching pLTS containing
three states s 1 , s 2 , s 3 and the countable set of transitions given by

˄
−ₒ

( s 2 2 n ↕

≥

s 1 s 3 ) n 1

For convenience, let ʔ n denote the distribution ( s 2 2 n ↕ s 3 ). Then { ʔ n | n ≥ 1 } is a

Cauchy sequence with limit s 3 . Trivially the set contains every ʔ n ,

but it does not contain the limit of the sequence, thus it is not closed.

{ ʔ | s 1 ⃒ ʔ }

Example 6.13 By adapting Example 6.12 , we obtain the following pLTS that
is finitely branching but has infinitely many states. Let t 1 and t 2 be two distinct
states. Moreover, for each n

≥ 1 , there is a state s n with two outgo in g tra ns itions:

˄
−ₒ s n + 1 and s n

˄
−ₒ t 1

s n ↕ t 2 . Let ʔ n denote the distribution t 1 ↕ t 2 . Then

1
2 n

1
2 n

{ ʔ n | n ≥ 1 } is a Cauchy sequence with limit t 2 . Th e set { ʔ | s 1 ⃒ ʔ } is not

closed because it contains each ʔ n but not the limit t 2 .
Corollary 6.6 ( Closure of

a
⃒

) For any state s in a finitary pLTS the set

a
⃒

{ ʔ | s ʔ }

is closed and convex.

Proof We first introduce a preliminary concept. We say a subset D ↆ D sub ( S )is

finitely generable whenever there is some finite set F ↆ D sub ( S ) such that D = F .

A relation R ↆ X × D sub ( S )is finitely generable if for every x in X the set x · R is

finitely generable. We observe that

(i) If a set is finitely generable, then it is closed and convex.
(ii) If R 1 , R 2 ↆ D sub ( S ) × D sub ( S ) are finitely generable then so is their composition

R 1 · R 2 .
The first property is a direct consequence of the definition of finite generability. To
prove the second property, we let

i Φ be a finite set of subdistributions such that

B

i Φ for i

Φ · R i = B = 1, 2. Then one can check that

2 1

ʔ · ( R 1 · R 2 ) =∪{ B

ʘ |

ʘ ∈ B

ʔ }

which implies that finite generability is preserved under composition of relations.
Notice that the relation

a
−ₒ·⃒

a
⃒ ⃒ ·

is a composition of three stages: .In

the proof of Lemma 6.17 , we have shown that ⃒ is finitely generable. In a finitary

a
−ₒ

pLTS, the relation is also finitely generable. It follows from property (ii) that

a
⃒

a
⃒

is finitely generable. By property (i) we have that is closed and convex.

a
⃒

Corollary 6.7 In a finitary pLTS, the relation is the lifting of the closed and

a
−ₒ⃒

convex relation ⃒ S , where s ⃒ S ʔ means s ⃒ ʔ.

a
−ₒ⃒

a
⃒

Proof The relation ⃒ S is restricted to point distributions. We have

a
⃒

a
−ₒ⃒

shown that is closed and convex in Corollary 6.6 . Therefore, ⃒ S is