Labelled Markov Processes (LMPs) are a combination of traditional labelled transition systems and Markov processes and are closely related to Markov Decision Processes (MDPs). They model systems featuring stochasticity as well as interaction with an external environment. Bisimulation is an equivalence relation that captures the idea of two systems that ``behave the same;'' it was introduced by Milner and Park in the early 1970s in their studies of concurrent systems. Probabilistic bisimulation was studied 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 pure internal nondeterminism. This is quite old work and was done jointly with Josee Desharnais and Abbas Edalat in 1998.