Logic in Computer Science, Symposium on (1997)

Warsaw, POLAND

June 29, 1997 to July 2, 1997

ISSN: 1043-6871

ISBN: 0-8186-7925-5

pp: 149

Abbas Edalat , Imperial College of Science

Prakash Panangaden , Aarhus University

Josee Desharnais , McGill University

Richard Blute , University of Ottawa

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

INDEX TERMS

CITATION

Abbas Edalat,
Prakash Panangaden,
Josee Desharnais,
Richard Blute,
"Bisimulation for Labelled Markov Processes",

*Logic in Computer Science, Symposium on*, vol. 00, no. , pp. 149, 1997, doi:10.1109/LICS.1997.614943SEARCH