Logic in Computer Science, Symposium on (1997)
June 29, 1997 to July 2, 1997
Richard Blute , University of Ottawa
Josee Desharnais , McGill University
Abbas Edalat , Imperial College of Science
Prakash Panangaden , Aarhus University
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 but the state space is a Polish space (the underlying topological space for a complete separable metric space), like the reals. Such systems are increasingly important for the study of hybrid systems. 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 definition 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. The mathematical ideas that we found useful are likely to be part of many future investigations of hybrid stochastic systems.
A. Edalat, P. Panangaden, J. Desharnais and R. Blute, "Bisimulation for Labelled Markov Processes," Logic in Computer Science, Symposium on(LICS), Warsaw, POLAND, 1997, pp. 149.