Logical characterization of probabilistic simulation and bisimulation

Abstract:

Twenty years ago Desharnais and her co-authors proved a striking logical characterization result for probabilistic bisimulation.  This proof applied to systems defined on continuous state spaces and did so with a simpler logic than had hitherto been been used for the discrete case. 

Simulation turned out to be much harder and was only achieved (by Desharnais et al.) as a consequence of approximation theory.  Last year at ICALP a new proof of the logical characterization of simulation was given by Fijalkow, Klin and me.  This proof used some new (to us) ideas from descriptive set theory and gave proofs for simulation and bisimulation that were closely parallel.  Along the way a new game theoretic way of thinking about bisimulation and simulation was developed.  In this talk I will summarize the early work and the new results.  This is joint work with Nathanael Fijalkow and Bartek Klin.