Paper: Bisimulation for Labelled Markov Processes (at LICS 1997)

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

BibTeX

  @InProceedings{BluteDesharnaisEdal-BisimulationforLabe,
    author = 	 {Richard Blute and Josée Desharnais and Abbas Edalat and Prakash Panangaden},
    title = 	 {Bisimulation for Labelled Markov Processes},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS 1997)},
    year =	 {1997},
    month =	 {June}, 
    pages =      {149--158},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }