Minimising the Probabilistic Bisimilarity Distance

TL;DR

This paper investigates the complexity of minimizing probabilistic bisimilarity distances in labelled MDPs, revealing that the problem is computationally hard and undecidable depending on strategy types, with implications for security verification.

Contribution

It establishes the complexity classifications for the distance minimization problem in labelled MDPs, including undecidability and EXPTIME-completeness results.

Findings

Distance minimization is ExTh(R)-complete for memoryless strategies.

The problem is undecidable for general strategies.

Qualitative distance reduction is EXPTIME-complete for general strategies.

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.