Logic Colloquium: A Logical Characterization of Probabilistic Bisimulation

Colloquium | December 2 | 4:10-5:15 p.m. | 60 Evans Hall

 Prakash Panangaden, School of Computer Science, McGill University

 Group in Logic and the Methodology of Science

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 probabilistic bisimulation for such systems and a logical characterization for it. The 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 traditional situation with Kripke structures where van Benthem and Hennessy and Milner characterized bisimulation using negation in an essential way.