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

6.6.1 Two Equivalent Definitions and Their Rationale

Let ʔ and its variants be subdistributions in a pLTS S , Act ˄ , ₒ .For a ∈ Act ,

a
−ₒ

a
⃒ ʔ whenever ʔ ʔ pre ʔ post ʔ . Extend this to Act ˄ by write ʔ ⃒ ⃒

˄
⃒

allowing as a special case that is simply ⃒ , that is, including identity (rather

˄
−ₒ

than requiring at least one ). For example, referring to Example 6.4 we have

a
⃒

a
⃒

A

1

[[ Q 1 ]] [[ 0 ]], while in Example 6.5 we have [[ s 2 ]]

2 [[ 0 ]] a n d [[ s 2 ]]

⃒ −ₒ

1

for any set A not containing a , because s 2 ⃒

2 [[ a. 0 ]] .
Definition 6.19 (Failure Simulation Preorder) Define

FS to be the largest

relation in D sub ( S ) × D sub ( S ) such that if ʘ FS ʔ then

( i p i ʔ i ), for ʱ Act ˄ and certain p i with i p i ≤

ʱ
⃒

1. whenever ʔ ∈ 1, then

( i p i ʘ i ) and ʘ i FS ʔ i for each i , and

ʱ
⃒ there are ʘ i ∈ D sub ( S ) with ʘ

A A

2. whenever ʔ ⃒ −ₒ then also ʘ ⃒ −ₒ .

Sometimes we write ʔ FS ʔ .

In the first case of the above definition, the summation is allowed to be empty,
which has the following useful consequence.

FS ʘ for ʘ

Lemma 6.20 If ʘ FS ʔ and ʔ diverges, then also ʘ diverges.

⃒ FS ʔ we can take the

Proof Divergence of ʔ means that ʔ ʵ , whence with ʘ

Although the regularity of Definition 6.19 is appealing—for example it is trivial
to see that

⃒

empty summation in Definition 6.19 to conclude that also ʘ ʵ .

FS is reflexive and transitive, as it should be—in practice, for specific
processes, it is easier to work with a characterisation of the failure simulation preorder
in terms of a relation between states and distributions.

e
FS

Definition 6.20 (Failure Similarity) Define to be the largest binary relation

e

in S × D sub ( S ) such that if s

FS ʘ then

ʱ
⃒

ʱ
⃒ ʔ , for ʱ Act ˄ , then there is a ʘ ∈ D sub ( S ) with ʘ ʘ

1. whenever s ∈

F S ) † ʘ , and
2. whenever s

and ʔ (

e

A A

⃒ −ₒ then ʘ ⃒ −ₒ .

Any relation R ↆ S × D sub ( S ) that satisfies the two clauses above is called a failure

simulation .
This is very close to Definition 5.4. The main difference is the use of the weak
transition s

ʱ
⃒

˄
⃒

ʔ . In particular, if s ʵ , then ʘ has to respond similarly by the

˄
⃒

transition ʘ ʵ .

Obviously, for any failure simulation

e

R we have R ↆ

FS . The following two

FS ) †

e

lemmas show that the lifted failure similarity relation ( ↆ D sub ( S ) × D sub ( S )

has simulating properties analogous to 1 and 2 above.

ʱ
⃒

ʱ
⃒

FS ) † ʘ and ʔ

e

ʔ for ʱ ʘ

Lemma 6.21 Suppose ʔ ( ∈ Act ˄ . Then ʘ

FS ) † ʘ .

for some ʘ such that ʔ (

e