Labelled Markov Processes (LMPs) are a combination of traditional labelled transition systems and Markov processes. Discrete versions of such systems have been around for a while and were thoroughly explored by Larsen and Skou in the late 1980s and early 1990s. Our contribution has been to extend this study to systems with continuous state spaces.

The main technical contribution that I will discuss in this talk is a definition of bisimulation for such systems and a logical characterization for bisimulation. The big surprise is that a very simple modal logic with no negative constructs or infinitary conjunctions suffices to characterize bisimulation, even with uncountable branching. This is quite different from the situation with nondeterminism. This result was proved in 1998 by Desharnais, Edalat and myself. Since then the subject has been actively developed by several groups. I will end with a survey of recent developments.