Minimising the Probabilistic Bisimilarity Distance

TL;DR

This work studies how to minimise the probabilistic bisimilarity distance between the induced labelled Markov chains that arise from labelled MDPs, distinguishing between memoryless and general strategies. The distance is defined as the least fixed point of an operator $\Delta$ over couplings of outgoing transitions, tying probabilistic bisimilarity to a quantitative pseudometric $d_{\mathcal{M}}$. The authors prove sharp complexity boundaries: memoryless distance minimisation is $\exists\mathbb{R}$-complete, general distance minimisation is undecidable, and the qualitative distance-$<1$ problem for general strategies is EXPTIME-complete (with NP-complete status for memoryless strategies). These results illuminate the security-relevant problem of probabilistic noninterference under scheduler control and delineate tractable versus intractable regimes, guiding both theory and security-sensitive applications.

Abstract

A labelled Markov decision process (MDP) is a labelled Markov chain with nondeterminism; i.e., together with a strategy a labelled MDP induces a labelled Markov chain. The model is related to interval Markov chains. Motivated by applications to the verification of probabilistic noninterference in security, we study problems of minimising probabilistic bisimilarity distances of labelled MDPs, in particular, whether there exist strategies such that the probabilistic bisimilarity distance between the induced labelled Markov chains is less than a given rational number, both for memoryless strategies and general strategies. We show that the distance minimisation problem is ExTh(R)-complete for memoryless strategies and undecidable for general strategies. We also study the computational complexity of the qualitative problem about making the distance less than one. This problem is known to be NP-complete for memoryless strategies. We show that it is EXPTIME-complete for general strategies.

Figures (6)

• Figure 1: The program from \ref{['ex:non1']} as an MDP. The states $s_0$ and $s_1$ have two available actions, ${\sf m}_0$ and ${\sf m}_1$. The default action ${\sf m}$ for the other states is omitted. Different colours (state labels) indicate the distinct values of the low data. Throughout the paper, transition probabilities out of each action are one unless explicitly specified.
• Figure 2: The program from \ref{['ex:non3']} as an MDP. The states $s_0$ and $s_1$ have two available actions, ${\sf m}_0$ and ${\sf m}_1$. The states $t_0$ and $t_1$ also have two available actions, ${\sf m}_2$ and ${\sf m}_3$. Different colours (state labels) indicate the distinct values of the low data.
• Figure 4: The first part of the MDP $\mathcal{D}$. The $\$$ state is the only one that has nondeterministic choices: it has two available actions, ${\sf m}_x$ and ${\sf m}_y$. The default action ${\sf m}$ for the other states is omitted. Different colours indicate different state labels.
• Figure 5: The second part of the MDP $\mathcal{D}$ is an LMC, constructed from the probabilistic automaton $\mathcal{A}$. The default deterministic action ${\sf m}$ for all states is omitted. The state $(b, q)$ in the MDP $\mathcal{D}$, where $q \in Q$, has the same transitions as the state $(a, q)$; it is labelled with $b$.
• Figure 6: (a) An infinite state LMC $\mathcal{M}$ with an infinite state space $S = \{s_i \mid i \in \{0, 1, 2, \ldots \}\} \cup \{t\}$. All states have the same label except $s_{0}$. The states $s_{0}$ and $t$ are sink states, that is, $\tau(s_{0})(s_{0}) = \tau(t)(t) = 1$. Each $s_{i}$ where $i \in \{1, 2, \ldots\}$ transitions to $s_{i-1}$ with probability $\frac{1}{3}$ and $s_{i+1}$ with probability $\frac{2}{3}$. (b) The Markov chain $\mathcal{C}_{\mathcal{M}}^T$ induced by an arbitrary policy $T$ in which only the states reachable from $(s_1, t)$ are shown. The shown part of $\mathcal{C}_{\mathcal{M}}^T$ is the same for every policy $T$.

Theorems & Definitions (31)

• Example 1
• Example 2
• Example 3
• Lemma 4
• Lemma 5
• Lemma 6
• Theorem 7
• Theorem 8
• Corollary 9
• Lemma 10