Simulation and Bisimulations for Probabilistic Systems, and their Logical Contents

on YouTube ↗28m

" summary

Defines models (labeled Markov chains, labeled MDPs with convex choices) and works on equivalence of the induced probability functions. Shows equality of two labeled Markov chains is decidable; existence of a strategy making an MDP match a Markov chain is decidable in coNP while the universal‑strategy version is undecidable. Recasts a distribution‑level notion of bisimulation on distributions as a spoiler/duplicator game, gives a PTIME algorithm and a modal logic that exactly characterizes distinguishability; a syntactic fragment corresponds to trace refinement and is undecidable.

AI-written summary · about

" chapters (8)

1. 0:00Intro
2. 0:12Bisimulation for Stochastic Systems
3. 5:53Reasoning about Stochastic Models
4. 9:09Key Notion: Bisimulation on Distributions
5. 13:35The two bisimulations are different
6. 15:11Spoiler and Duplicator
7. 17:1325 years of research on Probabilistic Bisimulation
8. 20:26Logical Characterisations