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

very different way, can be represented in terms of ours by requiring weak derivatives
to be total distributions.

We end this introduction with a brief glimpse at our proof strategy. In Chap. 5,
the characterisations for finite rpCSP processes were obtained using a probabilistic
extension of the Hennessy-Milner logic. Moving to recursive processes, we know
that process behaviour can be captured by a finite modal logic only if the underlying
labelled transition system (LTS) is finitely branching, or at least image-finite [ 5 ].
Thus to take advantage of a finite probabilistic Hennessy-Milner logic, we need
a property of pLTSs corresponding to finite branching in LTSs; this is topological
compactness, whose relevance we now sketch.
Subdistributions over (derivatives of) finitary rpCSP processes inherit the
standard (complete) Euclidean metric. One of our key results is that

Theorem 6.1 For every finitary rpCSP process P , the set { ʔ | [[ P ]] ⃒ ʔ } is

convex and compact.
Indeed, using techniques from the theory of Markov decision processes [ 6 ], we
can show that the potentially uncountable set is nevertheless the

convex closure of a finite set of subdistributions, from which Theorem 6.1 follows.
This key result allows an inductive characterisation of the simulation preorders
S and

{ ʔ | [[ P ]] ⃒ ʔ }

FS , here defined using our novel weak derivation relation ⃒

. 1

We first

S

construct a sequence of approximations for k ≥ 0 and, using Theorem 6.1 ,we

prove

Theorem 6.2 For every finitary rpCSP process P , and for every k ∈ N , the set

k

{ ʔ | [[ P ]]

S ʔ }

is convex and compact.
This in turn enables us to use the Finite Intersection Property of compact sets to
prove

k
S

Theorem 6.2 For finitary r pCSP processes we have P S Q iff P Q for all

k 0 .

Our main characterisation results can then be obtained by extending the proba-
bilistic modal logic used in Sect. 5.6, so that, for example,

≥

k
S

• it characterises for every k ≥ 0, and therefore it also characterises S ;

• every probabilistic modal formula can be mimicked by a may-test.

Similar results accrue for must testing: details are given in Sect. 6.7 .

1 When restricted to finite processes, the new definitions of simulation and failure simulation pre-
orders degenerate into the preorders in Sect. 5.5.1. So the extension is conservative and justifies our
use of the same symbols S and FS in this chapter.