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

Chapter 5
Testing Finite Probabilistic Processes

Abstract In this chapter we focus on finite processes and understand testing seman-
tics from three different aspects. First, we coinductively define simulation relations.
Unlike the nonprobabilistic setting, where there is a clear gap between testing and
simulation semantics, here testing semantics is as strong as simulation semantics.
Second, a probabilistic logic is presented to completely determine testing preorders.
Therefore, both positive and negative results can be established. For example, if two
finite processes P and Q are related by may preorder then we can construct a simu-
lation relation to witness this, otherwise a modal formula can be constructed that is
satisfiable by P but not by Q . Moreover, the distinguishing formula can be turned
into a test that P can pass but Q cannot. Finally, for finite processes, both may and
must testing preorders can be completely axiomatised.

Keywords Finite processes · Probabilistic simulation · Testing preorders · Modal

logic · Axiomatisation

5.1 Introduction

To succinctly represent the behaviour of probabilistic processes, we introduce a
simple process calculus that is a probabilistic extension of Hoare's communicating
sequential processes (CSP) [ 1 ], called pCSP .Ithas three choice operators, external
P

Q and a probabilistic choice P p ↕ Q . So a semantic theory for
pCSP will have to provide a coherent account of the precise relationships between
these operators.
We aim to give alternative characterisations of the testing preorders

Q , internal P

pmay and
pmust (cf. Definition 4.4). This problem was addressed previously by Segala in [ 2 ],
but using testing preorders (

pmust ) that differ in two ways from the ones
in [ 3 - 6 ] and ours. First of all, in [ 2 ] the success of a test is achieved by the actual
execution of a predefined success action , rather than reaching of a success state .We
call this an action-based approach, as opposed to the state-based approach used in
this topic. Second, [ 2 ] employs a countable number of success actions instead of a
single one, so this is vector-based , as opposed to scalar testing. Segala's results in
[ 2 ] depend crucially on this form of testing. To achieve our current results, we need
vector-based testing preorders as a stepping stone. We relate them to ours by using

pmay and