Probabilistic Bisimulation

Bisimulation for Stochastic Systems

Nathanaël Fijalkow

Formerly: University of Oxford, UK
Now: Research Fellow @ Simons
Next: Alan Turing Institute of Data Science, London, UK

Simons Institute for the Theory of Computing, Berkeley, November 7th, 2016

Induces a function $\ f : A^* \to [0,1]$

A strategy $\ \sigma : (Q \times A)^* \to \mathcal{D}(Q)$ induces a Markov Chain

Reasoning about Stochastic Models

Are two Labelled Markov Chains ($\Delta : Q \times A \to \mathcal{D}(Q)$) equivalent?
Decidable in PTIME (Schützenberger 61)

Given an MDP $M_1$ and a MC $M_2$, does there exist a strategy for $M_1$ making them equivalent?
Decidable in coNP (F., Kiefer, Shirmohammadi, FoSSaCS'16)

Given an MDP $M_1$ and a MC $M_2$, are $M_1$ and $M_2$ equivalent for all strategies of $M_1$?
Undecidable (F., Kiefer, Shirmohammadi, FoSSaCS'16)

Key Notion: Bisimulation on Distributions

(due to Hermanns, Krčál, Křetı́nský 2014)

Defined for MDP: $\Delta : Q \times A \to \text{Conv}(\mathcal{D}(Q))$

If $\delta \equiv \delta'$, then for all $a$ in $A$:

for all $\tau$ in $\Delta(\delta,a)$, there exists $\tau'$ in $\Delta(\delta',a)$ with $\tau \equiv \tau'$,
for all $\tau'$ in $\Delta(\delta',a)$, there exists $\tau$ in $\Delta(\delta,a)$ with $\tau \equiv \tau'$.

Theorem (folklore): $M_1,M_2$ two Labelled Markov Chains, bisimilarity on distributions is the same as equivalence.

Theorem (F., Kiefer, Shirmohammadi, FoSSaCS'16):

Given MDP $M_1$ and MC $M_2$, $M_1$ bisimilar on distributions to $M_2$ iff $M_1$ can be refined into $M_2$.
Bisimulation on distributions is decidable in coNP.

My Copernican Revolution about Probabilistic Bisimulation

Probabilistic Bisimulation

(due to Larsen, Skou 91)

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

Definition: If $p \equiv q$, then for all $a$ in $A$, for all $C$ equivalence class of $\equiv$, $$\Delta(p,a,C) = \Delta(q,a,C)$$

The two bisimulations are different

Probabilistic Bisimulation

(due to Larsen, Skou 91)

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

Definition: If $p \equiv q$, then for all $a$ in $A$, for all $C$ equivalence class of $\equiv$, $$\Delta(p,a,C) = \Delta(q,a,C)$$

Spoiler and Duplicator

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

Definition: if $p \equiv q$, then for all $a$ in $A$, for all $C$ equivalence class of $\equiv$, $$\Delta(p,a,C) = \Delta(q,a,C)$$
Equivalent 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

Logical characterisation

Extension to distances

Extension to simulation with approximation techniques

Extension to infinite and continuous-time Markov Chains

What are the properties of the new planet?

Two notions

$M_1,M_2$ two MDP

Trace refinement: there exists a strategy for $M_1$, such that for all strategies for $M_2$, they are equivalent, and the other way around
Bisimulation on Distribution

Logical Characterisations

\[ \phi\ =\ \top\ \mid\ \phi \wedge \phi\ \mid\ \langle a \rangle \phi\ \mid\ \Sigma_{\ge p} \text{ for } p \in \mathbb{Q} \] Theorem: (F., Klin @ Simons) Two distributions are bisimiliar if, and only if, they satisfy the same formulas of this logic

\[ \phi\ =\ \Sigma_{\ge p} \wedge \bigwedge_{a \in S} \langle a \rangle \phi \text{ for } p \in \mathbb{Q} \text{ and } S \subseteq A \text{ finite.} \] Theorem: (F., Klin @ Simons) Two distributions trace refine each other if, and only if, they satisfy the same formulas of this fragment

The relation corresponding to the fragment is undecidable, the one corresponding to the full logic is decidable!