Labelled Markov Processes

Prakash Panangaden

(McGill University)

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 unquantified nondeterminism nondeterminism. This
result was proved in 1998 by Desharnais, Edalat and myself. Since then the
subject has been actively developed by several groups including the
development of a coalgebraic viewpoint culminating by several people
including researchers at Indiana. I will end with a survey of recent
developments involving metrics and approximation techniques.

Tuesday 3rd May 2011, 14:00
Robert Recorde Room
Department of Computer Science