Introduction - Semantics of Probabilistic Processes: An Operational Approach - page 4

Chapter 3 introduces an operational model of probabilistic systems called
probabilistic labelled transition systems . In this model, a state might make a non-
deterministic choice among a set of available actions. Once an action is taken, the
state evolves into a distribution over successor states. Then in order to compare
the behaviour of two states, we need to know how to compare two distributions.
There is a nice lifting operation that turns a relation between states into a relation
between distributions. This operation is closely related to the Kantorovich metric
in mathematics and the network flow problem in optimisation theory. We give an
elementary account of the lifting operation because it entails a neat notion of prob-
abilistic bisimulation that can be characterised by behavioural pseudometrics and
decided by polynomial algorithms over finitary systems. We also provide modal char-
acterisations of the probabilistic bisimulation in terms of probabilistic extensions of
the Hennessy-Milner logic and the modal mu-calculus .
Starting from Chap. 4 we investigate the testing semantics of probabilistic pro-
cesses. We first set up a general testing framework that can be instantiated into a
vector-based testing or scalar testing approach, depending on the number of actions
used to indicate success states. A fundamental theorem is that for finitary systems
the two approaches are equally powerful. In order to prove this result we make use
of a notion of reward testing as a stepping stone. The separation hyperplane theorem
from discrete geometry plays an important role in the proof.
Chapter 5 investigates the connection between testing and simulation semantics.
For finite processes , i.e. processes that correspond to probabilistic labelled transition
systems with finite tree structures, testing semantics is not only sound but also com-
plete for simulation semantics. More specifically, may testing preorder coincides
with simulation preorder and must testing preorder coincides with failure simula-
tion preorder. Therefore, unlike the traditional (nonprobabilistic) setting, here there
is no gap between testing and simulation semantics. To prove this result we make
use of logical characterisations of testing preorders. For example, each state s has
a characteristic formula ˆ s in the sense that another state t can simulate s if and
only if t satisfies ˆ s . We can then turn this formula ˆ s into a characteristic test T s so
that if t is not related to s via the may testing preorder then T s is a witness test that
distinguishes t from s . Similarly for the case of failure simulation and must testing.
We also give a complete axiom system for the testing preorders in the finite fragment
of a probabilistic CSP. This chapter paves the way for the next chapter.
In Chap. 6 we extend the results in the last chapter from finite processes to finitary
processes , i.e. processes that correspond to probabilistic labelled transition systems
that are finite-state and finitely branching possibly with loops. The soundness and
completeness proofs inherit the general schemata from the last chapter. However, the
technicalities are much more subtle and more interesting. For example, we make a
significant use of subdistributions. A key topological property is that from any given
subdistribution, the set of subdistributions reachable from it by weak transitions can
be finitely generated. The proof is highly nontrivial and involves techniques from
Markov decision processes such as rewards and static policies. This result enables us
to approximate coinductively defined relations by stratified inductive relations. As a