### Bisimulation for Labelled Markov Processes

#### 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.

- 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:

PDFDOI: http://dx.doi.org/10.7146/brics.v4i4.18783

ISSN: 0909-0878

Hosted by the State and University Library and Aarhus University Library