Research Fellow @ Alan Turing Institute
Affiliated to Warwick
Short Talks at the Turing, Thursday 2nd March, 2017
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
Coinductive definition: If $p \equiv q$, then for all $a$ in $A$, for all $p' \in \Delta(p,a)$,
there exists $q' \in \Delta(q,a)$ such that $p' \equiv q'$
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)$$
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'$
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?
Find a formula satisfying one but not the other!
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