Bisimulation for Labelled Markov Processes

Richard Blute, Josée Desharnais, Abbas Edalat, Prakash Panangaden

Abstract


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.

Full Text:

PDF


DOI: http://dx.doi.org/10.7146/brics.v4i4.18783
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.
OK


ISSN: 0909-0878 

Hosted by the Royal Danish Library and Aarhus University Library