Title: Approximating Labelled Markov Again!

Speaker: Prakash Panangaden (Oxford University)

Time: 13th April 2015, 10:00

Venue: Seminar Room (334), Level 3, Building 5, Institute of Software, CAS

Abstract:

Markov processes with continuous state spaces or continuous time evolution or both arise naturally in many areas of computer science: robotics, performance evaluation, modelling and simulation for example. For discrete systems there was a pioneering treatment of probabilisitic bisimulation and logical characterizationdue to Larsen and Skou. The continuous case, however, was neglected for a time. For a little over a decade there has been significant activity among computer scientists as it came to be realized that ideas from process algebra, like bisimulation and the existence of a modal characterization, would be useful for the study of such systems. In a paper in 1997 continuous-state Markov processes with labels to capture interactions were christened labelled Markov processes　(LMPs).

A theory of approximation for LMPs was initiated in 1999. Finding finite approximations is vital to give a computational handle on such systems. The previous work was characterized by rather intricate proofs that did not seem to follow from basic ideas in any straightforward way. For example, the logical characterization of (probabilistic) bisimulation proved first in 1998 requires subtle properties of analytic spaces and rather painful constructions. Proofs of basic results in approximation theory also seemed to be more difficult than they should be.

In recent work we take an entirely new approach, in some ways "dual" to the normal view of probabilistic transition systems. We think of a Markov process as a transformer of functions defined on it, rather than as a transformer of the state. This is the probabilistic analogue of working with predicate transformers, a point of view advocated by Kozen in a path-breaking early paper on probabilistic systems and logic from 1985.

This new way of looking at things leads to three new results: 1. It is possible to define bisimulation on general spaces -- not just on analytic spaces -- and show that it is an equivalence relation with easy categorical constructions. The logical characterization of bisimulation can also be done generally, and with no complicated measure theoretic arguments. 2. A new and flexible approach to approximation based on averaging can be given. 3. It is possible to show that there is a minimal bisimulation equivalent to a process obtained as the limit of finite approximants. This is joint work with Philippe Chaput, my former Master's student at McGill University, and with Vincent Danos and Gordon Plotkin of the University of Edinburgh.

Biography:

Prakash Panangaden

Computing Laboratory

Oxford University

on sabbatical leave from

McGill University

Montreal, Canada

Prakash Panangaden primarily works on Markov processes: approximation, metrics, logics and reasoning principles. He also works on aspects of quantum information theory, quantum mechanics, relativity theory, programming languages and modal logics. He got his MSc from IIT Kanpur, an MS from the University of Chicago, his PhD from the University of Wisconsin-Milwaukee all in physics and an MS in computer science from the University of Utah. He has been an assistant professor in computer science at Cornell University, and is currently a professor in the School of　Computer Science at McGill University, Montreal, Canada. He is known for his work on renormalization of quantum field theory in curved spacetime, for semantics of indeterminate dataflow and of concurrent constraint programming, and for some topics in pure mathematics (nuclear ideal systems). He was elected a Fellow of the Royal Society of Canada in 2013 and was honoured by a 60th birthday Symposium organized at Oxford University in 2014.