Bisimulation for Stochastic Systems

Probabilistic Bisimulation

(due to Larsen, Skou 91)

Bisimulation for Non-Deterministic Systems

Bisimulation game: Duplicator claims that $p \equiv q$

• Spoiler: pick $a$ in $A$ and $p' \in Q$ such that $p' \in \Delta(p,a)$
• Duplicator: $q' \in \Delta(q,a)$ and claims $p' \equiv q'$

We say that $p$ and $q$ are bisimilar if Duplicator can play forever

Bisimulation for Labelled Markov Chains

Labelled Markov Chains: $\Delta : Q \times A \to \mathcal{D}(Q)$

Coinductive definition: If $p \equiv q$, then for all $a$ in $A$, for all union of equivalence classes $C$ of $\equiv$, $$\Delta(p,a,C) = \Delta(q,a,C)$$

Bisimulation game: Duplicator claims that $p \equiv q$

• Spoiler: pick $a$ in $A$ and $C \subseteq Q$ such that $\Delta(p,a,C) \neq \Delta(q,a,C)$
• Duplicator: $p'$ in $C$, $q'$ not in $C$ and claim that $p' \equiv q'$

25 years of research on Probabilistic Bisimulation

Computable in PTIME, and PTIME-complete
Extension to distances
Extension to simulation with approximation techniques
Extension to infinite and continuous-time Markov Chains

How to prove that two systems are not bisimilar?

Logical Characterisation

\[ \phi\ =\ \top\ \mid\ \phi \wedge \phi\ \mid\ \langle a \rangle_{> p} \phi\ \] Two Theorems:
- Desharnais, Edalat, Panangaden 1998: the state space is a Polish space, the transition function is measurable and the set of labels is countable
- F., Klin, Panangaden 2017: the state space is a Polish space and the transition function is continuous

Two states are bisimiliar if, and only if, they satisfy the same formulas of this logic