Personal tools
You are here: Home Events Prof Prakash Panangaden's lectures - Bisimulation, Approximation and Metrics for Labelled Markov Processes

Prof Prakash Panangaden's lectures - Bisimulation, Approximation and Metrics for Labelled Markov Processes

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. Probabilistic bisimulation was studied by Larsen and Skou in the late 1980s and early 1990s. Starting in the mid 1990s I worked with several people (Josee Desharnais, Abbas Edalat, Rick Blute, Radha Jagadeesan, Vineet Gupta, Vincent Danos) to extend this study to systems with continuous state spaces. This necessitates working with measure theory. In quantitative systems it is desirable to think of equivalence relations more quantitatively and the appropriate quantitative analogue of equivalence is a pseudometric. My coworkers and I have worked on metric analogues of bisimulation. Finally, in order to make contact with the tools developed for finite-state systems -- and for other reasons -- it is necessary to have a theory of approximation. We have also developed such theories over the years most recently in joint work with Philippe Chaput, Vincent Danos and Gordon Plotkin. In this series of 4 lectures I will discuss some of these developments. First, I will give a lecture on background on measure and probability theory. In the second lecture I give the logical characterization of bisimulation. In the third I will describe part of the approximation theory and finally I will give an introduction to metrics. The talks will be designed to be accessible to graduate students interested in probabilistic systems and are not intended for experts. Of course, I cannot cover everything, but I hope to provide a starting point for those who might be considering research in this area or who are working in related areas (quantum computation, systems biology, performance evaluation, theory).

  

Prof. Prakash Panangaden, McGill University, SICSA Distinguished Visiting Fellow

  

Title: Bisimulation, Approximation and Metrics for Labelled Markov Processes

 

Lecture 1 (12/07/2011)

Background on measure and probability theory

Video

 

Lecture 2 (19/07/2011)

The Giry monad and stochastic relations.

Video


I will describe a categorical approach to probability due originally to Lawvere and developed by Giry.  One can define a monad on the category of measurable spaces which behaves very much like the probabilistic analogue of the powerset.  From this one can define a natural notion of stochastic relations and then labelled Markov processes appear as co-algebras for Giry's functor.  I will discuss probabilistic semantics for a language of while loops and Kozen's duality.

This will complete what I thought I could cover in the first lecture.  In the third lecture I will give the logical characterization of bisimulation and in the fourth I will discuss metrics.  I will not be able to cover approximation theory as I had hoped.

 

Lecture 3 (26/07/2011)

Logical Characterization of Bisimulation

Video


I will define (strong probabilistic) bisimulation for reactive processes on analytic spaces.  I will also introduce a very parsimonious modal logic with no negative constructs at all and show that this logic characterizes bisimulation.  The proof involves some special properties of analytic spaces; accordingly I will define these spaces and state the relevant properties.  I will also define the dual concept of co-bisimulation and the related notion of event bisimulation which is, perhaps, more pertinent for probabilistic systems.  The first part is joint work with Josée Desharnais, Abbas Edalat, Vineet Gupta and Radha Jagadeesan while the second is with Vincent Danos, Josée Desharnais and François Laviolette.

 

Lecture 4 (2/8/2011)

Metrics for Labelled Markov Processes

Video

 

The use of equivalence relations like bisimulation for processes that depend on numerical parameters, for example, real-time or probabilistic systems, has been criticized on the grounds that a slight variation in the numerical parameters may make a drastic change in the relationship between two systems.  It behooves us to find a concept better adapted to the needs of quantitative reasoning.  Metrics are just the right concept for dealing with this situation.  In this talk I will define a quasimetric whose kernel is bisimulation.  It builds on ideas from optimization theory, specifically the Kantorovich metric defined in the context of optimal transport problems.  This work was joint with Josee Desharnais, Vineet Gupta and Radha Jagadeesan and has been greatly enriched by the contributions of James Worrell and Franck van Breugel.

 

Document Actions