Bisimulation for Labelled Markov Processes

Resumé

In this paper we introduce a new class of labelled transition systems
- Labelled Markov Processes - and define bisimulation for them.
Labelled Markov processes are probabilistic labelled transition systems
where the state space is not necessarily discrete, it could be the
reals, for example. We assume that it is a Polish space (the underlying
topological space for a complete separable metric space). The mathematical
theory of such systems is completely new from the point of
view of the extant literature on probabilistic process algebra; of course,
it uses classical ideas from measure theory and Markov process theory.
The notion of bisimulation builds on the ideas of Larsen and Skou and
of Joyal, Nielsen and Winskel. The main result that we prove is that
a notion of bisimulation for Markov processes on Polish spaces, which
extends the Larsen-Skou denition for discrete systems, is indeed an
equivalence relation. This turns out to be a rather hard mathematical
result which, as far as we know, embodies a new result in pure probability
theory. This work heavily uses continuous mathematics which
is becoming an important part of work on hybrid systems.