Labelled Transition Systems: $\Delta : Q \times A \to \mathcal{P}(Q)$
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 $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
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\
\]
Theorem: (Desharnais, Edalat, Panangaden 98)
Assumptions: the state space is a Polish space and the set of labels is countable
Two states are bisimiliar if, and only if, they satisfy the same formulas of this logic
Why countability of the set of labels?
$p$ and $q$ are not bisimilar
$p$ and $q$ satisfy the same formulas
Logical Characterisation, take 2
\[
\phi\ =\ \top\ \mid\ \phi \wedge \phi\ \mid\ \langle a \rangle_{> p} \phi\
\]
Theorem: (F., Klin, Panangaden)
Assumptions: 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
A strategy induces a Markov Chain
