Probabilistic Bisimulation - Semantics of Probabilistic Processes: An Operational Approach - page 22

Chapter 3
Probabilistic Bisimulation

Abstract We introduce the operational model of probabilistic labelled transition
systems, where a state evolves into a distribution after performing some action. To
define relations between distributions, we need to lift a relation on states to be a
relation on distributions of states. There is a natural lifting operation that nicely cor-
responds to the Kantorovich metric, a fundamental concept used in mathematics to
lift a metric on states to a metric on distributions of states, which is also related to
the maximum flow problem in optimisation theory.
The lifting operation yields a neat notion of probabilistic bisimulation, for which
we provide logical, metric and algorithmic characterisations. Specifically, we ex-
tend the Hennessy-Milner logic and the modal mu-calculus with a new modality,
resulting in an adequate and an expressive logic for probabilistic bisimilarity. The
correspondence of the lifting operation and the Kantorovich metric leads to a charac-
terisation of bisimulations as pseudometrics that are postfixed points of a monotone
function. Probabilistic bisimilarity also admits both partition refinement and “on-
the-fly” decision algorithms; the latter exploits the close relationship between the
lifting operation and the maximum flow problem.

Keywords Probabilistic labelled transition system · Lifting operation · Probabilistic

bisimulation · Modal logic · Algorithm

3.1 Introduction

In recent years, probabilistic constructs have been proven useful for giving quantita-
tive specifications of system behaviour. The first papers on probabilistic concurrency
theory [ 1 - 3 ] proceed by replacing nondeterministic with probabilistic constructs.
The reconciliation of nondeterministic and probabilistic constructs starts with [ 4 ]
and has received a lot of attention in the literature [ 5 - 22 ]. It could be argued that it
is one of the central problems of the area.
Also we shall work in a framework that features the coexistence of probability
and nondeterminism. More specifically, we deal with probabilistic labelled transition
systems (pLTSs) [ 19 ] that are an extension of the usual labelled transition systems
(LTSs) so that a step of transition is in the form s

a
−ₒ ʔ , meaning that state s can

perform action a and evolve into a distribution ʔ over some successor states. In this