TY - JOUR AU - Blute, Richard AU - Desharnais, Josée AU - Edalat, Abbas AU - Panangaden, Prakash PY - 1997/01/04 Y2 - 2024/03/29 TI - Bisimulation for Labelled Markov Processes JF - BRICS Report Series JA - BRICS VL - 4 IS - 4 SE - Articles DO - 10.7146/brics.v4i4.18783 UR - https://tidsskrift.dk/brics/article/view/18783 SP - AB - In this paper we introduce a new class of labelled transition systems<br />- Labelled Markov Processes - and define bisimulation for them.<br />Labelled Markov processes are probabilistic labelled transition systems<br />where the state space is not necessarily discrete, it could be the<br />reals, for example. We assume that it is a Polish space (the underlying<br />topological space for a complete separable metric space). The mathematical<br /> theory of such systems is completely new from the point of<br />view of the extant literature on probabilistic process algebra; of course,<br />it uses classical ideas from measure theory and Markov process theory.<br />The notion of bisimulation builds on the ideas of Larsen and Skou and<br />of Joyal, Nielsen and Winskel. The main result that we prove is that<br />a notion of bisimulation for Markov processes on Polish spaces, which<br />extends the Larsen-Skou denition for discrete systems, is indeed an<br />equivalence relation. This turns out to be a rather hard mathematical<br />result which, as far as we know, embodies a new result in pure probability<br />theory. This work heavily uses continuous mathematics which<br />is becoming an important part of work on hybrid systems. ER -