Testing Finite Probabilistic Processes - Semantics of Probabilistic Processes: An Operational Approach - page 131

5.6 A Modal Logic

F of our testing pre-
orders. Besides their intrinsic interest, these logical preorders also serve as a stepping
stone in proving Theorem 5.4 . In this section we show that the logical preorders are
sound with respect to the simulation and failure simulation preorders, and hence with
respect to the testing preorders; in the next section we establish completeness. To
start with, we define a set

L and

In this section, we present logical characterisations

F of modal formulae, inductively, as follows:

• ∈ F ,

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

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

• ʔ |= ˕ 1 ∧ ˕ 2 iff ʔ |= ˕ 1 and ʔ |= ˕ 2 ,

• [0, 1].

We often use the generalised probabilistic choice operator i ∈ I p i ·

˕ 1 p ↕ ˕ 2 ∈ F when ˕ 1 , ˕ 2 ∈ F and p ∈

˕ i , where I is a

nonempty finite index set, and i ∈ I p i =

1. This can be expressed in our language
by nested use of the binary probabilistic choice.
The satisfaction relation |= ↆ D ( sCSP ) × F is given by:

|= ∈ D

• ʔ for any ʔ ( S ),

X
−ₒ

˄
⃒

ˆ

ref ( X ) iff there is a ʔ with ʔ ʔ and ʔ

• ʔ |= ,

a
⃒ ʔ and ʔ |= ˕ ,

ˆ

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

•

• ʔ |= ˕ 1 ∧ ˕ 2 iff ʔ |= ˕ 1 and ʔ |= ˕ 2 ,

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

˄
⃒

ʔ p · ʔ 1 + (1 − p ) · ʔ 2 .

Let L be the subclass of F obtained by skipping the ref ( X ) clause. We shall write

L Q just when [[ P ]] F Q just when

P |= ˕ implies [[ Q ]] |= ˕ for all ˕ ∈ L , and P

[[ P ]] |= ˕ is implied by [[ Q ]] |= ˕ for all ˕ ∈ F (Note the opposing directions).

Remark 5.1 Compared with the two-sorted logic in Sect. 3.6.1, the logic F and its

sublogic drop state formulae and only contain distribution formulae. The reason is

that we will characterise failure simulation preorder and simulation preorder. Both
of them are distribution-based and strictly coarser than the state-based bisimilarity
investigated in Chap. 3.
In order to obtain the main result of this section, Theorem 5.5 , we introduce the
following tool.

L

F ∈ sCSP or

Definition 5.7 The -characteristic formula ˕ s or ˕ ʔ of a process s

∈ D

( sCSP ) is defined inductively: ʔ

= s

a
−ₒ}

˄
−ₒ

• ˕ s :

−ₒ ʔ

a ˕ ʔ ∧ ref ( { a | s )if s ,

a

= s

˕ ʔ ∧ s

−ₒ ʔ

• ˕ s : a

−ₒ ʔ ˕ ʔ otherwise,

a ˄

= s ∈ ʔ

• ˕ ʔ : ʔ ( s ) · ˕ s .