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

Theorem 4.7 from the last chapter saying that for finitary processes the preorders

pmay pmust

pmust . We will proceed in two steps:
finite processes are considered in this chapter and finitary processes, which may
have loops, are dealt with in Chap. 6.
We will first introduce the syntax and operational semantics of the language pCSP
and then instantiate the general testing framework in Sect. 4.1 to pCSP processes.
In Sect. 5.5 we use the transitions s

and coincide with pmay and

ʱ
−ₒ

ʔ to define two coinductive preorders,
the forward simulation (or simply called simulation ) preorder S [ 7 , 8 ], and the

FS over pCSP processes. The latter extends the failure
simulation preorder of [ 9 ] to probabilistic processes. Both preorders use a natural
generalisation of the transitions, first to take the form ʔ

failure simulation preorder

ʱ
−ₒ ʔ , and then to weak

ʱ
⃒ ʔ . The second preorder differs from the first one in the use of a

failure predicate s

versions ʔ

X
−ₒ

, indicating that in the state s none of the actions in X can be

performed.
Both preorders are preserved by all the operators in pCSP , and are sound with
respect to the testing preorders; that is P S Q implies P pmay Q and P FS Q implies

P pmust Q . The soundness is proved in a very standard method. But completeness ,

that the testing preorders imply the respective simulation preorders, requires some
ingenuity. We prove it indirectly, involving a characterisation of the testing and
simulation preorders in terms of a modal logic.
Our modal logic, defined in Sect. 5.6 , uses conjunction ˕ 1 ∧ ˕ 2 , the modality

˕ from the Hennessy-Milner Logic, and a probabilistic construct ˕ 1 p ↕ ˕ 2 .A
satisfaction relation between processes and formulae then gives, in a natural manner,
a logical preorder between processes: P

a

L Q means that every

L formula satisfied

L coincides with S (and hence pmay

by P is also satisfied by Q . We establish that

also).
To capture failures, we add, for every set of actions X , a formula ref ( X )toour
logic, satisfied by any process that, after it can do no further internal actions, can
perform none of the actions in X either. The constructs , and ref stem from

the modal characterisation of the nonprobabilistic failure simulation preorder, given
in [ 9 ]. We show that

a

pmust , as well as FS , can be characterised in a similar manner

with this extended modal logic.
We prove these characterisation results through two cycles of inclusions:

L ↆ S ↆ pmay =

pmay

ↆ L

F

pmust ↆ F
Sect. 5.6

ↆ FS ↆ pmust =

Sect. 5.5 Sect. 4.1 Sect. 4.7 Sect. 5.7

L Q implies P

In Sect. 5.6 we show that P S Q (and hence P pmay Q ), and likewise

FS ; the proof involves constructing, for each pCSP process P ,a
characteristic formula ˕ P . To obtain the other direction, in Sect. 5.7 we show how
every modal formula ˕ can be captured, in some sense, by a test T ˕ ; essentially the
ability of a pCSP process to satisfy ˕ is determined by its ability to pass the test T ˕ .

F

for and