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

Chapter 6
Testing Finitary Probabilistic Processes

Abstract In this chapter we extend the results of Chap. 5 from finite to finitary
processes, that is, finite-state and finitely branching processes. Testing preorders
can still be characterised as simulation preorders and admit modal characterisations.
However, to prove these results demands more advanced techniques. A new notion of
weak derivation is introduced; some of its fundamental properties are established. Of
particular importance is the finite generability property of the set of derivatives from
any distribution, which enables us to approximate coinductive simulation relations
by stratified inductive relations. This opens the way to characterise the behaviour
of finitary process by a finite modal logic. Therefore, if two processes are related it
suffices to construct a simulation relation, otherwise a finite test can be constructed
to tell them apart.
We also introduce a notion of real-reward testing that allows for negative re-
wards. Interestingly, for finitary convergent processes, real-reward testing preorder
coincides with nonnegative-reward testing preorder.

Keywords Finitary processes · Testing preorder · Simulation preorder · Modal logic ·

Weak derivation · Finite generability · Real-reward testing

6.1 Introduction

In order to describe infinite behaviour of processes, we extend the language pCSP to
a version of rpCSP with recursive process descriptions; we add a construct rec x.P
for recursion and extend the intensional semantics of Fig. 5.1 in a straightforward
manner. We restrict ourselves to finitary rpCSP processes, having finitely many
states and displaying finite branching.
The simulation relations S and FS given in Sect. 5.5.1 were defined in terms

˄
⃒

of weak transitions between distributions, obtained as the transitive closure of a

˄
−ₒ

relation between distributions that allows one part of a distribution to make a ˄ -

move with the other part remaining in place. This definition is, however, inadequate
for processes that can do an unbounded number of ˄ -steps. The problem is high-
lighted by the process Q 1 = a. 0 ) illustrated in Fig. 6.1 a. Process Q 1

is indistinguishable, using tests, from the simple process a. 0 :wehave Q 1 pmay a. 0
and Q 1 pmust a. 0 . This is because the process Q 1 will eventually perform the action

rec x. ( ˄.x 2 ↕