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