Monday, April 21, 2008
3:30 PM - note special time
5130 Upson Hall
  Theory Seminar
Spring 2008

CS 789

Prakash Panangaden
McGill University


 Bisimulation and Metrics for Labelled Markov Processes


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. I will discuss the limitations of bisimulation and discuss metrics analogues for bisimulation.