Queen Mary University of London, Thursday 6th, 2017
Why?
Probabilistic Bisimulation
(due to Larsen, Skou 91)
Bisimulation for Non-Deterministic Systems
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
Reasoning on Traces
Are two Markov Chains trace 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 trace 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$ trace 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'$.
From Traces to Bisimulation on Distributions
Theorem (folklore): For Markov Chains, bisimilarity on distributions is the same as trace 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.
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
