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

we have some ʘ k

FS ) † ʘ k . By Proposition 6.7 ,we
have to find some ʘ ∞ such that ʘ ⃒ ʘ ∞ and ʔ (

satisfying ʘ ⃒ ʘ k

k

and ʔ (

k

FS ) † ʘ ∞ . This can be done

exactly as in the proof of Theorem 6.14 .

6.7.2 The Modal Logic

We add to the modal language given in Sect. 5.6 a new constant div , representing

the ability of a process to diverge. The extended language, still written as

F

F in this

chapter, has the set of modal formulae defined inductively as follows:

• div , ∈ F ,

• ref ( X ) ∈ F when X ↆ Act ,

• a ˕ ∈ F when ˕ ∈ F and a ∈ Act ,

• ˕ 1 ∧ ˕ 2 ∈ F when ˕ 1 , ˕ 2 ∈ F ,

• ˕ 1 p ↕ ˕ 2 ∈ F when ˕ 1 , ˕ 2 ∈ F and p ∈ [0, 1].

Relative to a given pLTS S , Act ˄ , ₒ the satisfaction relation |= ↆ D sub ( S ) × F is

given by:

|= ∈ D sub ( S ),

• ʔ for any ʔ

• ʔ |= div iff ʔ ⃒ ʵ ,

X

• ʔ |= ref ( X )iff ʔ ⃒ −ₒ ,

a
⃒ |=

˕ iff there is a ʔ with ʔ ʔ and ʔ |=

• ʔ a ˕ ,

|=

˕ 1 ∧

|= |=

• ʔ ˕ 2 iff ʔ ˕ 1 and ʔ ˕ 2 ,

• |=

˕ 1 p ↕ ˕ 2 iff there are ʔ 1 , ʔ 2 ∈ D sub ( S ) with ʔ 1 |= ˕ 1 and ʔ 2 |= ʔ ˕ 2 , such

ʔ 2 .
We write ʘ F ʔ when ʔ |= ˕ implies ʘ |= ˕ for all ˕ ∈ F

that ʔ ⃒ p · ʔ 1 + (1 − p ) ·

—note the oppos-
ing directions. This is because the modal formulae express “bad” properties of our
processes, ultimately divergence and refusal; thus ʘ F ʔ means that any bad thing
implementation ʔ does must have been allowed by the specification ʘ .
For rpCSP processes, we use P F Q to abbreviate [[ P ]] F [[ Q ]] in the pLTS

given in Sect. 6.2 .
The set of formulae used here is obtained from that in Sect. 5.6 by adding one
operator, div . But the interpretation is quite different, as it uses the new silent move
relation . As a result, our satisfaction relation no longer enjoys a natural, and

expected, property. In the nonprobabilistic setting if a recursive CCS process P
satisfies a modal formula from the Hennessy-Milner logic, then there is a recursion-
free finite unwinding of P that also satisfies it. Intuitively, this reflects the fact that
if a nonprobabilistic process does a bad thing, then at some (finite) point it must
actually do it. But this is not true in our new, probabilistic setting: for example, the
process Q 1 given in Example 6.8 can do an a and then refuse anything; but all finite
unwindings of it achieve that with probability strictly less than one. That is, whereas
[[ Q 1 ]]

⃒

|= a , no finite unwinding of Q 1 will satisfy a .